22 June 2015

lambda calculus

语法

E = x $\lambda$.x E E1 E2
  • 三种形式的lambda表达式 : 变量/函数声明/函数应用.
  • 函数声明时, 函数体尽可能的向右扩展.
  • 函数应用时, 遵循左结合.
  • 多参数lambda表达式通过currying操作变成单参数表达式.

求值

  • Alpha 变换
  • Beta 归约

Y组合子

与图领停机同构. 不动点 : f(x) = x

Y(F) = f, F(f) = f

Y(F) = f = F(f) = F(Y(F)) => 任何函数作F用于Y, 就产生了F的不动点.

Y组合子 : Y(F) = F(Y(F)) => lambda y . (lambda x . y (x x)) (lambda x . y (x x))

定理

歌德尔: 任何足够强到蕴含了皮亚若算术系统(PA)的一致(即无矛盾)的系统都是不完备的, 所谓的不完备也就是说系统内存在一个为真的命题但无法在系统内推导的命题.

第二不完备定理的结论: 一个包含了PA的形式化公理系统永远无法在内部证明其自身的一致(无矛盾)性.

康托尔: 无穷集合, 对角线方法

组合逻辑 -> Lambda算子 SICP 谓词逻辑

«哥德尔、埃舍尔、巴赫——集异璧之大成» g9的博客 : http://blog.csdn.net/g9yuayon