Unrestricted Grammar Definitions

This file defines unrestricted grammars and their derivations.

Main declarations

• symbol
• grammar
• grammar_derives
• grammar_language

inductive symbol (T N : Type) : Type

The type of symbols is the disjoint union of terminals and nonterminals.

• terminal {T N : Type} : T → symbol T N
• nonterminal {T N : Type} : N → symbol T N

instance instDecidableEqSymbol_1 {T✝ N✝ : Type} [DecidableEq T✝] [DecidableEq N✝] : DecidableEq (symbol T✝ N✝)

Equations

• instDecidableEqSymbol_1 = instDecidableEqSymbol_1.decEq

def instDecidableEqSymbol_1.decEq {T✝ N✝ : Type} [DecidableEq T✝] [DecidableEq N✝] (x✝ x✝¹ : symbol T✝ N✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqSymbol_1.decEq (symbol.terminal a) (symbol.terminal b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqSymbol_1.decEq (symbol.terminal a) (symbol.nonterminal a_1) = isFalse ⋯
• instDecidableEqSymbol_1.decEq (symbol.nonterminal a) (symbol.terminal a_1) = isFalse ⋯
• instDecidableEqSymbol_1.decEq (symbol.nonterminal a) (symbol.nonterminal b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

structure grule (T N : Type) : Type

Transformation rule for a grammar without any restrictions.

• input_L : List (symbol T N)
• input_N : N
• input_R : List (symbol T N)
• output_string : List (symbol T N)

structure grammar (T : Type) : Type 1

Grammar (unrestricted) that generates words over the alphabet T (a type of terminals).

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

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

One step of grammatical transformation.

Equations

• One or more equations did not get rendered due to their size.

def grammar_derives {T : Type} (g : grammar T) : List (symbol T g.nt) → List (symbol T g.nt) → Prop

Any number of steps of grammatical transformation; reflexive+transitive closure of grammar_transforms.

Equations

• grammar_derives g = Relation.ReflTransGen (grammar_transforms g)

def grammar_generates {T : Type} (g : grammar T) (w : List T) : Prop

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

Equations

• grammar_generates g w = grammar_derives g [symbol.nonterminal g.initial] (List.map symbol.terminal w)

def grammar_language {T : Type} (g : grammar T) : Language T

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

Equations

• grammar_language g = setOf (grammar_generates g)