Recursion Schemes and Logical Reflection

Let R be a class of generators of node-labelled infinite trees, and L be a logical language for describing correctness properties of these trees. Given R is an element of R and phi is an element of L, we say that R-phi is a phi-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) under bar if u in [[R]] satisfies phi; it is f otherwise. Thus if [[R]] is the computation tree of a program R, we may regard R-phi as a transform of R that can internally observe its behaviour against a specification phi. We say that R is (constructively) reflective w.r.t. L just if there is an algorithm that transforms a given pair (R, phi) to R-phi. In this paper, we prove that higher-order recursion schemes are reflective w.r.t. both modal mu-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 a la Caucal.