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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
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)