Description
The reverse function in problem 3 incorrectly defined the recursive case
using the append operator @. This case should instead use the append function defined in
that problem. This has been fixed below.
Question 1: Power function, over natural numbers
Recall the OCaml power function over natural numbers, shown below:
let rec power n x =
match n with
| 0 -> 1.0
| _ -> x *. power (n-1) x
Using induction over natural numbers show that
power n x = x
n
.
Your proof must explicitly and clearly indicate the base case you prove, the inductive case you
prove and what the inductive hypothesis provides in the proof.
Each step in your proof must be accompanied by a justification describing why that step could be
taken.
Question 2: Power over structured numbers
Recall from lecture the OCaml type nat, the function toInt, and the power function working over
this representation of natural numbers:
type nat = Zero | Succ of nat
let toInt = function
| Zero -> 0
| Succ n -> toInt n + 1
let rec power n x = match n with
| Zero -> 1.0
| Succ n’-> x *. power n’ x
What is the principle of induction for the type nat?
Using induction over nat values show that
power n x = x
toInt(n)
Your proof must explicitly and clearly indicate the base case you prove, the inductive case you
prove and what the inductive hypothesis provides in the proof.
Each step in your proof must be accompanied by a justification describing why that step could be
taken.
1
Question 3: List reverse and append
Consider the following definition of append:
let rec reverse l = match l with
| [] -> []
| (h::t) -> append (reverse t) [h]
let rec append l1 l2 = match l1 with
| [] -> l2
| (h::t) -> h :: (append t l2)
Using the definition of reverse and the definition of append above, show, using induction, that
reverse (append l1 l2) = append (reverse l2) (reverse l1)
Your proof must explicitly and clearly indicate the base case you prove, the inductive case you
prove and what the inductive hypothesis provides in the proof.
Each step in your proof must be accompanied by a justification describing why that step could be
taken.
Question 4: List processing
Consider the following OCaml function definitions.
let isupper c = Char.code c >= Char.code ’A’ &&
Char.code c <= Char.code ’Z’
let rec someupper lst = match lst with
| [] -> false
| x::xs -> isupper x || someupper xs
Using the definition above, show using induction that
someupper (l1 @ l2) = someupper l1 || someupper l2
Your proof must explicitly and clearly indicate the base case you prove, the inductive case you
prove and what the inductive hypothesis provides in the proof.
Each step in your proof must be accompanied by a justification describing why that step could be
taken.
2
Question 5: List processing and folds Below we show again the functions defined in the
previous problem and a new alternative implementation of the recursive function defined in Question
4. This new version uses foldr. The definition of foldr is the same as you’ve seen before.
let isupper c = Char.code c >= Char.code ’A’ &&
Char.code c <= Char.code ’Z’
let rec someupper lst = match lst with
| [] -> false
| x::xs -> isupper x || someupper xs
let rec foldr (f:’a -> ’b -> ’b) (l:’a list) (v:’b) : ’b =
match l with
| [] -> v
| x::xs -> f x (foldr f xs v)
let upperor c b = isupper c || b
let foldupper lst = foldr upperor lst false
By induction, show that
someupper chs = foldupper chs
Your proof must explicitly and clearly indicate the base case you prove, the inductive case you
prove and what the inductive hypothesis provides in the proof.
Each step in your proof must be accompanied by a justification describing why that step could be
taken.
3
Question 6: Tree processing
Consider the following OCaml definitions of a tree type and a few functions over values of this type.
type ’a tree = Leaf of ’a
| Branch of ’a tree * ’a tree
let min x y = if x < y then x else y
let rec mintree t = match t with
| Leaf v -> v
| Branch (t1, t2) -> min (mintree t1) (mintree t2)
let rec tfold (l:’a -> ’b) (f: ’b -> ’b -> ’b) (t: ’a tree) : ’b = match t with
| Leaf v -> l v
| Branch (t1, t2) -> f (tfold l f t1) (tfold l f t2)
let fold_mintree t = tfold (fun x -> x) min t
Prove using induction that for any tree t of type int tree
mintree t = fold mintree t
Your proof must explicitly and clearly indicate the base case you prove, the inductive case you
prove and what the inductive hypothesis provides in the proof.
Each step in your proof must be accompanied by a justification describing why that step could be
taken.
Submission instructions: Writing proofs such as these requires a bit of clear thinking and it is
important to check your work.
Checking your work means you need to be able to read it. And to assess it, we need to be able
to read it as well.
Thus, we are requiring your solutions be electronically generated. You may turn your work in
using any of the following forms.
1. A PDF file – named hwk 03.pdf.
You may use LaTeX, enscript, or even MS Word to generate a PDF file that contains your
solutions.
2. A Markdown file – named hwk 03.md.
This is used for the lab and other homework specifications and makes it easy to see your
solution in GitHub.
3. A text file – named hwk 03.txt.
We’ve written proofs in text files in class and examples can be found in the Notes directory
of the public class repository.
Scanned or photographed versions of hand-written solutions will not be accepted.
This work is to be submitted via GitHub in a folder named Hwk 03.
The work is due by 5:00pm on Wednesday, March 7.
4
