Context-sensitive grammars

DefinitionNonterminal grammar symbols#✓fully proved

Whether a grammar symbol (Mathlib.Computability.Language.Symbol, shared with the context-free development) is a nonterminal.

def Symbol.isNonterminal {T N : Type*} : Symbol T N → Bool
  | .nonterminal _ => true
  | .terminal _ => false

Used by 3

Used byThe \(a^n b^n c^n\) grammar is context-sensitive · Context-sensitive grammar · The grammar of an LBA is context-sensitive

StructureUnrestricted grammar#✓fully proved

An unrestricted grammar: a finite list of productions and an initial nonterminal.

structure CSGrammar (T N : Type*) where
  /-- The finite list of productions, each a pair of symbol lists. -/
  rules : List (List (Symbol T N) × List (Symbol T N))
  /-- The initial nonterminal. -/
  initial : N

Used by 41

Used byThe word aabbcc is generated by the \(a^n b^n c^n\) grammar · Context-sensitive grammar for \(a^n b^n c^n\) · The \(a^n b^n c^n\) grammar is context-sensitive · The word abc is generated by the \(a^n b^n c^n\) grammar · Derivation in an unrestricted grammar · Derivations preserve balancedness · Context-sensitive grammar · Language of an unrestricted grammar · Generated words have equally many a's, b's and c's · One rewriting step of a grammar · Rewriting steps preserve balancedness · Applying a production in context is a grammar step · Derivations compose under concatenation · Derivations extend by a left context · Derivations extend by a right context · Non-head or accepting cells convert to terminals · Runs of an LBA give grammar derivations · An LBA step is a grammar derivation step on encodings · Generated form derives the initial configuration encoding · The generator derives the middle cells and itself · Replacing a block by a rule is a derivation step · Setting one list position by a production is a derivation step · Setting two adjacent list positions by a production is a derivation step · Two-cell replacement at indices \(i\) and \(j = i + 1\) · Replacing a single cell is a derivation step · Singleton-to-singleton productions are derivation steps · Tail cells derive their activated encoding · Transitivity of grammar derivations · Replacing two consecutive cells is a derivation step · The grammar of an LBA · The grammar of an LBA is context-sensitive · The activation rule belongs to the LBA grammar · The accepting conversion rule belongs to the LBA grammar · The non-head conversion rule belongs to the LBA grammar · The final generation rule belongs to the LBA grammar · The one-cell generation rule belongs to the LBA grammar · The first generation rule belongs to the LBA grammar · The generator step rule belongs to the LBA grammar · Left transitions give simulation rules · Right transitions give simulation rules · Stay transitions give simulation rules

DefinitionOne rewriting step of a grammar#✓fully proved

One rewriting step: apply a production in a sentential form context. This is the generic Cslib.Decidability.Rewriting.Step at the grammar's rules, so grammar derivations reuse the string-rewriting API instead of a second, incompatible copy of it.

def Rewrites {T N : Type*} (g : CSGrammar T N) (u v : List (Symbol T N)) : Prop :=
  Cslib.Decidability.Rewriting.Step g.rules u v

Uses 2 · Used by 1

Statement usesOne-step rewriting · Unrestricted grammar

Used byRewriting steps preserve balancedness

DefinitionDerivation in an unrestricted grammar#✓fully proved

Derivation: the reflexive-transitive closure of rewriting.

def Derives {T N : Type*} (g : CSGrammar T N) (u v : List (Symbol T N)) : Prop :=
  Cslib.Decidability.Rewriting.Derives g.rules u v

Uses 2 · Used by 25

Statement usesDerivations in a string rewriting system · Unrestricted grammar

Used byThe word aabbcc is generated by the \(a^n b^n c^n\) grammar · The word abc is generated by the \(a^n b^n c^n\) grammar · Derivations preserve balancedness · Language of an unrestricted grammar · Applying a production in context is a grammar step · Derivations compose under concatenation · Derivations extend by a left context · Derivations extend by a right context · Non-head or accepting cells convert to terminals · Runs of an LBA give grammar derivations · An LBA step is a grammar derivation step on encodings · Generated form derives the initial configuration encoding · The generator derives the middle cells and itself · The generator derives the full tail of cells · Replacing a block by a rule is a derivation step · Setting one list position by a production is a derivation step · Setting two adjacent list positions by a production is a derivation step · Two-cell replacement at indices \(i\) and \(j = i + 1\) · Replacing a single cell is a derivation step · Singleton-to-singleton productions are derivation steps · The start symbol derives the generated form of a word · Tail cells derive their activated encoding · Transitivity of grammar derivations · Replacing two consecutive cells is a derivation step · If the LBA accepts a nonempty word, the grammar derives it

DefinitionLanguage of an unrestricted grammar#✓fully proved

The language of a grammar: terminal words derived from the initial nonterminal.

def language {T N : Type*} (g : CSGrammar T N) : Set (List T) :=
  {w | Derives g [Symbol.nonterminal g.initial] (w.map Symbol.terminal)}

Uses 2 · Used by 5

Statement usesUnrestricted grammar · Derivation in an unrestricted grammar

Used byThe word aabbc is not generated by the \(a^n b^n c^n\) grammar · The word aabbcc is generated by the \(a^n b^n c^n\) grammar · The word abc is generated by the \(a^n b^n c^n\) grammar · Generated words have equally many a's, b's and c's · If the LBA accepts a nonempty word, the grammar derives it

DefinitionContext-sensitive grammar#✓fully proved

A grammar is context-sensitive when every production has a nonterminal on its left side (so the left side is nonempty and not terminal-only) and no production shrinks. The standard S → ε exception is not used here: the aⁿbⁿcⁿ grammar has n ≥ 1.

def IsContextSensitive {T N : Type*} (g : CSGrammar T N) : Prop :=
  ∀ r ∈ g.rules, r.1.any (·.isNonterminal) = true ∧ r.1.length ≤ r.2.length

Uses 2 · Used by 2

Statement usesUnrestricted grammar · Nonterminal grammar symbols

Used byThe \(a^n b^n c^n\) grammar is context-sensitive · The grammar of an LBA is context-sensitive

InductiveTerminals of the \(a^n b^n c^n\) grammar#✓fully proved

Terminals of the aⁿbⁿcⁿ grammar.

inductive ABC where
  | a : ABC
  | b : ABC
  | c : ABC
  deriving DecidableEq, Repr

Used by 16

Used byThe word aabbc is not generated by the \(a^n b^n c^n\) grammar · The word aabbcc is generated by the \(a^n b^n c^n\) grammar · Context-sensitive grammar for \(a^n b^n c^n\) · The \(a^n b^n c^n\) grammar is context-sensitive · The word abc is generated by the \(a^n b^n c^n\) grammar · Balanced sentential form · The initial sentential form is balanced · Symbol count of a sentential form · Count of a's in a sentential form · Count of b's in a sentential form · Count of c's in a sentential form · Symbol counts are additive over concatenation · Derivations preserve balancedness · Generated words have equally many a's, b's and c's · Rewriting steps preserve balancedness · Applying a production in context is a grammar step

InductiveNonterminals of the \(a^n b^n c^n\) grammar#✓fully proved

Nonterminals of the aⁿbⁿcⁿ grammar.

inductive ABCNT where
  | S : ABCNT
  | B : ABCNT
  | C : ABCNT
  deriving DecidableEq, Repr

Used by 16

Used byThe word aabbc is not generated by the \(a^n b^n c^n\) grammar · The word aabbcc is generated by the \(a^n b^n c^n\) grammar · Context-sensitive grammar for \(a^n b^n c^n\) · The \(a^n b^n c^n\) grammar is context-sensitive · The word abc is generated by the \(a^n b^n c^n\) grammar · Balanced sentential form · The initial sentential form is balanced · Symbol count of a sentential form · Count of a's in a sentential form · Count of b's in a sentential form · Count of c's in a sentential form · Symbol counts are additive over concatenation · Derivations preserve balancedness · Generated words have equally many a's, b's and c's · Rewriting steps preserve balancedness · Applying a production in context is a grammar step

DefinitionContext-sensitive grammar for \(a^n b^n c^n\)#✓fully proved

The standard context-sensitive grammar for {aⁿbⁿcⁿ | n ≥ 1}.

def abcGrammar : CSGrammar ABC ABCNT where
  rules :=
    [ ([.nonterminal .S], [.terminal .a, .nonterminal .S, .nonterminal .B, .nonterminal .C])
    , ([.nonterminal .S], [.terminal .a, .nonterminal .B, .nonterminal .C])
    , ([.nonterminal .C, .nonterminal .B], [.nonterminal .B, .nonterminal .C])
    , ([.terminal .a, .nonterminal .B], [.terminal .a, .terminal .b])
    , ([.terminal .b, .nonterminal .B], [.terminal .b, .terminal .b])
    , ([.terminal .b, .nonterminal .C], [.terminal .b, .terminal .c])
    , ([.terminal .c, .nonterminal .C], [.terminal .c, .terminal .c]) ]
  initial := .S

Uses 3 · Used by 8

Statement usesTerminals of the \(a^n b^n c^n\) grammar · Nonterminals of the \(a^n b^n c^n\) grammar · Unrestricted grammar

Used byThe word aabbc is not generated by the \(a^n b^n c^n\) grammar · The word aabbcc is generated by the \(a^n b^n c^n\) grammar · The \(a^n b^n c^n\) grammar is context-sensitive · The word abc is generated by the \(a^n b^n c^n\) grammar · Derivations preserve balancedness · Generated words have equally many a's, b's and c's · Rewriting steps preserve balancedness · Applying a production in context is a grammar step

TheoremApplying a production in context is a grammar step#✓fully proved

One grammar step: rewrite lhs to rhs in context p, q.

theorem step (lhs rhs p q : List (Symbol ABC ABCNT))
    (h : (lhs, rhs) ∈ abcGrammar.rules) :
    Derives abcGrammar (p ++ lhs ++ q) (p ++ rhs ++ q)

Uses 8 · Used by 2

Statement usesTerminals of the \(a^n b^n c^n\) grammar · Nonterminals of the \(a^n b^n c^n\) grammar · Unrestricted grammar · Derivation in an unrestricted grammar · Context-sensitive grammar for \(a^n b^n c^n\)

Proof usesDerivations in a string rewriting system · Rewriting rules · One-step rewriting

Used byThe word aabbcc is generated by the \(a^n b^n c^n\) grammar · The word abc is generated by the \(a^n b^n c^n\) grammar

TheoremThe \(a^n b^n c^n\) grammar is context-sensitive#✓fully proved

Every production of the aⁿbⁿcⁿ grammar is length-nondecreasing, so the grammar is context-sensitive.

theorem abcGrammar_contextSensitive : IsContextSensitive abcGrammar

Uses 6

Statement usesTerminals of the \(a^n b^n c^n\) grammar · Nonterminals of the \(a^n b^n c^n\) grammar · Context-sensitive grammar · Context-sensitive grammar for \(a^n b^n c^n\)

Proof usesUnrestricted grammar · Nonterminal grammar symbols

TheoremThe word abc is generated by the \(a^n b^n c^n\) grammar#✓fully proved

abc is generated.

theorem abc_mem : [ABC.a, ABC.b, ABC.c] ∈ language abcGrammar

Uses 10

Statement usesTerminals of the \(a^n b^n c^n\) grammar · Nonterminals of the \(a^n b^n c^n\) grammar · Context-sensitive grammar for \(a^n b^n c^n\) · Language of an unrestricted grammar

Proof usesDerivations in a string rewriting system · Rewriting rules · One-step rewriting · Unrestricted grammar · Derivation in an unrestricted grammar · Applying a production in context is a grammar step

TheoremThe word aabbcc is generated by the \(a^n b^n c^n\) grammar#✓fully proved

aabbcc is generated: grow two a's, shuttle the C's right past the B's, then convert B's and C's to terminals in order.

theorem aabbcc_mem :
    [ABC.a, ABC.a, ABC.b, ABC.b, ABC.c, ABC.c] ∈ language abcGrammar

Uses 10

Statement usesTerminals of the \(a^n b^n c^n\) grammar · Nonterminals of the \(a^n b^n c^n\) grammar · Context-sensitive grammar for \(a^n b^n c^n\) · Language of an unrestricted grammar

Proof usesDerivations in a string rewriting system · Rewriting rules · One-step rewriting · Unrestricted grammar · Derivation in an unrestricted grammar · Applying a production in context is a grammar step

DefinitionSymbol count of a sentential form#✓fully proved

Count of the symbol s in a sentential form (terminals a, b, c, and the "unborn" b/c nonterminals B, C).

def cnt (s : Symbol ABC ABCNT) (u : List (Symbol ABC ABCNT)) : ℕ :=
  u.countP (fun t => decide (t = s))

Uses 2 · Used by 5

Statement usesTerminals of the \(a^n b^n c^n\) grammar · Nonterminals of the \(a^n b^n c^n\) grammar

Used byCount of a's in a sentential form · Count of b's in a sentential form · Count of c's in a sentential form · Symbol counts are additive over concatenation · Rewriting steps preserve balancedness

DefinitionCount of a's in a sentential form#✓fully proved

The a-count of a sentential form.

def cntA (u : List (Symbol ABC ABCNT)) : ℕ :=
  cnt (.terminal .a) u

Uses 3 · Used by 4

Statement usesTerminals of the \(a^n b^n c^n\) grammar · Nonterminals of the \(a^n b^n c^n\) grammar · Symbol count of a sentential form

Used byThe word aabbc is not generated by the \(a^n b^n c^n\) grammar · Balanced sentential form · The initial sentential form is balanced · Rewriting steps preserve balancedness

DefinitionCount of b's in a sentential form#✓fully proved

The b-count: terminal b's plus unborn B's.

def cntB (u : List (Symbol ABC ABCNT)) : ℕ :=
  cnt (.terminal .b) u + cnt (.nonterminal .B) u

Uses 3 · Used by 4

Statement usesTerminals of the \(a^n b^n c^n\) grammar · Nonterminals of the \(a^n b^n c^n\) grammar · Symbol count of a sentential form

Used byThe word aabbc is not generated by the \(a^n b^n c^n\) grammar · Balanced sentential form · The initial sentential form is balanced · Rewriting steps preserve balancedness

DefinitionCount of c's in a sentential form#✓fully proved

The c-count: terminal c's plus unborn C's.

def cntC (u : List (Symbol ABC ABCNT)) : ℕ :=
  cnt (.terminal .c) u + cnt (.nonterminal .C) u

Uses 3 · Used by 4

Statement usesTerminals of the \(a^n b^n c^n\) grammar · Nonterminals of the \(a^n b^n c^n\) grammar · Symbol count of a sentential form

Used byThe word aabbc is not generated by the \(a^n b^n c^n\) grammar · Balanced sentential form · The initial sentential form is balanced · Rewriting steps preserve balancedness

DefinitionBalanced sentential form#✓fully proved

A sentential form is balanced when its a-, b- and c-counts agree.

def Balanced (u : List (Symbol ABC ABCNT)) : Prop :=
  cntA u = cntB u ∧ cntB u = cntC u

Uses 5 · Used by 4

Statement usesTerminals of the \(a^n b^n c^n\) grammar · Nonterminals of the \(a^n b^n c^n\) grammar · Count of a's in a sentential form · Count of b's in a sentential form · Count of c's in a sentential form

Used byThe initial sentential form is balanced · Derivations preserve balancedness · Generated words have equally many a's, b's and c's · Rewriting steps preserve balancedness

TheoremSymbol counts are additive over concatenation#✓fully proved

Counting over a concatenation of three forms splits additively.

theorem cnt_concat3 (p l q : List (Symbol ABC ABCNT)) (s : Symbol ABC ABCNT) :
    cnt s (p ++ l ++ q) = cnt s p + cnt s l + cnt s q

Uses 3 · Used by 1

Statement usesTerminals of the \(a^n b^n c^n\) grammar · Nonterminals of the \(a^n b^n c^n\) grammar · Symbol count of a sentential form

Used byRewriting steps preserve balancedness

TheoremRewriting steps preserve balancedness#✓fully proved

One rewriting step preserves balancedness: every production has the same imbalance on both sides, and the context contributes equally to all three counts.

theorem rewrites_balanced {u v : List (Symbol ABC ABCNT)}
    (h : Rewrites abcGrammar u v) (hu : Balanced u) : Balanced v

Uses 13 · Used by 1

Statement usesTerminals of the \(a^n b^n c^n\) grammar · Nonterminals of the \(a^n b^n c^n\) grammar · Balanced sentential form · One rewriting step of a grammar · Context-sensitive grammar for \(a^n b^n c^n\)

Proof usesRewriting rules · One-step rewriting · Unrestricted grammar · Symbol count of a sentential form · Count of a's in a sentential form · Count of b's in a sentential form · Count of c's in a sentential form · Symbol counts are additive over concatenation

Used byDerivations preserve balancedness

TheoremDerivations preserve balancedness#✓fully proved

Derivations preserve balancedness.

theorem derives_balanced {u v : List (Symbol ABC ABCNT)}
    (h : Derives abcGrammar u v) (hu : Balanced u) : Balanced v

Uses 8 · Used by 1

Statement usesTerminals of the \(a^n b^n c^n\) grammar · Nonterminals of the \(a^n b^n c^n\) grammar · Balanced sentential form · Derivation in an unrestricted grammar · Context-sensitive grammar for \(a^n b^n c^n\)

Proof usesOne-step rewriting · Unrestricted grammar · Rewriting steps preserve balancedness

Used byGenerated words have equally many a's, b's and c's

TheoremThe initial sentential form is balanced#✓fully proved

The initial form [S] is balanced, with all counts zero.

theorem balanced_initial : Balanced [Symbol.nonterminal ABCNT.S]

Uses 6 · Used by 1

Statement usesTerminals of the \(a^n b^n c^n\) grammar · Nonterminals of the \(a^n b^n c^n\) grammar · Balanced sentential form

Proof usesCount of a's in a sentential form · Count of b's in a sentential form · Count of c's in a sentential form

Used byGenerated words have equally many a's, b's and c's

TheoremGenerated words have equally many a's, b's and c's#✓fully proved

Every generated terminal word has equally many a's, b's and c's.

theorem language_subset_balanced {w : List ABC} (hw : w ∈ language abcGrammar) :
    Balanced (w.map Symbol.terminal)

Uses 8 · Used by 1

Statement usesTerminals of the \(a^n b^n c^n\) grammar · Nonterminals of the \(a^n b^n c^n\) grammar · Balanced sentential form · Context-sensitive grammar for \(a^n b^n c^n\) · Language of an unrestricted grammar

Proof usesUnrestricted grammar · The initial sentential form is balanced · Derivations preserve balancedness

Used byThe word aabbc is not generated by the \(a^n b^n c^n\) grammar

TheoremThe word aabbc is not generated by the \(a^n b^n c^n\) grammar#✓fully proved

aabbc is not generated: its counts are 2 = 2 ≠ 1.

theorem aabbc_not_mem : [ABC.a, ABC.a, ABC.b, ABC.b, ABC.c] ∉
    language abcGrammar

Uses 8

Statement usesTerminals of the \(a^n b^n c^n\) grammar · Nonterminals of the \(a^n b^n c^n\) grammar · Context-sensitive grammar for \(a^n b^n c^n\) · Language of an unrestricted grammar

Proof usesCount of a's in a sentential form · Count of b's in a sentential form · Count of c's in a sentential form · Generated words have equally many a's, b's and c's

24 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.