Résumé | Higher-order recursive schemes (HORS) are schematic representations of functional programs. They generate possibly infinite ranked labelled trees and, viewed as tree generators, are equivalent to λY-terms of ground type in which free variables can only have types of the form o → ... → o (with o as a special case). In this talk, I will show that any λY-term (with no restrictions on term type or the types of free variables) has an equivalent presentation as a HORS. That is, for any λY-term, there exists a HORS generating a tree that faithfully represents the Böhm tree of the λY-term. In particular, the HORS encodes higher-order binding information contained in the Böhm tree. The result reduces the problem of Böhm tree equivalence for the λY-calculus to the equivalence problem for HORS and enables MSO model-checking of Böhm trees. We also show how to adapt the methodology to finitary PCF (over finite datatypes). This is joint work with Andrzej Murawski. |