A halting computation, read off as a finite certificate

The mathematical content of CODEHALT ∈ RE: the code drawn by an instance halts on 0 exactly when a finite amount of data witnesses it – a numeral segment with a linear order on it, an addition and a pairing on the segment, the number of the code each node draws, and the value each code takes on each argument.

The shape of the certificate

DescriptiveComplexity.CodeHalt.Cert is the data and DescriptiveComplexity.CodeHalt.CertOK the conditions. Every condition but the last is a justification rule: each fact asserted must be derivable from facts already asserted, by one of the rules of the object it is about. Nothing asks the guessed relations to be closed under the rules – only supported by them – and nothing needs a rank, because two things already decrease:

• the numeral of a code: the arguments of a pair, comp, prec or rfind' are numbered below it (DescriptiveComplexity.CodeHalt.dec_pair and friends), so a code's own rules appeal to strictly smaller numbers;
• the argument of a prec, which is the one rule appealing to the same code: it steps down along the second component of the argument.

So soundness is a plain induction on the pair (code number, argument), and the instance is not asked to be a well-formed tree: a code is carried by its number, and numbers decode unambiguously.

Why rfind' has no chain

The search of an rfind' is stated by a bounded universal: the answer v is a place where the argument returns 0, and every place between the input and v returns something nonzero (DescriptiveComplexity.CodeHalt.evaln_rfind'_spec). A step-by-step reading would appeal to the same code at a larger argument, which no measure decreases along; the universal reading appeals only to the argument's code.

The certificate

structure DescriptiveComplexity.CodeHalt.Cert (A D : Type) : Type

A halting computation, as relations on a numeral segment. Le orders the segment; Add and Pr are addition and Nat.pair on it; Dec n e says the node n of the instance draws the code numbered e; Ev e x v says the code numbered e returns v on x.

• Le : D → D → Prop

  The order of the numeral segment.

• Add : D → D → D → Prop

  Add x y z: x + y = z.

• Pr : D → D → D → Prop

  Pr a b p: ⟨a, b⟩ = p, for Cantor's pairing.

• Dec : A → D → Prop

  Dec n e: the node n draws the code numbered e.

• Ev : D → D → D → Prop

  Ev e x v: the code numbered e returns v on the argument x.

def DescriptiveComplexity.CodeHalt.Cert.Lt {A D : Type} (c : Cert A D) (x y : D) : Prop

Strictly below, in the numeral segment.

Equations

• c.Lt x y = (c.Le x y ∧ x ≠ y)

def DescriptiveComplexity.CodeHalt.Cert.Quad {A D : Type} (c : Cert A D) (p q : D) : Prop

q is four times p.

Equations

• c.Quad p q = ∃ (s : D), c.Add p p s ∧ c.Add s s q

def DescriptiveComplexity.CodeHalt.Cert.Plus4 {A D : Type} (c : Cert A D) (q e : D) : Prop

e is q + 4.

Equations

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

def DescriptiveComplexity.CodeHalt.Cert.Plus5 {A D : Type} (c : Cert A D) (q e : D) : Prop

e is q + 5.

Equations

• c.Plus5 q e = ∃ (u : D), c.Plus4 q u ∧ DescriptiveComplexity.CodeHalt.IsS c.Le u e

def DescriptiveComplexity.CodeHalt.Cert.Plus6 {A D : Type} (c : Cert A D) (q e : D) : Prop

e is q + 6.

Equations

• c.Plus6 q e = ∃ (u : D), c.Plus5 q u ∧ DescriptiveComplexity.CodeHalt.IsS c.Le u e

def DescriptiveComplexity.CodeHalt.Cert.Plus7 {A D : Type} (c : Cert A D) (q e : D) : Prop

e is q + 7.

Equations

• c.Plus7 q e = ∃ (u : D), c.Plus6 q u ∧ DescriptiveComplexity.CodeHalt.IsS c.Le u e

def DescriptiveComplexity.CodeHalt.Cert.IsOne {A D : Type} (c : Cert A D) (e : D) : Prop

e is the numeral 1.

Equations

• c.IsOne e = ∃ (z : D), DescriptiveComplexity.CodeHalt.IsZ c.Le z ∧ DescriptiveComplexity.CodeHalt.IsS c.Le z e

def DescriptiveComplexity.CodeHalt.Cert.IsTwo {A D : Type} (c : Cert A D) (e : D) : Prop

e is the numeral 2.

Equations

• c.IsTwo e = ∃ (u : D), c.IsOne u ∧ DescriptiveComplexity.CodeHalt.IsS c.Le u e

def DescriptiveComplexity.CodeHalt.Cert.IsThree {A D : Type} (c : Cert A D) (e : D) : Prop

e is the numeral 3.

Equations

• c.IsThree e = ∃ (u : D), c.IsTwo u ∧ DescriptiveComplexity.CodeHalt.IsS c.Le u e

def DescriptiveComplexity.CodeHalt.Cert.IsPairE {A D : Type} (c : Cert A D) (e e₁ e₂ : D) : Prop

e numbers the code pair e₁ e₂.

Equations

• c.IsPairE e e₁ e₂ = ∃ (p : D) (q : D), c.Pr e₁ e₂ p ∧ c.Quad p q ∧ c.Plus4 q e

def DescriptiveComplexity.CodeHalt.Cert.IsPrecE {A D : Type} (c : Cert A D) (e e₁ e₂ : D) : Prop

e numbers the code prec e₁ e₂.

Equations

• c.IsPrecE e e₁ e₂ = ∃ (p : D) (q : D), c.Pr e₁ e₂ p ∧ c.Quad p q ∧ c.Plus5 q e

def DescriptiveComplexity.CodeHalt.Cert.IsCompE {A D : Type} (c : Cert A D) (e e₁ e₂ : D) : Prop

e numbers the code comp e₁ e₂.

Equations

• c.IsCompE e e₁ e₂ = ∃ (p : D) (q : D), c.Pr e₁ e₂ p ∧ c.Quad p q ∧ c.Plus6 q e

def DescriptiveComplexity.CodeHalt.Cert.IsRfindE {A D : Type} (c : Cert A D) (e e₁ : D) : Prop

e numbers the code rfind' e₁.

Equations

• c.IsRfindE e e₁ = ∃ (q : D), c.Quad e₁ q ∧ c.Plus7 q e

def DescriptiveComplexity.CodeHalt.Cert.NextPR {A D : Type} (c : Cert A D) (a' b' a b : D) : Prop

The successor rule of the pairing, on the segment: this is DescriptiveComplexity.CodeHalt.NextP with the arithmetic replaced by the guessed order.

Equations

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

def DescriptiveComplexity.CodeHalt.Cert.DecStep {A D : Type} (c : Cert A D) [FirstOrder.Language.code.Structure A] (n : A) (e : D) : Prop

What justifies “the node n draws the code numbered e”: the constructor mark of n, and – for the four binary constructors – children drawing the codes the number of e is built from.

Equations

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

def DescriptiveComplexity.CodeHalt.Cert.EvStep {A D : Type} (c : Cert A D) (e x v : D) : Prop

What justifies “the code numbered e returns v on x”: one clause per constructor, mirroring Nat.Partrec.Code.eval. The prec clause is the only one appealing to e itself, and it does so at a strictly smaller argument; the rfind' clause states its search by a bounded universal.

Equations

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

structure DescriptiveComplexity.CodeHalt.CertOK {A D : Type} [FirstOrder.Language.code.Structure A] (c : Cert A D) : Prop

The conditions making the guessed relations a halting computation. Four justification rules and the root clause; the segment's order is linear, and that is the only shape condition, all the rest being support.

• le_lin : IsLinOrd c.Le

  The numeral segment is linearly ordered.

• add_ok (x y z : D) : c.Add x y z → IsZ c.Le y ∧ z = x ∨ ∃ (y' : D) (z' : D), IsS c.Le y' y ∧ IsS c.Le z' z ∧ c.Add x y' z'

  Every addition fact is justified by the recurrence.

• pr_ok (a b p : D) : c.Pr a b p → IsZ c.Le p ∧ IsZ c.Le a ∧ IsZ c.Le b ∨ ∃ (p' : D) (a' : D) (b' : D), IsS c.Le p' p ∧ c.Pr a' b' p' ∧ c.NextPR a' b' a b

  Every pairing fact is justified by the successor rule.

• dec_ok (n : A) (e : D) : c.Dec n e → c.DecStep n e

  Every decoding fact is justified by the node's mark and its children.

• ev_ok (e x v : D) : c.Ev e x v → c.EvStep e x v

  Every evaluation fact is justified by the rules of its code.

• root : ∃ (n : A) (e : D) (z : D) (v : D), CRoot n ∧ c.Dec n e ∧ IsZ c.Le z ∧ c.Ev e z v

  The root draws a code that returns something on 0.

Soundness: a certificate really is a halting computation

Every guessed relation means what its name says, by induction along the two things a justification decreases: the numeral of a code, and – inside the one rule that keeps the code – the argument.

theorem DescriptiveComplexity.CodeHalt.lt_sound {A D : Type} [FirstOrder.Language.code.Structure A] [Finite D] {c : Cert A D} (h : CertOK c) {x y : D} : c.Lt x y ↔ numOf c.Le x < numOf c.Le y

theorem DescriptiveComplexity.CodeHalt.add_sound {A D : Type} [FirstOrder.Language.code.Structure A] [Finite D] {c : Cert A D} (h : CertOK c) (Y : ℕ) (x y z : D) : numOf c.Le y = Y → c.Add x y z → numOf c.Le x + numOf c.Le y = numOf c.Le z

theorem DescriptiveComplexity.CodeHalt.nextPR_sound {A D : Type} [FirstOrder.Language.code.Structure A] [Finite D] {c : Cert A D} (h : CertOK c) {a' b' a b : D} (hn : c.NextPR a' b' a b) : NextP (numOf c.Le a') (numOf c.Le b') (numOf c.Le a) (numOf c.Le b)

theorem DescriptiveComplexity.CodeHalt.pr_sound {A D : Type} [FirstOrder.Language.code.Structure A] [Finite D] {c : Cert A D} (h : CertOK c) (P : ℕ) (a b p : D) : numOf c.Le p = P → c.Pr a b p → Nat.pair (numOf c.Le a) (numOf c.Le b) = numOf c.Le p

theorem DescriptiveComplexity.CodeHalt.quad_sound {A D : Type} [FirstOrder.Language.code.Structure A] [Finite D] {c : Cert A D} (h : CertOK c) {p q : D} (hq : c.Quad p q) : numOf c.Le q = 4 * numOf c.Le p

theorem DescriptiveComplexity.CodeHalt.plus4_sound {A D : Type} [FirstOrder.Language.code.Structure A] [Finite D] {c : Cert A D} (h : CertOK c) {q e : D} (he : c.Plus4 q e) : numOf c.Le e = numOf c.Le q + 4

theorem DescriptiveComplexity.CodeHalt.plus5_sound {A D : Type} [FirstOrder.Language.code.Structure A] [Finite D] {c : Cert A D} (h : CertOK c) {q e : D} (he : c.Plus5 q e) : numOf c.Le e = numOf c.Le q + 5

theorem DescriptiveComplexity.CodeHalt.plus6_sound {A D : Type} [FirstOrder.Language.code.Structure A] [Finite D] {c : Cert A D} (h : CertOK c) {q e : D} (he : c.Plus6 q e) : numOf c.Le e = numOf c.Le q + 6

theorem DescriptiveComplexity.CodeHalt.plus7_sound {A D : Type} [FirstOrder.Language.code.Structure A] [Finite D] {c : Cert A D} (h : CertOK c) {q e : D} (he : c.Plus7 q e) : numOf c.Le e = numOf c.Le q + 7

theorem DescriptiveComplexity.CodeHalt.isOne_sound {A D : Type} [FirstOrder.Language.code.Structure A] [Finite D] {c : Cert A D} (h : CertOK c) {e : D} (he : c.IsOne e) : numOf c.Le e = 1

theorem DescriptiveComplexity.CodeHalt.isTwo_sound {A D : Type} [FirstOrder.Language.code.Structure A] [Finite D] {c : Cert A D} (h : CertOK c) {e : D} (he : c.IsTwo e) : numOf c.Le e = 2

theorem DescriptiveComplexity.CodeHalt.isThree_sound {A D : Type} [FirstOrder.Language.code.Structure A] [Finite D] {c : Cert A D} (h : CertOK c) {e : D} (he : c.IsThree e) : numOf c.Le e = 3

theorem DescriptiveComplexity.CodeHalt.isPairE_sound {A D : Type} [FirstOrder.Language.code.Structure A] [Finite D] {c : Cert A D} (h : CertOK c) {e e₁ e₂ : D} (he : c.IsPairE e e₁ e₂) : numOf c.Le e = 4 * Nat.pair (numOf c.Le e₁) (numOf c.Le e₂) + 4

theorem DescriptiveComplexity.CodeHalt.isPrecE_sound {A D : Type} [FirstOrder.Language.code.Structure A] [Finite D] {c : Cert A D} (h : CertOK c) {e e₁ e₂ : D} (he : c.IsPrecE e e₁ e₂) : numOf c.Le e = 4 * Nat.pair (numOf c.Le e₁) (numOf c.Le e₂) + 5

theorem DescriptiveComplexity.CodeHalt.isCompE_sound {A D : Type} [FirstOrder.Language.code.Structure A] [Finite D] {c : Cert A D} (h : CertOK c) {e e₁ e₂ : D} (he : c.IsCompE e e₁ e₂) : numOf c.Le e = 4 * Nat.pair (numOf c.Le e₁) (numOf c.Le e₂) + 6

theorem DescriptiveComplexity.CodeHalt.isRfindE_sound {A D : Type} [FirstOrder.Language.code.Structure A] [Finite D] {c : Cert A D} (h : CertOK c) {e e₁ : D} (he : c.IsRfindE e e₁) : numOf c.Le e = 4 * numOf c.Le e₁ + 7

theorem DescriptiveComplexity.CodeHalt.dec_sound {A D : Type} [FirstOrder.Language.code.Structure A] [Finite D] {c : Cert A D} (h : CertOK c) (E : ℕ) (n : A) (e : D) : numOf c.Le e = E → c.Dec n e → DecodesTo n (dec (numOf c.Le e))

The node really draws the code its number denotes.

theorem DescriptiveComplexity.CodeHalt.ev_sound {A D : Type} [FirstOrder.Language.code.Structure A] [Finite D] {c : Cert A D} (h : CertOK c) (E X : ℕ) (e x v : D) : numOf c.Le e = E → numOf c.Le x = X → c.Ev e x v → numOf c.Le v ∈ (dec (numOf c.Le e)).eval (numOf c.Le x)

The code really returns what the certificate says. The induction is on the pair (number of the code, argument), lexicographically: every rule but the recursive one of prec appeals to a strictly smaller code number, and that one appeals to the same code at a strictly smaller argument.

theorem DescriptiveComplexity.CodeHalt.holds_of_certOK {A D : Type} [FirstOrder.Language.code.Structure A] [Finite D] {c : Cert A D} (h : CertOK c) : CODEHALT.Holds A

A certificate exhibits a yes-instance.

Completeness: a halting computation is a certificate

The segment is Fin (N + 1), with N large enough to hold the number of the code, the step budget, and every value a bounded evaluation within that budget can return (DescriptiveComplexity.CodeHalt.valBound). That is the only place where finiteness of the certificate is at stake: every number the justification rules appeal to is either an argument of a bounded evaluation, hence below the budget, or one of its values, hence below the bound.

def DescriptiveComplexity.CodeHalt.numVal {N : ℕ} (a : ℕ) (h : a ≤ N) : Fin (N + 1)

A number at most N, as a value of the segment.

Equations

• DescriptiveComplexity.CodeHalt.numVal a h = ⟨a, ⋯⟩

@[simp]

theorem DescriptiveComplexity.CodeHalt.numVal_val {N a : ℕ} (h : a ≤ N) : ↑(numVal a h) = a

def DescriptiveComplexity.CodeHalt.finCert (A : Type) [FirstOrder.Language.code.Structure A] (E k N : ℕ) : Cert A (Fin (N + 1))

The certificate a halting bounded evaluation carries: numerals up to N, addition and pairing read off ℕ, the code each node draws, and the values a bounded evaluation with budget k returns for codes numbered at most E.

Equations

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

@[simp]

theorem DescriptiveComplexity.CodeHalt.finCert_add {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} {x y z : Fin (N + 1)} : (finCert A E k N).Add x y z ↔ ↑x + ↑y = ↑z

@[simp]

theorem DescriptiveComplexity.CodeHalt.finCert_pr {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} {a b p : Fin (N + 1)} : (finCert A E k N).Pr a b p ↔ Nat.pair ↑a ↑b = ↑p

@[simp]

theorem DescriptiveComplexity.CodeHalt.finCert_dec {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} {n : A} {e : Fin (N + 1)} : (finCert A E k N).Dec n e ↔ ∃ (c' : Nat.Partrec.Code), DecodesTo n c' ∧ c'.encodeCode = ↑e

@[simp]

theorem DescriptiveComplexity.CodeHalt.finCert_ev {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} {e x v : Fin (N + 1)} : (finCert A E k N).Ev e x v ↔ ↑e ≤ E ∧ ↑v ∈ Nat.Partrec.Code.evaln k (dec ↑e) ↑x

@[simp]

theorem DescriptiveComplexity.CodeHalt.finCert_isZ {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} {i : Fin (N + 1)} : IsZ (finCert A E k N).Le i ↔ ↑i = 0

@[simp]

theorem DescriptiveComplexity.CodeHalt.finCert_isS {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} {i j : Fin (N + 1)} : IsS (finCert A E k N).Le i j ↔ ↑j = ↑i + 1

@[simp]

theorem DescriptiveComplexity.CodeHalt.finCert_le {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} {i j : Fin (N + 1)} : (finCert A E k N).Le i j ↔ ↑i ≤ ↑j

@[simp]

theorem DescriptiveComplexity.CodeHalt.finCert_lt {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} {i j : Fin (N + 1)} : (finCert A E k N).Lt i j ↔ ↑i < ↑j

theorem DescriptiveComplexity.CodeHalt.finCert_quad {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} {p q : Fin (N + 1)} (hq : ↑q = 4 * ↑p) : (finCert A E k N).Quad p q

theorem DescriptiveComplexity.CodeHalt.finCert_plus4 {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} {q e : Fin (N + 1)} (he : ↑e = ↑q + 4) : (finCert A E k N).Plus4 q e

theorem DescriptiveComplexity.CodeHalt.finCert_plus5 {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} {q e : Fin (N + 1)} (he : ↑e = ↑q + 5) : (finCert A E k N).Plus5 q e

theorem DescriptiveComplexity.CodeHalt.finCert_plus6 {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} {q e : Fin (N + 1)} (he : ↑e = ↑q + 6) : (finCert A E k N).Plus6 q e

theorem DescriptiveComplexity.CodeHalt.finCert_plus7 {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} {q e : Fin (N + 1)} (he : ↑e = ↑q + 7) : (finCert A E k N).Plus7 q e

theorem DescriptiveComplexity.CodeHalt.finCert_isOne {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} {e : Fin (N + 1)} (he : ↑e = 1) : (finCert A E k N).IsOne e

theorem DescriptiveComplexity.CodeHalt.finCert_isTwo {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} {e : Fin (N + 1)} (he : ↑e = 2) : (finCert A E k N).IsTwo e

theorem DescriptiveComplexity.CodeHalt.finCert_isThree {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} {e : Fin (N + 1)} (he : ↑e = 3) : (finCert A E k N).IsThree e

theorem DescriptiveComplexity.CodeHalt.finCert_isPairE {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} {e e₁ e₂ : Fin (N + 1)} (he : ↑e = 4 * Nat.pair ↑e₁ ↑e₂ + 4) : (finCert A E k N).IsPairE e e₁ e₂

theorem DescriptiveComplexity.CodeHalt.finCert_isPrecE {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} {e e₁ e₂ : Fin (N + 1)} (he : ↑e = 4 * Nat.pair ↑e₁ ↑e₂ + 5) : (finCert A E k N).IsPrecE e e₁ e₂

theorem DescriptiveComplexity.CodeHalt.finCert_isCompE {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} {e e₁ e₂ : Fin (N + 1)} (he : ↑e = 4 * Nat.pair ↑e₁ ↑e₂ + 6) : (finCert A E k N).IsCompE e e₁ e₂

theorem DescriptiveComplexity.CodeHalt.finCert_isRfindE {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} {e e₁ : Fin (N + 1)} (he : ↑e = 4 * ↑e₁ + 7) : (finCert A E k N).IsRfindE e e₁

theorem DescriptiveComplexity.CodeHalt.finCert_nextPR {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} {a' b' a b : Fin (N + 1)} (h : NextP ↑a' ↑b' ↑a ↑b) : (finCert A E k N).NextPR a' b' a b

theorem DescriptiveComplexity.CodeHalt.certOK_finCert {A : Type} [FirstOrder.Language.code.Structure A] {E k N : ℕ} (hEN : E ≤ N) (hkN : k ≤ N) (hbN : valBound E k ≤ N) {n₀ : A} {c₀ : Nat.Partrec.Code} {v₀ : ℕ} (hroot : CRoot n₀) (hdec : DecodesTo n₀ c₀) (hE : c₀.encodeCode = E) (hv : v₀ ∈ Nat.Partrec.Code.evaln k c₀ 0) : CertOK (finCert A E k N)

A halting computation is a certificate.

theorem DescriptiveComplexity.CodeHalt.codehalt_iff_cert (A : Type) [FirstOrder.Language.code.Structure A] : CODEHALT.Holds A ↔ ∃ (m : ℕ) (c : Cert A (Fin m)), CertOK c

A yes-instance of CODEHALT is exactly one whose invented values carry a certificate. This is the mathematical content of CODEHALT ∈ RE; the syntax is in DescriptiveComplexity.Problems.CodeHalt.Membership.