Antonino Salibra
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.
- Abramsky, S. 1991. Domain theory in logical form. Ann. Pure Appl. Logic 51, 1--77.Google Scholar
- Abramsky, S. and Ong, C. 1993. Full abstraction in the lazy λ-calculus. Inf. Comput. 105, 159--267. Google Scholar
- Barendregt, H. 1984. The Lambda Calculus: Its Syntax and Semantics. Number 103 in Studies in Logic. North-Holland Publishing Co., Amsterdam, The Netherlands.Google Scholar
- Bastonero, O. 1998. Equational incompleteness and incomparability results for λ-calculus semantics. Manuscript.Google Scholar
- Bastonero, O. and Gouy, X. 1999. Strong stability and the incompleteness of stable models of λ-calculus. Ann. Pure Appl. Logic 100, 247--277.Google Scholar
- Bentz, W. 1999. Topological implications in varieties. Algebra Univ. 42, 9--16.Google Scholar
- Berline, C. 2000. From computation to foundations via functions and application: The λ-calculus and its webbed models. Theoret. Comput. Sci. 249, 81--161. Google Scholar
- Berry, G. 1978. Stable models of typed lambda-calculi. In Proceedings of the 5th International Colloqium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 62. Springer-Verlag, Berline, Germany. Google Scholar
- 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.Google Scholar
- Coleman, J. 1996. Separation in topological algebras. Algebra Univ. 35, 72--84.Google Scholar
- Coleman, J. 1997. Topological equivalents to n-permutability. Algebra Univ. 38, 200--209.Google Scholar
- Curry, H. B. 1930. Grundlagen der kombinatorischen logik. Amer. J. Math. 52, 509--536.Google Scholar
- Curry, H. B. and Feys, R. 1958. Combinatory Logic, Vol. I. North-Holland Publishing Co., Amsterdam, The Netherlands.Google Scholar
- Ehrhard, T. 1993. Hypercoherences: A strongly stable model of linear logic. Math. Struct. Comput. Sci. 2, 365--385.Google Scholar
- 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.Google Scholar
- Hofmann, K. and Mislove, M. 1995. All compact Hausdorff lambda models are degenerate. Funda. Inf. 22, 23--52. Google Scholar
- 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.Google Scholar
- Honsell, F. and Ronchi della Rocca, S. 1992. An approximation theorem for topological λ-models and the topological incompleteness of λ-calculus. J. Comput. Syst. Sci. 45, 49--75. Google Scholar
- Johnstone, P. 1982. Stone Spaces. Cambridge University Press, Cambridge, Mass.Google Scholar
- Kerth, R. 1998. Isomorphism and equational equivalence of continuous lambda models. Stud. Logica 61, 403--415.Google Scholar
- Kerth, R. 2001. On the construction of stable models of λ-calculus. Theoret. Comput. Sci. 269, 23--46.Google Scholar
- Lusin, S. and Salibra, A. 2003. A note on absolutely unorderable combinatory algebras. J. Logic Comput. to appear.Google Scholar
- Meyer, A. 1982. What is a model of the lambda calculus? Inf. Cont. 52, 87--122.Google Scholar
- Mislove, M. 1998. Topology, domain theory and theoretical computer science. Top. Appl. 89, 3--59.Google Scholar
- Pigozzi, D. and Salibra, A. 1998. Lambda abstraction algebras: coordinatizing models of lambda calculus. Fund. Inf. 33, 149--200. Google Scholar
- Plotkin, G. 1993. Set-theoretical and other elementary models of the λ-calculus. Theoret. Comput. Sci. 121, 351--409. Google Scholar
- Plotkin, G. 1996. On a question of H. Friedman. Inf. Comput. 126, 74--77. Google Scholar
- Salibra, A. 2000. On the algebraic models of lambda calculus. Theoret. Comput. Sci. 249, 197--240. Google Scholar
- Salibra, A. 2001a. A continuum of theories of lambda calculus without semantics. In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS'01). IEEE Computer Society Publications, Los Alamitos, Calif., 334--343. Google Scholar
- 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.Google Scholar
- Schönfinkel, M. 1924. Über die bausteine der mathematischen logik. Math Anal. 92, 305--316.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- Selinger, P. 1996. Order-incompleteness and finite lambda models. In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Publications, Los Alamitos, Calif. Google Scholar
- Selinger, P. 1997. Functionality, polymorphism, and concurrency: a mathematical investigation of programming paradigms. Ph.D. dissertation, University of Pennsylvania. Google Scholar
- Steen, L. and Seebach, J. 1978. Counterexamples in topology. Springer-Verlag, Berlin, Germany.Google Scholar
- Świerczkowski, S. 1964. Topologies in free algebras. Proc. London Math. Soc. 3, 566--576.Google Scholar
- Taylor, W. 1977. Varieties obeying homotopy laws. Canad. Journal Math. 29, 498--527.Google Scholar
- Ursini, A. 1994. On subtractive varieties, I. Algebra Univ. 31, 204--222.Google Scholar
- 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.Google Scholar
Index Terms
- Topological incompleteness and order incompleteness of the lambda calculus
Recommendations
Linear lambda calculus with non-linear first-class continuations
ICSCA '17: Proceedings of the 6th International Conference on Software and Computer ApplicationsThe Curry-Howard isomorphism is the correspondence between propositions and types, proofs and lambda-terms, and proof normalization and evaluation. In Curry-Howard isomorphism, we find a duality between values and continuations in pure functional ...
Lambda Abstraction Algebras: Coordinatizing Models of Lambda Calculus
Lambda abstraction algebras are designed to algebraize the untyped lambda calculus in the same way cylindric and polyadic algebras algebraize the first-order logic; they are intended as an alternative to combinatory algebras in this regard. Like ...
Lambda Abstraction Algebras: Coordinatizing Models of Lambda Calculus
Lambda abstraction algebras are designed to algebraize the untyped lambda calculus in the same way cylindric and polyadic algebras algebraize the first-order logic; they are intended as an alternative to combinatory algebras in this regard. Like ...
Comments