## AI helps you reading Science

## AI Insight

AI extracts a summary of this paper

Weibo:

# Context semantics, linear logic, and computational complexity

logic in computer science, no. 4 (2009): ArticleNo.25-ArticleNo.25

EI

Full Text

Weibo

Keywords

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...More

Code:

Data:

Introduction

- Linear logic has always been claimed to be resource-conscious: structural rules are applicable only when the involved formulas are modal, i.e. in the form !A.
- The weight WG of a proof-net G will be defined from the context semantics of G following two ideas: The cost of a given box inside G is the number of times it can possibly be copied during normalization; The weight of G is the sum of costs of boxes inside G, where boxes that are inside other boxes are possibly counted more than once.
- In Section 3, context semantics is defined and some examples of proof-nets are presented, together with their interpretation.

Highlights

- Linear logic has always been claimed to be resource-conscious: structural rules are applicable only when the involved formulas are modal, i.e. in the form !A
- Completely forbidding duplication highlights strong relations between proofs and boolean circuits [20]. These results demonstrate the relevance of linear logic in implicit computational complexity, where the aim is obtaining machineindependent, logic-based characterization of complexity classes
- Context semantics and the geometry of interaction have been used to prove the correctness of optimal reduction algorithms [14] and in the design of sequential and parallel interpreters for the lambda calculus [17, 18]
- A class of proof-nets which are not just strongly normalizing but normalizable in elementary time can still be captured in the geometry of interaction framework, as suggested by Baillot and Pedicini [3]
- The usual measure based on the length of regular paths cannot be used, since there are proof-nets which can be normalized in polynomial time but whose regular paths have exponential length
- The weight WG of a proof-net G will be defined from the context semantics of G following two ideas: The cost of a given box inside G is the number of times it can possibly be copied during normalization; The weight of G is the sum of costs of boxes inside G, where boxes that are inside other boxes are possibly counted more than once

Results

- The authors are ready to define the context semantics for a proof-net G.
- Context semantics can be defined on sharing graphs as well, proof-nets have been considered here.
- The authors define some proof-nets together with observations about how context-semantics reflects the complexity of normalization.
- Consider a proof-net G, an edge e 2 BG such that @(e) = 0 and let H be the box whose conclusion is e.
- Any proof-net G satisfying the conditions of Lemma 4 has strictly positive weights, WG = 0.
- Lemma 6 gives them enough information to establish strong correspondences between TG, WG and the number of steps necessary to rewrite G to normal form: Proposition 1 (Positive Weights, Absense of Cycles and Monotonicity) Let G be a proof-net.
- The following theorem holds: Theorem 2 Let G be a proof-net.
- This has very interesting consequences: for example, a family G of proof-nets can be normalized in polynomial time iff there is a polynomial p such that WG p(jGj) for every G 2 G .
- This observation can be slightly generalized into the following result: Proposition 2 (Subtree Property) Suppose t is a standard exponential signature.
- The intuitive idea behind the subtree property is the following: whenever t is a copy of e under U and U is canonical for e, the exponenial signature t must be completely “consumed” along the canonical path leading from (e; U; t; +) to a final context C.

Conclusion

- This restriction enforces the following property at the semantic level: Lemma 8 (Stratification) Let G be a ELL proof-net.
- The second inequality is satisfied, because there are at most 2jGj+1 exponential signatures with length at most jGj. If @(e) > 0, the authors can observe that canonical sequences for @(e) are in the form V t, where V is canonical for G(e) and t is a copy for G(e) under V .
- The authors define a context semantics for linear logic proof-nets, showing it gives precise quantitative information on the dynamics of normalization.

- Table1: Rewrite Rules for Vertices R(, L(,R , L , R8, L8 e
- Table2: Rewrite Rules for Vertices X, D, N , L! and R!

Funding

- The author is partially supported by PRIN project FOLLIA (2004) and ANR project NOCOST (2005)

Reference

- A. Asperti and S. Guerrini. The optimal implementation of functional programming languages. Cambridge University Press, 1998.
- A. Asperti and L. Roversi. Intuitionistic light affine logic. ACM Transactions on Computational Logic, 3(1):137–175, 2002.
- P. Baillot and M. Pedicini. Elementary complexity and geometry of interaction. Fundamenta Informaticae, 45(1-2):1–31, 2001.
- U. Dal Lago. The geometry of linear higher-order recursion. In Proc. 20th Annual Symposium on Logic in Computer Science, pages 366–375. IEEE Computer Society, 2005.
- U. Dal Lago. Context semantics, linear logic and computational complexity. In Proc. 21st Annual Symposium on Logic in Computer Science, pages 169–178. IEEE Computer Society, 2006.
- V. Danos and J.-B. Joinet. Linear logic and elementary time. Information and Computation, 183(1):123–137, 2003.
- V. Danos and L. Regnier. Proof-nets and Hilbert space. In J.-Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, pages 307–328. Cambridge University Press, 1995.
- V. Danos and L. Regnier. Reversible, irreversible and optimal lambda-machines. Theoretical Computer Science, 227(1-2):79–97, 1999.
- J.-Y. Girard. Geometry of interaction 2: deadlock-free algorithms. In Proc. Conference on Computer Logic, volume 417 of LNCS, pages 76–93, 1988.
- J.-Y. Girard. Geometry of interaction 1: interpretation of system F. In Proc. Logic Colloquium ’88, pages 221–260, 1989. Lecture Notes in Pure and Applied Mathematics, pages 97–124. Marcel Dekker, New York, 1995.
- [12] J.-Y. Girard. Light linear logic. Information and Computation, 143(2):175–204, 1998.
- [13] J.-Y. Girard, A. Scedrov, and P. J. Scott. Bounded linear logic: A modular approach to polynomial-time computability. Theoretical Computer Science, 97(1):1–66, 1992.
- [14] G. Gonthier, M. Abadi, and J.-J. Levy. The geometry of optimal lambda reduction. In Proc. 12th ACM Symposium on Principles of Programming Languages, pages 15–26, 1992.
- [15] G. Gonthier, M. Abadi, and J.-J. Levy. Linear logic without boxes. In Proc. 7th Annual Symposium on Logic in Computer Science, pages 223–234, 1992.
- [16] Y. Lafont. Soft linear logic and polynomial time. Theoretical Computer Science, 318:163–180, 2004. Conference on Typed Lambda Calculi and Applications, pages 385–399, 2001.
- Computer Science, pages 209–220, 2001.
- [20] K. Terui. Proof nets and boolean circuits. In Proc. 7th Annual Symposium on Logic in Computer Science, pages 182–191, 2004.

Tags

Comments

数据免责声明

页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果，我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问，可以通过电子邮件方式联系我们：report@aminer.cn