Recursively enumerable sets of bit strings are halting sets of the ambient model

exists_semidecider: for every recursively enumerable predicate p on bit strings (Mathlib's REPred) there is a well-scoped program S of the ambient model that halts on the encoding encode x of a bit string x exactly when p x. This is the form in which the compressibility criterion (MIPRE.Cost.compressibility_criterion) consumes semidecidability — its hypothesis hS : ∀ x, Halts S (encode x) ↔ x ∉ B — and, with rePred_halts (the halting set of a program on encoded strings is recursively enumerable), it identifies REPred on bit strings with the halting sets of the model (MIPRE.isRE_iff).

The route is that of exists_compile: through Turing.ToPartrec.Code and its translation Prog.ofCode, with one obstacle. A ToPartrec code cannot see trailing zeros of its input list (its primitives read [] and 0 :: v alike), whereas the bit false encodes as nil = ofNat 0, so no translated code can separate x from x ++ [false]. So S first shifts every bit up by one — shiftRevProg, a loop, which reverses the list on the way as loops naturally do — producing the encL-encoding of a list of ones and twos, which a ToPartrec loop (BitCode.convCode) folds into the Mathlib code number Encodable.encode x of the original string; a ToPartrec code for the r.e. predicate, from Turing.ToPartrec.Code.exists_code, then runs on that number.

A ToPartrec code reading a bit string off a list of ones and twos

def MIPRE.Cost.BitCode.swapCode : Turing.ToPartrec.Code

[a, b, rest...] ↦ [b, a, rest...] (and [a] ↦ [0, a]).

Equations

• MIPRE.Cost.BitCode.swapCode = (Turing.ToPartrec.Code.head.comp Turing.ToPartrec.Code.tail).cons (Turing.ToPartrec.Code.head.cons (Turing.ToPartrec.Code.tail.comp Turing.ToPartrec.Code.tail))

theorem MIPRE.Cost.BitCode.swapCode_eval (a b : ℕ) (rest : List ℕ) : swapCode.eval (a :: b :: rest) = pure (b :: a :: rest)

theorem MIPRE.Cost.BitCode.swapCode_eval_single (a : ℕ) : swapCode.eval [a] = pure [0, a]

def MIPRE.Cost.BitCode.stepFun (v : List.Vector ℕ 2) : ℕ

The step of the fold, [acc, n] ↦ pair n acc + 1, as a function on vectors: it is Encodable.encode (b :: l) from n = encode b and acc = encode l.

Equations

• MIPRE.Cost.BitCode.stepFun v = Nat.pair (v.get 1) v.head + 1

theorem MIPRE.Cost.BitCode.primrec_stepFun : Primrec stepFun

theorem MIPRE.Cost.BitCode.exists_stepCode : ∃ (c : Turing.ToPartrec.Code), ∀ (acc n : ℕ), c.eval [acc, n] = pure [Nat.pair n acc + 1]

A ToPartrec code for the step of the fold.

def MIPRE.Cost.BitCode.loopBody (cg : Turing.ToPartrec.Code) : Turing.ToPartrec.Code

Body of the folding loop, given a step code cg: on [acc, n + 1, rest...] continue with [pair n acc + 1, rest...]; on [acc] (or [acc, 0, ...]) stop with [acc].

Equations

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

theorem MIPRE.Cost.BitCode.loopBody_eval_stop (cg : Turing.ToPartrec.Code) (acc : ℕ) : (loopBody cg).eval [acc] = pure [0, acc]

theorem MIPRE.Cost.BitCode.loopBody_eval_step (cg : Turing.ToPartrec.Code) (hcg : ∀ (acc n : ℕ), cg.eval [acc, n] = pure [Nat.pair n acc + 1]) (acc n : ℕ) (rest : List ℕ) : (loopBody cg).eval (acc :: (n + 1) :: rest) = pure (1 :: (Nat.pair n acc + 1) :: rest)

def MIPRE.Cost.BitCode.foldEnc : List ℕ → ℕ → ℕ

The fold computed by the loop: foldEnc [n₁, …, nₖ] acc pairs the entries onto the accumulator from the left.

Equations

• MIPRE.Cost.BitCode.foldEnc [] x✝ = x✝
• MIPRE.Cost.BitCode.foldEnc (n :: w) x✝ = MIPRE.Cost.BitCode.foldEnc w (Nat.pair n x✝ + 1)

theorem MIPRE.Cost.BitCode.fix_loopBody_eval (cg : Turing.ToPartrec.Code) (hcg : ∀ (acc n : ℕ), cg.eval [acc, n] = pure [Nat.pair n acc + 1]) (w : List ℕ) (acc : ℕ) : (loopBody cg).fix.eval (acc :: List.map (fun (x : ℕ) => x + 1) w) = pure [foldEnc w acc]

def MIPRE.Cost.BitCode.convCode (cg : Turing.ToPartrec.Code) : Turing.ToPartrec.Code

The conversion code: on a list of positive naturals w.map (· + 1) it returns [foldEnc w 0].

Equations

• MIPRE.Cost.BitCode.convCode cg = (MIPRE.Cost.BitCode.loopBody cg).fix.comp Turing.ToPartrec.Code.zero'

theorem MIPRE.Cost.BitCode.convCode_eval (cg : Turing.ToPartrec.Code) (hcg : ∀ (acc n : ℕ), cg.eval [acc, n] = pure [Nat.pair n acc + 1]) (w : List ℕ) : (convCode cg).eval (List.map (fun (x : ℕ) => x + 1) w) = pure [foldEnc w 0]

theorem MIPRE.Cost.BitCode.foldEnc_encode (l m : List Bool) : foldEnc (List.map Encodable.encode l) (Encodable.encode m) = Encodable.encode (l.reverse ++ m)

Folding the codes of the bits of l onto the code of m yields the code of l.reverse ++ m.

theorem MIPRE.Cost.BitCode.exists_code_bitStr {p : BitStr → Prop} (hp : REPred p) : ∃ (c : Turing.ToPartrec.Code), ∀ (x : BitStr), (c.eval (List.map (fun (x : ℕ) => x + 1) (List.map Encodable.encode (List.reverse x)))).Dom ↔ p x

An r.e. predicate on bit strings is the halting set of a ToPartrec code on the list of shifted bit codes of the reversed string.

Shifting the bits up by one, in the ambient model

def MIPRE.Cost.Prog.shiftRevBody : Prog

Body of shiftRevProg: on state cons xs acc, stop with acc if xs is empty, otherwise move cons nil (head xs) onto acc.

Equations

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

def MIPRE.Cost.Prog.shiftRevProg : Prog

shiftRevProg on list l computes list ((l.map (cons nil)).reverse): on an encoded bit string, the reversed list of its bits shifted up by one (cons_nil_ofBool).

Equations

• MIPRE.Cost.Prog.shiftRevProg = ((MIPRE.Cost.Prog.var 0).cons MIPRE.Cost.Prog.nil).let_ MIPRE.Cost.Prog.shiftRevBody.loop

theorem MIPRE.Cost.Prog.shiftRevBody_wellScoped : WellScoped 1 shiftRevBody

theorem MIPRE.Cost.Prog.shiftRevProg_wellScoped : WellScoped 1 shiftRevProg

theorem MIPRE.Cost.Prog.shiftRevBody_step (h : Data) (l acc : List Data) : ∃ (t : ℕ), Eval [(Data.list (h :: l)).cons (Data.list acc)] shiftRevBody ((Data.nil.cons Data.nil).cons ((Data.list l).cons (Data.list (Data.nil.cons h :: acc)))) t

One iteration of shiftRevBody on a non-empty list.

theorem MIPRE.Cost.Prog.shiftRevBody_stop (acc : List Data) : ∃ (t : ℕ), Eval [(Data.list []).cons (Data.list acc)] shiftRevBody (Data.nil.cons (Data.list acc)) t

The stopping iteration of shiftRevBody on the empty list.

theorem MIPRE.Cost.Prog.shiftRevLoop_runs (l acc : List Data) (env : Env) : ∃ (t : ℕ), Eval ((Data.list l).cons (Data.list acc) :: env) shiftRevBody.loop (Data.list ((List.map Data.nil.cons l).reverse ++ acc)) t

theorem MIPRE.Cost.Prog.shiftRevProg_runs (l : List Data) : ∃ (t : ℕ), Eval [Data.list l] shiftRevProg (Data.list (List.map Data.nil.cons l).reverse) t

theorem MIPRE.Cost.Data.cons_nil_ofBool (b : Bool) : nil.cons (ofBool b) = ofNat (Encodable.encode b + 1)

A bit shifted up by one is the unary numeral of its code plus one: false ↦ ofNat 1, true ↦ ofNat 2.

theorem MIPRE.Cost.encode_bitStr_eq (x : BitStr) : encode x = Data.list (List.map Data.ofBool x)

theorem MIPRE.Cost.Data.list_shift_eq_encL (x : BitStr) : list (List.map nil.cons (List.map ofBool x)).reverse = encL (List.map (fun (x : ℕ) => x + 1) (List.map Encodable.encode (List.reverse x)))

The output of shiftRevProg on an encoded bit string is the encL-encoding of the shifted codes of the bits of the reversed string.

The semidecider

theorem MIPRE.Cost.exists_semidecider {p : BitStr → Prop} (hp : REPred p) : ∃ (S : Prog), Prog.WellScoped 1 S ∧ ∀ (x : BitStr), Halts S (encode x) ↔ p x

Recursively enumerable predicates are halting sets. For every r.e. predicate p on bit strings there is a well-scoped program halting on encode x exactly when p x: the hypothesis hS of compressibility_criterion, for p := (· ∉ B).

The converse: halting sets are recursively enumerable

theorem MIPRE.Cost.Data.primrec_ofBool : Primrec ofBool

theorem MIPRE.Cost.Data.ofList_eq_foldr {α : Type u_1} (f : α → Data) (l : List α) : ofList f l = List.foldr (fun (a : α) (d : Data) => (f a).cons d) nil l

theorem MIPRE.Cost.primrec_encode_bitStr : Primrec fun (x : BitStr) => encode x

The encoding of bit strings as data is primitive recursive.

theorem MIPRE.Cost.halts_iff_evalData_dom (S : Prog) (d : Data) : Halts S d ↔ (Machine.evalData S.toData d).Dom

theorem MIPRE.Cost.rePred_halts (S : Prog) : REPred fun (x : BitStr) => Halts S (encode x)

The halting set of a program on encoded bit strings is recursively enumerable.