DM22, Spring 2007 - Weekly Note 10

Lecture April 2

More on cyclic structures. The undefined value. Strict and non-strict functions. Proofs of properties of code.

Reading

Section 9.4 in Bird. Chapters 1 and 2 and Sections 4.1-2 in Bird again, now with a focus on the undefined value, and on proofs. Section 9.1 in Bird. For further information on infinite lists, see Sections 9.2-3 in Bird (which will not be curriculum).

Lecture April 16 (Expected Contents)

More on proofs of properties of code. The extensionality principle. Type inference.

Reading

Sections 1.4.1 and 4.2-4 in Bird again, now with a focus on proofs. Handouts from Thompson book (Chapter 13).

Comments

The author is fond of general laws allowing substitution of one expression (typically involving standard functions) for another. In particular, he likes their use in program derivation, where the starting point is an obviously correct, but inefficient expression, which is then transformed into a more efficient one through a sequence of equivalent expressions (which maintains correctness). For extensive examples of this, see Section 4.6 (not curriculum).

Exercises April 18

Exercises 4.2.6, 4.2.7, 4.3.2, 4.4.1, 4.4.2 (all involved definitions are in the appendix), 9.1.1, 9.1.4, 9.4.1, 9.4.2, and 9.4.3 in Bird (where 4.2.6, 4.2.7, and 4.4.2 should only be attempted after the lecture April 16).