Lambda Calculus是一种和图灵机同级的计算机设计理论。在CTF实战中，可以用于混淆。国外CTF以前出过，不过那个时候我太菜了分析不出来。

Lambda Calculus 0

这次先学基本概念，下一次再去研究具体编程语言上的实现。

简介

λ演算是一套从数学逻辑中发展，以变量绑定和替换的规则，来研究函数如何抽象化定义、函数如何被应用以及递归的形式系统。它由数学家阿隆佐·邱奇在20世纪30年代首次发表。lambda演算作为一种广泛用途的计算模型，可以清晰地定义什么是一个可计算函数，而任何可计算函数都能以这种形式表达和求值，它能模拟单一磁带图灵机的计算过程；尽管如此，lambda演算强调的是变换规则的运用，而非实现它们的具体机器。

λ演算是图灵完备的，或者说是和图灵机同级的。

有一种相对来说比较小众但也不失风气的编程类型便是函数式编程，其比如Haskell，还有Python和js等语言其中都有lambda函数的设计理念，其核心理论其实就是λ演算。

定义

名称（name）

一个用于标识符的名称（name），或者叫变量（variable），可以是a, b, c...字符中的任意一个。最常见的例子给的都是x和y。

表达式（expression）

λ演算中最重要的就是表达式（expression）。

表达式（expression） 会被递归地定义为：

1
2
3

<expression> := <name> | <function> | <application>
<function> := λ <name>.<expression>
<application> := <expression><expression>

1
2
3

<表达式> := <名称> | <函数> | <应用>
<函数> := λ <名称>.<表达式>
<应用> := <表达式><表达式>

解释一下：

1. 表达式可以是单独的一个名称，或者是函数，或者是应用
2. 函数则有固定的格式。点后面的表达式意味着这个定义是递归的。
3. 应用则是由多个表达式按顺序构成的。

这种递归定义法和编译器里的词法分析很像。

为了语法的清晰，表达式可以被括号包围。比如E是一个表达式，那么(E)也是同样的表达式。

仅有的关键词便是λ和点.。

为了避免用括号使表达式混乱，我们默认函数应用从左向右进行，比如

$$E_1E_2E_3…E_n$$

将会被看作为

$$
(…((E_1E_2)E_3)…E_n)
$$

从上面的定义可以看出，单个标识符（即名称，变量）就是一个表达式。比如常见的标识符x，它就可以是一个表达式。

函数（function）

那么根据<function> := λ <name>.<expression>的法则，我们可以构造出一个最简单的函数：

$$
\lambda x.x
$$

其中第一个x是name，第二个则是expression。

用过Python的lambda表达式的话，就会知道这个其实就是

1	lambda x : x

就是传入一个参数x（左侧形参表），返回x（右侧函数主体）
类比学习一下，其实很好理解的。理解这个类比对后面应用的求解（evaluation）有帮助。

λ紧跟的这个name是这个函数的形参（argument），而后面跟着的expression是函数的主体（body）

应用（application）

有了多个表达式，那么我们就可以组成一个应用了。

$$
(\lambda x.x)y
$$

这个便是将函数应用于y上面。括号是用于防止语法上的二义性。

求解（evaluation）

将

$$
(\lambda x.x)y
$$

求解，即将函数主体内与函数形参一致的变量，全部都替换成括号外应用的这个y。

$$
(\lambda x.x)y=[y/x]x=y
$$

其中[y/x]的意思就是，将函数主体内的x全部用y进行替换（/所以就可以看成替换符）。这可以看成一个替换指令。

中括号后面跟着的x则是函数主体，也就是待替换目标。

所以替换后就只剩下了一个y。

即Python中

1 2	func = lambda x : x func(y)

一样

值得注意的是，函数形参到底是什么名称是不重要的，只要保持和函数主体内一致的关系即可。

$$
\lambda x.x\equiv\lambda y.y\equiv\lambda z.z\equiv\lambda m.m
$$

我们用≡恒等号来定义这种当两个或多个等式意义相同时的关系。

约束变量与自由变量（bound/free）

$$
\lambda x.x
$$

中x是约束变量，因为参数表中有x。当此函数被求解时，主体x会被替换。

$$
(\lambda x.xy)
$$

其中x约束，而y是自由变量，因为参数表中没有用到y；求解时y将不变。

$$
(\lambda x.x)(\lambda y.yx)
$$

中第一个λ式的x是约束于第一个式的约束变量；第二个式的y是约束于二式的约束变量，而x反而是自由变量。

值得注意的是，一式x与二式x毫无关系。

总结一下：

自由变量

1. <name>在表达式 <name> 中是自由的。（比如单纯的一个x，肯定自由）
2. <name1>在λ<name2>.<exp>是自由的，只要<name2> != <name1>。（比如λx.xy中的y
3. <name1>在$E_1E_2$中是自由的，如果<name1>在E_1中是自由的，或者在E_2中是自由的

约束变量

1. <name1>在λ<name2>.<exp>是约束的，如果<name1> == <name2>，或者<name1>在<exp>内是约束的。
2. <name1>在E_1E_2中是约束的，如果<name1>在E_1中约束，或在E_2中约束。

值得一提的是，同样的标识符，可能在一表达式里是同时自由或者约束的。表达式

$$
(\lambda x.xy)(\lambda y.y)
$$

中的y，就是在1中自由，在2中约束。整体算作一个式子，那就是自由又约束。

替换

初学λ演算时，比较头疼的就是我们从来都不给函数起名字。我们直接写出整个函数的定义，然后着手于求解它。然而为了化简，我们为函数进行起名。使用大写字母，数字等符号来进行命名。

比如，我们定义

$$
I\equiv(\lambda x.x)
$$

那么

$$
II=(\lambda x.x)(\lambda x.x)
$$

实际上我们也可以重写II为

$$
II=(\lambda x.x)(\lambda z.z)
$$

然后我们根据上文的求解法则，将右侧表达式带入左侧进行替换。

$$
II = [\lambda z.z/x]x = \lambda z.z = I
$$

所以说，这个$\lambda x.x$函数的n层嵌套应用还将是它自己。

Python中的应用

利用Python加深理解

1
2
3
4
5
6
7
8
9

y = (lambda x:x)(lambda z:z)
y(1) # 1
# 看看汇编
import dis
dis.dis(y)
"""
  1           0 LOAD_FAST                0 (z)
              2 RETURN_VALUE
"""

直接就转义成了return z了。这说明了一种可能性，即Python编译器可能能够实现在编译过程中对lambda嵌套式的优化化简。

注意

在替换过程中，要注意不要错将自由变量和约束变量混到一起。

比如

$$
(\lambda x.(\lambda y.xy))y
$$

中λ式中的y显然是约束变量，而最外层最右侧的y显然是自由变量。要是错误的混淆在一起的话，则会化简成

$$
(\lambda x.(\lambda y.xy))y=[y/x](\lambda y.xy)= \lambda y.yy
$$

正确的方法是提前重命名进行区分。我们将约束变量y改成t

$$
(\lambda x.(\lambda y.xy))y=[y/x](\lambda t.xt)= \lambda t.yt
$$

所以，如果λx.exp被应用于表达式E，我们将替换exp中所有的自由变量x为E。（注意这里是自由变量！！，比如上文中的λy.xy中的x）

这里一开始引起了我的严重疑惑：那么一开始的例子(λx.x)y该去怎么理解？x不是约束变量嘛？

我思考了许久，给了一个比较合理的解释：说一个变量是不是约束还是自由，必须先确定你所说的表达式范围。

比如λx.x在这个有λ开头的函数中，x确确实实是约束的。我们记为F。
但是在函数F的主体F.body中，即x中，x却是自由的。

如果替换过程将带来一个自由变量E，而在原来的这个式子中有一个同名但是是约束变量E，那么我们应该提前将约束变量进行重命名以避免冲突。比如：

$$
(\lambda x.(\lambda y.(x(\lambda x.xy))))y
$$

最外层λ式的主体

$$
\lambda y.(x(\lambda x.xy))
$$

这个三层套娃确实挺麻烦的，我稍微分析一下。其中，在λx.xy这个小式子范围中，x是约束变量，y是自由变量。

而在整个主体λy.(x(λx.xy))中，最左侧与小λ式同级的x是自由变量，小λ式内的x是约束变量，而此时小λ式的y也因为大λ式的y形参而变成了约束变量。

$$
[y/x](\lambda y.(x(\lambda x.xy)))
$$

现在要进行替换。根据要求，在函数主体范围内，将其中的唯一的自由变量x全部都替换成y。但是发现已经有一个约束变量y了，所以要把这个约束变量y给重命名。改成t

$$
[y/x](\lambda y.(x(\lambda x.xy)))=
[y/x](\lambda t.(x(\lambda x.xt)))
$$

得出最后结果

$$
(\lambda t.(y(\lambda x.xt)))
$$

一般情况下我们都是从最左侧开始向右替换，直到没有可以替换的。

思考：虽然上面的解释能够大致让人理解如何正确的替换，但是这种思路似乎在稍微递归深一点的函数上就会变得很复杂，因为一下就要求解分析整个大函数主体各个变量的状态。

数字（丘奇数）

在λ演算中，数字也是一种函数。其整个数字集合的定义是通过皮亚诺公理来实现的。

即suc(0)=1，suc(suc(0))=2，…以此类推。

先定义0.

$$
0\equiv\lambda s.(\lambda z.z)
$$

这是一个拥有两个形参s和z的函数。

我们可以进一步简写成

$$
\lambda sz.z
$$

需要注意的是s在最左侧，在应用时将会是第一个被替换的。其次是z。

这样，我们继续定义其他自然数

$$
1\equiv\lambda sz.s(z)\newline
2\equiv\lambda sz.s(s(z))\newline
3\equiv\lambda sz.s(s(s(z)))\newline
$$

可以简单记成

$$
n\equiv\lambda sz.s^n(z)
$$

这个定义数的函数组成看上去很奇怪，尤其是括号位置，暗示着应用的顺序是从括号里向括号外传递的。比如1，s(z)就意味着是s应用于z上。

考虑到λs是第一个参数，比如s全都被替换成了某个λ函数，那么最右侧，括号中心里的z就会被应用，从里到外进行一个求解。

后继函数（successor）

首先有意思的就是successor()函数。可以被定义为

$$
S\equiv\lambda wyx.y(wyx)
$$

即

$$
\lambda w.(\lambda y.(\lambda x.(y(wyx))))
$$

于是我们将其应用到0上，得到

$$
S0\equiv(\lambda wyx.y(wyx))(\lambda sz.z)
$$

从左到右进行替换。首先将w给替换成$(\lambda sz.z)$得到

$$
\lambda yx.y((\lambda sz.z)yx)
$$

然后里面的(λsz.z)yx又能继续应用

$$
\lambda yx.y((\lambda sz.z)yx)=\lambda yx.y((\lambda z.z)x)=\lambda yx.y(x)=\lambda sz.s(z)=1
$$

这样我们就获得了0的后继1。

继续再试一个

$$
(\lambda wyx.y(wyx))(\lambda sz.s(z))=\newline
\lambda yx.y((\lambda sz.s(z))yx)=\newline
\lambda yx.y((\lambda z.y(z))x)=\newline
\lambda yx.y(y(x))=\newline
\lambda sz.s(s(z))=\newline
2
$$

所以我们总结并进行抽象，得到

$$
Sn\equiv n+1
$$

加法

虽然论文里面说加法很简单，但是还是花了我不少时间思考。

重新回顾最开始的递归定义，可以了解到

应用是由表达式组合而成的；而表达式可以是单一变量，函数，或者是另一个应用的嵌套。那么意思就是，诸如sz这样的由2个单变量构成的式子也是一种应用，即将s应用于z上面。如果没被应用保持现状，那么这就是最简式；如果被应用了，s被替换成了某个λ函数，那么z就会被s代表的函数应用，进行替换求解。

观察式子

$$
nS = (\lambda sz.s^n(z))S
$$

便于求解，已经进行了笼统概括处理。整个后继函数S将用于替换所有的s，那么得到结果（当然也可以S和n全都拆开不用简写，不过那就很麻烦了）

$$
nS=\lambda z.S^n(z)=\newline
\lambda z.S(S(S(…S(z))))=\newline
$$

上面后继函数的结论：

$$
S(n)\equiv(n+1)
$$

（这里的括号不要太在意，仅仅是表示应用顺序的）

层层带入，得到

$$
nS=\lambda z.S(z+n-1)=\lambda z.(z+n)
$$

（按理来说不应该有更高级的操作，比如加法号+，但是这里不妨令设一变量y=z+1，如此迭代，那么就可以避免这一问题。

现在我们拿这个玩意引用某个数字，比如m

$$
nSm=(\lambda z.(z+n))(m)=m/z=m+n
$$

以上是我觉得比较清晰且满意的理解方法。

这一块的证明参考 https://brilliant.org/wiki/lambda-calculus/

再举个例子，2+3，这次不使用任何简写，直接完全展开。

$$
2S=\newline
(\lambda sz.s(s(z)))(\lambda wyx.y(wyx))=\newline
\lambda z.(\lambda wyx.y(wyx))((\lambda abc.b(abc))(z))=\newline
\lambda z.(\lambda wyx.y(wyx))(\lambda bc.b(zbc))=\newline
\lambda z.(\lambda yx.y((\lambda bc.b(zbc))yx))=\newline
\lambda z.(\lambda yx.y((\lambda c.y(zyc))x))=\newline
\lambda z.(\lambda yx.y(y(zyx)))\newline
$$

$$
2S3=\newline(\lambda z.(\lambda yx.y(y(zyx))))(\lambda sb.s(s(s(b))))=\newline
(\lambda yx.y(y((\lambda sb.s(s(s(b))))yx)))=\newline
(\lambda yx.y(y((\lambda b.y(y(y(b))))x)))=\newline
(\lambda yx.y(y((y(y(y(x)))))))=\newline
5
$$

嗯算真TM算出来了居然，就离谱。不过由于中间的变换式没什么参考性与特殊性，原本还想着能从中学到什么其他有意义的变换式，看样子是不行了。就暂且当作一个迫真例子吧。

这证明里面，要注意避免冲突，修改名称。否则后面全都搞乱了。

理解了一下论文的思路，再来补充一下。

$$
2Sm=\newline
(\lambda sz.s(s(z)))(\lambda wyx.y(wyx))m=\newline
（S替代s）\newline
(\lambda z.(\lambda wyx.y(wyx))((\lambda wyx.y(wyx))(z)))m=\newline
（第二个数字m替代z）\newline
(\lambda wyx.y(wyx))((\lambda wyx.y(wyx))(m))=\newline
S(S(m))=\newline
m+2
$$

通过补全第二个数字m，避免了像刚才的2S3那样对着2S嗯化简，使得式子变得更加复杂了。m能够消去z参数，从而实现nSm到S(S(S(...S(m))))更基本的转变。

乘法

$$
Mul=\lambda xyz.x(yz)
$$

举例：2*2

$$
(\lambda xyz.x(yz))22=\newline
(\lambda yz.2(yz))2=\newline
(\lambda z.2(2(z)))=\newline
(\lambda z.(\lambda sb.s(s(b)))((\lambda mt.m(m(t)))(z)))=\newline
\lambda z.(\lambda sb.s(s(b)))(\lambda t.z(z(t)))=\newline
\lambda z.(\lambda b.(\lambda t.z(z(t)))((\lambda t.z(z(t)))(b)))=\newline
\lambda z.(\lambda b.(\lambda t.z(z(t)))(z(z(b))))=\newline
\lambda z.(\lambda b.(z(z(z(z(b))))))=\newline
\lambda zb.(z(z(z(z(b))))))=\newline
4
$$

这种证明到最后肯定是需要用邱奇数代替一般表示的数字2的。

条件语句

真

$$
T=\lambda xy.x
$$

假

$$
F=\lambda xy.y
$$

这两个函数获取两个参数，然后返回一个参数。

逻辑运算

和

$$
And=\lambda xy.xy(\lambda uv.v)=\lambda xy.xyF
$$

或

$$
Or=\lambda xy.x(\lambda uv.u)y=\lambda xy.xTy
$$

非

$$
Not=\lambda x.x(\lambda uv.v)(\lambda ab.a)=\lambda x.xFT
$$

举例：

$$
And(TT)=(\lambda xy.xyF)(TT)=\newline
(\lambda y.TyF)(T)=\newline
TTF=\newline
T
$$

$$
And(TF)=TFF=F\newline
And(FT)=FTF=F\newline
And(FF)=FFF=F
$$

$$
Or(TT)=TTT=T\newline
Or(TF)=TTF=T\newline
Or(FT)=FTT=T\newline
Or(FF)=FTF=F
$$

$$
Not(F)=FFT=T\newline
Not(T)=TFT=F
$$

条件测试

设计一个检查某数是否为0的函数：

$$
Z=\lambda x.xF\neg F
$$

首先得知道

$$
0fa=(\lambda sz.z)fa=a
$$

意思就是，将函数f在a上应用0次的结果（0f的意思）返回的还是a。

同时F应用于任意对象上面返回的都是I函数

$$
Fa=(\lambda xy.y)a=\lambda y.y=I
$$

测试Z函数：

$$
Z0=(\lambda x.xF\neg F)(\lambda sz.z)=\newline
(\lambda sz.z)F\neg F=\newline
0F\neg F=\newline
\neg F=\newline
T
$$

$$
Zn=(\lambda x.xF\neg F)n=\newline
nF\neg F=\newline
(nF)\neg F
$$

nF意味着要对$\neg$应用n次的F函数，但是我们知道F应用于任意对象无数次返回的都是I函数，所以

$$
IF=\newline
F
$$

前序函数（Predecessor）

前面我们了解过后继函数，即从n获得n+1。现在了解前驱函数，即实现(n, n-1)的序列。

对（pair）

由a和b组成的一个对(a, b)可以通过以下λ函数表示：

$$
\lambda x.xab
$$

其中传参是F或T

比如要取第一个值，那么应用T

$$
(\lambda x.xab)T=\newline
Tab=\newline
a
$$

取b

$$
(\lambda x.xab)F=\newline
Fab=\newline
b
$$

想要获得前驱函数P，首先考虑以下函数：

$$
\Phi=(\lambda pz.z(S(pT))(pT))
$$

函数有2个形参，p传入一个对；z传入T或F，用于选择第一个数还是第二个数字，即递增1还是返回原来数字。

主体有三个块，z，S(pT)，pT。S是后继函数。

比如将Φ应用于(λx.xab)T上面：

$$
(\lambda pz.z(S(pT))(pT))((\lambda x.xab)T)=\newline
T(S((\lambda x.xab)T))((\lambda x.xab)T)=\newline
T(S(a))(a)=\newline
S(a)=\newline
a+1
$$

而如果是(λx.xab)F，则返回第二个参数，那就是a。

获得数字n的前驱可以将Φ应用n次于对λz.00上，然后选择新对的第二个数字：

$$
P=\lambda n.((n\Phi)(\lambda z.z00)F)
$$

比如

$$
P2=(2\Phi)(\lambda z.z00)F=\newline
(\lambda z.\Phi(\Phi(z)))(\lambda z.z00)F=\newline
(\Phi(\Phi((\lambda z.z00))))F=\newline
(\Phi(\lambda z.z(1)(0)))F=\newline
(\lambda z.z21)F=\newline
1
$$

不过值得注意的是，根据这个定义，0的前驱还是0。

相等与不等

先定义大于等于：

大于等于

$$
G=(\lambda xy.Z(xPy))
$$

xPy即将P应用于y上x次，即获得y-x（当然由于函数P的特性，最小值是0，不会变成负数）

然后再扔进Z函数进行判断：返回T意味着y-x<=0，即x>=y。

等于

当x>=y且x<=y时，x==y。

$$
E=(\lambda xy.And((Z(xPy)(Z(yPx)))))
$$

同理，还可以定义大于，小于，不等函数。

递归

递归函数可以使用一个函数，这个函数调用函数y然后再重新生成它自身。

$$
Y=(\lambda y.(\lambda x.y(xx))(\lambda x.y(xx)))
$$

Y应用于R上：

$$
YR=(\lambda x.R(xx))(\lambda x.R(xx))=\newline
R((\lambda x.R(xx))(\lambda x.R(xx)))=\newline
R(YR)
$$

假设定义一个函数，能够对前n个自然数求和。我们使用递归定义法，因为

$$
\sum_{i=0}^n i=n+\sum_{i=0}^{n-1}i
$$

$$
R=(\lambda rn.Zn0(nS(r(Pn))))
$$

Zn用于判断传入参数的个数是否为0，如果是0，那么返回了T，那么整个函数就会返回T紧跟的数字0。

n不为0，那么就会返回后面的(nS(r(Pn)))，即将S后继函数对r(Pn)应用n次。r是一个递归调用，Pn便是n-1。

不过我们如何知道r是一个递归参数？我们不清楚，所以我们需要用Y操作符来尝试。

使用Y递归操作符实现0+1+2+3：

$$
YR3=R(YR)3=Z30(3S(YR(P3)))=\newline
F0(3S(YR(P3)))=\newline
3S(YR2)=\newline
$$

化简到这里，就能发现这个式子就是sum(3)=3+sum(2)了。

化简到最后：

$$
3S2S1S0=\newline
6
$$

预留任务

1. 定义小于，大于和不等
2. 定义正整数与负数
3. 定义加法和减法
4. 递归定义正整数除法
5. 定义n!
6. 以数字对定义有理数（分数法）
7. 定义有理数加减乘除
8. 定义数字列表
9. 定义列表取值函数a[i]
10. 定义len()递归函数，能够计算列表大小
11. 使用λ函数模拟图灵机

参考

1. https://brilliant.org/wiki/lambda-calculus/#ordered-pairs
2. https://zh.wikipedia.org/wiki/%CE%9B%E6%BC%94%E7%AE%97
3. https://personal.utdallas.edu/~gupta/courses/apl/lambda.pdf