Document Open Access Logo

Implicit Automata in Typed λ-Calculi I: Aperiodicity in a Non-Commutative Logic

Authors Lê Thành Dũng Nguyễn , Pierre Pradic

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2020.135.pdf
  • Filesize: 0.59 MB
  • 20 pages

Document Identifiers

Author Details

Lê Thành Dũng Nguyễn
  • Laboratoire d'informatique de Paris Nord, Villetaneuse, France
  • Laboratoire Cogitamus (http://www.cogitamus.fr/indexen.html)
Pierre Pradic
  • Department of Computer Science, University of Oxford, UK

Acknowledgements

The initial trigger for this line of work was twofold: the serendipitous rediscovery of Hillebrand and Kanellakis’s theorem by Damiano Mazza, Thomas Seiller and the first author, and Mikołaj Bojańczyk’s suggestion to the second author to look into connections between transducers and linear logic. Célia Borlido proposed looking at star-free languages at the Topology, Algebra and Categories in Logic 2019 summer school. During its long period of gestation, this work benefited from discussions with many other people: Pierre Clairambault, Amina Doumane, Marie Fortin, Jérémy Ledent, Paolo Pistone, Lorenzo Tortora de Falco, Noam Zeilberger and others that we may have forgotten to mention. We also thank the anonymous reviewers for their constructive feedback, especially for their highly relevant pointers to the literature.

Cite AsGet BibTex

Lê Thành Dũng Nguyễn and Pierre Pradic. Implicit Automata in Typed λ-Calculi I: Aperiodicity in a Non-Commutative Logic. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 135:1-135:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ICALP.2020.135

Abstract

We give a characterization of star-free languages in a λ-calculus with support for non-commutative affine types (in the sense of linear logic), via the algebraic characterization of the former using aperiodic monoids. When the type system is made commutative, we show that we get regular languages instead. A key ingredient in our approach – that it shares with higher-order model checking – is the use of Church encodings for inputs and outputs. Our result is, to our knowledge, the first use of non-commutativity in implicit computational complexity.

Subject Classification

ACM Subject Classification
  • Theory of computation → Algebraic language theory
  • Theory of computation → Linear logic
Keywords
  • Church encodings
  • ordered linear types
  • star-free languages

Metrics

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

Related Versions

References

  1. Samson Abramsky. Temperley–Lieb Algebra: From Knot Theory to Logic and Computation via Quantum Mechanics. In Goong Chen, Louis Kauffman, and Samuel Lomonaco, editors, Mathematics of Quantum Computation and Quantum Technology, volume 20074453, pages 515-558. Chapman and Hall/CRC, September 2007. URL: https://doi.org/10.1201/9781584889007.ch15.
  2. Klaus Aehlig. A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata. Logical Methods in Computer Science, 3(3), July 2007. URL: https://doi.org/10.2168/LMCS-3(3:1)2007.
  3. Rajeev Alur and Loris D'Antoni. Streaming Tree Transducers. Journal of the ACM, 64(5):1-55, August 2017. URL: https://doi.org/10.1145/3092842.
  4. Rajeev Alur and P. Madhusudan. Adding nesting structure to words. Journal of the ACM, 56(3):16:1-16:43, 2009. URL: https://doi.org/10.1145/1516512.1516518.
  5. Rajeev Alur and Pavol Černý. Expressiveness of streaming string transducers. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), pages 1-12, 2010. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2010.1.
  6. Jean-Marc Andreoli, Gabriele Pulcini, and Paul Ruet. Permutative logic. In C.-H. Luke Ong, editor, Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings, volume 3634 of Lecture Notes in Computer Science, pages 184-199. Springer, 2005. URL: https://doi.org/10.1007/11538363_14.
  7. Andrew Barber. Dual Intuitionistic Linear Logic. Technical report ECS-LFCS-96-347, LFCS, University of Edinburgh, 1996. URL: http://www.lfcs.inf.ed.ac.uk/reports/96/ECS-LFCS-96-347/.
  8. Mikołaj Bojańczyk. The simplest transducer models and their Krohn-Rhodes decompositions. https://www.mimuw.edu.pl/~bojan/slides/transducer-course/krohn-rhodes.html. Slides of a lecture given at FSTTCS '19, accessed on 11-02-2020. URL: https://www.mimuw.edu.pl/~bojan/slides/transducer-course/krohn-rhodes.html.
  9. Mikołaj Bojańczyk. Automata column: Some Open Problems in Automata and Logic. ACM SIGLOG News, 1(2):3-12, October 2014. URL: https://doi.org/10.1145/2677161.2677163.
  10. Mikołaj Bojańczyk. Polyregular Functions. CoRR, abs/1810.08760, October 2018. URL: http://arxiv.org/abs/1810.08760.
  11. Mikołaj Bojańczyk, Sandra Kiefer, and Nathan Lhote. String-to-String Interpretations With Polynomial-Size Output. In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019), volume 132 of Leibniz International Proceedings in Informatics (LIPIcs), pages 106:1-106:14. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.106.
  12. Corrado Böhm and Alessandro Berarducci. Automatic synthesis of typed λ-programs on term algebras. Theoretical Computer Science, 39:135-154, January 1985. URL: https://doi.org/10.1016/0304-3975(85)90135-5.
  13. Henry DeYoung and Frank Pfenning. Substructural proofs as automata. In Atsushi Igarashi, editor, Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, volume 10017 of Lecture Notes in Computer Science, pages 3-22, 2016. URL: https://doi.org/10.1007/978-3-319-47958-3_1.
  14. Joost Engelfriet and Hendrik Jan Hoogeboom. MSO definable string transductions and two-way finite-state transducers. ACM Transactions on Computational Logic, 2(2):216-254, April 2001. URL: https://doi.org/10.1145/371316.371512.
  15. Emmanuel Filiot and Pierre-Alain Reynier. Transducers, Logic and Algebra for Functions of Finite Words. ACM SIGLOG News, 3(3):4-19, August 2016. URL: https://doi.org/10.1145/2984450.2984453.
  16. Neil Ghani and Alexander Kurz. Higher dimensional trees, algebraically. In Till Mossakowski, Ugo Montanari, and Magne Haveraaen, editors, Algebra and Coalgebra in Computer Science, Second International Conference, CALCO 2007, Bergen, Norway, August 20-24, 2007, Proceedings, volume 4624 of Lecture Notes in Computer Science, pages 226-241. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73859-6_16.
  17. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, January 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  18. Jean-Yves Girard. Towards a geometry of interaction. In J. W. Gray and A. Scedrov, editors, Categories in Computer Science and Logic, volume 92 of Contemporary Mathematics, pages 69-108. American Mathematical Society, Providence, RI, 1989. Proceedings of a Summer Research Conference held June 14-20, 1987. URL: https://doi.org/10.1090/conm/092/1003197.
  19. Jean-Yves Girard. Light Linear Logic. Information and Computation, 143(2):175-204, June 1998. URL: https://doi.org/10.1006/inco.1998.2700.
  20. Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. Bounded linear logic: a modular approach to polynomial-time computability. Theoretical Computer Science, 97(1):1-66, April 1992. URL: https://doi.org/10.1016/0304-3975(92)90386-T.
  21. Charles Grellois. Semantics of linear logic and higher-order model-checking. PhD thesis, Université Paris 7, April 2016. URL: https://tel.archives-ouvertes.fr/tel-01311150/.
  22. Alessio Guglielmi. A system of interaction and structure. ACM Transactions on Computational Logic, 8(1), January 2007. URL: https://doi.org/10.1145/1182613.1182614.
  23. Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, and Olivier Serre. Collapsible Pushdown Automata and Recursion Schemes. ACM Transactions on Computational Logic, 18(3):25:1-25:42, August 2017. URL: https://doi.org/10.1145/3091122.
  24. Gerd G. Hillebrand and Paris C. Kanellakis. On the Expressive Power of Simply Typed and Let-Polymorphic Lambda Calculi. In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, pages 253-263. IEEE Computer Society, 1996. URL: https://doi.org/10.1109/LICS.1996.561337.
  25. Naoki Kobayashi. Model Checking Higher-Order Programs. Journal of the ACM, 60(3):1-62, June 2013. URL: https://doi.org/10.1145/2487241.2487246.
  26. Koichi Kodama, Kohei Suenaga, and Naoki Kobayashi. Translation of tree-processing programs into stream-processing programs based on ordered linear type. Journal of Functional Programming, 18(3):333-371, 2008. URL: https://doi.org/10.1017/S0956796807006570.
  27. Kenneth Krohn and John Rhodes. Algebraic theory of machines. I. Prime decomposition theorem for finite semigroups and machines. Transactions of the American Mathematical Society, 116:450-464, 1965. URL: https://doi.org/10.1090/S0002-9947-1965-0188316-1.
  28. Denis Kuperberg, Laureline Pinault, and Damien Pous. Cyclic Proofs and Jumping Automata. In Arkadev Chattopadhyay and Paul Gastin, editors, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019), volume 150 of Leibniz International Proceedings in Informatics (LIPIcs), pages 45:1-45:14. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2019.45.
  29. Joachim Lambek. The mathematics of sentence structure. American Mathematical Monthly, 65(3):154-170, 1958. Google Scholar
  30. Olivier Laurent. Polynomial time in untyped elementary linear logic. Theoretical Computer Science, 813:117-142, April 2020. URL: https://doi.org/10.1016/j.tcs.2019.10.002.
  31. Daniel Leivant. Reasoning about functional programs and complexity classes associated with type disciplines. In 24th Annual Symposium on Foundations of Computer Science (FOCS 1983), pages 460-469, Tucson, AZ, USA, November 1983. URL: https://doi.org/10.1109/SFCS.1983.50.
  32. Harry G. Mairson. A simple proof of a theorem of Statman. Theoretical Computer Science, 103(2):387-394, September 1992. URL: https://doi.org/10.1016/0304-3975(92)90020-G.
  33. Damiano Mazza. Polyadic Approximations in Logic and Computation. Habilitation à diriger des recherches, Université Paris 13, November 2017. URL: https://lipn.fr/~mazza/papers/Habilitation.pdf.
  34. 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.
  35. Paul-André Melliès. Ribbon Tensorial Logic. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science - LICS '18, pages 689-698, Oxford, United Kingdom, 2018. ACM Press. URL: https://doi.org/10.1145/3209108.3209129.
  36. Anca Muscholl and Gabriele Puppis. The Many Facets of String Transducers. In Rolf Niedermeier and Christophe Paul, editors, 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019), volume 126 of Leibniz International Proceedings in Informatics (LIPIcs), pages 2:1-2:21. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.STACS.2019.2.
  37. Lê Thành Dũng Nguyễn and Pierre Pradic. Implicit automata in typed λ-calculi I: aperiodicity in a non-commutative logic, 2020. Full version of this article. URL: https://hal.archives-ouvertes.fr/hal-02476219.
  38. C.-H. Luke Ong. On Model-Checking Trees Generated by Higher-Order Recursion Schemes. In 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06), pages 81-90, Seattle, WA, USA, 2006. IEEE. URL: https://doi.org/10.1109/LICS.2006.38.
  39. Jeff Polakow and Frank Pfenning. Natural deduction for intuitionistic non-communicative linear logic. 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 295-309. Springer, 1999. URL: https://doi.org/10.1007/3-540-48959-2_21.
  40. Jeff Polakow and Frank Pfenning. Relating Natural Deduction and Sequent Calculus for Intuitionistic Non-Commutative Linear Logic. Electronic Notes in Theoretical Computer Science, 20:449-466, January 1999. URL: https://doi.org/10.1016/S1571-0661(04)80088-4.
  41. Christian Retoré. Pomset logic: A non-commutative extension of classical linear logic. In Philippe de Groote, editor, Typed Lambda Calculi and Applications, Third International Conference on Typed Lambda Calculi and Applications, TLCA '97, Nancy, France, April 2-4, 1997, Proceedings, volume 1210 of Lecture Notes in Computer Science, pages 300-318. Springer, 1997. URL: https://doi.org/10.1007/3-540-62688-3_43.
  42. John C. Reynolds. The discoveries of continuations. LISP and Symbolic Computation, 6(3):233-247, November 1993. URL: https://doi.org/10.1007/BF01019459.
  43. James Rogers. Syntactic Structures as Multi-dimensional Trees. Research on Language and Computation, 1(3):265-305, September 2003. URL: https://doi.org/10.1023/A:1024695608419.
  44. Jacques Sakarovitch. Elements of Automata Theory. Cambridge University Press, 2009. Translated by Reuben Thomas. URL: https://doi.org/10.1017/CBO9781139195218.
  45. 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.
  46. Thomas Seiller. Interaction Graphs: Non-Deterministic Automata. ACM Transactions on Computational Logic, 19(3):21:1-21:24, August 2018. URL: https://doi.org/10.1145/3226594.
  47. Howard Straubing. First-order logic and aperiodic languages: a revisionist history. ACM SIGLOG News, 5(3):4-20, 2018. URL: https://doi.org/10.1145/3242953.3242956.
  48. 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.
  49. Igor Walukiewicz. LambdaY-calculus with priorities. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785674.
  50. David N. Yetter. Quantales and (noncommutative) linear logic. The Journal of Symbolic Logic, 55(1):41-64, March 1990. URL: https://doi.org/10.2307/2274953.
  51. Noam Zeilberger and Alain Giorgetti. A correspondence between rooted planar maps and normal planar lambda terms. Logical Methods in Computer Science, 11(3), September 2015. URL: https://doi.org/10.2168/LMCS-11(3:22)2015.
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