Workshop on Proof Theory and Computability Theory 2012, Feb. 21, 2012, Tokyo, Japan.
Order-theoretic Approaches to Computational
Complexity
– Towards more natural characterisations
Naohi Eguchi
Mathematical Institute, Tohoku University
Introduction
Introduction
✞ ✝
Aim: New characterisations of compt. complexity classes.☎ ✆
Introduction How to approach to comput. compl. Composition or recursion produces functions that
are not computable only using realistic resources. (Composition) f (⃗x) = h(⃗g(⃗x))
(Primitive recursion)
f(0, ⃗x) = g(⃗x),
f(S(y), ⃗x) = h(y, ⃗x, f (y, ⃗x)). It is natural to restrict them to approach to computational complexity.
Introduction Classical approach Classical approach: Explicit bounding.
(Composition) f (⃗x) = h(⃗g(⃗x)) (Bounded recursion)
f(0, ⃗x) = g(⃗x),
f (S(y), ⃗x) = h(y, ⃗x, f (y, ⃗x)), f (y, ⃗x) ≤ p(y, ⃗x).
☛
✡
✟
✠
Polynomially-bounded recursion captures the polytime functions. (A. Cobham 1964)
Introduction Alternative approach Alternative: Splitting into predicative; impredicative. (Predicative composition): (f : N × N → N )
f(x; α) = h(x; g(x; α)).
(Predicative recursion) (f : N × N × N → N ) f(0, x; α) = g(x; α),
f (S(y), x; α) = h(y, x; α, f (y, x; α)).
☛
✡
✟
✠
Predicative recursion captures the polytime func- tions. (D. Leivant ’91, S. Bellantoni & S. Cook ’92)
Outline
1. A path order is a w.f. relation on a set of terms. 2. Classical results: Multiset Path Order (D. Hofbauer
’90). Lexicographic Path Order (A. Weiermann ’95).
3. A syntactic restriction POP* of MPO is complete for P functions. (M. Avanzini and G. Moser 2008)
4. A syntactic restriction EPO* of LPO is complete for EXP functions. (Avanzini, E. and Moser 2011)
5. A new restriction sPOP* of MPO is complete for P functions. (M. Avanzini, E. N. and G. Moser)
Contents 1. Complexity classes
2. Term rewrite systems
3. Order-theoretic approaches
4. Path orders for complexity classes 5. New path order for P functions
6. Conclusion
Complexity classes Time-, Space complexity Definition Let T : N → N be a function.
FTIME(T ) := ∪k{f : Nk → N | f ( ⃗m) is computable by a determin- istic Turing machine in a step bounded by T (max | ⃗m|)}. FSPACE(T ) := ∪k{f : Nk → N | f ( ⃗m) is
computable by a determinis- tic Turing machine in a space bounded by T (max | ⃗m|)}.
Complexity classes FP, FPS and FEXP 1. FP := ∪k FTIME(O(λn.nk)).
2. FEXP := ∪k FTIME(λn.2O(nk)). 3. FPS := ∪k FSPACE(λn.O(nk)).
Complexity classes FP, FPS and FEXP 1. FP := ∪k FTIME(O(λn.nk)).
2. FEXP := ∪k FTIME(λn.2O(nk)). 3. FPS := ∪k FSPACE(λn.O(nk)).
Well known:
1. FP ⊆ FPS ⊆ FEXP and FP ̸= FEXP. 2. FP = FPNP ⇔ P = NP.
3. FP = FPS ⇔ P = PSPACE. Open:
• P ̸= PSPACE or PSPACE ̸= EXP.
Contents 1. Complexity classes
2. Term rewrite systems
3. Order-theoretic approaches
4. Path orders for complexity classes 5. New path order for P functions
6. Conclusion
Term rewrite systems What’s term rewriting Term rewriting is an abstract model of computations based on equational calculi.
1. A term rewrite system (TRS for short) R is a set of rewriting rules of the form t → s.
t → s ∈ R =⇒ tθ→Rsθ (θ: a substitution)
2. A subterm is successively replaced by an equal term until no further rewriting is possible.
t→Rs =⇒ f (· · · t · · · )→Rf (· · · s · · · )
Term rewrite systems Example 1
Defining equations for addition Eadd:
Eadd
0 + n = n
(m + 1) + n = (m + n) + 1
Term rewrite systems Example 1
Defining equations for addition Eadd:
Eadd
0 + n = n
(m + 1) + n = (m + n) + 1
The corresponding TRS Radd:
Radd
add(0, y) → y
add(s(x), y) → s(add(x, y))
where the signature Fadd for Radd is defined by Fadd = {0, s, add}.
Term rewrite systems Example 2
Defining equations for multiplication Emul := Eadd ∪ E:
E
0 · n = 0
(m + 1) · n = n + (m · n)
Term rewrite systems Example 2
Defining equations for multiplication Emul := Eadd ∪ E:
E
0 · n = 0
(m + 1) · n = n + (m · n)
The corresponding TRS Rmul := Radd ∪ R:
R
mul(0, y) → 0
mul(s(x), y) → add(y, mul(x, y))
where Fmul := Fadd ∪ {mul} = {0, s, add, mul}.
Term rewrite systems Example 3
Defining equations for the Fibonacci numbers
Efib a0 = a1 = 1
an+2 = an+1 + an (n ≥ 0)
Term rewrite systems Example 3
Defining equations for the Fibonacci numbers
Efib a0 = a1 = 1
an+2 = an+1 + an (n ≥ 0)
The corresponding TRS Rfib:
Rfib dfib(0, y) → s(y) dfib(s(0), y) → s(y)
dfib(s(s(x)), y) → dfib(s(x), dfib(x, y)) fib(x) → dfib(x, 0)
where Ffib := {0, s, dfib, fib}.
dfib(n, m) = an + m and hence fib(n) = an.
Term rewrite systems Example 4
Defining equations for the Ackermann function:
EA A(0, n) = n + 1
A(m + 1, 0) = A(m, 1)
A(m + 1, n + 1) = A(m, A(m + 1, n))
Term rewrite systems Example 4
Defining equations for the Ackermann function:
EA A(0, n) = n + 1
A(m + 1, 0) = A(m, 1)
A(m + 1, n + 1) = A(m, A(m + 1, n))
The corresponding TRS RA:
Rfib A(0, y) → s(y)
A(s(x), 0) → A(x, s(0))
A(s(x), s(y)) → A(x, A(s(x), y))
where FA := {0, s, A}.
Contents 1. Complexity classes
2. Term rewrite systems
3. Order-theoretic approaches
4. Path orders for complexity classes 5. New path order for P functions
6. Conclusion
Order-theoretic approaches Basic ideas Rough correspondence:
Let f be defined by Ef (or equivalently by Rf ). Time-complexity of
f defined by Ef
≈ the maximal length of Rf -rewriting se- quences
Space-complexity of f defined by Ef
≈ the maximal size of terms appearing in Rf -rewriting sequences
Order-theoretic approaches Path orders Definition A TRS R is terminating if there is no infinite rewriting sequence t0 →R t1 →R · · · .
A TRS R is terminating if there exists a monotone well-founded relation (path order) > such that
t →R s ⇒ t > s.
• Radd, Rmul: contained in Multiset Path Order (MPO) and Lexicographic Path Order (LPO).
• Rfib, RA: not contained in MPO but contained in LPO.
Order-theoretic approaches Definition of MPO Let >F : a partial order on the signature F.
Then t >MPO s iff one of the following holds: 1. t ✄ s. (s is a proper subterm of t.)
2. t = f (t1, . . . , tl), s = g(s1, . . . , sn), f >F g and t >MPO sj for ∀j ∈ {1, . . . , n}.
3. t = f (t1, . . . , tl), s = f (s1, . . . , sl) and
∃π : {1, . . . , l} → {1, . . . , l}: permutation s.t. { tj ⩾MPO sπ(j) for ∀j ∈ {1, . . . , l},
tj0 >MPO sπ(j0) for ∃j0 ∈ {1, . . . , l}.
Order-theoretic approaches Definition of LPO Let >F : a partial order on the signature F.
Then t >LPO s iff one of the following holds: 1. t ✄ s. (s is a proper subterm of t.)
2. t = f (t1, . . . , tl), s = g(s1, . . . , sn), f >F g and t >LPO sj for ∀j ∈ {1, . . . , n}.
3. t = f (t1, . . . , tl), s = f (s1, . . . , sl) and
∃i ≤ l s.t.
tj = sj if 1 ≤ j < i, tj >LPO sj if j = i
t >LPO sj if i < j < l.
Order-theoretic approaches MPO, LPO (completeness) Multiset Path Order MPO is designed so that
• every primitive recursive function is representable as a TRS contained in MPO.
(In this talk we only consider of a weak form of MPO with product comparison)
Lexicographic Path Order LPO is designed so that
• every multiply recursive function is representable as a TRS contained in LPO.
Order-theoretic approaches MPO, LPO (soundness) Theorem （Hofbauer, 1990） If a TRS R is
contained in MPO, then the maximal length of rewriting sequences w.r.t. →R is bounded by a
primitive recursive function (measured by the length of the starting term).
Theorem （Weiermann, 1995） If a TRS R is contained in LPO, then the maximal length of rewriting sequences w.r.t. →R is bounded by a multiply recursive function.
Order-theoretic approaches MPO, LPO (provability) Proposition
1. ∀f : primitive recursive ∃MPO s.t. I∆0(exp) ⊢
“MPO is well-founded′′ → “∀⃗x ∃yf (⃗x) = y′′. 2. ∀f : multiply recursive ∃LPO s.t. I∆0(exp) ⊢
“LPO is well-founded′′ → “∀⃗x ∃yf (⃗x) = y′′. Fact （Buchholz, 1995）
1. ∀MPO, IΣ1 ⊢ “MPO is well-founded′′ 2. ∀LPO, IΣ2 ⊢ “LPO is well-founded′′
Contents 1. Complexity classes
2. Term rewrite systems
3. Order-theoretic approaches
4. Path orders for complexity classes 5. New path order for P functions
6. Conclusion
Path orders for complexity classes How to approach Our approach is based on the following observations.
• Huge finite numbers behave like infinite ones in weak settings. (cf. Observation by R. Parikh ’71)
• Exponential is a second order or infinitary notion in weak theories. (cf. Two-sorted theories of
bounded arithmetic by S. Cook, P. Nguyen et al.)
• Primitive recursion contains impredicative
contexts. (Similar observations by E. Nelson ’86)
Path orders for complexity classes Predicative recursion Split: types of naturals into N (predicative) and N (impredicative), or even more N0, N1, . . . .
(Predicative composition): (f : ⃗N × ⃗N → N )
f(⃗x; ⃗α) = h(xi1 , . . . , xik ; g(⃗x; ⃗α)). (Predicative recursion) (f : N × ⃗N × ⃗N → N )
f(0, ⃗x; ⃗α) = g(⃗x; ⃗α),
f (S(y), ⃗x; ⃗α) = h(y, ⃗x; ⃗α, f (y, x; α)). This reflects that the result of composition or primitive recursion is not predicative.
Path orders for complexity classes Restricting MPO
✛
✚
✘
✙
The FP functions coincide with
functions of type ⃗N → N generated from ele- mentary initial functions by predicative composi- tion and predicative recursion (over binary words).
(S. Bellantoni & S. Cook ’92)
✓
✒
✏
✑
A syntactic restriction POP* of MPO that is com- plete for the FP functions.
(M. Avanzini & G. Moser ’08)
Path orders for complexity classes Restricting LPO
✛
✚
✘
✙
The FEXP functions coincide with
functions of type ⃗N → N generated from the same initial functions by predicative composi- tion and predicative nested recursion (over binary words). (T. Arai & N. E. ’09)
✓
✒
✏
✑
A syntactic restriction EPO* of LPO that is com- plete for the FEXP functions.
(M. Avanzini, N. E. & G. Moser ’11)
Contents 1. Complexity classes
2. Term rewrite systems
3. Order-theoretic approaches
4. Path orders for complexity classes 5. New path order for P functions
6. Conclusion
New path order for P functions Introducing sPOP* Introduce: another syntactic restriction small
Polynomial Path Order (sPOP*) of MPO s.t.
• sPOP* is weaker than POP* in practice.
• However every FP function is representable as a TRS contained in sPOP*. (Completeness) Advantage: we can read off degrees of polynomial
bounds on lengths of rewriting sequences TRSs contained in sPOP*.
New path order for P functions Definition of MPO Let >F : a partial order on the signature F.
Then t >MPO s iff one of the following holds: 1. t ✄ s. (s is a proper subterm of t.)
2. t = f (t1, . . . , tl), s = g(s1, . . . , sn), f >F g and t >MPO sj for ∀j ∈ {1, . . . , n}.
3. t = f (t1, . . . , tl), s = f (s1, . . . , sl) and
∃π : {1, . . . , l} → {1, . . . , l}: permutation s.t. { tj ⩾MPO sπ(j) for ∀j ∈ {1, . . . , l},
tj0 >MPO sπ(j0) for ∃j0 ∈ {1, . . . , l}.
New path order for P functions Definition of sPOP* f(t1, . . . , tk;tk+1, . . . , tk+l) = t >sPOP∗ s iff
1. t ✄ s. (s is a proper subterm of t.)
2. s = g(s1, . . . , sm;sm+1, . . . , sm+n), f >F g t ✄ sj for ∀j ∈ {1, . . . , m}, and
t >sPOP∗ sj for ∀j ∈ {m + 1, . . . , m + n}. 3. s = f (s1, . . . , sk;sk+1, . . . , sk+l) and ∃π s.t.
tj ☎ sπ(j) for ∀j ∈ {1, . . . , k}, tj0 ✄ sπ(j0) for ∃j0 ∈ {1, . . . , k},
tj ⩾sPOP∗ sπ(j) for ∀j ∈ {k + 1, . . . , k + l}.
New path order for P functions Soundness of sPOP* Theorem （Avanzini-E.-Moser, submitted） If a
TRS R is contained in sPOP* using recursion up to depth d, then for any argument normalised term
f(⃗t), the maximal length of (innermost) rewriting sequences starting with f (⃗t) in R is bounded by a polynomial of degree d in the sum of the sizes of ⃗t. Corollary If a confluent TRS R is contained in
sPOP*, then the function defined by R is in FP.
New path order for P functions Example 1 (MPO) TRS Radd for addition:
Eadd
0 + n = n
(m + 1) + n = (m + n) + 1 Radd
add(0, y) → y
add(s(x), y) → s(add(x, y))
Define >Fadd by add >Fadd 0, s.
Then Radd is contained in MPO induced by >Fadd .
New path order for P functions Example 1 (sPOP*) TRS Radd for addition:
Eadd
0 + n = n
(m + 1) + n = (m + n) + 1 Radd
add(0;y) → y
add(s(;x);y) → s(;add(x;y))
Define >Fadd by add >Fadd 0, s.
Then Radd is contained in sPOP* induced by >Fadd with recursion up to depth 1.
New path order for P functions Example 2 (MPO) TRS Rmul := Radd ∪ R for multiplication:
E
0 · n = 0
(m + 1) · n = n + (m · n) R
mul(0, y) → 0
mul(s(x), y) → add(y, mul(x, y))
Define >Fmul by mul >Fmul add >Fmul 0, s.
Then Rmul is contained in MPO induced by >Fmul.
New path order for P functions Example 2 (sPOP*) TRS Rmul := Radd ∪ R for multiplication:
E
0 · n = 0
(m + 1) · n = n + (m · n) R
mul(0, y;) → 0
mul(s(;x), y;) → add(y;mul(x, y;))
Define >Fmul by mul >Fmul add >Fmul 0, s.
Then Rmul is contained in sPOP* induced by >Fmul with recursion up to depth 2.
Contents 1. Complexity classes
2. Term rewrite systems
3. Order-theoretic approaches
4. Path orders for complexity classes 5. New path order for P functions
6. Conclusion
Conclusion
Summary: Introducing syntactic restrictions of MPO or LPO based on predicative recursion that complete for complexity classes.
Conjecture: f is representable as a confluent (constructor) TRS contained in sPOP* using
recursion up to depth d iff f is computable by a RM in a step bounded by a polynomial of degree d.
Future work: What is the minimal theory T such that T ⊢ “sPOP* is well-founded′′?
References
• “Complexity Analysis by Rewriting” M. Avanzini and G. Moser, in Proc. 9th FLOPS, 2008.
• “A Path Order for Rewrite Systems that Compute Exponential Time Functions” M. Avanzini, N. Eguchi and G. Moser, in Proc. of 22nd RTA, 2011.
• “A New Order-theoretic Characterisation of the Polytime Computable Functions” M. Avanzini, N. Eguchi and G. Moser, CoRR, cs/CC/1201.2553, 2012.
References
• “Complexity Analysis by Rewriting” M. Avanzini and G. Moser, in Proc. 9th FLOPS, 2008.
• “A Path Order for Rewrite Systems that Compute Exponential Time Functions” M. Avanzini, N. Eguchi and G. Moser, in Proc. of 22nd RTA, 2011.
• “A New Order-theoretic Characterisation of the Polytime Computable Functions” M. Avanzini, N. Eguchi and G. Moser, CoRR, cs/CC/1201.2553, 2012.
Thank you for your attention!
