##
Böhm Trees as Higher-Order Recursive Schemes

### Andrzej Murawski

Higher-order recursive schemes (HORS) are schematic representations of
functional programs. They generate possibly infinite ranked labelled
trees and, in that respect, are known to be equivalent to a restricted
fragment of the lambdaY-calculus, consisting of ground-type terms whose
free variables have types of the form o->...->o (with o as a special case).

In this paper, we show that any lambdaY-term (with no restrictions on
term type or the types of free variables) can actually be represented by
a HORS. That is, for any lambda Y-term M, there exists a HORS generating
a tree that faithfully represents M's Böhm tree. In particular, the HORS
captures higher-order binding information contained in the Böhm tree. An
analogous result holds for finitary PCF.

As a consequence, we can reduce a variety of problems related to the
lambdaY-calculus or finitary PCF to problems concerning higher-order
recursive schemes. For instance, Böhm tree equivalence can be reduced to
the equivalence problem for HORS. Our results also enable MSO
model-checking of Böhm trees.

This is joint work with Pierre Clairambault (University of Cambridge).