The input chain: getting the instance into the machine

Turing.ToPartrec.Code.exists_code gives codes for fixed-arity functions only, so the machine cannot be started on the variable-length bit table of the instance. The continuation stack solves this: since a comp frame applies its code to the value below it, a chain of comp frames applies a fixed code once per frame – one frame per bit (DescriptiveComplexity.HaltHard.inputChain). Each bit frame pushes its bit (Turing.ToPartrec.Code.zero', or the three-node DescriptiveComplexity.HaltHard.pushOne), the next frame folds it into the accumulator (2·acc + b, by a code exists_code supplies), and the last frame runs the semi-decision procedure on the folded number and the universe size.

The number the chain folds is the flattened relation table of the instance read back one binary digit at a time (DescriptiveComplexity.HaltHard.structOfBits, with DescriptiveComplexity.HaltHard.structOfBits_flatten the roundtrip): a FirstOrder.Language.FinStruct is a size and a table, so decoding owes only digit arithmetic, and it is primitive recursive (DescriptiveComplexity.HaltHard.primrec_structOfBits) – which is what lets the Part.assert trick of orderedReduction_codehalt run behind Nat.Partrec'.part_iff₂. The bits enter the chain most significant first, i.e. the flattened table reversed (DescriptiveComplexity.HaltHard.foldl_two_reverse).

The chain is pure comp frames, so its frame region is a run of bare headers (DescriptiveComplexity.HaltHard.frameSeg_inputChain), and its evaluation is total until the final procedure (DescriptiveComplexity.HaltHard.inputChain_dom_iff).

Bits, numbers and flattened tables

def DescriptiveComplexity.HaltHard.natOfBits : List Bool → ℕ

The number whose binary digits are the listed bits, least significant first.

Equations

• DescriptiveComplexity.HaltHard.natOfBits [] = 0
• DescriptiveComplexity.HaltHard.natOfBits (b :: l) = b.toNat + 2 * DescriptiveComplexity.HaltHard.natOfBits l

theorem DescriptiveComplexity.HaltHard.digitAt_natOfBits (l : List Bool) (j : ℕ) : FirstOrder.Language.digitAt 2 (natOfBits l) j = (l.getD j false).toNat

The digits of natOfBits are the listed bits.

theorem DescriptiveComplexity.HaltHard.foldl_two_reverse (l : List Bool) (acc : ℕ) : List.foldl (fun (a : ℕ) (b : Bool) => 2 * a + b.toNat) acc l.reverse = acc * 2 ^ l.length + natOfBits l

Folding bits most significant first computes natOfBits of their reversal.

theorem DescriptiveComplexity.HaltHard.flatten_getD {α : Type} (d : α) (l : List (List α)) (i : ℕ) : i < l.length → ∀ {t : ℕ}, t < (l.getD i []).length → l.flatten.getD ((List.map List.length (List.take i l)).sum + t) d = (l.getD i []).getD t d

Reading a flattened list of rows at a prefix-sum offset reads inside the row.

theorem DescriptiveComplexity.HaltHard.range_map_getD {α : Type} (l : List α) (d : α) : List.map (fun (t : ℕ) => l.getD t d) (List.range l.length) = l

Reading every position of a list back through getD is the list.

Decoding a number into a structure

def DescriptiveComplexity.HaltHard.offB {L : FirstOrder.Language} (V : L.FinVocab) (c : ℕ) : ℕ → ℕ

The offset of the row of symbol i inside the flattened table, over a universe of size c.

Equations

• DescriptiveComplexity.HaltHard.offB V c 0 = 0
• DescriptiveComplexity.HaltHard.offB V c i.succ = DescriptiveComplexity.HaltHard.offB V c i + if h : i < V.numSyms then c ^ V.arity ⟨i, h⟩ else 0

theorem DescriptiveComplexity.HaltHard.offB_eq_sum {L : FirstOrder.Language} (V : L.FinVocab) (c i : ℕ) : i ≤ V.numSyms → offB V c i = (List.map (fun (i' : Fin V.numSyms) => c ^ V.arity i') (List.take i (List.finRange V.numSyms))).sum

The offsets are the prefix sums of the row lengths.

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

Decoding a number into a concrete structure: the universe has size k + 1, and the relation tables read the binary digits of N, row by row at the offsets of DescriptiveComplexity.HaltHard.offB.

Equations

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

theorem DescriptiveComplexity.HaltHard.decide_toNat_eq_one (b : Bool) : decide (b.toNat = 1) = b

Reading a Boolean digit back.

theorem DescriptiveComplexity.HaltHard.structOfBits_flatten {L : FirstOrder.Language} (V : L.FinVocab) (s : FirstOrder.Language.FinStruct V) (hlen : s.table.length = V.numSyms) (hrow : ∀ (i : Fin V.numSyms), (s.table.getD ↑i []).length = s.card ^ V.arity i) : structOfBits V s.univSize (natOfBits s.table.flatten) = s

The roundtrip: decoding the number of the flattened table of a well-shaped concrete structure gives the structure back.

theorem DescriptiveComplexity.HaltHard.length_table_ofEquiv {L : FirstOrder.Language} (V : L.FinVocab) [L.IsRelational] {A : Type} [L.Structure A] [(n : ℕ) → (R : L.Relations n) → (x : Fin n → A) → Decidable (FirstOrder.Language.Structure.RelMap R x)] (k : ℕ) (e : Fin (k + 1) ≃ A) : (FirstOrder.Language.FinStruct.ofEquiv V k e).table.length = V.numSyms

The tables of FirstOrder.Language.FinStruct.ofEquiv are well-shaped: one row per symbol.

theorem DescriptiveComplexity.HaltHard.length_row_ofEquiv {L : FirstOrder.Language} (V : L.FinVocab) [L.IsRelational] {A : Type} [L.Structure A] [(n : ℕ) → (R : L.Relations n) → (x : Fin n → A) → Decidable (FirstOrder.Language.Structure.RelMap R x)] (k : ℕ) (e : Fin (k + 1) ≃ A) (i : Fin V.numSyms) : ((FirstOrder.Language.FinStruct.ofEquiv V k e).table.getD ↑i []).length = (FirstOrder.Language.FinStruct.ofEquiv V k e).card ^ V.arity i

The rows of FirstOrder.Language.FinStruct.ofEquiv have the lengths the offsets expect.

theorem DescriptiveComplexity.HaltHard.structOfBits_ofEquiv {L : FirstOrder.Language} (V : L.FinVocab) [L.IsRelational] {A : Type} [L.Structure A] [(n : ℕ) → (R : L.Relations n) → (x : Fin n → A) → Decidable (FirstOrder.Language.Structure.RelMap R x)] (k : ℕ) (e : Fin (k + 1) ≃ A) : structOfBits V k (natOfBits (FirstOrder.Language.FinStruct.ofEquiv V k e).table.flatten) = FirstOrder.Language.FinStruct.ofEquiv V k e

Decoding the folded table of an instance gives the instance's concrete presentation.

The decoder is primitive recursive

theorem DescriptiveComplexity.HaltHard.primrec_offB {L : FirstOrder.Language} (V : L.FinVocab) (i : ℕ) : Primrec fun (c : ℕ) => offB V c i

theorem DescriptiveComplexity.HaltHard.primrec_two_pow : Primrec fun (x : ℕ) => 2 ^ x

Powers of two are primitive recursive in the exponent.

theorem DescriptiveComplexity.HaltHard.primrec_structOfBits {L : FirstOrder.Language} (V : L.FinVocab) : Primrec fun (p : ℕ × ℕ) => structOfBits V p.1 p.2

The decoder is primitive recursive, as a function of the pair – what the Part.assert code needs.

The pushed bits, and the fold

def DescriptiveComplexity.HaltHard.pushOne : Turing.ToPartrec.Code

The code pushing a 1 in front of the value: v ↦ 1 :: v.

Equations

• DescriptiveComplexity.HaltHard.pushOne = (Turing.ToPartrec.Code.succ.comp Turing.ToPartrec.Code.zero').cons Turing.ToPartrec.Code.id

theorem DescriptiveComplexity.HaltHard.eval_pushOne (v : List ℕ) : pushOne.eval v = pure (1 :: v)

def DescriptiveComplexity.HaltHard.pushBit (b : Bool) : Turing.ToPartrec.Code

The code pushing a bit.

Equations

• DescriptiveComplexity.HaltHard.pushBit b = if b = true then DescriptiveComplexity.HaltHard.pushOne else Turing.ToPartrec.Code.zero'

theorem DescriptiveComplexity.HaltHard.eval_pushBit (b : Bool) (v : List ℕ) : (pushBit b).eval v = pure (b.toNat :: v)

def DescriptiveComplexity.HaltHard.foldSpec : List.Vector ℕ 3 →. ℕ

The fold specification: 2·acc + b, of the vector [b, acc, n].

Equations

• DescriptiveComplexity.HaltHard.foldSpec v = Part.some (2 * v.get 1 + v.get 0)

def DescriptiveComplexity.HaltHard.foldCode (cF : Turing.ToPartrec.Code) : Turing.ToPartrec.Code

The fold code: replace the pushed bit and the accumulator by their fold, keep the rest of the value.

Equations

• DescriptiveComplexity.HaltHard.foldCode cF = cF.cons (Turing.ToPartrec.Code.tail.comp Turing.ToPartrec.Code.tail)

theorem DescriptiveComplexity.HaltHard.eval_foldCode (cF : Turing.ToPartrec.Code) (hF : ∀ (v : List.Vector ℕ 3), cF.eval ↑v = pure <$> foldSpec v) (b acc n : ℕ) : (foldCode cF).eval [b, acc, n] = pure [2 * acc + b, n]

The chain

def DescriptiveComplexity.HaltHard.allCode (cF cP : Turing.ToPartrec.Code) : Turing.ToPartrec.Code

The global code the machine simulates: a container for the two bit pushes, the fold, and the semi-decision procedure. It is never dispatched at its root – only the positions of its four components are.

Equations

• DescriptiveComplexity.HaltHard.allCode cF cP = Turing.ToPartrec.Code.zero'.cons (DescriptiveComplexity.HaltHard.pushOne.cons ((DescriptiveComplexity.HaltHard.foldCode cF).cons cP))

def DescriptiveComplexity.HaltHard.posBit0 (cF cP : Turing.ToPartrec.Code) : CPos (allCode cF cP)

The position of Turing.ToPartrec.Code.zero' in the container.

Equations

• DescriptiveComplexity.HaltHard.posBit0 cF cP = Sum.inr (Sum.inl ())

def DescriptiveComplexity.HaltHard.posBit1 (cF cP : Turing.ToPartrec.Code) : CPos (allCode cF cP)

The position of the one-push in the container.

Equations

• DescriptiveComplexity.HaltHard.posBit1 cF cP = Sum.inr (Sum.inr (Sum.inr (Sum.inl (DescriptiveComplexity.HaltHard.cRoot DescriptiveComplexity.HaltHard.pushOne))))

def DescriptiveComplexity.HaltHard.posBit (cF cP : Turing.ToPartrec.Code) (b : Bool) : CPos (allCode cF cP)

The position of a bit push.

Equations

• DescriptiveComplexity.HaltHard.posBit cF cP b = if b = true then DescriptiveComplexity.HaltHard.posBit1 cF cP else DescriptiveComplexity.HaltHard.posBit0 cF cP

def DescriptiveComplexity.HaltHard.posFold (cF cP : Turing.ToPartrec.Code) : CPos (allCode cF cP)

The position of the fold in the container.

Equations

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

def DescriptiveComplexity.HaltHard.posProc (cF cP : Turing.ToPartrec.Code) : CPos (allCode cF cP)

The position of the semi-decision procedure in the container.

Equations

• DescriptiveComplexity.HaltHard.posProc cF cP = Sum.inr (Sum.inr (Sum.inr (Sum.inr (Sum.inr (Sum.inr (DescriptiveComplexity.HaltHard.cRoot cP))))))

@[simp]

theorem DescriptiveComplexity.HaltHard.codeAt_posBit0 (cF cP : Turing.ToPartrec.Code) : codeAt (posBit0 cF cP) = Turing.ToPartrec.Code.zero'

@[simp]

theorem DescriptiveComplexity.HaltHard.codeAt_posBit1 (cF cP : Turing.ToPartrec.Code) : codeAt (posBit1 cF cP) = pushOne

@[simp]

theorem DescriptiveComplexity.HaltHard.codeAt_posFold (cF cP : Turing.ToPartrec.Code) : codeAt (posFold cF cP) = foldCode cF

@[simp]

theorem DescriptiveComplexity.HaltHard.codeAt_posProc (cF cP : Turing.ToPartrec.Code) : codeAt (posProc cF cP) = cP

@[simp]

theorem DescriptiveComplexity.HaltHard.codeAt_posBit (cF cP : Turing.ToPartrec.Code) (b : Bool) : codeAt (posBit cF cP b) = pushBit b

def DescriptiveComplexity.HaltHard.inputChain (cF cP : Turing.ToPartrec.Code) : List Bool → PCont (allCode cF cP)

The input chain: one comp frame pushing each bit, one folding it in, and a last frame running the procedure.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HaltHard.inputChain cF cP [] = DescriptiveComplexity.HaltHard.PCont.comp (DescriptiveComplexity.HaltHard.posProc cF cP) DescriptiveComplexity.HaltHard.PCont.halt

theorem DescriptiveComplexity.HaltHard.cont_eval_comp (f : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont) (v : List ℕ) : (Turing.ToPartrec.Cont.comp f k).eval v = do let w ← f.eval v k.eval w

Evaluating a pending composition is composing the evaluations.

theorem DescriptiveComplexity.HaltHard.frameSeg_inputChain (cF cP : Turing.ToPartrec.Code) (bits : List Bool) : FrameSeg (inputChain cF cP bits) (List.flatMap (fun (b : Bool) => [SimSym.hComp (posBit cF cP b), SimSym.hComp (posFold cF cP)]) bits ++ [SimSym.hComp (posProc cF cP)])

The frame region of the chain: a run of bare comp headers.

theorem DescriptiveComplexity.HaltHard.cont_eval_inputChain (cF : Turing.ToPartrec.Code) (hF : ∀ (v : List.Vector ℕ 3), cF.eval ↑v = pure <$> foldSpec v) (cP : Turing.ToPartrec.Code) (bits : List Bool) (acc n : ℕ) : (inputChain cF cP bits).toCont.eval [acc, n] = cP.eval [List.foldl (fun (a : ℕ) (b : Bool) => 2 * a + b.toNat) acc bits, n]

Evaluating the chain folds the bits and hands the result to the procedure.

The procedure, and the whole chain

theorem DescriptiveComplexity.HaltHard.exists_chain_codes {L : FirstOrder.Language} {V : L.FinVocab} (P : DecisionProblem L) [L.IsRelational] (h : REPred (P.toPred V)) : ∃ (cF : Turing.ToPartrec.Code) (cP : Turing.ToPartrec.Code), (∀ (v : List.Vector ℕ 3), cF.eval ↑v = pure <$> foldSpec v) ∧ ∀ (N n : ℕ), (cP.eval [N, n]).Dom ↔ P.toPred V (structOfBits V (n - 1) N)

The two codes of the chain exist: a fold code, and a code whose halting on the folded number and the size decides the problem.

theorem DescriptiveComplexity.HaltHard.inputChain_dom_iff {L : FirstOrder.Language} {V : L.FinVocab} (P : DecisionProblem L) [L.IsRelational] {cF cP : Turing.ToPartrec.Code} (hF : ∀ (v : List.Vector ℕ 3), cF.eval ↑v = pure <$> foldSpec v) (hP : ∀ (N n : ℕ), (cP.eval [N, n]).Dom ↔ P.toPred V (structOfBits V (n - 1) N)) (bits : List Bool) (n : ℕ) : ((inputChain cF cP bits.reverse).toCont.eval [0, n]).Dom ↔ P.toPred V (structOfBits V (n - 1) (natOfBits bits))

What the chain decides: started on [0, n] under the chain of the reversed flattened table, the machine's abstract evaluation terminates exactly when the decoded instance is a yes-instance.