Lecture 5

In this lecture we start to talk about the relation between inductive datatypes and correctness. In fact, there is a strong link between the two. In mathematicians we know how to do inductive proofs over natural numbers, and in computer science, we push this principle forwards and generalize it to a principle of structural induction over datatype declarations.

In this lecture, we review mathematical induction using factorial numbers as example.

Code: poker.sml.

Reading: Programming Standard ML.

• Chapter 7: Recursive Functions
• Chapter 24: Specifications and Correctness
• Chapter 25: Induction and Recursion