Result Expressions

A result expression consists of symbols, parentheses, variables and function calls. The evaluation of a result expression produces either a ground expression, a failure, or an error.

Syntax

ResultExpression =
     { ResultTerm | NamedExpression }.
ResultTerm =
     StaticSymbol | Variable |
     "(" ResultExpression ")" |
     FunctionCall.
FunctionCall =
     "<" FunctionName CallArgument ">".
CallArgument =
     ResultExpression.

If two different variables appear in the same result expression, they must have different indices.

Notation

Henceforth, result expressions will be denoted by Re, result terms by Rt, variables by V, e-variables by Ve, and function names by Fname.

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