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 raw encoded syntax Code, a semantics languageOf : Code → Language α, and a validity promise valid : Code → Prop. It bundles three obligations:

1. CharacterizesOn C valid languageOf — the valid codes are adequate: their range is exactly C.
2. MembershipSemiDecidable languageOf — the encoding is effective: membership is uniformly recursively enumerable from the raw code, so languageOf cannot hide noncomputable semantic information in the decoding map.
3. The relevant predicate is ComputablePredOnPromise: one partial-recursive evaluator must halt and answer correctly on every valid code. It may diverge on invalid syntax, and valid itself need not be decidable.

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 supplied effective presentation. Without (1)–(2), a result could instead be vacuous or rely on an arbitrary, non-effective semantic map.

Main definitions

• MembershipSemiDecidable
• Characterizes
• CharacterizesOn
• 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 recognized from c; in particular, the semantic map cannot smuggle a non-r.e. membership oracle into the meaning of a raw 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 CharacterizesOn {α Code : Type} (C : Set (Language α)) (valid : Code → Prop) (languageOf : Code → Language α) : Prop

The valid codes characterize C: every valid code denotes a language in C, and every language in C has at least one valid code.

The promise may be semantic. For example, raw program syntax is computably encoded while valid c says that program c halts on every word.

Equations

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

theorem characterizesOn_true_iff {α Code : Type} (C : Set (Language α)) (languageOf : Code → Language α) : CharacterizesOn C (fun (x : Code) => True) languageOf ↔ Characterizes C languageOf

With the trivial promise, CharacterizesOn is the original range characterization.

theorem Characterizes.onTrue {α Code : Type} {C : Set (Language α)} {languageOf : Code → Language α} (h : Characterizes C languageOf) : CharacterizesOn C (fun (x : Code) => True) languageOf

An ordinary characterization supplies a characterization under the trivial promise.

def ComputableMembership {α Code : Type} [Primcodable Code] [Primcodable α] (C : Set (Language α)) (languageOf : Code → Language α) (valid : Code → Prop := fun (x : Code) => True) : 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

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

def ComputableEmptiness {α Code : Type} [Primcodable Code] [Primcodable α] (C : Set (Language α)) (languageOf : Code → Language α) (valid : Code → Prop := fun (x : Code) => True) : 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 valid = (CharacterizesOn C valid languageOf ∧ MembershipSemiDecidable languageOf ∧ ComputablePredOnPromise valid fun (c : Code) => languageOf c = ∅)

def ComputableUniversality {α Code : Type} [Primcodable Code] [Primcodable α] (C : Set (Language α)) (languageOf : Code → Language α) (valid : Code → Prop := fun (x : Code) => True) : 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 valid = (CharacterizesOn C valid languageOf ∧ MembershipSemiDecidable languageOf ∧ ComputablePredOnPromise valid fun (c : Code) => languageOf c = Set.univ)

def ComputableEquivalence {α Code : Type} [Primcodable Code] [Primcodable α] (C : Set (Language α)) (languageOf : Code → Language α) (valid : Code → Prop := fun (x : Code) => True) : 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

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