# 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