注：这篇文章主要是写给自己和lcw看的，可能会比较混乱和难以理解
默认的概念：
-
对象：数学上一切皆可以看做对象。
-
朴素的相等关系（\(=\not=\)）：一个对象始终等于其本身，不等于其他任何一个对象。
-
定义：定义是给满足某种条件的一类对象起名字。
-
标识符：又叫做名称或者代数，指代对象所使用的名字。
-
表达式：又叫做算式，一个由若干个对象有序排列所构成的整体。
-
逻辑量词：任意（\(\forall\)）、存在（\(\exists\)）。
逻辑对象与运算
1 定义 有序对：有序对是一种特殊的对象。由两个对象 \(a,b\) 所构成的整体，就是有序对，记作 \((a,b)\)。
2 记号 \((a,b,c)\)：若一个有序对所包含的第二个对象是另一个二元组，则我们可以使用简化记号 \((a,b,c)\) 表示 \((a,(b,c))\)。
3 定义 lambda表达式：在lambda演算系统中，一个合法的lambda表达式能且仅能为下面三种中的任意一种（下面简称“合法的lambda表达式”为“表达式”）：
-
标识符：用于代指一个对象 \(x\)，如果已经定义了这个名称所对应的对象，则称为绑定名称，否则称为自由名称，记作 \(x\)。
-
抽象：一个由标识符 \(x\) 和表达式 \(M\) 所组成的特殊的有序对，记作 \(\lambda x.M\)。
-
应用：一个由表达式 \(M\) 和表达式 \(N\) 所组成的特殊的有序对，记作 \(MN\)。
4 记号 消除歧义约定：考虑到有的表达式直接书写会产生歧义（例如 \(\lambda x.xy\)，可以解释为 \(\lambda x.(xy)\) 或者 \((\lambda x.x)y\)），为此我们必须在必要的地方添加括号以改变运算顺序。另一方面，在不添加括号时，我们约定：
-
一个抽象的表达式部分将尽最大可能向右扩展，即：\(\lambda x.MN\) 代表的是一个抽象 \(\lambda x.(MN)\) 而不是应用 \((\lambda x.M)N\)。
-
应用是左结合的，即 \(M N P\) 意为 \((M N) P\) 而非 \(M (N P)\)。
5.1 定义 替换规约：对于一个表达式 \(M\)，将其中所有的自由名称 \(a\) 替换为 \(b\)，记作 \(M[a\leftarrow b]\)。
5.2 定义 \(\beta\)规约：对于一个应用 \(MN\)，其中 \(M\) 是一个形如 \(\lambda x.E\) 的抽象，则应用 \(MN\) 可以规约为 \(E[x\leftarrow N]\)。
5.3 定义 \(\alpha\)规约：对于一个抽象 \(\lambda x.x\) 和一个任意标识符 \(y\)，抽象 \(\lambda x.x\) 可以规约为 \(\lambda y.y\)。
5.4 定义 \(\eta\)规约：对于一个形如 \(\lambda x.f x\) 的抽象，可以将其规约为 \(f\)。
5.5 定义 表达式等价：我们称表达式 \(a\) 和表达式 \(b\) 是等价的，当且仅当 \(a\) 和 \(b\) 分别通过有限次规约（上述四种任意）后可以得到一个相等的表达式，或者一个表达式经过有限次规约后可以分别得到 \(a\) 和 \(b\)，此时记作 \(a\equiv b\)，否则称 \(a\) 和 \(b\) 不等价，记作 \(a\not\equiv b\)。
6.1 定义 真：我们称 \(\lambda x.\lambda y.x\) 为真（又称为K组合子），记作 \(\circledast\) 或 \(\mathrm K\)。
6.2 定义 假：我们称 \(\lambda x.\lambda y.y\) 为假（又称为 \(0\)），记作 \(\circledcirc\) 或 \(0\)。
7.1 定义 逻辑非：我们称 \(\lambda x.x \circledcirc\circledast\) 为逻辑非运算，记作 \(\lnot x\)
7.2 定义 逻辑与：我们称 \(\lambda x.\lambda y.xyx\) 为逻辑与运算，记作 \(x\wedge y\)。
7.3 定义 逻辑或：我们称 \(\lambda x.\lambda y.xxy\) 为逻辑或运算，记作 \(x\vee y\)。
7.4 定义 逻辑异或：我们称 \(\lambda x.\lambda y.x(\lnot y)y\) 为逻辑异或运算，记作 \(x\oplus y\)。
8 定义 命题：一个表达式 \(p\) 被称为命题，当且仅当 \(p\) 与真等价或者 \(p\) 与假等价。
9.1 定义 蕴含：我们称 \(\lambda x.\lambda y.xy\circledast\) 为蕴含，记作 \(x\Rightarrow y\)。
9.2 定义 命题等价：我们称 \(x\Leftrightarrow y\)，是指 \(x\Rightarrow y\wedge y\Rightarrow x\)。
基础建设
10.1 定义 Y组合子：我们称 \(\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))\) 为Y组合子，记作 \(\mathrm Y\)。
10.2 定义 I组合子：我们称 \(\lambda x.x\) 为I组合子，记作 \(\mathrm I\)。
10.3 定义 S组合子：我们称 \(\lambda x.\lambda y.\lambda z.xz(yz)\) 为S组合子，记作 \(\mathrm S\)。
10.4 定理：\(\mathrm I\equiv\mathrm S\mathrm K\mathrm K\)。（证明显然）
10.5 二元组：我们称 \(\lambda x.\lambda y.\lambda f.fxy\) 为二元组，记作 \(\mathrm P\)。
10.6 定义 B组合子：我们称 \(\lambda x.\lambda y.\lambda z.x(yz)\) 为B组合子，记作 \(\mathrm B\)。
10.7 定义 W组合子：我们称 \(\lambda x.\lambda y.xyy\) 为W组合子，记作 \(\mathrm W\)。
自然数
11.1 定义 后继运算：我们称 \(\lambda n.\lambda f.\lambda x.f(nfx)\) 为后继运算，记作 \({}^+n\)。
11.2 记号 后继：我们称 \(a\rightarrow b\)，是指 \({}^+a\equiv b\)。
12 定义 可达：对于两个表达式 \(a,b\)，我们称 \(a\) 可达 \(b\)，当且仅当下面两点中的任意至少一点成立，记作 \(a\rightsquigarrow b\)，否则称 \(a\) 不可达 \(b\)，记作 \(a\not\rightsquigarrow b\)。
-
\(a\rightarrow b\)
-
\(\exists_{c}a\rightsquigarrow c\wedge c\rightsquigarrow b\)
13.1 定义 自然数： 我们称表达式 \(a\) 是一个自然数，当且仅当 \(a\leftrightarrow0\vee0\rightsquigarrow a\)。（注：这个定义等价于表达式 \(\mathrm Y(\lambda f.\lambda n.n(\lambda x.\mathrm Bf(\lambda n.n(\lambda p.\mathrm P(\mathrm B{}^+p\circledast)(p\circledast))(\mathrm P00)\circledcirc)x)\circledast)a\) 可以规约到 \(\circledast\)。）
13.2 记号 \(1,2,\cdots\)：我们记 \(1={}^+0,2={}^+1,\cdots\)。
14.1 定义 加法：\(\lambda m.\lambda n.\lambda f.\lambda x.mf(nfx)\) ，记作 \(m+n\)。
14.2 定义 零命题：\(\lambda n.n(\lambda x.\circledcirc)\circledast\)，记作 \(n=0\)。
14.3 定义 乘法：\(\lambda m.\lambda n.m(+n)0\)，记作 \(m\times n\)。
14.4 定义 正自然数：对于一个自然数 \(n\)，当且仅当 \(n(\lambda x.\circledast)\circledcirc\) 等价于 \(\circledast\) 时 \(n\) 被称为正自然数。
14.5 定义 自然数指数运算：\(\lambda m.\lambda n.nm\)，记作 \(m^n\)。
15.1 定义 前驱：\(\lambda n.n(\lambda p.\mathrm P(\mathrm B{}^+p\circledast)(p\circledast))(\mathrm P00)\circledcirc\)，记作 \({}^-n\)。
15.2 定义 半减法：\(\lambda m.\lambda n.n{}^-x\)，记作 \(m\ominus n\)。
15.3 定义 自然数小于等于：\(n\ominus m=0\)，记作 \(n\leqslant m\)。
15.4 定义 自然数大于等于：\(m\leqslant n\)，记作 \(n\geqslant m\)。
15.5 定义 自然数等于：\(n\leqslant m\wedge n\leqslant m\)，记作 \(n=m\)。
15.6 定义 自然数小于：\(n\leqslant m\wedge\lnot n=m\)，记作 \(n<m\)。
15.7 定义 自然数大于：\(m<n\)，记作 \(n>m\)。
16.1 定理 加法交换律：对于自然数 \(n,m\)，\(n+m=m+n\)。
证明：TODO:补充证明 \(\qquad\texttt{Q.E.D}\)
16.2 定理 乘法交换律：对于自然数 \(n,m\)，\(n\times m=m\times n\)。
证明：TODO:补充证明 \(\qquad\texttt{Q.E.D}\)
TODO: 补充其他运算性质
集合
17 定义 可判定对象：一个对象 \(x\) 要么是不可判定的，要么存在一个抽象 \(\triangle_x\)，满足对其进行 \(\beta\)规约时有
\[_\beta\triangle_xy=\begin{cases}\mathrm K &\text{可判定}x\equiv y\\0 &\text{其他情况}\end{cases} \]18.1 定义 空集：\(\lambda x.\circledcirc\)，记作 \(\varnothing\)。
18.2 定义 单元素集：对于一个可判定的对象 \(x\)，\(\lambda a.\triangle_xa\) 为关于 \(x\) 的单元素集，记作 \(\{x\}\)。
18.3 定义 属于：\(\lambda A.\lambda x.Ax\)，记作 \(x\in A\)，其中 \(x\) 是一个可判定对象，\(A\) 为一个表达式。
18.4 定义 并集：\(\lambda A.\lambda B.\lambda x.Ax\circledast Bx\)，记作 \(A\cup B\)，其中 \(A,B\) 均为表达式。
19 定义 有限制的集合：一个集合是有限制的集合，当且仅当
to be continued...
标签：定义,演算,自然数,circledast,数学分析,lambda,表达式,mathrm From： https://www.cnblogs.com/szdytom/p/lambda-calculus-basis.html