A domain model characterising strong normalisation

Building on previous work by Coquand and Spiwack [8] we construct a strict domaintheoretic model for the untyped -calculus with pattern matching and term rewriting which has the property that a term is strongly normalising if its value is not . There are no disjointness or confluence conditions imposed on the rewrite rules, and under a mild but necessary condition completeness of the method is proven. As an application, we prove strong normalisation for barrecursion in higher types combined with polymorphism and non-deterministic choice. Key words: -calculus, term rewriting, normalisation, domain theory

• Type: Journal
• Year: 2008
• Where: APAL
• Authors: Ulrich Berger
• Keywords: APAL 2008, Necessary Condition Completeness, Strict Domaintheoretic Model, Term Rewriting