A Type System Describing Unboundedness
| Autor: | Paweł Parys |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
simultaneous-unboundedness problem
higher-order recursion schemes intersection types reflection [info.info-fl]computer science [cs]/formal languages and automata theory [cs.fl] [info.info-lo]computer science [cs]/logic in computer science [cs.lo] [info.info-cc]computer science [cs]/computational complexity [cs.cc] Mathematics QA1-939 |
| Zdroj: | Discrete Mathematics & Theoretical Computer Science, Vol vol. 22 no. 4, Iss Automata, Logic and Semantics (2020) |
| Druh dokumentu: | article |
| ISSN: | 1365-8050 |
| DOI: | 10.23638/DMTCS-22-4-2 |
| Popis: | We consider nondeterministic higher-order recursion schemes as recognizers of languages of finite words or finite trees. We propose a type system that allows to solve the simultaneous-unboundedness problem (SUP) for schemes, which asks, given a set of letters A and a scheme G, whether it is the case that for every number n the scheme accepts a word (a tree) in which every letter from A appears at least n times. Using this type system we prove that SUP is (m-1)-EXPTIME-complete for word-recognizing schemes of order m, and m-EXPTIME-complete for tree-recognizing schemes of order m. Moreover, we establish the reflection property for SUP: out of an input scheme G one can create its enhanced version that recognizes the same language but is aware of the answer to SUP. |
| Databáze: | Directory of Open Access Journals |
| Externí odkaz: |
|