Syntactic analysis of eta-expansions in Pure Type Systems
By a detailed analysis of the interaction between -reduction -->(beta) and eta-expansion -->((&eta;) 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(&eta;) over bar) from that of -->(beta) and -->((&eta;) 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.
pure type systems strong normalization q-expansion