Strong normalisation for applied lambda calculi

TL;DR

This paper introduces a domain-theoretic model demonstrating that in certain lambda calculi, all well-typed terms are strongly normalising if their constants are total, extending to systems like G"odel's T and F with bar recursion.

Contribution

It provides a general normalisation theorem for applied typed lambda-calculi, including extensions with bar recursion, establishing strong normalisation under totality conditions.

Findings

All typeable terms are strongly normalising if constants have total values.

The model applies to extensions of G"odel's T and system F with bar recursion.

Strong normalisation was previously unknown for these extended systems.

Abstract

We consider the untyped lambda calculus with constructors and recursively defined constants. We construct a domain-theoretic model such that any term not denoting bottom is strongly normalising provided all its `stratified approximations' are. From this we derive a general normalisation theorem for applied typed lambda-calculi: If all constants have a total value, then all typeable terms are strongly normalising. We apply this result to extensions of G\"odel's system T and system F extended by various forms of bar recursion for which strong normalisation was hitherto unknown.