×

An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus. (English) Zbl 0763.03012

Summary: It is well known that a reflexive object in the Cartesian closed category of complete partial orders and Scott-continuous functions is a model of \(\lambda\)-calculus (briefly a topological model). A topological model, through the interpretation function, induces a \(\lambda\)-theory, i.e., a congruence relation on \(\lambda\)-terms closed under \(\alpha\)- and \(\beta\)-reduction. It is natural to ask if all possible \(\lambda\)- theories are induced by a topological model, i.e., if topological models are complete w.r.t. \(\lambda\)-calculus. The authors prove an Approximation Theorem, which holds in all topological models. Using this theorem, they analyze some topological models and their induced \(\lambda\)-theories, and they exhibit a \(\lambda\)-theory which cannot be induced by a topological model. So they prove that topological models are not complete w.r.t. \(\lambda\)-calculus.

MSC:

03B40 Combinatory logic and lambda calculus
68Q55 Semantics in the theory of computing
18D15 Closed categories (closed monoidal and Cartesian closed categories, etc.)
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Barendregt, H., The lambda calculus: its syntax and semantics, (1984), North-Holland Amsterdam, revised version · Zbl 0551.03007
[2] Barendregt, H.; Coppo, M.; Dezani, M., A filter lambda model and the completeness of type assignment, J. symbolic logic, 48, 931-940, (1983) · Zbl 0545.03004
[3] Coppo, M.; Dezani, M.; Honsell, F.; Longo, G., Extended type structures and filter lambda models, (), 241-262 · Zbl 0558.03007
[4] Hyland, J.M.E., A syntactic charaterization of the equality in some models of the λ-calculus, J. London math. soc. (2), 12, 361-370, (1976), (1976) · Zbl 0329.02010
[5] Honsell, F.; Della Rocca, S.Ronchi, Models for theories of functions strictly depending on all their arguments, internal report, (1986), Dipartimento di Informatica, University of Turin
[6] Longo, G., Set-theoretical models of λ-calculus: theories, expansions, isomorphisms, Ann. pure appl. logic, 24, 153-188, (1982) · Zbl 0513.03009
[7] Morris, J.M., Lambda calculus models of programming languages, ()
[8] Park, D., The Y-combinator in Scott’s lambda calculus models, ()
[9] Plotkin, G.D., LCF considered as a programming language, Theoret. comput. sci., 5, 223-255, (1977) · Zbl 0369.68006
[10] Scott, D., Continuous lattices, (), 97-136
[11] {\scD. Scott}, private communication, 1984.
[12] Wadsworth, C.P., The relation between computational and denotational properties for Scott’s D∞-models of the lambda calculus, SIAM J. comput., 5, 488-521, (1976) · Zbl 0346.02013
[13] Wadsworth, C.P., Approximate reductions and λ-calculus models, SIAM J. comput., 7, 337-356, (1978) · Zbl 0407.03021
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.