First-order interpretations on binary encodings

The universe-preserving interpretation acts computably on decidable structures. Its string map decodes, interprets, and re-encodes, sending malformed strings to the empty string. Arithmetic table generation supplies a polynomial-time implementation of this same map in the surface module.

This is the encoding bridge from structural first-order reductions to machine many-one reductions, following Immerman's Descriptive Complexity, Chapter 3. Tagged tuple interpretations and exact projective reductions are separate APIs.

def Complexity.DescriptiveComplexity.FOInterpretation.applyDec {V W : Vocabulary} (I : FOInterpretation V W) (A : DecFinStruct V) : DecFinStruct W

Interpret a decidable structure by evaluating the defining relation formulas.

Equations

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

def Complexity.DescriptiveComplexity.FOInterpretation.rawEncoding {V W : Vocabulary} (I : FOInterpretation V W) (card : ℕ) (input : List Bool) : List Bool

Generate target tables arithmetically at a supplied universe size, without validation.

Equations

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

def Complexity.DescriptiveComplexity.FOInterpretation.mapEncoding {V W : Vocabulary} (I : FOInterpretation V W) (input : List Bool) : List Bool

Decode, interpret, and re-encode; malformed input maps to the fixed non-encoding [].

Equations

• I.mapEncoding input = match Complexity.DescriptiveComplexity.decodeStruct V input with | none => [] | some A => Complexity.DescriptiveComplexity.encodeStruct (I.applyDec A)