Type homogeneity is not a restriction for safe recursion schemes

TL;DR

This paper demonstrates that the safety restriction in higher-order recursion schemes, specifically the homogeneity type constraint, is unnecessary for establishing their equivalence with order-n pushdown automata in generating trees.

Contribution

It proves that the syntactic safety restriction alone suffices for the equi-expressivity result, removing the need for the type homogeneity constraint.

Findings

Homogeneity is not necessary for safety in recursion schemes.

Syntactic safety restriction alone ensures equivalence with pushdown automata.

The result simplifies the understanding of safe recursion schemes.

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.