Nested Term Graphs

C.A. Grabmayer, V. van Oostrom

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

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 languageEnglish
Title of host publicationProceedings 8th International Workshop on Computing with Terms and Graphs, Vienna, Austria, July 13, 2014
EditorsF. van Raamsdonk, A. Middeldorp
PublisherVienna Summer of Logic
Pages48-65
Volume2015
Edition183
DOIs
Publication statusPublished - 2015
Event8th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2014) -
Duration: 13 Jul 201413 Jul 2014

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
ISSN (Print)2075-2180

Conference

Conference8th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2014)
Period13/07/1413/07/14

Bibliographical note

Proceedings title: Proceedings 8th International Workshop on Computing with Terms and Graphs, Vienna, Austria, July 13, 2014
Publisher: Open Publishing Association
Editors: F. van Raamsdonk, A. Middeldorp

Fingerprint

Dive into the research topics of 'Nested Term Graphs'. Together they form a unique fingerprint.

Cite this