Lambda演算的简单入门
Lambda 演算 (Lambda Calculus) 是数学家 阿隆佐·邱奇 在 1930 年代发明的一套形式系统，它用非常简单的规则来定义计算、函数和应用。它的目标是探究“什么是可计算？”这一根本问题。
邱奇-图灵论题 The Church-Turing thesis
邱奇-图灵论题 (The Church-Turing thesis) 是计算机科学领域关于可计算性本质的核心假说，提出所有有效可计算函数均可由图灵机实现，常规编程语言具备完整的算法表达能力。该论题通过图灵机模型将数学中的”有效方法”概念形式化，但对”有效方法”本身未给出严格的数学定义。
起源
该论题源于1936年图灵在 《论可计算数及其在判定问题中的应用》 提出的图灵机模型，同时期邱奇通过 λ演算 (也就是我们今天的议题) 和 递归函数 理论描述可计算性。两人分别独立解决了希尔伯特判定性1问题，并证明各自模型的计算能力等价。
哲学思考
论题的哲学内涵涉及数学基础与计算边界问题，其思想源于对希尔伯特计划2的反思，并在哥德尔不完备定理3的背景下发展形成
我们这里要讨论的是Lambda演算，它其实是编程语言中Lambda表达式的源头，但其本身并不服务于计算机语言，而是计算理论
Lambda演算の核心思想
一切皆函数 在 Lambda 演算中，所有东西都是函数。没有数字、字符串、布尔值这些基本类型——它们全都可以用函数的组合来表示。
我们将在接下来的几章中详细探讨并阐述我的个人理解
变量 Variable
代表一个输入值，即实参 (arguments)
- 形如 $x,y,z$
抽象 Abstraction
相当于定义一个函数，并规定输入量，其本身就代表一个函数
- 形如 $\lambda{x}.M$ ，其中 $\lambda$ 是一个函数定义符，它代表一个函数定义的起点
- $M$ 即为函数体，而 $x$ 即为形参 (parameters)
- $M$ 即为返回的值
应用 Application
相当于对函数的调用，其本身输出一个变量
- 形如 $(M N)$，表示将 $M$ 应用于 $N$ ，即 $N \rightarrow M$
- 当然，这个括号不是必须的，总之就是后者应用于前者
你需要搞清楚的是，以上三种东西其实都可以作为一个函数存在，即自然数也被定义为了函数、自然数也是有参数和返回值的函数，在Lambda演算中，所有东西都必须是函数。 当然，我们这里说的“函数”也并非lambda演算的内容，这是为了方便理解所引入的概念 数学语言里描述的种种东西，在lambda演算中都有自己的表达方式，但首先，让我们了解它的基本运算规则
β归约 $\beta\ reduction$
这个过程其实相当好理解，我们有了形参 parameters和实参 arguments，那么就完全可以把实参带入到形参的位置，这就是β-规约 (β-reduction)。比如下面这个例子
\[\lambda x.(xb)E\]注意到这个和上面的Application的模板一样，即 $M=\lambda x.(xb)$ $N=E$ β规约后，我们得到了
\[\lambda x.(xb)E\rightarrow_\beta Eb\]$λ$ 的存在就指定了 $N$ 应该替换的部分，在这个例子里，是 $\lambda x.$ 指定了形参 $x$ 。所以你就将 $N$，这里是$E$，代入进去，并去掉函数的定义部分
另外，当一个式子被β规约到无法继续规约了，我们称其为β标准型 β Normal Form
多参数输入 / 柯里化 Currying
可见，Application这个模板里只允许一个形参的定义和一个实参的传入，那么多参数的传入就需要嵌套了
\[(\lambda x.(\lambda y.x)Y)X\]上面这个演算所实现的功能是输入两个值，只返回前者，在这里为 $X$。我们进行两次β规约，则有
\[\displaylines{ (\lambda y.X)Y\\ X }\]这个过程被我们称作柯里化 Currying。我们之后就直接在 $\lambda$ 和 $.$ 中允许多个变量的存在，以方便观看和阅读
η等价 $\eta-equivalence$
这个是视频里没有讲的，我是通过问AI才问出来的
定义: 如果一个函数$F$对任意一个输入$x$都有$F\ x=G\ x$，那么可以认为$F$与$G$是等价的，写作 \(F =_{\eta}G\)
例如函数 $F:=λx.M x$，对于任意参数$y$都有$F y=(λx.M x) y→βM y$ 所以我们说$F ={\eta}M$ 也就是说，形如上面这种的基本都可以把$x$省略掉
布尔类型的定义
实际上，柯里化中我们给到的式子就是TRUE的表达形式，我们这里再写一遍
\[\displaylines{ \lambda a b.a \equiv TRUE\ (1)\\ \lambda ab.b \equiv FALSE\ (2) }\]可以实验一下，如果给 $(1)$ 传入 $V_1\ V_2$，则会返回 $V_1$ 其实不该说布尔“类型”，而是一个布尔函数，它本质上是一个选择器
if-else定义
所有东西都是函数！包括输入和输出！
上文提到了$TRUE$和$FALSE$本质上是一个选择器
- 如果是$TRUE$，他会选择输入的两个值的前者
- 如果是$FALSE$，他会选择输入的两个值的后者
由此，我们可以很轻易的用它来表示一个if-else函数
\[\lambda X.(X\ A\ B)X\]这里的 $X$ 应当为 $TRUE$ 或者 $FALSE$，而 $A$ 和 $B$ 在 $X$ 输入后作为其两个参数输入，从而实现对 $A$ 或者 $B$ 的选择。其实现的功能伪代码如下
if X == TRUE:
select A
if X == FALSE:
select B
当然，这里的 $X$ 意思是一个 返回 TRUE or FALSE 的函数。
逻辑门定义
$TRUE$ 和 $FALSE$ 的表达式我们上面已经知道了，之后就用英文字符串来代替了
非门实际上是最好想的，只需要把上文提到的 $A$ 和 $B$ 替换为 $FALSE$ 和 $TRUE$ 就行了
\[\lambda X.(X\ FALSE\ TRUE)X\]与门需要两个参数的输入，只有两个都为 $TRUE$ 才返回 $TRUE$，这里我们不妨一级一级去判定。 假设输入的是 $xy$ ，我们先来判定 $x$ ，如果 $x$ 是 $FALSE$，那么返回 $FALSE$，如果 $x$ 不是，则再去判断 $y$，后面不做赘述。 其实不难发现，这是一个if-else的嵌套，所以也可以很容易的写出
\[\displaylines{ (\lambda{xy}.(x\ (y\ TRUE\ FALSE)\ FALSE)\ x\ y)\\ 注意到y\Leftrightarrow(y\ TRUE\ FALSE)，原式可化简为：\\ (\lambda{xy}.(x\ y\ FALSE)\ x\ y) }\]或门同理可得
\[(\lambda{xy}.(x\ TRUE\ y)\ x\ y)\]零判断符 $isZero$
$0$ 有一个性质，那就是其相当于 $FALSE$，对于输入的两个函数，它会将前者执行于后者 $0$ 次，也就是说，他会返回后者本身
\[\lambda n.(n\ (\lambda x.FALSE)\ TRUE)\]这样以来，若 $n=0$ ,则返回 $TRUE$，否则 $(λx.FALSE)$ 至少一次的应用于 $TRUE$，即最终返回 $FALSE$ 进一步解释一下，若 $n\neq0$，这里 $x$ 输入的实际上 $TRUE$，但是由于这个函数不管 $x$ 什么事，只返回 $FALSE$，所以逻辑是自洽的。
小于等于 $leq$
这需要我们下面提到的减法定义作为前提 另外需要注意的是，在执行$(-\ m\ n)$时，若$m<n$，那么其返回值依旧是$0$
很好理解，两个数相减，若其差为$0$，则必满足$m\leq n$
\[leq=\lambda{mn}.(isZero\ (-\ m\ n))\]等于 eq
当且仅当$m\leq n$和$n\leq m$同时成立，满足$m=n$
\[eq=\lambda mn.((AND\ (leq\ m\ n)\ (leq\ n\ m))\ TRUE\ FALSE)\]小于 lt
即小于等于成立且等于不成立的情况
\[lt=\lambda mn.(AND\ (leq\ m\ n)\ (not\ (eq\ m\ n)))\]大于等于 geq
\[geq=\lambda mn.(not\ (lt\ m\ n))\]大于 gt
\[gt = \lambda mn.(not\ (leq\ m\ n))\]在定义自然数之前，我们要理解数学上的自然数是怎么定义的
皮亚诺公理 Peano Axioms
这个公理经常被营销号拿来作秀，即为什么$1+1=2$的问题
皮亚诺公理体系 Peano Axioms针对于一个给定的三元组$(A,0,(.)^)$ 其中的集合$A$是待检验的自然数集合，$0$是$A$中的一个元素，$(.)$代表后计算符，表示$A\rightarrow{A}$的映射
- Axiom 1 : 0是自然数 ($0 \in A$)
- Axiom 2 : 如果$n$是自然数，则它有一个后继$n^*$，且后继也为自然数
- Axiom 3 : 0不是任何自然数的后继 ($\forall n \in A\ :\ n^*\neq 0$)
- Axiom 4 : $n\mapsto n^$是单射 ($\forall n,m\in A:n\neq m \Rightarrow n^\neq m^*$)
- Axiom 5 : 对于命题$P$，若$P$对$0$成立，且$P$对$n$成立蕴涵$P$对$n^*$成立，则$P$对任意自然数皆成立
- 其中公理1,2确定了取自然数的方法
- 公理3,4,5分别确保了“0前面无自然数”，“一个自然数后面只有唯一的一个自然数”，“没有孤岛，闭环存在”。
- 另外，仔细看，公理五其实类似于第一类数学归纳法，即对$0$成立 / 若$n$成立，则$n^*$也成立，则命题对所有自然数均成立
邱奇数 Church numeral
你会发现，你很难在Lambda演算的体系中去定义一个数字，所以这里我们引入邱奇数 Church Numeral
我们假设$0$，即起点为$A$，后继函数为$f(n)$，也就有$0=0$，$1=f(0)$，$2=f(f(0))$……
当然，这里的$0$我们更应该理解为一个变量，即$x$ 我们可以规定$x$为$0$，此时的三元组即为$(A,x,f)$，那么自然数$n$就可以表示为 \(n=f^n(x)\)
再次强调 这些自然数实际上是函数！他们接收两个值，即表示 $0$ 的 $x$ 和后继函数$f$，即 \(n\equiv(\lambda{fx}.(f^n\ x))\) 所以自然数的作用实际上是将 $f$ 应用于 $x$ n次! 另外，先不要管 $f^n$ 要如何表示，我们先利用自然数函数解决下面的问题
后继函数 Succession Function
这样就很轻松的定义了自然数——即一个后继函数 succession function$f$的调用次数 但这也引出了一个新的问题——后继函数 succession function是什么呢？
不妨类比一下现存的自然数体系，我们把后继运算符$()^*$具象化为一个函数$succ(n)$，既有
\[succ(n)=n+1\]那么在Lambda演算中，我们定义的后继函数需要接受一个函数，并返回一个对这个函数运用了一次后继函数之后的函数
- 接收一个数字 $(\lambda n.(\ ))$
- 返回一个数字 $(\lambda n.(\lambda{fx}.\ )$
- 思考一下，我们返回的数字应当是n+1，所以有 $(\lambda n.(\lambda{fx}.(f\ (n\ f\ x)))$
这样，我们就得到了后继函数$succ(n)\equiv (\lambda n.(\lambda{fx}.(f\ (n\ f\ x)))$
后继类运算的定义
再次注意 四则运算的结果也是自然数函数，所以它的返回理所应当的也应该是一个接收f和x的函数!
当我说后继，我指的是自然数不断增大的计算，这是非常好理解的，毕竟皮亚诺定理做的也是单射，即$x\mapsto x*$，但是并没有内置的前驱函数。这个我们在之后解决，先来解决好解决的后继问题
加法
- 接收两个数字 $(\lambda mn. )$
- 思考，要计算$m+1$实际上等价于$succ(m)$，所以$m+n$等价于$succ^n(m)$
- 易知有 $(\lambda mn. (n\ succ\ m))$
- 进一步思考，我们意识到这等同于 $(\lambda mn. (m\ succ\ n))$，于是得到加法交换律
所以加法的式子为
\[(\lambda mn. (n\ succ\ m))\]可以化简为
\[(\lambda{mn.}(\lambda{fx.(m\ f\ (n\ f\ x))}))\]理解一下，$(n\ f\ x)$相当于$n$的定义，所以下一层就有$(m\ f\ n)$，即，将$f$应用于$n$ $m$次，也就有了$m+n$
乘法
有了加法，乘法也很好理解了
\[(\lambda mn. (\lambda fx.(m\ (n f)\ x)))\]就是 m 次将 n 次 f 应用于 x，也就是 m*n。现在我们对其进行柯里化和η等价，有
幂运算
\[λmn.(λfx.((n\ m\ f)\ x))\]幂运算出人意料的简介，不过仔细思考，这是合理的
- 自然数函数接收两个值，即$f$与$x$，这里$n$接收$m$和$f$。
- 光一次$m$应用于$f$即为$f^m$，那么$n$次的将$m$应用于$f$，即为$f^{m^n}$
关于η等价的注意事项 之所以幂函数的$f$能被等价，而上面的乘法不能被等价，是因为$f$在这里是作为单独一个函数存在的，而乘法中的f和n被绑在了一起，作为一个全新函数出现
前驱类运算的定义 / 减法的定义
这里说的前驱类运算单指减法，除法更加棘手 由于没有内置的前驱函数，我们需要手动定义一个。当然这并不像链表一样用一个下标访问前驱地址就行了。在这里，如果我们要“访问”前驱，就得重新模拟一遍加法的过程，直到当前数的前一个数。
前驱拓展
要做到这一点，我们需要在计算时同时记录当前数和前一个数，由此，我们相当可以创建一个数据类型，即$pair$数对，如果需要其中的任何一个值，只需要使用选择器即可
\[pair := (\lambda abz.(z\ a\ b))\]这里的$z$就是选择器，你需要“手动填入”的只是$a$和$b$，输入$TRUE$和$FALSE$即可，我们大可再定义两个函数$fst$和$snd$，这里的$p$就代表一个$pair$类型
\[\displaylines{ fst = \lambda p.(p\ TRUE)\\ snd= \lambda p.(p\ FALSE) }\]接下来，我们要将数对作为新的基底去运算，即一个新的后继函数$\varphi(p)$，应当做到输入$(prev,curr)$返回$(prev+1,curr+1)$，即$(curr,curr+1)$
\[\varphi:=\lambda p.(pair\ (snd\ p)\ (succ\ (snd\ p)))\]那么就会有，
\[(\varphi\ (pair\ 0\ 0)) = (0,1)\]因为“新的数对的前者”取的是“旧数对的后者”，所以0也就留了下来，这样，在$\varphi$对$(pair\ 0\ 0)$进行$n$次运算后，也就得到了$(n-1,n)$
前驱函数
不妨令前驱函数为$pred$，则有
\[pred :=\lambda n. (fst\ (n\ \varphi\ (pair\ 0\ 0)))\]这样，我们就得到了减法函数，虽然无法得到负数
\[\lambda mn.(n\ pred\ m)\]我们以阶乘来举例，就叫$fac(n)$好了，首先在一个高级语言里面写好一个代码逻辑，这里用Python
def FACTORIAL(n):
if n == 0:
return 1
else:
return n * FACTORIAL(n - 1)
可见，有一个边界条件，即判断n是否为0，我们假设这个判断的函数为$IS_0$，在将$n$应用于它后，它会返回一个布尔值，那么这个函数在lambda演算中就可以表示为
\[fac\equiv\lambda n.((IS\_0\ n)\ 1\ (×\ fac\ (-\ n\ 1)))\]$IS_0$实际上是上面提到的零判定符
不动点
对于这种函数套函数的问题，我们中学其实做了很多了，一般有两种办法
- 再进行一次嵌套，从而替换
- 不动点
显然，前者在这里是不管用的，所以我们用不动点来解决这里的循环定义问题
再次明确一下不动点 fixed points的定义 简单来说，对于任意一个函数图像$f(x)$，它与直线$y=x$的交点即为不动点 更准确的说，输入的值和输出的值是一样的
对于一般数学函数的不动点，有些是存在的，而有些在实数平面上是不存在的。 但是lambda演算中，函数的不动点ALWAYS EXISTS
图灵不动点组合子 Turing Fixed Point Combinator
我们假设一个函数$U$为$\lambda xy.(y((xx)y))$，不管这个函数怎么来的，我们有这么个组合子叫做图灵不动点组合子 Turing Fixed Point Combinator
\[\theta = UU\]对于任意一个函数$F$，我们将$\theta$应与于它，通过β规约可以得到
\[\displaylines{ \theta{F}=F(\theta{F})\\ 即F(\theta{F})=\theta{F} }\]也就是说，$\theta{F}$就是$F$的不动点！ 这个组合子可以用来表示任何lambda演算中函数的不动点！
回到我们需要解决的问题上来，我们不妨将$fac$换为$F$，内层的$fac$换位$f$，那么就有
\[F=\lambda n.((IS\_0\ n)\ 1\ (×\ f\ (-\ n\ 1)))\]对两边应用不动点组合子，就有
\[\theta F=(\lambda n.((IS\_0\ n)\ 1\ (×\ f\ (-\ n\ 1))))(\theta F)\]β规约
\[\theta F=(\lambda n.((IS\_0\ n)\ 1\ (×\ (\theta F)\ (-\ n\ 1))))\]这时，你会惊奇的发现$\theta F$和$fac$的位置一模一样，也就是说$\theta F$就是$fac$函数！ 注意！这里我们并没有循环定义！$F$的定义在上面被标明了，而$\theta$也只是一个组合子