Documentation

DescriptiveComplexity.Computability.CodeHalt

Drawing a partial recursive code as a concrete instance #

The computable half of the undecidability bridge: a primitive recursive map

Nat.Partrec.Code → FirstOrder.Language.FinStruct codeVocab

whose image is a yes-instance of DescriptiveComplexity.CODEHALT exactly when the code halts on 0 (DescriptiveComplexity.codehalt_toPred_codeStruct).

Nothing here simulates anything: the code is the instance, so the map is a plain tree flattening. DescriptiveComplexity.codeNodes lists the nodes of a code in preorder, each node carrying its constructor tag and the relative offsets of its children – relative, so that the flattening of a subterm is literally a segment of the flattening of the whole (DescriptiveComplexity.Seg), which is what makes the correctness proof an induction on the code and nothing more.

This is exactly what the machine route could not deliver. Mathlib's universal machine Turing.PartrecToTM2.tr is not finite-state, so code ↦ machine instance is not available; code ↦ syntax tree is trivially primitive recursive, and pushes the whole difficulty into CODEHALT ∈ RE, an ordinary membership proof of the catalog (DescriptiveComplexity.Problems.CodeHalt.Membership).

Whence the two results the layer exists for: DescriptiveComplexity.not_computablePred_of_RE_hard, every RE-hard problem is undecidable, and its first instance DescriptiveComplexity.finsat_not_computable, Trakhtenbrot's theorem.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqSigmaNatRelationsCode :

DecidableEq ((n : ℕ) × FirstOrder.Language.code.Relations n)

Equations

DescriptiveComplexity.instDecidableEqSigmaNatRelationsCode = DescriptiveComplexity.instDecidableEqSigmaNatRelationsCode._aux_1

Dependency graph

def DescriptiveComplexity.codeVocab :

FirstOrder.Language.code.FinVocab

The vocabulary of code instances, presented: eleven symbols, nine unary and two binary.

Equations

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

Instances For

Dependency graph

Flattening a code into a list of nodes #

def DescriptiveComplexity.nodeNone :

ℕ × ℕ × ℕ

The reading of an index outside the flattening: a tag no constructor carries, and no children.

Equations

DescriptiveComplexity.nodeNone = (8, 0, 0)

Instances For

Dependency graph

def DescriptiveComplexity.codeNodes :

Nat.Partrec.Code → List (ℕ × ℕ × ℕ)

The nodes of a code, in preorder. Each node carries its constructor tag and the offsets of its children relative to itself, 0 meaning "no such child". Relative offsets are what make the flattening of a subterm a segment of the flattening of the whole.

Equations

DescriptiveComplexity.codeNodes Nat.Partrec.Code.zero = [(0, 0, 0)]
DescriptiveComplexity.codeNodes Nat.Partrec.Code.succ = [(1, 0, 0)]
DescriptiveComplexity.codeNodes Nat.Partrec.Code.left = [(2, 0, 0)]
DescriptiveComplexity.codeNodes Nat.Partrec.Code.right = [(3, 0, 0)]
DescriptiveComplexity.codeNodes (cf.pair cg) = (4, 1, (DescriptiveComplexity.codeNodes cf).length + 1) :: (DescriptiveComplexity.codeNodes cf ++ DescriptiveComplexity.codeNodes cg)
DescriptiveComplexity.codeNodes (cf.comp cg) = (5, 1, (DescriptiveComplexity.codeNodes cf).length + 1) :: (DescriptiveComplexity.codeNodes cf ++ DescriptiveComplexity.codeNodes cg)
DescriptiveComplexity.codeNodes (cf.prec cg) = (6, 1, (DescriptiveComplexity.codeNodes cf).length + 1) :: (DescriptiveComplexity.codeNodes cf ++ DescriptiveComplexity.codeNodes cg)
DescriptiveComplexity.codeNodes cf.rfind' = (7, 1, 0) :: DescriptiveComplexity.codeNodes cf

Instances For

Dependency graph

theorem DescriptiveComplexity.flat_ne_nil (c : Nat.Partrec.Code) :

codeNodes c ≠ []

Dependency graph

theorem DescriptiveComplexity.flat_length_pos (c : Nat.Partrec.Code) :

0 < (codeNodes c).length

Dependency graph

Segments #

def DescriptiveComplexity.Seg (L M : List (ℕ × ℕ × ℕ)) (i : ℕ) :

Seg L M i: the list M sits inside L starting at index i.

Equations

DescriptiveComplexity.Seg L M i = (i + M.length ≤ L.length ∧ ∀ k < M.length, L.getD (i + k) DescriptiveComplexity.nodeNone = M.getD k DescriptiveComplexity.nodeNone)

Instances For

Dependency graph

theorem DescriptiveComplexity.seg_self (M : List (ℕ × ℕ × ℕ)) :

Seg M M 0

Dependency graph

theorem DescriptiveComplexity.Seg.head {L M : List (ℕ × ℕ × ℕ)} {i : ℕ} (h : Seg L M i) (hM : M ≠ []) :

L.getD i nodeNone = M.getD 0 nodeNone

Dependency graph

theorem DescriptiveComplexity.Seg.tail {L : List (ℕ × ℕ × ℕ)} {a : ℕ × ℕ × ℕ} {M : List (ℕ × ℕ × ℕ)} {i : ℕ} (h : Seg L (a :: M) i) :

Seg L M (i + 1)

Dependency graph

theorem DescriptiveComplexity.Seg.appendLeft {L M N : List (ℕ × ℕ × ℕ)} {i : ℕ} (h : Seg L (M ++ N) i) :

Seg L M i

Dependency graph

theorem DescriptiveComplexity.Seg.appendRight {L M N : List (ℕ × ℕ × ℕ)} {i : ℕ} (h : Seg L (M ++ N) i) :

Seg L N (i + M.length)

Dependency graph

The instance a code draws #

def DescriptiveComplexity.tagAt (L : List (ℕ × ℕ × ℕ)) (i : ℕ) :

The constructor tag of the node at index i.

Equations

DescriptiveComplexity.tagAt L i = (L.getD i DescriptiveComplexity.nodeNone).1

Instances For

Dependency graph

def DescriptiveComplexity.off1At (L : List (ℕ × ℕ × ℕ)) (i : ℕ) :

The offset of the first child of the node at index i, 0 for none.

Equations

DescriptiveComplexity.off1At L i = (L.getD i DescriptiveComplexity.nodeNone).2.1

Instances For

Dependency graph

def DescriptiveComplexity.off2At (L : List (ℕ × ℕ × ℕ)) (i : ℕ) :

The offset of the second child of the node at index i, 0 for none.

Equations

DescriptiveComplexity.off2At L i = (L.getD i DescriptiveComplexity.nodeNone).2.2

Instances For

Dependency graph

def DescriptiveComplexity.codeRelBool (L : List (ℕ × ℕ × ℕ)) {n : ℕ} :

FirstOrder.Language.code.Relations n → (Fin n → Fin (L.length + 1)) → Bool

The relations a list of nodes denotes.

Equations

DescriptiveComplexity.codeRelBool L FirstOrder.Language.codeRel.croot x_3 = decide (↑(x_3 0) = 0)
DescriptiveComplexity.codeRelBool L FirstOrder.Language.codeRel.czero x_3 = decide (DescriptiveComplexity.tagAt L ↑(x_3 0) = 0)
DescriptiveComplexity.codeRelBool L FirstOrder.Language.codeRel.csucc x_3 = decide (DescriptiveComplexity.tagAt L ↑(x_3 0) = 1)
DescriptiveComplexity.codeRelBool L FirstOrder.Language.codeRel.cleft x_3 = decide (DescriptiveComplexity.tagAt L ↑(x_3 0) = 2)
DescriptiveComplexity.codeRelBool L FirstOrder.Language.codeRel.cright x_3 = decide (DescriptiveComplexity.tagAt L ↑(x_3 0) = 3)
DescriptiveComplexity.codeRelBool L FirstOrder.Language.codeRel.cpair x_3 = decide (DescriptiveComplexity.tagAt L ↑(x_3 0) = 4)
DescriptiveComplexity.codeRelBool L FirstOrder.Language.codeRel.ccomp x_3 = decide (DescriptiveComplexity.tagAt L ↑(x_3 0) = 5)
DescriptiveComplexity.codeRelBool L FirstOrder.Language.codeRel.cprec x_3 = decide (DescriptiveComplexity.tagAt L ↑(x_3 0) = 6)
DescriptiveComplexity.codeRelBool L FirstOrder.Language.codeRel.crfind x_3 = decide (DescriptiveComplexity.tagAt L ↑(x_3 0) = 7)
DescriptiveComplexity.codeRelBool L FirstOrder.Language.codeRel.carg1 x_3 = decide (DescriptiveComplexity.off1At L ↑(x_3 0) ≠ 0 ∧ ↑(x_3 1) = ↑(x_3 0) + DescriptiveComplexity.off1At L ↑(x_3 0))
DescriptiveComplexity.codeRelBool L FirstOrder.Language.codeRel.carg2 x_3 = decide (DescriptiveComplexity.off2At L ↑(x_3 0) ≠ 0 ∧ ↑(x_3 1) = ↑(x_3 0) + DescriptiveComplexity.off2At L ↑(x_3 0))

Instances For

Dependency graph

def DescriptiveComplexity.listStruct (L : List (ℕ × ℕ × ℕ)) :

FirstOrder.Language.FinStruct codeVocab

The instance a list of nodes draws. One element per node, and one spare element at the end which carries no mark – out-of-range readings return DescriptiveComplexity.nodeNone, whose tag is no constructor's.

Equations

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

Instances For

Dependency graph

def DescriptiveComplexity.codeStruct (c : Nat.Partrec.Code) :

FirstOrder.Language.FinStruct codeVocab

The instance a code draws.

Equations

DescriptiveComplexity.codeStruct c = DescriptiveComplexity.listStruct (DescriptiveComplexity.codeNodes c)

Instances For

Dependency graph

@[simp]

theorem DescriptiveComplexity.card_listStruct (L : List (ℕ × ℕ × ℕ)) :

(listStruct L).card = L.length + 1

Dependency graph

theorem DescriptiveComplexity.relMapBool_listStruct (L : List (ℕ × ℕ × ℕ)) {n : ℕ} (R : FirstOrder.Language.code.Relations n) (x : Fin n → (listStruct L).Univ) :

(listStruct L).relMapBool R x = codeRelBool L R x

Dependency graph

theorem DescriptiveComplexity.cRoot_iff (L : List (ℕ × ℕ × ℕ)) (i : (listStruct L).Univ) :

CRoot i ↔ ↑i = 0

Dependency graph

theorem DescriptiveComplexity.cZero_iff (L : List (ℕ × ℕ × ℕ)) (i : (listStruct L).Univ) :

CZero i ↔ tagAt L ↑i = 0

Dependency graph

theorem DescriptiveComplexity.cSucc_iff (L : List (ℕ × ℕ × ℕ)) (i : (listStruct L).Univ) :

CSucc i ↔ tagAt L ↑i = 1

Dependency graph

theorem DescriptiveComplexity.cLeft_iff (L : List (ℕ × ℕ × ℕ)) (i : (listStruct L).Univ) :

CLeft i ↔ tagAt L ↑i = 2

Dependency graph

theorem DescriptiveComplexity.cRight_iff (L : List (ℕ × ℕ × ℕ)) (i : (listStruct L).Univ) :

CRight i ↔ tagAt L ↑i = 3

Dependency graph

theorem DescriptiveComplexity.cPair_iff (L : List (ℕ × ℕ × ℕ)) (i : (listStruct L).Univ) :

CPair i ↔ tagAt L ↑i = 4

Dependency graph

theorem DescriptiveComplexity.cComp_iff (L : List (ℕ × ℕ × ℕ)) (i : (listStruct L).Univ) :

CComp i ↔ tagAt L ↑i = 5

Dependency graph

theorem DescriptiveComplexity.cPrec_iff (L : List (ℕ × ℕ × ℕ)) (i : (listStruct L).Univ) :

CPrec i ↔ tagAt L ↑i = 6

Dependency graph

theorem DescriptiveComplexity.cRfind_iff (L : List (ℕ × ℕ × ℕ)) (i : (listStruct L).Univ) :

CRfind i ↔ tagAt L ↑i = 7

Dependency graph

theorem DescriptiveComplexity.cArg1_iff (L : List (ℕ × ℕ × ℕ)) (i j : (listStruct L).Univ) :

CArg1 i j ↔ off1At L ↑i ≠ 0 ∧ ↑j = ↑i + off1At L ↑i

Dependency graph

theorem DescriptiveComplexity.cArg2_iff (L : List (ℕ × ℕ × ℕ)) (i j : (listStruct L).Univ) :

CArg2 i j ↔ off2At L ↑i ≠ 0 ∧ ↑j = ↑i + off2At L ↑i

Dependency graph

theorem DescriptiveComplexity.head_flat {L : List (ℕ × ℕ × ℕ)} {c : Nat.Partrec.Code} {i : ℕ} (h : Seg L (codeNodes c) i) :

L.getD i nodeNone = (codeNodes c).getD 0 nodeNone

Dependency graph

The instance a code draws does draw it #

theorem DescriptiveComplexity.decodesTo_of_seg (L : List (ℕ × ℕ × ℕ)) (c : Nat.Partrec.Code) (i : ℕ) (hi : i < L.length + 1) :

Seg L (codeNodes c) i → DecodesTo ⟨i, hi⟩ c

Every subterm is drawn at its segment.

Dependency graph

theorem DescriptiveComplexity.decodesTo_root (c : Nat.Partrec.Code) :

DecodesTo ⟨0, ⋯⟩ c

The root of the instance a code draws does draw that code.

Dependency graph

The instance a code draws is well formed #

Dependency graph

theorem DescriptiveComplexity.mark_iff (L : List (ℕ × ℕ × ℕ)) (t : CodeTag) (a : (listStruct L).Univ) :

Mark t a ↔ tagAt L ↑a = tagNum t

Dependency graph

theorem DescriptiveComplexity.codeWF_listStruct (L : List (ℕ × ℕ × ℕ)) :

CodeWF (listStruct L).Univ

Dependency graph

The instance draws the code, and nothing else #

theorem DescriptiveComplexity.codehalt_codeStruct (c : Nat.Partrec.Code) :

CODEHALT.Holds (codeStruct c).Univ ↔ (c.eval 0).Dom

The instance a code draws is a yes-instance exactly when the code halts on 0.

Dependency graph

theorem DescriptiveComplexity.codehalt_toPred_codeStruct (c : Nat.Partrec.Code) :

CODEHALT.toPred codeVocab (codeStruct c) ↔ (c.eval 0).Dom

Dependency graph

The map is primitive recursive #

theorem DescriptiveComplexity.primrec_flat :

Primrec codeNodes

Dependency graph

theorem DescriptiveComplexity.primrec_codeStruct :

Primrec codeStruct

Dependency graph

Undecidability #

theorem DescriptiveComplexity.not_computablePred_codehalt :

¬ComputablePred (CODEHALT.toPred codeVocab)

CODEHALT is undecidable. Mathlib's halting problem maps into it by the tree encoding, which is primitive recursive, so a decision procedure for the concrete instances would decide whether a partial recursive code halts.

Dependency graph

theorem DescriptiveComplexity.not_computablePred_of_RE_hard {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (hP : RE.Hard P) (V : L.FinVocab) :

¬ComputablePred (P.toPred V)

An RE-hard problem is undecidable. Hardness in this library is cofinal, so an RE-hard problem is in particular a target of CODEHALT, which is undecidable; and a first-order reduction is a computable many-one reduction of the induced sets (DescriptiveComplexity.not_computablePred_of_relOrderedReduction).

This is the leverage the whole DescriptiveComplexity.Computability layer exists for: every completeness theorem for RE now yields undecidability with no computability work of its own.

Dependency graph

theorem DescriptiveComplexity.finsat_not_computable :

¬ComputablePred (FINSAT.toPred finsatVocab)

Trakhtenbrot's theorem: whether a first-order sentence has a finite model is undecidable.

Dependency graph