The interpretation that draws an instance as a program

The defining formulas of the reduction P ≤ᶠᵒ[≤] CODEHALT, and the interpretation DescriptiveComplexity.codeProgInterp they assemble, of dimension DescriptiveComplexity.dimOf V over the ordered expansion of the source vocabulary.

Three things make the formulas short.

• The mark of an element depends only on its tag (DescriptiveComplexity.ProgTag.mark), because the two leaves oneN and zeroN are shared and a bit of the input is read as an edge – which of the two the last chain node points at – rather than as a mark.
• The guard of an element depends only on its tag as well: a tag uses DescriptiveComplexity.ProgTag.used coordinates and the rest are minima (DescriptiveComplexity.canonF of DescriptiveComplexity.Padding), so every defining formula is a conjunction of the two guards with a small body (DescriptiveComplexity.arg1Body, DescriptiveComplexity.arg2Body).
• Every body is a walk of the input order: the immediate successor of a coordinate (DescriptiveComplexity.succF), its being a maximum, and equality of the other coordinates. No lexicographic order and no arithmetic on positions appears – that is what nesting the table by coordinate buys.

The section “Characterization of the interpreted relations” reads each relation of FirstOrder.Language.code back through DescriptiveComplexity.FOInterpretation.relMap_map; the two semantic relations DescriptiveComplexity.Arg1On and DescriptiveComplexity.Arg2On are the only interface the correctness proof uses.

Selecting the coordinates of an argument

def DescriptiveComplexity.CodeProgRed.sel₀ {L : FirstOrder.Language} (V : L.FinVocab) (j : Fin (dimOf V)) : Fin 1 × Fin (dimOf V)

The coordinates of the only argument of a unary symbol.

Equations

• DescriptiveComplexity.CodeProgRed.sel₀ V j = (0, j)

def DescriptiveComplexity.CodeProgRed.selA {L : FirstOrder.Language} (V : L.FinVocab) (j : Fin (dimOf V)) : Fin 2 × Fin (dimOf V)

The coordinates of the first argument of a binary symbol.

Equations

• DescriptiveComplexity.CodeProgRed.selA V j = (0, j)

def DescriptiveComplexity.CodeProgRed.selB {L : FirstOrder.Language} (V : L.FinVocab) (j : Fin (dimOf V)) : Fin 2 × Fin (dimOf V)

The coordinates of the second argument of a binary symbol.

Equations

• DescriptiveComplexity.CodeProgRed.selB V j = (1, j)

def DescriptiveComplexity.CodeProgRed.fz {L : FirstOrder.Language} (V : L.FinVocab) : Fin (dimOf V)

The first coordinate: the one the numeral chain walks.

Equations

• DescriptiveComplexity.CodeProgRed.fz V = ⟨0, ⋯⟩

The atomic builders

@[reducible, inline]

abbrev DescriptiveComplexity.CodeProgRed.srcSym {L : FirstOrder.Language} {V : L.FinVocab} (i : Fin V.numSyms) : (L.sum FirstOrder.Language.order).Relations (V.arity i)

A symbol of the source vocabulary, in the ordered expansion.

Equations

• DescriptiveComplexity.CodeProgRed.srcSym i = Sum.inl (V.sym i)

def DescriptiveComplexity.CodeProgRed.relAtF {L : FirstOrder.Language} {V : L.FinVocab} (i : Fin V.numSyms) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (dimOf V))

The symbol i of the source vocabulary holds of the first coordinates of the tuple held by the first argument, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.CodeProgRed.maxAF {L : FirstOrder.Language} {V : L.FinVocab} (j : Fin (dimOf V)) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (dimOf V))

The coordinate j of the first argument is a maximum, as a formula.

Equations

• DescriptiveComplexity.CodeProgRed.maxAF j = DescriptiveComplexity.maxF (DescriptiveComplexity.CodeProgRed.selA V j)

noncomputable def DescriptiveComplexity.CodeProgRed.botBF {L : FirstOrder.Language} {V : L.FinVocab} (j : Fin (dimOf V)) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (dimOf V))

The coordinate j of the second argument is a minimum, as a formula.

Equations

• DescriptiveComplexity.CodeProgRed.botBF j = DescriptiveComplexity.botF (DescriptiveComplexity.CodeProgRed.selB V j)

noncomputable def DescriptiveComplexity.CodeProgRed.succCoF {L : FirstOrder.Language} {V : L.FinVocab} (j : Fin (dimOf V)) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (dimOf V))

The coordinate j of the second argument covers that of the first, as a formula.

Equations

• DescriptiveComplexity.CodeProgRed.succCoF j = DescriptiveComplexity.succF (DescriptiveComplexity.CodeProgRed.selA V j) (DescriptiveComplexity.CodeProgRed.selB V j)

@[simp]

theorem DescriptiveComplexity.CodeProgRed.realize_relAtF {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [L.Structure A] [LinearOrder A] {v : Fin 2 × Fin (dimOf V) → A} (i : Fin V.numSyms) : (relAtF i).Realize v ↔ bitOf V i fun (j : Fin (dimOf V)) => v (selA V j)

@[simp]

theorem DescriptiveComplexity.CodeProgRed.realize_maxAF {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [L.Structure A] [LinearOrder A] {v : Fin 2 × Fin (dimOf V) → A} (j : Fin (dimOf V)) : (maxAF j).Realize v ↔ IsTop (v (selA V j))

@[simp]

theorem DescriptiveComplexity.CodeProgRed.realize_botBF {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [L.Structure A] [LinearOrder A] {v : Fin 2 × Fin (dimOf V) → A} (j : Fin (dimOf V)) : (botBF j).Realize v ↔ IsBot (v (selB V j))

@[simp]

theorem DescriptiveComplexity.CodeProgRed.realize_succCoF {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [L.Structure A] [LinearOrder A] {v : Fin 2 × Fin (dimOf V) → A} (j : Fin (dimOf V)) : (succCoF j).Realize v ↔ v (selA V j) < v (selB V j) ∧ ∀ (a : A), ¬(v (selA V j) < a ∧ a < v (selB V j))

The bodies of the child relations

noncomputable def DescriptiveComplexity.CodeProgRed.arg1Body {L : FirstOrder.Language} (V : L.FinVocab) (cP : Nat.Partrec.Code) : ProgTag V cP → ProgTag V cP → (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (dimOf V))

The body of the first-child relation, one case per pair of tags.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.CodeProgRed.arg1Body V cP DescriptiveComplexity.ProgTag.root (DescriptiveComplexity.ProgTag.cp p) = if p = DescriptiveComplexity.codeRootPos cP then ⊤ else ⊥
• DescriptiveComplexity.CodeProgRed.arg1Body V cP (DescriptiveComplexity.ProgTag.cp p) (DescriptiveComplexity.ProgTag.cp q) = if DescriptiveComplexity.sub1 cP p = some q then ⊤ else ⊥
• DescriptiveComplexity.CodeProgRed.arg1Body V cP DescriptiveComplexity.ProgTag.numN DescriptiveComplexity.ProgTag.oneN = ⊤
• DescriptiveComplexity.CodeProgRed.arg1Body V cP x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.CodeProgRed.arg2Body {L : FirstOrder.Language} (V : L.FinVocab) (cP : Nat.Partrec.Code) : ProgTag V cP → ProgTag V cP → (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (dimOf V))

The body of the second-child relation, one case per pair of tags.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.CodeProgRed.arg2Body V cP DescriptiveComplexity.ProgTag.root DescriptiveComplexity.ProgTag.pairN = ⊤
• DescriptiveComplexity.CodeProgRed.arg2Body V cP (DescriptiveComplexity.ProgTag.cp p) (DescriptiveComplexity.ProgTag.cp q) = if DescriptiveComplexity.sub2 cP p = some q then ⊤ else ⊥
• DescriptiveComplexity.CodeProgRed.arg2Body V cP DescriptiveComplexity.ProgTag.pairN (DescriptiveComplexity.ProgTag.symN i) = if ↑i = 0 then ⊤ else ⊥
• DescriptiveComplexity.CodeProgRed.arg2Body V cP DescriptiveComplexity.ProgTag.pairN DescriptiveComplexity.ProgTag.zeroN = if V.numSyms = 0 then ⊤ else ⊥
• DescriptiveComplexity.CodeProgRed.arg2Body V cP (DescriptiveComplexity.ProgTag.symN i) (DescriptiveComplexity.ProgTag.symN i') = if ↑i' = ↑i + 1 then ⊤ else ⊥
• DescriptiveComplexity.CodeProgRed.arg2Body V cP (DescriptiveComplexity.ProgTag.symN i) DescriptiveComplexity.ProgTag.zeroN = if ↑i + 1 = V.numSyms then ⊤ else ⊥
• DescriptiveComplexity.CodeProgRed.arg2Body V cP (DescriptiveComplexity.ProgTag.chainN i l) DescriptiveComplexity.ProgTag.zeroN = DescriptiveComplexity.CodeProgRed.maxAF l
• DescriptiveComplexity.CodeProgRed.arg2Body V cP x✝¹ x✝ = ⊥

The defining formulas

noncomputable def DescriptiveComplexity.CodeProgRed.guardF {L : FirstOrder.Language} (V : L.FinVocab) (cP : Nat.Partrec.Code) {γ : Type} (sel : Fin (dimOf V) → γ) (t : ProgTag V cP) : (L.sum FirstOrder.Language.order).Formula γ

The guard of a tag on the argument selected by sel: the coordinates it does not use are minima.

Equations

• DescriptiveComplexity.CodeProgRed.guardF V cP sel t = DescriptiveComplexity.canonF t.used sel

noncomputable def DescriptiveComplexity.CodeProgRed.markF {L : FirstOrder.Language} (V : L.FinVocab) (cP : Nat.Partrec.Code) (s : CodeTag) (t : ProgTag V cP) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (dimOf V))

The mark of a constructor, as a formula: the tag draws it, and the argument is canonically padded.

Equations

• DescriptiveComplexity.CodeProgRed.markF V cP s t = if t.mark = s then DescriptiveComplexity.CodeProgRed.guardF V cP (DescriptiveComplexity.CodeProgRed.sel₀ V) t else ⊥

noncomputable def DescriptiveComplexity.CodeProgRed.rootMarkF {L : FirstOrder.Language} (V : L.FinVocab) (cP : Nat.Partrec.Code) (t : ProgTag V cP) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin (dimOf V))

Being the root, as a formula.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.CodeProgRed.rootMarkF V cP t = ⊥

noncomputable def DescriptiveComplexity.CodeProgRed.arg1F {L : FirstOrder.Language} (V : L.FinVocab) (cP : Nat.Partrec.Code) (t t' : ProgTag V cP) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (dimOf V))

The first-child relation, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.CodeProgRed.arg2F {L : FirstOrder.Language} (V : L.FinVocab) (cP : Nat.Partrec.Code) (t t' : ProgTag V cP) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin (dimOf V))

The second-child relation, as a formula.

Equations

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

The interpretation

noncomputable def DescriptiveComplexity.codeProgInterp {L : FirstOrder.Language} (V : L.FinVocab) (cP : Nat.Partrec.Code) : FOInterpretation (L.sum FirstOrder.Language.order) FirstOrder.Language.code (ProgTag V cP) (dimOf V)

The interpretation drawing an instance as a program: the root of the drawn code composes the fixed procedure cP with the pair of the numeral of the universe size and the nest of the tables.

Equations

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

The semantics of the drawing

def DescriptiveComplexity.progPt {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} (t : ProgTag V cP) (u : Fin (dimOf V) → A) : (codeProgInterp V cP).Map A

The element of the drawn instance with a given tag and tuple.

Equations

• DescriptiveComplexity.progPt t u = (t, u)

theorem DescriptiveComplexity.exists_progPt {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} (q : (codeProgInterp V cP).Map A) : ∃ (t : ProgTag V cP) (u : Fin (dimOf V) → A), q = progPt t u

def DescriptiveComplexity.OkOn {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [LinearOrder A] (t : ProgTag V cP) (u : Fin (dimOf V) → A) : Prop

The guard of an element: the coordinates its tag does not use are minima. Elements failing it carry no mark and no child, so they draw nothing.

Equations

• DescriptiveComplexity.OkOn t u = DescriptiveComplexity.Canon t.used u

def DescriptiveComplexity.Arg1On {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [L.Structure A] [LinearOrder A] : ProgTag V cP → ProgTag V cP → (Fin (dimOf V) → A) → (Fin (dimOf V) → A) → Prop

The first-child relation of the drawing, one case per pair of tags.

Equations

• DescriptiveComplexity.Arg1On DescriptiveComplexity.ProgTag.root (DescriptiveComplexity.ProgTag.cp p) x✝¹ x✝ = (p = DescriptiveComplexity.codeRootPos cP)
• DescriptiveComplexity.Arg1On (DescriptiveComplexity.ProgTag.cp p) (DescriptiveComplexity.ProgTag.cp q) x✝¹ x✝ = (DescriptiveComplexity.sub1 cP p = some q)
• DescriptiveComplexity.Arg1On DescriptiveComplexity.ProgTag.pairN DescriptiveComplexity.ProgTag.numN x✝¹ x✝ = IsBot (x✝ (DescriptiveComplexity.CodeProgRed.fz V))
• DescriptiveComplexity.Arg1On DescriptiveComplexity.ProgTag.numN DescriptiveComplexity.ProgTag.oneN x✝¹ x✝ = True
• DescriptiveComplexity.Arg1On (DescriptiveComplexity.ProgTag.symN i) (DescriptiveComplexity.ProgTag.chainN i' l) x✝¹ x✝ = ((i = i' ∧ ↑l = 0) ∧ IsBot (x✝ (DescriptiveComplexity.CodeProgRed.fz V)))
• DescriptiveComplexity.Arg1On (DescriptiveComplexity.ProgTag.chainN i l) (DescriptiveComplexity.ProgTag.chainN i' l') x✝¹ x✝ = ((i = i' ∧ ↑l' = ↑l + 1) ∧ x✝ = x✝¹)
• DescriptiveComplexity.Arg1On (DescriptiveComplexity.ProgTag.chainN i l) DescriptiveComplexity.ProgTag.oneN x✝¹ x✝ = (↑l + 1 = DescriptiveComplexity.dimOf V ∧ DescriptiveComplexity.bitOf V i x✝¹)
• DescriptiveComplexity.Arg1On (DescriptiveComplexity.ProgTag.chainN i l) DescriptiveComplexity.ProgTag.zeroN x✝¹ x✝ = (↑l + 1 = DescriptiveComplexity.dimOf V ∧ ¬DescriptiveComplexity.bitOf V i x✝¹)
• DescriptiveComplexity.Arg1On x✝³ x✝² x✝¹ x✝ = False

def DescriptiveComplexity.Arg2On {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [LinearOrder A] : ProgTag V cP → ProgTag V cP → (Fin (dimOf V) → A) → (Fin (dimOf V) → A) → Prop

The second-child relation of the drawing, one case per pair of tags.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Arg2On DescriptiveComplexity.ProgTag.root DescriptiveComplexity.ProgTag.pairN x✝¹ x✝ = True
• DescriptiveComplexity.Arg2On (DescriptiveComplexity.ProgTag.cp p) (DescriptiveComplexity.ProgTag.cp q) x✝¹ x✝ = (DescriptiveComplexity.sub2 cP p = some q)
• DescriptiveComplexity.Arg2On DescriptiveComplexity.ProgTag.pairN (DescriptiveComplexity.ProgTag.symN i) x✝¹ x✝ = (↑i = 0)
• DescriptiveComplexity.Arg2On DescriptiveComplexity.ProgTag.pairN DescriptiveComplexity.ProgTag.zeroN x✝¹ x✝ = (V.numSyms = 0)
• DescriptiveComplexity.Arg2On DescriptiveComplexity.ProgTag.numN DescriptiveComplexity.ProgTag.zeroN x✝¹ x✝ = IsTop (x✝¹ (DescriptiveComplexity.CodeProgRed.fz V))
• DescriptiveComplexity.Arg2On (DescriptiveComplexity.ProgTag.symN i) (DescriptiveComplexity.ProgTag.symN i') x✝¹ x✝ = (↑i' = ↑i + 1)
• DescriptiveComplexity.Arg2On (DescriptiveComplexity.ProgTag.symN i) DescriptiveComplexity.ProgTag.zeroN x✝¹ x✝ = (↑i + 1 = V.numSyms)
• DescriptiveComplexity.Arg2On (DescriptiveComplexity.ProgTag.chainN i l) DescriptiveComplexity.ProgTag.zeroN x✝¹ x✝ = IsTop (x✝¹ l)
• DescriptiveComplexity.Arg2On x✝³ x✝² x✝¹ x✝ = False

Characterization of the interpreted relations

theorem DescriptiveComplexity.realize_arg1Body {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [L.Structure A] [LinearOrder A] (t t' : ProgTag V cP) (u u' : Fin (dimOf V) → A) (v : Fin 2 × Fin (dimOf V) → A) (hA : ∀ (j : Fin (dimOf V)), v (CodeProgRed.selA V j) = u j) (hB : ∀ (j : Fin (dimOf V)), v (CodeProgRed.selB V j) = u' j) : (CodeProgRed.arg1Body V cP t t').Realize v ↔ Arg1On t t' u u'

theorem DescriptiveComplexity.realize_arg2Body {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [L.Structure A] [LinearOrder A] (t t' : ProgTag V cP) (u u' : Fin (dimOf V) → A) (v : Fin 2 × Fin (dimOf V) → A) (hA : ∀ (j : Fin (dimOf V)), v (CodeProgRed.selA V j) = u j) (hB : ∀ (j : Fin (dimOf V)), v (CodeProgRed.selB V j) = u' j) : (CodeProgRed.arg2Body V cP t t').Realize v ↔ Arg2On t t' u u'

theorem DescriptiveComplexity.cRoot_pt {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [L.Structure A] [LinearOrder A] (t : ProgTag V cP) (u : Fin (dimOf V) → A) : CRoot (progPt t u) ↔ OkOn t u ∧ t = ProgTag.root

theorem DescriptiveComplexity.mark_pt {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [L.Structure A] [LinearOrder A] (s : CodeTag) (t : ProgTag V cP) (u : Fin (dimOf V) → A) : Mark s (progPt t u) ↔ OkOn t u ∧ t.mark = s

theorem DescriptiveComplexity.cArg1_pt {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [L.Structure A] [LinearOrder A] (t t' : ProgTag V cP) (u u' : Fin (dimOf V) → A) : CArg1 (progPt t u) (progPt t' u') ↔ OkOn t u ∧ OkOn t' u' ∧ Arg1On t t' u u'

theorem DescriptiveComplexity.cArg2_pt {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [L.Structure A] [LinearOrder A] (t t' : ProgTag V cP) (u u' : Fin (dimOf V) → A) : CArg2 (progPt t u) (progPt t' u') ↔ OkOn t u ∧ OkOn t' u' ∧ Arg2On t t' u u'