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 proof file (possibly to 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.

Grammar side	Relation	Automaton side
Regular languages (Left-regular ⇔🔗 Right-regular)	⇔ 🔗	DFA languages (Mathlib)
⊊ 🔗		⊊ 🔗
LR(k) grammar 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 (DLBA ⊆ 🔗 LBA, LBA ⊆? DLBA)
⊊ 🔗		⊊ 🔗 (⊆ RE 🔗)
Recursive languages	≝ 🔗	Turing-machine languages (Mathlib), with halting deciders
⊊ 🔗		⊊ 🔗
Recursively enumerable languages	⇔ 🔗	Turing-machine languages (Mathlib)

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	Yes	No 🔗	Yes 🔗

Additional DCFL results:

Union with a regular language

Additional CFL results:

Additional CSL results:

Terminal bijections

Decidability

Each column refers to the corresponding uniform computability predicate (ComputableMembership, ComputableEmptiness, ComputableUniversality, ComputableEquivalence) defined in 🔗.

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:

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!