A Semantic Strong Normalization Proof for Higher-Order Rewrite Systems

Photograph of Ulrich Berger

Ulrich Berger

(Swansea)

We consider the untyped lambda calculus with constructors and recursively defined constants. We define the n-th approximation of a term M as the term M_n obtained by replacing every constant c with a constant c_n which is defined like c except that it unfolds only n times. We show that if M does not denote bottom in a suitable strict domain-theoretic model and all M_n are strongly normalizing, then M is strongly normalizing. We transfer this result to typed lambda calculi extended by various forms of recursion in higher types for which strong normalization was hitherto unknown. The motivation for this work comes from computational problems arising in connection with program extraction from classical proofs.
Tuesday 5th October 2004, 14:00
Robert Recorde Room
Department of Computer Science