2017/01/19 by Paweł Parys, Parys, Paweł
Computer Science · #Algorithms and Data Compression #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #semigroups and automata theory
paper · doi:10.48550/arxiv.1701.05303
openalex publication_date 2017/01/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We present a new approach to the following meta-problem: given a quantitative property of trees, design a type system such that the desired property for the tree generated by an infinitary ground λ-term corresponds to some property of a derivation of a type for this λ-term, in this type system. Our approach is presented in the particular case of the language finiteness problem for nondeterministic higher-order recursion schemes (HORSes): given a nondeterministic HORS, decide whether the set of all finite trees generated by this HORS is finite. We give a type system such that the HORS can generate a tree of an arbitrarily large finite size if and only if in the type system we can obtain derivations that are arbitrarily large, in an appropriate sense; the latter condition can be easily decided.