Direct plain polynomial-time primitives

The canonical rules normalize plain realizing machines inside the internal proof, combine them with machine-level combinators, and conclude plain computability. No tidy asymptotic predicate or bridge participates in their statements or derivations.

Main results

• ComputableInPolyTime.comp, .trans, .pair, .ite, .foldl: direct closure rules.
• ComputableInPolyTime.fst, .snd: ordinary encoded-pair projections.
• ComputableInPolyTime.frame, .unframe, .dropFrame: total word framing and parsers.

theorem Turing.MultiTapeTM.ComputableInPolyTime.frame : ComputableInPolyTime MultiTapeTM.frame encBits encBits

Frame a raw word with the existing streaming encoder.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unframe : ComputableInPolyTime MultiTapeTM.unframe encBits encBits

Read the first framed word, including incomplete or malformed inputs.

theorem Turing.MultiTapeTM.ComputableInPolyTime.dropFrame : ComputableInPolyTime MultiTapeTM.dropFrame encBits encBits

Drop the first framed word, including incomplete or malformed inputs.

theorem Turing.MultiTapeTM.ComputableInPolyTime.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {f : β → γ} {g : α → β} (hf : ComputableInPolyTime f encMid encOut) (hg : ComputableInPolyTime g encIn encMid) : ComputableInPolyTime (f ∘ g) encIn encOut

Composition, through the machine-level composition of tidy machines. The intermediate word is no longer than the time of the inner machine.

theorem Turing.MultiTapeTM.ComputableInPolyTime.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {f : α → β} {g : β → γ} (hf : ComputableInPolyTime f encIn encMid) (hg : ComputableInPolyTime g encMid encOut) : ComputableInPolyTime (fun (x : α) => g (f x)) encIn encOut

Compose in execution order. This lets fun_prop infer the intermediate encoding from the inner function when it cannot be inferred from the outer function.

theorem Turing.MultiTapeTM.ComputableInPolyTime.comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {f : β → γ} {g : α → β} (hf : ComputableInPolyTime f encMid encOut) (hg : ComputableInPolyTime g encIn encMid) : ComputableInPolyTime (fun (a : α) => f (g a)) encIn encOut

theorem Turing.MultiTapeTM.ComputableInPolyTime.pair {α β₁ β₂ : Type u} {encIn : α ↪ List Bool} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {enc : β₁ × β₂ ↪ List Bool} [PairEncoding enc₁ enc₂ enc] {f : α → β₁} {g : α → β₂} (hf : ComputableInPolyTime f encIn enc₁) (hg : ComputableInPolyTime g encIn enc₂) : ComputableInPolyTime (fun (x : α) => (f x, g x)) encIn enc

Pairing, for any encoding of pairs, through its pairing combinator.

theorem Turing.MultiTapeTM.ComputableInPolyTime.ite {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encC : Bool ↪ List Bool} {c : α → Bool} {f g : α → β} (hc : ComputableInPolyTime c encIn encC) (hf : ComputableInPolyTime f encIn encMid) (hg : ComputableInPolyTime g encIn encMid) : ComputableInPolyTime (fun (x : α) => if c x = true then f x else g x) encIn encMid

Case distinction on a Boolean test computable in polynomial time, in any encoding of Bool.

theorem Turing.MultiTapeTM.ComputableInPolyTime.foldl {γ α β : Type u} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} {encBA : β × α ↪ List Bool} {encS : List α × β ↪ List Bool} {encO : Option (List α × β) ↪ List Bool} [ListEncoding encA encL] [PairEncoding encB encA encBA] [PairEncoding encL encB encS] [OptionEncoding encS encO] {list : γ → List α} {init : γ → β} {step : β → α → β} (hlist : ComputableInPolyTime list encIn encL) (hinit : ComputableInPolyTime init encIn encB) (hstep : ComputableInPolyTime (fun (p : β × α) => step p.1 p.2) encBA encB) {L : ℕ → ℕ} (hL : Cslib.PolynomiallyBounded L) (hlen : ∀ (x : γ), (list x).length ≤ L (encIn x).length) (harg : ∀ (x : γ) (i : ℕ) (hi : i < (list x).length), (encBA (List.foldl step (init x) (List.take i (list x)), (list x)[i])).length ≤ L (encIn x).length) (hstate : ∀ (x : γ), ∀ i ≤ (list x).length, (encS (List.drop i (list x), List.foldl step (init x) (List.take i (list x)))).length ≤ L (encIn x).length) : ComputableInPolyTime (fun (x : γ) => List.foldl step (init x) (list x)) encIn encB

Left folds, through the machine-level loop. Besides certificates for the list, the initial value and the step, a polynomially bounded L must bound the length of the list, the encoded arguments of every step and the encoded intermediate states.

theorem Turing.MultiTapeTM.PairEncoding.computableInPolyTime_fst {β₁ β₂ : Type u} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {enc : β₁ × β₂ ↪ List Bool} [h : PairEncoding enc₁ enc₂ enc] : ComputableInPolyTime (fun (p : β₁ × β₂) => p.1) enc enc₁

The first projection of an encoding of pairs, from its linear-time machine.

theorem Turing.MultiTapeTM.PairEncoding.computableInPolyTime_snd {β₁ β₂ : Type u} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {enc : β₁ × β₂ ↪ List Bool} [h : PairEncoding enc₁ enc₂ enc] : ComputableInPolyTime (fun (p : β₁ × β₂) => p.2) enc enc₂

The second projection of an encoding of pairs, from its linear-time machine.

theorem Turing.MultiTapeTM.ComputableInPolyTime.fst {α β : Type u} (enc₁ : α ↪ List Bool) (enc₂ : β ↪ List Bool) : ComputableInPolyTime (fun (p : α × β) => p.1) (encPair enc₁ enc₂) enc₁

Project the first entry of an ordinary framed pair.

theorem Turing.MultiTapeTM.ComputableInPolyTime.snd {α β : Type u} (enc₁ : α ↪ List Bool) (enc₂ : β ↪ List Bool) : ComputableInPolyTime (fun (p : α × β) => p.2) (encPair enc₁ enc₂) enc₂

Project the second entry of an ordinary framed pair.

theorem Turing.MultiTapeTM.ComputableInPolyTime.of_enc_eq {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {δ : Type u_4} {encD : δ ↪ List Bool} {f : α → β} {g : α → δ} (hf : ComputableInPolyTime f encIn encMid) (h : ∀ (a : α), encD (g a) = encMid (f a)) : ComputableInPolyTime g encIn encD

Reuse the same realizing machine for an equal encoded output.

theorem Turing.MultiTapeTM.ComputableInPolyTime.polyBounded_length {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (hf : ComputableInPolyTime f encIn encMid) : PolyBounded (fun (a : α) => (encIn a).length) fun (a : α) => (encMid (f a)).length

The complete encoded output is bounded by the actual time of its realizing machine.

theorem Turing.MultiTapeTM.ComputableInPolyTime.prod {α β₁ β₂ : Type u} {encIn : α ↪ List Bool} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {f : α → β₁} {g : α → β₂} (hf : ComputableInPolyTime f encIn enc₁) (hg : ComputableInPolyTime g encIn enc₂) : ComputableInPolyTime (fun (a : α) => (f a, g a)) encIn (encPair enc₁ enc₂)

Pair two computed outputs using the standard pair encoding.

theorem Turing.MultiTapeTM.ComputableInPolyTime.fst' {α : Type u_1} {encIn : α ↪ List Bool} {β₁ β₂ : Type u} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {f : α → β₁ × β₂} (hf : ComputableInPolyTime f encIn (encPair enc₁ enc₂)) : ComputableInPolyTime (fun (a : α) => (f a).1) encIn enc₁

Project the first entry after computing a pair; the input universe is independent.

theorem Turing.MultiTapeTM.ComputableInPolyTime.snd' {α : Type u_1} {encIn : α ↪ List Bool} {β₁ β₂ : Type u} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {f : α → β₁ × β₂} (hf : ComputableInPolyTime f encIn (encPair enc₁ enc₂)) : ComputableInPolyTime (fun (a : α) => (f a).2) encIn enc₂

Project the second entry after computing a pair; the input universe is independent.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bool_and : ComputableInPolyTime (fun (p : Bool × Bool) => p.1 && p.2) (encPair encBool encBool) encBool

Boolean conjunction on its fixed finite input domain.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bool_and' {γ : Type} {input : γ ↪ List Bool} {left right : γ → Bool} (hleft : ComputableInPolyTime left input encBool) (hright : ComputableInPolyTime right input encBool) : ComputableInPolyTime (fun (a : γ) => left a && right a) input encBool

Conjunction of two computed Booleans.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bool_not : ComputableInPolyTime not encBool encBool

Boolean negation on its fixed finite input domain.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bool_or : ComputableInPolyTime (fun (p : Bool × Bool) => p.1 || p.2) (encPair encBool encBool) encBool

Boolean disjunction is polynomial-time in the standard Boolean encoding.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bool_xor : ComputableInPolyTime (fun (p : Bool × Bool) => p.1 ^^ p.2) (encPair encBool encBool) encBool

Boolean exclusive disjunction on its fixed finite input domain.

theorem Turing.MultiTapeTM.ComputableInPolyTime.decide_and {α : Type} {encA : α ↪ List Bool} {left right : α → Prop} [(a : α) → Decidable (left a)] [(a : α) → Decidable (right a)] (hleft : ComputableInPolyTime (fun (a : α) => decide (left a)) encA encBool) (hright : ComputableInPolyTime (fun (a : α) => decide (right a)) encA encBool) : ComputableInPolyTime (fun (a : α) => decide (left a ∧ right a)) encA encBool

Conjunction preserves the full input encoding of both decision procedures.

theorem Turing.MultiTapeTM.ComputableInPolyTime.ite_decide {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {condition : α → Prop} [(a : α) → Decidable (condition a)] {yes no : α → β} (hcondition : ComputableInPolyTime (fun (a : α) => decide (condition a)) encA encBool) (hyes : ComputableInPolyTime yes encA encB) (hno : ComputableInPolyTime no encA encB) : ComputableInPolyTime (fun (a : α) => if condition a then yes a else no a) encA encB

A proposition-valued conditional computes its decision in the standard Boolean encoding.