Böhm Trees as Higher-Order Recursive Schemes

Authors Pierre Clairambault, Andrzej S. Murawski

Thumbnail PDF


  • Filesize: 0.61 MB
  • 12 pages

Document Identifiers

Author Details

Pierre Clairambault
Andrzej S. Murawski

Cite AsGet BibTex

Pierre Clairambault and Andrzej S. Murawski. Böhm Trees as Higher-Order Recursive Schemes. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 91-102, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


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 lambda-Y-calculus consisting of ground-type terms whose free variables have types of the form o -> ... -> o (with o being a special case). In this paper, we show that any lambda-Y-term (with no restrictions on term type or the types of free variables) can actually be represented by a HORS. More precisely, for any lambda-Y-term M, there exists a HORS generating a tree that faithfully represents M's (eta-long) 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 lambda-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, despite the general undecidability of the problem.
  • Lambda calculus
  • Böhm trees
  • Recursion Schemes


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail