License:
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2013.91
URN: urn:nbn:de:0030-drops-43644
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4364/
Clairambault, Pierre ;
Murawski, Andrzej S.
Böhm Trees as Higher-Order Recursive Schemes
Abstract
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.
BibTeX - Entry
@InProceedings{clairambault_et_al:LIPIcs:2013:4364,
author = {Pierre Clairambault and Andrzej S. Murawski},
title = {{B{\"o}hm Trees as Higher-Order Recursive Schemes}},
booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)},
pages = {91--102},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-64-4},
ISSN = {1868-8969},
year = {2013},
volume = {24},
editor = {Anil Seth and Nisheeth K. Vishnoi},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2013/4364},
URN = {urn:nbn:de:0030-drops-43644},
doi = {10.4230/LIPIcs.FSTTCS.2013.91},
annote = {Keywords: Lambda calculus, B{\"o}hm trees, Recursion Schemes}
}
Keywords: |
|
Lambda calculus, Böhm trees, Recursion Schemes |
Collection: |
|
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013) |
Issue Date: |
|
2013 |
Date of publication: |
|
10.12.2013 |