[程序设计理论] lambda calculus -- zz from lily

rickxbx · 发表于 2006-12-7 09:47:28

【以下文字转载自 CompLang 讨论区】
【原文由 starfish 所发表】

1. λ-演算的起源

在十八世纪初，现代数学取得了辉煌的成果。其中G. W. Leibniz
(1646 -- 1716)是当时的杰出者，他是微积分学的创始人之一。作为
数学家和哲学家，他为推动现代逻辑的发展也作出过重大的贡献。
Leibniz曾有一个宏伟的理想：（1）建立一个通用语言，使得所有
的问题能在其中表述；以及（2）找出一种判定方法，解答所有在通
用语言中表述的问题。

人们为实现这一理想付出了很多努力，直至二十世纪才出现一些重要
成果。谓词逻辑和集合论的建立实际上完成了Leibniz的第一条理
想，这归功于一些一流的数学家，如Frege, Cantor, Russell, Hilbert
和 G\"odel。Leibniz的第二个理想成为了一个哲学问题：“是否存在
一个通用的判定方法求解所有用通用语言表述的问题呢？”这就是所
谓的Entscheidungsproblem（德语，意思是“判定问题”）。

在1936年，A Church和Alan Turing独立地给出了这个问题的否定
答案。为了解决此问题，他们以不同的方式形式化定义了“可判定”
的概念（或者“可计算”的概念）。事实上他们给出了两种不同的计
算模型：Turing发明了一组机器---Turing机，并以此定义可计算性；
Church发明了一个形式系统---λ-演算，并以此定义了可计算性。
就这样，λ-演算问世了。

rickxbx · 发表于 2006-12-7 09:48:27

【以下文字转载自 CompLang 讨论区】
【原文由 starfish 所发表】

2. λ-演算的直观描述
λ-演算有两种基本运算：“作用(Application)”与“抽象(Abstract)”。
表达式 FA 表示对象 F 作用于对象 A，FA 既可被理解为计算 FA 的过程，
也可被理解为此过程的输出。λ-演算是无类型系统，从而自作用 FF 是合
法的，这将模拟递归。
在抽象运算中，记号λ将被引入。对于数学式x^2，λx. x^2 表示函数
x |→ x^2
一般来说，若 M[x] 为表达式，则 λx. M[x] 表示函数
x |→ M[x]
把作用与抽象结合起来就有如下方程
(λx. M[x])N = M[N]
这一方程便是所谓的β-变换。这里 M[N] 通常写成 M[x:=N]，表示在M中
将所有“自由出现”的 x 替换为 N 所得到的结果（事实上替换过程中 N
的表达式也可能要改变，这一点将在后面详细说明）。
λ-演算只讨论一元函数，这是因为多元函数可通过重复作用一元函数的运
算而得到，这是由 Sch"onfinkel 首先提出的。以二元函数为例，对于
f(x, y)，定义 F_x = λy. f(x, y)，F = λx. F_x，从而
(Fx)y = F_x y = f(x, y)
下面我们将给出λ-演算的形式描述。

复制代码

rickxbx · 发表于 2006-12-7 09:49:25

【以下文字转载自 CompLang 讨论区】
【原文由 starfish 所发表】

3. λ-演算的语法
【定义1】λ-演算的字母表由以下组成：
●变元集合：Δ = {v, v', v'', v''', …}, Δ无穷
●抽象算子：λ
●括号：(, )
【定义2】λ-项的集合Λ归纳定义为满足以下条件的最小集合：
● x ∈Δ → x ∈ Λ
● M, N ∈Λ → (MN) ∈ Λ
● M ∈Λ, x ∈Δ → (λx M) ∈ Λ
若用BNF(Backus Normal Form)表示，则有
Δ ::= v | Δ'
Λ ::= Δ | (ΛΛ) | (λΔΛ)
【定义3】我们做以下约定：
● x, y, z, … 表示任意变元；
● M, N, L, … 表示任意λ项；
● M ≡ N 表示M和N语法恒同；
● 通常采用以下省略括号表示法：
(i) F M_1 M_2 … M_n ≡ (…((F M_1) M_2)…M_n) (左结合)
(ii) λx_1x_2…x_n. M ≡ (λ x_1 (λ x_2 (…(λx_n M)…) ) )
● 设 P ≡ M N_1 N_2 … N_k (k ≥ 0)，当k=0时，P ≡ M;
设 P ≡ λx_1x_2…x_k. M (k ≥ 0)，当k=0时，P ≡ M。
【定义4】设M ∈ Λ，M的长度ρ(M)被定义为M中变元出现的次数，即
● ρ(x) = 1, x ∈Δ
● ρ(MN) = ρ(M) + ρ(N)
● ρ(λx. M) = ρ(M) + 1
以后我们说对M的结构作归纳是指对M的长度ρ(M)作归纳，这是自然数上的
归纳。
【定义5】设M∈Λ，对M的结构作归纳，定义M的子项集合Sub(M)如下：
● Sub(x) = {x} , x ∈Δ
● Sub(N_1 N_2) = Sub(N_1) ∪ Sub(N_2) ∪ { N_1N_2 }
● Sub(λx.N ) = Sub(N) ∪ {λx.N }
若N ∈ Sub(M)，则称N为M的子项。
例如：y为 λx.yy 的子项，但是x不是 λx.yy 的子项。
【定义6】设M ∈Λ，
● M 的自由变元集合 FV(M) 归纳定义如下：
FV(x) = {x}
FV(N_1N_2) = FV(N1) ∪ FV(N_2)
FV(λx.N ) = FV(N) - {x}
● 若x出现于M中，且x不属于FV(M)，则称x是约束的。
● 若FV(M)为空集，则称M为闭λ-项（或组合子），且记全
体闭λ-项的集合为 Λ* 。
例如 M ≡ λx. yxy ，则其中x 是约束变元，y是自由变元。
N ≡ λxy. yxy 是一个闭λ-项。
事实上约束变元和自由变元的概念在数学的其他领域也出现过，
例如在微积分中
∫(3xy+x-y) dx
这里dx其实就表明在3xy+x-y中x是约束变元。
【定义7】上下文(Contexts)
λ上下文集合C[]定义为满足下列条件的最小集合：
● x ∈C[]
● [] ∈ C[]
● C_1[], C_2[] ∈ C[] → (C_1[]C_2[]) ∈ C[]
● C_1[] ∈ C[] → (λx. C_1[]) ∈ C[]
上下文中的空白用一个[]表示。引入上下文的概念是为了方便以后的讨论。
例如
C_1[] = (λx. []x) M
则
C_1[λy.y] = (λx. (λy.y) x) M
换句话说，C_1[N] 就是把 C_1[] 中的 [] 出现的地方都填入 N。这种填入
替换和前面说的 M[x:=N] 不同，M[x:=N] 要把M中所有自由出现的x替换成N，
并且N本身可能也会适当地改变。但是C_1[N]的替换则是把所有的[]都换成N，
且N不做任何改变。
另外需要注意的是，FV[M]中的变元在 C[M] 中可能会变成约束变元。

复制代码

rickxbx · 发表于 2006-12-7 09:54:55

下面定义λ演算的公理化系统。
【定义8】若M, N ∈Λ，则称 M = N 为 λ-公式。
【定义9】形式理论λβ由以下的公理和规则组成：
公理：
(ρ) M ＝ M
(β) (λx. M) N = M[x:=N]
规则：
M = N
(σ) ---------------
N = M
M = N, N = L
(τ) ---------------
M = L
M = N
(μ) ---------------
ZM = ZN
M = N
(ν) ---------------
MZ = NZ
M = N
(ξ) ---------------
λx.M = λx.N
公式 M = N 在λβ中可记为λβ|- M = N，有时简记为 M = N，
这时称M可β转换于N。
上面的公理和规则的名称来源于 Curry[1958]。

复制代码

rickxbx · 发表于 2006-12-7 09:55:44

【以下文字转载自 CompLang 讨论区】
【原文由 starfish 所发表】

上述公理系统中的β公理其实就是λ演算中的作用（Application）过程。
从计算机程序设计的角度来看，任何一个λ项都可以看作是一段子程序，
λx. M 就表示该子程序的输入参数是x，而 (λx. M) N 则表示把N作为参数
x带入到子程序M中进行计算。M本身的语法形式描述了M的计算过程，因而只需
要把M中所有“自由出现”的x替换成N即可得到计算结果。注意，这里一直强调
要替换“自由出现”的x，下面我们举一个例子来说明这一点。
假设我们已经在λ演算中定义了加减乘除运算，设
L ≡ λx. (y + x)
M ≡ L (x * x)
则
(λx. M) t ≡ (λx. L(x*x) ) t
≡ (λx. (λx. (y + x)) (x*x) ) t
= (λx. (y + x))(t*t)
= y + t*t
注意其中第一个＝号处不能把(λx. (y + x))中的x替换成t，因为(λx. (y + x))
中的x是约束的，如果把(λx. (y + x))中的x也换成t的话，将得到
(λx. M) t ≡ (λx. (λx. (y + x)) (x*x) ) t
= (λx. (y + t)) (t*t)
= y + t
在计算第二个等号的时候约束变元x在 (y + t)中没有出现，所以实际上并没有做
任何替换，只是简单地浪费掉一个参数(t*t)，最后得到结果y+t。但这个替换的
结果并非我们所希望的。
从程序设计的角度来看，λx. M 相当于一段子程序，"λx."说明了子程序M的输入
参数是x，M中除了x以外的其他自由变量都相当于子程序中的全局变量。
如果用PASCAL语言来描述上述的计算过程，则如下所示：
program Example_1;
var
y, t: integer;
function M(x: integer): integer;
function L(x: integer): integer; // L是子程序M内部的嵌套子程序
begin
L := y + x;
end;
begin
M := L( x * x );
end;
begin
readln( y, t );
writeln( M(t) );
end.
在上述程序中，计算机在进入子程序M计算M(t)的时候，把M中出现的形式参数x都用
实际参数t来取代，但是却不能把L中的x也用t来取代，因为L中的x是L本身的形式参
数，不能和其外部的同名变量x混淆，这其实就是程序设计中所一再强调的一点：要
搞清变量的作用域，区分全局变量和局部变量。
因此在λ演算中规定 M[x:=N] 只能把M中“自由出现”的x换成N。

复制代码

rickxbx · 发表于 2006-12-7 13:10:58

【以下文字转载自 CompLang 讨论区】
【原文由 starfish 所发表】

在上一回中，我们说到β替换有两个基本原则：
1。M[x:=N] 只能把M中自由出现的x替换为N；
2。原来在N中自由出现的变元，在M[x:=N] 的结果中也应该保持自由。
下面我们介绍三条实现β替换的途径。
一。古典方法
这是Church当年提出λ演算的时候提出的方法。这个方法其实是对
M[x:=N]这个符号做了一个递归定义：
【定义10】
(1) x[x:=N] ≡ N
(2) y[x:=N] ≡ y 其中x和y不同
(3) (λx.M)[x:=N] ≡ λx.M
(4) (λy.M)[x:=N] ≡ λy.M[x:=N]
其中 x 不属于 FV(M) 或者 y 不属于 FV(N)
(5) (λy.M)[x:=N] ≡ λz.(M[y:=z])[x:=N]
其中x ∈FV(M) and y ∈FV(N)，z是一个新变元
(6) (M_1 M_2)[x:=N] ≡ (M_1[x:=N])(M_2[x:=N])
上述定义中的(1)(2)(3)(6)都很容易理解。关键在于(4)(5)，这是在
β替换中避免variable capture的关键。
我们先看第(4)条。如果x 不属于 FV(M)，则(λy.M)[x:=N]和λy.M[x:=N]
其实都不做任何替换，得到的结果都是λy.M；如果y不属于FV(N)，那么直
接把M中的x替换成N，必然不会令N中自由出现的y变为约束出现（因为N中
根本没有自由出现的y），所以这一步的替换没有产生variable capture，
然后递归地进行M[x:=N]的替换，只要每一次递归替换都按照上述规则来进
行，就能保证在每一层都不出现variable capture。
再看第(5)条。如果x ∈FV(M) and y ∈FV(N)，直接把x:=N带入M中进行替换，
则因为最外层有一个λy.，N中原来自由出现的y就会变为约束出现。这个时候
要先把最外层的λy.换一个名字，即先把λy.M变换为 λz.M[y:=z]，这里z是
一个新变元，即从来没有在M和N中出现过的变元。这样把λy.M变换为
λz.M[y:=z]以后，我们再进行(λz.M[y:=z])[x:=N]的替换，这时可以根据规
则(4)得到(λz.M[y:=z])[x:=N] ≡ λz. ((M[y:=z])[x:=N])，把这两个过程
合起来就是规则5了。
Church的这个方法，不仅给出了M[x:=N]这个符号的定义，也给出了递归计算
M[x:=N]的算法过程。这个方法的本质是，在进行下一步替换的时候，先检测
下一步替换是否可能产生variable capture，如果有可能，则先把当前的λ项
最外层的约束变元改名，然后再继续替换。总而言之，Church的方法是在替换
的过程中改名，这一点和我们下面将要介绍的“变元约定”方法有所区别。
二。变元约定 (variable convention)
【定义11】约束变元的改名
设P ∈Λ，λx.M ∈Sub(P)，且y为新变元（即未曾使用过的变元），在P中由
λx.M[x := y] 替代 λx.M 的过程称为P中约束变元的改名。P可α--转换为
Q是指Q可由P经过若干次约束变元的改名而得到，记作 P ≡_α Q。
例如
λxy.x(xy) ≡_α λvu.v(vu)
【命题1】
(1) M ≡_α N ==> FV(M) = FV(N)
(2) ≡_α 是等价关系
(3) 对于任何 M∈Λ，存在 N ∈Λ，使得 M ≡_α N，且N中所有的约束变元
不同于其自由变元。
由于当 M ≡_α N 时，从语义角度看，M与N具有相同的解释，故我们也可令
M 在语法上恒同于 N，因而有
【约定12】
若 M ≡_α N ，则 M ≡ N
根据命题1的(3)，我们可以做所谓的变元约定：
【约定13】
若 M_1, …, M_n 出现在某个数学表述过程中，则在这些项中所有的约束变元
不同于其中的自由变元。
【定义14】
(1) x[x:=N] ≡ N
(2) y[x:=N] ≡ y 其中x和y不同
(3) (M_1 M_2)[x:=N] ≡ (M_1[x:=N])(M_2[x:=N])
(4) (λy.M)[x:=N] ≡ λy.M[x:=N]
注意，由于约定13，在上述定义的(4)中，不需要加上条件y不等于x且y 不属于
FV(N)，因为约定13保证了这些条件的成立。
β替换中的这种变元约定的实质是在进行M[x:=N]的替换之前，把M,N中的所有约
束变元改名，使得任何约束变元不同明于M,N中的自由变元，然后在进行替换。这
和Chruch的方法的最大不同之处在于Church的方法是在替换过程中改名，而此方法
实在替换之前一次性地改名。

复制代码

iverine · 发表于 2006-12-7 22:24:49

λ-演算是好东西，不过rickxbx的帖子还是太抽象，属于理论基础。想要在实践中体会λ-演算的魅力，推荐大家学习scheme，是Lisp的一种“方言”。具体信息就请大家自己去google了。

Iambitious · 发表于 2006-12-8 09:14:37

这个是不是属于程序设计理论方面的知识阿。

rickxbx · 发表于 2006-12-8 18:02:52

Post by Iambitious
这个是不是属于程序设计理论方面的知识阿。

可以这么说.
老师常说的一句话是: 学完了 lambda-calculus, 就学会了编程

sinanjj · 发表于 2009-5-3 16:18:24

看来看去都是面向对象构架。。。

构架设计的怎么样就看设计者了。跟理论无关

		自动登录	找回密码
密码			注册