λ演算中后继函数单射性证明的合理性问询及等价性证明方法咨询

嗨，看起来你已经摸到λ演算里证明单射性的门道了，你的思路大体是对的，但有几个细节需要再严谨一点，咱们一步步拆解：

首先，你的核心思路是利用外延性——也就是λ项的等价性定义：如果两个项对所有参数的应用结果都相同，那这两个项本身等价（即$M = N$当且仅当对任意$X$，$M X = N X$，这个规则叫η-等价或者外延等价，取决于你用的λ演算系统）。

咱们来梳理你的证明步骤的合理性：

• 从$suc , a = suc , b$推导出$\lambda fx.f (a f x) = \lambda fx.f (b f x)$，这一步完全没问题，因为$suc$的定义就是λ nfx.f(nfx)，直接代入展开就行。
• 接下来你说“对所有$g$和$y$应用后结果相同”，这其实就是用了外延性规则的逆用：如果两个λ抽象等价，那它们对任意参数的应用都等价，这在标准的λ演算系统（比如带外延性的λη演算）里是合法的规则。
• 得到$g (a g y) = g (b g y)$后，你选择了单射的$g$，这里需要明确一点：在λ演算里，我们可以构造出单射的函数项吗？当然可以，比如恒等函数id := λ x.x就是单射的（因为$id , M = id , N$直接推出$M=N$）。当你取$g=id$时，式子就变成$id(a , id , y) = id(b , id , y)$，也就是$a , id , y = b , id , y$，再结合外延性，对所有$y$都成立，所以$a , id = b , id$，再一次用外延性就能推出$a = b$。

你的思路的关键漏洞在于：你需要明确在λ演算的框架内，这样的单射$g$是存在的，不然这个推理就没有根基。不过好在λ演算的表达能力足够，能构造出这样的函数，所以这个步骤是可以补全的。

那λ演算里一般怎么证明等价性呢？主要有几种方法：

• 外延性证明：就是你用的方法，证明两个项对所有可能的参数应用后结果都相同，从而推出项本身等价。这是最常用的方法之一，尤其是证明函数的单射、满射性质时。
• β-归约/η-归约：通过一步步的β-转换（把函数应用展开，比如(λ x.M)N → M[N/x]）或者η-转换（$\lambda x.Mx = M$当$x$不在$M$中自由出现），把两个项归约到同一个标准形式（比如β-范式），从而证明它们等价。
• 归纳法：如果涉及到递归定义的项（比如自然数的Church编码），可以用结构归纳法，对项的结构或者自然数的“大小”进行归纳证明。比如证明后继函数的性质时，可以归纳自然数的编码结构。
• 利用已知的等价性定理：比如Church编码的自然数的性质，配对函数的性质等，把复杂的等价性拆解成已知的简单等价性。

回到你的证明，补全细节后就是一个严谨的证明了：

假设$suc , a = suc , b$，代入$suc$的定义得$\lambda fx.f(a f x) = \lambda fx.f(b f x)$。根据外延性，对任意$g$和$y$，有$g(a g y) = g(b g y)$。取$g$为恒等函数id := λ x.x，则$id(a id y) = id(b id y)$，即$a id y = b id y$。再根据外延性，对任意$y$成立，所以$a id = b id$。又因为对任意$h$，$a h = a (\lambda x.h x) = a id h$（这里用了η-等价，$h = \lambda x.h x$），同理$b h = b id h$，所以$a h = b h$对任意$h$成立，再由外延性得$a = b$。

这样整个证明就严谨了。

备注：内容来源于stack exchange，提问作者Chirmol Studio