More exactly, each path appearing in a function definition can be assigned a non-negative
integer k, the level of the path. If we move forward along a path, the level
increases by 1 each time we pass over \?, and decreases by
1 each time we pass over \!. Thus, each cut
\! unambiguously corresponds to its "pair" fence \?.
Now, to give this requirement a more exact formulation, we introduce the following notation.
Let k be a non-negative integer, and Q a path. The judgment
k |- Q means that the path Q can be assigned the level
k.
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, let Palt be a pattern alternative. Then the judgment k |-
Palt means that the pattern alternative Palt can be assigned the
level k.
Now we can formulate the restrictions imposed on the use of cuts in the function definitions.
Let the definition of a function Fname be Fname Palt.
Then there must be satisfied 0 |- Palt.
The relations k |- Q and k |- Palt are defined by the
following inference rules.
0 |- S 0 |- S
k |- R k |- R
--------- ---------------
k |- S R k |- S :: He R
0 |- S''
0 |- S' 0 |- S
k |- R k |- R
------------------------- -------------
k |- S'' $iter S' :: He R k |- S : P R
0 |- S
k |- Q k |- R k+1 |- Q
--------- ----------- ----------
k |- , Q k |- # S R k |- \? Q
k |- Q 0 |- Q
------------ k |- $fail ---------
k+1 |- \! Q k |- = Q
0 |- Q
0 |- Q k |- Palt
-------------- ------------------------
k |- $error Q k |- $trap Q $with Palt
k |- Qj for all j=1,...,n
---------------------------
k |- \{Q1; ... Qn;}
0 |- S
k |- Palt
-------------- k |- Re
k |- S : Palt
k |- Rj for all j=1,...,n
---------------------------
k |- \{P1 R1; ... Pn Rn;}