类型论 2025.1.6

定义 A.1.1($\lambda$-term): 设 $V$ 是一个无穷集，或者说 "字" 集/符号集. 我们构造一个集合 $L$ ，其是由符号组成的词语/句子组成的集合. 其构造如下:

基本元素/符号准备: $(1).$ $\forall x \in V, x \in L$ . $(2).$ 假设 $( \notin V, ) \notin V$ (存在性见集合论有关内容) . 但 $( \in L,) \in L$ . $(3).$ 假设 $\lambda \notin V$ , 但 $\lambda \in L$.

构造规则:

$(1).$ 如果 $x,y \in V$ , 那么 $x(y) \in L$. $(2).$ 如果 $x \in V , t\in L$ , 那么 $\lambda xt \in L$ .

此构造规则亦可看做某种输入输出的东西. 考虑到我们可以有好多不同的 $\lambda$, 可以视 $\lambda$ 为某种对 $x$ 的操作，这个操作得到了某个 $t$ , 然后整个结果我们记为 $\lambda x t$ . 当然你可能会问，似乎 $\lambda x t_1$ , $\lambda xt_2$ 等等都是合法的词啊，这会不会存在歧义？答案是不会，可以视这个过程为创造所有的我们 "能写出来" 的词 , 而那些是 "合法" 的,或者说是有意义的，可以再做规定. (因为我们还没有对 $\lambda$ 有任何的规定性)

Example A.1.2: 我们可以写出很多在 $L$ 中的元素 , 比如 $\lambda x x \in L$ , $\lambda x(t) \in L , \lambda x \lambda y x(y) \in L$ 等等.

约定 A.1.3: $t(u_1(u_2(...(u_k))))$ 在无歧义时记为 $tu_1u_2...u_k$ . (实际上有可能会有歧义)

定义 A.1.4(Free occurence): 设 $x \in V ,t \in L$, 我们称 $x$ 在 $t$ 中是自由的:

$(1).$ 如果 $t=x$. $(2).$ 如果 $t=u_1(u_2)$, 那么只有当 $x$ 在 $u_1$ 或者在 $u_2$ 中是自由的 $(3).$ 如果 $t= \lambda y u, y\neq x$, 那么当 $x$ 在 $u$ 中是自由的.

$(4).$ 如果 $t = \lambda x u$ , 那么 $x$ 在 $t$ 中不是自由的. (也就是说后面 $u$ 中无论有没有括号都没用了)

自由即意味着：“没有任何约束”，而这个定义即将 $\lambda$ 视为对这些本来没有任何意义的符号带来一定的限制，此时其即不再是自由的. 而括号则具有某种 "划分区域" 的含义，即之前被 $\lambda$ 污染过的 (bushi) 符号在括号的范围之外又焕然一新了！

如果 $x$ 在 $t$ 中至少有一个自由位置，那么我们称 $x$ 是在 $t$ 中的自由变量（至少在一处自由） 如果 $x$ 出现在一个 $\lambda$ 后面且被这个 $\lambda$ 限制，那么我们称 $x$ 是在 $t$ 中被限制的（至少在一处被限制）

Example A.1.5: 设 $u_1 =x, u_2 =\lambda x x$, 那么在 $u_1(u_2) = x(\lambda xx)$ 中，只有第一个位置的 $x$ 是自由的，而在 $\lambda x \lambda y x(y)$ 中没有自由的 $x$ .

定义 A.1.6(Subotitutia): 设 $t,t_1,...,t_k$ 是 $L$ 中的元素，$x_1,...,x_k$ 是在 $V$ 中的不同的元素, 我们定义 $t \langle t_1/x_1,...,t_k/x_k \rangle \in L$ .其有以下的规定性 (在这里的等于号更贴近某种替换的含义，或者理解为 "可替换为):

$(1).$ 如果 $t= x_i$, 那么 $t \langle t_1/x_1,...,t_k / x _k \rangle =t_i$
$(2).$ 如果 $t \in V \setminus \{ x_1,...,x_k \}$ , 那么 $t \langle t_1/x_1,...,t_k/x_k \rangle = t$ . (即后面这坨对 $t$ 没有意义) $(3).$ 如果 $t= u_1(u_2)$, 那么 $t\langle t_1/x_1,...,t_k/x_k \rangle=u_1 \langle t_1/x_1,...,t_k/x_k \rangle (u_2 \langle t_1/x_1,...,t_k/x_k \rangle)$ $(4).$ 如果 $t= \lambda x_i u$ , 那么 $t \langle t_1/x_1,...,t_k/x_k \rangle = \lambda x_i u \langle t_1 / x_1 ,...,t_{i-1} / x_{i-1} , t_{i+1} / x_{i+1}, ..., t_k / x_k \rangle$ $(5).$ 如果 $t= \lambda x u$, $x \notin \{ x_1,...,x_k \}$ . $t \langle t_1 / x_1,...,t_k /x _k \rangle = \lambda x u \langle t_1 / x_1,...,t_k /x_k \rangle$ 表面上没做仍和操作，但是实际上我们接下来就考虑的是 $u \langle t_1/x_1,...,t_k/x_k \rangle$ 是否还能继续往下递归了.

Example A.1.7: 设 $t= \lambda x x(y), t_1 = \lambda x x$ . 那么:

定义 A.1.8($\alpha$-Equivalence): 我们定义一个在 $L$ 上的二元关系 $\equiv$ , 我们以递归的方式去定义:

$(1).$ 如果 $t \in V$ , $t \equiv t'$ 当且仅当 $t=t'$ . (回忆 $V \subseteq L$ 是 $L$ 的最基本的零件) $(2).$ 如果 $t=u_1(u_2)$, $t \equiv t'$ 当且仅当存在 $u'_1,u'_2 \in L$, 使得 $t'=u'_1 (u'_2)$ 且 $u'_1 \equiv u_1,u'_2 \equiv u_2$ . $(3).$ 如果 $t= \lambda x u$ , $t \equiv t'$ 当且仅当 $t'$ 是形如 $t' = \lambda x' u'$ 的形式，且 $u \langle y/x \rangle \equiv u' \langle y / x' \rangle$ . (For all but finitely many $y \in V$ (what)).

Facts A.1.9: $(1).$ $\equiv$ 是一个 $L$ 上的等价关系，$(2).$ 如果 $t \equiv t'$ ，则其至少具有相同的自由变量 （ 自由变量可以视为全局变量，此断言由 $A.1.8(1)$ 立见）.

$(3).$ $t,t',t_1,t_1',...,t_k,t_k'$ 是 $L$ 中的一些元素，$x_1,...,x_k$ 是不同的变量，如果 $t \equiv t'$ 且 $\forall i \in \{1,...,k\} \ \ t_i \equiv t'$ , 且在 $t_1,...,t_k$ 中的自由变量没有在被 $t,t'$ 中限制，或者说他们在 $t,t'$ 中仍然是自由的，那么: $t \langle t_1/ x_1,...,t_k / x_k \rangle \equiv t' \langle t'_1 / x_1 , ... ,t'_k / x_k \rangle$ 首先注意到自由变量在 $\equiv$ 下保持不变，故而由 $A.1.6(1)$ 可得，是唯一可能使得 $t_1,...,t_k$ "影响"到上述式子的的方式, 而此时 $t_i$ 中的元素会原封不动的加入到 $t$ 或者 $t'$ 的最后面，而此时他们如果还需要等价，就需要 $t_i$ 中元素的"自由"性没有被 $t,t'$ 影响.

$(4).$ $\equiv$ 是 $\lambda$-Compatible, 即 : 如果 $t \equiv t'$, 那么 $\lambda x t \equiv \lambda x t'$. (可能根据 $A.1.8(3)$)

因此我们可以构造一个 $\bigwedge := L / \equiv$ , 在上面可以过渡 $L$ 的很多性质: $(a).$ 对于任意 $U_1,U_2 \in \bigwedge$ , 取 $u_1$ 和 $u_2$ 为他们的代表元，那么 $U_1(U_2)$ 是 $u_1(u_2)$ 的等价类 $(b).$ $\forall x \in V, T \in \bigwedge$ , $t$ 是 $T$ 中的代表元，那么 $\lambda x T$ 是 $\lambda x t$ 的等价类.

$(5).$ 如果 $y$ 不在 $t$ 中出现，那么 $\lambda x t \equiv \lambda y t \langle y / x \rangle$ . (既然 $t$ 中没有 $y$ , $t \langle y / x \rangle$ 的结果中可能多出 $x$, 而 $x,y$ 均不是自由元，故而可以在等价关系下替换?)

$(6).$ 对于 $t \in L , x_1,...,x_k \in V$, 存在 $t' \in L, t' \equiv t$, 满足 $x_1,...,x_k$ 均不是在 $t'$ 中被限制的元素（已经自由的全局变量不用换，局部变量可以换名字）

$(7).$ 对于 $T \in \bigwedge$ , 所有 $T$ 中的代表元具有相同的自由变量，故而可以良定的称呼为 $T$ 的自由变量.

定义 A.1.10: 设 $T,T_1,...,T_k$ 都是 $\bigwedge$ 中的元素，取 $t,t_1,...,t_k$ 为他们的代表元，且满足 $t_1,...,t_k$ 中都是自由的字在 $t$ 中都是自由的. 那么我们定义 : $T [T_1/x_1,...,T_k/x_k] := \text{the equivalance class of }t \langle t_1/x_1,...,t_k /x_k\rangle$

Fact A.1.11: $(1).$ 如果 $x_1$ 在 $T$ 中不是自由的，那么: $T[T_1/x_1,...,T_k/x_k] = T[T_2/x_2,...,T_k/x_k]$ 似乎是因为 $A.1.6(4)$，若 $x_1$ 不是自由的 ，其肯定就不在 $\lambda xu$ 中的 $u$ 中出现，此时可以省去一项. $(2).$ 设 $x_1,...,x_m,y_1,...y_n$ 满足 $x_1=y_1,x_2=y_2,...,x_k=y_k$, 且 $x_1,...,x_m,y_{k+1},...,y_n$ 是两两不同的，$T,T_1,...,T_m,U_1,...,U_n$ 是 $\bigwedge$ 中的元素， $T_i'= T_i [U_1/y_1,...,U_n/y_n]$ , 那么: $T[T_1/x_1,...,T_m/x_m][U_1/y_1,...,U_n/y_n]= T[T_1'/x_1,...,T'_m/x_m,U_{k+1}/x_{k+1},...,U_n/y_n]$ $(3).$ 如果 $i \in \{ 1,..., k \}$ , 我们有 $x_i[T_1/x_1,...,T_k/x_k] = T_i$ . (和 $A.1.6(1)$ 类似) $(4).$ 对于 $x \in V \setminus \{x_1,...,x_k \}$, $x [T_1/x_1,...,T_k/x_k]=x$. (和 $A.1.6(2)$ 类似) $(5).$ 如果 $T = \lambda x U$, 其中 $x$ 在 $T_1,...,T_k$ 中不是自由的且 $T[T_1/x_1,...,T_k/x_k]= \lambda x U [T_1/x_1,...,T_k/x_k]$ (和 $A.1.6(4)$ 类似) $(6)$ $\lambda x U (T) = \lambda x' U' (T') \Rightarrow U[T/x] = U'[T'/x]$ . 这个也和 $A.1.6(5)$ 类似.

定义 A.1.12($\beta$-conversion): 我们定义在 $\bigwedge$ 上的二元关系 $\beta_0$, 其满足:

$(1).$ 如果 $x \in V$, 那么不存在相异的 $T'$ 使得 $x \beta_0 T'$ . $(2).$ 如果 $T = U_1(U_2)$, $T \beta_0 T'$ 当且仅当满足以下条件之一: