Abstract Computability Predicates for Encoded Language Classes

This file defines predicates capturing genuine, uniform computability properties of encoded language presentations.

The important point is that the encoded object representing the language is an argument of the computed predicate. For example, membership takes both the encoded language and the candidate word as input; emptiness takes the encoded language as input; equivalence takes both encoded languages as input.

These predicates are intentionally separate from statements of the form ComputablePred (fun w => w ∈ L) for a fixed language L. Such a statement may only say that one already-chosen language has computable membership. The definitions below express a uniform algorithm for a whole encoded presentation class.

Each predicate is stated for a language class C : Set (Language α) together with an encoding languageOf : Code → Language α, and bundles three obligations:

1. Characterizes C languageOf — the encoding is adequate: its range is exactly C (sound: every code denotes a member of C; complete: every member of C is denoted by some code).
2. MembershipSemiDecidable languageOf — the encoding is effective: membership is uniformly recursively enumerable.
3. The relevant decision predicate is ComputablePred.

Adequacy and effectivity make both the positive results (e.g. "regular emptiness is decidable") and the negative ones (e.g. "r.e. emptiness is not decidable") genuine statements about the class: without (1)–(2), ¬ComputableEmptiness could be made vacuous or trivially true by an adversarial encoding.

Main definitions

• MembershipSemiDecidable
• Characterizes
• ComputableMembership
• ComputableEmptiness
• ComputableUniversality
• ComputableEquivalence

def MembershipSemiDecidable {α Code : Type} [Primcodable Code] [Primcodable α] (languageOf : Code → Language α) : Prop

The encoding has semi-decidable (r.e.) uniform membership: the relation "w ∈ languageOf c" is recursively enumerable in the pair (c, w).

This ensures that the language of c can actually be computed from c, i.e. the encoding does not "smuggle" information about the language into the code.

The counterexample this rules out is an encoding over codes Bool × Code, where e (false, c) denotes the empty language and e (true, c) denotes the language of c — unless the language of c is empty, in which case e (true, c) denotes the full language instead (so that the true branch is always nonempty). This family still covers every language, yet it lets one decide emptiness from the encoding alone — a language is empty exactly when the first component is false — without any computation on the language itself. But that decoding function branches on the undecidable test "is the language of c empty?", so it has no semi-decidable membership relation, and is therefore disallowed.

It is the minimal effectivity demanded of a presentation, the common denominator across all classes (decidable membership implies it).

Equations

• MembershipSemiDecidable languageOf = REPred fun (p : Code × List α) => p.2 ∈ languageOf p.1

def Characterizes {α Code : Type} (C : Set (Language α)) (languageOf : Code → Language α) : Prop

The encoding characterizes the class C: its range is exactly C.

Soundness (∃ direction, read right-to-left): every code denotes a language in C. Completeness (left-to-right): every language in C is denoted by some code.

Equations

• Characterizes C languageOf = ∀ (L : Language α), L ∈ C ↔ ∃ (c : Code), languageOf c = L

def ComputableMembership {α Code : Type} [Primcodable Code] [Primcodable α] (C : Set (Language α)) (languageOf : Code → Language α) : Prop

Uniform computability of membership for the class C under the encoding languageOf: the encoding is an adequate, effective presentation of C and membership is uniformly decidable.

The input to the decision predicate is a pair (c, w), with c the encoded presentation and w the candidate word.

Equations

• ComputableMembership C languageOf = (Characterizes C languageOf ∧ MembershipSemiDecidable languageOf ∧ ComputablePred fun (p : Code × List α) => p.2 ∈ languageOf p.1)

def ComputableEmptiness {α Code : Type} [Primcodable Code] [Primcodable α] (C : Set (Language α)) (languageOf : Code → Language α) : Prop

Uniform computability of emptiness for the class C under the encoding languageOf: the encoding is an adequate, effective presentation of C and "languageOf c = ∅" is uniformly decidable in the code c.

Equations

• ComputableEmptiness C languageOf = (Characterizes C languageOf ∧ MembershipSemiDecidable languageOf ∧ ComputablePred fun (c : Code) => languageOf c = ∅)

def ComputableUniversality {α Code : Type} [Primcodable Code] [Primcodable α] (C : Set (Language α)) (languageOf : Code → Language α) : Prop

Uniform computability of universality for the class C under the encoding languageOf: the encoding is an adequate, effective presentation of C and "languageOf c = univ" is uniformly decidable in the code c.

Equations

• ComputableUniversality C languageOf = (Characterizes C languageOf ∧ MembershipSemiDecidable languageOf ∧ ComputablePred fun (c : Code) => languageOf c = Set.univ)

def ComputableEquivalence {α Code : Type} [Primcodable Code] [Primcodable α] (C : Set (Language α)) (languageOf : Code → Language α) : Prop

Uniform computability of equivalence for the class C under the encoding languageOf: the encoding is an adequate, effective presentation of C and "languageOf c₁ = languageOf c₂" is uniformly decidable in the pair of codes.

Equations

• ComputableEquivalence C languageOf = (Characterizes C languageOf ∧ MembershipSemiDecidable languageOf ∧ ComputablePred fun (p : Code × Code) => languageOf p.1 = languageOf p.2)