Elementary complexity and geometry of interaction
The aim of the paper is to define a setting as large, and simple, as possible for elementarily bounded computations. An algebra of clauses is presented along the lines of \textit{J.-Y. Girard}'s paper [in: J.-Y. Girard et al. (eds.), Advances in linear logic. Lond. Math. Soc. Lect. Note Ser. 222, 329-389 (1995; Zbl 0828.03027)] with a kind of depth-preservation property analogous to that of Elementary Linear Logic (ELL). Execution is defined through resolution and the operators are certain sets of clauses. In addition to usual execution formulas weak execution is defined which amounts to giving up the computation of certain products of execution. Weak execution coincides with usual execution for operators coming from proof-nets. NEWLINENEWLINENEWLINESize and depth are defined for general operators. The main result being that weak execution always terminates and that when the depth is fixed, the number of steps of the computation is bounded by a function of the size of the program which is elementary, that is, a bound can be computed in advance, provided that size and depth are known. Therefore the intrinsic elementary bound obtained in ELL by logical means has been extended to a semantic setting.
- scientific article; zbMATH DE number 1342271
- scientific article; zbMATH DE number 1231531
- Linear logic by levels and bounded time complexity
- Realizability models and implicit complexity
- scientific article; zbMATH DE number 2182488
- scientific article; zbMATH DE number 922617
- scientific article; zbMATH DE number 1424049
- Propositional computability logic II
- The addition of bounded quantification and partial functions to a computational logic and its theorem prover
- Light types for polynomial time computation in lambda calculus
- Linear logic and elementary time
- Paths-based criteria and application to linear logic subsystems characterizing polynomial time
- Stratified coherence spaces: A denotational semantics for light linear logic
- On the expressivity of elementary linear logic: characterizing Ptime and an exponential time hierarchy
- An abstract approach to stratification in linear logic
- A structural approach to reversible computation
- Logarithmic space and permutations
- Unary resolution: characterizing \textsc{Ptime}
- Memoryful geometry of interaction. II: Recursion and adequacy
- Interaction graphs: graphings
- On paths-based criteria for polynomial time complexity in proof-nets
- Dynamics of complexity of intersections
- scientific article; zbMATH DE number 1342271 (Why is no real title available?)
- scientific article; zbMATH DE number 6917940 (Why is no real title available?)
- A correspondence between maximal abelian sub-algebras and linear logic fragments
- Implicit computation complexity in higher-order programming languages
- Light logics and optimal reduction: completeness and complexity
- Principal types as partial involutions
- Two views on unification: terms as strategies
This page was built for publication: Elementary complexity and geometry of interaction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2708316)
