Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

type-two polynomial time and restriced lookahead
Bruce Kapron and Florian Steinberg
INRIA

July 5, 2018

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

1

Second-order complexity theory

2

Oracle polynomial-time

3

Additional restrictions

4

Composition and decomposition

Composition and decomposition

Thx

Second-order complexity theory

Oracle polynomial-time

Oracle Turing machinesϕ ∈ B := Σ∗ → Σ∗

ϕ
c

ϕ(c)

Additional restrictions

Composition and decomposition

Thx

Second-order complexity theory

Oracle polynomial-time

Oracle Turing machinesϕ ∈ B := Σ∗ → Σ∗

ϕ
c

ϕ(c)
M

Additional restrictions

Composition and decomposition

Thx

Second-order complexity theory

Oracle polynomial-time

Oracle Turing machinesϕ ∈ B := Σ∗ → Σ∗

ϕ
c

ϕ(c)
M
b

Additional restrictions

Composition and decomposition

Thx

Second-order complexity theory

Oracle polynomial-time

Oracle Turing machinesϕ ∈ B := Σ∗ → Σ∗

ϕ
c

ϕ(c)
M
a

b

Additional restrictions

Composition and decomposition

Thx

Second-order complexity theory

Oracle polynomial-time

Oracle Turing machinesϕ ∈ B := Σ∗ → Σ∗

ϕ
c

ϕ(c)
M
a

b

Additional restrictions

Composition and decomposition

Thx

Second-order complexity theory

Oracle polynomial-time

Oracle Turing machinesϕ ∈ B := Σ∗ → Σ∗

ϕ
c

Mϕ
ϕ(c)
M

a

b

Additional restrictions

Composition and decomposition

Thx

Second-order complexity theory

Oracle polynomial-time

Oracle Turing machinesϕ ∈ B := Σ∗ → Σ∗

ϕ
c

Mϕ
ϕ(c)
M

a M ϕ (a)Additional restrictions

Composition and decomposition

Thx

Second-order complexity theory

Oracle polynomial-time

Oracle Turing machinesϕ ∈ B := Σ∗ → Σ∗
F : ⊆ B → B,ϕc

ϕ 7→ M ϕ

Mϕ
ϕ(c)
M

a M ϕ (a)Additional restrictions

Composition and decomposition

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Oracle Turing machinesϕ ∈ B := Σ∗ → Σ∗
F : ⊆ B → B,ϕc

ϕ 7→ M ϕ

Mϕ
ϕ(c)
M

a M ϕ (a)timeM (ϕ, a)Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Oracle Turing machinesϕ ∈ B := Σ∗ → Σ∗
F : ⊆ B → B,ϕc

ϕ 7→ M ϕ

Mϕ
ϕ(c)
M

a M ϕ (a)timeM (ϕ, a) ≤ T (. . . , |a|)Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Oracle Turing machinesϕ ∈ B := Σ∗ → Σ∗
F : ⊆ B → B,

timeM (ϕ, a) ≤ T (. . . , |a|)ϕ 7→ M ϕ|ϕ|(n) := max |ϕ(a)|,
|a|≤n

ϕ
c

Mϕ
ϕ(c)
M

a M ϕ (a)ThxSecond-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Oracle Turing machinesϕ ∈ B := Σ∗ → Σ∗
F : ⊆ B → B,

timeM (ϕ, a) ≤ T (|ϕ|, |a|)ϕ 7→ M ϕ|ϕ|(n) := max |ϕ(a)|,
|a|≤n

ϕ
c

Mϕ
ϕ(c)
M

a M ϕ (a)ThxSecond-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Thx

Oracle Turing machinesϕ ∈ B := Σ∗ → Σ∗
F : ⊆ B → B,

timeM (ϕ, a) ≤ T (|ϕ|, |a|)ϕ 7→ M ϕ|ϕ|(n) := max |ϕ(a)|,
|a|≤n

ϕ
c

Mϕ
ϕ(c)
M

a M ϕ (a)|ϕ| : N → N

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Thx

Oracle Turing machinesϕ ∈ B := Σ∗ → Σ∗
F : ⊆ B → B,

timeM (ϕ, a) ≤ T (|ϕ|, |a|)ϕ 7→ M ϕ|ϕ|(n) := max |ϕ(a)|,
|a|≤n

ϕ
c

Mϕ
ϕ(c)
M

a M ϕ (a)|ϕ| : N → N

Second-order polynomials...

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Thx

Oracle Turing machinesϕ ∈ B := Σ∗ → Σ∗
F : ⊆ B → B,

timeM (ϕ, a) ≤ T (|ϕ|, |a|)ϕ 7→ M ϕ|ϕ|(n) := max |ϕ(a)|,
|a|≤n

ϕ
c

Mϕ
ϕ(c)
M

a M ϕ (a)|ϕ| : N → N

Second-order polynomials...
Theorem
Closed under composition.

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Thx

Oracle Turing machinesϕ ∈ B := Σ∗ → Σ∗
F : ⊆ B → B,

timeM (ϕ, a) ≤ T (|ϕ|, |a|)ϕ 7→ M ϕ|ϕ|(n) := max |ϕ(a)|,
|a|≤n

ϕ
c

Mϕ
ϕ(c)
M

a M ϕ (a)|ϕ| : N → N

Second-order polynomials...
Theorem
Closed under composition.
Corollary
Preserves polynomial-time
computability.

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Comments
Original definition: bounded recursion scheme.

Composition and decomposition

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Comments
Original definition: bounded recursion scheme.
Theorem (Cook, Kapron, Urquart)
Coincides with the lambda closure of the polytime functions and alimited recursion operator.

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Comments
Original definition: bounded recursion scheme.
Theorem (Cook, Kapron, Urquart)
Coincides with the lambda closure of the polytime functions and alimited recursion operator.
Be carefull with resource bounded machines!

ThxSecond-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Comments
Original definition: bounded recursion scheme.
Theorem (Cook, Kapron, Urquart)
Coincides with the lambda closure of the polytime functions and alimited recursion operator.
Be carefull with resource bounded machines!
Theorem
The length function is notpolytime.

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Comments
Original definition: bounded recursion scheme.
Theorem (Cook, Kapron, Urquart)
Coincides with the lambda closure of the polytime functions and alimited recursion operator.
Be carefull with resource bounded machines!
Can not evaluate runningTheorem
times.
The length function is notpolytime.

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Comments
Original definition: bounded recursion scheme.
Theorem (Cook, Kapron, Urquart)
Coincides with the lambda closure of the polytime functions and alimited recursion operator.
Be carefull with resource bounded machines!
Can not evaluate runningTheorem
times.
The length function is notpolytime.

Clockability.

ThxSecond-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Comments
Original definition: bounded recursion scheme.
Theorem (Cook, Kapron, Urquart)
Coincides with the lambda closure of the polytime functions and alimited recursion operator.
Be carefull with resource bounded machines!
Can not evaluate runningTheorem
times.
The length function is notpolytime.
Theorem (Kawamura, S.)
Clocking is impossible.

Clockability.

ThxSecond-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Oracle polynomial-time
t : N → N is step-count
ϕ
ci

Mϕ
di
M

a M ϕ (a)ThxSecond-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Oracle polynomial-time
t : N → N is step-count if
ϕ
ci

Mϕ
di
M

a M ϕ (a)timeM (ϕ, a) ≤ t(mϕ,a ),Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Oracle polynomial-time
t : N → N is step-count if
ϕ
ci

Mϕ
di
M

a M ϕ (a)timeM (ϕ, a) ≤ t(mϕ,a ),
wheremϕ,a := max{|a|, |di |}.

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Oracle polynomial-time
t : N → N is step-count if
ϕ
ci

Mϕ
di
M

a M ϕ (a)timeM (ϕ, a) ≤ t(mϕ,a ),
wheremϕ,a := max{|a|, |di |}.

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Oracle polynomial-time
t : N → N is step-count if
ϕ
ci

Mϕ
di
M

timeM (ϕ, a) ≤ t(mϕ,a ),
wheremϕ,a := max{|a|, |di |}.

a M ϕ (a)Lemma
Step-count condition holds ineach step.

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Oracle polynomial-time
t : N → N is step-count if
ϕ
ci

Mϕ
di
M

timeM (ϕ, a) ≤ t(mϕ,a ),
wheremϕ,a := max{|a|, |di |}.

a M ϕ (a)Lemma
Step-count condition holds ineach step.
because: total.

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Oracle polynomial-time
t : N → N is step-count if
ϕ
ci

Mϕ
di
M

timeM (ϕ, a) ≤ t(mϕ,a ),
wheremϕ,a := max{|a|, |di |}.

a M ϕ (a)Theorem
Total operators havestep-counts.

Lemma
Step-count condition holds ineach step.
because: total.

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Oracle polynomial-time
t : N → N is step-count if
ϕ
ci

Mϕ
di
M

timeM (ϕ, a) ≤ t(mϕ,a ),
wheremϕ,a := max{|a|, |di |}.

a M ϕ (a)Theorem
Total operators havestep-counts.

Lemma
Step-count condition holds ineach step.
because: total.

TheoremM runs in time P

n 7→ P(ln , n) is step-count.

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Opt but not pt

ϕExampleConsider the operator
F (ϕ)(a) := ϕ|a| (1).
atime(ϕ, a).

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Opt but not pt

ϕExampleConsider the operator
F (ϕ)(a) := ϕ|a| (1).
atime(ϕ, a).

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Opt but not pt

ϕExampleConsider the operator
F (ϕ)(a) := ϕ|a| (1).

1atime(ϕ, a).

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Opt but not pt

ϕExampleConsider the operator
F (ϕ)(a) := ϕ|a| (1).

ϕ(1)

1

a
time(ϕ, a).

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Opt but not pt

ϕExampleConsider the operator
F (ϕ)(a) := ϕ|a| (1).

ϕ(1)

atime(ϕ, a).

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Opt but not pt

ϕExampleConsider the operator
F (ϕ)(a) := ϕ|a| (1).

ϕ(1) ϕ2 (1)atime(ϕ, a).

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Opt but not pt

ϕExampleConsider the operator
F (ϕ)(a) := ϕ|a| (1).

ϕ|a| (1)atime(ϕ, a).

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Opt but not pt

ϕExampleConsider the operator
F (ϕ)(a) := ϕ|a| (1).
a ϕ|a| (1)time(ϕ, a).

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Opt but not pt

ϕExampleConsider the operator
F (ϕ)(a) := ϕ|a| (1).
a ϕ|a| (1)2
time(ϕ, a) = O(mϕ,a).

ThxSecond-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Opt but not pt

ϕExampleConsider the operator
F (ϕ)(a) := ϕ|a| (1).
Consider ϕ(a) := aa.

a ϕ|a| (1)2
time(ϕ, a) = O(mϕ,a).

ThxSecond-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Opt but not pt

ϕExampleConsider the operator
F (ϕ)(a) := ϕ|a| (1).
Consider ϕ(a) := aa.
Then |F (ϕ)| ' 2|a| .

a ϕ|a| (1)2
time(ϕ, a) = O(mϕ,a).

ThxSecond-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Opt but not pt

ϕExampleConsider the operator
F (ϕ)(a) := ϕ|a| (1).
Consider ϕ(a) := aa.
Then |F (ϕ)| ' 2|a| .
F not polytime.

a ϕ|a| (1)2
time(ϕ, a) = O(mϕ,a).

ThxSecond-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Opt but not pt

ϕExampleConsider the operator
F (ϕ)(a) := ϕ|a| (1).
Consider ϕ(a) := aa.
Then |F (ϕ)| ' 2|a| .
F not polytime.
Essentially iteration operator.

a ϕ|a| (1)2
time(ϕ, a) = O(mϕ,a).

ThxSecond-order complexity theory

Oracle polynomial-time

Additional restrictions

length and lookahead revisions
ϕ
ci

Mϕ
di
M

a M ϕ (a)Composition and decomposition

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

length and lookahead revisions
ϕ
ci

Mϕ
di
M

a M ϕ (a)Definition
finite length revision(spt).

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

length and lookahead revisions
ϕ
ci

Mϕ

Definition
finite length revision(spt).

diM
polynomial r.t.:a M ϕ (a)(l, n) 7→ (p ◦ l)r (p(n)) + p(n).

ThxSecond-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

length and lookahead revisions
ϕ
ci

Mϕ

Definition
finite length revision(spt).

diM
polynomial r.t.:a M ϕ (a)(l, n) 7→ (p ◦ l)r (p(n)) + p(n).

First query can not be bigger than p(|a|)... etc.

ThxSecond-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

length and lookahead revisions
ϕ
ci

Mϕ
di
M

Definition
finite length revision(spt).
finite lookahead revision(mpt).
polynomial r.t.:a M ϕ (a)(l, n) 7→ (p ◦ l)r (p(n)) + p(n).

First query can not be bigger than p(|a|)... etc.

ThxSecond-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

length and lookahead revisions
ϕ
ci

Mϕ
di
M

Definition
finite length revision(spt).
finite lookahead revision(mpt).
In both cases polynomial r.t.:a M ϕ (a)(l, n) 7→ (p ◦ l)r (p(n)) + p(n).

First query can not be bigger than p(|a|)... etc.

ThxSecond-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

length and lookahead revisions
ϕ
ci

Mϕ
di
M

Definition
finite length revision(spt).
finite lookahead revision(mpt).
In both cases polynomial r.t.:a M ϕ (a)Lemma
Finite length revision(l, n) 7→ (p ◦ l)r (p(n)) + p(n).
finite lookahead revision.

First query can not be bigger than p(|a|)... etc.

ThxSecond-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

length and lookahead revisions
ϕ
ci

Mϕ

Definition
finite length revision(spt).
finite lookahead revision(mpt).

diM

In both cases polynomial r.t.:a M ϕ (a)Lemma
Finite length revision(l, n) 7→ (p ◦ l)r (p(n)) + p(n).
finite lookahead revision.

First query can not be bigger than p(|a|)... etc.
Have to modify machines.

ThxSecond-order complexity theory

Oracle polynomial-time

Additional restrictions

ExamplesExamplesF (ϕ)(a) := max{|ϕ(b)| | b ⊆ a}Composition and decomposition

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

ExamplesExamplesF (ϕ)(a) := max{|ϕ(b)| | b ⊆ a} is polytime

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

ExamplesExamplesF (ϕ)(a) := max{|ϕ(b)| | b ⊆ a} is polytime has finite
lookahead revision

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

ExamplesExamplesF (ϕ)(a) := max{|ϕ(b)| | b ⊆ a} is polytime has finite
lookahead revision but no finite length revision.

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

ExamplesExamplesF (ϕ)(a) := max{|ϕ(b)| | b ⊆ a} is polytime has finite
lookahead revision but no finite length revision.
Iteration: no finite lookahead revision

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

ExamplesExamplesF (ϕ)(a) := max{|ϕ(b)| | b ⊆ a} is polytime has finite
lookahead revision but no finite length revision.
Iteration: no finite lookahead revision but not polytime.

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

ExamplesExamplesF (ϕ)(a) := max{|ϕ(b)| | b ⊆ a} is polytime has finite
lookahead revision but no finite length revision.
Iteration: no finite lookahead revision but not polytime.
There is an operator F that is polytime but not mpt.

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

ExamplesExamplesF (ϕ)(a) := max{|ϕ(b)| | b ⊆ a} is polytime has finite
lookahead revision but no finite length revision.
Iteration: no finite lookahead revision but not polytime.
There is an operator F that is polytime but not mpt. First
define functionals Fi by
F0 (ϕ) :=  and Fn+1 (ϕ) := (ϕ ◦ ϕ)(Fn (ϕ))≤|ϕ()| .

ThxSecond-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

ExamplesExamplesF (ϕ)(a) := max{|ϕ(b)| | b ⊆ a} is polytime has finite
lookahead revision but no finite length revision.
Iteration: no finite lookahead revision but not polytime.
There is an operator F that is polytime but not mpt. First
define functionals Fi by
F0 (ϕ) :=  and Fn+1 (ϕ) := (ϕ ◦ ϕ)(Fn (ϕ))≤|ϕ()| .
Then set
F (ϕ)(a) := F|a| (ϕ).

ThxSecond-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

ExamplesExamplesF (ϕ)(a) := max{|ϕ(b)| | b ⊆ a} is polytime has finite
lookahead revision but no finite length revision.
Iteration: no finite lookahead revision but not polytime.
There is an operator F that is polytime but not mpt. First
define functionals Fi by
F0 (ϕ) :=  and Fn+1 (ϕ) := (ϕ ◦ ϕ)(Fn (ϕ))≤|ϕ()| .
Then set
F (ϕ)(a) := F|a| (ϕ).
This operator is polytime but not mpt.

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

The recursion operator
Theorem (Cook, Urquart)
The feasible functionals of type-two are exactly those realized bylambda terms with polytime functions and R as constants.

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

The recursion operator
Theorem (Cook, Urquart)
The feasible functionals of type-two are exactly those realized bylambda terms with polytime functions and R as constants.
Let R be defined by R(ϕ, a, ψ, ) := a andR(ϕ, a, ψ, ci) := ϕ(ci, R(ϕ, a, ψ, c)) if smaller than |ψ(ci)|.
Lemma (Kapron, S.)
R is mpt.

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

The recursion operator
Theorem (Cook, Urquart)
The feasible functionals of type-two are exactly those realized bylambda terms with polytime functions and R as constants.
Let R be defined by R(ϕ, a, ψ, ) := a andR(ϕ, a, ψ, ci) := ϕ(ci, R(ϕ, a, ψ, c)) if smaller than |ψ(ci)|.
Lemma (Kapron, S.)
R is mpt.
Theorem
The lambda closure of mpt are the feasible functionals.

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

A decomposition result

Theorem (Kapron, S.)
Every mpt operator can be decomposed into two spt operators.

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

A decomposition result

Theorem (Kapron, S.)
Every mpt operator can be decomposed into two spt operators.
ExampleDecomposition of the maximization operator.

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

A decomposition result

Theorem (Kapron, S.)
Every mpt operator can be decomposed into two spt operators.
ExampleDecomposition of the maximization operator.
Corollary
The lambda closure of spt are the feasible functionals.

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Conclusion

Conclusion.

Composition and decomposition

Thx

Second-order complexity theory

Oracle polynomial-time

Additional restrictions

Composition and decomposition

Thanks!

Thank you for listening!

Thx