Slide 8.5: Reduction rules for integer arithmetic expressions

Slide 8.4: Logical inference rules
Slide 8.6: Reduction rules for integer arithmetic expressions (cont.)
Home

Reduction Rules for Arithmetic Expressions

We use the notion of inference rules to describe the way the control operates to reduce an expression to its value. There are several styles in current use to how these rules are written:

Structural operational semantics: Structural operational semantics strive to capture the smallest possible changes in configurations. For this reason, they are sometimes called small-step semantics.

Natural semantics: An alternative semantics describe the computation in large steps providing a direct relation between initial and final states. It is therefore called big-step semantics or natural semantics.

Structural operational semantics will be used in the following examples. The abstract syntax for integer arithmetic expressions are as follows:

   E ::= E₁ '+' E₂ | E₁ '–' E₂ | E₁ '*' E₂ | '(' E₁ ')' | N
   N ::= N₁ D | D
   D ::= '0' | '1' | … | '9'

Same as the denotational semantics, the symbols < and > enclosing a nonterminal are removed. For example,

   <N> ::= <N> <D> | <D>  →  N ::= N D | D

Terminal symbols are enclosed by single quotes. For the time being, we can ignore the storage, since this grammar does not include identifiers. We use the following notation:

E, E₁, and so on are used to denote expression that have not yet been reduced to values;

V, V₁, and so on will stand for integer values;

E ⇒ E₁ states that expression E reduces to expression E₁ by some reduction rule.