Linear Languages

This file defines the class of linear languages. A linear grammar is a context-free grammar in which every production has at most one nonterminal on the right-hand side. Equivalently, every rule has the form A → w or A → u B v where u, v are terminal strings and B is a nonterminal.

Linear languages sit strictly between the regular and the context-free languages in the Chomsky hierarchy:

Regular ⊊ Linear ⊊ Context-Free

Main declarations

• linear_output — Predicate: a symbol string has at most one nonterminal.
• grammar_linear — Predicate: an unrestricted grammar is linear.
• is_Linear — A language is linear.
• Linear — The class of linear languages.

def linear_output {T N : Type} (s : List (symbol T N)) : Prop

A symbol string has linear output form if it contains at most one nonterminal. Concretely, it is either a purely terminal string or can be decomposed as map terminal u ++ [nonterminal B] ++ map terminal v.

Equations

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

def grammar_linear {T : Type} (g : grammar T) : Prop

An unrestricted grammar is linear if every rule is context-free (empty left/right context) and has linear output.

Equations

• grammar_linear g = ∀ r ∈ g.rules, r.input_L = [] ∧ r.input_R = [] ∧ linear_output r.output_string

def is_Linear {T : Type} (L : Language T) : Prop

A language is linear if it is generated by some linear unrestricted grammar.

Equations

• is_Linear L = ∃ (g : grammar T), grammar_linear g ∧ grammar_language g = L

def Linear {T : Type} : Set (Language T)

The class of linear languages.

Equations

• Linear = setOf is_Linear