Documentation

Complexitylib.DescriptiveComplexity.Circuit.Input

Input tables for formula expansion #

There is one input bit for each relation tuple and for each possible value of a constant. A fixed finite equivalence numbers these sites. This numbering depends only on the vocabulary and universe size, not on the structure's relations or constant values. It supplies unconditional compilation theorems for all structures.

The numbering is chosen noncomputably; the formula compiler itself is computable given a layout. Circuit.Encoding provides a separate computable layout for the existing list encoding, including its unary prefix offset.

source
noncomputable def Complexity.DescriptiveComplexity.tableInputEquiv (V : Vocabulary) (card : ℕ) :
InputSite V card ≃ Fin (tableInputCount V card)

A fixed numbering of the input sites, independent of the represented structure.

Equations
Instances For
    source
    noncomputable def Complexity.DescriptiveComplexity.tableLayout (V : Vocabulary) (card : ℕ) :
    StructureInput V card (tableInputCount V card)

    The input layout induced by the fixed numbering of table sites.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def Complexity.DescriptiveComplexity.tableInput {V : Vocabulary} (A : DecFinStruct V) :
      BitString (tableInputCount V A.card)

      Present the structure's tables in the chosen fixed order.

      Equations
      Instances For
        source
        theorem Complexity.DescriptiveComplexity.tableInputCount_eq (V : Vocabulary) (card : ℕ) :
        tableInputCount V card = ∑ i : Fin V.numRels, card ^ V.relArity i + V.numConsts * card

        The input width is the sum of relation-table sizes and constant-block sizes.

        source
        theorem Complexity.DescriptiveComplexity.tableInput_represents {V : Vocabulary} (A : DecFinStruct V) :
        StructureInput.Represents A (tableLayout V A.card) (tableInput A)

        Every structure has the exact table representation required by the compiler.