| 6ix07 |
Lecture 1 |
Discussed Floyd’s 1967 paper.
Suggested reading for next time is Hoare(69) & Dijkstra(75), especially the latter. Useful backup (but not necessary) would be Galois connections(Supp); and in the background (also not necessary) start to look through ARP(Ch 1).
|
| 13ix07 |
No lecture |
| 20ix07 |
Lecture 2 |
Discussed (briefly) Hoare’s 1969 paper and Dijkstra’s 1975 paper. Gave “in-your-pocket” semantics for Dijkstra’s small imperative language GCL, but left loops for later. Example of invariant-based development of a small program.
Didn’t quite make it to Galois connections, but here is an example.
|
| 27ix07 |
Lecture 3 |
Having now seen how the concepts developed piecemeal, we leap forward to the present and explain it all with hindsight in the now-conventional style: effectively “Program Semantics 101.” Normally such material might occur at the beginning of a course on domain theory, the cost being that one would then have to do the more advanced stuff as well. We won’t be — we will cover only as much as we need: operational semantics for deterministic/terminating programs, then possibly non-terminating.
|
| 4x07 |
Lecture 4 |
We continued from last week’s lecture with possibly non-deterministic programs, the (Smyth) powerdomain for dealing with those, the sudden appearance of pre-orders and how, by up-closure/quotient, we can get rid of the pre-. We concluded that section with a summary of the relational semantics.
Then we examined the (dual) predicate-transformer semantics and finished, with all that in place, by looking at the Galois connection between the two styles of semantics, and how it defines so-called Healthiness Conditions. Later we will see what use those conditions are. |
| 11x07 |
No lecture |
| 18x07 |
Lecture 5 |
We began probabilistic semantics, both relational and transformer, by taking the key insights from Kozen’s pioneering approach in which he introduced an expectation-based logic generalising the Hoare/Dijkstra assertions. He did not treat demonic nondeterminism; and (in this lecture) neither did we. (Continue to read our Chapter 1 for that.)
We did however whiz through the construction of a suitable domain for representing probabilistic/possibly-nonterminating computations , to which next week we will add nondeterminism. |
| 25x07 |
Lecture 6 |
We (finally) added nondeterminism, very briefly; and then we started Chapter 1, right from the beginning. With all the construction work done we were able to recall some of the reasons (it conceals under the excuse of being an introductory section) for the way things are that way. It helps to have
Chapter 6 in the back of your mind. |
| 1xi07 |
Lecture 7 |
We continued with Chapter 1, discussing the infamous Monty Hall example, and reaching finally the somewhat unlikely-in-appearance “healthiness condition” of sub-linearity (which Plotkin says should have been called “super-linearity”). Whatever its name, it has surprisingly nice specialisations that generalise the healthiness conditions we have seen already, for standard programs, like conjunctivity.
But where does sub-linearity come from...? And does it really have to look like that, or can it be split up into smaller more-intuitive pieces?
[ Further on Monty Hall: the example revealed a hidden benefit of precise semantics, that it becomes impossible –or at least much harder– to ask ill-formed questions. ]
|
| 8xi07 |
Lecture 8 |
Based on a (still-in-draft)
conference submission, the lecture showed how checking-for- and, in particular, refuting refinements can be automated using a Satisfaction-Modulo-Theories solver.
Strangely, the
Separating Hyperplane Lemma
did not appear in the lecture (in spite of the advertisement that it would, and indeed that it was essential). Yet it is essential. Where did Annabelle hide it?
(Separating hyperplanes are used in the famous Case of the Federalist Papers.)
|
| 15xi07 |
Lecture 9 |
We explored probabilistic termination, thus reaching finally the front cover of the text. It depicts a synchronous network with probabilistic transitions where the tokens move independently from place to place and yet –with probability one– end up all in the same node.
The rules are that grouped tokens always move together, having non-zero (but otherwise unconstrained) probabilities of choosing any particular out-arc (including the degenerate stay-here option); they form larger groups if/when they merge. Watch the logo top-right for several minutes to see it in action. Can you prove they always end up together eventually?
But we did not discuss the book cover after all, moving instead directly to... the probabilistic Dining Philosophers.
Afterwards, there was some discussion of random walks: here are three articles (one, two and three) that show how they can be thought of in terms of networks of resistors, using Ohm’s and Kirchoff’s Laws.
|
| 22xi07 |
No lecture |
 |
| 29xi07 |
Lecture 10 |
This lecture is planned to cover probabilistic loop invariants, relying on our treatment of termination in Lecture 9. One of the examples should be the small program in the book’s preface
which, specialised to p=1/3, becomes a program for making a fair three-way choice using a two-sided coin:
x:= 1/3;
WHILE 1/2 DO // Choose w/prob 1/2 whether to (re)enter or exit the loop.
x:= 1-x
OD;
IF x=2/3 THEN /* 1/3 probability here */
ELSE /* 2/3 probability here */
FI
This program can easily be supervised even by an innumerate parent, boiling down to
“Flip the coin until heads appears; with probability exactly 1/3 that will be an even number of times.” Thus let the youngest of three children flip until heads, awarding the ice-cream if the number of flips is even; if odd, flip once more to decide between the older two.
|
| 6xii07 |
Lecture 11 |
This is planned to be a data-projector presentation, based on Annabelle McIver’s recent tutorial at the Voss Workshop in Leiden, covering the whole enterprise (probability, refinement and abstraction) for an informed audience who have not seen the material before. As such, it will provide for us a good round-up of all we have covered.
|