On the expressivity of linear recursion schemes
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....
| Main Authors: | , |
|---|---|
| Format: | Conference item |
| Published: |
Schloss Dagstuhl
2019
|
| _version_ | 1826259662077427712 |
|---|---|
| author | Clairambault, P Murawski, A |
| author_facet | Clairambault, P Murawski, A |
| author_sort | Clairambault, P |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-06T18:53:22Z |
| format | Conference item |
| id | oxford-uuid:11001b5f-786b-434b-99fa-1a19949477ec |
| institution | University of Oxford |
| last_indexed | 2024-03-06T18:53:22Z |
| publishDate | 2019 |
| publisher | Schloss Dagstuhl |
| record_format | dspace |
| spelling | oxford-uuid:11001b5f-786b-434b-99fa-1a19949477ec2022-03-26T09:59:47ZOn the expressivity of linear recursion schemesConference itemhttp://purl.org/coar/resource_type/c_5794uuid:11001b5f-786b-434b-99fa-1a19949477ecSymplectic Elements at OxfordSchloss Dagstuhl2019Clairambault, PMurawski, AWe 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. |
| spellingShingle | Clairambault, P Murawski, A On the expressivity of linear recursion schemes |
| title | On the expressivity of linear recursion schemes |
| title_full | On the expressivity of linear recursion schemes |
| title_fullStr | On the expressivity of linear recursion schemes |
| title_full_unstemmed | On the expressivity of linear recursion schemes |
| title_short | On the expressivity of linear recursion schemes |
| title_sort | on the expressivity of linear recursion schemes |
| work_keys_str_mv | AT clairambaultp ontheexpressivityoflinearrecursionschemes AT murawskia ontheexpressivityoflinearrecursionschemes |