A Predicative Strong Normalisation Proof for a-calculus with Interleaving Inductive
A Predicative Strong Normalisation Proof for a-calculus with Interleaving Inductive
复制标题
具有交错归纳的a-演算的预测强归一化证明
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
Andreas Abel
中科院分区：
文献类型：
--
作者：
Andreas Abel
本文给出了严格正归纳类型λ交错的λ-演算的一个新的强规范化证明，它避免了使用非谓词推理，即，Knaster-Tarski定理相反，它只使用表语，即，严格正归纳的定义上的元。为了实现这一点，我们表明，每一个严格的积极运营商的类型产生一个运营商的饱和集，这不仅是单调的，而且（确定性）集为基础的-一个概念介绍了彼得Aczel的背景下，直觉集理论。我们还扩展到共归纳类型使用最大不动点的严格单调算子的元水平。
We present a new strong normalisation proof for a λ-calculus with interleaving strictly positive inductive types λ which avoids the use of impredicative reasoning, i.e., the theorem of Knaster-Tarski. Instead it only uses predicative, i.e., strictly positive inductive definitions on the metalevel. To achieve this we show that every strictly positive operator on types gives rise to an operator on saturated sets which is not only monotone but also (deterministically) set based – a concept introduced by Peter Aczel in the context of intuitionistic set theory. We also extend this to coinductive types using greatest fixpoints of strictly monotone operators on the metalevel.