Journal of Logic and Computation, Volume 10, Issue 3, pp. 381-410: Abstract.
A syntactical analysis of normalization
Z Khasidashvili1 and A Piperno2
1Department of Mathematics and Computer Science, Bar-Ilan University, Ramat-Gan 52900, Israel, E-mail: email@example.com, 2Dipartimento di Scienze dell'Informazione, Università di Roma 'La Sapienza', Via Salaria 113, 00198 Roma, Italy, E-mail: firstname.lastname@example.org
Some [lgr]-terms exhibit the following alternation property: whenever a redex having the shape ([lgr]x.P) ([lgr]y.Q) is created in a reduction path starting with the contraction of M N, then either [lgr]x appears in M and [lgr]y in N, or [lgr]x appears in N and [lgr]y in M. In this paper, we investigate the alternation property and we establish its relevance in the context of typed calculi. In particular, we prove that the alternation property implies normalization. To this aim, we use a simple technique based on labels. The intended meaning of the labelling is to give information about the minimal number of contractions needed by a variable to be substituted during the reduction process. Further, we apply this result to obtain new normalization proofs for Curry's simply typed lambda calculus and, similarly, for terms typable with intersection types.
Keywords: Lambda-calculus, type assignment systems, normalization