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-01-01
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.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.
