Documentation

DescriptiveComplexity.Problems.CodeHalt.Hardness.Tags

The elements of the CODEHALT instance an instance is drawn as #

The tags of the reduction P ≤ᶠᵒ[≤] CODEHALT, and the positions of the one abstract code it mentions.

The abstract code is drawn one tag per node #

The reduction composes a fixed code cP – the semi-decision procedure of the source problem, which Mathlib's Nat.Partrec.Code.exists_code supplies rather than has to be built – with the value the instance is written as. The subtree of cP has no reason to be indexed by the input structure, so it is drawn with one tag per node: DescriptiveComplexity.SubPos cP, the positions of a code's syntax tree, defined by recursion on the code so that a position's subterm (DescriptiveComplexity.subAt) and children (DescriptiveComplexity.sub1, DescriptiveComplexity.sub2) are read off definitionally. Tags cost nothing at any instance size, which is what makes this compatible with hardness being cofinal in the reduction order.

The rest of the tags #

tagcoordinatesdraws
root–comp cP (pair numeral nest)
cp p–the node p of cP
pairN–the pair of the numeral and the nest
numN(x, ⊥, …)the comp succ … chain of the numeral, from x on
symN i–the nest of the blocks of the symbols, from i on
chainN i l(x₀, …, x_l, ⊥, …)the level-l chain of the block of i, from x_l on
oneN–succ: the value 1
zeroN–zero: the value 0, and every empty tail

Two of them are shared: oneN and zeroN are single elements, pointed at by every chain that ends and by every bit of the table. A drawing is a relation on the elements, so an element may have several parents – and sharing is what keeps the bit of a tuple an edge of the drawing rather than a conditional mark, so that every tag has one constructor (DescriptiveComplexity.ProgTag.mark) and exclusivity of the marks is immediate.

The positions of a code's syntax tree #

source
def DescriptiveComplexity.SubPos :
Nat.Partrec.Code → Type

The positions of the syntax tree of a code, by recursion on the code.

Equations
Instances For
    Dependency graph
    source
    instance DescriptiveComplexity.instFiniteSubPos (c : Nat.Partrec.Code) :
    Finite (SubPos c)
    Dependency graph
    source
    @[instance_reducible]
    instance DescriptiveComplexity.instDecidableEqSubPos (c : Nat.Partrec.Code) :
    DecidableEq (SubPos c)
    Equations
    Dependency graph
    source
    def DescriptiveComplexity.codeRootPos (c : Nat.Partrec.Code) :
    SubPos c

    The root position of a code's syntax tree.

    Equations
    Instances For
      Dependency graph
      source
      instance DescriptiveComplexity.instNonemptySubPos (c : Nat.Partrec.Code) :
      Nonempty (SubPos c)
      Dependency graph
      source
      def DescriptiveComplexity.subAt (c : Nat.Partrec.Code) :
      SubPos c → Nat.Partrec.Code

      The subterm sitting at a position.

      Equations
      Instances For
        Dependency graph
        source
        def DescriptiveComplexity.sub1 (c : Nat.Partrec.Code) :
        SubPos c → Option (SubPos c)

        The position of the first child of a position, if it has one.

        Equations
        Instances For
          Dependency graph
          source
          def DescriptiveComplexity.sub2 (c : Nat.Partrec.Code) :
          SubPos c → Option (SubPos c)

          The position of the second child of a position, if it has one.

          Equations
          Instances For
            Dependency graph
            source
            @[simp]
            theorem DescriptiveComplexity.subAt_codeRootPos (c : Nat.Partrec.Code) :
            subAt c (codeRootPos c) = c
            Dependency graph

            The tags #

            source
            inductive DescriptiveComplexity.ProgTag {L : FirstOrder.Language} (V : L.FinVocab) (cP : Nat.Partrec.Code) :
            Type

            The tags of the reduction into CODEHALT.

            Instances For
              Dependency graph
              source
              def DescriptiveComplexity.ProgTag.idx {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} :
              ProgTag V cP → Option (SubPos cP) × Option (Fin V.numSyms) × Option (Fin (dimOf V)) × Fin 8

              The numbering that makes the tags a finite type.

              Equations
              Instances For
                Dependency graph
                source
                theorem DescriptiveComplexity.ProgTag.idx_injective {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} :
                Function.Injective idx
                Dependency graph
                source
                instance DescriptiveComplexity.ProgTag.instFinite {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} :
                Finite (ProgTag V cP)
                Dependency graph
                source
                instance DescriptiveComplexity.ProgTag.instNonempty {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} :
                Nonempty (ProgTag V cP)
                Dependency graph
                source
                @[instance_reducible]
                instance DescriptiveComplexity.ProgTag.instDecidableEq {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} :
                DecidableEq (ProgTag V cP)
                Equations
                Dependency graph
                source
                def DescriptiveComplexity.ProgTag.mark {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} :
                ProgTag V cP → CodeTag

                The constructor each tag draws. Every tag draws exactly one, which is what makes the exclusivity of the marks immediate.

                Equations
                Instances For
                  Dependency graph
                  source
                  def DescriptiveComplexity.ProgTag.used {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} :
                  ProgTag V cP → ℕ

                  The number of coordinates a tag uses; the others are padded with the minimum of the input order.

                  Equations
                  Instances For
                    Dependency graph