Day03_recursion
Recursion
Recall our definition of pred, the predecessor function on
nats.
Definition pred (n : nat) : nat :=
match n with
| O ⇒ O
| S n' ⇒ n'
end.
Check pred. (* ===> nat -> nat *)
Check (pred 5). (* ===> nat *)
Compute (pred 5). (* ===> 4 *)
Compute (pred 0). (* ===> 0 (nobody's perfect) *)
match n with
| O ⇒ O
| S n' ⇒ n'
end.
Check pred. (* ===> nat -> nat *)
Check (pred 5). (* ===> nat *)
Compute (pred 5). (* ===> 4 *)
Compute (pred 0). (* ===> 0 (nobody's perfect) *)
In addition to the Check command to see an expression's type and
the Compute command to see how it evaluates, there's a Print
command to see something's definition. Let's try it.
Huh, weird! We defined pred with the Definition command, but
Coq used a fun. It turns out that these notions are
equivalent.
That is, writing:
Definition foo (x:T) (y:U) : Z := blah.
is just the same as:
Definition foo : T → U → Z := fun (x:T) (y:U) : Z ⇒ blah.
which is just the same as:
Definition foo (x:T) : U → Z := fun (y:U) ⇒ blah.
It's very useful to know equivalences in your programming
language!
It's also important to know the various forms of syntax. A
Definition takes the form:
Definition NAME ARGS× : RETURN TYPE := EXPRESSION.
where NAME is an identifier and ARGS× zero or more arguments
(optionally, wrapped in parentheses and annotated with
types). (It's conventional in computer science to use * to mean
"zero or more". The name comes from the 20th Century theorist
Stephen Cole Kleene.) The syntax for anonymous functions is
similar:
fun ARGS+ ⇒ EXPRESSION
Where the + means one or more.
For Definitions return types are optional and for funs they
are forbidden; a Definition need not have arguments, but
anonymous functions need them.
Finally---we introduced some of these concepts without such a nice
description yesterday. Hopefully things are clearer now!
What about recursive functions? I briefly showed you
evenb'... let's look at the recursive double function again,
in a bit more detail:
Definition foo (x:T) (y:U) : Z := blah.
Definition foo : T → U → Z := fun (x:T) (y:U) : Z ⇒ blah.
Definition foo (x:T) : U → Z := fun (y:U) ⇒ blah.
Definition NAME ARGS× : RETURN TYPE := EXPRESSION.
fun ARGS+ ⇒ EXPRESSION
Fixpoint double (n:nat) :=
match n with
| O ⇒ O
| S n' ⇒ S (S (double n'))
end.
Print double.
(* ===>
double = fix double (n : nat) : nat := match n with
| 0 => 0
| S n' => S (S (double n'))
end
: nat -> nat
*)
match n with
| O ⇒ O
| S n' ⇒ S (S (double n'))
end.
Print double.
(* ===>
double = fix double (n : nat) : nat := match n with
| 0 => 0
| S n' => S (S (double n'))
end
: nat -> nat
*)
Rather than writing fun, it says fix double. Interesting!
After that, it looks mostly like a fun, though there's a return
type, too.
Here's another equivalence, where ARGS+ means one or more arguments:
Fixpoint NAME ARGS+ : RETURN TYPE := EXPRESSION.
is just the same as:
Definition NAME := fix NAME ARGS+ : RETURN TYPE := EXPRESSION.
Fixpoint NAME ARGS+ : RETURN TYPE := EXPRESSION.
Definition NAME := fix NAME ARGS+ : RETURN TYPE := EXPRESSION.
Exercise: 2 stars, standard (half)
Define a function half : nat → nat that divides a number by two, rounding down.
Fixpoint half (n:nat) : nat (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Compute (half 4). (* ==> 2 *)
Compute (half 9). (* ==> 4 *)
☐
Compute (half 4). (* ==> 2 *)
Compute (half 9). (* ==> 4 *)
☐
Exercise: 2 stars, standard (third)
Define a function third : nat → nat that divides a number by three, rounding down.
Fixpoint third (n:nat) : nat (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Compute (third 4). (* ==> 1 *)
Compute (third 9). (* ==> 3 *)
☐
Compute (third 4). (* ==> 1 *)
Compute (third 9). (* ==> 3 *)
☐
Case study: binary and trinary numbers
Exercise: 3 stars, standard (binary)
Consider a different, more efficient representation of natural numbers using a binary rather than unary system. That is, instead of saying that each natural number is either zero or the successor of a natural number, we can say that each binary number is either- zero,
- twice a binary number, or
- one more than twice a binary number.
Inductive bin : Type :=
| BZ (* zero *)
| T2 (n : bin) (* twice n *)
| T2P1 (n : bin). (* twice n, plus one *)
| BZ (* zero *)
| T2 (n : bin) (* twice n *)
| T2P1 (n : bin). (* twice n, plus one *)
How does this work? Let's compare some binary and unary
numbers. Zero is easy:
One isn't so bad either. To get 1 in unary, just add an S. To
get it in binary, well, what could we do? If we simply enumerate
possibilities, the next up after BZ itself are T2 BZ and
T2P1.
T2 BZ is "twice BZ", i.e., "twice zero", i.e. "zero". Not what
we want.
T2P1 BZ is "twice BZ plus one", i.e., "zero plus one", i.e.,
"one". Perfect!
For the number two, the nats do the same thing: just add an S.
Noting that 2 = 2 * 1, we have our answer for binary, too.
Let's do three.
Let's skip a few. What about the number nine?
Definition u_nine : nat := S (S (S (S (S (S (S (S (S O)))))))).
Definition b_nine : bin := T2P1 (T2 (T2 (T2P1 BZ))).
Definition b_nine : bin := T2P1 (T2 (T2 (T2P1 BZ))).
Eleven?
Definition u_eleven : nat := S (S (S (S (S (S (S (S (S (S (S O)))))))))).
Definition b_eleven : bin := T2P1 (T2P1 (T2 (T2P1 BZ))).
Definition b_eleven : bin := T2P1 (T2P1 (T2 (T2P1 BZ))).
You may be wondering... what do T2 and T2P1 and BZ have to
do with, you know, binary? 0s and 1s?
To see, take a binary number and working from BZ out, write 1
for T2P1 and then 0 for T2.
These are indeed the binary numbers!
(a) First, write an increment function incr for binary numbers,
and a function bin_to_nat to convert binary numbers to unary
numbers.
(b) Write five unit tests for your increment and binary-to-unary
functions. (A "unit test" in Coq is just a Compute that you can
quickly check.) Notice that incrementing a binary number and then
converting it to unary should yield the same result as first
converting it to unary and then incrementing. You only need to
write five tests total, but please be certain to test both
functions.
- b_one: 1
- b_two: 10
- b_three: 11
- b_nine: 1001
- b_eleven: 1011
(* FILL IN HERE *)
(* Do not modify the following line: *)
Definition manual_grade_for_binary : option (nat×string) := None.
☐
(* Do not modify the following line: *)
Definition manual_grade_for_binary : option (nat×string) := None.
☐
Exercise: 2 stars, standard (nat_to_bin)
(* FILL IN HERE *)
(* Do not modify the following line: *)
Definition manual_grade_for_nat_to_bin : option (nat×string) := None.
☐
(* Do not modify the following line: *)
Definition manual_grade_for_nat_to_bin : option (nat×string) := None.
☐
(* Answer to (b): 0 has many representations: it can be written
BZ, T2 BZ, T2 T2 BZ, and so on.
For these alternate representations if you do bin_to_nat
then nat_to_bin, you don't get back what you started with.
(Any other number also has many representations, after applying
constructors to the multiple representations of zero.) *)
BZ, T2 BZ, T2 T2 BZ, and so on.
For these alternate representations if you do bin_to_nat
then nat_to_bin, you don't get back what you started with.
(Any other number also has many representations, after applying
constructors to the multiple representations of zero.) *)
(* FILL IN HERE *)
(* Do not modify the following line: *)
Definition manual_grade_for_normalize : option (nat×string) := None.
☐
(* Do not modify the following line: *)
Definition manual_grade_for_normalize : option (nat×string) := None.
☐
Exercise: 3 stars, standard, optional (trinary)
We saw above how to write a type definition for binary numbers. Now write one to represent trinary numbers, i.e., numbers made up of the digits 0, 1, and 2. Be careful to use fresh names (O and S and BZ and T2 and T2P1 are all taken!).
(* FILL IN HERE *)
Define a function trin_to_nat to convert a trinary number to a unary nat.
(* FILL IN HERE *)
For extra glory (but no credit), write nat_to_trin. You'll need
some helper functions!
(* Do not modify the following line: *)
Definition manual_grade_for_trinary : option (nat×string) := None.
☐
Definition manual_grade_for_trinary : option (nat×string) := None.
☐
What's happening here?
(* 2021-09-28 15:37 *)