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 R and L, 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 R is (constructively) reflective w.r.t. L 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

• Type: Journal
• Year: 2010
• Where: LICS
• Authors: Christopher H. Broadbent, Arnaud Carayol, C.-H. Luke Ong, Olivier Serre
• Keywords: Automated Reasoning, LICS 2010, Node-labelled Infinite Trees, Recursion Schemes, Tree