Computability of Membership for Deterministic Context-Free Languages

Membership here is the joint problem specified by a grammar code and a word. Since the repository does not yet have an EncodedDPDA, we use raw EncodedCFG codes and the semantic promise that the grammar's language is deterministic context-free. The existing CYK algorithm is total on every encoded CFG, and therefore uniformly decides membership on the promised DCFL codes in particular.

Main results

• DCFEncodedCFG.eval_decidesMembership – the encoded grammar and word are joint inputs to one uniform membership procedure, correct under DCFEncodedCFG.Valid.
• DCFEncodedCFG.exists_valid_iff_is_DCF – the valid encoded grammars present exactly the deterministic context-free languages.
• DCFEncodedCFG.dcf_computableMembership – the complete result packaged by the promise-aware ComputableMembership predicate.
• dcf_membership_computable – membership in a fixed deterministic context-free language is a ComputablePred.

def DCFEncodedCFG.Valid {T : Type} [Fintype T] (G : EncodedCFG T) : Prop

The semantic promise that a raw encoded context-free grammar presents a deterministic context-free language.

Equations

• DCFEncodedCFG.Valid G = is_DCF (contextFreeLanguageOf G)

theorem DCFEncodedCFG.exists_valid_iff_is_DCF {T : Type} [Fintype T] (L : Language T) : (∃ (G : EncodedCFG T), Valid G ∧ contextFreeLanguageOf G = L) ↔ is_DCF L

The valid raw encoded grammars present exactly the deterministic context-free languages. Validity is a semantic promise; it is not asserted to be decidable.

def DCFEncodedCFG.evalMembership {T : Type} [Fintype T] [DecidableEq T] (G : EncodedCFG T) (w : List T) : Part Bool

Run the existing encoded-CFG membership checker as a partial Boolean evaluator. It is in fact total even when the DCFL promise does not hold.

Equations

• DCFEncodedCFG.evalMembership G w = Part.some (checkMembershipEncoded (G, w))

theorem DCFEncodedCFG.evalMembership_partrec₂ {T : Type} [Fintype T] [DecidableEq T] [Primcodable T] : Partrec₂ evalMembership

The encoded-CFG membership evaluator is partial recursive jointly in the raw grammar code and the input word.

theorem DCFEncodedCFG.eval_decidesMembership {T : Type} [Fintype T] [DecidableEq T] [Primcodable T] : DecidesOnPromise Valid evalMembership fun (G : EncodedCFG T) (w : List T) => w ∈ contextFreeLanguageOf G

A single evaluator decides membership from an encoded grammar and a word, under the promise that the encoded grammar presents a deterministic context-free language.

The evaluator is actually total and correct for every raw EncodedCFG; the promise is used to restrict the presented language class to exactly the DCFLs.

theorem DCFEncodedCFG.dcf_computableMembership {T : Type} [Fintype T] [DecidableEq T] [Primcodable T] : ComputableMembership DCF contextFreeLanguageOf Valid

DCFL membership is uniformly computable from an encoded grammar and a word. Valid encoded CFGs present exactly the deterministic context-free languages, raw CFG membership is effective, and the joint CYK evaluator is total and correct (in fact on every raw CFG code).

theorem dcf_membership_computable {T : Type} [Fintype T] [DecidableEq T] [Primcodable T] {L : Language T} (hL : is_DCF L) : ComputablePred fun (w : List T) => w ∈ L

Membership in any fixed deterministic context-free language is a computable predicate. This is a corollary of the effective encoded-grammar membership algorithm, via DCF ⊆ CF.