Effective compilation of total Boolean families

This file packages the parameter theorem (s-m-n) for the promised presentation of recursive languages. A Boolean predicate test a w which is computable jointly in a parameter a and a word w can be compiled into a raw partial-recursive code. The compiler is itself computable in a, and every code it produces satisfies the semantic RecursiveDeciderCode.Valid promise.

The construction is useful for reductions to semantic questions about recursive languages: it ensures that a reduction never queries the putative algorithm on an invalid (non-total) code.

def RecursiveDeciderCode.compileBoolJoint {A T : Type} [Primcodable A] [Primcodable T] (test : A → List T → Bool) : ℕ →. ℕ

The unary partial function which evaluates a jointly computable Boolean family after decoding its parameter/word pair.

Equations

• RecursiveDeciderCode.compileBoolJoint test n = (↑(Encodable.decode n)).bind fun (p : A × List T) => Part.some (Encodable.encode (test p.1 p.2))

theorem RecursiveDeciderCode.compileBoolJoint_partrec {A T : Type} [Primcodable A] [Primcodable T] (test : A → List T → Bool) (htest : Computable₂ test) : Nat.Partrec (compileBoolJoint test)

noncomputable def RecursiveDeciderCode.compileBoolBase {A T : Type} [Primcodable A] [Primcodable T] (test : A → List T → Bool) (htest : Computable₂ test) : Nat.Partrec.Code

A fixed code for the joint evaluator underlying compileBool.

Equations

• RecursiveDeciderCode.compileBoolBase test htest = Classical.choose ⋯

theorem RecursiveDeciderCode.compileBoolBase_spec {A T : Type} [Primcodable A] [Primcodable T] (test : A → List T → Bool) (htest : Computable₂ test) : (compileBoolBase test htest).eval = compileBoolJoint test

noncomputable def RecursiveDeciderCode.compileBool {A T : Type} [Primcodable A] [Primcodable T] (test : A → List T → Bool) (htest : Computable₂ test) : A → Nat.Partrec.Code

Compile a parameterized total Boolean predicate into a raw decider code.

Although a base universal program is chosen noncomputably once, specialization in the parameter is the computable syntactic Code.curry operation.

Equations

• RecursiveDeciderCode.compileBool test htest a = (RecursiveDeciderCode.compileBoolBase test htest).curry (Encodable.encode a)

theorem RecursiveDeciderCode.compileBool_computable {A T : Type} [Primcodable A] [Primcodable T] (test : A → List T → Bool) (htest : Computable₂ test) : Computable (compileBool test htest)

Specializing the joint program is computable in the parameter.

theorem RecursiveDeciderCode.compileBool_eval {A T : Type} [Primcodable A] [Primcodable T] (test : A → List T → Bool) (htest : Computable₂ test) (a : A) (w : List T) : (compileBool test htest a).eval (Encodable.encode w) = Part.some (Encodable.encode (test a w))

The compiled raw program returns the encoded Boolean result.

theorem RecursiveDeciderCode.evalBool_compileBool {A T : Type} [Primcodable A] [Primcodable T] (test : A → List T → Bool) (htest : Computable₂ test) (a : A) (w : List T) : evalBool (compileBool test htest a) w = Part.some (test a w)

evalBool of a compiled code is exactly the original total Boolean test.

theorem RecursiveDeciderCode.compileBool_valid {A T : Type} [Primcodable A] [Primcodable T] (test : A → List T → Bool) (htest : Computable₂ test) (a : A) : Valid (compileBool test htest a)

Every code produced by compileBool satisfies the always-halting promise.

theorem RecursiveDeciderCode.mem_language_compileBool_iff {A T : Type} [Primcodable A] [Primcodable T] (test : A → List T → Bool) (htest : Computable₂ test) (a : A) (w : List T) : w ∈ language (compileBool test htest a) ↔ test a w = true

Membership in a compiled language is the source Boolean test.

theorem RecursiveDeciderCode.language_compileBool {A T : Type} [Primcodable A] [Primcodable T] (test : A → List T → Bool) (htest : Computable₂ test) (a : A) : language (compileBool test htest a) = {w : List T | test a w = true}

The language of a compiled code is the language selected by the Boolean test.