Encodings of fixed finite tables

A function on a fixed finite index type is stored as a framed list of all its values. Values may have unbounded encodings, such as words or tapes. Every entry and its framing contribute to size.

Main definitions

• Turing.MultiTapeTM.encPi: store a finite family in a fixed index order.

Main results

• Turing.MultiTapeTM.length_encPi_le: bound the whole table from the sizes of its entries.

References

Adapts Computability/Probabilistic/Pi.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the existing framed list encoding.

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

Encode a family by listing every entry in a fixed order, independently of runtime inputs.

@[simp]

theorem Turing.MultiTapeTM.encPi_apply {Index Value : Type} [Fintype Index] (enc : Value ↪ List Bool) (values : Index → Value) : (encPi enc) values = (encList enc) (List.ofFn fun (i : Fin (Fintype.card Index)) => values ((Fintype.equivFin Index).symm i))

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

The table encoding charges every entry, including its list framing.