Given two closed lambda-terms A and B we consider the question whether the equation A = B is consistent with the lambda-beta-calculus. In general the problem is undecidable. However if A is a 0-term we can give good sufficient conditions for the consistency. This allows us to prove some counterintuitive results such as: (1) there is a closed lambda-term X which can be consistently equated to every closed lambda-term with the exception of the identity lambda x.x. (2) there is a closed lambda-term which can be consistenlty equated to every closed normal form, but not to the Curry fixed point operator Y.
Some new results on easy lambda-terms
BERARDUCCI, ALESSANDRO;
1993-01-01
Abstract
Given two closed lambda-terms A and B we consider the question whether the equation A = B is consistent with the lambda-beta-calculus. In general the problem is undecidable. However if A is a 0-term we can give good sufficient conditions for the consistency. This allows us to prove some counterintuitive results such as: (1) there is a closed lambda-term X which can be consistently equated to every closed lambda-term with the exception of the identity lambda x.x. (2) there is a closed lambda-term which can be consistenlty equated to every closed normal form, but not to the Curry fixed point operator Y.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.
