Evaluation
The evaluation of a source S : \{Snt1; ... Sntn;}
always produces the same result as the evaluation of the path S : Ve, \{Ve :
Snt1; ... Ve : Sntn;}, provided that Ve
is an e-variable that does not appear in the program in other places.
A source S : {Snt1; ... Sntn;} is equivalent to the
source S : \{Snt1; ... Sntn; e $error(Fname "Unexpected
fail");}, where Fname is the name of the function in which the
construct appears.
S : {Snt1; ... Sntn;} =>=>
S : \{Snt1; ... Sntn;
e $error(Fname "Unexpected fail");}
Fname is the name of the function in which
the construct appears.
Env,0,St |- S => Ge,St'
Env,m,St'|- \{Ge : Snt1; ... Ge : Sntn;} => X,St''
--------------------------------------------------
Env,m,St |- S : \{Snt1; ... Sntn;} => X,St''
Env,0,St |- S => $fail(k),St'
--------------------------------------------------
Env,m,St |- S : \{Snt1; ... Sntn;} => $fail(0),St'
Env,0,St |- S => $error(Ge),St'
----------------------------------------------------
Env,m,St |- S : \{Snt1; ... Sntn;} => $error(Ge),St'