Decoding finite structures #
Read a candidate structure using the encoder's exact bit positions, choosing the first set bit in each constant block. The decoder checks the universe size and encoded length, then accepts only if re-encoding the candidate reproduces the whole input. This final check rejects malformed constant blocks, missing bits, and trailing data. No machine running-time bound is asserted here.
def
Complexity.DescriptiveComplexity.readStructCandidate
(V : Vocabulary)
(card : ℕ)
(hcard : 2 ≤ card)
(bits : List Bool)
:
Read a candidate; defaults make the operation total even on malformed input.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Complexity.DescriptiveComplexity.decodeStruct
(V : Vocabulary)
(bits : List Bool)
:
Option (DecFinStruct V)
Parse exactly the image of encodeStruct, returning none on malformed input.
Equations
- One or more equations did not get rendered due to their size.