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

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 - 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. [1] F. Alessi and M. Dezani-Ciancaglini, TLCA list of open problems : Problem 19, http://tlca.di.unito.it/opltlca/problem19.pdf (2002). 
  2. [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. [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. [4] F. Alessi, M. Dezani-Ciancaglini and S. Lusin, Intersection types and domain operators. Theoret. Comput. Sci.316 (2004) 25–47. Zbl1055.03011MR2074923
  5. [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. [6] H.P. Barendregt, Some extensional term models for combinatory logics and λ-calculi. Ph.D. thesis, University of Utrecht (1971). 
  7. [7] H.P. Barendregt, The Lambda calculus : Its syntax and semantics. North-Holland, Amsterdam (1984). Zbl0551.03007MR774952
  8. [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. [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. [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. [11] A. Berarducci and B. Intrigila, Some new results on easy lambda-terms. Theoret. Comput. Sci.121 (1993) 71–88. Zbl0796.03022MR1249540
  12. [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. [13] C. Berline, Graph models of λ-calculus at work, and variations. Math. Struct. Comput. Sci.16 (2006) 185–221. Zbl1097.03011MR2228853
  14. [14] C. Berline and A. Salibra, Easiness in graph models. Theoret. Comput. Sci.354 (2006) 4–23. Zbl1088.68034MR2207939
  15. [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. [16] G. Berry, Stable models of typed lambda-calculi, in Proc. of ICALP’78. Lect. Notes Comput. Sci. 62 (1978). Zbl0382.68041
  17. [17] C. Böhm, Alcune proprietá delle forme β-η-normali nel λ-K-calcolo. Technical Report 696, CNR (1968). 
  18. [18] A. Bucciarelli and T. Ehrhard, Sequentiality and strong stability, in Proc. of LICS’91. IEEE Computer Society Press (1991) 138–145. 
  19. [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. [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. [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. [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. [23] E. Engeler, Algebras and combinators. Algebra Univers.13 (1981) 389–392. Zbl0482.08005MR631731
  24. [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. [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. [26] B. Intrigila, A problem on easy terms in lambda-calculus. Fundamenta Informaticae15 (1991) 99–106. Zbl0751.03006MR1153289
  27. [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. [28] G. Jacopini and M. Venturini-Zilli, Equating for recurrent terms of λ-calculus and combinatory logic. Technical Report 85, CNR (1978). Zbl0432.03010
  29. [29] G. Jacopini and M. Venturini-Zilli, Easy terms in the lambda-calculus. Fundam. Inform.8 (1985) 225–233. Zbl0574.03005MR798546
  30. [30] R. Kerth, Isomorphism et équivalence équationnelle entre modèles du λ-calcul. Master’s thesis, Université de Paris 7 (1995). 
  31. [31] R. Kerth, Isomorphism and equational equivalence of continuous lambda models. Stud. Log.61 (1998) 403–415. Zbl0964.03015MR1657121
  32. [32] R. Kerth, On the construction of stable models of λ-calculus. Theoret. Comput. Sci.269 (2001) 23–46. Zbl0992.68022MR1862408
  33. [33] C.P.J. Koymans, Models of the lambda calculus. Inform. Control52 (1982) 306–332. Zbl0542.03004MR707579
  34. [34] J. Kuper, On the Jacopini technique. Inform. Comput.138 (1997) 101–123. Zbl0887.68010MR1479318
  35. [35] G. Longo, Set-theoretical models of λ-calculus : theories, expansions, isomorphisms. Ann. Pure Appl. Logic24 (1983) 153–188. Zbl0513.03009MR713298
  36. [36] A.R. Meyer, What is a model of the lambda calculus? Inform. Control52 (1982) 87–122. Zbl0507.03002MR693998
  37. [37] G.D. Plotkin, Set-theoretical and other elementary models of the λ-calculus. Theoret. Comput. Sci.121 (1993) 351–409. Zbl0790.03014MR1249549
  38. [38] A. Salibra, Topological incompleteness and order incompleteness of the lambda calculus. ACM Trans. Comput. Log.4 (2003) 379–401. MR1995005
  39. [39] D.S. Scott, Continuous lattices, in Toposes, algebraic geometry and logic. Springer-Verlag (1972). Zbl0239.54006MR404073
  40. [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. [41] D.S. Scott, Lambda calculus : some models, some philosophy, in The Kleene Symposium. Amsterdam, The Netherlands, North-Holland (1980). Zbl0515.03004MR591884
  42. [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. [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. [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.