tatsdeza06 (In proceedings)

Author(s)  Makoto Tatsuta and Mariangiola DezaniCiancaglini 
Title  « Normalisation is Insensible to Lambdaterm Identity or Difference » 
In  LICS'06 
Editor(s)  Rajeev Alur 
Page(s)  327336 
Year  2006 
Publisher  IEEE Computer Society 
PDF  http://www.di.unito.it/˜dezani/papers/td.pdf 
Abstract 
This paper analyses the computational behaviour of lambdaterm 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 lambdaterm M to a fixed number n of copies of the same arbitrary strongly normalising lambdaterm is strongly normalising if and only if the application of M to different arbitrary strongly normalising lambdaterms 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 lambdaterms in normal form. For strong normalisation we consider Klop's extended lambdacalculus (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 lambdaterms whose interpretation is the top element (in the environment which associates the top element to all variables) of the HonsellLenisa model are exactly the lambdaterms which applied to an arbitrary number of strongly normalising lambdaterms produce always strongly normalising lambdaterms. 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 DezaniCiancaglini, Mariangiola},
booktitle = {{LICS'06}},
editor = {Rajeev Alur},
title = {{Normalisation is Insensible to Lambdaterm Identity or Difference}},
abstract = {This paper analyses the computational behaviour of lambdaterm
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 lambdaterm M to a fixed number n of
copies of the same arbitrary strongly normalising lambdaterm is
strongly normalising if and only if the application of M to
different arbitrary strongly normalising lambdaterms 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 lambdaterms in normal form. For strong
normalisation we consider Klop's extended lambdacalculus (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 lambdaterms whose interpretation
is the top element (in the environment which associates the top
element to all variables) of the HonsellLenisa model are exactly
the lambdaterms which applied to an arbitrary number of strongly
normalising lambdaterms produce always strongly normalising
lambdaterms. 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 = {327336},
year = {2006},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)