Abstract
We report on work in progress on ‘nested term graphs’ for formalizing higher-order terms (e.g. finite or infinite λ-terms), including those expressing recursion (e.g. terms in the λ-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 intensionally, as tree-like recursive graph specifications that associate nested symbols with usual term graphs, and extensionally, 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.
Original language | English |
---|---|
Title of host publication | Proceedings 8th International Workshop on Computing with Terms and Graphs, Vienna, Austria, July 13, 2014 |
Editors | F. van Raamsdonk, A. Middeldorp |
Publisher | Vienna Summer of Logic |
Pages | 48-65 |
Volume | 2015 |
Edition | 183 |
DOIs | |
Publication status | Published - 2015 |
Event | 8th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2014) - Duration: 13 Jul 2014 → 13 Jul 2014 |
Publication series
Name | Electronic Proceedings in Theoretical Computer Science |
---|---|
Publisher | Open Publishing Association |
ISSN (Print) | 2075-2180 |
Conference
Conference | 8th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2014) |
---|---|
Period | 13/07/14 → 13/07/14 |
Bibliographical note
Proceedings title: Proceedings 8th International Workshop on Computing with Terms and Graphs, Vienna, Austria, July 13, 2014Publisher: Open Publishing Association
Editors: F. van Raamsdonk, A. Middeldorp