循环λ-项的项图表示
Term Graph Representations for Cyclic Lambda-Terms
摘要：
我们研究了各种表示为循环的高阶或一阶项图。我们专注于“高次项图”（高次项图），这是一阶项图赋予了一个良好的范围功能，和他们的表示为“高次项图”，这是普通的一阶项图与范围顶点，满足一定的范围要求。具体来说，我们解决的问题：哪一类的一阶项图承认一个忠实的嵌入？在这个意义上，（i）的同态为基础的共享顺序的？我们系统地研究是否有一些类的ESTA项图有这个属性，我们发现一个特定的类ESTA项图，满足这一标准。该类的术语图由应用程序、抽象、变量和作用域顶点构建，并且具有后两种顶点具有到相应抽象的反向链接的特征。这一结果在理论上和算法上处理了高阶项图的子项共享的概念：我们获得了一个容易实现的方法来获得最大共享形式的高阶项图。此外，我们打开了可能性，拉回性能从一阶项图到双线性项图，性能，如完整的晶格结构的互模拟等价类的共享顺序。
英文摘要：
We study various representations for cyclic lambda-terms as higher-order or as first-order term graphs. We focus on the relation between 'lambda-higher-order term graphs' (lambda-ho-term-graphs), which are first-order term graphs endowed with a well-behaved scope function, and their representations as 'lambda-term-graphs', which are plain first-order term graphs with scope-delimiter vertices that meet certain scoping requirements. Specifically we tackle the question: Which class of first-order term graphs admits a faithful embedding of lambda-ho-term-graphs in the sense that (i) the homomorphism-based sharing-order on lambda-ho-term-graphs is preserved and reflected, and (ii) the image of the embedding corresponds closely to a natural class (of lambda-term-graphs) that is closed under homomorphism? We systematically examine whether a number of classes of lambda-term-graphs have this property, and we find a particular class of lambda-term-graphs that satisfies this criterion. Term graphs of this class are built from application, abstraction, variable, and scope-delimiter vertices, and have the characteristic feature that the latter two kinds of vertices have back-links to the corresponding abstraction. This result puts a handle on the concept of subterm sharing for higher-order term graphs, both theoretically and algorithmically: We obtain an easily implementable method for obtaining the maximally shared form of lambda-ho-term-graphs. Furthermore, we open up the possibility to pull back properties from first-order term graphs to lambda-ho-term-graphs, properties such as the complete lattice structure of bisimulation equivalence classes with respect to the sharing order.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
