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

Acknowledgements

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

Cite AsGet 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
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