Abstract
Relational semantics is one of the simplest and categorically most natural semantics of Linear Logic. The co-Kleisli category MRel associated with its multiset exponential comonad contains a fully abstract model of the untyped λ-calculus. That particular object of MRel is also a model of the resource λ-calculus, deriving from Ehrhard and Regnier’s differential extension of Linear Logic and related to Boudol’s λ-calculus with multiplicities. Bucciarelli et al. conjectured that model to be fully-abstract also for the resource λ-calculus. We give a counter-example to the conjecture. As a by-product we achieve a context lemma for the resource λ-calculus.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Boudol, G.: The lambda-calculus with multiplicities. INRIA Research Report 2025 (1993)
Breuvart, F.: On the discriminating power of tests. arXiv preprint arXiv:1205.4691 (2012) (unpublished)
Bucciarelli, A., Carraro, A., Ehrhard, T., Manzonetto, G.: Full Abstraction for Resource Calculus with Tests. In: Bezem, M. (ed.) Computer Science Logic (CSL 2011) - 25th International Workshop/20th Annual Conference of the EACSL, Leibniz International Proceedings in Informatics (LIPIcs), vol. 12, pp. 97–111. Schloss Dagstuhl Leibniz-Zentrum fuer Informatik, Dagstuhl (2011)
Bucciarelli, A., Carraro, A., Ehrhard, T., Manzonetto, G.: Full Abstraction for the Resource Lambda Calculus with Tests, through Taylor Expansion. Logical Methods in Computer Science 8(4), 1–44 (2012)
Bucciarelli, A., Ehrhard, T., Manzonetto, G.: Not Enough Points Is Enough. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 298–312. Springer, Heidelberg (2007)
Bucciarelli, A., Ehrhard, T., Manzonetto, G.: A relational model of a parallel and non-deterministic λ-calculus. In: Artemov, S., Nerode, A. (eds.) LFCS 2009. LNCS, vol. 5407, pp. 107–121. Springer, Heidelberg (2008)
De Carvalho, D., Tortora de Falco, L.: The relational model is injective for Multiplicative Exponential Linear Logic (without weakenings). Annals of Pure and Applied Logic (2012)
De Carvalho, D.: Execution time of lambda-terms via denotational semantics and intersection types. arXiv preprint arXiv:0905.4251 (2009)
Ehrhard, T.: A model-oriented introduction to differential linear logic (2011) (accepted)
Ehrhard, T.: An application of the extensional collapse of the relational model of linear logic. In: Accepted at CSL 2012 (2012)
Ehrhard, T., Regnier, L.: The differential lambda-calculus. Theoretical Computer Science (2004)
Ehrhard, T., Regnier, L.: Böhm Trees, Krivine’s Machine and the Taylor Expansion of 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)
Laird, J., Manzonetto, G., McCusker, G., Pagani, M.: Weighted relational models of typed lambda-calculi (submitted, 2013)
Manzonetto, G.: A general class of models of \(\mathcal{H}^*\). In: Královič, R., Niwiński, D. (eds.) MFCS 2009. LNCS, vol. 5734, pp. 574–586. Springer, Heidelberg (2009)
Manzonetto, G.: What is a Categorical Model of the Differential and the Resource λ-Calculi? Mathematical Structures in Computer Science 22(3), 451–520 (2012)
Pagani, M., Tranquilli, P.: Parallel reduction in resource lambda-calculus. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 226–242. Springer, Heidelberg (2009)
Pagani, M., Ronchi Della Rocca, S.: Linearity, Non-determinism and Solvability. Fundamenta Informaticae 103(1-4), 173–202 (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Breuvart, F. (2013). The Resource Lambda Calculus Is Short-Sighted in Its Relational Model. In: Hasegawa, M. (eds) Typed Lambda Calculi and Applications. TLCA 2013. Lecture Notes in Computer Science, vol 7941. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38946-7_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-38946-7_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38945-0
Online ISBN: 978-3-642-38946-7
eBook Packages: Computer ScienceComputer Science (R0)