Easy lambda-terms are not always simple

Alberto Carraro; Antonino Salibra

RAIRO - Theoretical Informatics and Applications (2012)

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

Abstract

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

How to cite

top

Carraro, Alberto, and Salibra, Antonino. "Easy lambda-terms are not always simple." RAIRO - Theoretical Informatics and Applications 46.2 (2012): 291-314. <http://eudml.org/doc/222014>.

@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},
keywords = {Lambda calculus; easy lambda-terms; simple easy lambda-terms; filter models; ris models; lambda calculus; easy lambda terms; simple easy lambda terms},
language = {eng},
month = {4},
number = {2},
pages = {291-314},
publisher = {EDP Sciences},
title = {Easy lambda-terms are not always simple},
url = {http://eudml.org/doc/222014},
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
DA - 2012/4//
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; lambda calculus; easy lambda terms; simple easy lambda terms
UR - http://eudml.org/doc/222014
ER -

References

top
  1. F. Alessi and M. Dezani-Ciancaglini, TLCA list of open problems : Problem 19, (2002).  URIhttp://tlca.di.unito.it/opltlca/problem19.pdf
  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.03014
  4. F. Alessi, M. Dezani-Ciancaglini and S. Lusin, Intersection types and domain operators. Theoret. Comput. Sci.316 (2004) 25–47.  Zbl1055.03011
  5. J.C.M. Baeten and B. Boerboom, Omega can be anything it should not be. Proc. of Indagationes Mathematicae82 (1979) 111–120.  Zbl0417.03006
  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.03007
  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.03004
  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.03005
  11. A. Berarducci and B. Intrigila, Some new results on easy lambda-terms. Theoret. Comput. Sci.121 (1993) 71–88.  Zbl0796.03022
  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.68049
  13. C. Berline, Graph models of λ-calculus at work, and variations. Math. Struct. Comput. Sci.16 (2006) 185–221.  Zbl1097.03011
  14. C. Berline and A. Salibra, Easiness in graph models. Theoret. Comput. Sci.354 (2006) 4–23.  Zbl1088.68034
  15. C. Berline, G. Manzonetto and A. Salibra, Effective λ-models versus recursively enumerable λ-theories. Math. Struct. Comput. Sci.19 (2009) 897–942.  Zbl1186.03023
  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.  
  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.03010
  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.03007
  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.03007
  23. E. Engeler, Algebras and combinators. Algebra Univers.13 (1981) 389–392.  Zbl0482.08005
  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.03012
  26. B. Intrigila, A problem on easy terms in lambda-calculus. Fundamenta Informaticae15 (1991) 99–106.  Zbl0751.03006
  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.02023
  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.03005
  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.03015
  32. R. Kerth, On the construction of stable models of λ-calculus. Theoret. Comput. Sci.269 (2001) 23–46.  Zbl0992.68022
  33. C.P.J. Koymans, Models of the lambda calculus. Inform. Control52 (1982) 306–332.  Zbl0542.03004
  34. J. Kuper, On the Jacopini technique. Inform. Comput.138 (1997) 101–123.  Zbl0887.68010
  35. G. Longo, Set-theoretical models of λ-calculus : theories, expansions, isomorphisms. Ann. Pure Appl. Logic24 (1983) 153–188.  Zbl0513.03009
  36. A.R. Meyer, What is a model of the lambda calculus?Inform. Control52 (1982) 87–122.  Zbl0507.03002
  37. G.D. Plotkin, Set-theoretical and other elementary models of the λ-calculus. Theoret. Comput. Sci.121 (1993) 351–409.  Zbl0790.03014
  38. A. Salibra, Topological incompleteness and order incompleteness of the lambda calculus. ACM Trans. Comput. Log.4 (2003) 379–401.  
  39. D.S. Scott, Continuous lattices, in Toposes, algebraic geometry and logic. Springer-Verlag (1972).  
  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.  
  41. D.S. Scott, Lambda calculus : some models, some philosophy, in The Kleene Symposium. Amsterdam, The Netherlands, North-Holland (1980).  
  42. D.S. Scott, Domains for denotational semantics, in Proc. of ICALP ’82. ACM Press. New York, NY, USA (1982) 95–104.  Zbl0495.68025
  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.  
  44. C. Zylberajch, Syntaxe et sémantique de la facilité enλ-calcul. Thèse de Doctorat D’État, Université Paris 7 (1991).  

NotesEmbed ?

top

You must be logged in to post comments.

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

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.