请选择 进入手机版 | 继续访问电脑版
λ-calculus的构成部分

下面为λ-calculus构成的简要介绍, 受限于篇幅省略了一些例子和详细说明, 需要详细介绍的小伙伴可以查阅Lambda calculus(Wikipedia)和书籍.

二元关系:
二元关系的定义为对于两个集合的乘积的子集为A与B上的二元关系, 即:

在二元关系上定义偏序:

(称小于)
的传递闭包, 记作, 既满足以下的最小二元关系:

可表示为:

的自反闭包, 记作, 既满足以下的最小二元关系:

可表示为:


标识符:

为可数标识符集合, 为标识符.

表达式:

亦或定义为满足:

的最小集合.
的一些例子:


一个lambda表达式可以理解为一个匿名函数, 如为接受一个参数x返回x, 不做任何变化的恒等函数:,

长度:
表达式项的长度定义为:


自由名称(free variables):
为自由名称, 与之相对的概念为绑定名称(bound variables), 如中的.
定义自由名称映射为:

的唯一性可由对表达式项的长度做归纳证明, 存在性由表达式的长度有限即标识符(名称)有限可得.
如果, 则称为闭合的(closed)

替换(substitution):
表示替换中所有为, 如
定义替换规则如下:

推论:

证明可由对替换步骤数做归纳证明.


α等价(α-equivalence)
α-equivalence为Lambda表达式之间的最小二元关系(binary relation), 为重命名(renaming)等价, 记作, 定义如下:

在推导规则下闭合:

一些例子:


λ-term:
λ-term为在α-equivalence下的表达式商集:


可理解为对任何重命名等价的表达式当作同一表达式, 因为名称的区别在λ-calculus中并不重要. 为了表达简洁, 下文中对λ-term的操作为对其等价类的代表元进行操作. 同样上文中的记号与定义同样适用于λ-term.

η规约(η-reduction):
单步η-reduction为λ-term之上的最小二元关系, 记作, 定义为:

在推导规则下闭合:


β规约(β-reduction):
单步β-reduction为λ-term之上的最小二元关系, 记作, 定义为:

在推导规则下闭合:

多步β-reduction为单步β-reduction的传递自反闭包(transitive-reflexive closure), 记作,即满足下述推导规则的最小关系:

如果某个λ-term无法进行β-reduction则称其为正规项(β-normal form)
β等价(β-equality)为多步β-reduction添加上对称性的最小二元关系, 记作

值得注意的是并不是所有的λ-term都有β-normal form, 一个很典型的例子:


为β-reduction下的一个不动点, 显然不具有β-normal form. 有些人会称其为weak head normal form(在λ-term上定义离散拓扑, 该β-reduction序列收敛).

λ-calculus规约求值问题

对λ-term进行求值即为进行β-reduction直到规约得到normal form. 但一个λ-term中可能包含多步不同规约, 并且不同的规约可以有不同的执行顺序, 如下:
定义:,
即:
或者是:
即:

(先进行的β-reduction还是的β-reduction顺序)
对于任意的λ-term进行β-reduction, 若能得到normal form, 结果是与reduction顺序相关的吗? 即是进行β-reduction得到的normal form是否唯一.
想必小伙伴都知道结果是唯一顺序无关的, 那么应该怎么证明呢? (感兴趣的小伙伴们思考一下)

The Church-Rosser Theorem

The Church-Rosser Theorem指出, 对于某一λ-term 若有:

则存在一λ-term满足:
与  

定义: 平行β-规约(parallel reduction)为λ-term之上的最小二元关系满足推导规则:


引理1:是的传递闭包.
证明: 的每一个推导规则为一个或多个推导的复合.
故有
同取传递闭包得:
于是有:. 证毕.

引理2:
证明: 证明分两步(这个引理得证明很长很繁琐可以略过不看)
第一步证明
对结构做归纳:
归纳基础:
若, 成立
若, 成立
归纳步骤: 归纳假设对有成立
对情况:
1. 若即归纳基础, 成立.
2. 若根据归纳假设:


则有
成立.
3. 若根据归纳假设:

若, 成立.
若, 或
两种替换不影响证明, 因为:

以为例有:
成立.
综上: 若有成立.
即得若有成立, 则对于有成立.
由归纳得: 对于有成立.

第二步证明
对推导步骤做归纳:
归纳基础: ,推导一步完成, 则根据证明步骤一结论可得
归纳步骤: 归纳假设对推导小于等于步的均有成立.
对推导为步情况:
1. 若
推导最多为步, 由归纳假设得:
关于的符号替换不影响证明, 类比于第一步证明中的符号替换.
2. 若
推导最多为步, 由归纳假设得:

则有: , 即成立.
3. 若

推导最多为步, 由归纳假设得:

若:


(由替换推论得)
即:  
:
由替换推论得:
同情况.
:


(由替换推论得)
(注: 性质可对归纳得出. 每一步并不会引入新名称)
即:  
:
进行α重命名, 即
令新的同上情况()可证.
对于有成立.
故对推导为步时成立.
综上, 由归纳得: 对于有成立.

结合证明步骤一与步骤二得. 证毕.

定义: 对角性质(diamond property). 对于二元关系满足:
存在使得 则称二元关系具有对角性质.

Lambda calculus引论(一): 规约求值-186.png

引理3: 二元关系具有对角性质, 即若 存在使得.
证明: 对推导步骤做归纳.
归纳基础: 若则, 令, 即满足对角性质.
归纳步骤: 归纳假设对推导小于等于步的均有存在使得成立.
对推导为步情况:
1. 若

由归纳假设得: 存在使得成立.
则令. 则满足成立.
2. 若
有与
由归纳假设得: 存在与使得与成立.
则令. 则满足成立.
3. 若
有与
由归纳假设得: 存在与使得与成立.
则令.
由引理2可得: , , 即满足成立.

综上, 由归纳得: 对于若 则存在使得成立, 即二元关系具有对角性质.

引理4: 二元关系具有对角性质, 其传递闭包亦满足对角性质.
证明: 证明分三步.
第一步证明: 若有并且则存在满足并
对做归纳:
归纳基础: , ,  由具有对角性质存在满足与.
归纳步骤: 归纳假设对时存在满足并且.
当时:

由归纳假设得: 存在满足并且.
由, 与具有对角性质得: 存在满足与.
即设对时存在满足并且
综上, 由归纳得对于任意,  若有并且则存在满足并成立.

第二步证明: 若有并且则存在满足并.
对做归纳:
归纳基础: , ,  对于可表示为.
由第一步证明得存在满足与.
归纳步骤: 归纳假设对时存在满足并且.
当时:

由归纳假设得: 存在满足并且.
由, 和归纳基础得: 存在满足与.
即设对时存在满足并且
综上, 由归纳得对于任意,  若有并且则存在满足并成立.

第三步证明: 若 存在使得.
可表示为. 又有.
由第二步证明得: 存在满足.
, 即得:  .

综上若 存在使得即具有对角性质的二元关系的传递闭包亦具有对角性质.

定理: Church-Rosser Theorem
证明: 由引理3得二元关系具有对角性质, 又由引理1得是的传递闭包, 因此由引理4得具有对角性.
即若 与 , 则存在λ-term满足: 与 . 证毕.

推论1(Church-Rosser property): 若λ-term有, 则存在满足 与 .
证明: 由得: 存在使得, , . 由Church-Rosser Theorem得: 存在满足, , .
对重复上述步骤得到, 重复次, 得到, 即有, 令即是, . 证毕.

推论2: 若λ-term有, 为normal form. 则. 即若规约存在normal form则规约序列长度有上界.
证明: 由引理1有
对规约序列长度做归纳: 证明对于任何归纳序列均有.
归纳基础: 当规约序列长度为0时, 即, 平凡情况.
归纳步骤: 归纳假设对规约序列长度时, 有.
当时:

对另一任意规约序列, 由引理3得具有对角性, 即有: 存在满足:. 由于规约序列长度为, 由归纳假设得归纳序列长度为, 即, 故规约序列长度为.
再次由由归纳假设得所有规约序列长度为, 即得规约序列长度为. 归纳假设仍成立.
由归纳得对于任意规约序列成立.
由于为有限步的复合, 故任意序列的β-规约次数有限, 存在上界. 证毕.

推论2给出了结论: 若λ-calculus规约求值能得到normal form, 则该规约序列长度存在上界, 无论采用什么规约顺序均会在有限步内完成, 即停机.

推论3: 若λ-term有, 为normal form. 则对于任意的子表达式均存在normal form. 即的子表达式规约为normal form的序列长度有上界.
证明: 另为任意子表达式. 的规约序列蕴含在某一规约序列中. 由推论2得长度有上界, 故规约序列亦有上界. 证毕.
推论3给出了结论: 若λ-calculus规约求值能得到normal form, 则该规约序列长度存在上界, 无论在局部采用什么规约顺序该部分均会在有限步内完成, 即局部停机.

推论4(unique normal form): 若λ-term有 与 并且为normal form. 则.
证明: 假设, 由Church-Rosser Theorem得: 存在满足 与 .
由于故. 则或中可进行至少一次β-reduction, 与normal form定义矛盾. 因此. 证毕.

推论4回答了上文的规约求值问题, 即在λ-calculus中求值顺序与最终结果顺序无关, 若是求值停机, 则结果唯一. 推论2,3,4的结论为各种求值策略如call by name与call by value以及全局或局部策略选择的well-defined性质提供了支持.

(是不是应该起标题为: Lambda calculus从入门到放弃 比较好呢? 笑~)
分享到 :
0 人收藏

15 个回复

倒序浏览
谢谢莎莎姐~  成为专栏编辑啦, 以后文章都放专栏里.
梦呓  高级会员 | 4 天前
有一点请教,替换规则里,(lambda x.P )(N/x)不可以理解为使用alpha变换么,那结果不应该是lambda N.(P(N/x))么?
隔海书信  高级会员 | 4 天前
并不是喔喵, 这里[N/x]意思是名称x被替换为N, N是一个表达式不是一个名称喔.
比如(λy.x)[(λz.z)/x]这里N是(λz.z)替换结果是λy.(λz.z).
而(λx.P)[N/x]=λx.P
x在P里是一个绑定名称, 不是自由名称, 因此不应该被替换, 所以结果还是λx.P喔.
至于α变换是对绑定名称进行重命名比如
λx.x变换为λy.y这里将名称x变为了y.
明白了喵?
荒凉い  中级会员 | 4 天前
请教关于自由变量:
这个FV(λχ.P)=FV(P)是什么意思?
难道说FV(λx.x)=FV(x)=x?
烟痞  高级会员 | 4 天前
谢谢提醒喵~ 漏了一点点东西, 补上啦.
噢,看到啦,谢谢。
这里应该说置换的定义是用N取代x在前式的自由出现,置换定义如此
暔寻  高级会员 | 4 天前
对啊, 替换是将某个自由名称替换为某个表达式, 所以替换并不是α变换啦
淡然  高级会员 | 4 天前
FV的唯一性可由对表达式项的长度做归纳证明
不strcutral reduction吗?
您需要登录后才可以回帖 登录 | 立即注册

本版积分规则

Archiver|手机版|小黑屋|翁笔

© 2001-2018 Wengbi.com

返回顶部