Reading encoded structures in polynomial time

Two polynomial-time primitives on the binary encoding encStructure of finite relational structures: reading the truth table of a relation symbol, and checking that an input is well formed for a vocabulary. Both are fun_prop rules for Turing.MultiTapeTM.ComputableInPolyTime, used by the model checkers and verifiers that read encoded structures.

Main results

• Cslib.Logic.Vocabulary.computableInPolyTime_table: reading a table of the input is polynomial-time.
• Cslib.Logic.Vocabulary.computableInPolyTime_checkShape: checking well-formedness is polynomial-time.

theorem Cslib.Logic.Vocabulary.computableInPolyTime_table {L : FirstOrder.Language} {v : Vocabulary L} {γ : Type} {encIn : γ ↪ List Bool} (r : (n : ℕ) × L.Relations n) {a : γ → EncodedStructure} (ha : Turing.MultiTapeTM.ComputableInPolyTime a encIn encStructure) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => v.table (a x) r) encIn Turing.MultiTapeTM.encBits

Reading a table of the input is polynomial-time.

theorem Cslib.Logic.Vocabulary.computableInPolyTime_checkShape {L : FirstOrder.Language} {v : Vocabulary L} : Turing.MultiTapeTM.ComputableInPolyTime v.checkShape encStructure Turing.MultiTapeTM.encBool

Checking well-formedness is polynomial-time.