def contextFreeLanguageOf {T : Type} (G : EncodedCFG T) : Language T

The language represented by an encoded context-free grammar.

Equations

• contextFreeLanguageOf G = CF_language G.toCFGrammar

def contextFreeMembershipPredicate {T : Type} (p : EncodedCFG T × List T) : Prop

The uniform membership predicate for encoded context-free grammars.

The input is a pair (G, w), with both the encoded grammar and the word freshly provided to the predicate.

Equations

• contextFreeMembershipPredicate p = (p.2 ∈ contextFreeLanguageOf p.1)

@[reducible, inline]

abbrev ContextFreeComputableMembership (T : Type) [Primcodable T] (C : Set (Language T)) : Prop

Uniform computability of membership for encoded context-free grammars, relative to the language class C.

Equations

• ContextFreeComputableMembership T C = ComputableMembership C contextFreeLanguageOf