CODEHALT: does the partial recursive code drawn in the instance halt?

The instance is a syntax tree, drawn with one element per node: a node carries one of the eight constructor marks of Nat.Partrec.Code, and its children are named by two binary symbols. The yes-instances are those whose root draws a code that halts on input 0.

This is the catalog problem the undecidability of the whole development goes through. Its point is that the passage from Mathlib's halting problem to an instance is a plain tree encoding – DescriptiveComplexity.codeStruct, in DescriptiveComplexity.Computability.CodeHalt – rather than the simulation of a machine: the code is the instance, and only the computation has to be guessed. That is what makes the map c ↦ instance primitive recursive, which the machine route could not deliver: Mathlib's universal machine is not finite-state, so a machine instance cannot carry the program it runs.

The semantics

DescriptiveComplexity.DecodesTo relates a node of the instance to a Nat.Partrec.Code, by recursion on the code: a node decodes to zero when it carries the zero mark, to pair cf cg when it carries the pair mark and its two children decode to cf and cg, and so on. A yes-instance is one whose root decodes to a code halting on 0.

Reading the semantics off an existential over codes, rather than as a fixed point computed inside the instance, is what keeps this file small: the encoding direction is then immediate, and the converse needs only that decoding is unique (DescriptiveComplexity.decodesTo_unique), which holds as soon as the marks are exclusive and the child relations are functional (DescriptiveComplexity.CodeWF).

inductive FirstOrder.Language.codeRel : ℕ → Type

Relation symbols of code instances.

• croot : codeRel 1

  croot n: n is the root of the syntax tree.

• czero : codeRel 1

  czero n: n draws the constructor zero.

• csucc : codeRel 1

  csucc n: n draws the constructor succ.

• cleft : codeRel 1

  cleft n: n draws the constructor left.

• cright : codeRel 1

  cright n: n draws the constructor right.

• cpair : codeRel 1

  cpair n: n draws the constructor pair.

• ccomp : codeRel 1

  ccomp n: n draws the constructor comp.

• cprec : codeRel 1

  cprec n: n draws the constructor prec.

• crfind : codeRel 1

  crfind n: n draws the constructor rfind'.

• carg1 : codeRel 2

  carg1 n m: m is the first child of n.

• carg2 : codeRel 2

  carg2 n m: m is the second child of n.

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqCodeRel {a✝ : ℕ} : DecidableEq (codeRel a✝)

Equations

• FirstOrder.Language.instDecidableEqCodeRel = FirstOrder.Language.instDecidableEqCodeRel.decEq

def FirstOrder.Language.instDecidableEqCodeRel.decEq {a✝ : ℕ} (x✝ x✝¹ : codeRel a✝) : Decidable (x✝ = x✝¹)

Equations

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

def FirstOrder.Language.code : Language

The relational language of code instances: the eight constructor marks, the mark of the root, and the two child relations.

Equations

• FirstOrder.Language.code = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.codeRel }

instance FirstOrder.Language.instIsRelationalCode : Language.code.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.cRoot : Language.code.Relations 1

The root symbol.

Equations

• FirstOrder.Language.cRoot = FirstOrder.Language.codeRel.croot

@[reducible, inline]

abbrev FirstOrder.Language.cZero : Language.code.Relations 1

The zero symbol.

Equations

• FirstOrder.Language.cZero = FirstOrder.Language.codeRel.czero

@[reducible, inline]

abbrev FirstOrder.Language.cSucc : Language.code.Relations 1

The succ symbol.

Equations

• FirstOrder.Language.cSucc = FirstOrder.Language.codeRel.csucc

@[reducible, inline]

abbrev FirstOrder.Language.cLeft : Language.code.Relations 1

The left symbol.

Equations

• FirstOrder.Language.cLeft = FirstOrder.Language.codeRel.cleft

@[reducible, inline]

abbrev FirstOrder.Language.cRight : Language.code.Relations 1

The right symbol.

Equations

• FirstOrder.Language.cRight = FirstOrder.Language.codeRel.cright

@[reducible, inline]

abbrev FirstOrder.Language.cPair : Language.code.Relations 1

The pair symbol.

Equations

• FirstOrder.Language.cPair = FirstOrder.Language.codeRel.cpair

@[reducible, inline]

abbrev FirstOrder.Language.cComp : Language.code.Relations 1

The comp symbol.

Equations

• FirstOrder.Language.cComp = FirstOrder.Language.codeRel.ccomp

@[reducible, inline]

abbrev FirstOrder.Language.cPrec : Language.code.Relations 1

The prec symbol.

Equations

• FirstOrder.Language.cPrec = FirstOrder.Language.codeRel.cprec

@[reducible, inline]

abbrev FirstOrder.Language.cRfind : Language.code.Relations 1

The rfind' symbol.

Equations

• FirstOrder.Language.cRfind = FirstOrder.Language.codeRel.crfind

@[reducible, inline]

abbrev FirstOrder.Language.cArg1 : Language.code.Relations 2

The first-child symbol.

Equations

• FirstOrder.Language.cArg1 = FirstOrder.Language.codeRel.carg1

@[reducible, inline]

abbrev FirstOrder.Language.cArg2 : Language.code.Relations 2

The second-child symbol.

Equations

• FirstOrder.Language.cArg2 = FirstOrder.Language.codeRel.carg2

The shorthands of the vocabulary

def DescriptiveComplexity.CRoot {A : Type} [FirstOrder.Language.code.Structure A] (a : A) : Prop

Being the root.

Equations

• DescriptiveComplexity.CRoot a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.cRoot ![a]

def DescriptiveComplexity.CZero {A : Type} [FirstOrder.Language.code.Structure A] (a : A) : Prop

Drawing the constructor zero.

Equations

• DescriptiveComplexity.CZero a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.cZero ![a]

def DescriptiveComplexity.CSucc {A : Type} [FirstOrder.Language.code.Structure A] (a : A) : Prop

Drawing the constructor succ.

Equations

• DescriptiveComplexity.CSucc a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.cSucc ![a]

def DescriptiveComplexity.CLeft {A : Type} [FirstOrder.Language.code.Structure A] (a : A) : Prop

Drawing the constructor left.

Equations

• DescriptiveComplexity.CLeft a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.cLeft ![a]

def DescriptiveComplexity.CRight {A : Type} [FirstOrder.Language.code.Structure A] (a : A) : Prop

Drawing the constructor right.

Equations

• DescriptiveComplexity.CRight a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.cRight ![a]

def DescriptiveComplexity.CPair {A : Type} [FirstOrder.Language.code.Structure A] (a : A) : Prop

Drawing the constructor pair.

Equations

• DescriptiveComplexity.CPair a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.cPair ![a]

def DescriptiveComplexity.CComp {A : Type} [FirstOrder.Language.code.Structure A] (a : A) : Prop

Drawing the constructor comp.

Equations

• DescriptiveComplexity.CComp a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.cComp ![a]

def DescriptiveComplexity.CPrec {A : Type} [FirstOrder.Language.code.Structure A] (a : A) : Prop

Drawing the constructor prec.

Equations

• DescriptiveComplexity.CPrec a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.cPrec ![a]

def DescriptiveComplexity.CRfind {A : Type} [FirstOrder.Language.code.Structure A] (a : A) : Prop

Drawing the constructor rfind'.

Equations

• DescriptiveComplexity.CRfind a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.cRfind ![a]

def DescriptiveComplexity.CArg1 {A : Type} [FirstOrder.Language.code.Structure A] (a b : A) : Prop

Being the first child.

Equations

• DescriptiveComplexity.CArg1 a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.cArg1 ![a, b]

def DescriptiveComplexity.CArg2 {A : Type} [FirstOrder.Language.code.Structure A] (a b : A) : Prop

Being the second child.

Equations

• DescriptiveComplexity.CArg2 a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.cArg2 ![a, b]

Decoding a node into a code

inductive DescriptiveComplexity.CodeTag : Type

The eight constructors of Nat.Partrec.Code, as a tag. Naming them makes the exclusivity of the marks one statement instead of twenty-eight, and the uniqueness of decoding a uniform argument instead of sixty-four cases.

• zero : CodeTag

  The tag of zero.

• succ : CodeTag

  The tag of succ.

• left : CodeTag

  The tag of left.

• right : CodeTag

  The tag of right.

• pair : CodeTag

  The tag of pair.

• comp : CodeTag

  The tag of comp.

• prec : CodeTag

  The tag of prec.

• rfind : CodeTag

  The tag of rfind'.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqCodeTag : DecidableEq CodeTag

Equations

• DescriptiveComplexity.instDecidableEqCodeTag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DescriptiveComplexity.Mark {A : Type} [FirstOrder.Language.code.Structure A] : CodeTag → A → Prop

The mark a tag stands for.

Equations

• DescriptiveComplexity.Mark DescriptiveComplexity.CodeTag.zero = DescriptiveComplexity.CZero
• DescriptiveComplexity.Mark DescriptiveComplexity.CodeTag.succ = DescriptiveComplexity.CSucc
• DescriptiveComplexity.Mark DescriptiveComplexity.CodeTag.left = DescriptiveComplexity.CLeft
• DescriptiveComplexity.Mark DescriptiveComplexity.CodeTag.right = DescriptiveComplexity.CRight
• DescriptiveComplexity.Mark DescriptiveComplexity.CodeTag.pair = DescriptiveComplexity.CPair
• DescriptiveComplexity.Mark DescriptiveComplexity.CodeTag.comp = DescriptiveComplexity.CComp
• DescriptiveComplexity.Mark DescriptiveComplexity.CodeTag.prec = DescriptiveComplexity.CPrec
• DescriptiveComplexity.Mark DescriptiveComplexity.CodeTag.rfind = DescriptiveComplexity.CRfind

def DescriptiveComplexity.tagOf : Nat.Partrec.Code → CodeTag

The tag of a code.

Equations

• DescriptiveComplexity.tagOf Nat.Partrec.Code.zero = DescriptiveComplexity.CodeTag.zero
• DescriptiveComplexity.tagOf Nat.Partrec.Code.succ = DescriptiveComplexity.CodeTag.succ
• DescriptiveComplexity.tagOf Nat.Partrec.Code.left = DescriptiveComplexity.CodeTag.left
• DescriptiveComplexity.tagOf Nat.Partrec.Code.right = DescriptiveComplexity.CodeTag.right
• DescriptiveComplexity.tagOf (a.pair a_1) = DescriptiveComplexity.CodeTag.pair
• DescriptiveComplexity.tagOf (a.comp a_1) = DescriptiveComplexity.CodeTag.comp
• DescriptiveComplexity.tagOf (a.prec a_1) = DescriptiveComplexity.CodeTag.prec
• DescriptiveComplexity.tagOf a.rfind' = DescriptiveComplexity.CodeTag.rfind

def DescriptiveComplexity.DecodesTo {A : Type} [FirstOrder.Language.code.Structure A] (n : A) : Nat.Partrec.Code → Prop

The node n draws the code c. A recursion on the code: the mark of the node must be the constructor's, and its children must draw the constructor's arguments.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.DecodesTo n Nat.Partrec.Code.zero = DescriptiveComplexity.CZero n
• DescriptiveComplexity.DecodesTo n Nat.Partrec.Code.succ = DescriptiveComplexity.CSucc n
• DescriptiveComplexity.DecodesTo n Nat.Partrec.Code.left = DescriptiveComplexity.CLeft n
• DescriptiveComplexity.DecodesTo n Nat.Partrec.Code.right = DescriptiveComplexity.CRight n
• DescriptiveComplexity.DecodesTo n a.rfind' = (DescriptiveComplexity.CRfind n ∧ ∃ (a_1 : A), DescriptiveComplexity.CArg1 n a_1 ∧ DescriptiveComplexity.DecodesTo a_1 a)

theorem DescriptiveComplexity.decodesTo_mark {A : Type} [FirstOrder.Language.code.Structure A] (c : Nat.Partrec.Code) (n : A) : DecodesTo n c → Mark (tagOf c) n

structure DescriptiveComplexity.CodeWF (A : Type) [FirstOrder.Language.code.Structure A] : Prop

Well-formedness of a code instance: at most one constructor mark per node, and functional child relations. This is what makes decoding unique; it is not folded into the yes-instances, because the problem is stated by an existential over codes and a junk instance simply decodes to nothing.

• exclusive (a : A) (t t' : CodeTag) : Mark t a → Mark t' a → t = t'

  At most one constructor mark per node.

• arg1_fun (a b b' : A) : CArg1 a b → CArg1 a b' → b = b'

  The first child is unique.

• arg2_fun (a b b' : A) : CArg2 a b → CArg2 a b' → b = b'

  The second child is unique.

theorem DescriptiveComplexity.tag_eq_of_decodesTo {A : Type} [FirstOrder.Language.code.Structure A] (h : CodeWF A) {c c' : Nat.Partrec.Code} {n : A} (h1 : DecodesTo n c) (h2 : DecodesTo n c') : tagOf c = tagOf c'

theorem DescriptiveComplexity.decodesTo_unique {A : Type} [FirstOrder.Language.code.Structure A] (h : CodeWF A) (c c' : Nat.Partrec.Code) (n : A) : DecodesTo n c → DecodesTo n c' → c = c'

Decoding is unique on a well-formed instance.

Isomorphism-invariance

theorem DescriptiveComplexity.decodesTo_equiv {A B : Type} [FirstOrder.Language.code.Structure A] [FirstOrder.Language.code.Structure B] (e : FirstOrder.Language.code.Equiv A B) (c : Nat.Partrec.Code) (n : A) : DecodesTo n c ↔ DecodesTo (e n) c

Decoding transports along an isomorphism: what a node draws is a first-order property of the instance.

The problem

def DescriptiveComplexity.CODEHALT : DecisionProblem FirstOrder.Language.code

CODEHALT: does the partial recursive code drawn by the root of the instance halt on input 0?

The yes-instances are stated by an existential over Nat.Partrec.Code: some node is the root, it draws some code, and that code halts on 0. Nothing is promised of the instance, so a junk one simply draws nothing and is a no-instance.

Equations

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

@[simp]

theorem DescriptiveComplexity.codehalt_holds_iff (A : Type) [FirstOrder.Language.code.Structure A] : CODEHALT.Holds A ↔ ∃ (n : A) (c : Nat.Partrec.Code), CRoot n ∧ DecodesTo n c ∧ (c.eval 0).Dom