Topological incompleteness and order incompleteness of the lambda calculus

ABSTRACT

A model of the untyped lambda calculus univocally induces a lambda theory (i.e., a congruence relation on λ-terms closed under α- and β-conversion) through the kernel congruence relation of the interpretation function. A semantics of lambda calculus is (equationally) incomplete if there exists a lambda theory that is not induced by any model in the semantics. In this article, we introduce a new technique to prove in a uniform way the incompleteness of all denotational semantics of lambda calculus that have been proposed so far, including the strongly stable one, whose incompleteness had been conjectured by Bastonero, Gouy and Berline. We apply this technique to prove the incompleteness of any semantics of lambda calculus given in terms of partially ordered models with a bottom element. This incompleteness removes the belief that partial orderings with a bottom element are intrinsic to models of the lambda calculus, and that the incompleteness of a semantics is only due to the richness of the structure of representable functions. Instead, the incompleteness is also due to the richness of the structure of lambda theories. Further results of the article are: (i) an incompleteness theorem for partially ordered models with finitely many connected components (= minimal upward and downward closed sets); (ii) an incompleteness theorem for topological models whose topology satisfies a suitable property of connectedness; (iii) a completeness theorem for topological models whose topology is non-trivial and metrizable.

REFERENCES

• 1: Abramsky, S. 1991. Domain theory in logical form. Ann. Pure Appl. Logic 51, 1--77.
• 2: Samson Abramsky , C.-H. Luke Ong, Full abstraction in the lazy lambda calculus, Information and Computation, v.105 n.2, p.159-267, Aug. 1993 [doi>10.1006/inco.1993.1044]
• 3: Barendregt, H. 1984. The Lambda Calculus: Its Syntax and Semantics. Number 103 in Studies in Logic. North-Holland Publishing Co., Amsterdam, The Netherlands.
• 4: Bastonero, O. 1998. Equational incompleteness and incomparability results for λ-calculus semantics. Manuscript.
• 5: Bastonero, O. and Gouy, X. 1999. Strong stability and the incompleteness of stable models of λ-calculus. Ann. Pure Appl. Logic 100, 247--277.
• 6: Bentz, W. 1999. Topological implications in varieties. Algebra Univ. 42, 9--16.
• 7: Chantal Berline, From computation to foundations via functions and application: The &lgr;-calculus and its webbed models, Theoretical Computer Science, v.249 n.1, p.81-161, Oct. 2000 [doi>10.1016/S0304-3975(00)00057-8]
• 8: Gérard Berry, Stable Models of Typed lambda-Calculi, Proceedings of the Fifth Colloquium on Automata, Languages and Programming, p.72-89, July 17-21, 1978
• 9: Bucciarelli, A. and Ehrhard, T. 1991. Sequentiality and strong stability. In Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Publications, Los Alamitos, Calif., 138--145.
• 10: Coleman, J. 1996. Separation in topological algebras. Algebra Univ. 35, 72--84.
• 11: Coleman, J. 1997. Topological equivalents to n-permutability. Algebra Univ. 38, 200--209.
• 12: Curry, H. B. 1930. Grundlagen der kombinatorischen logik. Amer. J. Math. 52, 509--536.
• 13: Curry, H. B. and Feys, R. 1958. Combinatory Logic, Vol. I. North-Holland Publishing Co., Amsterdam, The Netherlands.
• 14: Ehrhard, T. 1993. Hypercoherences: A strongly stable model of linear logic. Math. Struct. Comput. Sci. 2, 365--385.
• 15: Gouy, X. 1995. Etude des théories équationnelles et des propriétés algébriques des modéles stables du λ-calcul. Ph.D. dissertation. Université de Paris 7, Paris, France.
• 16: Hofmann, K. and Mislove, M. 1995. All compact Hausdorff lambda models are degenerate. Funda. Inf. 22, 23--52.
• 17: Honsell, F. and Ronchi della Rocca, S. 1990. Reasoning about interpretation in qualitative λ-models. In Programming Concepts and Methods, M. Broy and C. Jones, Eds. Elsevier Science Publishing Co., Amsterdam, The Netherlands, 505--521.
• 18: Furio Honsell , Simonetta Ronchi Della Rocca, An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus, Journal of Computer and System Sciences, v.45 n.1, p.49-75, Aug. 1992 [doi>10.1016/0022-0000(92)90040-P]
• 19: Johnstone, P. 1982. Stone Spaces. Cambridge University Press, Cambridge, Mass.
• 20: Kerth, R. 1998. Isomorphism and equational equivalence of continuous lambda models. Stud. Logica 61, 403--415.
• 21: Kerth, R. 2001. On the construction of stable models of λ-calculus. Theoret. Comput. Sci. 269, 23--46.
• 22: Lusin, S. and Salibra, A. 2003. A note on absolutely unorderable combinatory algebras. J. Logic Comput. to appear.
• 23: Meyer, A. 1982. What is a model of the lambda calculus? Inf. Cont. 52, 87--122.
• 24: Mislove, M. 1998. Topology, domain theory and theoretical computer science. Top. Appl. 89, 3--59.
• 25: Don Pigozzi , Antonino Salibra, Lambda abstraction algebras: coordinatizing models of Lambda calculus, Fundamenta Informaticae, v.33 n.2, p.149-200, Feb. 1, 1998
• 26: Gordon D. Plotkin, Set-theoretical and other elementary models of the &lgr;-calculus, Theoretical Computer Science, v.121 n.1-2, p.351-409, Dec. 6, 1993 [doi>10.1016/0304-3975(93)90094-A]
• 27: Gordon Plotkin, On a question of H. Friedman, Information and Computation, v.126 n.1, p.74-77, April 10, 1996 [doi>10.1006/inco.1996.0035]
• 28: Antonino Salibra, On the algebraic models of Lambda calculus, Theoretical Computer Science, v.249 n.1, p.197-240, Oct. 2000 [doi>10.1016/S0304-3975(00)00059-1]
• 29: Antonino Salibra, A Continuum of Theories of Lambda Calculus without Semantics, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.334, June 16-19, 2001
• 30: Salibra, A. 2001b. Towards lambda calculus order-incompleteness. In Workshop on Böhm theorem: Applications to Computer Science Theory (BOTH 2001). Electronics Notes in Theoretical Computer Science, vol. 50. Elsevier Science Publishing Company, Amsterdam, The Netherlands, 147--160.
• 31: Schönfinkel, M. 1924. Über die bausteine der mathematischen logik. Math Anal. 92, 305--316.
• 32: Scott, D. 1972. Continuous lattices. In Toposes, Algebraic geometry and Logic, F. Lawvere, Ed. Lecture Notes in Computer Science, Vol. 274. Springer-Verlag, Berlin, Germany, 97--136.
• 33: Scott, D. 1980. Lambda calculus: Some models, some philosophy. In The Kleene Symposium, H. K. J. Barwise and K. Kunen, Eds. Number 101 in Studies in Logic. North-Holland Publishing Co., Amsterdam, The Netherlands, 97--136.
• 34: Peter Selinger, Order-Incompleteness and Finite Lambda Models, Extended Abstract, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.432, July 27-30, 1996
• 35: Peter Selinger, Functionality, polymorphism, and concurrency: a mathematical investigation of programming paradigms, University of Pennsylvania, Philadelphia, PA, 1998
• 36: Steen, L. and Seebach, J. 1978. Counterexamples in topology. Springer-Verlag, Berlin, Germany.
• 37: Świerczkowski, S. 1964. Topologies in free algebras. Proc. London Math. Soc. 3, 566--576.
• 38: Taylor, W. 1977. Varieties obeying homotopy laws. Canad. Journal Math. 29, 498--527.
• 39: Ursini, A. 1994. On subtractive varieties, I. Algebra Univ. 31, 204--222.
• 40: Visser, A. 1980. Numerations, λ-calculus and arithmetic. In To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, J. Hindley and J. Seldin, Eds. Academic Press, New York, 259--284.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Denotational semantics

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Languages, Theory

Keywords:
Lambda calculus, Lambda theories, order and topological incompleteness, orderability/unorderability, partially ordered models, topological models