Encoding order-free interpreted structures

An interpretation maps a well-formed structure instance to its interpreted structure, numbered by increasing tuple-index rank. An instance (n, tables) with invalid table shapes maps to a fixed malformed target instance, outside every target query language. This is a map between parsed instances; no claim about decoding arbitrary bit strings is made.

Main definitions

• Cslib.Logic.FO.Interpretation.encodedMap: the encoded interpreted structure.

Main results

• Cslib.Logic.FO.Interpretation.wellFormed_encodedMap_iff: shape validity is preserved and reflected by the map.
• Cslib.Logic.FO.Interpretation.mem_queryLanguage_encodedMap_iff: target query membership is equivalent to validity of the source instance and membership of its interpreted structure.

References

• N. Immerman, Descriptive Complexity

noncomputable def Cslib.Logic.FO.Interpretation.encodedMap {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {ι : Type} {d : ℕ} (I : Interpretation L L' ι) (v : Vocabulary L) (v' : Vocabulary L') (e : ι ≃ Fin d) (a : EncodedStructure) : EncodedStructure

Encode the structure interpreted in a well-formed input, numbering its elements by ranks. Malformed inputs map to a fixed malformed structure encoding. This includes empty structures, empty interpreted domains, nullary relations, and interpretations of dimension zero.

theorem Cslib.Logic.FO.Interpretation.encodedMap_of_wellFormed {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {ι : Type} {d : ℕ} (I : Interpretation L L' ι) (v : Vocabulary L) (v' : Vocabulary L') (e : ι ≃ Fin d) {a : EncodedStructure} (ha : v.WellFormed a) : I.encodedMap v v' e a = v'.encode (I.Model (Fin a.1)) (I.rankEquiv e a.1)

theorem Cslib.Logic.FO.Interpretation.encodedMap_of_not_wellFormed {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {ι : Type} {d : ℕ} (I : Interpretation L L' ι) (v : Vocabulary L) (v' : Vocabulary L') (e : ι ≃ Fin d) {a : EncodedStructure} (ha : ¬v.WellFormed a) : I.encodedMap v v' e a = (0, List.replicate (v'.count + 1) [])

theorem Cslib.Logic.FO.Interpretation.not_wellFormed_encodedMap {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {ι : Type} {d : ℕ} (I : Interpretation L L' ι) (v : Vocabulary L) (v' : Vocabulary L') (e : ι ≃ Fin d) {a : EncodedStructure} (ha : ¬v.WellFormed a) : ¬v'.WellFormed (I.encodedMap v v' e a)

@[simp]

theorem Cslib.Logic.FO.Interpretation.wellFormed_encodedMap_iff {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {ι : Type} {d : ℕ} (I : Interpretation L L' ι) (v : Vocabulary L) (v' : Vocabulary L') (e : ι ≃ Fin d) {a : EncodedStructure} : v'.WellFormed (I.encodedMap v v' e a) ↔ v.WellFormed a

The encoded interpreted structure is well formed exactly when the input is.

theorem Cslib.Logic.FO.Interpretation.mem_queryLanguage_encodedMap_iff {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {ι : Type} {d : ℕ} (I : Interpretation L L' ι) (v : Vocabulary L) (v' : Vocabulary L') (e : ι ≃ Fin d) {a : EncodedStructure} {K' : Set (CategoryTheory.Bundled L'.Structure)} (hK' : IsoClosed K') : I.encodedMap v v' e a ∈ v'.queryLanguage K' ↔ v.WellFormed a ∧ CategoryTheory.Bundled.of (I.Model (Fin a.1)) ∈ K'

For an isomorphism-closed target class, target query membership is exactly source validity and membership of the interpreted structure in that class.