Type homogeneity is not a restriction for safe recursion schemes
arXiv:1701.02118
Abstract
Knapik et al. introduced the safety restriction which constrains both the types and syntax of the production rules defining a higher-order recursion scheme. This restriction gives rise to an equi-expressivity result between order-n pushdown automata and order-n safe recursion schemes, when such devices are used as tree generators. We show that the typing constraint of safety, called homogeneity, is unnecessary in the sense that imposing the syntactic restriction alone is sufficient to prove the equi-expressivity result for trees.
The result presented in this paper was privately circulated for the first time in 2009 and shared on my personal website but was never published in a journal or conference