(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.Robert Recorde Room

Department of Computer Science