Abstract
Given a semi-ring with unit which satisfies some algebraic conditions, we define an exponential functor on the category of sets and relations which allows to define a denotational model of differential linear logic and of the lambda-calculus with resources. We show that, when the semi-ring has an element which is infinite in the sense that it is equal to its successor, this model does not validate the Taylor formula and that it is possible to build, in the associated Kleisli cartesian closed category, a model of the pure lambda-calculus which is not sensible. This is a quantitative analogue of the standard graph model construction in the category of Scott domains. We also provide examples of such semi-rings.
This is a preview of subscription content, log in via an institution to check access.
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
Amadio, R., Curien, P.-L.: Domains and lambda-calculi. Cambridge Tracts in Theoretical Computer Science, vol. 46. Cambridge University Press, Cambridge (1998)
Barendregt, H.: The Lambda Calculus. Studies in Logic and the Foundations of Mathematics, vol. 103. North-Holland, Amsterdam (1984)
Bucciarelli, A., Ehrhard, T., Manzonetto, G.: Not enough points is enough. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646. Springer, Heidelberg (2007)
Bucciarelli, A., Ehrhard, T., Manzonetto, G.: A relational model of a parallel and non-deterministic lambda-calculus. In: Artëmov, S.N., Nerode, A. (eds.) LFCS 2009. LNCS, vol. 5407, pp. 107–121. Springer, Heidelberg (2008)
Bierman, G.: What is a categorical model of intuitionistic linear logic? In: Dezani-Ciancaglini, M., Plotkin, G.D. (eds.) TLCA 1995. LNCS, vol. 902, pp. 73–93. Springer, Heidelberg (1995)
De Carvalho, D.: Execution Time of λ-Terms via Denotational Semantics and Intersection Types. Research Report RR-6638, INRIA (2008)
Ehrhard, T., Laurent, O.: Interpreting a finitary pi-calculus in differential interaction nets. Information and Computation 208(6) (2010); Special Issue: 18th International Conference on Concurrency Theory (CONCUR 2007)
Ehrhard, T., Regnier, L.: The differential lambda-calculus. Theoretical Computer Science 309(1-3), 1–41 (2003)
Ehrhard, T., Regnier, L.: Böhm trees, Krivine machine and the Taylor expansion of ordinary lambda-terms. In: Beckmann, A., Berger, U., Löwe, B., Tucker, J.V. (eds.) CiE 2006. LNCS, vol. 3988, pp. 186–197. Springer, Heidelberg (2006)
Ehrhard, T., Regnier, L.: Differential interaction nets. Theoretical Computer Science 364(2), 166–195 (2006)
Ehrhard, T., Regnier, L.: Uniformity and the Taylor expansion of ordinary lambda-terms. Theoretical Computer Science 403(2-3), 347–372 (2008)
Girard, J.-Y.: Normal functors, power series and the λ-calculus. Annals of Pure and Applied Logic 37, 129–177 (1988)
Krivine, J.-L.: Lambda-Calculus, Types and Models. Ellis Horwood Series in Computers and Their Applications. Ellis Horwood, Masson (1993) Translation by René Cori from French edition (1990)
Manzonetto, G., Salibra, A.: Applying universal algebra to lambda calculus. Journal of Logic and Computation (2009) (to appear)
Pigozzi, D., Salibra, A.: Lambda Abstraction Algebras: Coordinatizing Models of Lambda Calculus. Fundamenta Informaticae 33(2), 149–200 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Carraro, A., Ehrhard, T., Salibra, A. (2010). Exponentials with Infinite Multiplicities. In: Dawar, A., Veith, H. (eds) Computer Science Logic. CSL 2010. Lecture Notes in Computer Science, vol 6247. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15205-4_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-15205-4_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15204-7
Online ISBN: 978-3-642-15205-4
eBook Packages: Computer ScienceComputer Science (R0)