lambda演算表达式全解释

BNF范式表达上下无关文法描述

hello BNF

前面两个用于生成函数，第三条则是函数作用在参数上的形式

def1:λ项：假设我们有一个无穷的字符串集合，里面的元素被称为变量，那λ项定义如下：

我们可以更加正式的说：a. 所有变量都是λ形式（所有变量都是合法的λ表达式）; b. 如果x和y是λ形式，那么(xy)是λ形式; c. 那么(λx.y)是λ形式。通过这三条规则，我们可以写出所有的λ表达式。如果我们从左向右读λ表达式，我们可以少写一些括号：(λy.xy) ab是 (((λy.(x y)) a) b)的化简版。

lambda1省略

由于省略的出现，所以也需要适当的考虑结合问题，什么时候是应用什么时候是函数抽象取决于：

λy.xy为什么代表函数抽象而不是将函数λy.x应用于y的函数应用呢？为了消除类似的表达式歧义，可以多使用小括号，也有以下几个消歧约定可以参考：

自由变量

对一个λ项P，我们可以定义P中的自由变量集合FV(P)如下：

所以可以看出抽象λφ.M中的变量φ是要除去自由变量的

α规约（置换公理）

λ xy.x+y = λab.a+b

β规约（代入公理）

（λ xy. x+y) a b = a + b

（非必要规约）eta | η 归约

灵活运用alpha和beta已经可以解决所有的lambda表达式归约问题，但是考虑这样一个表达式：

 

将它应用于任意一个参数上，比如(λx.M x) N，进行beta归约和替换后会发现它等价于M N，这岂不是意味着

 

没错，对于形如λx.M x，其中表达式M不包含绑定变量x的函数抽象，它是冗余的，等价于M，而这就是eta归约，它一般用于清除lambda表达式中存在的冗余函数抽象。

explanation:在函数后边又跟了一个表达式时，它可以被解析。解析过程就是将头部一个变量去掉，然后将它所有在体部的出现的这个变量替换成写在函数后边跟着的表达式。 也就是说，我们剪切函数后面的表达式，然后粘贴进体，替换和头部同名的那个变量；做完这一步，我们把头部的那个变量删了，因为它已经完成了它的使命，告诉我们替换哪个变量。

lambda3

函数应用

函数可以被应用在表达式上。在表达式 EA 中，E 是一个函数，它被应用到了表达式 A 上。换句话来说，表达式 A 就是表达式 E 的输入，然后输出 E(A) 。

把 E 替换成抽象体 λ y.y ^2，然后得到下面的式子

EA = E(A)

EA = (λy. y²)(A)

 

多参数函数

用不同的方式，我们可以先定义一个函数，这个函数接收一个参数 x ，返回一个新的函数，这个新的函数接收一个参数 y ：

λx.(λy. x y)

lambda2

eg: 定义I=\x.x , 则Ia≡(\x.x)a≡β a

模拟、定义数据类型

布尔类型：

true = \a (\b.a)

false= \a(\b.b)

先来经历一个模拟自然数的过程：

定义所有自然数最简单的方法就是从第一个开始（0），然后定义后继操作（successor operation)。通过在自然数上定义后继操作，我们的到一个比它更大的自然数，然后一个一个定义所有的自然数。

让我们这样定义0：

0 :⇔ λ sz.z

（记住：这是 λs.λz.z的缩写，它和λab.b, 或 λqx.x是一个意思。）

Church numerals

这个表达式有一个有意思的特性:当它被解析，它会把第一个表达式丢掉，然后第二个原封不动。它的约束变量s会被空字符串替换（因为它不在体中出现），所以最后留下一个z。

类似的，

1 = λ sz.s(z)

2 = λ sz.s(s(z))

3 = λ sz.s(s(s(z)))

4 = λ sz.s(s(s(s(z))))

...

换句话说，我们的计数法其实就是在z之上嵌套表达式s(...)，数字多大嵌套多少次。（也就是说：如果我们解析数字n，上述过程被复制n次）。我们可以这样说：我们对z应用了n次s。

一个好的后继函数是：

S :⇔ λ abc.b(abc)

让我们用这个后继函数计算0：

S0 = (λ abc.b(abc)) (λ sz.z)

= λ bc.b((λ sz.z) bc)

= λ bc.b((λ z.z) c)

*= λ bc.b(c) *

最后一个表达式不可以再简化了（没有函数了），然后——

λ bc.b(c) = λ sz.s(z) = 1

换句话说，这个后继函数应用在0上产生了1，让我们再重复一次：

S1 = (λ abc.b(abc)) (λ sz.s(z))

= λ bc.b((λ sz.s(z)) bc)

= λ bc.b((λ z.b(z)) c)

= λ bc.b(b(c))

瞧！看哪~

λ bc.b(b(c)) = λ sz.s(s(z)) = 2

就像我们看到的，我们的后继函数完成了我们期待的工作：从0开始，它产生自然数。它用s(...)将传入的自然数括起来，从而得到下一个数。

自然数模拟的所需演算：

lam

example: MULT THREE TWO

模拟递归（加参数）

• Lambda> FACT1 = \f.\n.IF (ISZERO n) ONE (MULT n (f f (PRED n)))

• Lambda> FACT = FACT1 FACT1 • Lambda> FACT THREE • \f.\x.f (f (f (f (f (f x)))))

• Lambda> FACT FOUR \f.\x.f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x)))))))))))))))))))))))

Fixed-point Combinator

In mathematics and computer science in general, a fixed point of a function is a value that is mapped to itself by the function.

In combinatory logic for computer science, a fixed-point combinator (or fixpoint combinator)[1]: page 26  is a higher-order function fix{\displaystyle {\textsf {fix}}} that returns some fixed point of its argument function, if one exists.

Formally, if the function f has one or more fixed points, then

and hence, by repeated application,

一些示范

• TRUE = \x.\y.x

• FALSE = \x.\y.y

• AND = \p.\q.p q p

• OR = \p.\q.p p q

• NOT = \p.\a.\b.p b a

• IF = \p.\a.\b.p a b

• 求NOT (NOT TRUE)

• 求IF (OR FALSE FALSE) a b

NOT (NOT TRUE)

=NOT((\p.\a.\b.p b a)\x.\y.x)

=NOT(\a.\b.( \x.\y.x) b a)

=NOT(\a.\b.b)

=( \p.\a.\b.p b a)(\x.\y.y)

=\a.\b.( \x.\y.y) b a

=\a.\b.a

=\x.\y.x

IF (OR FALSE FALSE) a b

= \p.\a.\b.p a b (OR FALSE FALSE) a b

= (OR FALSE FALSE) a b

= (\p.\q.p p q FALSE FALSE) a b

=( FALSE FALSE FALSE)a b

=(\x.\y.y FALSE FALSE)a b

=( FALSE)a b

=(\x.\y.y)a b

=b

5.

• LEQ = \m.\n.ISZERO (SUB m n)

• 求⼤大于等于GEQ

GEQ = OR (NOT LEQ) EQ

= (\p.\q.p p q) (( \p.\a.\b.p b a) LEQ) EQ

= (\m.\n.ISZERO (SUB n m)) ( \m.\n.ISZERO (SUB n m)) EQ

= ISZERO (SUB (\a.\b.ISZERO (SUB b a)) EQ)

= ISZERO (SUB (\b.ISZERO (SUB (\m.\n. AND (LEQ m n) (LEQ n m)) a)))

= ISZERO (SUB (\b.ISZERO (SUB (\m.\n. AND (\m.\n.ISZERO (SUB m n)( \n.\m.ISZERO (SUB n m)))))))