Documentation

CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.DPi

Polynomial-time dependent finite table operations #

The types of entries may depend on the table index. Each entry has its own encoding; the encoded words form an ordinary finite table. Construction, fixed-index lookup and update therefore reuse the existing finite-table calculus without requiring a decoder for any entry encoding.

Main results #

References #

Extends the finite-table calculus in CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Pi.

source
theorem Turing.MultiTapeTM.ComputableInPolyTime.dpi {α Index : Type} {Value : Index → Type} [Fintype Index] {input : α ↪ List Bool} {enc : (i : Index) → Value i ↪ List Bool} {values : α → (i : Index) → Value i} (hvalues : ∀ (i : Index), ComputableInPolyTime (fun (a : α) => values a i) input (enc i)) :
ComputableInPolyTime values input (encDPi enc)

Construct a fixed dependent family, retaining the original input for each entry.

source
theorem Turing.MultiTapeTM.ComputableInPolyTime.dpi_apply {Index : Type} {Value : Index → Type} [Fintype Index] (enc : (i : Index) → Value i ↪ List Bool) (i : Index) :
ComputableInPolyTime (fun (values : (j : Index) → Value j) => values i) (encDPi enc) (enc i)

Read a fixed dependent-table entry, charging the stored prefix and requiring no default.

source
theorem Turing.MultiTapeTM.ComputableInPolyTime.dpi_update {α Index : Type} {Value : Index → Type} [Fintype Index] {input : α ↪ List Bool} {enc : (i : Index) → Value i ↪ List Bool} [DecidableEq Index] {values : α → (i : Index) → Value i} {i : Index} {value : α → Value i} (hvalues : ComputableInPolyTime values input (encDPi enc)) (hvalue : ComputableInPolyTime value input (enc i)) :
ComputableInPolyTime (fun (a : α) => Function.update (values a) i (value a)) input (encDPi enc)

Update one dependent-table entry while retaining and charging all other entries.