A variable appearing in a result expression must have been already defined. A variable gets defined, when it appears in a pattern or in a hard expression. If several different variables get defined at the same place, their indices must be different.
To give these restrictions a more exact formulation, we introduce the following notation.
vars[X] denotes the set of variables appearing in the construct X.
{} denotes the empty set.
v1+v2 denotes the union of the sets v1 and v2.
v1++v2 denotes the variable set v1 extended with the variable set v2. To put it more exactly, v1++v2 contains all the variables from v2, as well as all variables from v1 whose indices are different from the indices of the variables contained in v2. For example, {sX, sY} ++ {eY, eZ} = {sX, eY, eZ} .
A judgment v |- Q means that all variables in v have different indices, and all variables whose values are needed for the evaluation of the path Q belong to v.
Rests, sources, and result expressions may be regarded as particular cases of paths, for which reason the above notation is applicable to them as well as to paths.
Similarly, a judgment v |- Palt means that all variables in v have different indices, and all variables whose values are needed for the evaluation of the pattern alternative Palt belong to v.
Now we can formulate the restrictions imposed on the use of variables in the function definitions.
Let the definition of a function Fname be Fname Palt. Then there must be satisfied {} |- Palt.
The relations v |- Q and v |- Palt are defined by the following inference rules.
v |- S v |- S
v |- R v++vars[He] |- R
---------- -----------------
v |- S R v |- S :: He R
v |- S''
v++vars[He] |- S' v |- S
v++vars[He] |- R v+vars[P] |- R
------------------------- ---------------
v |- S'' $iter S' :: He R v |- S : P R
v |- S
v |- Q v |- R v |- Q
--------- ----------- ----------
v |- , Q v |- # S R v |- \? Q
v |- Q v |- Q
---------- v |- $fail ---------
v |- \! Q v |- = Q
v |- Q
v |- Q v |- Palt
-------------- ------------------------
v |- $error Q v |- $trap Q $with Palt
v |- Qj for all j=1,...,n
---------------------------
v |- \{Q1; ... Qn;}
v |- S
v |- Palt
--------------
v |- S : Palt
all variables in v have different indices
all variables in vars[Re] belong to v
-----------------------------------------
v |- Re
v+vars[Pj] |- Rj for all j=1,...,n
------------------------------------
v |- \{P1 R1; ... Pn Rn;}