DOAJ Open Access 2020

A Type System Describing Unboundedness

Paweł Parys

Lihat Sumber DOI

Abstrak

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.

Topik & Kata Kunci

Mathematics

Penulis (1)

Paweł Parys

Format Sitasi

APA MLA BibTeX

Parys, P. (2020). A Type System Describing Unboundedness. https://doi.org/10.23638/DMTCS-22-4-2

Akses Cepat

Lihat di Sumber doi.org/10.23638/DMTCS-22-4-2

Informasi Jurnal

Tahun Terbit: 2020
Sumber Database: DOAJ
DOI: 10.23638/DMTCS-22-4-2
Akses: Open Access ✓