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.
@article{ITA_2012__46_2_291_0,
author = {Carraro, Alberto and Salibra, Antonino},
title = {Easy lambda-terms are not always simple},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
volume = {46},
year = {2012},
pages = {291-314},
doi = {10.1051/ita/2012005},
mrnumber = {2931250},
zbl = {1253.03035},
language = {en},
url = {http://dml.mathdoc.fr/item/ITA_2012__46_2_291_0}
}
Carraro, Alberto; Salibra, Antonino. Easy lambda-terms are not always simple. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 46 (2012) pp. 291-314. doi : 10.1051/ita/2012005. http://gdmltest.u-ga.fr/item/ITA_2012__46_2_291_0/
[1] and , TLCA list of open problems : Problem 19, http://tlca.di.unito.it/opltlca/problem19.pdf (2002).
[2] and , Simple easy terms, ITRS '02, Intersection Types and Related Systems (FLoC Satellite Event). Electron. Notes Theoret. Comput. Sci. 70 (2003) 1-18. | Zbl 1270.03028
[3] , and , Filter models and easy terms, in ICTCS '01 : Proc. of the 7th Italian Conference on Theoretical Computer Science. Springer-Verlag, London, UK (2001) 17-37. | MR 1915405 | Zbl 1042.03014
[4] , and , Intersection types and domain operators. Theoret. Comput. Sci. 316 (2004) 25-47. | MR 2074923 | Zbl 1055.03011
[5] and , Omega can be anything it should not be. Proc. of Indagationes Mathematicae 82 (1979) 111-120. | MR 535560 | Zbl 0417.03006
[6] , Some extensional term models for combinatory logics and λ-calculi. Ph.D. thesis, University of Utrecht (1971).
[7] , The Lambda calculus : Its syntax and semantics. North-Holland, Amsterdam (1984). | MR 774952 | Zbl 0551.03007
[8] , and , A filter lambda model and the completeness of type assignment. J. Symbolic Logic 48 (1983) 931-940. | MR 727784 | Zbl 0545.03004
[9] , and , Structures for lazy semantics, in Programming Concepts and Methods (PROCOMET'98), edited by D. Gries and W.P. de Roever. Chaptman & Hall (1998) 30-48.
[10] , Infinite lambda-calculus and non-sensible models, in Logic and Algebra (Pontignano, 1994). Lect. Notes Pure Appl. Math. Ser. 180 (1996) 339-378. | MR 1404948 | Zbl 0857.03005
[11] and , Some new results on easy lambda-terms. Theoret. Comput. Sci. 121 (1993) 71-88. | MR 1249540 | Zbl 0796.03022
[12] , From computation to foundations via functions and application : the λ-calculus and its webbed models. Theoret. Comput. Sci. 249 (2000) 81-161. | MR 1791954 | Zbl 0949.68049
[13] , Graph models of λ-calculus at work, and variations. Math. Struct. Comput. Sci. 16 (2006) 185-221. | MR 2228853 | Zbl 1097.03011
[14] and , Easiness in graph models. Theoret. Comput. Sci. 354 (2006) 4-23. | MR 2207939 | Zbl 1088.68034
[15] , and , Effective λ-models versus recursively enumerable λ-theories. Math. Struct. Comput. Sci. 19 (2009) 897-942. | MR 2545507 | Zbl 1186.03023
[16] , Stable models of typed lambda-calculi, in Proc. of ICALP'78. Lect. Notes Comput. Sci. 62 (1978).
[17] , Alcune proprietá delle forme β-η-normali nel λ-K-calcolo. Technical Report 696, CNR (1968).
[18] and , Sequentiality and strong stability, in Proc. of LICS'91. IEEE Computer Society Press (1991) 138-145.
[19] and , Reflexive Scott domains are not complete for the extensional lambda calculus, in Proc. of the Twenty-Fourth Annual IEEE Symposium on Logic in Computer Science (LICS 2009). IEEE Computer Society Press (2009) 91-100. | MR 2932373
[20] and , An extension of the basic functionality theory for the λ-calculus. Notre-Dame J. Form. Log. 21 (1980) 685-693. | MR 592528 | Zbl 0423.03010
[21] , , and , Extended type structures and filter lambda models, in Logic Colloquium 82, edited by G. Lolli, G. Longo and A. Marcja. Amsterdam, The Netherlands, North-Holland (1984) 241-262. | MR 762113 | Zbl 0558.03007
[22] , , and , Extended type structures and filter lambda models, in Logic Colloquium 82, edited by G. Lolli, G. Longo and A. Marcja. Amsterdam, The Netherlands, North-Holland (1984) 241-262. | MR 762113 | Zbl 0558.03007
[23] , Algebras and combinators. Algebra Univers. 13 (1981) 389-392. | MR 631731 | Zbl 0482.08005
[24] and , Reasoning about interpretations in qualitative lambda models, in Proc. of the IFIP Working Group 2.2/2.3, edited by M. Broy and C.B. Jones. North-Holland (1990) 505-521.
[25] and , An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus. J. Comput. System Sci. 45 (1992) 49-75. | MR 1170917 | Zbl 0763.03012
[26] , A problem on easy terms in lambda-calculus. Fundamenta Informaticae 15 (1991) 99-106. | MR 1153289 | Zbl 0751.03006
[27] , A condition for identifying two elements of whatever model of combinatory logic, in Proceedings of the Symposium on Lambda-Calculus and Computer Science Theory. Springer-Verlag, London, UK (1975) 213-219. | MR 462922 | Zbl 0357.02023
[28] and , Equating for recurrent terms of λ-calculus and combinatory logic. Technical Report 85, CNR (1978). | Zbl 0432.03010
[29] and , Easy terms in the lambda-calculus. Fundam. Inform. 8 (1985) 225-233. | MR 798546 | Zbl 0574.03005
[30] , Isomorphism et équivalence équationnelle entre modèles du λ-calcul. Master's thesis, Université de Paris 7 (1995).
[31] , Isomorphism and equational equivalence of continuous lambda models. Stud. Log. 61 (1998) 403-415. | MR 1657121 | Zbl 0964.03015
[32] , On the construction of stable models of λ-calculus. Theoret. Comput. Sci. 269 (2001) 23-46. | MR 1862408 | Zbl 0992.68022
[33] , Models of the lambda calculus. Inform. Control 52 (1982) 306-332. | MR 707579 | Zbl 0542.03004
[34] , On the Jacopini technique. Inform. Comput. 138 (1997) 101-123. | MR 1479318 | Zbl 0887.68010
[35] , Set-theoretical models of λ-calculus : theories, expansions, isomorphisms. Ann. Pure Appl. Logic 24 (1983) 153-188. | MR 713298 | Zbl 0513.03009
[36] , What is a model of the lambda calculus? Inform. Control 52 (1982) 87-122. | MR 693998 | Zbl 0507.03002
[37] , Set-theoretical and other elementary models of the λ-calculus. Theoret. Comput. Sci. 121 (1993) 351-409. | MR 1249549 | Zbl 0790.03014
[38] , Topological incompleteness and order incompleteness of the lambda calculus. ACM Trans. Comput. Log. 4 (2003) 379-401. | MR 1995005
[39] , Continuous lattices, in Toposes, algebraic geometry and logic. Springer-Verlag (1972). | MR 404073 | Zbl 0239.54006
[40] , Data types as lattices, in ISILC Logic Conference, edited by G. Müller, A. Oberschelp and K. Potthoff. Lect. Notes Math. 499 (1975) 579-651. | MR 405908 | Zbl 0322.02024
[41] , Lambda calculus : some models, some philosophy, in The Kleene Symposium. Amsterdam, The Netherlands, North-Holland (1980). | MR 591884 | Zbl 0515.03004
[42] , Domains for denotational semantics, in Proc. of ICALP '82. ACM Press. New York, NY, USA (1982) 95-104. | MR 675486 | Zbl 0495.68025
[43] , Numerations, λ-calculus, and arithmetic, in To H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism, edited by J.R. Hindley and J.P. Seldin (1980) 259-284. | MR 592807
[44] , Syntaxe et sémantique de la facilité en λ-calcul. Thèse de Doctorat D'État, Université Paris 7 (1991).