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.  
  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.  
  4. F. Alessi, M. Dezani-Ciancaglini and S. Lusin, Intersection types and domain operators. Theoret. Comput. Sci.316 (2004) 25–47.  
  5. J.C.M. Baeten and B. Boerboom, Omega can be anything it should not be. Proc. of Indagationes Mathematicae82 (1979) 111–120.  
  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).  
  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.  
  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.  
  11. A. Berarducci and B. Intrigila, Some new results on easy lambda-terms. Theoret. Comput. Sci.121 (1993) 71–88.  
  12. C. Berline, From computation to foundations via functions and application : the λ-calculus and its webbed models. Theoret. Comput. Sci.249 (2000) 81–161.  
  13. C. Berline, Graph models of λ-calculus at work, and variations. Math. Struct. Comput. Sci.16 (2006) 185–221.  
  14. C. Berline and A. Salibra, Easiness in graph models. Theoret. Comput. Sci.354 (2006) 4–23.  
  15. C. Berline, G. Manzonetto and A. Salibra, Effective λ-models versus recursively enumerable λ-theories. Math. Struct. Comput. Sci.19 (2009) 897–942.  
  16. G. Berry, Stable models of typed lambda-calculi, in Proc. of ICALP’78. Lect. Notes Comput. Sci.62 (1978).  
  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.  
  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.  
  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.  
  23. E. Engeler, Algebras and combinators. Algebra Univers.13 (1981) 389–392.  
  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.  
  26. B. Intrigila, A problem on easy terms in lambda-calculus. Fundamenta Informaticae15 (1991) 99–106.  
  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.  
  28. G. Jacopini and M. Venturini-Zilli, Equating for recurrent terms ofλ-calculus and combinatory logic. Technical Report 85, CNR (1978).  
  29. G. Jacopini and M. Venturini-Zilli, Easy terms in the lambda-calculus. Fundam. Inform.8 (1985) 225–233.  
  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.  
  32. R. Kerth, On the construction of stable models of λ-calculus. Theoret. Comput. Sci.269 (2001) 23–46.  
  33. C.P.J. Koymans, Models of the lambda calculus. Inform. Control52 (1982) 306–332.  
  34. J. Kuper, On the Jacopini technique. Inform. Comput.138 (1997) 101–123.  
  35. G. Longo, Set-theoretical models of λ-calculus : theories, expansions, isomorphisms. Ann. Pure Appl. Logic24 (1983) 153–188.  
  36. A.R. Meyer, What is a model of the lambda calculus?Inform. Control52 (1982) 87–122.  
  37. G.D. Plotkin, Set-theoretical and other elementary models of the λ-calculus. Theoret. Comput. Sci.121 (1993) 351–409.  
  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.  
  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.