Document Open Access Logo

On the Expressivity of Linear Recursion Schemes

Authors Pierre Clairambault, Andrzej S. Murawski

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2019.50.pdf
  • Filesize: 0.67 MB
  • 14 pages

Document Identifiers

Author Details

Pierre Clairambault
  • Univ Lyon, EnsL, UCBL, CNRS, LIP, F-69342, LYON Cedex 07, France
Andrzej S. Murawski
  • Department of Computer Science, University of Oxford, UK

Funding

  • Clairambault, Pierre: Supported by ANR RAPIDO (ANR-14-CE25-0007) and 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).
  • Murawski, Andrzej S.: Supported by a Royal Society Leverhulme Trust Senior Research Fellowship (LT170023).

Acknowledgements

We would like to thank Sylvain Salvati for consultations on formal languages.

Cite As Get BibTex

Pierre Clairambault and Andrzej S. Murawski. On the Expressivity of Linear Recursion Schemes. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 50:1-50:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.MFCS.2019.50

Abstract

We investigate the expressive power of higher-order recursion schemes (HORS) restricted to linear types. Two formalisms are considered: multiplicative additive HORS (MAHORS), which feature both linear function types and products, and multiplicative HORS (MHORS), based on linear function types only.
For MAHORS, we establish an equi-expressivity result with a variant of tree-stack automata. Consequently, we can show that MAHORS are strictly more expressive than first-order HORS, that they are incomparable with second-order HORS, and that the associated branch languages lie at the third level of the collapsible pushdown hierarchy.
In the multiplicative case, we show that MHORS are equivalent to a special kind of pushdown automata. It follows that any MHORS can be translated to an equivalent first-order MHORS in polynomial time. Further, we show that MHORS generate regular trees and can be translated to equivalent order-0 HORS in exponential time. Consequently, MHORS turn out to have the same expressive power as 0-HORS but they can be exponentially more concise.
Our results are obtained through a combination of techniques from game semantics, the geometry of interaction and automata theory.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program semantics
Keywords
  • higher-order recursion schemes
  • linear logic
  • game semantics
  • geometry of interaction

Metrics

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

References

  1. Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full Abstraction for PCF. Inf. Comput., 163(2):409-470, 2000. URL: https://doi.org/10.1006/inco.2000.2930.
  2. Klaus Aehlig, Jolie G. de Miranda, and C.-H. Luke Ong. Safety Is not a Restriction at Level 2 for String Languages. In Proceedings of FOSSACS, volume 3441 of Lecture Notes in Computer Science, pages 490-504. Springer, 2005. Google Scholar
  3. Patrick Baillot. Approches dynamiques en sémantique de la logique linéaire: jeux et géométrie de l'interaction. PhD thesis, Aix-Marseille 2, 1999. Google Scholar
  4. Ahmed Bouajjani, Javier Esparza, and Oded Maler. Reachability Analysis of Pushdown Automata: Application to Model-Checking. In Proceedings of CONCUR, volume 1243 of Lecture Notes in Computer Science, pages 135-150. Springer, 1997. Google Scholar
  5. Pierre Clairambault, Charles Grellois, and Andrzej S. Murawski. Linearity in higher-order recursion schemes. PACMPL, 2(POPL):39:1-39:29, 2018. Google Scholar
  6. Vincent Danos and Laurent Regnier. Reversible, Irreversible and Optimal lambda-Machines. Theor. Comput. Sci., 227(1-2):79-97, 1999. Google Scholar
  7. Tobias Denkinger. An Automata Characterisation for Multiple Context-Free Languages. In Proceedings of DLT, volume 9840 of Lecture Notes in Computer Science, pages 138-150. Springer, 2016. Google Scholar
  8. Joost Engelfriet and Sven Skyum. Copying Theorems. Inf. Process. Lett., 4(6):157-161, 1976. Google Scholar
  9. Javier Esparza, David Hansel, Peter Rossmanith, and Stefan Schwoon. Efficient Algorithms for Model Checking Pushdown Systems. In Proceedings of CAV, volume 1855 of Lecture Notes in Computer Science, pages 232-247. Springer, 2000. Google Scholar
  10. Jean-Yves Girard. Linear Logic. Theoretical Computer Science, 50:1-102, 1987. Google Scholar
  11. Jean-Yves Girard. Geometry of Interaction 1: Interpretation of System F. Studies in Logic and the Foundations of Mathematics, 127:221-260, 1989. Google Scholar
  12. Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, and Olivier Serre. Collapsible Pushdown Automata and Recursion Schemes. ACM Trans. Comput. Log., 18(3):25:1-25:42, 2017. Google Scholar
  13. Naohiko Hoshino, Koko Muroya, and Ichiro Hasuo. Memoryful geometry of interaction: from coalgebraic components to algebraic effects. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 52:1-52:10, 2014. URL: https://doi.org/10.1145/2603088.2603124.
  14. Martin Hyland. Game semantics. Semantics and logics of computation, 14:131, 1997. Google Scholar
  15. Makoto Kanazawa. Second-Order Abstract Categorial Grammars as Hyperedge Replacement Grammars. Journal of Logic, Language and Information, 19(2):137-161, 2010. Google Scholar
  16. Makoto Kanazawa and Sylvain Salvati. The Copying Power of Well-Nested Multiple Context-Free Grammars. In Proceedings of LATA, volume 6031 of Lecture Notes in Computer Science, pages 344-355. Springer, 2010. Google Scholar
  17. Naoki Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In Proceedings of POPL, pages 416-428, 2009. Google Scholar
  18. Olivier Laurent. A Token Machine for Full Geometry of Interaction. In Proceedings of TLCA, pages 283-297, 2001. URL: https://doi.org/10.1007/3-540-45413-6_23.
  19. Sylvain Salvati. Encoding second order string ACG with deterministic tree walking transducers. In Proceedings of FG, pages 143-156. CSLI Publications, 2006. Google Scholar
  20. Sylvain Salvati. MIX is a 2-MCFL and the word problem in Z^2 is captured by the IO and the OI hierarchies. J. Comput. Syst. Sci., 81(7):1252-1277, 2015. Google Scholar
  21. Hiroyuki Seki, Takashi Matsumura, Mamoru Fujii, and Tadao Kasami. On Multiple Context-Free Grammars. Theor. Comput. Sci., 88(2):191-229, 1991. Google Scholar
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 About DROPS Imprint Privacy Contact