Böhm Trees as Higher-Order Recursive Schemes

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 λ Y -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 λ Y -term (with no restrictions on term type or the types of free variables) can actually be represented by a HORS. That is, for any λ 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 λ Y -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.

Authors

• Andrzej Murawski

Keywords

No keywords are indexed for this paper.