The number an instance is written as, and the code that writes it

The arithmetic half of the reduction P ≤ᶠᵒ[≤] CODEHALT: the value the drawn code computes on input 0, and the concrete finite structure that value is decoded back into. Nothing here mentions a formula – the first-order side is DescriptiveComplexity.Problems.CodeHalt.Hardness.Interp.

The shape of the value

Every branch of the drawn code is evaluated at input 0, so a constructor node computes a constant: zero is 0, succ is 1, and Nat.pair is what pair does. A nest is therefore a list of numbers, held as Nat.pair a₀ (Nat.pair a₁ (…)) with 0 for the empty list (DescriptiveComplexity.natNestFrom), and reading its d-th entry is following d links (DescriptiveComplexity.nestGet).

The value an instance is written as is

Nat.pair card (nest over the symbols of the vocabulary)

where the entry of a symbol is a nest of nests, dim levels deep, one level per coordinate of a tuple: at the bottom of the j-th chain sits 1 if the symbol holds of the tuple the chain positions spell out, and 0 if it does not. The point of nesting by coordinate rather than numbering tuples in a mixed radix is that each level is a plain walk of the input order, which is what a first-order guard can describe, and no arithmetic on positions has to be proved anywhere.

Reading a value back

DescriptiveComplexity.structOf is the decoding, a FirstOrder.Language.FinStruct over the same vocabulary: the universe size is the first component, and a relation holds of a tuple exactly when following the tuple's coordinates down the nests reaches 1. It is primitive recursive (DescriptiveComplexity.primrec_structOf), which is what lets the reduction compose with the semi-decision procedure of the source problem.

Nests of numbers

def DescriptiveComplexity.nestDrop (v d : ℕ) : ℕ

Following d links of a nest.

Equations

• DescriptiveComplexity.nestDrop v d = (fun (w : ℕ) => (Nat.unpair w).2)^[d] v

def DescriptiveComplexity.nestGet (v d : ℕ) : ℕ

The d-th entry of a nest.

Equations

• DescriptiveComplexity.nestGet v d = (Nat.unpair (DescriptiveComplexity.nestDrop v d)).1

def DescriptiveComplexity.nestLeaf (v : ℕ) (ds : List ℕ) : ℕ

Following the coordinates of a tuple down a nest of nests.

Equations

• DescriptiveComplexity.nestLeaf v ds = List.foldl DescriptiveComplexity.nestGet v ds

@[simp]

theorem DescriptiveComplexity.nestDrop_zero (v : ℕ) : nestDrop v 0 = v

theorem DescriptiveComplexity.nestDrop_succ (a b d : ℕ) : nestDrop (Nat.pair a b) (d + 1) = nestDrop b d

@[simp]

theorem DescriptiveComplexity.nestDrop_zero_left (d : ℕ) : nestDrop 0 d = 0

@[simp]

theorem DescriptiveComplexity.nestGet_zero_left (d : ℕ) : nestGet 0 d = 0

@[simp]

theorem DescriptiveComplexity.nestGet_pair_zero (a b : ℕ) : nestGet (Nat.pair a b) 0 = a

theorem DescriptiveComplexity.nestGet_pair_succ (a b d : ℕ) : nestGet (Nat.pair a b) (d + 1) = nestGet b d

@[simp]

theorem DescriptiveComplexity.nestLeaf_nil (v : ℕ) : nestLeaf v [] = v

@[simp]

theorem DescriptiveComplexity.nestLeaf_cons (v d : ℕ) (ds : List ℕ) : nestLeaf v (d :: ds) = nestLeaf (nestGet v d) ds

Nests, as values and as codes

A nest is written by a chain of pair nodes, whose tail is the constant 0. Both the chain of values and the chain of codes are indexed by a starting position, because that is what the first-order interpretation has one element for: the node standing at position k of the chain.

@[irreducible]

def DescriptiveComplexity.natNestFrom {m : ℕ} (g : Fin m → ℕ) (k : ℕ) : ℕ

The nest of the entries g k, g (k+1), …, as a number.

Equations

• DescriptiveComplexity.natNestFrom g k = if h : k < m then Nat.pair (g ⟨k, h⟩) (DescriptiveComplexity.natNestFrom g (k + 1)) else 0

@[irreducible]

def DescriptiveComplexity.codeNestFrom {m : ℕ} (g : Fin m → Nat.Partrec.Code) (k : ℕ) : Nat.Partrec.Code

The nest of the entries g k, g (k+1), …, as a code.

Equations

• DescriptiveComplexity.codeNestFrom g k = if h : k < m then (g ⟨k, h⟩).pair (DescriptiveComplexity.codeNestFrom g (k + 1)) else Nat.Partrec.Code.zero

theorem DescriptiveComplexity.natNestFrom_of_lt {m : ℕ} (g : Fin m → ℕ) {k : ℕ} (h : k < m) : natNestFrom g k = Nat.pair (g ⟨k, h⟩) (natNestFrom g (k + 1))

theorem DescriptiveComplexity.natNestFrom_of_ge {m : ℕ} (g : Fin m → ℕ) {k : ℕ} (h : ¬k < m) : natNestFrom g k = 0

theorem DescriptiveComplexity.codeNestFrom_of_lt {m : ℕ} (g : Fin m → Nat.Partrec.Code) {k : ℕ} (h : k < m) : codeNestFrom g k = (g ⟨k, h⟩).pair (codeNestFrom g (k + 1))

theorem DescriptiveComplexity.codeNestFrom_of_ge {m : ℕ} (g : Fin m → Nat.Partrec.Code) {k : ℕ} (h : ¬k < m) : codeNestFrom g k = Nat.Partrec.Code.zero

theorem DescriptiveComplexity.nestGet_natNestFrom {m : ℕ} (g : Fin m → ℕ) (d k : ℕ) : nestGet (natNestFrom g k) d = if h : k + d < m then g ⟨k + d, h⟩ else 0

Reading an entry of a nest: d links past the start k sits the entry k + d, and 0 past the end.

The evaluation of the codes that write a value

theorem DescriptiveComplexity.eval_zero_zero : Nat.Partrec.Code.zero.eval 0 = Part.some 0

theorem DescriptiveComplexity.eval_succ_zero : Nat.Partrec.Code.succ.eval 0 = Part.some 1

theorem DescriptiveComplexity.eval_pair_zero {cf cg : Nat.Partrec.Code} {a b : ℕ} (hf : cf.eval 0 = Part.some a) (hg : cg.eval 0 = Part.some b) : (cf.pair cg).eval 0 = Part.some (Nat.pair a b)

theorem DescriptiveComplexity.eval_comp_zero {cf cg : Nat.Partrec.Code} {b : ℕ} (hg : cg.eval 0 = Part.some b) : (cf.comp cg).eval 0 = cf.eval b

def DescriptiveComplexity.numCode : ℕ → Nat.Partrec.Code

The code of a numeral: n applications of succ to zero.

Equations

• DescriptiveComplexity.numCode 0 = Nat.Partrec.Code.zero
• DescriptiveComplexity.numCode n.succ = Nat.Partrec.Code.succ.comp (DescriptiveComplexity.numCode n)

theorem DescriptiveComplexity.eval_numCode (n : ℕ) : (numCode n).eval 0 = Part.some n

theorem DescriptiveComplexity.eval_codeNestFrom {m : ℕ} (gc : Fin m → Nat.Partrec.Code) (gv : Fin m → ℕ) (h : ∀ (j : Fin m), (gc j).eval 0 = Part.some (gv j)) (k : ℕ) : (codeNestFrom gc k).eval 0 = Part.some (natNestFrom gv k)

The chain of codes writes the chain of values.

The dimension of the interpretation

def DescriptiveComplexity.dimOf {L : FirstOrder.Language} (V : L.FinVocab) : ℕ

The dimension the reduction works in: one more than the greatest arity of the vocabulary, so that every symbol's arguments fit in a tuple and the tuples have at least one coordinate (which the numeral chain walks).

Equations

• DescriptiveComplexity.dimOf V = (Finset.univ.sup fun (i : Fin V.numSyms) => V.arity i) + 1

theorem DescriptiveComplexity.arity_lt_dimOf {L : FirstOrder.Language} (V : L.FinVocab) (i : Fin V.numSyms) : V.arity i < dimOf V

theorem DescriptiveComplexity.arity_le_dimOf {L : FirstOrder.Language} (V : L.FinVocab) (i : Fin V.numSyms) : V.arity i ≤ dimOf V

theorem DescriptiveComplexity.dimOf_pos {L : FirstOrder.Language} (V : L.FinVocab) : 0 < dimOf V

The value an ordered structure is written as

def DescriptiveComplexity.setCo {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} (j : ℕ) (a : A) (t : Fin (dimOf V) → A) : Fin (dimOf V) → A

Overwriting one coordinate of a tuple.

Equations

• DescriptiveComplexity.setCo V j a t j' = if ↑j' = j then a else t j'

theorem DescriptiveComplexity.setCo_self {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} {j : ℕ} (hj : j < dimOf V) (t : Fin (dimOf V) → A) : setCo V j (t ⟨j, hj⟩) t = t

theorem DescriptiveComplexity.setCo_apply_self {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} (j : ℕ) (hj : j < dimOf V) (a : A) (t : Fin (dimOf V) → A) : setCo V j a t ⟨j, hj⟩ = a

theorem DescriptiveComplexity.setCo_apply_ne {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} {j : ℕ} {j' : Fin (dimOf V)} (h : ↑j' ≠ j) (a : A) (t : Fin (dimOf V) → A) : setCo V j a t j' = t j'

noncomputable def DescriptiveComplexity.bitOf {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} [L.Structure A] (i : Fin V.numSyms) (t : Fin (dimOf V) → A) : Prop

Whether the symbol i holds of the first V.arity i coordinates of the tuple t: the bit at the bottom of the chains.

Equations

• DescriptiveComplexity.bitOf V i t = FirstOrder.Language.Structure.RelMap (V.sym i) fun (j : Fin (V.arity i)) => t (Fin.castLE ⋯ j)

noncomputable def DescriptiveComplexity.levelVal {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} [L.Structure A] (n : ℕ) (f : Fin n → A) (i : Fin V.numSyms) : ℕ → (Fin (dimOf V) → A) → ℕ

The value of a symbol's block, from m levels above the bottom. At the bottom it is the bit; one level up it is the nest of the values below, indexed by the coordinate dimOf V - m, walked in the order of the input.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.levelVal V n f i 0 x✝ = if DescriptiveComplexity.bitOf V i x✝ then 1 else 0

noncomputable def DescriptiveComplexity.levelCode {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} [L.Structure A] (n : ℕ) (f : Fin n → A) (i : Fin V.numSyms) : ℕ → (Fin (dimOf V) → A) → Nat.Partrec.Code

The code writing DescriptiveComplexity.levelVal.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.levelCode V n f i 0 x✝ = if DescriptiveComplexity.bitOf V i x✝ then Nat.Partrec.Code.succ else Nat.Partrec.Code.zero

theorem DescriptiveComplexity.levelVal_zero {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [L.Structure A] (n : ℕ) (f : Fin n → A) (i : Fin V.numSyms) (t : Fin (dimOf V) → A) : levelVal V n f i 0 t = if bitOf V i t then 1 else 0

theorem DescriptiveComplexity.levelCode_zero {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [L.Structure A] (n : ℕ) (f : Fin n → A) (i : Fin V.numSyms) (t : Fin (dimOf V) → A) : levelCode V n f i 0 t = if bitOf V i t then Nat.Partrec.Code.succ else Nat.Partrec.Code.zero

theorem DescriptiveComplexity.levelVal_succ {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [L.Structure A] (n : ℕ) (f : Fin n → A) (i : Fin V.numSyms) (m : ℕ) (t : Fin (dimOf V) → A) : levelVal V n f i (m + 1) t = natNestFrom (fun (d : Fin n) => levelVal V n f i m (setCo V (dimOf V - (m + 1)) (f d) t)) 0

theorem DescriptiveComplexity.levelCode_succ {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [L.Structure A] (n : ℕ) (f : Fin n → A) (i : Fin V.numSyms) (m : ℕ) (t : Fin (dimOf V) → A) : levelCode V n f i (m + 1) t = codeNestFrom (fun (d : Fin n) => levelCode V n f i m (setCo V (dimOf V - (m + 1)) (f d) t)) 0

theorem DescriptiveComplexity.eval_levelCode {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [L.Structure A] (n : ℕ) (f : Fin n → A) (i : Fin V.numSyms) (m : ℕ) (t : Fin (dimOf V) → A) : (levelCode V n f i m t).eval 0 = Part.some (levelVal V n f i m t)

noncomputable def DescriptiveComplexity.blockVal {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} [L.Structure A] (n : ℕ) (f : Fin n → A) (t₀ : Fin (dimOf V) → A) (i : Fin V.numSyms) : ℕ

The value of the block of the symbol i: its chains, all dimOf V of them, over an arbitrary starting tuple (every coordinate is overwritten on the way down).

Equations

• DescriptiveComplexity.blockVal V n f t₀ i = DescriptiveComplexity.levelVal V n f i (DescriptiveComplexity.dimOf V) t₀

noncomputable def DescriptiveComplexity.blockCode {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} [L.Structure A] (n : ℕ) (f : Fin n → A) (t₀ : Fin (dimOf V) → A) (i : Fin V.numSyms) : Nat.Partrec.Code

The code of the block of the symbol i.

Equations

• DescriptiveComplexity.blockCode V n f t₀ i = DescriptiveComplexity.levelCode V n f i (DescriptiveComplexity.dimOf V) t₀

noncomputable def DescriptiveComplexity.structVal {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} [L.Structure A] (n : ℕ) (f : Fin n → A) (t₀ : Fin (dimOf V) → A) : ℕ

The value of a structure: its size, paired with the nest of the blocks of its symbols.

Equations

• DescriptiveComplexity.structVal V n f t₀ = Nat.pair n (DescriptiveComplexity.natNestFrom (DescriptiveComplexity.blockVal V n f t₀) 0)

Reading a value back as a concrete structure

def DescriptiveComplexity.leafOf (N i : ℕ) (ds : List ℕ) : ℕ

The leaf of the nests reached by the coordinates ds, in the block of the symbol numbered i.

Equations

• DescriptiveComplexity.leafOf N i ds = DescriptiveComplexity.nestLeaf (DescriptiveComplexity.nestGet (Nat.unpair N).2 i) ds

def DescriptiveComplexity.structOf {L : FirstOrder.Language} (V : L.FinVocab) (N : ℕ) : FirstOrder.Language.FinStruct V

The concrete structure a value denotes: the universe has as many elements as the first component says, and a symbol holds of a tuple exactly when the coordinates of that tuple lead to 1 in the symbol's block.

Equations

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

@[simp]

theorem DescriptiveComplexity.card_structOf {L : FirstOrder.Language} (V : L.FinVocab) (N : ℕ) : (structOf V N).card = (Nat.unpair N).1 - 1 + 1

theorem DescriptiveComplexity.relMapBool_structOf {L : FirstOrder.Language} (V : L.FinVocab) (N : ℕ) {a : ℕ} (R : L.Relations a) (x : Fin a → (structOf V N).Univ) : (structOf V N).relMapBool R x = decide (leafOf N (↑(V.index R)) (List.ofFn fun (j : Fin (dimOf V)) => if h : ↑j < a then ↑(x ⟨↑j, h⟩) else 0) = 1)

The value is read back as the structure it was written from

theorem DescriptiveComplexity.nestLeaf_levelVal {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} [L.Structure A] (n : ℕ) (f : Fin n → A) (i : Fin V.numSyms) (ds : Fin (dimOf V) → ℕ) (hds : ∀ (j : Fin (dimOf V)), ds j < n) (m : ℕ) : m ≤ dimOf V → ∀ (t : Fin (dimOf V) → A), (∀ (j : Fin (dimOf V)), ↑j < dimOf V - m → t j = f ⟨ds j, ⋯⟩) → nestLeaf (levelVal V n f i m t) (List.drop (dimOf V - m) (List.ofFn ds)) = if bitOf V i fun (j : Fin (dimOf V)) => f ⟨ds j, ⋯⟩ then 1 else 0

Following the coordinates of a tuple down the chains reaches the bit of that tuple. The induction is on the level: one coordinate is consumed at each step, and the tuple built so far is the one the chains have already walked.

@[simp]

theorem DescriptiveComplexity.unpair_structVal_fst {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} [L.Structure A] (n : ℕ) (f : Fin n → A) (t₀ : Fin (dimOf V) → A) : (Nat.unpair (structVal V n f t₀)).1 = n

@[simp]

theorem DescriptiveComplexity.unpair_structVal_snd {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} [L.Structure A] (n : ℕ) (f : Fin n → A) (t₀ : Fin (dimOf V) → A) : (Nat.unpair (structVal V n f t₀)).2 = natNestFrom (blockVal V n f t₀) 0

theorem DescriptiveComplexity.leafOf_structVal {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} [L.Structure A] (n : ℕ) (f : Fin n → A) (t₀ : Fin (dimOf V) → A) (i : Fin V.numSyms) (ds : Fin (dimOf V) → ℕ) (hds : ∀ (j : Fin (dimOf V)), ds j < n) : leafOf (structVal V n f t₀) (↑i) (List.ofFn ds) = if bitOf V i fun (j : Fin (dimOf V)) => f ⟨ds j, ⋯⟩ then 1 else 0

The leaf of the value of a structure is the bit of the tuple the coordinates spell out.

theorem DescriptiveComplexity.relMap_heq {L : FirstOrder.Language} {A : Type} [L.Structure A] {m a : ℕ} (h : m = a) (R : L.Relations m) (R' : L.Relations a) (hR : R ≍ R') (y : Fin m → A) (z : Fin a → A) (hy : ∀ (j : Fin m), y j = z (Fin.cast h j)) : FirstOrder.Language.Structure.RelMap R y ↔ FirstOrder.Language.Structure.RelMap R' z

Reading a relation through the number of its symbol: the arity dependency of FirstOrder.Language.FinVocab, discharged for a Prop-valued reading.

theorem DescriptiveComplexity.relMapBool_structVal {L : FirstOrder.Language} (V : L.FinVocab) {A : Type} [L.Structure A] (n : ℕ) (hn : 0 < n) (f : Fin n → A) (t₀ : Fin (dimOf V) → A) {a : ℕ} (R : L.Relations a) (y : Fin a → (structOf V (structVal V n f t₀)).Univ) (z : Fin a → Fin n) (hyz : ∀ (j : Fin a), ↑(y j) = ↑(z j)) : (structOf V (structVal V n f t₀)).relMapBool R y = decide (FirstOrder.Language.Structure.RelMap R fun (j : Fin a) => f (z j))

Reading the decoded structure is reading the structure it was written from, once the two tuples are matched by their numbers.

noncomputable def DescriptiveComplexity.structValEquiv {L : FirstOrder.Language} [L.IsRelational] (V : L.FinVocab) {A : Type} [L.Structure A] (n : ℕ) (hn : 0 < n) (f : Fin n ≃ A) (t₀ : Fin (dimOf V) → A) : L.Equiv (structOf V (structVal V n (⇑f) t₀)).Univ A

The decoding of the value of a structure is that structure, along the numbering the value was written with. This is the one mathematical fact the reduction rests on: a semi-decision procedure reading concrete instances, applied to the value drawn in the instance, answers about the instance itself.

Equations

• DescriptiveComplexity.structValEquiv V n hn f t₀ = { toEquiv := (finCongr ⋯).trans f, map_fun' := ⋯, map_rel' := ⋯ }

The decoding is primitive recursive

theorem DescriptiveComplexity.primrec_nestGet : Primrec₂ nestGet

theorem DescriptiveComplexity.primrec_nestLeaf : Primrec₂ nestLeaf

theorem DescriptiveComplexity.primrec_structOf {L : FirstOrder.Language} (V : L.FinVocab) : Primrec (structOf V)

The decoding is primitive recursive: this is what lets the reduction compose with a semi-decision procedure of the source problem.