Natural Semantics Specifications

The method that is be used to describe the execution of Refal Plus programs is known as Natural Semantics or Structural Operational Semantics.

The name Natural Semantics [Plotkin1983], [Apt1983] is due to the similarity of this description technique to Gentzen's Natural Deduction in mathematical logic. When this technique is applied, the semantics of a language is considered to be an unordered set of judgments about programs and their fragments.

          Env,St' |- E => X,St''

Informally, such a judgment may be interpreted in the following way: if the evaluation of E starts in the environment E and global state St', it may result in producing the value X and the global state St''.

The symbol |- (which may be pronounced "implies" or "entails") indicates the dependency of E's evaluation on the current environment Env and the global state St'.

Thus, to define a language semantics, we have to describe a set of (true) judgments about programs and their fragments.

A Natural Semantics definition is an unordered collection of inference rules, which enables true judgments to be derived from other true judgments.

A rule has basically two parts, a numerator and a denominator. The numerator of a rule is an unordered collection of formulae, the premises of the rule, whereas the denominator is always a single formula, the conclusion. A rule that contains no premise on the numerator is called an axiom, in which case the horizontal line may be omitted.

Besides, a rule may contain additional conditions, which impose certain restrictions on the applicability of the rule. The restrictions are placed slightly to the right of the rule or under the rule.

For example, suppose that the language to be described has the construct if E then E' else E'', whose meaning may be informally defined as follows.

Evaluate E. If the value of E is true, evaluate E' and assume the value obtained to be the result of the whole construct. Otherwise, if the value of E is false, evaluate E'' and assume the value obtained to be the result of the whole construct.

A drawback of the above description is that there is no explicit information about the environment in which the evaluation of E, E', and E'' takes place. Thus, the description may be reformulated as follows.

If the result of evaluating E in the environment Env is true, and the result of evaluating E' in the environment Env is X, then X is the result of evaluating if E then E' else E'' in the environment Env.

If the result of evaluating E in the environment Env is false, and the result of evaluating E'' in the environment Env is X, then X is the result of evaluating if E then E' else E'' in the environment Env.

     Env,St |- E => true,St'
     Env,St'|- E' => X,St''
     -----------------------------------------
     Env,St |- if E then E' else E'' => X,St''


     Env,St |- E => false,St'
     Env,St'|- E'' => X,St''
     -----------------------------------------
     Env,St |- if E then E' else E'' => X,St''

Take notice of the fact that, in contrast to the informal semantics definition, the formal one provides a precise description of the way in which the global state is modified when the program is executed.