Evaluation of Result Expressions
A result expression Re may be evaluated in an environment
Env, on condition that Env provides values for all
variables appearing in Re.
If the evaluation of Re terminates, it results in producing either a
ground expression Ge, a failure $fail(0), or an error
$error(Ge), where Ge is an error message.
Evaluating a function call may result in the global program state being changed (for
example, if it involves input/output or some manipulations with objects). Hence, if a result
expression contains function calls, evaluating the expression may also result in the global
state being changed.
A judgment Env,St |- Re => X,St' means that the result of
evaluating the result expression Re in the environment Env
is X, and if the evaluation starts in the global state St,
it terminates in the global state St'.
A result expression Re is evaluated from left to right, the variables
being replaced with their values, and the function calls being executed.
The evaluation of a function call <Fname Re> begins by
evaluating the result expression Re. If a ground expression
Ge is returned, the function Fname is applied to
Ge.
A judgment St |- <Fname Ge> => X,St' means that the
result of applying the function Fname to the ground expression
Ge is X, and if the evaluation starts in the global state
St, it terminates in the global state St'.
Env,St |- => ,St
Env,St |- Re => Ge',St'
Env,St'|- Rt => Ge",St"
------------------------------
Env,St |- Re Rt => Ge' Ge",St"
Env,St |- Re => Ge',St'
Env,St'|- Rt => $fail(0),St"
-------------------------------
Env,St |- Re Rt => $fail(0),St"
Env,St |- Re => Ge',St'
Env,St'|- Rt => $error(Ge"),St"
----------------------------------
Env,St |- Re Rt => $error(Ge"),St"
Env,St |- Re => $fail(0),St'
-------------------------------
Env,St |- Re Rt => $fail(0),St'
Env,St |- Re => $error(Ge'),St'
----------------------------------
Env,St |- Re Rt => $error(Ge'),St'
Env,St |- Gs => Gs,St
Env,St |- V => Ge,St
where Ge=Env(V).
Env,St |- Re => Ge,St'
--------------------------
Env,St |- (Re) => (Ge),St'
Env,St |- Re => $fail(0),St'
------------------------------
Env,St |- (Re) => $fail(0),St'
Env,St |- Re => $error(Ge),St'
--------------------------------
Env,St |- (Re) => $error(Ge),St'
Env,St |- Re => Ge,St'
St' |- <Fname Ge> => X,St"
-----------------------------
Env,St |- <Fname Re> => X,St"
Env,St |- Re => $fail(0),St'
------------------------------------
Env,St |- <Fname Re> => $fail(0),St'
Env,St |- Re => $error(Ge),St'
--------------------------------------
Env,St |- <Fname Re> => $error(Ge),St'
Examples
Here are examples of result expressions:
(A B) C D
t.Head e.Tail
While t.Condition Do t.Statement
<Mult sN <Factorial <Sub sN 1>>
The following result expressions are result terms:
(A B)
t.Head
<Mult sN <Factorial <Sub sN 1>>
Let Env1 = {sM = 2, sN = 3, eA = A B C, tB = (D E F)},
Add be the name of the function that adds integers, and
Mult be the name of the function that multiplies integers. Thus, the
judgments
St |- <Add 3 100> => 103, St
St |- <Mult 2 103> => 206, St
hold for any global state St, because the functions Add
and Mult do not change the global state.
Then we have
Env1,St |- eA (eA tB) tB =>
A B C (A B C (D E F)) (D E F), St
Env1,St |- <Mult sM <Add sN 100>> => 206, St