嵌套术语图(工作正在进行中)
Nested Term Graphs (Work In Progress)
摘要:
我们报告正在进行的工作“嵌套项图”的形式化高阶项(例如有限或无限的递归项),包括那些表达递归(例如在递归演算与letrec的项)。其思想是通过术语图的嵌套结构来表示高阶术语的嵌套范围结构。基于被划分为原子和嵌套函数符号的签名,我们定义嵌套的术语图都在功能表示,作为树状递归图规范,关联嵌套符号与通常的术语图,并在结构表示,丰富的术语图结构。这些定义诱导嵌套项图之间的互模拟的相应概念。我们的主要结果表明,嵌套项图可以忠实地实现一阶项图。关键词:高阶项图,上下文无关文法,循环循环项,高阶重写系统
英文摘要:
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
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。