article

Topological incompleteness and order incompleteness of the lambda calculus

Author:

Antonino SalibraAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 4, Issue 3

Pages 379 - 401

https://doi.org/10.1145/772062.772067

Published: 01 July 2003 Publication History

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]

Abramsky, S. and Ong, C. 1993. Full abstraction in the lazy λ-calculus. Inf. Comput. 105, 159--267.

[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]

Berline, C. 2000. From computation to foundations via functions and application: The λ-calculus and its webbed models. Theoret. Comput. Sci. 249, 81--161.

[8]

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.

[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]

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.

[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]

Pigozzi, D. and Salibra, A. 1998. Lambda abstraction algebras: coordinatizing models of lambda calculus. Fund. Inf. 33, 149--200.

[26]

Plotkin, G. 1993. Set-theoretical and other elementary models of the λ-calculus. Theoret. Comput. Sci. 121, 351--409.

[27]

Plotkin, G. 1996. On a question of H. Friedman. Inf. Comput. 126, 74--77.

[28]

Salibra, A. 2000. On the algebraic models of lambda calculus. Theoret. Comput. Sci. 249, 197--240.

[29]

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.

[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]

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.

[35]

Selinger, P. 1997. Functionality, polymorphism, and concurrency: a mathematical investigation of programming paradigms. Ph.D. dissertation, University of Pennsylvania.

[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.

Cited By

Gabbay MGabbay M(2017)Representation and duality of the untyped λ-calculus in nominal lattice and topological semantics, with a proof of topological completenessAnnals of Pure and Applied Logic10.1016/j.apal.2016.10.001168:3(501-621)Online publication date: Mar-2017
https://doi.org/10.1016/j.apal.2016.10.001
Salibra A(2012)Scott is always simpleProceedings of the 37th international conference on Mathematical Foundations of Computer Science10.1007/978-3-642-32589-2_3(31-45)Online publication date: 27-Aug-2012
https://dl.acm.org/doi/10.1007/978-3-642-32589-2_3
Kowalski TPaoli F(2011)Joins and subdirect products of varietiesAlgebra universalis10.1007/s00012-011-0137-065:4(371-391)Online publication date: 17-Jun-2011
https://doi.org/10.1007/s00012-011-0137-0
Show More Cited By

Index Terms

Topological incompleteness and order incompleteness of the lambda calculus
1. Mathematics of computing
  1. Continuous mathematics
    1. Calculus
      1. Lambda calculus
  2. Mathematical analysis
    1. Calculus
      1. Lambda calculus
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics
      1. Denotational semantics

Recommendations

Linear lambda calculus with non-linear first-class continuations
ICSCA '17: Proceedings of the 6th International Conference on Software and Computer Applications

The 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

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 4, Issue 3

July 2003

121 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/772062

Issue’s Table of Contents

Copyright © 2003 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 July 2003

Published in TOCL Volume 4, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

24
Total Citations
View Citations
504
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)1

Reflects downloads up to 06 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Gabbay MGabbay M(2017)Representation and duality of the untyped λ-calculus in nominal lattice and topological semantics, with a proof of topological completenessAnnals of Pure and Applied Logic10.1016/j.apal.2016.10.001168:3(501-621)Online publication date: Mar-2017
https://doi.org/10.1016/j.apal.2016.10.001
Salibra A(2012)Scott is always simpleProceedings of the 37th international conference on Mathematical Foundations of Computer Science10.1007/978-3-642-32589-2_3(31-45)Online publication date: 27-Aug-2012
https://dl.acm.org/doi/10.1007/978-3-642-32589-2_3
Kowalski TPaoli F(2011)Joins and subdirect products of varietiesAlgebra universalis10.1007/s00012-011-0137-065:4(371-391)Online publication date: 17-Jun-2011
https://doi.org/10.1007/s00012-011-0137-0
Bou FPaoli FLedda ASpinks MGiuntini R(2010)The Logic of Quasi-MV AlgebrasJournal of Logic and Computation10.1093/logcom/exp08020:2(619-643)Online publication date: 1-Apr-2010
https://dl.acm.org/doi/10.1093/logcom/exp080
Manzonetto GSalibra A(2010)Applying Universal Algebra to Lambda Calculus*Journal of Logic and Computation10.1093/logcom/exn08520:4(877-915)Online publication date: 1-Aug-2010
https://dl.acm.org/doi/10.1093/logcom/exn085
Carraro ASalibra A(2009)Reflexive Scott Domains are Not Complete for the Extensional Lambda CalculusProceedings of the 2009 24th Annual IEEE Symposium on Logic In Computer Science10.1109/LICS.2009.22(91-100)Online publication date: 11-Aug-2009
https://dl.acm.org/doi/10.1109/LICS.2009.22
Gabbay M(2009)Nominal Algebra and the HSP TheoremJournal of Logic and Computation10.1093/logcom/exn05519:2(341-367)Online publication date: 1-Apr-2009
https://dl.acm.org/doi/10.1093/logcom/exn055
Berline CManzonetto GSalibra A(2009)Effective λ-models versus recursively enumerable λ-theoriesMathematical Structures in Computer Science10.1017/S096012950999005319:5(897-942)Online publication date: 1-Oct-2009
https://dl.acm.org/doi/10.1017/S0960129509990053
Honsell FPlotkin G(2009)On the completeness of order-theoretic models of the λ-calculusInformation and Computation10.1016/j.ic.2008.03.027207:5(583-594)Online publication date: 1-May-2009
https://dl.acm.org/doi/10.1016/j.ic.2008.03.027
Bou FPaoli FLedda AFreytes H(2008)On some properties of quasi-MV algebras and $$\sqrt{^{\prime}}$$ quasi-MV algebras. Part IISoft Computing - A Fusion of Foundations, Methodologies and Applications10.5555/2698239.269830912:4(341-352)Online publication date: 1-Feb-2008
https://dl.acm.org/doi/10.5555/2698239.2698309
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents