Non-Contracting Grammar Definitions

This file defines non-contracting grammars as unrestricted grammars whose rules never decrease the length of the rewritten sentential form. It also contains the grammar-level translation machinery relating non-contracting grammars to context-sensitive grammars.

Overview

A non-contracting grammar (also called monotone grammar) is an unrestricted grammar where every rule satisfies |output| ≥ |input|, i.e., the right-hand side is at least as long as the left-hand side.

The equivalence of these two formulations is a classical result in formal language theory. Every context-sensitive grammar is non-contracting (easy direction), and every non-contracting grammar can in principle be converted to an equivalent context-sensitive grammar (hard direction).

Main declarations

• grammar_noncontracting — predicate for non-contracting unrestricted grammars
• is_noncontracting — language class of non-contracting grammars

References

The equivalence is standard; see e.g. Hopcroft, Motwani, Ullman, "Introduction to Automata Theory, Languages, and Computation", Chapter 9.

Non-contracting grammars

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

An unrestricted grammar is non-contracting (monotone) if for every rule, the output string is at least as long as the full input pattern input_L ++ [input_N] ++ input_R.

Equations

• grammar_noncontracting g = ∀ r ∈ g.rules, r.output_string.length ≥ r.input_L.length + 1 + r.input_R.length

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

Predicate: a language is generated by some non-contracting grammar.

Equations

• is_noncontracting L = ∃ (g : grammar T), grammar_noncontracting g ∧ grammar_language g = L