2026-09-30T04:53:56Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4364 2026-09-29T23:30:21Z ddc:004 open_access

Böhm Trees as Higher-Order Recursive Schemes Clairambault, Pierre Murawski, Andrzej S. Lambda calculus Böhm trees Recursion 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 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Pierre Clairambault and Andrzej S. Murawski 2013 Is Part Of LIPIcs, Volume 24, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2013.91 urn:nbn:de:0030-drops-43644 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2013.91 eng https://creativecommons.org/licenses/by/3.0/legalcode