PLF skimming

aexp, bexp, commands, programs, program equivalence, behavioral equivalence, states, program transformation, soundness of a program transformation, program inequivalence.

We have a programming language with aexp and bexp and comm: arithmetic expressions, boolean expressions and commands. Programs are evaluated depending on the state and may alter the state via commands. See: Imp.v.

One notion of program equivalence is behavioral equivalence. That is, two programs are behaviorally equivalent if they evaluate to the same ending state (or not terminate in any final state) whenever they start in the same initial state.

We then show that behavioral equivalence is an equivalence, that they are reflexive, symmetric and transitive. And furthermore, behavioral equivalence is a congruence - if two subprograms are equivalent, the larger programs in which they are embedded are equivalent.

A program transformation is a function that takes a program as input and produces a modified program as output. A program transformation is sound if it preserves the behavior of the original program (is behaviorally equivalent to the original program).

An expression is constant if it has no variable references. Constant folding is an optimization that finds constant expressions and replaces them by their values. We show that constant folding is sound.

We show that (0 + n) elimination is sound.

Finally, now that we’ve studied behavioral equivalence, we can prove that some programs are not equivalent, by (exercise..)

aexp, bexp, commands, programs, program equivalence, behavioral equivalence, states, program transformation, soundness of a program transformation, program inequivalence.

The evaluators so far in the book have been formulated in a big-step style semantics, that is, they specify how a given expression evaluates to its final valus in one big step.

Gilles Kahn popularized this and called it natural semantics. However, it does not do well with semantics of concurrent programs, because the intermediate states that it passes through along the way are crucial.

The motivation for types in the course is to distinguish between non-termination (like infinite while loops) versus getting stuck in an erroneous configruation eg 1 + "1".

A toy language is presented, with just constants and additions. Then a big-step relation is presented, as well as a small-step evaluation relation.

We show the strong progress theorem for this language: If t is a term, then either t is a value or there exists a term t' such that t --> t'. It’s called strong progress, because every term is either a value or can make progress by stepping to another term. It’s noticable that values are exactly the terms that cannot make progress. They are called normal forms. We show that value (a syntactic concept) is equivalent to normal form (a semantic concept). We can also define a multi-step reduction relation -->*, which relates t and t' if t can reach t' by any number of reduction steps -->. Then, a result of a term t is a normal form that t can reach by multi-step reduction.

Multistep R is reflexive and is a closure of R.

Finally, we show that the big-step semantics and small-step semantics of this simple language is equivalent.

The semantics of Imp are also explored in the final section.

aexp, bexp, commands, programs, program equivalence, behavioral equivalence, states, program transformation, soundness of a program transformation, program inequivalence.

We can exclude ill-defined terms by defining a typing relation that relates terms to the types of their typing result. It is written |-- t \in T, pronounced t is type T. The typing relation is a conservative / static approximation = it does not consider what happens when the term is reduced and does not calculate the type of the normal form.

We have the progress theorem / property of typing, that states that well-typed normal forms are not stuck, or conversely, if a term is well typed, then either it is a value or it can take at least one step. We prove this by exercise.

The second theorem / property of typing is called type preservation. That is, wehn a well-typed term takes a step the result is a well-typed term of the same type.

Putting progress and preservation together, we see that a well-typed term can never reach a stuck state. Proof in the exercises.

---

Back to Top