lambda 演算的严格理想完备

由 Kennaway 等人开创的无穷 lambda 演算通过度量完备将基本 lambda 演算扩展至无穷项与归约。依据所选度量，所得无穷演算表现出不同的严格性概念。为获得这些演算的无穷正规化与无穷合流性质，Kennaway 等人将 $\beta$-归约扩展以包含无穷多条“$\bot$-规则”，其将无意义项直接收缩为 $\bot$。所得 B\"ohm 归约演算中有三个具有对应于 B\"ohm 类树的唯一无穷正规形。本文中我们基于理想完备而非度量完备发展了相应的无穷 lambda 演算理论。我们证明我们的每个演算都保守地扩展相应的基于度量的演算。我们的三个演算是无穷正规化且合流的；它们的唯一无穷正规形恰为相应基于度量的演算的 B\"ohm 类树。我们的演算摒弃了基于度量的演算中的无穷多条 $\bot$-规则。完全非严格演算（称为 $111$）仅由 $\beta$-归约组成，而另两个演算（称为 $001$ 与 $101$）需要两条附加规则来精确表述其严格性性质：$\lambda x.\bot \to \bot$（对于 $001$）与 $\bot\,M \to \bot$（对于 $001$ 与 $101$）。