Bounded linear logic: A modular approach to polynomial time computability. Extended abstract

MaRDI QIDQ4035310zbMATH OpenFDO

Authors Jean-Yves Girard, Andre Scedrov, Philip Scott

Publication date 18 May 1993

zbMATH Keywords

bounded exclamation markbounded linear logicbounded storagecomputable functioninteractive behaviour of algorithmspolynomial-time functionsstructural rulestyping

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Other nonclassical logic (03B60) Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Real polynomials: analytic properties, etc. (26C05) Analysis of algorithms and problem complexity (68Q25)

Review text

[For the entire collection see Zbl 0753.00018.] The article deals with typing as a way of describing the interactive behaviour of algorithms. It proposes Bounded Linear Logic (BLL) to represent successfully the dynamics of typing systems and restore the contraction rule. BLL is intermediate between second-order Rudimentary Linear Logic (RLL) and full second-order Linear Logic (LL) with respect to the representation of polynomial-time functions. It considers the bounded storage concept and the corresponding bounded exclamation mark as a new kind of typing instructions. The syntax of BLL is considered as a possible framework for a modular calculus of efficient algorithms. The paper presents brief descriptions of relevant results from RLL and LL and compares them with corresponding concepts and facts for BLL (e.g., rules for Storage, Weakening, Contraction, Dereliction). The main results are presented as sequence of theorems and lemmas with illustrating examples provided. The following conclusions are drawn: a) BLL normalizes in polynomial time. b) Every polynomial-time computable function can be typed in BLL. Topics and directions of further investigations based on BLL are outlined.

Recommendations

• Bounded linear logic: A modular approach to polynomial-time computability
• Polynomial time in untyped elementary linear logic
• Linear logic by levels and bounded time complexity
• Realizability models for BLL-like languages
• Linear logic and polynomial time

Cited in

(12)

• Bounded linear logic: A modular approach to polynomial-time computability
• Full intuitionistic linear logic
• Realizability models for BLL-like languages
• Algorithmically broad languages for polynomial time and space
• An arithmetic for polynomial-time computation
• Computing on structures
• An analysis of the Core-ML language: expressive power and type reconstruction
• Polynomial and Exponential Bounded Logic Programs with Function Symbols: Some New Decidable Classes
• Bounded linear logic, revisited
• Bounded Linear Logic, Revisited
• Computation models and function algebras
• Tropical mathematics and the lambda-calculus I: metric and differential analysis of effectful programs

This page was built for publication: Bounded linear logic: A modular approach to polynomial time computability. Extended abstract

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