A Predicative Strong Normalisation Proof for a λCalculus with Interleaving Inductive Types

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 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.

The use of the term interleaving for this situation is due to Ralph Matthes, e.g., see [Mat98]. An alternative would be mutually.