Context-Free Grammar Definitions

This file defines context-free grammars, their derivation relation, and the induced language predicate.

Main declarations

• CF_grammar
• CF_transforms
• CF_derives
• CF_language

structure CF_grammar (T : Type) : Type 1

Context-free grammar that generates words over the alphabet T (a type of terminals).

• nt : Type
• initial : self.nt
• rules : List (self.nt × List (symbol T self.nt))

def CF_transforms {T : Type} (g : CF_grammar T) (w₁ w₂ : List (symbol T g.nt)) : Prop

One step of context-free transformation.

Equations

• CF_transforms g w₁ w₂ = ∃ (r : g.nt × List (symbol T g.nt)) (u : List (symbol T g.nt)) (v : List (symbol T g.nt)), r ∈ g.rules ∧ w₁ = u ++ [symbol.nonterminal r.1] ++ v ∧ w₂ = u ++ r.2 ++ v

def CF_derives {T : Type} (g : CF_grammar T) : List (symbol T g.nt) → List (symbol T g.nt) → Prop

Any number of steps of context-free transformation; reflexive+transitive closure of CF_transforms.

Equations

• CF_derives g = Relation.ReflTransGen (CF_transforms g)

def CF_generates_str {T : Type} (g : CF_grammar T) (s : List (symbol T g.nt)) : Prop

Accepts a string (a List of symbols) iff it can be derived from the initial nonterminal.

Equations

• CF_generates_str g s = CF_derives g [symbol.nonterminal g.initial] s

def CF_generates {T : Type} (g : CF_grammar T) (w : List T) : Prop

Accepts a word (a List of terminals) iff it can be derived from the initial nonterminal.

Equations

• CF_generates g w = CF_generates_str g (List.map symbol.terminal w)

def CF_language {T : Type} (g : CF_grammar T) : Language T

The Set of words that can be derived from the initial nonterminal.

Equations

• CF_language g = setOf (CF_generates g)