[TD+06] Normalisation is Insensible to Lambda-term Identity or Difference

Abstract

This paper analyses the computational behaviour of lambda-term applications. The properties we are interested in are weak normalisation (i.e. there is a terminating reduction) and strong normalisation (i.e. all reductions are terminating). We can prove that the application of a lambda-term M to a fixed number n of copies of the same arbitrary strongly normalising lambda-term is strongly normalising if and only if the application of M to different arbitrary strongly normalising lambda-terms is strongly normalising. I.e. we have that MX... X (n times) is strongly normalising for an arbitrary strongly normalising X if and only if MX1... Xn is strongly normalising for arbitrary strongly normalising X1,...,Xn. The analogous property holds when replacing strongly normalising by weakly normalising. The proof for weak normalisation uses a detailed analysis on how variables are replaced inside lambda-terms in normal form. For strong normalisation we consider Klop's extended lambda-calculus (for which it is shown that weak normalisation is equivalent to strong normalisation) and we generalise to this calculus the analysis of variable replacements. As an application of the result on strong normalisation we show that the lambda-terms whose interpretation is the top element (in the environment which associates the top element to all variables) of the Honsell-Lenisa model are exactly the lambda-terms which applied to an arbitrary number of strongly normalising lambda-terms produce always strongly normalising lambda-terms. This proof uses a finitary logical description of the model by means of intersection types. Therefore we solve an open question stated by Dezani, Honsell and Motohama.

@inproceedings{tatsdeza06, pdf = {http://www.di.unito.it/~dezani/papers/td.pdf}, author = {Tatsuta, Makoto and Dezani-Ciancaglini, Mariangiola}, booktitle = {{LICS'06}}, editor = {Rajeev Alur}, title = {{Normalisation is Insensible to Lambda-term Identity or Difference}}, abstract = {This paper analyses the computational behaviour of lambda-term applications. The properties we are interested in are weak normalisation (i.e. there is a terminating reduction) and strong normalisation (i.e. all reductions are terminating). We can prove that the application of a lambda-term M to a fixed number n of copies of the same arbitrary strongly normalising lambda-term is strongly normalising if and only if the application of M to different arbitrary strongly normalising lambda-terms is strongly normalising. I.e. we have that MX... X (n times) is strongly normalising for an arbitrary strongly normalising X if and only if MX1... Xn is strongly normalising for arbitrary strongly normalising X1,...,Xn. The analogous property holds when replacing strongly normalising by weakly normalising. The proof for weak normalisation uses a detailed analysis on how variables are replaced inside lambda-terms in normal form. For strong normalisation we consider Klop's extended lambda-calculus (for which it is shown that weak normalisation is equivalent to strong normalisation) and we generalise to this calculus the analysis of variable replacements. As an application of the result on strong normalisation we show that the lambda-terms whose interpretation is the top element (in the environment which associates the top element to all variables) of the Honsell-Lenisa model are exactly the lambda-terms which applied to an arbitrary number of strongly normalising lambda-terms produce always strongly normalising lambda-terms. This proof uses a finitary logical description of the model by means of intersection types. Therefore we solve an open question stated by Dezani, Honsell and Motohama.}, publisher = {IEEE Computer Society}, pages = {327-336}, year = {2006}, }

tatsdeza06 (In proceedings)
Author(s)	Makoto Tatsuta and Mariangiola Dezani-Ciancaglini
Title	« Normalisation is Insensible to Lambda-term Identity or Difference »
In	LICS'06
Editor(s)	Rajeev Alur
Page(s)	327-336
Year	2006
Publisher	IEEE Computer Society
PDF	http://www.di.unito.it/˜dezani/papers/td.pdf