2017/01/09 by William Blum, Blum, William
Computer Science · #Formal Methods in Verification #Logic, programming, and type systems #Software Engineering Research #cs.LO
paper · pdf · doi:10.48550/arxiv.1701.02118
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
arxiv created 2017/01/09 · arxiv updated 2017/01/10
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.