Hostname: page-component-78c5997874-g7gxr Total loading time: 0 Render date: 2024-11-09T12:47:19.116Z Has data issue: false hasContentIssue false
  • English
  • Français

Infinitary affine proofs

Published online by Cambridge University Press:  07 July 2015

DAMIANO MAZZA
DAMIANO MAZZA*
Affiliation:
CNRS, UMR 7030, Laboratoire d'Informatique de Paris Nord, Université Paris 13, Sorbonne Paris Cité, F-93430 Villetaneuse, France Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Even though the multiplicative–additive fragment of linear logic forbids structural rules in general, is does admit a bounded form of exponential modalities enjoying a bounded form of structural rules. The approximation theorem, originally proved by Girard, states that if full linear logic proves a propositional formula, then the multiplicative–additive fragment proves every bounded approximation of it. This may be understood as the fact that multiplicative–additive linear logic is somehow dense in full linear logic. Our goal is to give a technical formulation of this informal remark. We introduce a Cauchy-complete space of infinitary affine term-proofs and we show that it yields a fully complete model of multiplicative exponential polarised linear logic, in the style of Girard's ludics. Moreover, the subspace of finite term-proofs, which is a model of multiplicative polarised linear logic, is dense in the space of all term-proofs.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 27 , Special Issue 5: Computing with Lambda-terms. A Special Issue Dedicated to Corrado Böhm for his 90th Birthday , June 2017 , pp. 581 - 602
Copyright
Copyright © Cambridge University Press 2015 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abramsky, S., Jagadeesan, R. and Malacaria, P. (2000). Full abstraction for PCF. Information Computation 163 (2) 409–470.Google Scholar
Arnold, A. and Nivat, M. (1980). The metric space of infinite trees. Algebraic and topological properties. Fundamenta Informaticae 3 (4) 445–476.Google Scholar
Basaldella, M. (2008). On Exponentials in Ludics, PhD thesis, University of Siena.Google Scholar
Basaldella, M. and Faggian, C. (2009). Ludics with repetitions (exponentials, interactive types and completeness). In: Proceedings of LICS 375–384.Google Scholar
Boudol, G. (1993). The lambda-calculus with multiplicities. Technical report 2025, INRIA Sophia-Antipolis.Google Scholar
Bourbaki, N. (1998). General Topology: Chapters 1–4, Springer.Google Scholar
Courcelle, B. (1983). Fundamental properties of infinite trees. Theoretical Computer Science 25 (2) 95–169.Google Scholar
Curien, P. (1998). Abstract böhm trees. Mathematical Structures in Computer Science 8 (6) 559–591.Google Scholar
Curien, P.-L., Herbelin, H., Krivine, J.-L. and Melliès, P.-A. (2010). Interactive Models of Computation and Program Behavior, American Mathematical Society.Google Scholar
Dershowitz, N., Kaplan, S. and Plaisted, D. A. (1991). Rewrite, rewrite, rewrite, rewrite, rewrite,. . . . Theoretical Computer Science 83 (1) 71–96.Google Scholar
Ehrhard, T. (2005). Finiteness spaces. Mathematical Structures in Computer Science 15 (4) 615–646.Google Scholar
Ehrhard, T. and Regnier, L. (2008). Uniformity and the Taylor expansion of ordinary lambda-terms. Theoretical Computer Science, 403 (2–3) 347–372.Google Scholar
Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science 50 (1) 1–102.Google Scholar
Girard, J.-Y. (1991). A New Constructive Logic: Classical Logic. Mathematical Structures in Computer Science 1 (3) 255–296.Google Scholar
Girard, J.-Y. (2001). Locus solum. Mathematical Structures in Computer Science 11 (3) 301–506.Google Scholar
Hyland, M. and Ong, L. (2000). On full abstraction for PCF: I, II and III. Information Computation 163 (2) 285–408.Google Scholar
Kennaway, R., Klop, J. W., Sleep, R. and de Vries, F.-J. (1997). Infinitary lambda calculus. Theoretical Computer Science. 175 (1) 93–125.Google Scholar
Kfoury, A. J. (2000). A linearization of the lambda-calculus and consequences. Journal of Logic and Computation 10 (3) 411–436.Google Scholar
Laurent, O. (2004). Polarized games. Annals of Pure and Applied Logic 130 (1–3) 79–123.Google Scholar
Laurent, O. and Regnier, L. (2003). About translations of classical logic into polarized linear logic. In: Proceedings of LICS 11–20.Google Scholar
Mazza, D. (2012). An infinitary affine lambda-calculus isomorphic to the full lambda-calculus. In: Proceedings of LICS 471–480.Google Scholar
Mazza, D. (2014). Non-uniform polytime computation in the infinitary affine lambda-calculus. In: Proceedings of ICALP, Part II 305–317.Google Scholar
Melliès, P.-A. (2004). Asynchronous games 1: A group-theoretic formulation of uniformity. Technical Report PPS//04//06//n°31, Preuves, Programmes et Systèmes.Google Scholar
Melliès, P.-A. (2005). Asynchronous games 4: A fully complete model of propositional linear logic. In: Proceedings of LICS 386–395.Google Scholar
Melliès, P.-A. (2006). Asynchronous games 2: The true concurrency of innocence. Theoretical Computer Science 358 (2–3) 200–228.Google Scholar
Melliès, P.-A., Tabareau, N. and Tasson, C. (2009). An explicit formula for the free exponential modality of linear logic. In: Proceedings of ICALP 247–260.Google Scholar
Pellissier, L. (2014). Another Formula for the Free Exponential Modality in Linear Logic. Mémoire de Master 2, ENS Cachan.Google Scholar
Révész, G. E. (1992). A list-oriented extension of the lambda-calculus satisfying the Church–Rosser theorem. Theoretical Computer Science 93 (1) 75–89.Google Scholar
Rodenburg, P. H. (1998). Termination and confluence in infinitary term rewriting. Journal of Symbolic Logic 63 (4) 1286–1296.Google Scholar
Terese (2003). Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science volume 55, Cambridge University Press.Google Scholar
Terui, K. (2011). Computational ludics. Theoretical Computer Science 412 (20) 2048–2071.Google Scholar
Vial, P. (2014). Structures uniformes en lambda-calcul polyadique affine. Mémoire de Master 2, Université Paris 7.Google Scholar
Vollmer, H. (1999). Introduction to Circuit Complexity - A Uniform Approach, Texts in Theoretical Computer Science, Springer.Google Scholar