Incremental evaluation

 

Consider a needed narrowing sequence . Since each step is scheduled by (where is a definitional tree for ), and it usually changes only small parts of , it is obvious that, if , then the needed narrowing step for (i.e., the computation of ) might wastefully examine some of the symbols already considered in the preceding step and take almost the same decisions. In order to avoid this wasting, we look for an incremental definition of which is able to locally resume the search from for some . Intuitively, whenever and , we can be sure that the symbols occurring at the position immediately above p have not been modified. On the other hand, the term may or may not be operation-rooted. If , then should be further narrowed until a constructor-rooted term or a variable is obtained. If , then the next needed narrowing step is determined by the definitional tree of , where q<p is the position of the defined symbol occurring at the position immediately above p.

 

-Proof. us first consider the case when (note that, since we impose , it follows that is not empty; i.e., q does exist.). Then, the computation of has reached a branch node and there is an operation-rooted subterm at the inductive position o. Thus the computation of first reaches the same branch node and then proceeds by checking whether is a constructor-rooted term or a variable, since it cannot be an operation-rooted term unless q=p, which contradicts the original assumption. In both cases, a subtree for is selected before resuming the computation. If is a branch subtree, then the computed position p' will be below q; otherwise (that is, is a rule subtree), p'=q.

Now consider the case when q=p. Then is operation-rooted and this position needs to be further narrowed in order to compute a constructor-rooted term. Then, the computed position is trivially q or below q.

 

Since each step in a needed narrowing sequence is performed using , where is a definitional tree for , Corollary 4.2 ensures that, whenever is operation-rooted, then . Thus, we take , where and is a definitional tree for . If is constructor-rooted or a variable, then it is necessary to resume the evaluation somewhere above . Proposition 4.1 allows us to come back to by taking the (`most defined') definitional subtree of the definitional tree of which has been used in the computation of immediately before obtaining . Thus, we let , where .

Thus, we define a data structure which contains the information needed to perform the needed narrowing steps incrementally. Given a term t, we let denote a list of pairs where p is a position and is an incremental definitional tree. The incremental needed narrowing strategy is denoted by . It takes as arguments a term t and an auxiliary list which plays the role of the definitional tree in the original strategy . Given an operation-rooted term t and a list with , we compute , where p is the position pointing to the subterm of t to be narrowed, R is the rule to be applied, is the computed substitution, and is a list containing the information which allows us to proceed with the subsequent evaluation steps incrementally. Formally,

The following notations are helpful. Given a position p and a list of pairs position/incremental definitional tree, we define:

We also use the standard operator ` ' for concatenating lists. The following auxiliary result is used below.

 

-Proof. , by definition of .

The following proposition states that is able to compute the same needed narrowing step than starting from a given term and an initial list of incremental information.

 

-Proof. from the definition of and .

Now, we have to ensure that the defined function symbols occurring at positions which are above (or at) a previously narrowed position are obtained by the strategy and thus considered for the subsequent narrowing steps.

 

-Proof. noetherian induction on pairs (strictly) ordered by iff or and , i.e., is a subtree of [AEH94]. Here, is the number of defined function symbols in t.

• (Base) Since , then t is operation-rooted. Hence, the base case consists in considering those pairs such that t is operation-rooted and does not contain any other defined function symbol, and is a rule node . By hypothesis, , hence let . Thus, only the first case for applies, i.e., and we have either
  1. is not operation-rooted, hence . Then, from the definition of , we have that .
  2. is operation-rooted, hence . Then, from the definition of , , where is an incremental definitional tree for .
  On the other hand, if , then from the definition of , we have that is not operation-rooted and hence . If is not empty, then , and thus is operation-rooted, i.e., .
• (Induction) We consider the different cases for separately.
  1. If is a rule node, we reason as in the base case.
  2. If and is a variable x, then , where for some and . Thus, . Since and , by induction hypothesis we have that, for , iff . From the definition of , the conclusion follows.
  3. If and is constructor-rooted, the conclusion follows by a similar reasoning to case 2.
  4. If and is operation-rooted, then (where is a definitional tree for and p=o.p'), i.e., . Since , by the induction hypothesis if and only if , for . Since , by Lemma 4.3 the conclusion follows.

The following theorem shows that the needed narrowing steps performed by the incremental strategy and the computation steps carried out by the original needed narrowing strategy are equivalent.

 

-Proof. prove it by induction on the length of the derivation.

i = 1. This case is trivial, since by Proposition 4.4 it amounts to a call to .

i > 1. Let for some definitional tree . By the induction hypothesis, we have that if and only if . Since , by Proposition 4.5, q points to a defined symbol of which is above or at the position . By the ordering between the positions recorded in (see Lemma 4.3), q is the position of the defined symbol immediately above or at the position . By Proposition 4.1, , where . Then, by Proposition 4.4, . Now, since all positions in the first component of the position/incremental definitional tree lists correspond to operation-rooted subterms, by using Lemma 4.3 it is immediate that if .

Thus, .

Although we only provide in this paper the definition of in terms of incremental definitional trees, the function can be easily redefined to perform with standard definitional trees, similarly to . We make free with this in the following section, where different implementations of needed narrowing are compared.