Iteration

In Refal Plus, recursion is the principal means of representing loops. In many cases, however, this means is too universal, for which reason Refal Plus provides a special search construct $iter.

Syntactically, a search construct is a path of the form
    S'' $iter S' :: He R

where the sources S'' and S' are assistants, and the rest R a provider (which is essential in cases where S'', S', or R contain right hand sides of the form = Q).

If the hard expression He is empty, it may be omitted along with the keyword ::. If the rest R consists of a single comma, it may also be omitted.

A search construct introduces new local variables (in the same way as a binding S :: He R does). The initial values of these variables are obtained by evaluating the source S''. Then an attempt is made to evaluate the rest R. If the evaluation of R succeeds, the value returned is taken to be the result of the whole construct. Otherwise, if the evaluation of R fails, the local variables are bound to new values (obtained by evaluating the source S' in the old environment associating the local variables with their old values). Then, again, an attempt is made to evaluate the rest R, etc.

Thus, in a sense, the search construct tries to find for the variables in He such values that the evaluation of the rest R succeeds.

The easiest way to explain the exact meaning of the search construct consists in defining it in terms of more elementary constructs, such as bindings and alternatives. Namely, a search S'' $iter S' :: He R is equivalent to the path
    S" :: He, \{ R; S' $iter S' :: He R; }
This path, again, contains a search construct, which, again, may be "unfolded". Thus we get
    S" :: He, \{ R;
         S' :: He, \{ R;
              S' $iter S' :: He R;
    };}
By repeating the unfolding infinitely many times, we can transform the original construct into the infinite path
    S" :: He, \{ R;
         S' :: He, \{ R;
              S' :: He, \{ R;
     ...
     ... };};}

The following example illustrates the use of the search construct.

Let us consider the well-known factorial function, which is usually given the following recursive definition:
$func Fact sN = sFact;

Fact
  {
  0 = 1;
  sN = <Mult sN <Fact <Sub sN 1>>>;
  };

The drawback of the above definition is that the call to the function Mult cannot be evaluated until the evaluation of the internal call to the function Fact has terminated. Thus, the calls to Mult accumulate. However, the function Fact can be given a more "iterative" definition (making use of the auxiliary function FactAux).

$func Fact sN = sFact;
$func FactAux sR sK = sFact;

Fact  sN =
  <FactAux 1 sN>;

FactAux  sR sK =
  {
  sK : 0
    = sR;
    = <FactAux <Mult sR sK> <Sub sK 1>>;
  };
The same can be expressed with the search construct in the following way:
$func Fact sN = sFact;

Fact  sN =
  1 sN
    $iter <Mult sR sK> <Sub sK 1>
      :: sR sK,
  sK : 0,
    = sR;