Shape-Preserving Transformations of Higher-Order Recursion Schemes

Higher-order recursion scheme model functional programs in the sense that they describe the recursive definitions of the user-defined functions of a program, without interpreting the built-in functions. Therefore the semantics of a higher-order recursion scheme is the (possibly infinite) tree of executions of a program. As for programming languages several evaluation policies are possible, two of which are OI and IO, roughly corresponding to 'call-by-name' and 'call-by-value'. This thesis focus on verification related problems. The MSO modelchecking problem, i.e. the problem of knowing whether the tree generated by a scheme satisfy an monadic second order logic (MSO) formula, has been solved by Ong in 2006. In 2010 Broadbent Carayol Ong and Serre extended this result by showing that one can transform a scheme such that the nodes in the tree satisfying a given MSO formula are marked, this problem is called the reflection problem. Finally in 2012 Carayol and Serre have solved the selection problem: if the tree of a given scheme satisfies a formula of the form 'There exist a set of node such that...', one can transform the scheme such that a set witnessing the property is marked. These two last results were obtained using collapsible pushdown automata, a class of automata equi-expressive with schemes to generate infinite trees. The drawback of going back and forth between collapsible pushdown automata and schemes is that the resulting scheme is structurally very far from the original one: this is a serious problem when one is interested in doing automated correction of programs or even synthesis. In this thesis, we use a semantics approach to study scheme transformation related problems. Our goal is to give shape-preserving solutions to such problems, i.e. solutions where the output scheme has the same structure as the input one. In this idea, we establish a simulation algorithm that takes a scheme G and an evaluation policy π ∈ {OI, IO} and outputs a scheme G′ such that the value tree of G′ under the policy π≠π is equal to the value tree of G under π. Then we give new proofs of the reflection and selection, that do not involve collapsible pushdown automata, and are again shape preserving.