Syntactic analysis of η-expansions in Pure Type Systems

By a detailed analysis of the interaction between -reduction -->(beta) and eta-expansion -->((η) over bar) in the simply typed lambda-calculus, a modular and purely syntactic proof method is devised in order to derive strong normalization of the combined reduction -->(beta(η) over bar) from that of -->(beta) and -->((η) over bar). It is shown how this technique extends to beta-normalizing functional Pure Type Systems with Barthe's formulation of eta-expansion. (C) 2003 Elsevier Science (USA). All rights reserved.