A cartesian closed fibration of higher-order regular languages
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915755266670592 |
|---|---|
| author | Melliès, Paul-André Moreau, Vincent |
| author_facet | Melliès, Paul-André Moreau, Vincent |
| contents | We explain how to construct in two different ways a cartesian closed fibration of higher-order regular languages in the sense of Salvati. In the first construction, we use fibrational techniques to derive the cartesian closed fibration from the various categories of regular languages of $λ$-terms associated to finite sets of ground states. In the second construction, we take advantage of the recent notion of profinite $λ$-calculus to define the cartesian closed fibration by a change-of-base from the fibration of clopen subsets over the category of Stone spaces, using an elegant idea coming from Hermida. We illustrate the expressive power of the cartesian closed fibration by generalizing the notion of Brzozowski derivative to higher-order regular languages, using an Isbell-like adjunction in the sense of Melliès and Zeilberger. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_18000 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | A cartesian closed fibration of higher-order regular languages Melliès, Paul-André Moreau, Vincent Logic in Computer Science Formal Languages and Automata Theory Category Theory We explain how to construct in two different ways a cartesian closed fibration of higher-order regular languages in the sense of Salvati. In the first construction, we use fibrational techniques to derive the cartesian closed fibration from the various categories of regular languages of $λ$-terms associated to finite sets of ground states. In the second construction, we take advantage of the recent notion of profinite $λ$-calculus to define the cartesian closed fibration by a change-of-base from the fibration of clopen subsets over the category of Stone spaces, using an elegant idea coming from Hermida. We illustrate the expressive power of the cartesian closed fibration by generalizing the notion of Brzozowski derivative to higher-order regular languages, using an Isbell-like adjunction in the sense of Melliès and Zeilberger. |
| title | A cartesian closed fibration of higher-order regular languages |
| topic | Logic in Computer Science Formal Languages and Automata Theory Category Theory |
| url | https://arxiv.org/abs/2601.18000 |