The language induced by a Boolean query

The bridge from descriptive complexity to the machine model: a Boolean query over finite structures induces a language (a set of bit strings) — the encodings of the structures satisfying it. This is where a logical characterization of a query becomes a statement about a machine-model Language, the connection Fagin's theorem (NP = ∃SO) and the other planned logic/complexity correspondences ultimately rest on.

Main definitions and results

• DescriptiveComplexity.queryLanguage — the language of a query.
• DescriptiveComplexity.mem_queryLanguage — a Q-satisfying structure's encoding is in Q's language.
• mem_queryLanguage_iff_decodeStruct — exact membership via successful decoding.
• encodeStruct_mem_queryLanguage_iff — encoding preserves and reflects the query.
• not_mem_queryLanguage_of_decodeStruct_eq_none — malformed inputs are rejected.

def Complexity.DescriptiveComplexity.queryLanguage {V : Vocabulary} (Q : BooleanQuery V) : Language

The language induced by a Boolean query Q: the set of bit strings that encode a (decidable) structure satisfying Q.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.DescriptiveComplexity.mem_queryLanguage {V : Vocabulary} (Q : BooleanQuery V) (A : DecFinStruct V) (hQ : Q A.toFinStruct) : encodeStruct A ∈ queryLanguage Q

Encoding a Q-satisfying structure lands in Q's induced language.

theorem Complexity.DescriptiveComplexity.mem_queryLanguage_iff_decodeStruct {V : Vocabulary} (Q : BooleanQuery V) (bits : List Bool) : bits ∈ queryLanguage Q ↔ ∃ (A : DecFinStruct V), decodeStruct V bits = some A ∧ Q A.toFinStruct

Query-language membership is exactly successful decoding followed by the query.

theorem Complexity.DescriptiveComplexity.encodeStruct_mem_queryLanguage_iff {V : Vocabulary} (Q : BooleanQuery V) (A : DecFinStruct V) : encodeStruct A ∈ queryLanguage Q ↔ Q A.toFinStruct

Encoding preserves and reflects the answer to any structural Boolean query.

theorem Complexity.DescriptiveComplexity.not_mem_queryLanguage_of_decodeStruct_eq_none {V : Vocabulary} (Q : BooleanQuery V) (bits : List Bool) (h : decodeStruct V bits = none) : bits ∉ queryLanguage Q

A malformed encoding is outside every induced query language.