Natural Numbers Lists Trees
1
Structural Induction with Haskell
Dr. Liam O’Connor
University of Edinburgh LFCS UNSW, Term 3 2020
Natural Numbers Lists Trees
Recap: Induction
Definition
Let P(x) be a predicate on natural numbers x ∈ N. To show ∀x ∈ N. P(x), we can use induction:
Show P(0)
Assuming P(k) (the inductive hypothesis), show P(k + 1).
Example (Sum of Integers)
Write a recursive function sumTo to sum up all integers from 0 to the input n. Show that:
∀n ∈ N. sumTo n = n(n + 1) 2
2
Natural Numbers Lists Trees
Haskell Data Types
We can define natural numbers as a Haskell data type, reflecting this inductive structure.
data Nat = Z | S Nat
Example
Define addition, prove that ∀n. n + Z = n.
Inductive Structure
Observe that the non-recursive constructors correspond to base cases and the recursive constructors correspond to inductive cases
3
Natural Numbers Lists Trees
Lists
Lists are singly-linked lists in Haskell. The empty list is written as [] and a list node is written as x : xs. The value x is called the head and the rest of the list xs is called the tail. Thus:
“hi!” == [‘h’, ‘i’, ‘!’] == ‘h’:(‘i’:(‘!’:[]))
== ‘h’ : ‘i’ : ‘!’ : []
When we define recursive functions on lists, we use the last form for pattern matching.
Example
(Re)-define the functions length, take and drop.
4
Natural Numbers Lists Trees
Induction on Lists
If lists weren’t already defined in the standard library, we could define them ourselves:
data List a = Nil | Cons a (List a)
Induction
If we want to prove that a proposition holds for all lists:
5
∀xs. P(xs)
1 Show P([]) (the base case from nil)
2 Assuming the inductive hypothesis P(xs), show P(x:xs) (the inductive case from cons).
It suffices to:
Natural Numbers Lists Trees
Induction on Lists
Example (Take and Drop)
6
Show that take (length xs) xs = xs for all xs.
Show that take 5 xs ++ drop 5 xs = xs for all xs. =⇒ Sometimes we must generalise the proof goal. =⇒ Sometimes we must prove auxiliary lemmas.
Natural Numbers Lists
Trees
Induction Principle
Binary Trees
data Tree a = Leaf
| Branch a (Tree a) (Tree a)
To prove a property P(t) for all trees t: Prove the base case P(Leaf ).
Assuming the two inductive hypotheses:
P(l) and P(r)
We must show P(Branch x l r).
Example (Tree functions)
Define leaves and height, and show ∀t. height t < leaves t
7
Natural Numbers Lists Trees
Rose Trees
data Forest a = Empty | Cons (Rose a) (Forest a)
data Rose a = Node a (Forest a) Note that Forest and Rose are defined mutually.
Example (Rose tree functions)
Define size and height, and try to show
∀t. height t ≤ size t
8
Natural Numbers Lists Trees
Simultaneous Induction
To prove a property about two types defined mutually, we have to prove two properties simultaneously.
data Forest a = Empty | Cons (Rose a) (Forest a) data Rose a = Node a (Forest a)
Inductive Principle
To prove a property P(t) about all Rose trees t and a property Q(ts) about all Forests ts simultaneously:
Prove Q(Empty)
Assuming P(t) and Q(ts) (inductive hypotheses), show Q(Cons t ts). Assuming Q(ts) (inductive hypothesis), show P(Node x ts).
9