The name Natural Semantics
For example, suppose the language to be described deals with expressions containing
variables, and the evaluation of the expressions may cause side effects (which may be due to
the input/output operations). Then, the language description may involve the judgments of the
form
Informally, such a judgment may be interpreted in the following way: if the evaluation of
The symbol
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
Evaluate
A drawback of the above description is that there is no explicit information about the
environment in which the evaluation of
If the result of evaluating
If the result of evaluating
This verbose definition may be given a more concise and comprehensible formulation by means
of two inference rules:
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.