Hostname: page-component-7b7567c8c-jswmv Total loading time: 0 Render date: 2026-11-15T21:08:24.616Z Has data issue: false hasContentIssue false
  • English
  • Français

Easy lambda-terms are not always simple

Published online by Cambridge University Press:  23 February 2012

Alberto Carraro and
Antonino Salibra
Alberto Carraro
Affiliation:
DAIS, Università Ca’ Foscari Venezia, via Torino 155, 30172 Mestre, Italy. acarraro@dsi.unive.it, salibra@dsi.unive.itPPS, Université Paris Diderot, 175 rue de Chevaleret, 75013 Paris, France
Antonino Salibra
Affiliation:
DAIS, Università Ca’ Foscari Venezia, via Torino 155, 30172 Mestre, Italy. acarraro@dsi.unive.it, salibra@dsi.unive.it

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

A closed λ-term M is easy if, for anyother closed term N, the lambda theory generated byM = N is consistent. Recently, it has been introduceda general technique to prove the easiness of λ-terms through thesemantical notion of simple easiness. Simple easiness implies easiness and allows to proveconsistency results via construction of suitable filter models ofλ-calculus living in the category of complete partial orderings: givena simple easy term M and an arbitrary closed term N, itis possible to build (in a canonical way) a non-trivial filter model which equates theinterpretation of M and N. The question whether easinessimplies simple easiness constitutes Problem 19 in the TLCA list of open problems. In thispaper we negatively answer the question providing a non-empty co-r.e. (complement of arecursively enumerable) set of easy, but not simple easy, λ-terms.

Keywords

Lambda calculuseasy lambda-termssimple easy lambda-termsfilter modelsris models

References

F. Alessi and M. Dezani-Ciancaglini, TLCA list of open problems : Problem 19, http://tlca.di.unito.it/opltlca/problem19.pdf (2002).
Alessi, F. and Lusin, S., Simple easy terms, ITRS ’02, Intersection Types and Related Systems (FLoC Satellite Event). Electron. Notes Theoret. Comput. Sci. 70 (2003) 1–18. Google Scholar
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.
Alessi, F., Dezani-Ciancaglini, M. and Lusin, S., Intersection types and domain operators. Theoret. Comput. Sci. 316 (2004) 25–47. Google Scholar
Baeten, J.C.M. and Boerboom, B., Omega can be anything it should not be. Proc. of Indagationes Mathematicae 82 (1979) 111–120. Google Scholar
H.P. Barendregt, Some extensional term models for combinatory logics and λ -calculi. Ph.D. thesis, University of Utrecht (1971).
H.P. Barendregt, The Lambda calculus : Its syntax and semantics. North-Holland, Amsterdam (1984).
Barendregt, H.P., Coppo, M. and Dezani-Ciancaglini, M., A filter lambda model and the completeness of type assignment. J. Symbolic Logic 48 (1983) 931–940. Google Scholar
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.
Berarducci, A., Infinite lambda-calculus and non-sensible models, in Logic and Algebra (Pontignano, 1994). Lect. Notes Pure Appl. Math. Ser. 180 (1996) 339–378. Google Scholar
Berarducci, A. and Intrigila, B., Some new results on easy lambda-terms. Theoret. Comput. Sci. 121 (1993) 71–88. Google Scholar
Berline, C., From computation to foundations via functions and application : the λ-calculus and its webbed models. Theoret. Comput. Sci. 249 (2000) 81–161. Google Scholar
Berline, C., Graph models of λ-calculus at work, and variations. Math. Struct. Comput. Sci. 16 (2006) 185–221. Google Scholar
Berline, C. and Salibra, A., Easiness in graph models. Theoret. Comput. Sci. 354 (2006) 4–23. Google Scholar
Berline, C., Manzonetto, G. and Salibra, A., Effective λ-models versus recursively enumerable λ-theories. Math. Struct. Comput. Sci. 19 (2009) 897–942. Google Scholar
G. Berry, Stable models of typed lambda-calculi, in Proc. of ICALP’78. Lect. Notes Comput. Sci. 62 (1978).
C. Böhm, Alcune proprietá delle forme β - η -normali nel λ -K-calcolo. Technical Report 696, CNR (1968).
A. Bucciarelli and T. Ehrhard, Sequentiality and strong stability, in Proc. of LICS’91. IEEE Computer Society Press (1991) 138–145.
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.
Coppo, M. and Dezani-Ciancaglini, M., An extension of the basic functionality theory for the λ-calculus. Notre-Dame J. Form. Log. 21 (1980) 685–693. Google Scholar
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.
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.
Engeler, E., Algebras and combinators. Algebra Univers. 13 (1981) 389–392. Google Scholar
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.
Honsell, F. and Ronchi Della Rocca, S., An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus. J. Comput. System Sci. 45 (1992) 49–75. Google Scholar
Intrigila, B., A problem on easy terms in lambda-calculus. Fundamenta Informaticae 15 (1991) 99–106. Google Scholar
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.
G. Jacopini and M. Venturini-Zilli, Equating for recurrent terms of λ -calculus and combinatory logic. Technical Report 85, CNR (1978).
Jacopini, G. and Venturini-Zilli, M., Easy terms in the lambda-calculus. Fundam. Inform. 8 (1985) 225–233. Google Scholar
R. Kerth, Isomorphism et équivalence équationnelle entre modèles du λ -calcul. Master’s thesis, Université de Paris 7 (1995).
Kerth, R., Isomorphism and equational equivalence of continuous lambda models. Stud. Log. 61 (1998) 403–415. Google Scholar
Kerth, R., On the construction of stable models of λ-calculus. Theoret. Comput. Sci. 269 (2001) 23–46. Google Scholar
Koymans, C.P.J., Models of the lambda calculus. Inform. Control 52 (1982) 306–332. Google Scholar
Kuper, J., On the Jacopini technique. Inform. Comput. 138 (1997) 101–123. Google Scholar
Longo, G., Set-theoretical models of λ-calculus : theories, expansions, isomorphisms. Ann. Pure Appl. Logic 24 (1983) 153–188. Google Scholar
Meyer, A.R., What is a model of the lambda calculus? Inform. Control 52 (1982) 87–122. Google Scholar
Plotkin, G.D., Set-theoretical and other elementary models of the λ-calculus. Theoret. Comput. Sci. 121 (1993) 351–409. Google Scholar
Salibra, A., Topological incompleteness and order incompleteness of the lambda calculus. ACM Trans. Comput. Log. 4 (2003) 379–401. Google Scholar
D.S. Scott, Continuous lattices, in Toposes, algebraic geometry and logic. Springer-Verlag (1972).
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.
D.S. Scott, Lambda calculus : some models, some philosophy, in The Kleene Symposium. Amsterdam, The Netherlands, North-Holland (1980).
D.S. Scott, Domains for denotational semantics, in Proc. of ICALP ’82. ACM Press. New York, NY, USA (1982) 95–104.
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.
C. Zylberajch, Syntaxe et sémantique de la facilité en λ -calcul. Thèse de Doctorat D’État, Université Paris 7 (1991).