有类型λ演算
维基百科,自由的 encyclopedia
有类型lambda演算是使用lambda符号()指示匿名函数抽象的一种有类型的形式化。有类型lambda演算是基础编程语言并且是有类型的函数式编程语言如ML和Haskell和更间接的指令式编程语言的基础。它们通过Curry-Howard同构密切关联于直觉逻辑并可以被认为是范畴的类的内部语言,比如简单类型lambda演算是笛卡尔闭范畴(CCC)的语言。
此条目没有列出任何参考或来源。 (2017年4月5日) |
传统上,有类型lambda演算被看作无类型lambda演算的精细化。更现代的观点把有类型lambda演算看做更基础的理论,而把无类型lambda演算看作它的只有一个类型的特殊情况。