Langlib

Langlib is a Lean 4 library of formalized results from formal language theory, defining and relating various grammars, language classes, and automata across the Chomsky hierarchy and beyond.

📖 Documentation: overview · API reference

Proof overview

The goal of this library is to encapsulate some core results of the (extended) Chomsky hierarchy: inclusions, closures and decidability. The following gives a rough overview over the contents in highly condensed form.

The tables contain standard results. 🔗 indicates that this repository contains a corresponding definition or proof file (possibly for a weaker variant of the result, e.g. ⊊ vs. ⊆ and ⇔ vs. ⇒). More detailed results and developed tooling (e.g., Pumping lemmas, Totalizations) can be found in the documentation.

Hierarchy And Equivalences

Each class of the (extended) hierarchy is charaterized as grammar or automaton (or both, and variants thereof). We show (strict) inclusions of the classes and equivalences between different characterizations.

In an inclusion row, a link is attached only when the cited file states a theorem explicitly for the language or presentation classes displayed in that column. The proof may use established equivalences. Parenthesized ⊆ links record a proved weaker inclusion when the displayed strict result is not yet formalized for those classes.

Class Name	Grammar	Relation	Automaton
Regular	Regular (Left-regular 🔗 ⇔🔗 Right-regular 🔗)	⇔ 🔗	Finite Automata 🔗 (NFA ⇔ 🔗 DFA)
	⊊ 🔗		⊊ 🔗
Deterministic context-free	LR(k) 🔗	⇔ 🔗	Deterministic Pushdown Automata 🔗
	⊊ 🔗		⊊ 🔗
Context-free	Context-free 🔗	⇔ 🔗	Pushdown Automata 🔗 (Final State ⇔ 🔗 Empty Stack)
	⊊ 🔗 (⊊ CS 🔗)		⊊
Indexed	Indexed 🔗	⇔	Nested Stack Automata
	⊊ 🔗		⊊
Context-sensitive	Context-sensitive 🔗 (Non-erasing ⇔ 🔗 Non-contracting 🔗)	⇔ 🔗	Linear Bounded Automaton 🔗 (DLBA 🔗 ⇔? NLBA (⊆ 🔗))
			⊊ 🔗
Recursive	⊊ 🔗 (⊆ 🔗)		Turing-machines with halting deciders 🔗
			⊊ 🔗
Recursively Enumerable	Unrestricted 🔗	⇔ 🔗	Turing-machines 🔗

The strict inclusion Indexed ⊊ CS is formalized for finite alphabets with at least two symbols. The underlying inclusion Indexed ⊆ CS 🔗 holds over every terminal type.

Additional results

Context Free Languages ⇔ 🔗 Mathlib's IsContextFree.
Regular ⊊ 🔗 Linear ⊊ 🔗 Context-free.
Regular ⊆ 🔗 Recursive.
Context-free ⊆ 🔗 Recursive.

Closure

We define abstract closure predicates (ClosedUnderUnion, ClosedUnderHomomorphism, etc.) for uniform proofs in 🔗.

Operation	Regular	DCFL	CFL	IND	CSL	Recursive	RE
Union	Yes 🔗	No 🔗	Yes 🔗	Yes 🔗	Yes 🔗	Yes 🔗	Yes 🔗
Intersection	Yes 🔗	No 🔗	No 🔗	No	Yes 🔗	Yes 🔗	Yes 🔗
Complement	Yes 🔗	Yes 🔗	No 🔗	No	Yes 🔗	Yes 🔗	No 🔗
Concatenation	Yes 🔗	No 🔗	Yes 🔗	Yes 🔗	Yes 🔗	Yes 🔗	Yes 🔗
Kleene star	Yes 🔗	No 🔗	Yes 🔗	Yes 🔗	Yes 🔗	Yes 🔗	Yes 🔗
(String) homomorphism	Yes 🔗	No 🔗	Yes 🔗	Yes 🔗	No 🔗	No 🔗	Yes 🔗
`ε`-free (string) homomorphism	Yes 🔗	No 🔗	Yes 🔗	Yes 🔗	Yes 🔗	Yes 🔗	Yes 🔗
Substitution	Yes 🔗	No 🔗	Yes 🔗	Yes 🔗	No 🔗	No 🔗	Yes 🔗
Inverse homomorphism	Yes 🔗	Yes 🔗	Yes 🔗	Yes 🔗	Yes 🔗	Yes 🔗	Yes 🔗
Reverse	Yes 🔗	No 🔗	Yes 🔗	Yes 🔗	Yes 🔗	Yes 🔗	Yes 🔗
Intersection with a regular language	Yes 🔗	Yes 🔗	Yes 🔗	Yes 🔗	Yes 🔗	Yes 🔗	Yes 🔗
Right quotient	Yes 🔗	No 🔗	No 🔗	No	No 🔗	No 🔗	Yes 🔗
Right quotient with a regular language	Yes 🔗	Yes 🔗	Yes 🔗	Yes 🔗	No 🔗	No 🔗	Yes 🔗

For a negative closure entry, No means that closure fails over some finite alphabet; it does not claim failure over every alphabet. The linked files expose embedding/cardinality variants (for example, _of_embedding and _of_card) giving the proved sufficient alphabet-size bounds. Positive entries are stated uniformly over the finite alphabet assumptions required by their definitions.

Additional DCFL results:

Union with a regular language

Additional CFL results:

Additional CSL results:

Terminal bijections

Decidability

Membership is the uniform word problem for a concrete presentation: the input is a valid encoded automaton or grammar together with a word. ComputableMembership 🔗 takes an optional validity promise, requires valid codes to present exactly the stated language class, and requires one partial-recursive evaluator to halt and answer correctly on every valid code-and-word pair. It separately requires raw encoded membership to be uniformly recursively enumerable; this prevents the semantic decoding map itself from hiding a non-r.e. membership oracle.

The remaining columns use the corresponding uniform emptiness, universality, and equivalence problems for the indicated standard presentation.

Language	Membership	Emptiness	Universality	Equivalence
Regular	✓ 🔗	✓ 🔗	✓ 🔗	✓ 🔗
Deterministic context-free	✓ 🔗	✓ 🔗	✓	✓
Context-free	✓ 🔗	✓ 🔗	✗	✗
Context-sensitive	✓ 🔗	✗	✗	✗
Recursive	✓ 🔗	✗ 🔗	✗ 🔗	✗ 🔗
Recursively enumerable	✗ 🔗	✗ 🔗	✗ 🔗	✗ 🔗

For Recursive membership, the input program is promised to be an always-halting decider. The linked theorem supplies one universal evaluator taking the raw program code and word jointly, proves that it halts and is correct under that promise, and shows that valid codes present exactly the recursive languages over every finite computably encoded alphabet. Emptiness, universality, and equivalence are undecidable for this presentation over every nonempty computably encoded alphabet; nonemptiness is optimal because an empty alphabet has only the empty word. The separate diagonal result 🔗 says that these semantically valid programs cannot instead be replaced by an adequate Primcodable type on which membership is total for every raw code; that is a different, stronger requirement.

How To Use The Library

For most uses, import the hub:

import Langlib

If you only need one part of the development, import the corresponding module directly, for example:

import Langlib.Classes.ContextFree.Definition
import Langlib.Grammars.ContextFree.Definition
import Langlib.Automata.Pushdown.Equivalence.ContextFree
import Langlib.Classes.Regular.Decidability.Membership
import Langlib.Classes.Recursive.Decidability.Membership

The files in test/LanglibTest provide small worked examples:

To build the library and examples, run:

lake build

Installation Instructions

To install Lean 4, follow the Lean community manual.

To download and build this project, run:

git clone https://github.com/nielstron/langlib
cd langlib
lake build

Acknowledgements

This repository started as a Lean 4 port of madvorak/grammars. It further includes a port of the Pumping Lemma proof from AlexLoitzl/pumping_cfg and the equivalence proof between CFGs and PDAs from shetzl/autth.

A part of this repository was created with the help of Aristotle. It's an amazing tool for ambitious proofs. Special thanks to the developers to provide this tool to the community!