Document Open Access Logo

A Cartesian Closed Fibration of Higher-Order Regular Languages

Authors Paul-André Melliès , Vincent Moreau

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.73.pdf
  • Filesize: 0.91 MB
  • 25 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Regular languages
  • Theory of computation → Tree languages
  • Theory of computation → Denotational semantics
  • Theory of computation → Type theory
  • Theory of computation → Categorical semantics
Keywords
  • automata theory
  • categorical models and logics
  • logics of programs
  • programming language semantics

Metrics

Abstract

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.

Cite As Get BibTex

Paul-André Melliès and Vincent Moreau. A Cartesian Closed Fibration of Higher-Order Regular Languages. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 73:1-73:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.73

Author Details

Paul-André Melliès
  • CNRS, Université Paris Cité, INRIA, France
Vincent Moreau
  • Tallinn University of Technology, Estonia

Funding

  • Melliès, Paul-André: This work has received funding from the European Research Council under the European Union’s Horizon 2020 research and innovation programme (Synergy Project Malinca, ERC Grant Agreement No 670624).
  • Moreau, Vincent: This work has received funding from the Estonian Centre of Excellence in Artificial Intelligence (EXAI), funded by the Estonian Research Council (ETAG).

Acknowledgements

We would like to thank the anonymous reviewers for their feedback, as well as Thomas Colcombet, Mai Gehrke, Sam van Gool, Tito Nguyễn, Daniela Petrisan, Cécilia Pradic, and Sylvain Salvati for interesting discussions on this work.

References

  1. Jiří Adámek, Robert El Bashir, Manuela Sobral, and Jiří Velebil. On functors which are lax epimorphisms. Theory and Applications of Categories, 8(20):509-521, 2001. URL: http://www.tac.mta.ca/tac/volumes/8/n20/8-20abs.html.
  2. Jorge Almeida. Finite Semigroups and Universal Algebra. WORLD SCIENTIFIC, 1995. URL: https://doi.org/10.1142/2481.
  3. Jorge Almeida, Alfredo Costa, Revekka Kyriakoglou, and Dominique Perrin. Profinite Semigroups and Symbolic Dynamics. Springer International Publishing, 2020. URL: https://doi.org/10.1007/978-3-030-55215-2.
  4. Mikołaj Bojańczyk, Bartek Klin, and Julian Salamanca. Monadic Monadic Second Order Logic, pages 701-754. Springer International Publishing, 2023. URL: https://doi.org/10.1007/978-3-031-24117-8_19.
  5. Ivan Di Liberti. Codensity: Isbell duality, pro-objects, compactness and accessibility. Journal of Pure and Applied Algebra, 224(10):106379, 2020. URL: https://doi.org/10.1016/j.jpaa.2020.106379.
  6. Mai Gehrke and Sam van Gool. Topological Duality for Distributive Lattices: Theory and Applications. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2024. Google Scholar
  7. Mai Gehrke, Serge Grigorieff, and Jean-Éric Pin. Duality and equational theory of regular languages. In Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz, editors, Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part II - Track B: Logic, Semantics, and Theory of Programming & Track C: Security and Cryptography Foundations, volume 5126 of Lecture Notes in Computer Science, pages 246-257. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70583-3_21.
  8. Mai Gehrke, Serge Grigorieff, and Jean-Éric Pin. A topological approach to recognition. In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors, Automata, Languages and Programming, 37th International Colloquium, ICALP 2010, Bordeaux, France, July 6-10, 2010, Proceedings, Part II, volume 6199 of Lecture Notes in Computer Science, pages 151-162. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14162-1_13.
  9. Sam van Gool, Paul-André Melliès, and Vincent Moreau. Profinite lambda-terms and parametricity. Electronic Notes in Theoretical Informatics and Computer Science, Volume 3 - Proceedings of MFPS XXXIX , November 2023. URL: https://doi.org/10.46298/entics.12280.
  10. Alexander Grothendieck. Categories Fibrees et Descente, pages 145-194. Springer Berlin Heidelberg, 1971. URL: https://doi.org/10.1007/bfb0058662.
  11. Masahito Hasegawa. Categorical glueing and logical predicates for models of linear logic. Preprint RIMS-1223, Kyoto University, 1999. URL: http://www.kurims.kyoto-u.ac.jp/~hassei/papers/full.pdf.
  12. Masahito Hasegawa. Logical predicates for intuitionistic linear type theories. In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings, volume 1581 of Lecture Notes in Computer Science, pages 198-212. Springer, 1999. URL: https://doi.org/10.1007/3-540-48959-2_15.
  13. Claudio Alberto Hermida. Fibrations, logical predicates and indeterminates. DAIMI Report Series, 22(462), November 1993. URL: https://doi.org/10.7146/dpb.v22i462.6935.
  14. Gerd G. Hillebrand and Paris C. Kanellakis. On the expressive power of simply typed and let-polymorphic lambda calculi. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, pages 253-263. IEEE Computer Society, 1996. URL: https://doi.org/10.1109/LICS.1996.561337.
  15. B. Jacobs. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam, 1999. Google Scholar
  16. Peter T. Johnstone. Sketches of an Elephant A Topos Theory Compendium. Oxford University Press, September 2002. URL: https://doi.org/10.1093/oso/9780198515982.001.0001.
  17. Shin-ya Katsumata. Relating computational effects by ⊤⊤-lifting. Information and Computation, 222:228-246, January 2013. URL: https://doi.org/10.1016/j.ic.2012.10.014.
  18. William Lawvere. Equality in hyperdoctrines and comprehension schema as an adjoint functor. Proceedings of the American Mathematical Society Symposium on Pure Mathematics XVII, 999:1-14, 1970. Google Scholar
  19. Paul-André Melliès. Categorical semantics of linear logic, pages 1-196. Number 27 in Panoramas et Synthèses. Société Mathématique de France, 2009. Google Scholar
  20. Paul-André Melliès and Noam Zeilberger. Functors are type refinement systems. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '15, pages 3-16, New York, NY, USA, 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2676726.2676970.
  21. Paul-André Melliès and Noam Zeilberger. An isbell duality theorem for type refinement systems. Mathematical Structures in Computer Science, 28(6):736-774, 2018. URL: https://doi.org/10.1017/S0960129517000068.
  22. Vincent Moreau. A topological and fibrational approach to higher-order automata. Theses, Université Paris Cité, July 2025. URL: https://theses.hal.science/tel-05428993.
  23. Lê Thành Dũng Nguy~ên. Implicit automata in linear logic and categorical transducer theory. PhD thesis, Université Paris XIII, 2021. URL: https://hal.science/tel-04132636.
  24. Lê Thành Dũng Nguy~ên and Cécilia Pradic. Implicit automata in typed λ-calculi I: aperiodicity in a non-commutative logic. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbrücken, Germany (Virtual Conference), volume 168 of LIPIcs, pages 135:1-135:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.135.
  25. Jean-Éric Pin. Profinite Methods in Automata Theory. In Susanne Albers and Jean-Yves Marion, editors, 26th International Symposium on Theoretical Aspects of Computer Science, volume 3 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31-50, Dagstuhl, Germany, 2009. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.STACS.2009.1856.
  26. Nicholas Pippenger. Regular languages and stone duality. Theory of Computing Systems, 30(2):121-134, April 1997. URL: https://doi.org/10.1007/bf02679444.
  27. Cécilia Pradic and Colin Riba. Lmso: A curry-howard approach to church’s synthesis via linear logic. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’18, pages 849-858. ACM, July 2018. URL: https://doi.org/10.1145/3209108.3209195.
  28. Cécilia Pradic and Colin Riba. A curry-howard approach to church’s synthesis. Logical Methods in Computer Science, Volume 15, Issue 4, December 2019. URL: https://doi.org/10.23638/LMCS-15(4:13)2019.
  29. Cécilia Pradic and Colin Riba. A Dialectica-Like Interpretation of a Linear MSO on Infinite Words, pages 470-487. Springer International Publishing, 2019. URL: https://doi.org/10.1007/978-3-030-17127-8_27.
  30. Colin Riba. Monoidal-closed categories of tree automata. Mathematical Structures in Computer Science, 30(1):62-117, 2020. URL: https://doi.org/10.1017/S0960129519000173.
  31. Sylvain Salvati. Recognizability in the simply typed lambda-calculus. In Hiroakira Ono, Makoto Kanazawa, and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information and Computation, 16th International Workshop, WoLLIC 2009, Tokyo, Japan, June 21-24, 2009. Proceedings, volume 5514 of Lecture Notes in Computer Science, pages 48-60. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02261-6_5.
  32. Richard Statman. Completeness, invariance and lambda-definability. Journal of Symbolic Logic, 47(1):17-26, 1982. URL: https://doi.org/10.2307/2273377.
  33. Richard Statman and Gilles Dowek. On statman’s finite completeness theorem, 2023. URL: https://doi.org/10.48550/arXiv.2309.03602.
  34. Sam van Gool and Jérémie Marquès. On duality and model theory for polyadic spaces. Annals of Pure and Applied Logic, 175(2):103388, February 2024. URL: https://doi.org/10.1016/j.apal.2023.103388.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact