Decidable Grammar Membership Test

This file shows that the basic operations of unrestricted grammars are decidable / computable, which is needed to express grammar membership as a search procedure.

Main results

• applyRuleAt — computable function that applies a rule at a position
• applyRuleSeq — computable function that applies a sequence of rules
• extractTerminals — extract the terminal word from a terminal sentential form
• grammarTest — the decidable test for grammar membership
• grammarTest_sound / grammarTest_complete — correctness of the test

Computable rule application

def applyRuleAt {T : Type} [DecidableEq T] {N : Type} [DecidableEq N] (r : grule T N) (sf : List (symbol T N)) (pos : ℕ) : Option (List (symbol T N))

Given a grammar, a sentential form, a rule index, and a position, attempt to apply the rule at that position. Returns none if the rule doesn't match at that position.

Equations

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

theorem applyRuleAt_correct {T : Type} [DecidableEq T] {N : Type} [DecidableEq N] (r : grule T N) (sf sf' : List (symbol T N)) (pos : ℕ) (h : applyRuleAt r sf pos = some sf') : ∃ (u : List (symbol T N)) (v : List (symbol T N)), sf = u ++ r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R ++ v ∧ sf' = u ++ r.output_string ++ v

def applyRuleSeq {T : Type} [DecidableEq T] {N : Type} [DecidableEq N] (rules : List (grule T N)) (init : List (symbol T N)) (seq : List (ℕ × ℕ)) : Option (List (symbol T N))

Apply a sequence of (rule_index, position) pairs to a sentential form, starting from a given initial form. Returns none if any step fails.

This is the core "derivation simulator": given a sequence of instructions [(r₀, p₀), (r₁, p₁), ...], it:

1. Starts with init
2. Applies rule rules[rᵢ] at position pᵢ
3. Returns the final sentential form (or none if any step fails)

Equations

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

theorem applyRuleSeq_derives {T : Type} [DecidableEq T] (g : grammar T) [DecidableEq g.nt] (init sf' : List (symbol T g.nt)) (seq : List (ℕ × ℕ)) (h : applyRuleSeq g.rules init seq = some sf') : grammar_derives g init sf'

Terminal checking

def extractTerminals {T N : Type} (sf : List (symbol T N)) : Option (List T)

Extract the terminal word from a sentential form, if all symbols are terminals. Returns none if any nonterminal is present.

Equations

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

theorem extractTerminals_eq_map_iff {T N : Type} (sf : List (symbol T N)) (w : List T) : extractTerminals sf = some w ↔ sf = List.map symbol.terminal w

The Grammar Test Function

The key function: given a derivation sequence (encoded as a List (ℕ × ℕ)) and an input word w, check whether the derivation produces w.

def grammarTest {T : Type} [DecidableEq T] (g : grammar T) [DecidableEq g.nt] (seq : List (ℕ × ℕ)) (w : List T) : Bool

The grammar membership test.

Given a grammar g, a derivation sequence seq, and a target word w:

1. Apply the rule sequence starting from [nonterminal g.initial]
2. Check if the result is exactly w.map symbol.terminal

Returns true iff the derivation sequence witnesses w ∈ grammar_language g.

Equations

• grammarTest g seq w = match applyRuleSeq g.rules [symbol.nonterminal g.initial] seq with | none => false | some sf => extractTerminals sf == some w

theorem grammarTest_sound {T : Type} [DecidableEq T] (g : grammar T) [DecidableEq g.nt] (seq : List (ℕ × ℕ)) (w : List T) (h : grammarTest g seq w = true) : w ∈ grammar_language g

theorem grammarTest_complete {T : Type} [DecidableEq T] (g : grammar T) [DecidableEq g.nt] (w : List T) (hw : w ∈ grammar_language g) : ∃ (seq : List (ℕ × ℕ)), grammarTest g seq w = true