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/
Go to the corresponding LIPIcs Volume Portal

Clairambault, Pierre ; Murawski, Andrzej S.

Böhm Trees as Higher-Order Recursive Schemes

pdf-format:
5.pdf (0.6 MB)

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

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI