Closure Properties of General Grammars -- Formally Verified
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910767331147776 |
|---|---|
| author | Dvorak, Martin Blanchette, Jasmin |
| author_facet | Dvorak, Martin Blanchette, Jasmin |
| contents | We formalized general (i.e., type-0) grammars using the Lean 3 proof assistant. We defined basic notions of rewrite rules and of words derived by a grammar, and used grammars to show closure of the class of type-0 languages under four operations: union, reversal, concatenation, and the Kleene star. The literature mostly focuses on Turing machine arguments, which are possibly more difficult to formalize. For the Kleene star, we could not follow the literature and came up with our own grammar-based construction. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2302_06420 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Closure Properties of General Grammars -- Formally Verified Dvorak, Martin Blanchette, Jasmin Formal Languages and Automata Theory We formalized general (i.e., type-0) grammars using the Lean 3 proof assistant. We defined basic notions of rewrite rules and of words derived by a grammar, and used grammars to show closure of the class of type-0 languages under four operations: union, reversal, concatenation, and the Kleene star. The literature mostly focuses on Turing machine arguments, which are possibly more difficult to formalize. For the Kleene star, we could not follow the literature and came up with our own grammar-based construction. |
| title | Closure Properties of General Grammars -- Formally Verified |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2302.06420 |