Documentation

Complexitylib.DescriptiveComplexity.Encoding.Arithmetic.Defs

Arithmetic addresses in structure encodings #

The encoder varies the first tuple coordinate fastest. Its tuple index is thus the little-endian base-card numeral of the coordinates. Relation addresses add the unary header and the lengths of earlier relation tables. Constant addresses skip all relation tables and then the preceding one-hot blocks.

Coordinates are natural numbers in these computations; the correctness theorems specialize to coordinates in Fin card. This interface permits direct use of polynomial-time unary arithmetic without enumerating the tuple universe. tupleDigits also decodes a numeric index to its fixed-width coordinates, for writing truth tables in the same order.

source
def Complexity.DescriptiveComplexity.tupleIndex (card : ℕ) {k : ℕ} :
(Fin k → ℕ) → ℕ

Little-endian base-card index, matching the first-coordinate-fastest tuple order.

Equations
Instances For
    source
    def Complexity.DescriptiveComplexity.tupleDigits (card k a✝ : ℕ) :
    Fin k → ℕ

    Recover the fixed-width little-endian base-card coordinates of a tuple index.

    Equations
    Instances For
      source
      def Complexity.DescriptiveComplexity.relationAddress (V : Vocabulary) (card : ℕ) (r : Fin V.numRels) (args : Fin (V.relArity r) → ℕ) :
      ℕ

      Arithmetic position of a relation-table bit in the full structure encoding.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Complexity.DescriptiveComplexity.constantAddress (V : Vocabulary) (card : ℕ) (c : Fin V.numConsts) (a : ℕ) :
        ℕ

        Arithmetic position of a constant's one-hot bit in the full structure encoding.

        Equations
        Instances For