Encodings of dependent finite tables

A fixed finite table may store a different type at each index. Encode each entry using its own encoding and store the resulting words with the existing finite-table encoding encPi.

Main definitions

• Turing.MultiTapeTM.encDPi: encode a dependent family over a fixed finite index type.

Main results

• Turing.MultiTapeTM.length_encDPi_le: bound the table from the encoded sizes of its entries.
• Turing.MultiTapeTM.length_encDPi: the exact sum of the framed entry sizes.
• Turing.MultiTapeTM.length_encDPi_update_le: changing one entry only charges its size growth.

References

Extends the finite-table encoding in Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pi.

noncomputable def Turing.MultiTapeTM.encDPi {Index : Type} {Value : Index → Type} [Fintype Index] (enc : (i : Index) → Value i ↪ List Bool) : ((i : Index) → Value i) ↪ List Bool

Encode each entry separately, then store all the resulting words in a finite table.

@[simp]

theorem Turing.MultiTapeTM.encDPi_apply {Index : Type} {Value : Index → Type} [Fintype Index] (enc : (i : Index) → Value i ↪ List Bool) (values : (i : Index) → Value i) : (encDPi enc) values = (encPi encBits) fun (i : Index) => (enc i) (values i)

theorem Turing.MultiTapeTM.length_encDPi {Index : Type} {Value : Index → Type} [Fintype Index] (enc : (i : Index) → Value i ↪ List Bool) (values : (i : Index) → Value i) : ((encDPi enc) values).length = ∑ i : Index, (2 * ((enc i) (values i)).length + 1)

The dependent-table encoding is the sum of its framed entry sizes.

theorem Turing.MultiTapeTM.length_encDPi_le {Index : Type} {Value : Index → Type} [Fintype Index] (enc : (i : Index) → Value i ↪ List Bool) (values : (i : Index) → Value i) {bound : ℕ} (hbound : ∀ (i : Index), ((enc i) (values i)).length ≤ bound) : ((encDPi enc) values).length ≤ Fintype.card Index * (2 * bound + 1)

The dependent-table encoding charges every entry and its framing.

theorem Turing.MultiTapeTM.length_encDPi_update_le {Index : Type} {Value : Index → Type} [Fintype Index] [DecidableEq Index] (enc : (i : Index) → Value i ↪ List Bool) (values : (i : Index) → Value i) (i : Index) (value : Value i) {growth : ℕ} (hgrowth : ((enc i) value).length ≤ ((enc i) (values i)).length + growth) : ((encDPi enc) (Function.update values i value)).length ≤ ((encDPi enc) values).length + 2 * growth

Updating one entry grows the full table by at most twice that entry's growth.