Langlib
Langlib is a Lean 4 library of formalized results about grammars, language classes, and automata across the Chomsky hierarchy.
Regular Languages
Linear and DCF Languages
Context-Free Languages
Indexed Languages
Context-Sensitive Languages
Recursive Languages
Recursively Enumerable Languages
Automata
- Pushdown automata
- Deterministic pushdown automata
- Linear bounded automata
- Deterministic linear bounded automata
Examples
Proof overview
🔗 indicates that this repository contains a corresponding proof file.
Hierarchy And Equivalences
| Grammar side | Relation | Automaton side |
|---|---|---|
| Regular languages (Left-regular ⇔🔗 Right-regular) | ⇔ 🔗 | DFA languages (Mathlib) |
| ⊊ 🔗 | ⊊ 🔗 | |
| Deterministic context-free languages | ≝ 🔗 | DPDA final-state languages |
| ⊊ (⊆ 🔗) | ⊊ (⊆ 🔗) | |
| Context-free languages | ⇔ 🔗 | PDA languages (Final State ⇔ Empty Stack 🔗) |
| ⊊ 🔗 (⊆ CS 🔗) | ⊊ | |
| Indexed languages | ⇔ | Nested Stack Automata |
| ⊊ | ⊊ | |
| Context-sensitive languages (Non-erasing ⇔ Non-contracting (⇒ 🔗)) | ⇔ | LBA languages (LBA ⇔? DLBA) |
| ⊊ (⊆ RE 🔗) | ⊊ (⊆ RE 🔗) | |
| Recursive languages | ≝ 🔗 | Turing-machine languages (Mathlib), with halting deciders |
| ⊊ (⊆ 🔗) | ⊊ (⊆ 🔗) | |
| Recursively enumerable languages | ⇔ (⇐ 🔗) | Turing-machine languages (Mathlib) |
Additional results
Closure
Abstract closure predicates (ClosedUnderUnion, ClosedUnderHomomorphism, etc.) are defined 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 (letter-to-letter 🔗) | No | Yes 🔗 | Yes | No | No | Yes |
ε-free (string) homomorphism | Yes 🔗 | No | Yes 🔗 | Yes | Yes | Yes | Yes 🔗 |
| Substitution | Yes 🔗 | No | Yes 🔗 | Yes | Yes | 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 🔗 | No | Yes 🔗 | Yes | Yes | Yes | Yes |
Notes on the table above:
Additional context-free closure results formalized here:
Decidability
Results marked ✓ᶜ use ComputablePred (the strongest form). Results marked ✓ use only Mathlib's Decidable instance (weaker — does not establish computability).
| Language | Membership | Emptiness | Universality | Equivalence |
|---|---|---|---|---|
| Regular | ✓ᶜ 🔗 | ✓ 🔗 | ✓ 🔗 | ✓ 🔗 |
| Deterministic context-free | ✓ | ✓ | ✓ | ✓ |
| Context-free | ✓ᶜ 🔗 | ✓ᶜ 🔗 | ✗ | ✗ |
| Context-sensitive | ✓ 🔗 | ✗ | ✗ | ✗ |
| Recursive | ✓ 🔗 | ✗ | ✗ | ✗ |
| Recursively enumerable | ✗ 🔗 | ✗ 🔗 | ✗ 🔗 | ✗ 🔗 |
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:
- test/LanglibTest/DemoContextFree.lean
- test/LanglibTest/DemoContextSensitive.lean
- test/LanglibTest/DemoUnrestricted.lean
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 large 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!