Jas*_*ker 25 lisp type-theory lambda-calculus
我试图更好地掌握类型如何在lambda演算中发挥作用.不可否认,许多类型理论的东西都在我的头上.Lisp是一种动态类型语言,大致对应于无类型lambda演算？还是有一种我不知道的"动态类型的lambda演算"？
Nor*_*sey 37
Lisp是一种动态类型语言,大致对应于无类型lambda演算？
是的,但只是粗略的.在"纯粹的"无类型lambda演算中,一切都被编码为函数.(你可以谷歌流行的"教会编码"和不太流行的"斯科特编码".)Lisp有非功能性数据,如原子和数字并且这样的,所以这正如计数"无类型演算与常量扩展".
另一个重要的区别是评估顺序.减少lambda演算术语的规则是非常不确定的.(有一个定理,教会罗塞定理,它松散,只要事情终止说,评价的顺序并不重要).在实际拉姆达方面使用最左边最靠外又名"正常秩序"减量化,因为如果一般降低任何减少策略都会终止,那就是.这与Lisp非常不同,Lisp总是在进行beta减少之前评估正常形式的参数.此评估顺序称为"按值调用".
总之,Lisp对应于使用常量扩展的无类型,按值调用的lambda演算.