Langlib

Langlib.Classes.Regular.Decidability.Membership

Computability of Membership #

This file proves that membership is computable for regular languages, using ComputablePred rather than the weaker Decidable.

Main results #

Part 1: Regular Languages #

source
theorem dfa_membership_computablePred {α : Type u_1} {σ : Type u_2} [Primcodable α] [Primcodable σ] [Finite σ] [Finite α] (M : DFA α σ) [DecidablePred fun (x : σ) => x ∈ M.accept] :
ComputablePred fun (x : List α) => x ∈ M.accepts

Membership in a DFA's accepted language is a computable predicate.

The proof constructs the computable decision function explicitly as the composition of M.eval (which is List.foldl M.step M.start, primitive recursive by Primrec.list_foldl since M.step is a function from a finite domain) with the accept-state test (primitive recursive by Primrec.dom_finite).

source
noncomputable def regular_membership_computablePred {α : Type u_1} [Primcodable α] [Finite α] (L : Language α) (hL : L.IsRegular) :
ComputablePred fun (x : List α) => x ∈ L

Membership in a regular language is a computable predicate.

Equations
  • ⋯ = ⋯
Instances For

    Part 2: Uniform computability over encoded right-regular grammars #

    source
    theorem Regular.EncodedRG.regular_membership_computablePred {T : Type} [Fintype T] [DecidableEq T] [Primcodable T] :
    ComputablePred fun (p : EncodedRG T × List T) => p.2 ∈ p.1.regularLanguageOf

    The raw uniform membership decider for encoded right-regular grammars, obtained by composing the context-free membership decider with the primitive-recursive translation toCFG : EncodedRG T → EncodedCFG T.

    source
    theorem Regular.EncodedRG.regular_computableMembership {T : Type} [Fintype T] [DecidableEq T] [Primcodable T] :
    ComputableMembership RG regularLanguageOf

    Membership is uniformly computable for the regular languages: encoded right-regular grammars are an adequate, effective presentation (regularLanguageOf_characterizes) with uniformly decidable membership.