Operational Semantics

1. While Language

The While programming language is composed of three syntactic categories:

Also, ranges over the variable identifiers, and ranges over the natural numbers. Brackets are used for disambiguation.

We use operators like and instead of and to avoid confusion. For example and are mathematically equal, but and are not syntactically equal.

We also define a smaller expression language for expressions without variables, .

An operational symantic for will tell us how to evaluate an expression to get a result. For our language, this can be done in two ways: big step and small step.

Inference rules describe term execution. They have two forms, (i.e. if then ) or (i.e. always holds). We sometimes write them in the form:

1.1 Big Step Semantics

Big Step Semantics take the form of a relation , where means that the expression evaluates to the number . It can be seen as a final answer relation. Some basic inference rules are:

For example, the derivation tree of is shown below. The derivation tree requires at its leaves.

also has some notable properties:

• Determinacy: .
• Totality: .

1.2 Small Step Semantics

Sometimes, it is desirable to be more explicit about exactly how programs are evaluated. We define a relation where means that the expression can be reduced to the expression in one step. This can be seen as a step-by-step relation. We can now define more inference rules:

These rules tell us to follow these steps:

1. First evaluate the left hand argument.
2. When you get a number, evaluate the right hand argument.
3. When you get another number, add them using the rule.

Note that the order of evaluation is fixed by these semantics. So here, .

From , we can define the reflexive transitive closure : holds iff either or there is a finite sequence . For our semantics, we say that is the final answer of if .

An expression is in normal form (irreducible) if .

is deterministic, confluent, weakly normalizing, strongly normalizing and has a unique normal form. For any rewrite relation , we can define:

• is in normal form if
• is deterministic if .
• is confluent if .
• is weakly normalized if .
• is strongly normalized if .
• has unique normal forms if .

We can relate and with .

2. State

A state is a partial function from variables to numbers () such that is defined for finitely many (e.g. ). Our next small step semantics will be defined in terms of configurations , and .

We define the state update operation on states as:

For example, if , then:

2.1 Small Step Semantics

We can define a new relation for while with the following inference rules:

Similarly, we can define a relation for commands with the following inference rules:

We can also find that , and are deterministic and confluent. We can easily show this for , by saying that :

• If and , then .
• If and then there exists a such that and .

2.2 More Configurations

Answer configurations are normal form configurations that describe the answer to some computation:

• Answer configurations of are in the form where .
• Answer configurations of are in the form where .
• Answer configurations of are in the form .

Stuck configurations are normal form configurations that are not answer configurations. They are configurations that cannot take any more steps.

The evaluations and are normalizing, while is not normalizing. Specifically, we can have infinite loops, such as the program . The proof for this is trivial.

2.3 Strictness

We can define some short circuit semantics for :

An operation is called strict in one of its arguments if it always needs to evaluate that argument. For example:

• Addition is strict in both arguments.
• is strict in its first argument (left-strict), but not in its second argument.