Abstract
Models of the untyped λ-calculus may be defined either as applicative structures satisfying a bunch of first-order axioms (λ-models), or as reflexive objects in cartesian closed categories (categorical models). In this paper we show that any categorical model of λ-calculus can be presented as a λ-model, even when the underlying category does not have enough points. We provide an example of an extensional model of λ-calculus in a category of sets and relations which has not enough points. Finally, we present some of its algebraic properties which make it suitable for dealing with non-deterministic extensions of λ-calculus.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Information and Computation 163(2), 409–470 (2000)
Amadio, R.M., Curien, P.-L.: Domains and lambda-calculi. Cambridge University Press, New York (1998)
Asperti, A., Longo, G.: Categories, types and structures. In: Categories, types and structures, MIT Press, Cambridge (1991)
Barendregt, H.P.: The lambda calculus: Its syntax and semantics. North-Holland Publishing Co., Amsterdam (1984)
Berline, C.: From computation to foundations via functions and application: The λ-calculus and its webbed models. Theoretical Computer Science 249, 81–161 (2000)
Berry, G., Curien, P.-L.: Sequential algorithms on concrete data structures. Theoretical Computer Science 20, 265–321 (1985)
Bucciarelli, A., Ehrhard, T.: On phase semantics and denotational semantics: the exponentials. Ann. Pure Appl. Logic 109(3), 205–241 (2001)
Curry, H.B., Feys, R.: Combinatory Logic, vol. I. North-Holland, Amsterdam (1958)
Dezani Ciancaglini, M., de’Liguoro, U., Piperno, A.: A filter model for concurrent λ-calculus. SIAM Journal of Computing 27(5), 1376–1419 (1998)
de’Liguoro, U., Piperno, A.: Non deterministic extensions of untyped λ-calculus. Information and Computation 109, 149–177 (1955)
Di Gianantonio, P., Franco, G., Honsell, F.: Game semantics for untyped lambda calculus. In: Duke, D.J., Marshall, M.S., Herman, I. (eds.) PREMO: A Framework for Multimedia Middleware. LNCS, vol. 1591, pp. 114–128. Springer, Heidelberg (1999)
Girard, J.-Y.: Normal functors, power series and the λ-calculus. Annals of pure and applied logic 37, 129–177 (1988)
Hindley, J.R., Longo, G.: Lambda calculus models and extensionality. Z. Math. Logik Grundlag. Math. 26, 289–310 (1980)
Hyland, M.: A syntactic characterization of the equality in some models for the lambda calculus. J. London Math. Soc. 12(3), 361–370 (1975)
Hyland, M., Nagayama, M., Power, J., Rosolini, G.: A category theoretic formulation for Engeler-style models of the untyped λ-calculus. Electronic notes in theoretical computer science 161, 43–57 (2006)
Hyland, M., Ong, C.-H.L.: On full abstraction for PCF: I. Models, observables and the full abstraction problem, II. Dialogue games and innocent strategies, III. A fully abstract and universal game model. Inf. and Comp. 163, 285–408 (2000)
Ker, A.D., Nickau, H., Ong, C.-H.L.: A universal innocent game model for the Boehm tree lambda theory. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 405–419. Springer, Heidelberg (1999)
Kerth, R.: On the construction of stable models of λ-calculus. Theoretical Computer Science 269, 23–46 (2001)
Koymans, C.P.J.: Models of the lambda calculus. Information and Control 52(3), 306–332 (1982)
Lambek, J.: From lambda calculus to Cartesian closed categories. In: Seldin, J.P., Hindley, J. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, London (1980)
Lambek, J., Scott, P.J.: Introduction to Higher Order Categorical Logic. The Journal of Symbolic Logic 54(3) (1989)
Plotkin, G.D.: The λ-calculus is ω-incomplete. J. Symb. Log. 39(2), 313–317 (1974)
Plotkin, G.D.: T ω as a Universal Domain. J. Comput. System Sci. 17, 209–236 (1978)
Scott, D.S.: Continuous lattices. In: Toposes, Algebraic geometry and Logic. LNM, vol. 274, Springer, Heidelberg (1972)
Selinger, P.: The lambda calculus is algebraic. J. Funct. Program. 12(6), 549–566 (2002)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bucciarelli, A., Ehrhard, T., Manzonetto, G. (2007). Not Enough Points Is Enough. In: Duparc, J., Henzinger, T.A. (eds) Computer Science Logic. CSL 2007. Lecture Notes in Computer Science, vol 4646. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74915-8_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-74915-8_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74914-1
Online ISBN: 978-3-540-74915-8
eBook Packages: Computer ScienceComputer Science (R0)