Minimal and optimal computations of recursive programs
Minimal and optimal computations of recursive programs
复制标题
递归程序的最小和最优计算
DOI：
10.1145/512950.512971
复制
发表时间：
1977
期刊：
影响因子：
--
通讯作者：
J. Lévy
中科院分区：
文献类型：
--
作者：
G. Berry;J. Lévy
过程调用机制主要在没有赋值的递归程序框架中进行研究，因为它们的操作和指称语义简单（参见Scott [16]，Nivat [14]，Vuillemin [17]）。根据操作语义，过程调用充当文本重写;“计算规则”在每个计算步骤中选择要重写的未知函数的出现。如果计算规则计算的值是指称语义给出的值，则该计算规则被称为正确的。Vuillemin [17，18]，Montangero-Pacini-Turini [13]，Downey-Sethi [7]研究了计算规则的正确性和效率。主要结果是众所周知的：最内层的求值（按值调用）是不正确的，并行最外层或完全替换是正确的。Vuillemin [17，18]给出了一个规则正确的充分条件（安全性），后来由Downey-Sethi [7]扩展为一个充分必要条件（安全性）。Vuillemin还研究了按名称呼叫的延迟规则的具体实现;他证明了其在合理实现成本方面的最优性，前提是解释满足顺序性条件。这个结果实际上是双重的：顺序性允许消除无用的步骤，并且通过在术语实现中使用共享机制来实现最优性。所有这些研究的基础是下面的定理（Vuillemin [17，18]）：只要满足程序的某些限制条件，从给定项可导的项集在导序下是格。我们的目标是延长这些结果，有以下三个原因：第一，虽然每一个程序可以转换，以配合Vuillemin的条件，转换可能会影响成本的计算：一个更直接的证明可以调查。第二，直接推广到<$演算并不简单，因为<$项绝对不构成格。第三，符号（或Herbrand）解释[5]不是Vuillemin意义上的序列，也没有已知的最优性结果。我们的观点将是纯粹的句法：我们在导子中重构格性质。我们研究最小计算（即有限或无限导子）的符号解释，并将它们转化为最优的。最后，我们描述的解释，类似的结果适用。在[10]中对ë-演算进行了扩展。术语的格属性通常会被打破：两个非常不同的推导可能会通过语法上的意外导致同一个术语，这会使两个先验不同的术语崩溃。在第一节中，我们通过引入导子上的等价和前序来处理这个事实。我们给出了这些关系的三个特征。对于主要的一个，我们通过定义导子的导子的残差来扩展经典的残差概念[4]。我们证明，派生类形成一个格。在第二节中，我们研究了Vuillemin用标号定义的“简单导子”（这里称为完全导子）。我们在通常的形式主义中给出了它们的两个特征。第三节，致力于极小性和最优性的结果。我们对无限导子和有限导子进行排序，构造了由程序确定的无限树的每一个句法近似的最小计算。相关的完整推导是最佳的Vuillemin的成本。因此，只要解释满足句法条件，就可以直接扩展到解释。[2，6，11，17]中考虑的所有序列解释类都满足这个条件。我们用来构造最优计算的“计算规则”一般来说效率很低，但在顺序解释中可以简化为通常的延迟规则。
Procedure call mechanisms have mainly been studied in the framework of recursive programs without assignments, for the simplicity of their operational and denotational semantics (See Scott [16], Nivat [14], Vuillemin [17]). According to operational semantics, procedure calls act as textual rewritings ; "computation rules" select at each computation step the occurrences of unknown functions to be rewritten. A computation rule is called correct if the value it computes is the one given by the denotational semantics. Correctness and efficiency of computation rules have been studied in Vuillemin [17,18], Montangero-Pacini-Turini [13], Downey-Sethi [7]. The main results are well-known: innermost evaluation (call by value) is not correct, parallel outermost or full substitution are correct. Vuillemin [17,18] gives a sufficient condition for a rule to be correct, (safety), later extended by Downey-Sethi [7] into a necessary and sufficient one (security). Vuillemin also studies particular implementation of call-by-name, the delay rule ; he shows its optimality with respect to a reasonable implementation cost, provided interpretations satisfy a sequentiality condition. This result is in fact twofold : sequentiality allows elimination of useless steps, and optimality follows by using sharing mechanisms in term implementation. The basis of all these studies is the following theorem (Vuillemin [17,18]) : provided some restrictive conditions on programs are satisfied, the set of terms derivable from a given term is a lattice under the derivation ordering. Our aim is to extend these results, for the three following reasons : first, though every program can be transformed to match Vuillemin's conditions, the transformations may affect the costs of computations : a more direct proof can be investigated. Second, a direct generalization to the ë-calculus is not straightforward, since ë-terms definitely do not form lattices. Third, the symbolic (or Herbrand) interpretation [5] is not sequential in the sense of Vuillemin, and no optimality result is known for it. Our point of view will be purely syntactic : we reconstruct the lattice property in derivations. We study minimal computations (i.e. finite or infinite derivations)in the symbolic interpretation, and transform them into optimal ones. Eventually, we characterize interpretations to which similar results apply. Extension towards the ë-calculus is done in [10]. The lattice property of terms breaks down in general : two very different derivations may lead to the same term by syntactical accidents, which collapse two a priori different terms. In section I, we take care of this fact by introducing an equivalence and a preorder on derivations. We give three characterizations of these relations. For the main one, we extend the classical notion of residuals [4] by defining residuals of derivations by derivations. We show that derivation classes form a lattice. In section II, we study the "simple derivations" defined by Vuillemin with use of labels (named here complete derivations). We give two characterizations of them in the usual formalism. Section III, is devoted to minimality and optimality results. Ordering infinite derivations as well as finite one, we construct least computations of every syntactic approximation of the infinite tree determined by the program. The associated complete derivation are optimal with respect to Vuillemin's cost. Extension to interpretations is then straightforward, as soon as they satisfy a syntactic condition. All classes of sequential interpretations considered in [2,6,11,17] do satisfy this condition. The "computation rule" we use for constructing the optimal computations is very inefficient in general, but reduces to the usual delay rules in sequential interpretations.