λ演算中“兼容关系”两种定义的等价性证明正确性验证

$\newcommand{\abstraction}[2]{\lambda #1. #2}$
$\newcommand{\application}[2]{\left(#1 #2\right)}$
$\newcommand{\substitution}[3]{#1 \left[#2 := #3\right]}$
$\newcommand{\freevars}[1]{\operatorname{FV}\left(#1\right)}$ $\newcommand{\closedlambdaset}{\Lambda^{0}}$
$\newcommand{\lambdaexprswithfreevars}[1]{\closedlambdaset\left(#1\right)}$ $\newcommand{\subterm}[1]{\operatorname{Sub}\left(#1\right)}$
$\newcommand{\vars}[1]{\operatorname{Var}\left(#1\right)}$
$\newcommand{\context}[2]{{#1}\left[#2\right]}$
$\newcommand{\hole}{\ }$

你的思路完全没问题，这两种兼容关系定义的等价性证明逻辑是通顺的，我来帮你把细节再理清楚，让整个证明更严谨：

先明确基础定义 #

首先我们先把用到的核心定义再明确一遍：

• 兼容关系的两种定义：

  1. Statement 1（Barendregt原始定义）：二元关系$R \subseteq \Lambda^2$是兼容的，当且仅当对所有$M,M',Z \in \Lambda$，若$(M,M') \in R$，则：
     $$\begin{align}
     \left(\application{Z}{M}, \application{Z}{M'} \right) \in R,\
     \left( \application{M}{Z}, \application{M'}{Z} \right) \in R,\
     \left( \abstraction{x}{M}, \abstraction{x}{M'} \right) \in R
     \end{align}$$
  2. Statement 2（上下文式定义）：二元关系$R \subseteq \Lambda^2$是兼容的，当且仅当对所有$M,M' \in \Lambda$和所有单洞上下文$\context{C}{}$，若$(M,M') \in R$，则$\left( \context{C}{M}, \context{C}{M'} \right) \in R$。

• 上下文的归纳定义（来自你的参考资料）：

  • 变量$x$是一个上下文（无洞）；
  • 空上下文$\context{}{}$是一个上下文（单洞）；
  • 若$\context{C_1}{}$和$\context{C_2}{}$是上下文，则$\application{\context{C_1}{}}{\context{C_2}{}}$是上下文；
  • 若$\context{C_1}{}$是上下文，则$\abstraction{x}{\context{C_1}{}}$是上下文。

从Statement 2推导出Statement 1 #

你提到的单洞上下文的分类完全正确——所有单洞上下文都可以归纳为以下四类：

1. 空上下文$\context{}{}$：此时$\context{C}{M}=M$，$\context{C}{M'}=M'$，显然$(M,M') \in R$能直接推出$(\context{C}{M},\context{C}{M'}) \in R$；
2. 形如$\application{Z}{\context{}{}}$的上下文（其中$Z$是无洞的λ项，即把$\context{C_1}{}$取为$Z$，$\context{C_2}{}$取为单洞上下文）：此时$\context{C}{M}=\application{Z}{M}$，$\context{C}{M'}=\application{Z}{M'}$，根据Statement 2的条件，直接得到Statement 1的第一条；
3. 形如$\application{\context{}{}}{Z}$的上下文（同理，$\context{C_1}{}$取为单洞上下文，$\context{C_2}{}$取为$Z$）：对应Statement 1的第二条；
4. 形如$\abstraction{x}{\context{}{}}$的上下文（$\context{C_1}{}$取为单洞上下文）：对应Statement 1的第三条。

这四类刚好覆盖了Statement 1的所有要求，所以从Statement 2推Statement 1是完全成立的。

从Statement 1推导出Statement 2 #

这里需要用上下文结构的归纳法来严谨证明，你的思路是对的，我们把它细化：

• 基例：当上下文是$\context{}{}$时，结论显然成立（就是$(M,M') \in R$本身）；
• 归纳步骤：
  1. 假设对于单洞上下文$\context{C_1}{}$，有$(M,M') \in R \implies (\context{C_1}{M},\context{C_1}{M'}) \in R$（归纳假设）；
  2. 考虑上下文$\application{Z}{\context{C_1}{}}$（$Z$是任意λ项）：根据Statement 1的第一条，若$(\context{C_1}{M},\context{C_1}{M'}) \in R$，则$(\application{Z}{\context{C_1}{M}},\application{Z}{\context{C_1}{M'}}) \in R$，也就是$(\context{C}{M},\context{C}{M'}) \in R$；
  3. 考虑上下文$\application{\context{C_1}{}}{Z}$：同理，根据Statement 1的第二条，结合归纳假设，可证得结论；
  4. 考虑上下文$\abstraction{x}{\context{C_1}{}}$：根据Statement 1的第三条，结合归纳假设，可证得结论。

因为所有单洞上下文都是通过这几个归纳规则生成的，所以归纳法能覆盖所有情况，包括你提到的像$\application{Z}{\application{A}{\context{}{}}}$或者$\abstraction{x}{\application{Z}{\context{}{}}}$这类复杂的单洞上下文——它们都是通过多次应用归纳规则生成的，每一步都能通过Statement 1的条件保证结论成立。

你担心的“无穷多单洞上下文”其实完全没问题——归纳法就是用来处理这种由有限规则生成的无穷对象的，每一层的上下文都能通过归纳步骤从更简单的上下文推导出来，所以你的核心思路完全正确，没有遗漏关键环节。

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