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;}