|
Abstract : |
Abstract. 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 denitions 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 xpoints of strictly monotone, |
