Exact decoding of finite structures

Decoding and encoding are inverse on structures, including their relation and constant interpretations. The decoder succeeds precisely on valid encodings; every other bit string is rejected. These are computability and correctness results, without a machine time or space bound.

@[simp]

theorem Complexity.DescriptiveComplexity.decodeStruct_nil (V : Vocabulary) : decodeStruct V [] = none

The empty input is not a structure encoding.

@[simp]

theorem Complexity.DescriptiveComplexity.decodeStruct_encodeStruct {V : Vocabulary} (A : DecFinStruct V) : decodeStruct V (encodeStruct A) = some A

Every encoded structure is recovered exactly by the computable decoder.

theorem Complexity.DescriptiveComplexity.decodeStruct_eq_some_iff {V : Vocabulary} (bits : List Bool) (A : DecFinStruct V) : decodeStruct V bits = some A ↔ encodeStruct A = bits

Successful decoding is equivalent to exact re-encoding of the returned structure.

theorem Complexity.DescriptiveComplexity.decodeStruct_eq_none_iff {V : Vocabulary} (bits : List Bool) : decodeStruct V bits = none ↔ ¬∃ (A : DecFinStruct V), encodeStruct A = bits

A rejected input is exactly a string outside the image of the encoder.

theorem Complexity.DescriptiveComplexity.encodeStruct_injective {V : Vocabulary} : Function.Injective encodeStruct

The bit-string encoding determines all fields of a decidable finite structure.