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.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.

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

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.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.

The decoder is primitive recursive

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

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'

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.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.

The procedure, and the whole chain

theorem DescriptiveComplexity.HaltHard.inputChain_dom_iff {L : FirstOrder.Language} {V : L.FinVocab} [L.IsRelational] (P : DecisionProblem L) {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.