Lambda 演算入门

1. 单个字母被称为变量
2. 约束变量：一个变量同时出现在函数体和函数参数中
   1. 如 λx.x ，其中 x 同时出现在了 . 字符之前函数参数中和 .字符之后的函数体
   2. 解释为：一个参数为 x ，函数体也为 x 的 函数
3. 自由变量：即变量没有在函数体内被预先声明
4. 一行符号被叫做表达式，或者称为λ项，表达式可以包含
   1. 变量 variables
   2. 函数 function
   3. 应用 application
5. ()括号：有括号时表示期内的表达式是一个整体，没有括号时 从左往右计算

函数

1. λ参数.函数体，. 字符之前为参数，. 字符之后为函数体。这样的一个表达式称为函数
2. 函数可以由一个或多个表达式构成，必须包括头部和身体部分
   1. 头部：.字符之前的部分，由 λ和变量开头
   2. 身体部分： .字符之后的部分，是一个表达式

变量

1. 所有变量都是 λ 形式（即所有变量都是合法的 λ 表达式）
2. 如果，变量 x 和变量 y 都是 λ 形式，那么 (xy) 也是 λ 形式
   1. 即一个字母是表达式，多个字母也是表达式
   2. 两个表达式组合在一起为一个新的表达式
   3. 且 (λx.y) 也是 λ 形式
3. 这样的话，可以理解 (λy.xy)ab 等价于 (((λy.(x y)a))b)
   1. 表达式1 为： (λy.xy) ，y是函数参数，xy 是函数体
   2. 表达式2 为：ab

求值

函数在只有一个表达式的时候是不会进行任何操作的，当它有其他的表达式，那么这个函数就可以被解析（resolving），即求值。

解析过程

这个过程极其类似于我们较为常用的 Ctrl + x 和 Ctrl + v

参数与函数体中有同名变量

1. 以 (λy.x(yz))(ab) 为例
2. 要替换的变量为函数参数 y
3. 然后将表达式2 作为一个整体，替换至表达式1 中的身体部分
4. 删除函数参数 y
5. 得到结果 x(abz)

参数与函数体中没有同名变量

1. 以 (λx.y)a为例
2. 要替换的变量为函数参数 x
3. 但是没有在表达式1 即函数的身体部分 中找到同名变量
4. 那么表达式2 会被删除，因为相当于你 Ctrl + x 了一个变量，但没有找到需要插入的位置
5. 删除函数参数 x
6. 得到结果 y

高阶函数

1. 以 (λx.(λy.x))a为例
2. () 内的整体为函数的身体部分，即表达式1
3. 将表达式1 中的同名变量替换为表达式2
4. 删除函数参数 x
5. 得到结果 λy.a