Hostname: page-component-745bb68f8f-hvd4g Total loading time: 0 Render date: 2025-01-09T06:21:09.283Z Has data issue: false hasContentIssue false
  • English
  • Français

Effective λ-models versus recursively enumerable λ-theories

Published online by Cambridge University Press:  04 September 2009

CHANTAL BERLINE ,
GIULIO MANZONETTO  and
ANTONINO SALIBRA
CHANTAL BERLINE
Affiliation:
CNRS, Laboratoire PPS, Université Paris 7, 2, place Jussieu (case 7014), 75251 Paris Cedex 05, France Email: chantal.berline@pps.jussieu.fr
GIULIO MANZONETTO
Affiliation:
INRIA Email: giulio.manzonetto@inria.fr
ANTONINO SALIBRA
Affiliation:
Università Ca'Foscari di Venezia, Dipartimento di Informatica, Via Torino 155, 30172 Venezia, Italy Email: salibra@dsi.unive.it
Get access Rights & Permissions [Opens in a new window]

Abstract

A longstanding open problem is whether there exists a non-syntactical model of the untyped λ-calculus whose theory is exactly the least λ-theory λβ. In this paper we investigate the more general question of whether the equational/order theory of a model of the untyped λ-calculus can be recursively enumerable (r.e. for short). We introduce a notion of effective model of λ-calculus, which covers, in particular, all the models individually introduced in the literature. We prove that the order theory of an effective model is never r.e.; from this it follows that its equational theory cannot be λβ or λβη. We then show that no effective model living in the stable or strongly stable semantics has an r.e. equational theory. For Scott's semantics, we investigate the class of graph models and prove that no order theory of a graph model can be r.e., and that there exists an effective graph model whose equational/order theory is the minimum among the theories of graph models. Finally, we show that the class of graph models enjoys a kind of downwards Löwenheim–Skolem theorem.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 19 , Issue 5 , October 2009 , pp. 897 - 942
Copyright
Copyright © Cambridge University Press 2009

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Amadio, R. and Curien, P.-L. (1998) Domains and lambda-calculi, Cambridge Tracts in Theoretical Computer Science 46, Cambridge University Press.CrossRefGoogle Scholar
Baeten, J. and Boerboom, B. (1979) Omega can be anything it should not be. In: Proc. Koninklijke Netherlandse Akademie van Wetenschappen. Indag. Matematicae Serie A 41 111–120.CrossRefGoogle Scholar
Barendregt, H. (1984) The Lambda calculus: Its syntax and semantics, North-Holland.Google Scholar
Bastonero, O. (1996) Modèles fortement stables du λ-calcul et résultats d'incomplétude, Ph.D. thesis, Université de Paris 7.Google Scholar
Berardi, S. and Berline, C. (2002) βη-complete models for System F. Mathematical Structures in Computer Science 12 823–874.CrossRefGoogle Scholar
Berline, C. (2000) From computation to foundations via functions and application: The λ-calculus and its webbed models. Theoretical Computer Science 249 81–161.CrossRefGoogle Scholar
Berline, C. (2006) Graph models of λ-calculus at work, and variations. Mathematical Structures in Computer Science 16 1–37.Google Scholar
Berline, C., Manzonetto, G. and Salibra, A. (2007) Lambda theories of effective lambda models. In: 16th EACSL Annual Conference on Computer Science and Logic (CSL'07). Springer-Verlag Lecture Notes in Computer Science 4646 268–282.Google Scholar
Berline, C. and Salibra, A. (2006) Easiness in graph models. Theoretical Computer Science 354 4–23.CrossRefGoogle Scholar
Berry, G. (1978) Stable models of typed lambda-calculi. In: Proceedings of the Fifth Colloquium on Automata, Languages and Programming. Springer-Verlag Lecture Notes in Computer Science 62.Google Scholar
Berry, G. (1979) Modèles complètement adéquats et stable des λ-calculs typés, Ph.D. thesis, Université de Paris 7.Google Scholar
Berry, G., Curien, P.-L. and Lévy, J.-J. (1985) Full abstraction for sequential languages: the state of the art. Algebraic Methods in Semantics 89–132.Google Scholar
Bucciarelli, A. and Ehrhard, T. (1991a) Extensional embedding of a strongly stable model of pcf. In: ICALP '91: Proceedings of the 18th International Colloquium on Automata, Languages and Programming, London, U.K., Springer-Verlag 35–46.Google Scholar
Bucciarelli, A. and Ehrhard, T. (1991b) Sequentiality and strong stability. In: Sixth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press 138–145.Google Scholar
Bucciarelli, A. and Salibra, A. (2003) The minimal graph model of lambda calculus. In: MFCS'03. Springer-Verlag Lecture Notes in Computer Science 2747 300–307.Google Scholar
Bucciarelli, A. and Salibra, A. (2004) The sensible graph theories of lambda calculus. In: 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), IEEE Computer Society Publications 276–285.Google Scholar
Bucciarelli, A. and Salibra, A. (2008) Graph lambda theories. Mathematical Structures in Computer Science 18 (5)975–1004.CrossRefGoogle Scholar
Coppo, M. and Dezani-Ciancaglini, M. (1980) An extension of the basic functionality theory for the λ-calculus. Notre-Dame Journal of Formal Logic 21 (4)685–693.CrossRefGoogle Scholar
Coppo, M., Dezani-Ciancaglini, M., Honsell, F. and Longo, G. (1984) Extended Type Structures and Filter Lambda Models. In: Lolli, G., Longo, G. and Marcja, A. (eds.) Logic Colloquium 82, Amsterdam, the Netherlands, North-Holland 241–262.CrossRefGoogle Scholar
Coppo, M., Dezani-Ciancaglini, M. and Zacchi, M. (1987) Type theories, normal forms and D ∞ λ-models. Information and Computation 72 85–116.CrossRefGoogle Scholar
David, R. (2001) Computing with Böhm trees. Fundam. Inform. 45 (1–2)53–77.Google Scholar
Di Gianantonio, P., Honsell, F. and Plotkin, G. (1995) Uncountable limits and the lambda calculus. Nordic Journal of Computing 2 (2)126–145.Google Scholar
Escardó, M. (1996) Pcf extended with real numbers. Theoretical Computer Science 162 (1)79–115.Google Scholar
Giannini, P. and Longo, G. (1984) Effectively given domains and lamba-calculus models. Information and Control 62 36–63.CrossRefGoogle Scholar
Gouy, X. (1995) Etude des théories équationnelles et des propriétés algébriques des modèles stables du λ-calcul, Ph.D. thesis, Université de Paris 7.Google Scholar
Gruchalski, A. (1996) Computability on di-domains. Inf. Comput. 124 (1)7–19.CrossRefGoogle Scholar
Honsell, F. (2007) TLCA list of open problems: Problem # 22. (Available at http://tlca.di.unito.it/opltlca/problem22.pdf.)Google Scholar
Honsell, F. and Ronchi Della Rocca, S. (1990) Reasoning about interpretations in qualitative lambda models. In: Broy, M. and Jones, C. B. (eds.) Proceedings of the IFIP Working Group 2.2/2.3, North-Holland 505–521.Google Scholar
Honsell, F. and Ronchi Della Rocca, S. (1992) An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus. Journal of Computer and System Sciences 45 49–75.Google Scholar
Jiang, Y. (1993) Consistence et inconsistence de théories de λ-calcul étendus, Ph.D. thesis, Université de Paris 7.Google Scholar
Kerth, R. (1994) 2ℵ0 modèles de graphes non-équationnellement équivalents. Notes de comptes-rendus de l'Académie des Sciences 318 587–590.Google Scholar
Kerth, R. (1995) Isomorphism et équivalence équationnelle entre modèles du λ-calcul, Ph.D. thesis, Université de Paris 7.Google Scholar
Kerth, R. (1998a) The interpretation of unsolvable terms in models of pure λ-calculus. J. Symbolic Logic 63 1529–1548.Google Scholar
Kerth, R. (1998b) Isomorphism and equational equivalence of continuous lambda models. Studia Logica 61 403–415.CrossRefGoogle Scholar
Kerth, R. (2001) On the construction of stable models of λ-calculus. Theoretical Computer Science 269 23–46.Google Scholar
Krivine, J.-L. (1993) Lambda-calculus, types and models. Horwood, Ellis. (Translated from the French original: Lambda-calcul, Types et Modeles (1990) Masson, Paris.)Google Scholar
Longo, G. (1983) Set-theoretical models of λ-calculus: theories, expansions, isomorphisms. Ann. Pure Appl. Logic 24 (2)153–188.CrossRefGoogle Scholar
Lusin, S. and Salibra, A. (2004) The lattice of lambda theories. Journal of Logic and Computation 14 373–394.Google Scholar
Manzonetto, G. and Salibra, A. (2006) Boolean algebras for lambda calculus. In: Proc. 21th IEEE Symposium on Logic in Computer Science (LICS 2006) 139–148.Google Scholar
Odifreddi, P. (1989) Classical Recursion Theory, Elsevier.Google Scholar
Plotkin, G. (1977) LCF considered as a programming language. Theoretical Computer Science 5 223–255.Google Scholar
Plotkin, G. (1993) Set-theoretical and other elementary models of the lambda-calculus. Theoretical Computer Science 121 (1–2)351–409.CrossRefGoogle Scholar
Pravato, A., Bastonero, O. and Ronchi Della Rocca, S. (1997) Structures for lazy semantics.CrossRefGoogle Scholar
Salibra, A. (2003) Topological incompleteness and order incompleteness of the lambda calculus. In: LICS'01 Special Issue. ACM Transactions on Computational Logic 4 379–401.CrossRefGoogle Scholar
Scott, D. (1972) Continuous lattices. In: Toposes, algebraic geometry and logic, Springer-Verlag.Google Scholar
Selinger, P. (1996) Order-incompleteness and finite lambda models – extended abstract. In: LICS'96: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society 432.Google Scholar
Selinger, P. (2003) Order-incompleteness and finite lambda reduction models. Theoretical Computer Science 309 43–63.CrossRefGoogle Scholar
Stoltenberg-Hansen, V., Lindström, I. and Griffor, E. (1994) Mathematical theory of domains, Cambridge University Press.Google Scholar
Visser, A. (1980) Numerations, λ-calculus, and arithmetic. In: Hindley, J. R. and Seldin, J. P. (eds.) Essays on Combinatory Logic, Lambda-Calculus, and Formalism, Academic Press 259–284.Google Scholar