超解释的合成：一个综述
Synthesis of sup-interpretations: a survey
摘要：
在本文中，我们调查的复杂性不同的方法，允许程序员合成一个超解释，一个功能提供一个上限的大小计算的输出值的程序。它是一个静态的空间分析工具，不考虑时间消耗。虽然有明显的相关性，但超解释与终止无关，因为它只提供了终止计算的上限。首先，我们从理论上研究了超解释的一些不可判定性。接下来，我们固定长期重写系统作为我们的计算模型，我们表明，一个超解释可以通过使用一个著名的终止技术，多项式的解释。缺点是这种方法只适用于全函数（强规范化程序）。为了克服这个问题，我们还研究超解释通过准解释的概念。准解释也有一个缺点，那就是子项属性。这个属性极大地限制了所考虑的函数的形状。再次，我们克服了这个问题，引入了一个新的概念，主要是基于依赖对方法的解释。我们研究的可判定性和复杂性的超解释综合问题，所有这三个工具的多项式集。最后，我们利用一些以前的工作终止和运行时的复杂性推断超解释。
英文摘要：
In this paper, we survey the complexity of distinct methods that allow the programmer to synthesize a sup-interpretation, a function providing an upper- bound on the size of the output values computed by a program. It consists in a static space analysis tool without consideration of the time consumption. Although clearly related, sup-interpretation is independent from termination since it only provides an upper bound on the terminating computations. First, we study some undecidable properties of sup-interpretations from a theoretical point of view. Next, we fix term rewriting systems as our computational model and we show that a sup-interpretation can be obtained through the use of a well-known termination technique, the polynomial interpretations. The drawback is that such a method only applies to total functions (strongly normalizing programs). To overcome this problem we also study sup-interpretations through the notion of quasi-interpretation. Quasi-interpretations also suffer from a drawback that lies in the subterm property. This property drastically restricts the shape of the considered functions. Again we overcome this problem by introducing a new notion of interpretations mainly based on the dependency pairs method. We study the decidability and complexity of the sup-interpretation synthesis problem for all these three tools over sets of polynomials. Finally, we take benefit of some previous works on termination and runtime complexity to infer sup-interpretations.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
