Context-Sensitive Grammar Definitions

This file defines context-sensitive grammars, their derivations, and the induced language predicate.

A context-sensitive grammar has rules of the form αAβ → αγβ where:

• α (context_left) and β (context_right) are the context (strings of symbols),
• A (input_nonterminal) is a nonterminal, and
• γ (output_string) is a non-empty string of symbols.

The non-emptiness requirement on γ ensures that derivation steps never decrease the length of the sentential form, which is the defining property of context-sensitive grammars.

Main declarations

• csrule
• CS_grammar
• CS_transforms
• CS_language

structure csrule (T N : Type) : Type

Transformation rule for a context-sensitive grammar.

A rule αAβ → αγβ where α is context_left, A is input_nonterminal, β is context_right, and γ is output_string.

• context_left : List (symbol T N)
• input_nonterminal : N
• context_right : List (symbol T N)
• output_string : List (symbol T N)

structure CS_grammar (T : Type) : Type 1

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

The output_nonempty field ensures that every rule has a non-empty output string, matching the standard definition of context-sensitive grammars. This guarantees that derivation steps never decrease the length of the sentential form.

• nt : Type
• initial : self.nt
• rules : List (csrule T self.nt)
• output_nonempty (r : csrule T self.nt) : r ∈ self.rules → r.output_string ≠ []

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

One step of context-sensitive transformation.

Equations

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

def CS_derives {T : Type} (g : CS_grammar T) : List (symbol T g.nt) → List (symbol T g.nt) → Prop

Any number of steps of context-sensitive transformation; reflexive+transitive closure of CS_transforms.

Equations

• CS_derives g = Relation.ReflTransGen (CS_transforms g)

def CS_language {T : Type} (g : CS_grammar T) : Language T

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

Equations

• CS_language g w = CS_derives g [symbol.nonterminal g.initial] (List.map symbol.terminal w)