Positions in the finite-structure encoding

The table sites follow exactly the computable enumeration used by encodeStruct: relation symbols in order, their tuples in allTuples order, then one-hot constant blocks. encodingPosition includes the unary-cardinality prefix.

@[reducible, inline]

abbrev Complexity.DescriptiveComplexity.InputSite (V : Vocabulary) (card : ℕ) : Type

A relation-table cell or one entry in a constant's one-hot block.

Equations

• Complexity.DescriptiveComplexity.InputSite V card = ((i : Fin V.numRels) × (Fin (V.relArity i) → Fin card) ⊕ Fin V.numConsts × Fin card)

def Complexity.DescriptiveComplexity.tableInputCount (V : Vocabulary) (card : ℕ) : ℕ

Number of bits in the relation tables and constant blocks.

Equations

• Complexity.DescriptiveComplexity.tableInputCount V card = Fintype.card (Complexity.DescriptiveComplexity.InputSite V card)

def Complexity.DescriptiveComplexity.inputSiteValue {V : Vocabulary} (A : DecFinStruct V) : InputSite V A.card → Bool

The value stored at a table-input site.

Equations

• Complexity.DescriptiveComplexity.inputSiteValue A (Sum.inl ⟨i, args⟩) = A.rel i args
• Complexity.DescriptiveComplexity.inputSiteValue A (Sum.inr (c, a)) = decide (A.const c = a)

def Complexity.DescriptiveComplexity.encodingTableSites (V : Vocabulary) (card : ℕ) : List (InputSite V card)

Table sites in the computable order used by the structure encoder.

Equations

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

def Complexity.DescriptiveComplexity.encodingLength (V : Vocabulary) (card : ℕ) : ℕ

Full encoded length, including the unary cardinality and its terminator.

Equations

• Complexity.DescriptiveComplexity.encodingLength V card = card + 1 + (List.map (fun (i : Fin V.numRels) => card ^ V.relArity i) (List.finRange V.numRels)).sum + V.numConsts * card

def Complexity.DescriptiveComplexity.encodingPosition (V : Vocabulary) (card : ℕ) (site : InputSite V card) : ℕ

Zero-based bit position of a table entry in the full encoding.

Equations

• Complexity.DescriptiveComplexity.encodingPosition V card site = card + 1 + List.idxOf site (Complexity.DescriptiveComplexity.encodingTableSites V card)