Lecture notes on the IF+/ Language: Operational Semantics
Table of Contents
- 1. Revision History
- 2. Introduction
- 3.
IF+/Syntax - 4. Semantic domains
- 5.
IF+/Rewrite (redex) rules - 6. Reduction (small step semantics)
- 7. Semantic Properties
- 8. Examples of simplification resulting in an error
- 9. Errors: Normal forms that do not represent values
- 10. Valuation (Big step) Semantics
- 11. Theorem (Consistency between small-step and valuation semantics)
- 12. Implementations (Reduction Strategies)
- 13. Theorem (Relating reduction, evaluation and implementation)
1 Revision History
- Created.
2 Introduction
We define the language IF+/ by extending the ADDITION
language in two orthogonal directions. First, we extend
semantic (value) domain to include boolean constants. Second,
we include the division operation \(/\) corresponding to division
over numbers. We also include ifte, the ``if then else''
operator, common to many programming languages.
As we will see, the language IF+/ exhibits interesting
semantic behaviour not found in the ADDITION language. For
example, normal forms are no longer values. We encounter the
possibility of errors.
3 IF+/ Syntax
4 Semantic domains
4.1 Theorem (Values are represented by literals)
4.1.1 Statement
If \(v\) is a value, then \(\overline{v}\) is an expression.
4.1.2 Proof
By inspection of the syntax of expressions and the definition of the value domain.
Expressions of the form \(\overline{v}\) are called literals.
5 IF+/ Rewrite (redex) rules
\[\rewritesto \subseteq \id{EXP}\times \id{EXP}\]
\begin{align*} \overline{n_1}+\overline{n_2} \rewritesto \overline{n_1+n_2}\qquad \scriptstyle{PLUS} \\ \\ \\ \overline{n_1}/\overline{n_2} \rewritesto \overline{n_1/n_2}\quad n_2\neq 0\quad\scriptstyle{DIV} \\ \\ \\ {\sf{if}}\ \overline{\true} \ e\ e' \rewritesto e \quad \scriptstyle{IFTRUE}\\ \\ \\ {\sf{if}}\ \overline{\false} \ e\ e' \rewritesto e' \quad \scriptstyle{IFFALSE} \end{align*}Note how the rewrite rules for \({\sf if}\) capture the intended meaning of an d\({\sf if}\) expression.
6 Reduction (small step semantics)
\[\reducesto \subseteq \id{EXP}\times \id{EXP}\]
\begin{align*} \frac{e \hookrightarrow e'}{e\reducesto e'}\quad \scriptstyle{REWRITE} \\ \\ \\ % \frac{e_1\rightarrow e_1'}{e_1+e_2 \reducesto e_1'+e_2}\quad \scriptstyle{P\_LEFT} \\ \\ \\ % \frac{e_2\reducesto e_2'}{e_1+e_2 \reducesto e_1+e'_2}\quad \scriptstyle{P\_RIGHT} \\ \\ \\ % \frac{e_1\rightarrow e_1'}{e_1/e_2 \reducesto e_1'/e_2}\quad \scriptstyle{D\_LEFT} \\ \\ \\ % \frac{e_2\reducesto e_2'}{e_1/e_2 \reducesto e_1/e'_2}\quad \scriptstyle{D\_RIGHT} \\ \\ \\ % \frac{e_1 \reducesto e'_1}{{\sf if}\ e_1\ e_2\ e_3 \reducesto {\sf if}\ e'_1\ e_2\ e_3}\quad \scriptstyle{IF\_TEST} \\ \\ \\ % \end{align*}Note the reduction rules for \({\sf if}\). These capture our intuition that in an {\sf if} expression, the then or else expressions are reduced only after the test expression is reduced to either the literal \(\true\) or \(\false\), respectively.
7 Semantic Properties
7.1 Theorem (Literals are irreducible)
7.1.1 Statement
If \(v\) is a value then \(\overline{v}\) is irreducible.
7.1.2 Proof
By inspection of the reduction rules. \(\overline{v}\) does not match the right hand side of the consequent of any of the rules.
Note that the converse is not true: there are irreducible expressions that are not values, e.g., \(5/0\). (Can you give other examples?) Contrast this with the ADDITION langugae, where every irreducible expression represented a value.
7.2 Theorem (Termination)
7.2.1 Statement
\(\reducesto\) is terminating.
7.2.2 Proof
Exercise.
7.3 Theorem (Local Confluence)
7.3.1 Statement
If \(e\reducesto e_1\) and \(e\reducesto e_2\), there there exists \(e_3\) such that \(e_1\simplifiesto e_3\) and \(e_2 \simplifiesto e_3\).
7.3.2 Proof
Exercise.
7.4 Theorem (Confluence)
7.4.1 Statement
\(\reducesto\) is confluent.
7.4.2 Proof
Follows from termination and local confluence.
7.5 Theorem (Convergence)
7.5.1 Statement
Every expression simplifies to a unique normal form.
7.5.2 Proof
Confluence and termination imply convergence.
8 Examples of simplification resulting in an error
9 Errors: Normal forms that do not represent values
A normal form that is not a literal is an error. Note that an expression may terminate at a literal representing a value, or terminate at an error.
9.1 Type Errors versus /0 Errors
A closer examination of the errors shows that errors arise when operators receive arguments that do not match their specification. For example:
- \({\sf if}\) expects its test argument to be boolean, but it is not (TYPE ERROR)
- \(+\) expects both its arguments to be numbers, but one or more of the arguments are not numbers. (TYPE ERROR)
- \(/\) expects both its arguments to be numbers, but one or more of its arguments are not numbers. (TYPE ERROR)
- \(/\) expects its second argument (denominator) to be non-zero, but it is in fact zero. (CHECKED ERROR: /0)
Of these, the first three error are called type errors. The last kind of error (4) is what called a checked error.
To a certain extent, the classification of errors into type errors versus checked errors is arbitrary. In our semantics, both actually occur at runtime (simplification) and checks are runtime necessary to flag them. The classification, however, serves a useful purpose when, with some compromises on the semantics, we can eliminate checking for the type errors completely at runtime. How this is done and what compromises this entails is material for the chapter on type systems (coming soon to a classroom near you.)
9.2 Theorem (Progress)
9.2.1 Statement
Every expression
- is reducible, or
- is is irreducible, in which case it is a
- literal,
- type error, or
- /0 error
9.2.2 Proof
Exercise.
10 Valuation (Big step) Semantics
10.1 Evaluation Rules
\[\evaluatesto \subseteq \id{EXP}\times \id{VAL}\]
\begin{align*} \frac{}{\overline{v}\evaluatesto v}\quad \scriptstyle{VAL} \\ \\ \\ \frac{{e_1\evaluatesto n_1}\qquad {e_2\evaluatesto n_2}}{e_1+e_2 \evaluatesto n_1+n_2}\quad \scriptstyle{PLUS} \\ \\ \\ \frac{{e_1\evaluatesto n_1}\qquad {e_2\evaluatesto n_2}\quad n_2\neq 0}{e_1/e_2 \evaluatesto n_1/n_2}\quad \scriptstyle{DIV} \\ \\ \\ \frac{{e_1\evaluatesto {\sf true}}\qquad{e_2\evaluatesto v_2}}{{\sf if}\ e_1\ e_2 \ e_3 \evaluatesto v_2}\quad \scriptstyle{IF\_TRUE} \\ \\ \\ \frac{{e_1\evaluatesto {\sf false}}\qquad{e_3\evaluatesto v_3}}{{\sf if}\ e_1\ e_2 \ e_3 \evaluatesto v_3}\quad \scriptstyle{IF\_FALSE} \\ \\ \\ \end{align*}11 Theorem (Consistency between small-step and valuation semantics)
11.0.1 Statement
\[e\simplifiesto \overline{v}\] iff \[e\evaluatesto v\]
11.0.2 Proof
Left as an exercise.
12 Implementations (Reduction Strategies)
Exercise.
13 Theorem (Relating reduction, evaluation and implementation)
13.0.1 Statement
\(e\simplifiesto \overline{v}\) \(\qquad\) iff \(\qquad\) \(e\lsimplifiesto \overline{v}\) \(\qquad\) iff \(\qquad\) \(e\evaluatesto v\).
13.0.2 Proof
Exercise.