关于 H* 模型的刻画：操作层面

针对无类型 $\lambda$-演算的一大类模型，我们刻画了其中那些对头规范化完全抽象的模型，即其等式理论为 $\mathcal{H}^*$。一个广延 K-模型 $D$ 是完全抽象的，当且仅当它是超免疫的，即 $D$ 中元素的非良基链不能被任何递归函数捕获。本文与其姊妹篇及一个短版共享第一标题。它是一篇独立论文，给出了该结果的纯语法证明，而其姊妹篇给出了完全相同结果的独立且纯语义的证明。