Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Deducibility in the full Lambek calculus with weakening is HAck-complete

Vitor Greati, Revantha Ramanayake

Abstract

We prove that the problem of deciding the consequence relation of the full Lambek calculus with weakening is complete for the class HAck of hyper-Ackermannian problems (i.e., level F_ω^ω of the ordinal-indexed hierarchy of fast-growing complexity classes). Provability was already known to be PSPACE-complete. We prove that deducibility is HAck-complete even for the multiplicative fragment. Lower bounds are proved via a novel reduction from reachability in lossy channel systems and the upper bounds are obtained by combining structural proof theory (forward proof search over sequent calculi) and well-quasi-order theory (length theorems for Higman's Lemma).

Deducibility in the full Lambek calculus with weakening is HAck-complete

Abstract

We prove that the problem of deciding the consequence relation of the full Lambek calculus with weakening is complete for the class HAck of hyper-Ackermannian problems (i.e., level F_ω^ω of the ordinal-indexed hierarchy of fast-growing complexity classes). Provability was already known to be PSPACE-complete. We prove that deducibility is HAck-complete even for the multiplicative fragment. Lower bounds are proved via a novel reduction from reachability in lossy channel systems and the upper bounds are obtained by combining structural proof theory (forward proof search over sequent calculi) and well-quasi-order theory (length theorems for Higman's Lemma).
Paper Structure (18 sections, 2 equations, 1 figure, 1 table)

This paper contains 18 sections, 2 equations, 1 figure, 1 table.

Table of Contents

  1. Introduction
  2. An overview of the lower bound argument
  3. The upper bound argument
  4. Contributions
  5. Noncommutative substructural logics with weakening
  6. Hyper-Ackermannian lower bounds
  7. Lossy channel systems
  8. Encoding reachability in LCSs into sequent-deducibility
  9. Hyper-Ackermannian upper bounds
  10. Just enough on well-quasi-order theory
  11. A well-quasi-order over sequents based on weakening
  12. Decision procedure for amenable sequent calculi
  13. Complexity analysis
  14. Final considerations
  15. Complexity of the word problem in integral FL-algebras
  16. ...and 3 more sections

Figures (1)

  • Figure 1: The sequent calculus $\mathbf{FL}_{\mathbf{w}}^{}$.

Theorems & Definitions (14)

  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • ...and 4 more