Context semantics, linear logic, and computational complexity

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Context semantics, linear logic, and computational complexity

Full text

Pdf (885 KB)

Source

ACM Transactions on Computational Logic (TOCL) archive
Volume 10 , Issue 4 (August 2009) table of contents

Article No. 25

Year of Publication: 2009

ISSN:1529-3785

Author

Ugo Dal Lago

Università di Bologna, Bologna, Italy

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 11, Downloads (12 Months): 86, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1555746.1555749 What is a DOI?

ABSTRACT

We show that context semantics can be fruitfully applied to the quantitative analysis of proof normalization in linear logic. In particular, context semantics lets us define the weight of a proof-net as a measure of its inherent complexity: it is both an upper bound to normalization time (modulo a polynomial overhead, independently on the reduction strategy) and a lower bound to the amount of resources needed to compute the normal form. Weights are then exploited in proving strong soundness theorems for various subsystems of linear logic, namely elementary linear logic, soft linear logic, and light linear logic.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Andrea Asperti , Stefano Guerrini, The optimal implementation of functional programming languages, Cambridge University Press, New York, NY, 1999
	2	Andrea Asperti , Luca Roversi, Intuitionistic Light Affine Logic, ACM Transactions on Computational Logic (TOCL), v.3 n.1, p.137-175, January 2002 [doi>10.1145/504077.504081]
	3	Patrick Baillot , Paolo Coppola , Ugo Dal Lago, Light Logics and Optimal Reduction: Completeness and Complexity, Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, p.421-430, July 10-14, 2007 [doi>10.1109/LICS.2007.27]
	4	Patrick Baillot , Marco Pedicini, Elementary Complexity and Geometry of Interaction, Fundamenta Informaticae, v.45 n.1-2, p.1-31, January 2001
	5	Ugo Dal Lago, The Geometry of Linear Higher-Order Recursion, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, p.366-375, June 26-29, 2005 [doi>10.1109/LICS.2005.52]
	6	Ugo Dal Lago, Context Semantics, Linear Logic and Computational Complexity, Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, p.169-178, August 12-15, 2006 [doi>10.1109/LICS.2006.21]
	7	Vincent Danos , Jean-Baptiste Joinet, Linear logic and elementary time, Information and Computation, v.183 n.1, p.123-137, May 25, 2003 [doi>10.1016/S0890-5401(03)00010-5]
	8	V. Danos , L. Regnier, Proof-nets and the Hilbert space, Proceedings of the workshop on Advances in linear logic, p.307-328, June 1995
	9	Vincent Danos , Laurent Reginer, Reversible, irreversible and optimal &lgr;-machines, Theoretical Computer Science, v.227 n.1-2, p.79-97, Oct. 1, 1999 [doi>10.1016/S0304-3975(99)00049-3]
	10	Jean-Yves Girard, Geometry of interaction 2: deadlock-free algorithms, Proceedings of the International Conference on Computer Logic, p.76-93, December 01, 1988
	11	Girard, J.-Y. 1989. Geometry of interaction 1: Interpretation of system F. In Proceedings of the Logic Colloquium '88. 221--260.
	12	Girard, J.-Y. 1995. Proof-nets: The parallel syntax for proof-theory. In Logic and Algebra, A. Ursini and P. Agliano, Eds. Lecture Notes in Pure and Applied Mathematics, vol. 180. Marcel Dekker, New York, 97--124.
	13	Jean-Yves Girard, Light linear logic, Information and Computation, v.143 n.2, p.175-204, June 15, 1998 [doi>10.1006/inco.1998.2700]
	14	Jean-Yves Girard , Andre Scedrov , Philip J. Scott, Bounded linear logic: a modular approach to polynomial-time computability, Theoretical Computer Science, v.97 n.1, p.1-66, April 20, 1992 [doi>10.1016/0304-3975(92)90386-T]
	15	Georges Gonthier , Martín Abadi , Jean-Jacques Lévy, The geometry of optimal lambda reduction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.15-26, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143172]
	16	Gonthier, G., Abadi, M., and Lévy, J.-J. 1992b. Linear logic without boxes. In Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 223--234.
	17	Yves Lafont, Soft linear logic and polynomial time, Theoretical Computer Science, v.318 n.1-2, p.163-180, June 2004 [doi>10.1016/j.tcs.2003.10.018]
	18	Ian Mackie, The geometry of interaction machine, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.198-208, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199483]
	19	Pinto, J. S. 2001. Parallel implementation models for the lambda-calculus using the geometry of interaction. In Proceedings of the 5th International Conference on Typed Lambda Calculi and Applications. 385--399.
	20	Terui, K. 2001. Light affine lambda calculus and polytime strong normalization. In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 209--220.
	21	Kazushige Terui, Proof Nets and Boolean Circuits, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, p.182-191, July 13-17, 2004 [doi>10.1109/LICS.2004.34]