CS代考 Structural Induction – cscodehelp代写

Structural Induction
COMP1600 / COMP6260
Australian National University
Semester 2, 2020
1/60

Induction on Lists
Q. How do we make all finite lists?
A. All lists (over type A) can be obtained via the following: the empty list [] is a list (of elements of type A)
given a list as and an element a (of type A), then prefixing as with a is a list (written a : as).
That is, lists are an inductively defined data type.
Q. How do we prove a property P(l) for all lists l?
A. We (only) need to prove it for list constructed as above. establish that the property holds for [], i.e. P([])
if as is a list for which P(as) holds, and a is arbitrary, show that P(a : as) holds.
2/60

Making and Proving in Lockstep
Suppose we want to establish that P(as) holds for all lists as. Stage 0. as = [].
need to establish P([]).
Stage 1. as = [a] has length 1.
need to establish that P([a])
already know that P([]) holds, may use this knowledge!
…
Stagen+1. as=a:as′ haslengthn+1
need to establish that P(a : as′)
already know that P(as′) and may use this knowledge
May use the fact that P(as) holds for lists constructed at previous stage
3/60

List Induction, Informally
To prove that ∀as.P(as) it suffices to show
Base Case. P([]), i.e. P holds for the empty list
Step Case. ∀a.∀as.P(as) → P(a : as)
assuming that P(as) holds for all lists as (considered at previous
stage)
show that also P(a : as) holds, for an arbitrary element a
Example.
P([1,3,4,7]) follows from P([3,4,7]) by step case P([3,4,7]) follows from P([4,7]) by step case P([4,7]) follows from P([7]) by step case
P([7]) follows from P([]) by step case P([]) holds by base case.
4/60

Induction on Structure
List Induction as a proof rule:
P([ ])
Annotated with types: P([ ] :: [a])
∀x. ∀xs. P(xs) → P(x : xs) ∀xsP(xs)
∀(x :: a). ∀(xs :: [a]). P(xs) → P(x : xs) ∀(xs :: [a]). P(xs)
5/60

Standard functions
Recall the following (standard library) function definitions:
length [] length (x:xs)
map f []
map f (x:xs)
[] ++ys (x:xs) ++ ys
=0
= 1 + length xs
=[] =fx:mapfxs
=ys =x:(xs++ys)
— (L1)
— (L2)
— (M1)
— (M2)
— (A1) — (A2)
We read (and use) each line of the definition as equation.
6/60

Example. Mapping over Lists Preserves Length
Show. ∀xs.length (map f xs) = length xs.
Need to establish both premises of induction rule: P([]), and
∀x.∀xs.P(xs) → P(x : xs).
Base Case: P([ ])
length (map f []) = length []
Both sides are equal by M1: map f [] = [].
7/60

Step Case: ∀x. ∀xs. P(xs) → P(x : xs)
Induction Hypothesis. Assume for an arbitrary list as that
length (map f as) = length as — (IH)
Proof Goal. For arbitrary a, now prove that P(a : as), i.e. length (map f (a:as)) = length (a:as)
length (map f (a:as))
= length (f a : map f as) — by (M2)
= 1 + length (map f as) = 1 + length as
= length (a:as)
— by (L2) — by (IH) — by (L2)
Formally (using → I and ∀I )
this gives P(as) → P(a : as)
as both a and as were arbitrary, have ∀x.∀xs.P(xs) → P(x : xs)
8/60

In terms of Natural Deduction
Fixing arbitrary a and as and assuming P(as), we show P(a : as). That is, we reason as follows:
1aas P(as)
.
6 7
8 9
.
P(a : as)
P(as) → P(a : as) ∀xs. P(xs) → P(a : xs)
∀x. ∀xs. P(xs) → P(x : xs)
→-I, 1–6 ∀-I, 7
∀-I, 8
9/60

Concatenation
Show: length (xs ++ ys) = length xs + length ys statement contains two lists: xs and ys
but induction principle only allows for one?
Formally. Show that
∀xs.∀ys.length (xs ++ ys) = length xs + length ys.
􏰣 􏰢􏰡 􏰤
P(xs)
Equivalent Alternative.
∀ys.∀xs.length (xs ++ ys) = length xs + length ys. 􏰣 􏰢􏰡 􏰤
P(ys)
As a slogan.
list induction allows us to induct on one list only. the other list is treated as a constant.
but on which list should we induct?
10/60

List Concatenation: Even more Options!
Show: length (xs ++ ys) = length xs + length ys Option 1. Do induction on xs
∀xs.∀ys.length (xs ++ ys) = length x + length ys. 􏰣 􏰢􏰡 􏰤
P(x) Option 2. Reformulate and do induction on ys
∀ys.∀xs.length (xs ++ ys) = length xs + length ys. 􏰣 􏰢􏰡 􏰤
P(ys)
Option 3. Fix an arbitrary ys and show the below, then use ∀I
∀xs.length (xs ++ ys) = length xs + length ys. 􏰣 􏰢􏰡 􏰤
P(xs)
Option 4. Fix an arbitrary xs and show the below, then use ∀I
∀ys.length (xs ++ ys) = length xs + length ys. 􏰣 􏰢􏰡 􏰤
P(ys)
11/60

Choosing the most helpful formulation
Problem. For length (xs ++ ys) = length xs + length ys induct on xs (and treat ys as a constant), or
induct on ys (and treat xs as a constant)?
Clue. Look at the definition of xs ++ ys: [] ++ys =ys
(x:xs) ++ ys = x : (xs ++ ys) the list xs (i.e. the first argument of ++) changes
–(A1) — (A2)
the second argument (i.e. ys) remains constant Approach. Induction on xs and treat ys as a constant, i.e.
∀xs.∀ys.length (xs ++ ys) = length xs + length ys. 􏰣 􏰢􏰡 􏰤
P(xs)
12/60

The Base Case
Given.
length [] length (x:xs)
map f []
map f (x:xs)
[] ++ys (x:xs) ++ ys
=0
= 1 + length xs
=[] =fx:mapfxs
=ys =x:(xs++ys)
— (L1) — (L2)
— (M1) — (M2)
— (A1) — (A2)
Base Case: P([ ]) We want to prove
length ([] ++ ys) = length [] + length ys
length ([] ++ ys) = length ys — by (A1) = 0 + length ys
= length [] + length ys — by (L1)
13/60

Concatenation preserves length: step case
Step Case.Show that ∀x. ∀xs. P(xs) → P(x : xs) Assume P(as)
∀ys. length (as ++ ys) = length as + length ys — (IH) Prove P(a : as), that is
∀ys.length ((a:as) ++ ys) = length (a:as) + length ys For arbitrary ys we have:
length ((a:as) ++ ys)
= length (a : (as ++ ys)) — by (A2) = 1 + length (as ++ ys) — by (L2) = 1 + length as + length ys — by (IH) = length (a:as) + length ys — by (L2)
Theorem proved!
14/60

A few meta-points:
On the induction hypothesis:
The induction hypothesis ties the recursive knot in the proof.
If you haven’t used it, the proof is likely wrong.
It’s important to know what precisely the induction hypothesis actually is!
On rules:
Only use the rules that are given, that is
􏲓 the function definitions
􏲓 the induction hypothesis
􏲓 basic arithmetic
15/60

Concatenation Distributes over Map
Show: map f (xs ++ ys) = map f xs ++ map f ys
Which list?
as before, ++ defined by recursion on xs
treat ys as a constant. Show.
∀xs.∀ys. map f (xs ++ ys) = map f xs ++ map f ys 􏰣 􏰢􏰡 􏰤
P(xs)
Solet P(xs) be mapf(xs++ys)=mapfxs++mapfys
Base Case: P ([ ]). Show for arbitrary ys , that mapf([]++ys) =mapf[]++mapfys.
mapf([]++ys) =mapfys –by(A1) = [] ++ map f ys — by (A1) = map f [] ++ map f ys — by (M1)
16/60

Concatenation Distributes over Map, Continued
Step Case: ∀x. ∀xs. P(xs) → P(x : xs) Assume P(as)
map f (as ++ ys) = map f as ++ map f ys — (IH)
Prove P(a : as), that is
map f ((a:as) ++ ys) = map f (a:as) ++ map f ys
map f ((a:as) ++ ys)
= map f (a : (as ++ ys))
= f a : map f (as ++ ys)
= f a : (map f as ++ map f ys) = (f a : map f as) ++ map f ys = map f (a:as) ++ map f ys
Theorem proved!
— by (A2) — by (M2) — by (IH) — by (A2) — by (M2)
17/60

Observe a Trilogy
Inductive Definition defines all lists data [a] = [] | a : [a]
Recursive Function Definitions give a value for all lists f [] = ….
f (x:xs) = …. (definition usually involves f xs)
Structural Induction Principle establishes property for all lists Prove P([ ])
Prove ∀x. ∀xs. P(xs) → P(x : xs) (proof usually uses P(xs))
Each version has a base case and a step case.
The form of the inductive type definition determines the form of recursive function definitions and the structural induction principle.
18/60

Induction on Finite Trees
Inductive Definition of finite trees (for an arbitrary type a)
1. Nul is of type Tree a
2. If landrareoftypeTree aandxisoftypea,thenNode l x ris of type Tree a.
No object is a finite tree of a’s unless justified by these clauses.
Tree Induction. To show that P(t) for all t of type Tree a:
Show that P(Nul) holds
Show that P(Node l x r) holds whenever both P(l) and P(r) are true.
19/60

Induction for Lists and Trees
Natural Numbers.
data Nat =
O | S Nat
Lists.
data [a] =
[] | a : [a]
Trees.
data Tree a =
Nul
P(O)
∀n.P(n) → P(Sn) ∀n.P (n)
∀x.∀xs.P(xs) → P(x : xs) ∀xs.P (xs)
P([])
P(Nul) ∀l.∀x.∀r.P(l) ∧ P(r) → P(Node l x r)
| Node (Tree a) a (Tree a)
∀t .P (t)
20/60

Why does it Work?
Given.
Base Case: P(Nul) Step Case:
22
14 11
∀x l r.P(l) ∧ P(r) → P(Node l x r)
Show. P(Node(Node14NulNul)22(NodeNul11Nul))
1. P(Nul) is given
2. P(Node Nul 14 Nul) follows from P(Nul) and P(Nul) 3. P(Node Nul 11 Nul) follows from P(Nul) and P(Nul)
4. P(Node (Node Nul 14 Nul) 22 (Node Nul 11 Nul))
follows from P(Node Nul 14 Nul) and P(Node Nul 11 Nul)
21/60

Induction on Structure
Data Type.
data Tree a =
Nul
| Node (Tree a) a (Tree a)
Tree Induction as a proof rule:
P(Nul) ∀t1. ∀x. ∀t2. P(t1) ∧ P(t2) → P(Node t1 x t2)
∀tP(t)
with the following types: x::a is of type a
t1::Tree a and t2::Tree a are of type Tree a.
22/60

Standard functions
mapT f Nul = Nul — (M1) mapT f (Node t1 x t2)
= Node (mapT f t1) (f x) (mapT f t2) — (M2)
count Nul = 0 count (Node t1 x t2)
= 1 + count t1 + count t2
Example. We use tree induction to show that
count (mapT f t) = count t
holds for all functions f and all trees t.
(Analogous to length (map f xs) = length xs for lists)
— (C1) — (C2)
23/60

Show count (mapT f t) = count t
Base Case: P (Nul )
count (mapT f Nul) = count Nul
This holds by (M1)
24/60

Step case
Show. ∀l.∀x.∀r.P(l)∧P(r)→P(Nodelxr)
Induction Hypothesis for arbitrary u1 and u2: P(u1) ∧ P(u2) written as
count (mapT f u1) = count u1 — (IH1)
count (mapT f u2) = count u2 — (IH2)
Proof Goal. For arbitrary a, show that P(Node u1 a u2), i.e. count (mapT f (Node u1 a u2)) = count (Node u1 a u2)
25/60

Step case continued
Proof Goal. P(Node u1 a u2), i.e.
count (mapT f (Node a u1 u2)) = count (Node a u1 u2)
Our Reasoning:
count (mapT f (Node a u1 u2))
= count (Node (mapT f u1) (f x) (mapT f u2)) — by (M2) =1+count(mapTfu1)+count(mapTfu2) –by(C2) = 1 + count u1 + count u2 — by (IH1, IH2) = count (Node a u1 u2) — by (C2)
Theorem proved!
26/60

Observe the Trilogy Again
There are three related stories exemplified here, now for trees
Inductive Definition
dataTreea=Nul|Node (Treea) a(Treea)
Recursive Function Definitions
f Nul = … f(Node l x r)=…
Structural Induction Principle
Prove P(Nul)
Prove ∀l.∀x.∀r.P (l) ∧ P (r) → P (Node l x r)
Similarities.
One definition / proof obligation per Constructor Assuming that smaller cases are already defined / proved
27/60

Flashback: Accumulating Parameters
Two version of summing a list:
sum1 []
sum1 (x:xs)
sum2 xs
sum2’ acc []
sum2’ acc (x:xs) = sum2’ (acc + x) xs
Crucial Differences.
=0
= x + sum1 xs
— (S1)
— (S2)
— (T1)
— (T2)
— (T3)
= sum2’ 0 xs
= acc
one parameter in sum1, two in sum2
both parameters change in the recursive call in sum2
28/60

Show: sum1 xs = sum2 xs
sum1 []
sum1 (x:xs)
sum2 xs
sum2’ acc []
sum2’ acc (x:xs) = sum2’ (acc + x) xs
Base Case: P ([])
sum2 [] = sum1 [] sum2[]=sum2’0[] –by(T1)
= 0 — by (T2)
= sum1 [] — by (S1)
=0
= x + sum1 xs
— (S1)
— (S2)
— (T1)
— (T2)
— (T3)
= sum2’ 0 xs
= acc
29/60

Step case
Step Case: ∀x.∀xs.P(xs) → P(x : xs) Assume:
sum2 as = sum1 as
Prove:
sum2 (a:as) = sum1 (a:as)
sum2 (a:as) = sum2’ 0 (a:as)
= sum2’ (0 + a) as
sum1 (a:as) = a + sum1 as
= a + sum2 as
= a + sum2’ 0 as
Problem.
can’t apply IH: as 0 ̸= 0 + a
accumulating parameter in sum2 has changed
— (IH)
— by (T1)
— by (T3)
— by (S2)
— by (IH)
— by (T1)
30/60

Proving a Stronger Property
Solution. Prove a property that involved both arguments.
sum1 []
sum1 (x:xs)
sum2 xs
sum2’ acc []
sum2’ acc (x:xs) = sum2’ (acc + x) xs
=0
= x + sum1 xs
— (S1)
— (S2)
— (T1)
— (T2)
— (T3)
= sum2’ 0 xs
= acc
Observation. (from looking at the code, or experimenting) sum2’ acc xs = acc + sum1 xs
Formally. We show that
∀xs.∀acc.sum2’ acc xs = acc + sum1 xs
􏰣 􏰢􏰡 􏰤
P (xs)
Base Case: Show P([]), i.e. ∀acc.acc + sum1 [] = sum2’ acc [].
acc + sum1 [] = acc + 0 = acc — by (S1)
= sum2’ acc [] — by (T2)
31/60

Step case
Step Case. ∀x.∀xs.P(xs) → P(x : xs). Induction Hypothesis
∀acc.acc + sum1 as = sum2’ acc as (IH)
Show.
∀acc.acc + sum1 (a:as) = sum2’ acc (a:as) Our Reasoning:
acc + sum1 (a:as) = acc + a + sum1 as — by (S2) =sum2’(acc+a)as –by(IH)(*)
= sum2’ acc (a:as) — by (T3)
Our induction hypothesis is ∀ acc. . . .
In (*) we instantiate ∀acc with it acc + a
∀ acc is absolutely needed in induction hypothesis
32/60

Proving the Original Property
We have. ∀xs. P(xs), that is:
∀xs. ∀acc. acc + sum1 xs = sum2’ acc xs
Equivalent Formulation. (change order of quantifiers) ∀acc. ∀xs. acc + sum1 xs = sum2’ acc xs
Instantiation (acc = 0) ∀xs.0+sum1xs=sum2’0xs
∀xs. sum1 xs = sum2’ 0 xs ∀ xs. sum1 xs = sum2 xs
That is, we have (finally) proved the original property.
–by ∀-E — by arith — by T1
33/60

When might a stronger property P be necessary ? Alarm Bells.
sum2’ acc (x:xs) = sum2’ (acc + x) xs
Pattern.
both arguments change in recursive calls Programming Perspective.
to evaluate sum2’, need evaluation steps where acc ̸= 0 Proving Perspective.
to prove facts about sum2’, need inductive steps where acc ̸= 0
Orthogonal Take.
sum2’ is more capable than sum2 (works for all values of acc) when proving, need stronger statement that also works for all acc
34/60

Look at proving it for xs = [2, 3, 5]
Backwards Proof for a special case:
0 + sum1 [2,3,5] = sum2’ 0 [2,3,5] because
0 + 2 + sum1 [3,5] = sum2’ (0+2) [3,5] because
0 + 2 + 3 + sum1 [5] = sum2’ (0+2+3) [5] because 0+2+3+5+sum1[]=sum2’(0+2+3+5)[] because 0 + 2 + 3 + 5 = (0+2+3+5)
Termination.
the list gets shorter with every recursive call despite the accumulator getting larger!
35/60

Another example
flatten :: Tree a -> [a]
flatten Nul = [] — (F1)
flatten (Node l a r) = flatten l ++ [a] ++ flatten r — (F2)
flatten2 :: Tree a -> [a]
flatten2 tree = flatten2’ tree []
flatten2’ :: Tree a -> [a] -> [a]
flatten2’ Nul acc = acc
flatten2’ (Node l a r) acc =
flatten2’ l (a:flatten2’ r acc)
Show.
flatten2’ t acc = flatten t ++ acc for all t :: Tree a, and all acc :: [a].
— (G)
— (H1)
— (H2)
36/60

Proof
Proof Goal.
∀t.∀acc.flatten2’ t acc = flatten t ++ acc 􏰣 􏰢􏰡 􏰤
P (t)
Base Case t = Nul. Show that
flatten2’ Nul acc = flatten Nul ++ acc
flatten2’ Nul acc = acc
= [] ++ acc
— by (H1)
— by (A1)
— by (F1)
= flatten Nul ++ acc
Step Case: t = Node y t1 t2. Assume that for all acc,
flatten2’ t1 acc = flatten t1 ++ acc — (IH1)
flatten2’ t2 acc = flatten t2 ++ acc — (IH2)
Required to Show. For all acc,
flatten2’ (Node t1 y t2) acc = flatten (Node t1 y t2) ++ acc
37/60

Proof (continued)
Proof (of Step Case): Let a be given (we will generalise a to ∀acc)
flatten2’ (Node t1 y t2) a
= flatten2’ t1 (y : flatten2’ t2 a)
= flatten t1 ++ (y : flatten2’ t2 a)
= flatten t1 ++ (y : flatten t2 ++ a)
= flatten t1 ++ ((y : flatten t2) ++ a) — by (A2)
= (flatten t1 ++ (y : flatten t2)) ++ a — (++ assoc)
= flatten (Node t1 y t2) ++ a
Notes.
in IH1, acc is instantiated with (y : in IH1, acc is instantiated with a
As a was arbitrary, this completes the proof.
— by (F2)
flatten2’ t2 a)
— by (H2)
— (IH1)(*)
— (IH2)(*)
38/60

General Principle
Inductive Definition
dataTreea=Nul|Node (Treea) a(Treea) Constructors with arguments, may include type being defined!
Structural Induction Principle
Prove P(Nul)
Prove ∀l.∀x.∀r.P (l) ∧ P (r) → P (Node l x r)
One proof obligation for each constructor
All arguments universally quantified
May assume property of same type arguments
39/60

General Principle: Example
Given. Inductive data type definition of type T
data T = C1 Int
| C2 T T
| C3 T Int T
Constructors:
C1 :: Int -> T
| C2 :: T -> T -> T
| C3 :: T -> Int -> T -> T
Q. What does the induction principle for T look like?
40/60

General Principle: Example
Given. Inductive data type definition of type T
data T = C1 Int
| C2 T T
| C3 T Int T
Constructors:
C1 :: Int -> T
| C2 :: T -> T -> T
| C3 :: T -> Int -> T -> T
Q. What does the induction principle for T look like?
A. To show ∀t :: T,P(t), need to show
three things (three constructors)
all arguments are universally quantified
P(t) may be assumed for arguments of type t:T
More Concretely. To show ∀t :: T,P(t), need to show ∀n.P (C1 n)
∀t1.∀t2.P (t1) ∧ P (t2) → P (C2 t1 t2) ∀t1.∀n.∀t2.P (t1) ∧ P (t2) → P (C3 t1 n t2)
40/60

Induction on Formulae
Boolean Formulae without negation as Inductive Data Type
data NFForm =
TT
| Var Int
| Conj NFForm NFForm
| Disj NFForm NFForm
| Impl NFForm NFForm
Induction Principle. ∀f :: NFForm.P(f) follows from P (TT)
∀n.P (Var n)
∀f1.∀f2.P (f1) ∧ P (f2) → P (Conj f1 f2) ∀f1.∀f2.P (f1) ∧ P (f2) → P (Disj f1 f2) ∀f1.∀f2.P (f1) ∧ P (f2) → P (Impl f1 f2)
41/60

Recursive Definition
Given.
data NFForm =
TT
| Var Int
| Conj NFForm NFForm
| Disj NFForm NFForm
| Impl NFForm NFForm
Evaluation of a (negation free) formula:
eval :: (Int -> Bool) -> NFForm -> Bool
eval theta TT = True
eval theta (Var n) = theta n
eval theta (Conj f1 f2) = (eval theta f1) && (eval theta f2)
eval theta (Disj f1 f2) = (eval theta f1) || (eval theta f2)
eval theta (Impl f1 f2) = (not (eval theta f1)) || (eval theta f2)
42/60

Example Proof
Theorem. If f is a negation free formula, then f evaluates to True under the valuation theta = True.
More precise formulation. Let theta be defined by theta = True. Then, for all f of type NFForm, we have eval theta f = True.
Proof using the induction principle for negation free formulae. Base Case 1. Show that eval theta TT = True. (immediate). Base Case 2. Show that ∀n.eval theta (Var n) = True.
eval theta (Var n) = theta n = True (by definition of eval and definition of theta)
43/60

Proof of Theorem, Continued
Step Case 1. Assume that
eval theta f1 = True (IH1) and eval theta f2 = True (IH2).
Show that
eval theta (Conj f1 f2) = True
Proof (of Step Case 1).
eval theta (Conj f1 f2)
= (eval theta f1) && (eval theta f2)
= True && True
= True
— defn eval
— IH1, IH2
— defn &&
44/60

Wrapping Up
Step Case 2 and Step Case 3. In both cases, we may assume eval theta f1 = True (IH1) and
eval theta f2 = True (IH2).
and need to show that
eval theta (Conj f1 f2) = True (Step Case 2) eval theta (Impl f1 f2) = True (Step Case 3)
The reasoning is almost identical to that of Step Case 1, and we use
True || True = True
False || True = True
Summary. Having gone through all the (base and step) cases, the theorem is proved using induction for the data type NFForm.
45/60

Inductive Types: Degenerate Examples
Consider the following Haskell type definition:
data Roo a b =
MkRoo a b
Q. Given types a and b, what is the type Roo a b?
46/60

Inductive Types: Degenerate Examples
Consider the following Haskell type definition:
data Roo a b =
MkRoo a b
Q. Given types a and b, what is the type Roo a b?
A. It is the type of pairs of elements of a and b
To make an element of Roo a b, can use constructor MkRoo: b -> Roo a b
No other way to “make” elements of Roo a b.
Let’s give this type its usual name:
data Pair a b =
MkPair a b
a ->
46/60

Recursion and Induction Principle
Data Type.
data Pair a b =
MkPair a b
Pair Recursion. To define a function f::Pair a b -> T: f(MkPairxy)=… x… y… we may use both the values of x and y – same as for pairs
Pair Induction. To prove ∀x::Pair a b.P(x) show that ∀x.∀y.P(MkPair xy)
just one constructor and no occurrences of arguments of pair type
47/60

Inductive Types: More Degenerate Examples
Consider the following Haskell type definition:
data Wombat a b =
Left a
| Right b
Q. Given types a and b, what is the type Wombat a b?
48/60

Inductive Types: More Degenerate Examples
Consider the following Haskell type definition:
data Wombat a b =
Left a
| Right b
Q. Given types a and b, what is the type Wombat a b?
A. It is the type of tagged elements of either a or b. use constructor Left: a -> Wombat a b
use the constructor Right: b -> Wombat a b No other way to “make” elements of Wombat a b.
Let’s give this type its usual name:
data CoPair a b =
Left a
| Right b
48/60

Recursion and Induction Principle
Data Type.
data CoPair a b =
Left a
| Right b
Copair Recursion. To define a function f::CoPair a b -> T: f(Leftx)=… x… …
f(Righty)=… y… …
we have to give equations for both cases: left and right.
Copair Induction. To prove ∀z::CoPair a b.P(z) show that ∀x.P(Left x)
show that ∀y.P(Right y)
here: two constructors and no occurrences of arguments of copair type
49/60

Limitations of Inductive Proof
Termination. Consider the following (legal) definition in Haskell nt :: Int -> Int
nt x = nt x +1
Taking Haskell definitions as equations we can prove 0 = 1: 0 = nt 0 – nt 0 = nt 0 + 1 – nt 0 = 1
I.e. a statement that is patently false.
Limitation 1. The proof principles outlined here only work if all functions are terminating.
50/60

Limitations, Continued
Finite Data Structures. Consider the following (legal) Haskell definition blink :: [Bool]
blink = True:False:blink
and consider for example
length blink
Clearly, length blink is undefined and so may introduce false
statements.
Limitation 2. The proof principles outlined here only work for all finite elements of inductive types.
51/60

Addressing Termination
Q. How do we prove that a function terminates? Example 1. The argument gets “smaller”
length [] = 0
length (x:xs) = 1 + length xs
Example 2. Only one argument gets “smaller”? length’ [] a = a
length’ (x:xs) a = length’ xs (a+1)
Q. What does “getting smaller” really mean?
52/60

Termination Measures
Given. The function f defined below as follows f :: T1 -> T2
fx= exp(x)
Q. When does the argument of f “get smaller”?
A. Need measure of smallness: m: T1 -> N
Informally.
in every recursive call, the measure m of the argument of the call is smaller
termination, because natural numbers cannot get smaller indefinitely.
Formally. A function m: T1 -> N is a termination measure for f if for every defining equation f x = exp, and
for every recursive call f y in exp
wehavethatm y < m x. 53/60 Example List Reversal. rev :: [a] -> [a]
rev [] = []
rev (x:xs) = (rev xs) + [x]
Termination Measure.
m :: [a] -> N
m xs = length xs
Recursive Calls only in the second line of function definition Show that m xs < m (x:xs) I.e. length xs < length (x:xs) – this is obvious. 54/60 Termination Measures: General Case Consider a recursively defined function f : T1 -> T2 -> … -> Tn -> T0
that is defined using multiple equations of the form
f x1 .. xn = exp(x1, …, x_n)
taking n arguments of types T1, . . . , Tn and computes a value of type T.
Definition. A termination measure for f is a function of type m: T1->T2->…->Tn->N
such that
for every defining equation f x1 … xn = exp, and for every recursive call f y1 … yn in exp
wehavethatm y1 .. yn < m x1 ... xn. 55/60 Termination Proofs Theorem. Let f: T1 -> … -> Tn -> T be a function with termination measure m: T1 -> T2 -> …-> Tn -> N.
Then the evaluation of f x1 .. xn terminates for all x1, . . . , xn.
Proof. We show the following statement by induction on n ∈ N. ∀n.if m x1 … xn < n then f x1 .. xn terminates Base Case. n = 0 is trivial(!) Step Case. Assume that the statement is true for all n0 < n and let x1, . . . , xn be given. Then the recursive call f x1 .. xn = exp(x1, ..., xn) onlycontainscallsoftheformf y1 .. ynforwhichm y1 .. yn < m x1 ... xn so that these calls terminate by induction hypothesis. Therefore f x1 ... xn terminates. 56/60 Example rev_a :: [a] -> [a] -> [a]
rev_a [] ys = ys
rev_a (x:xs) = rev_a xs (x:ys)
Termination Measure (for any type a) m :: [a] -> [a] -> N
m xsys=lengthxs
Recursive Calls only in second line of function definition. Show that m xs (x:ys) < m (x:xs) ys. I.e. length xs < length (x:xs) – this is obvious. 57/60 Outlook: Induction Principles More General Type Definitions data Rose a = Rose a [Rose a] Example using TTree eat :: TTree a b -> [a] -> b
eat (Wry)_=y
eat (Rd f) (x:xs) = eat (f x) xs
Induction Principles
for Rose: may assume IH for all list elements for TTree: mayh assume IH for all values of f
data TTree a b =
Wr b | Rd (a -> TTree a b)
58/60

Outlook: Termination Proofs
More Complex Function Definitions
ack :: Int -> Int -> Int
ack 0 y = y+1
ack x 0 = ack (x-1) 1
ack x y = ack (x-1) (ack x (y-1))
Termination Measures
m x y = x doesn’t account for last line of function definition difficulty: nested recursive calls
Digression. Both induction and termination proofs scratch the surface!
59/60

Outlook: Formal Proof in a Theorem Prover
The Coq Theorem Prover https://coq.inria.fr based on Theory Coqand’s Calculus of Constructions requires that all functions terminate.
Examples.
Natural Deduction:
Lemma ex_univ {A: Type} (P: A -> Prop) (Q: Prop): ((existsx,Px)->Q)->forallx, Px->Q.
Inductive Proofs:
Lemma len_map {A B: Type} (f: A -> B): forall (l: list A),
length l = length (map f l).
(and some other examples)
60/60