Lisp可以轻松地举例说明哪种类型的Lambda演算? [英] What type of lambda calculus would Lisp loosely be an example of?

问题描述

我试图更好地掌握类型在lambda演算中的作用.诚然，很多类型理论方面的东西都困扰着我. Lisp是一种动态类型化的语言，它会大致对应于未类型化的lambda演算吗?还是我不知道某种动态类型的lambda演算"?

解决方案

Lisp是一种动态类型化的语言，大致相当于未类型化的lambda演算吗?

是的，但仅是粗略的.在纯"无类型lambda演算中，所有内容都被编码为函数. (您可以在Google上找到流行的"Church编码"和不太流行的"Scott编码".)Lisp具有非功能性数据，例如原子和数字等，因此将被视为用常数扩展的无类型Lambda微积分". /p>

另一个重要区别是评估顺序.减少lambda-演算项的规则是高度不确定的. (有一个定理，Church-Rosser定理，它松散地说，只要事情终止，评估的顺序就没有关系.)实际上，lambda项通常使用最左端的aka正常顺序的约简来简化，因为如果任何减少策略都会终止，而那个策略会终止. 这与Lisp截然不同，Lisp总是在进行beta缩减之前将参数评估为正常形式.此评估顺序称为按值致电".

总而言之，Lisp对应于用常量扩展的无类型按值调用lambda演算.

I'm trying to get a better grip on how types come into play in lambda calculus. Admittedly, a lot of the type theory stuff is over my head. Lisp is a dynamically typed language, would that roughly correspond to untyped lambda calculus? Or is there some kind of "dynamically typed lambda calculus" that I'm unaware of?

解决方案

Lisp is a dynamically typed language, would that roughly correspond to untyped lambda calculus?

Yes, but only roughly. In the "pure" untyped lambda calculus, everything is coded as functions. (You can google for the popular "Church encoding" and the less popular "Scott encoding".) Lisp has non-functional data, like atoms and numbers and such, so this would count as "untyped lambda calculus extended with constants."

Another important difference is in order of evaluation. Rules for reducing lambda-calculus terms are highly nondeterministic. (There's a theorem, the Church-Rosser theorem, which says loosely that as long as things terminate, order of evaluation doesn't matter.) In practice lambda terms are typically reduced using leftmost-outermost aka "normal-order" reduction because if any reduction strategy terminates, that one does. This is very different from Lisp which always evaluates arguments to normal form before doing a beta-reduction. This evaluation order is called "call by value."

In summary, Lisp corresponds to an untyped, call-by-value lambda calculus extended with constants.

这篇关于Lisp可以轻松地举例说明哪种类型的Lambda演算?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！