A cartesian closed fibration of higher-order regular languages

Prelegent(ci)

Vincent Moreau

Afiliacja

Tallinn University of Technology

Język referatu

angielski

Termin

4 listopada 2026 14:15

Pokój

p. 5440

Tytuł w języku polskim

A cartesian closed fibration of higher-order regular languages

Seminarium

Seminarium „Teoria automatów”

Higher-order regular language, as introduced by Salvati, form a conservative extension of regular languages of finite words and ranked trees to the simply typed λ-calculus. In this work, we investigate the new closure properties enabled by this extension, and we establish that higher-order regular languages are stable under finite products, exponentials, and inverse image by all λ-terms.

These fundamental stability properties of higher-order regular languages amount to a structure of a cartesian closed fibration, which we construct in two different ways. 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 due to 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. Finally, we examine the case of stability of higher-regular regular languages under direct image of λ-terms and its relation with monadic second order logic.

This is joint work with Paul-André Melliès.