[TYPES] questiuon about strong normalization in untyped lambda-calculus

[Mariangiola Dezani]

> For all terms T,
>  [T is in A]
> iff
>  [the term T T_1 ... T_n is strongly normalizing
>   for all natural numbers n and terms T_1,...,T_n in A]

a strict subset of A is the set PSN of persistently strongly  
normalizing terms defined by

[T is in PSN]
iff
  [the term T T_1 ... T_n is strongly normalizing
   for all natural numbers n and strongly normalizing terms T_1,...,T_n]

The set PSN has been characterised (also with types) in:

M. Tatsuta and M. Dezani-Ciancaglini.  Normalisation is Insensible to  
Lambda-term Identity or Difference,   LICS'06.  In Rajeev Alur  
ed(s).,  pages 327-336,  2006,  IEEE Computer Society. http://www.di.unito.it/ 
˜dezani/papers/td.pdf

Characterisations of other sets of lambda terms related to  
normalization properties can be found in:

M. Dezani-Ciancaglini, F. Honsell and Y. Motohama.  Compositional  
Characterization of λ-terms using Intersection Types,   Theoretical  
Computer Science,  340(3):459-495,  2005. http://www.di.unito.it/~dezani/papers/tcsf.pdf

Best Regards Mariangiola Dezani

@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@

Mariangiola Dezani-Ciancaglini
Dipartimento di Informatica
Universita' di Torino
c.Svizzera 185, 10149 Torino (Italy)

e-mail :  dezani at di.unito.it
phone: 39-011-6706850
fax : 39-011-751603
mobile: 39-320-4359903 (preferred) 39-348-2251592

http://www.di.unito.it/~dezani

**********************************************************************
Unless unavoidable, no Word, Excel or PowerPoint attachments, please.
See http://www.gnu.org/philosophy/no-word-attachments.html
**********************************************************************

"L'ITALIA RIPUDIA LA GUERRA come strumento di offesa alla libertà  
degli altri
popoli e come mezzo di risoluzione delle controversie internazionali."
(Art. 11 della Costituzione della Repubblica Italiana)