Nested Term Graphs (Work In Progress)

Clemens Grabmayer
(VU University Amsterdam)
Vincent van Oostrom
(Utrecht University)

We report on work in progress on 'nested term graphs' for formalizing higher-order terms (e.g. finite or infinite lambda-terms), including those expressing recursion (e.g. terms in the lambda-calculus with letrec). The idea is to represent the nested scope structure of a higher-order term by a nested structure of term graphs.

Based on a signature that is partitioned into atomic and nested function symbols, we define nested term graphs both in a functional representation, as tree-like recursive graph specifications that associate nested symbols with usual term graphs, and in a structural representation, as enriched term graph structures. These definitions induce corresponding notions of bisimulation between nested term graphs. Our main result states that nested term graphs can be implemented faithfully by first-order term graphs.

keywords: higher-order term graphs, context-free grammars, cyclic lambda-terms, higher-order rewrite systems

In Aart Middeldorp and Femke van Raamsdonk: Proceedings 8th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2014), Vienna, Austria, July 13, 2014, Electronic Proceedings in Theoretical Computer Science 183, pp. 48–65.
Published: 26th May 2015.

ArXived at: https://dx.doi.org/10.4204/EPTCS.183.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org