We treat a general technique to obtain Church - Rosser extensions of the lambda-beta-calculus, based on the notion of ``confining class'' and on an infinitary version of lambda-calculus. We apply the technique to find a large class of terms which can be consistently equated to every other term, and we also show that many equations between lambda-terms can be consistently added to the the lambda-beta-calculus.

Church-Rosser lambda-theories, infinite lambda-terms and consistency problems

BERARDUCCI, ALESSANDRO;
1996

Abstract

We treat a general technique to obtain Church - Rosser extensions of the lambda-beta-calculus, based on the notion of ``confining class'' and on an infinitary version of lambda-calculus. We apply the technique to find a large class of terms which can be consistently equated to every other term, and we also show that many equations between lambda-terms can be consistently added to the the lambda-beta-calculus.
Berarducci, Alessandro; Intrigila, B.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11568/46466
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact