类型论 2025.1.6

· · 个人记录

定义 A.1.1(\lambda-term): 设 V 是一个无穷集，或者说 "字" 集/符号集. 我们构造一个集合 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 $(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) $(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$ . 那么:
t \langle t_1 /y \rangle = \lambda x \ x(y) \langle t_1 / y \rangle = \lambda x \ x \langle t_1 / y \rangle (y \langle t_1 / y \rangle)= \lambda x \ x(t_1) =\lambda x \ x (\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)). 关于 $A.1.8(3)$ : 为什么这么定义的话，似乎是因为前面的 $\lambda x$ 和 $\lambda x'$ 是不同的，而 $\langle y / x \rangle$ 或 $\langle y / x' \rangle$ 这一项可以加入到前面只有是 $u$ 的结尾可能有出现 $x$ 或者 $x'$, > **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'$ 当且仅当满足以下条件之一: $$(a). T' = U_1 (U_2'), 且 U_2 \beta_0 U_2'$$ $$(b).T' = U_1' (U_2), 且 U_1 \beta_0 U_1'$$ $$(c).U_1 =\lambda x W, 且 T' = W[U_2/x]$$ 我们记 $\cong_\beta$ 是最小的包含 $\beta_0$ 的等价关系. 其中 $(c).$ $T= \lambda x W (U_2)$ , 我们希望 $T' = W[U_2/x]$ 这样，似乎是比较弱的？ 参考文献 : Jean-Leuis Krivine : Lambda-calculus , type and models