Context-Free Languages

This file defines the class of context-free languages via unrestricted grammars satisfying the context-free rule-shape property.

def grammar_context_free {T : Type} (g : grammar T) : Prop

An unrestricted grammar is context-free if every rule has empty left and right context.

Equations

• grammar_context_free g = ∀ r ∈ g.rules, r.input_L = [] ∧ r.input_R = []

def is_CF {T : Type} (L : Language T) : Prop

Predicate that a language is context-free.

Equations

• is_CF L = ∃ (g : grammar T), grammar_context_free g ∧ grammar_language g = L

def is_CF_via_cfg {T : Type} (L : Language T) : Prop

Characterization of context-free languages via CF_grammar.

Equations

• is_CF_via_cfg L = ∃ (g : CF_grammar T), CF_language g = L

def CF {T : Type} : Set (Language T)

The class of context-free languages.

Equations

• CF = setOf is_CF