Encoding ordered interpretations with a domain formula

A well-formed source of size at least two is mapped to the encoding of its image, whose universe is numbered by the lexicographic rank of the domain tuples. This is defined for every source, including those with fewer than two domain tuples, whose encoded image has no canonical ordered decoding. Only the target input relations are serialized; the canonical order, BIT and constants are determined by the cardinality. Malformed sources and sizes zero and one map to the same malformed target as FullTupleInterpretation.encodedMap.

Partial decoding of source-only encodings turns an ordered query language into the set of encodings that decode to members, and an admissible interpretation commutes with decoding. This is the simulation hypothesis of Cslib.Complexity.ManyOneReducibleBy.lift.

Main definitions

• Cslib.Logic.FO.Ordered.decode?: partial decoding of source-only encodings.
• Cslib.Logic.FO.Ordered.DomainInterpretation.encodedMap: the total map on parsed instances.

Main results

• Cslib.Logic.FO.Ordered.Query.encodedLanguage_eq: query languages by partial decoding.
• Cslib.Logic.FO.Ordered.DomainInterpretation.card_encodedMap: the number of domain tuples.
• Cslib.Logic.FO.Ordered.DomainInterpretation.wellFormed_encodedMap_iff: exact shape guard.
• Cslib.Logic.FO.Ordered.DomainInterpretation.table_encodedMap: exact table numbering.
• Cslib.Logic.FO.Ordered.DomainInterpretation.decode?_encodedMap: commutation with decoding.

References

• N. Immerman, Descriptive Complexity, Proviso 1.15 and Definition 1.26.

def Cslib.Logic.FO.Ordered.decode? {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) (a : EncodedStructure) : Option (Structure L)

Decode a source-only encoding as a canonically ordered structure, when it is well formed and has at least two elements.

theorem Cslib.Logic.FO.Ordered.decode?_of_admissible {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) {a : EncodedStructure} (ha : v.WellFormed a) (hn : 2 ≤ a.1) : decode? v a = some (decoded v a hn)

theorem Cslib.Logic.FO.Ordered.decode?_of_not_admissible {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) {a : EncodedStructure} (ha : ¬(v.WellFormed a ∧ 2 ≤ a.1)) : decode? v a = none

@[simp]

theorem Cslib.Logic.FO.Ordered.decode?_encode {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) (M : Structure L) : decode? v (encode v M) = some M

Canonical encodings decode to their structures.

theorem Cslib.Logic.FO.Ordered.decode?_eq_some_iff {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) {a : EncodedStructure} {M : Structure L} : decode? v a = some M ↔ ∃ (_ : v.WellFormed a) (hn : 2 ≤ a.1), decoded v a hn = M

theorem Cslib.Logic.FO.Ordered.Query.encodedLanguage_eq {L : FirstOrder.Language} [L.IsRelational] (K : Query L) (v : Vocabulary L) : K.encodedLanguage v = {a : EncodedStructure | ∃ M ∈ K, decode? v a = some M}

An ordered query language consists of the encodings decoding to members of the query.

noncomputable def Cslib.Logic.FO.Ordered.DomainInterpretation.encodedMap {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : DomainInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') (a : EncodedStructure) : EncodedStructure

Encode the target input relations on the ranks of the domain tuples. Invalid shapes or sizes below two produce one empty table too many, outside every target query language.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.encodedMap_of_admissible {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : DomainInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') {a : EncodedStructure} (ha : v.WellFormed a) (hn : 2 ≤ a.1) : I.encodedMap v v' a = v'.encode (Fin (I.card (decoded v a hn))) (Equiv.refl (Fin (I.card (decoded v a hn))))

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.encodedMap_of_not_admissible {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : DomainInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') {a : EncodedStructure} (ha : ¬(v.WellFormed a ∧ 2 ≤ a.1)) : I.encodedMap v v' a = (0, List.replicate (v'.count + 1) [])

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.card_encodedMap {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : DomainInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') {a : EncodedStructure} (ha : v.WellFormed a) (hn : 2 ≤ a.1) : (I.encodedMap v v' a).1 = I.card (decoded v a hn)

The encoded image has one element per domain tuple.

@[simp]

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.wellFormed_encodedMap_iff {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : DomainInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') {a : EncodedStructure} : v'.WellFormed (I.encodedMap v v' a) ↔ v.WellFormed a ∧ 2 ≤ a.1

Shape validity of the result is exactly source admissibility, whatever the number of domain tuples.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.table_encodedMap {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : DomainInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') {a : EncodedStructure} (ha : v.WellFormed a) (hn : 2 ≤ a.1) {r : ℕ} (R : L'.Relations r) (x : Fin r → Fin (I.card (decoded v a hn))) : (v'.table (I.encodedMap v v' a) ⟨r, R⟩).getD (tupleIndex x) false = true ↔ (I.rel R).Realize fun (p : Fin r × Fin k) => I.unrank (decoded v a hn) (x p.1) p.2

The bit at the table index of some target ranks is the defining formula on the domain tuples of these ranks. Numeric predicates are not serialized as extra tables.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.length_encStructure_encodedMap {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : DomainInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') {a : EncodedStructure} (ha : v.WellFormed a) (hn : 2 ≤ a.1) : (encStructure (I.encodedMap v v' a)).length = 2 * I.card (decoded v a hn) + 1 + ∑ j : Fin v'.count, (2 * I.card (decoded v a hn) ^ v'.arity j + 1)

The output length includes its unary cardinality and every framed relation table.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.encodedMap_eq_encode {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : DomainInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') {a : EncodedStructure} (hI : I.Admissible) (ha : v.WellFormed a) (hn : 2 ≤ a.1) : I.encodedMap v v' a = encode v' (I.map hI (decoded v a hn))

For an admissible interpretation, the encoded image is the canonical encoding of the image.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.decode?_encodedMap {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {k : ℕ} (I : DomainInterpretation L L' k) (v : Vocabulary L) (v' : Vocabulary L') (hI : I.Admissible) (a : EncodedStructure) : decode? v' (I.encodedMap v v' a) = Option.map (I.map hI) (decode? v a)

Decoding commutes with an admissible interpretation. Undecodable sources map to undecodable targets.