Document Open Access Logo

Syntactically and Semantically Regular Languages of λ-Terms Coincide Through Logical Relations

Authors Vincent Moreau , Lê Thành Dũng (Tito) Nguyễn

PDF
Thumbnail PDF

File

LIPIcs.CSL.2024.40.pdf
  • Filesize: 0.96 MB
  • 22 pages

Document Identifiers

Author Details

Vincent Moreau
  • IRIF & Université Paris Cité & Inria Paris, France
Lê Thành Dũng (Tito) Nguyễn
  • Laboratoire de l'informatique du parallélisme (LIP), École normale supérieure de Lyon, France

Funding

  • Nguyễn, Lê Thành Dũng (Tito): Supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR).

Acknowledgements

We would like to thank Amina Doumane, Sam van Gool, Paul-André Melliès and Sylvain Salvati for in-depth discussions that significantly helped us refine our ideas. We are also grateful to Sam and Paul-André for proof-reading drafts of this paper, and to the ReFL discussion group https://www.engboris.fr/refl/ for hosting a reading group on logical relations and normalization by evaluation. The first author would like to thank the Felicissimo family for their support during the writing process of this article.

Cite AsGet BibTex

Vincent Moreau and Lê Thành Dũng (Tito) Nguyễn. Syntactically and Semantically Regular Languages of λ-Terms Coincide Through Logical Relations. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 40:1-40:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CSL.2024.40

Abstract

A fundamental theme in automata theory is regular languages of words and trees, and their many equivalent definitions. Salvati has proposed a generalization to regular languages of simply typed λ-terms, defined using denotational semantics in finite sets. We provide here some evidence for its robustness. First, we give an equivalent syntactic characterization that naturally extends the seminal work of Hillebrand and Kanellakis connecting regular languages of words and syntactic λ-definability. Second, we show that any finitary extensional model of the simply typed λ-calculus, when used in Salvati’s definition, recognizes exactly the same class of languages of λ-terms as the category of finite sets does. The proofs of these two results rely on logical relations and can be seen as instances of a more general construction of a categorical nature, inspired by previous categorical accounts of logical relations using the gluing construction.

Subject Classification

ACM Subject Classification
  • Theory of computation → Denotational semantics
  • Theory of computation → Regular languages
Keywords
  • regular languages
  • simple types
  • denotational semantics
  • logical relations

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Categorical reconstruction of a reduction free normalization proof. In David H. Pitt, David E. Rydeheard, and Peter T. Johnstone, editors, Category Theory and Computer Science, 6th International Conference, CTCS '95, Cambridge, UK, August 7-11, 1995, Proceedings, volume 953 of Lecture Notes in Computer Science, pages 182-199. Springer, 1995. URL: https://doi.org/10.1007/3-540-60164-3_27.
  2. Roberto M. Amadio and Pierre-Louis Curien. Domains and Lambda-Calculi, volume 46 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998. URL: https://doi.org/10.1017/CBO9780511983504.
  3. Robert Atkey. Syntax for free: Representing syntax with binding using parametricity. In Pierre-Louis Curien, editor, Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings, volume 5608 of Lecture Notes in Computer Science, pages 35-49. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02273-9_5.
  4. Mikołaj Bojańczyk. Languages recognised by finite semigroups, and their generalisations to objects such as trees and graphs, with an emphasis on definability in monadic second-order logic. CoRR, abs/2008.11635, 2020. URL: https://arxiv.org/abs/2008.11635.
  5. Mikołaj Bojańczyk, Bartek Klin, and Sławomir Lasota. Automata theory in nominal sets. Logical Methods in Computer Science, 10(3), 2014. URL: https://doi.org/10.2168/LMCS-10(3:4)2014.
  6. Antonio Bucciarelli. Logical relations and lambda theories. In Advances in Theory and Formal Methods of Computing, proceedings of the 3rd Imperial College Workshop, pages 37-48, 1996. Google Scholar
  7. Thomas Ehrhard. The Scott model of linear logic is the extensional collapse of its relational model. Theoretical Computer Science, 424:20-45, 2012. URL: https://doi.org/10.1016/j.tcs.2011.11.027.
  8. Marcelo Fiore. Semantic analysis of normalisation by evaluation for typed lambda calculus. Mathematical Structures in Computer Science, 32(8):1028-1065, 2022. URL: https://doi.org/10.1017/S0960129522000263.
  9. Jean-Yves Girard. The Blind Spot: Lectures on logic. European Mathematical Society, September 2011. URL: https://doi.org/10.4171/088.
  10. Charles Grellois. Semantics of linear logic and higher-order model-checking. PhD thesis, Université Paris 7, April 2016. URL: https://hal.science/tel-01311150.
  11. Pierre A. Grillet. Semigroups. An introduction to the structure theory. Chapman & Hall/CRC Pure and Applied Mathematics. Dekker, 1995. URL: https://doi.org/10.4324/9780203739938.
  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. Gerco van Heerdt, Tobias Kappé, Jurriaan Rot, Matteo Sammartino, and Alexandra Silva. Tree Automata as Algebras: Minimisation and Determinisation. In Markus Roggenbach and Ana Sokolova, editors, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019), volume 139 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1-6:22, Dagstuhl, Germany, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CALCO.2019.6.
  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. Naoki Kobayashi. Model checking higher-order programs. Journal of the ACM, 60(3):20:1-20:62, 2013. URL: https://doi.org/10.1145/2487241.2487246.
  16. Naoki Kobayashi. 10 years of the higher-order model checking project (extended abstract). In Ekaterina Komendantskaya, editor, Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, PPDP 2019, Porto, Portugal, October 7-9, 2019, pages 2:1-2:2. ACM, 2019. URL: https://doi.org/10.1145/3354166.3354167.
  17. Gregory M. Kobele and Sylvain Salvati. The IO and OI hierarchies revisited. Information and Computation, 243:205-221, 2015. URL: https://doi.org/10.1016/j.ic.2014.12.015.
  18. Paul-André Melliès. Categorical Semantics of Linear Logic. In P.-L. Curien, H. Herbelin, J.-L. Krivine, and P.-A. Melliès, editors, Interactive models of computation and program behaviour, volume 27 of Panoramas et Synthèses. Société Mathématique de France, 2009. URL: https://smf.emath.fr/publications/semantique-categorielle-de-la-logique-lineaire.
  19. Paul-André Melliès. Higher-order parity automata. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12, Reykjavik, Iceland, June 2017. IEEE. URL: https://doi.org/10.1109/LICS.2017.8005077.
  20. John C. Mitchell and Andre Scedrov. Notes on sconing and relators. In Egon Börger, Gerhard Jäger, Hans Kleine Büning, Simone Martini, and Michael M. Richter, editors, Computer Science Logic, 6th Workshop, CSL '92, San Miniato, Italy, September 28 - October 2, 1992, Selected Papers, volume 702 of Lecture Notes in Computer Science, pages 352-378. Springer, 1992. URL: https://doi.org/10.1007/3-540-56992-8_21.
  21. 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.
  22. 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.
  23. C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 81-90. IEEE Computer Society, 2006. URL: https://doi.org/10.1109/LICS.2006.38.
  24. C.-H. Luke Ong. Higher-order model checking: An overview. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 1-15. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.9.
  25. Gordon D. Plotkin. Recursion does not always help. In Fairouz Kamareddine, editor, A Century since Principia’s Substitution Bedazzled Haskell Curry. In Honour of Jonathan Seldin’s 80th Anniversary. College Publications, 2023. URL: https://arxiv.org/abs/2206.08413.
  26. Simona Ronchi Della Rocca. Intersection Types and Denotational Semantics: An Extended Abstract (Invited Paper). In Silvia Ghilezan, Herman Geuvers, and Jelena Ivetić, editors, 22nd International Conference on Types for Proofs and Programs (TYPES 2016), volume 97 of Leibniz International Proceedings in Informatics (LIPIcs), pages 2:1-2:7, Dagstuhl, Germany, 2018. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2016.2.
  27. 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.
  28. Sylvain Salvati. Lambda-calculus and formal language theory. Habilitation à diriger des recherches, Université de Bordeaux, 2015. URL: https://hal.science/tel-01253426.
  29. B. Srivathsan and Igor Walukiewicz. An alternate proof of Statman’s finite completeness theorem. Information Processing Letters, 112(14-15):612-616, 2012. URL: https://doi.org/10.1016/j.ipl.2012.04.014.
  30. Richard Statman. Completeness, invariance and lambda-definability. Journal of Symbolic Logic, 47(1):17-26, 1982. URL: https://doi.org/10.2307/2273377.
  31. Richard Statman. On the λ Y calculus. Annals of Pure and Applied Logic, 130(1-3):325-337, 2004. URL: https://doi.org/10.1016/j.apal.2004.04.004.
  32. Richard Statman and Gilles Dowek. On Statman’s finite completeness theorem, 1992. URL: https://arxiv.org/abs/2309.03602.
  33. Kazushige Terui. Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12), pages 323-338, 2012. URL: https://doi.org/10.4230/LIPIcs.RTA.2012.323.
  34. 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.
  35. Igor Walukiewicz. Automata theory and higher-order model-checking. ACM SIGLOG News, 3(4):13-31, 2016. URL: https://doi.org/10.1145/3026744.3026745.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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