Issue |
RAIRO-Theor. Inf. Appl.
Volume 46, Number 2, April-June 2012
12th Italian Conference on Theoretical Computer Science (ICTCS)
|
|
---|---|---|
Page(s) | 291 - 314 | |
DOI | https://doi.org/10.1051/ita/2012005 | |
Published online | 23 February 2012 |
Easy lambda-terms are not always simple
1
DAIS, Università Ca’ Foscari Venezia, via Torino 155, 30172
Mestre,
Italy
acarraro@dsi.unive.it, salibra@dsi.unive.it
2
PPS, Université Paris Diderot, 175 rue de Chevaleret, 75013
Paris,
France
Received:
21
December
2010
Accepted:
18
January
2012
A closed λ-term M is easy if, for any other closed term N, the lambda theory generated by M = N is consistent. Recently, it has been introduced a general technique to prove the easiness of λ-terms through the semantical notion of simple easiness. Simple easiness implies easiness and allows to prove consistency results via construction of suitable filter models of λ-calculus living in the category of complete partial orderings: given a simple easy term M and an arbitrary closed term N, it is possible to build (in a canonical way) a non-trivial filter model which equates the interpretation of M and N. The question whether easiness implies simple easiness constitutes Problem 19 in the TLCA list of open problems. In this paper we negatively answer the question providing a non-empty co-r.e. (complement of a recursively enumerable) set of easy, but not simple easy, λ-terms.
Mathematics Subject Classification: 03B40
Key words: Lambda calculus / easy lambda-terms / simple easy lambda-terms / filter models / ris models
© EDP Sciences 2012
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.