Operational Semantics
Operational semantics describe the precise rules for the evaluation
of expressions in a given language. The rules make up the description
of an abstract machine which passes
through different states, one rule (or step)
at a time, until the machine halts
and produces a value.
Typically, operational semantics begin by first giving a set of
values, indicating the final results
of evaluation, and a set of identifiers syntactically identifying
the set of evaluable
expressions. The
evaluation rules themselves are given in a style similar to
type rules,
where a rule applies if the
premises above the horizontal line are
true, and the
conclusion indicates how
the state of the abstract machine changes when the rule is applied.
As an example, assume a language of conditional expressions.
An example expression in this language would be:
The values of this language are
true and false.
The expressions in this language
include the values, and the form
if e₀ then e₁ else e₂ end, where
e₀,
e₁ and
e₂ are expressions. There
are clearly multiple ways to evaluate expressions in this language,
but in order to produce an algorithm that will execute on a computer,
the evaluation rules should be:
The operational semantics for the language could be written as
follows:
Expressions are assigned the identifiers
e₀ to
eₙ, so terms of those forms
are assumed to be evaluable expressions when they appear in rules.
The notation e → e' should be
read "e evaluates to e'
in a single step".
The if_true rule states that
if the condition of an if expression
is exactly true, then the expression
evaluates to the expression given in the left branch, in one step.
The if_false rule states that
if the condition of an if expression
is exactly false, then the expression
evaluates to the expression given in the right branch, in one step.
The if_condition rule states that
if the condition of an if expression
is not a value, then the condition is evaluated first.
The example expression given earlier can now be evaluated completely
and deterministically by following the given rules:
The substitution notation
e [x := y] denotes
the expression e where all
occurences (if any) of the variable x
have been replaced with y. This
is used, for example, to describe function evaluation:
The function_eval_0 and
function_eval_1 rules state that
expressions are evaluated from left-to-right when applying
f to a pair of arguments.
The function_eval_2 rule states
that when all of the expressions passed to f
have been reduced to values, the expression as a whole evaluates to
the body of f, called
e, with occurrences of
the arguments x and
y in
e substituted with their
values.