lambda演算

旧城等待， 2022-08-09 17:57 194阅读 0赞

> 由简入深，适时复习，温故知新。 — housir
> 
> λ演算基于最简单的定义函数的思想：  
> 一为函数抽象λx.E，由λ说明的x在函数体E中出现均为形参变元。E是一个λ表达式。  
> 一为函数应用(λx.E)(a),即E中的x均由a置换变成E(a)。

接上一篇 [**博客**][Link 1] 继续写点有关lambda演算的东西。

## 基本函数 ##

*  基本的λ表达式

// 布尔类型
    T = λx.λy.x  // True
    F = λx.λy.y  // False
    // 数字
    0=λx.λy.y            //与F的λ表达式相同
    1=λx.λy.x y  
    2=λx.λy.x(x y)
    n=λx.λy.x(x(…(x y)…)       // λy.之后有n个x

*  基本操作函数

// 逻辑操作函数
    not = λz.((z F) T)=λz.((zλx.λy.y)(λx.λy.x))
    and = λa.λb.((a b)F) = λa.λb.((a b)λx.λy.y))
    or  = λa.λb.((a T)b) = λa.λb.((a λx.λy.x)b)  // 算术操作函数
    + = add = λx.λy.λa.λb.((x a)(y a)b)
    * = multiply = λx.λy.λa.((x(y a)))
    succ = λn.(λx.λy.n x(x y))                        //后继函数
    zerop = λn.n(λx.F)T =λn.n(λz.λx.λy.y)(λx.λy.y)   //判零函数

此外，还有sqr(幂运算)、identity（同一函数）、positive(取正整数)、neg(取负)、divide(除法)、subtract(-、减法)，pred(前驱)等函数。

## 示例 ##

下面介绍几道有关lambda演算的题目，在实践中理解lambda演算。

### 判零（zerop） ###

1.证明：zerop 1 = F

zerop 1
    = (λn.n(λx.F)T ) 1 
    = 1 (λx.F)T β归约[1/n]
    = (λp.λq.pq) (λx.F)T
    = (λq.(λx.F)q)T β归约[(λx.F)/p]
    = (λx.F)T β归约[T/q] 或者η归约
    = F η归约

2.证明：zerop 0 = T

zerop 0
    = (λn.n(λx.F)T ) 0
    = 0 (λx.F)T β归约[0/n]
    = (λp.λq.q) (λx.F)T
    = (λq.q)T β归约[(λx.F)/p]
    = T β归约[T/q]

### 加法（add） ###

核心的λ演算只有单目运算，例如：add 1它返回的结果是函数，再应用到后面的表达式上。这样，1+2就写add 1 2，add 1返回“加1函数”应用到2上当然就是3

1 add 2
    = add 1 2
    = (λx.λy.λa.λb.((x a)(y a)b)) 1 2
    = (λy.λa.λb.((1 a)(y a)b)) 2 // β归约[1/x]
    = λa.λb.((1 a)(2 a)b) // β归约[2/y]
    = λa.λb.(( (λx.λy.x y) a )((λx.λy.x (x y)) a)b) // 1 2 展开
    = λa.λb.((λy.a y) (λy.a (a y))b ) // β归约[a/x]
    = λa.λb.( (λy.a y)(a (a b)) ) // β归约[b/y]
    = λa.λb.(a (a (a b))) // β归约[(a (a b))/y]
    = 3

### 后继（succ） ###

succ 1
    = λn.(λx.λy.n x(x y)) 1
    = λx.λy.1 x(x y) // β归约[1/n]
    = λx.λy. (λp.λq.p q) x (x y)
    = λx.λy.(λq.x q)(x y) // β归约[x/p]
    = λx.λy.x(x y) // β归约[(x y)/q]
    = 2

Lambda演算能力还是比较强的，Church的理论证明，λ演算（核心λ演算）是个完备的系统，可以表示任何计算函数。初次接触可能感觉陌生，一旦熟悉之后就会非常简单。

[Link 1]: http://blog.csdn.net/houmou/article/details/41702161