Lecture 6

Today, we return to the example from Lecture 5, and talk about recursive datatypes, how to reason about them by structural induction. We will also talk about the distinction between total and partial correctness.

Recursive datatypes occur very often, in forms of lists, queues, trees, but also dictonaries, tables, and so on. In the next lecture we will introduce a notion of lists that is built into ML.

Code: poker.sml.

Reading: Programming Standard ML.
Chapter 24: Specification and Correctness
Chapter 25: Induction and Recursion
Chapter 26: Structural Induction.