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;