Recursive membership via promised decider codes

The raw codes in this file are Mathlib's Nat.Partrec.Code. Their universal evaluator is partial on arbitrary codes. A code is a Valid decider when that evaluator halts on every encoded word; on such codes, evalBool uniformly decides membership in language.

This is the promise-problem formulation of uniform membership for the class of recursive languages. It does not assert that the set of total program codes is decidable (it is not), nor does it package those codes as a Primcodable subtype.

Main results

• RecursiveDeciderCode.eval_decidesMembership gives the one universal membership procedure, total and correct under the validity promise.
• RecursiveDeciderCode.exists_valid_iff_computablePred characterizes computable membership predicates by valid codes.
• RecursiveDeciderCode.exists_valid_iff_is_Recursive specializes that characterization to the repository's is_Recursive language class.
• RecursiveDeciderCode.recursive_computableMembership packages the intended encoded-device-and-word result using ComputableMembership itself.

def RecursiveDeciderCode.evalBool {T : Type} [Primcodable T] (c : Nat.Partrec.Code) (w : List T) : Part Bool

Run a raw partial-recursive code on the encoding of a word and interpret an odd natural-number result as true and an even result as false.

Equations

• RecursiveDeciderCode.evalBool c w = Part.map Nat.bodd (c.eval (Encodable.encode w))

def RecursiveDeciderCode.Valid {T : Type} [Primcodable T] (c : Nat.Partrec.Code) : Prop

The semantic promise that a raw program code halts on every encoded word.

Equations

• RecursiveDeciderCode.Valid c = ∀ (w : List T), (RecursiveDeciderCode.evalBool c w).Dom

def RecursiveDeciderCode.language {T : Type} [Primcodable T] (c : Nat.Partrec.Code) : Language T

The language denoted by a raw decider code: precisely the words on which its Boolean evaluation returns true. This is meaningful for every raw code, although only Valid codes are promised to decide it totally.

Equations

• RecursiveDeciderCode.language c = {w : List T | true ∈ RecursiveDeciderCode.evalBool c w}

theorem RecursiveDeciderCode.evalBool_partrec₂ {T : Type} [Primcodable T] : Partrec₂ evalBool

The universal Boolean evaluator is partial recursive jointly in the raw code and the input word.

theorem RecursiveDeciderCode.eval_decidesMembership {T : Type} [Primcodable T] : DecidesOnPromise Valid evalBool fun (c : Nat.Partrec.Code) (w : List T) => w ∈ language c

evalBool is a uniform membership decider on the promise that its raw code is valid.

theorem RecursiveDeciderCode.language_membershipSemiDecidable {T : Type} [Primcodable T] : MembershipSemiDecidable language

Raw decider-code membership is uniformly recursively enumerable, even away from the totality promise: simulate the program and return exactly when its Boolean result is true. This is the effectivity condition preventing language from hiding noncomputable information in the decoding map.

theorem RecursiveDeciderCode.exists_valid_iff_computablePred {T : Type} [Primcodable T] (L : Language T) : (∃ (c : Nat.Partrec.Code), Valid c ∧ language c = L) ↔ ComputablePred fun (w : List T) => w ∈ L

A language has a computable membership predicate exactly when it is denoted by some valid raw partial-recursive decider code.

theorem RecursiveDeciderCode.exists_valid_iff_is_Recursive {T : Type} [Primcodable T] [DecidableEq T] [Fintype T] (L : Language T) : (∃ (c : Nat.Partrec.Code), Valid c ∧ language c = L) ↔ is_Recursive L

Over finite computably encoded alphabets, valid always-halting Boolean decider codes denote exactly the recursive languages.

theorem RecursiveDeciderCode.recursive_computableMembership {T : Type} [Primcodable T] [DecidableEq T] [Fintype T] : ComputableMembership Recursive language Valid

Membership for recursive languages is uniformly computable from an encoded always-halting decider and a word.

Raw program syntax is Primcodable; Valid is the semantic promise that the program halts on every encoded word. The universal evaluator is partial-recursive on all raw codes and total/correct on valid codes, while the valid codes denote exactly all recursive languages.