Documentation

DescriptiveComplexity.Exponential.KernelArity

Giving every guessed variable an argument #

A machine that stores a guessed relation on its tape addresses an entry by the encoding of its arguments, so a relation variable of arity zero has the empty address for its only entry – the cell the head starts on, below everything the machine writes. Every construction that reads a stage on a tape therefore asks that the guessed variables have an argument, and a kernel taken from an arbitrary Σ₁ definition need not.

The remedy is to give every variable one more argument and to say nothing about it: R(x̄) becomes R(z, x̄) for a variable z quantified in front of the whole kernel. An assignment of the extended block read at one value of the extra argument is an assignment of the original (SOBlock.atParam), and the extension that ignores the argument reads back as itself, so the two kernels hold at exactly the same structures – as long as the universe is nonempty, which a finite structure of a decision problem is.

This file is that transformation on formulas (arityLift), its correctness (realize_arityLift), and the kernel it makes (NexKernel.withArg, NexKernel.withArg_holds).

The formula transformation #

source
def DescriptiveComplexity.argTerm {Lb : FirstOrder.Language} [Lb.IsRelational] (B : SOBlock) {β : Type} :
(Lb.sum B.lang).Term β → (Lb.sum B.withParam.lang).Term β

A term of a relational vocabulary is a variable, so there is nothing to do.

Equations
Instances For
    Dependency graph
    source
    def DescriptiveComplexity.arityLift {Lb : FirstOrder.Language} [Lb.IsRelational] (B : SOBlock) {α : Type} (p : α) {n : ℕ} :
    (Lb.sum B.lang).BoundedFormula α n → (Lb.sum B.withParam.lang).BoundedFormula α n

    The extra argument, put in front of every guessed atom: a relation variable of the block takes the parameter as a further argument, and everything else – the base vocabulary, the equalities, the quantifiers – is left alone.

    Equations
    Instances For
      Dependency graph
      source
      theorem DescriptiveComplexity.realize_argTerm {Lb : FirstOrder.Language} [Lb.IsRelational] {B : SOBlock} {N : Type} [instN : Lb.Structure N] {β : Type} (ρ : B.withParam.Assignment N) (c : N) (v : β → N) (t : (Lb.sum B.lang).Term β) :
      FirstOrder.Language.Term.realize v (argTerm B t) = FirstOrder.Language.Term.realize v t
      Dependency graph
      source
      theorem DescriptiveComplexity.realize_arityLift {Lb : FirstOrder.Language} [Lb.IsRelational] {B : SOBlock} {α : Type} {p : α} {N : Type} [instN : Lb.Structure N] (ρ : B.withParam.Assignment N) (v : α → N) {n : ℕ} (φ : (Lb.sum B.lang).BoundedFormula α n) (xs : Fin n → N) :
      (arityLift B p φ).Realize v xs ↔ φ.Realize v xs

      The transformation is correct: read at an assignment of the extended block, the lifted formula says what the original said of that assignment read at the value the parameter holds.

      Dependency graph

      The kernel with an argument #

      source
      noncomputable def DescriptiveComplexity.NexKernel.withArg {L : FirstOrder.Language} (K : NexKernel L) :
      NexKernel L

      A kernel whose guessed variables all have an argument: every variable takes one more, and the kernel says of it only that some value of it works.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Dependency graph
        source
        @[simp]
        theorem DescriptiveComplexity.NexKernel.withArg_X {L : FirstOrder.Language} (K : NexKernel L) :
        K.withArg.X = K.X
        Dependency graph
        source
        @[simp]
        theorem DescriptiveComplexity.NexKernel.withArg_B {L : FirstOrder.Language} (K : NexKernel L) :
        K.withArg.B = K.B.withParam
        Dependency graph
        source
        theorem DescriptiveComplexity.NexKernel.withArg_arity_pos {L : FirstOrder.Language} (K : NexKernel L) (i : K.withArg.B.ι) :
        0 < K.withArg.B.arity i

        Every variable of the padded kernel's block has an argument.

        Dependency graph
        source
        def DescriptiveComplexity.SOBlock.ofParam (B : SOBlock) {M : Type} (ρ : B.Assignment M) :
        B.withParam.Assignment M

        An assignment that ignores the extra argument: what the padded kernel is satisfied by when the kernel is.

        Equations
        Instances For
          Dependency graph
          source
          @[simp]
          theorem DescriptiveComplexity.SOBlock.atParam_ofParam (B : SOBlock) {M : Type} (ρ : B.Assignment M) (c : M) :
          B.atParam (B.ofParam ρ) c = ρ
          Dependency graph
          source
          theorem DescriptiveComplexity.NexKernel.withArg_holds {L : FirstOrder.Language} (K : NexKernel L) {M : Type} [instM : K.X.E.Structure M] [instO : LinearOrder M] [Nonempty M] :
          K.withArg.Holds M ↔ K.Holds M

          Padding the arities changes no meaning: an assignment of the padded block read at the value the quantifier picks is an assignment of the original, and an assignment of the original ignoring the extra argument satisfies the padded kernel. The universe has to be nonempty for the quantifier to have something to pick, which a finite structure of a decision problem is.

          Dependency graph