Recursion schemes and logical reflection

Let ℛ be a class of generators of node-labelled infinite trees, and ℒ be a logical language for describing correctness properties of these trees. Given R ∈ R and φ ∈ ℒ, we say that Rφ is a φ-reflection of R just if (i) R and Rφ generate the same underlying tree, and (ii) suppose a node u of the tree [R] generated by R has label f, then the label of the node u of [Rφ] is f if u in [R] satisfies φ; it is f otherwise. Thus if [R] is the computation tree of a program R, we may regard Rφ as a transform of R that can internally observe its behaviour against a specification φ. We say that ℛ is (constructively) reflective w.r.t. ℒ just if there is an algorithm that transforms a given pair (R,φ) to Rφ. In this paper, we prove that higher-order recursion schemes are reflective w.r.t. both modal μ-calculus and monadic second order (MSO) logic. To obtain this result, we give the first characterisation of the winning regions of parity games over the transition graphs of collapsible pushdown automata (CPDA): they are regular sets defined by a new class of automata. (Order-n recursion schemes are equi-expressive with order-n CPDA for generating trees.) As a corollary, we show that these schemes are closed under the operation of MSO-interpretation followed by tree unfolding à la Caucal.