Context semantics, linear logic, and computational complexity

DOI10.1145/1555746.1555749zbMATH Open1351.03061arXivcs/0510092OpenAlexW2169724594WikidataQ130874238 ScholiaQ130874238MaRDI QIDQ2946582FDOQ2946582

Authors: Ugo Dal Lago 

Publication date: 17 September 2015

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

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 number of steps to normal form (for certain reduction strategies). 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.

Full work available at URL: https://arxiv.org/abs/cs/0510092

Recommendations

• scientific article; zbMATH DE number 1948160
• On context semantics and interaction nets
• Quantitative Game Semantics for Linear Logic
• A semantic account of strong normalization in linear logic
• Linear logic and polynomial time

zbMATH Keywords

implicit computational complexitylinear logicgeometry of interaction

Mathematics Subject Classification ID

Complexity of proofs (03F20) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Complexity of computation (including implicit computational complexity) (03D15)

Cited In (14)

• Towards a geometry of recursion
• Polynomial time in untyped elementary linear logic
• Title not available (Why is that?)
• Context-Sensitive Languages, Rational Graphs and Determinism
• The computational complexity of ideal semantics
• Linear dependent types in a call-by-value scenario
• Implicit computation complexity in higher-order programming languages
• Characterizing polynomial and exponential complexity classes in elementary lambda-calculus
• Paths-based criteria and application to linear logic subsystems characterizing polynomial time
• On paths-based criteria for polynomial time complexity in proof-nets
• Is the Optimal Implementation Inefficient? Elementarily Not
• Quantitative Game Semantics for Linear Logic
• Geometry of resource interaction and Taylor-Ehrhard-Regnier expansion: \textit{a minimalist approach}
• Geometry of resource interaction -- \textit{a minimalist approach}

This page was built for publication: Context semantics, linear logic, and computational complexity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946582)