Slide 8.3: A reduction machine
Slide 8.5: Reduction rules for integer arithmetic expressions (cont.)
Home

Logical Inference Rules

Operational semantics represents computation by means of deductive systems that turn the abstract machine into a system of logical inferences. The semantics use reduction rules to specify how the control reduces the constructs of the language to a value. These reduction rules are given in a mathematical notation similar to logical inference rules, which are written in the following form: 
   premise   
conclusion
That is, the premise, or condition, is written first; then a line is drawn, and the conclusion, or result, is written. This indicates that whenever the premise is true, the conclusion is also true. As an example, we can express the commutative property of addition as the following inference rule: 
   a + b = c   
b + a = c
In logic, such inference rules are used to express the basic rules of propositional and predicate calculus. As an example of an inference rule in logic, the transitive property of implication is given by the following rule: 
   a → b, b → c   
a → c
This says that if a implies b and b implies c, then a implies c. Axiom are inference rules with no premise—they are always true. An example of an axiom is a + 0 = a for integer addition. This can be written as an inference rule with an empty premise: 
   a + 0 = a  
More often, this is written without the horizontal line: 
a + 0 = a