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.
|Autori:||BERARDUCCI A; INTRIGILA B|
|Titolo:||Some new results on easy lambda-terms|
|Anno del prodotto:||1993|
|Digital Object Identifier (DOI):||10.1016/0304-3975(93)90084-7|
|Appare nelle tipologie:||1.1 Articolo in rivista|