Nested Term Graphs (Work In Progress)

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.