# Easy lambda-terms are not always simple

Alberto Carraro; Antonino Salibra

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2012)

- Volume: 46, Issue: 2, page 291-314
- ISSN: 0988-3754

## Access Full Article

top## Abstract

top## How to cite

topCarraro, Alberto, and Salibra, Antonino. "Easy lambda-terms are not always simple." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 46.2 (2012): 291-314. <http://eudml.org/doc/273020>.

@article{Carraro2012,

abstract = {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.},

author = {Carraro, Alberto, Salibra, Antonino},

journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},

keywords = {lambda calculus; easy lambda-terms; simple easy lambda-terms; filter models; ris models; easy lambda terms; simple easy lambda terms},

language = {eng},

number = {2},

pages = {291-314},

publisher = {EDP-Sciences},

title = {Easy lambda-terms are not always simple},

url = {http://eudml.org/doc/273020},

volume = {46},

year = {2012},

}

TY - JOUR

AU - Carraro, Alberto

AU - Salibra, Antonino

TI - Easy lambda-terms are not always simple

JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

PY - 2012

PB - EDP-Sciences

VL - 46

IS - 2

SP - 291

EP - 314

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

LA - eng

KW - lambda calculus; easy lambda-terms; simple easy lambda-terms; filter models; ris models; easy lambda terms; simple easy lambda terms

UR - http://eudml.org/doc/273020

ER -

## References

top- [1] F. Alessi and M. Dezani-Ciancaglini, TLCA list of open problems : Problem 19, http://tlca.di.unito.it/opltlca/problem19.pdf (2002).
- [2] F. Alessi and S. Lusin, Simple easy terms, ITRS ’02, Intersection Types and Related Systems (FLoC Satellite Event). Electron. Notes Theoret. Comput. Sci. 70 (2003) 1–18. Zbl1270.03028
- [3] F. Alessi, M. Dezani-Ciancaglini and F. Honsell, 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. Zbl1042.03014MR1915405
- [4] F. Alessi, M. Dezani-Ciancaglini and S. Lusin, Intersection types and domain operators. Theoret. Comput. Sci.316 (2004) 25–47. Zbl1055.03011MR2074923
- [5] J.C.M. Baeten and B. Boerboom, Omega can be anything it should not be. Proc. of Indagationes Mathematicae82 (1979) 111–120. Zbl0417.03006MR535560
- [6] H.P. Barendregt, Some extensional term models for combinatory logics and λ-calculi. Ph.D. thesis, University of Utrecht (1971).
- [7] H.P. Barendregt, The Lambda calculus : Its syntax and semantics. North-Holland, Amsterdam (1984). Zbl0551.03007MR774952
- [8] H.P. Barendregt, M. Coppo and M. Dezani-Ciancaglini, A filter lambda model and the completeness of type assignment. J. Symbolic Logic48 (1983) 931–940. Zbl0545.03004MR727784
- [9] O. Bastonero, A. Pravato and S. Ronchi Della Rocca, 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] A. Berarducci, Infinite lambda-calculus and non-sensible models, in Logic and Algebra (Pontignano, 1994). Lect. Notes Pure Appl. Math. Ser. 180 (1996) 339–378. Zbl0857.03005MR1404948
- [11] A. Berarducci and B. Intrigila, Some new results on easy lambda-terms. Theoret. Comput. Sci.121 (1993) 71–88. Zbl0796.03022MR1249540
- [12] C. Berline, From computation to foundations via functions and application : the λ-calculus and its webbed models. Theoret. Comput. Sci.249 (2000) 81–161. Zbl0949.68049MR1791954
- [13] C. Berline, Graph models of λ-calculus at work, and variations. Math. Struct. Comput. Sci.16 (2006) 185–221. Zbl1097.03011MR2228853
- [14] C. Berline and A. Salibra, Easiness in graph models. Theoret. Comput. Sci.354 (2006) 4–23. Zbl1088.68034MR2207939
- [15] C. Berline, G. Manzonetto and A. Salibra, Effective λ-models versus recursively enumerable λ-theories. Math. Struct. Comput. Sci.19 (2009) 897–942. Zbl1186.03023MR2545507
- [16] G. Berry, Stable models of typed lambda-calculi, in Proc. of ICALP’78. Lect. Notes Comput. Sci. 62 (1978). Zbl0382.68041
- [17] C. Böhm, Alcune proprietá delle forme β-η-normali nel λ-K-calcolo. Technical Report 696, CNR (1968).
- [18] A. Bucciarelli and T. Ehrhard, Sequentiality and strong stability, in Proc. of LICS’91. IEEE Computer Society Press (1991) 138–145.
- [19] A. Carraro and A. Salibra, 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. MR2932373
- [20] M. Coppo and M. Dezani-Ciancaglini, An extension of the basic functionality theory for the λ-calculus. Notre-Dame J. Form. Log.21 (1980) 685–693. Zbl0423.03010MR592528
- [21] M. Coppo, M. Dezani-Ciancaglini, F. Honsell and G. Longo, 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. Zbl0558.03007MR762113
- [22] M. Coppo, M. Dezani-Ciancaglini, F. Honsell and G. Longo, 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. Zbl0558.03007MR762113
- [23] E. Engeler, Algebras and combinators. Algebra Univers.13 (1981) 389–392. Zbl0482.08005MR631731
- [24] F. Honsell and S. Ronchi Della Rocca, 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] F. Honsell and S. Ronchi Della Rocca, An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus. J. Comput. System Sci.45 (1992) 49–75. Zbl0763.03012MR1170917
- [26] B. Intrigila, A problem on easy terms in lambda-calculus. Fundamenta Informaticae15 (1991) 99–106. Zbl0751.03006MR1153289
- [27] G. Jacopini, 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. Zbl0357.02023MR462922
- [28] G. Jacopini and M. Venturini-Zilli, Equating for recurrent terms of λ-calculus and combinatory logic. Technical Report 85, CNR (1978). Zbl0432.03010
- [29] G. Jacopini and M. Venturini-Zilli, Easy terms in the lambda-calculus. Fundam. Inform.8 (1985) 225–233. Zbl0574.03005MR798546
- [30] R. Kerth, Isomorphism et équivalence équationnelle entre modèles du λ-calcul. Master’s thesis, Université de Paris 7 (1995).
- [31] R. Kerth, Isomorphism and equational equivalence of continuous lambda models. Stud. Log.61 (1998) 403–415. Zbl0964.03015MR1657121
- [32] R. Kerth, On the construction of stable models of λ-calculus. Theoret. Comput. Sci.269 (2001) 23–46. Zbl0992.68022MR1862408
- [33] C.P.J. Koymans, Models of the lambda calculus. Inform. Control52 (1982) 306–332. Zbl0542.03004MR707579
- [34] J. Kuper, On the Jacopini technique. Inform. Comput.138 (1997) 101–123. Zbl0887.68010MR1479318
- [35] G. Longo, Set-theoretical models of λ-calculus : theories, expansions, isomorphisms. Ann. Pure Appl. Logic24 (1983) 153–188. Zbl0513.03009MR713298
- [36] A.R. Meyer, What is a model of the lambda calculus? Inform. Control52 (1982) 87–122. Zbl0507.03002MR693998
- [37] G.D. Plotkin, Set-theoretical and other elementary models of the λ-calculus. Theoret. Comput. Sci.121 (1993) 351–409. Zbl0790.03014MR1249549
- [38] A. Salibra, Topological incompleteness and order incompleteness of the lambda calculus. ACM Trans. Comput. Log.4 (2003) 379–401. MR1995005
- [39] D.S. Scott, Continuous lattices, in Toposes, algebraic geometry and logic. Springer-Verlag (1972). Zbl0239.54006MR404073
- [40] D.S. Scott, 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. Zbl0322.02024MR405908
- [41] D.S. Scott, Lambda calculus : some models, some philosophy, in The Kleene Symposium. Amsterdam, The Netherlands, North-Holland (1980). Zbl0515.03004MR591884
- [42] D.S. Scott, Domains for denotational semantics, in Proc. of ICALP ’82. ACM Press. New York, NY, USA (1982) 95–104. Zbl0495.68025MR675486
- [43] A. Visser, 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. MR592807
- [44] C. Zylberajch, Syntaxe et sémantique de la facilité en λ-calcul. Thèse de Doctorat D’État, Université Paris 7 (1991).

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.