A domain-theoretic characterisation of strong normalisation
for the Lambda-R-calculus

Ulrich Berger, Swansea

Abstract

Building on work by Coquand and Spiwack we construct a strict
domain-theoretic model for the untyped lambda-calculus with
constructors and recursively defined constants, which has the property
that a term is strongly normalising if and only if its value is not
bottom.  There are no disjointness or confluence conditions imposed on
the rewrite rules, and it is possible for one function symbol to have
infinitely many rules.  As an application, we prove strong
normalisation for system F extended by barrecursion, non-deterministic
choice, omega-rule, and permutative conversions.