第 1 周：\(\lambda\) 演算¶
\(\lambda\) 项¶
- 变量（名字）：一个变量 x 是一个 \(\lambda\) 项。
- 抽象（定义）：t 是一个 \(\lambda\) 项，x 是一个变量：\(\lambda x.t\) 是一个 \(\lambda\) 项。你暂时可以把 t 看成一个函数，x 是其可能有的形参。
- 应用（调用）：t 和 s 是 \(\lambda\) 项：ts 是一个 \(\lambda\) 项。可能会被写成 ap(ts)。
- \((\lambda x.x) y\)：把 \(\lambda x.x\) 应用于 y。
消岐约定¶
- 一个函数抽象的函数体将尽最大可能向右扩展。
- \(\lambda x.MN\) 是 \(\lambda x.(MN)\) 而不是 \((\lambda x.M)N\)
- 函数应用是左结合的
- MNP 是 (MN)P 而不是 M(NP)
所以 \(\lambda x.(\lambda y.xyz)x\) 是 \(\lambda x.((\lambda y.((xy)z))x)\)。
自由变量与绑定变量¶
类似于形参绑定于函数体，形参是绑定变量，比如 \(\int f(x) \mathrm{d} x\) 里面的 x，可以变成 \(\int f(y) \mathrm{d} y\)。
绑定变量可以任意改名，但是自由变量不可以。
比如 \((\lambda y.y)(\lambda x.xy)\)，前面的 y 是绑定变量，后面的 y 是自由变量；\(\lambda x.(\lambda y.xyz)\) 的 x 和 y 都是绑定变量。
自由变量 Free Variables¶
\[FV(x) = \{x\} \\ FV(\lambda x.t) = FV(t) - \{x\} \\ FV(ab) = FV(a) \cup FV(b)\]
绑定变量 Bound Variables¶
\[BV(x) = \varnothing \\ BV(\lambda x.t) = \{x\} \cup BV(t) \\ BV(ab) = BV(a) \cup BV(b)\]