Lambda Calculus是非经典逻辑中的一种，形式比图灵机模型和一阶谓词逻辑等简洁优雅许多，是函数式编程语言的理论支柱，本文主要简单梳理了untyped Lambda Calculus以及Church数的构造。

Functional Programming Languages

• Properties
  
  • based-on lambda calculus
  • closure(functor) and high-order function
  • lazy evaluation
  • recursion
  • reference transparently
  • no side-effects
  • expression

Lambda Calculus

• Four core components

  • expression
  • variable(value)
  • function
  • application

• Grammar

  • (expression) := (variable) | (function) | (application)
  • (function) := lambda (variable).(expression)
  • (application) := (expression)(expression)
  • examples
    
    • function definition : lambda x.x ==> Identity function I
    • function application : (lambda x.x)(y) = y

• free and bound variables

  • lambda x.xy ==> x bound but y free

• substitution and reduction

  • alpha substitution
  • beta reduction

• numbers definition(Church numbers)

  • S : lambda wyx.y(wyx) (Successor function)
  • 0 : lambda sz.z
  • 1 : lambda sz.s(z)
    
    • S(0) = (lambda wyx.y(wyx))(lambda sz.z)
      = lambda yx.y((lambda sz.z)(y)x)
      = lambda yx.y(x) = 1
  • 2 : lambda sz.s(s(z))
    
    • S(1) = (lambda wyx.y(wyx))(lambda sz.s(z))
      = lambda yx.y((lambda sz.s(z))yx)
      = lambda yx.y((lambda z.y(z))x)
      = lambda yx.y(y(x)) = 2
  • 3 : lambda sz.s(s(s(z)))
  • 3(Func)(var) ==> apply 3 Func times on var

• addition

  • ’+’ : lambda wyx.y(wyx) (successor function)
  • 1 + 2 = 1S(2)
  • (lambda sz.s(z)) (lambda wyx.y(wyx)) (lambda ab.a(a(b))) = (lambda z.(lambda wyx.y(wyx))(z)) (2)
    = (lambda zyx.y(zyx))(2) = S(2)
  • 2 + 2 = 2S(2)
  • (lambda sz.s(s(z))) (lambda wyx.y(wyx)) (2) = (lambda z.S(S(z)))(2) = S(S(2))

• multiplication

  • ’*’ : lambda xyz.x(yz)
  • 1*2 = (lambda abc.a(bc))(1,2) = (lambda bc.1(bc))(2)
    = (lambda c.1(2(c)))
    = (lambda c.(lambda sz.s(z))(lambda sz.s(s(z)))(c))
    = lambda c.(lambda cz.c(c(z))) = 2

• Condition

  • T : lambda xy.x
  • F : lambda xy.y

• logic operation

  • && : lambda xy.xyF

    • &&(T,T) = (lambda x1y1.x1)(lambda x2y2.x2)(lambda xy.y) = lambda x2y2.x2 = T
    • &&(F,Any) = (lambda x1y1.y1)(Any)(lambda xy.y) = lambda xy.y = F

  • | : lambda xy.xTy

    • |(F,F) = (lambda x1y1.y1)(lambda xy.x)(lambda x2y2.y2) = lambda x2y2.y2 = F
    • |(T,Any) = (lambda x1y1.x1)(lambda xy.x)(Any) = lambda xy.x = T

  • ~ : lambda x.xFT

    • ~(F) = (lambda xy.y)(lambda x1y1.y1)(lambda x2y2.x2) = lambda x2y2.x2 = T
    • ~(T) = (lambda xy.x)(lambda x1y1.y1)(lambda x2y2.x2) = lambda x1y1.y1 = F

• conditional test

  • Z : lambda x.xF~F ==> T if x==0 else F
  • Z(0) = 0F(~F) = (lambda sz.z)F~F = ~F = T
  • Z(1) = (lambda sz.s(z))F~F = F(~)F = (lambda xy.y)(~)(F) = IF = F

• predecessor

  • p : lambda zxy.xy ==> a pair (x,y)
  • Inc : lambda pz.z(S(pT))(pT) ==> increase each element of one pair (x,x-1) -> (x+1,x)
  • P : (lambda n.n(In(lambda z.z00)))F
  • nP(0) = 0

• equality and inequality

  • >= : lambda xy.Z(xPy) [if x>=y return True else False]
  • <= : lambda xy.Z(yPx) [if x<=y return True else False]
  • = : lambda xy.^(Z(xPy))(Z(yPx))

• recursion

  • Y combinator : Y = lambda f.(lambda x.f(xx))(lambda x.f(xx))
    = f((lambda x.f(xx))(lambda x.f(xx)))
  • Yf = f(Yf) [Yf ==> recursion of f]
  • example 1+2+3…+n : f = lambda rn.(Zn)(0)(nS(r(Pn)))
  • Yf = f(Yf) = lambda Yfn.(Zn)(0)(nS(Yf(Pn))) ==> Yf recursion

  ref:《A Tutorial Introduction to the Lambda Calculus》