Warning
Your handin should be uploaded as a group on Canvas, i.e., not, repeat, not as an individual, so that all the members of the group get a recorded grade on Canvas, not only the individual who submitted.
Here is the way to go.
First of all, you should be able to access the user page and the group page of the CS3234 page on Canvas.
Here are the steps to follow:
This is a mechanism, not a solution.
If you forgot to join a group on Canvas and the handin is already submitted, just join the group, add a comment to the effect that you have now joined the group and the handin is the same, and resubmit.
If you forgot to join a group on Canvas and the handin is already graded, just join the group, add a comment to the effect that you have now joined the group and the handin is the same, and resubmit. The lecturer will give the handin the same grade, and everybody in the group, including you, will have this grade.
Please spend the weekly time allocated for LPP to solve as many of the following exercises as you can:
You are expected to produce at least two files:
The report should contain:
The introduction should situate the weekly assignment in the trajectory of the semester, and outline its significance.
The conclusion should put the weekly assignment into perspective.
In the long run,
Quotes that support your discourse are welcome.
Of course the report should be spell checked.
For the rest, the report should be precise and as concise as time allows.
As a guideline, write what the future version of you will want to read.
Ostensibly, the learning goal of these exercises is to become familiar with the notation and use of Gallina. In actuality, their lasting value is to become mindful of the way each function is defined and of the way the computation takes place. The rest of this note articulates this point in a conversational, interludic form.
Anton: Hi Mimer. To increment the value of e, we can just write e + 1, can’t we? That seems like the simplest thing to do.
Mimer: Hi Anton. Yes, writing e + 1 looks simple, but + is syntactic sugar for plus (which itself an alias for Nat.add), and plus is defined by structural recursion over its first argument. So any reasoning about e + 1 will involve an induction over e, which might be arbitrarily complicated. Or it will require using the property that plus is commutative, which is indirect.
Alfrothul: Hi Mimer. Should we write 1 + e then? That should work too.
Mimer: Hi Alfrothul. Writing 1 + e is indeed better than writing e + 1 since plus is defined by structural recursion over its first argument. So reasoning about 1 + e will only require two successive unfoldings of the call to plus: one to obtain S (plus 0 e) and one to obtain S e, which is the simplest form to reason with.
Dana: Hi Mimer. So should we write S e instead?
Mimer: Hi Dana. Writing S e is best because it requires no proof steps to reason about this expression. It corresponds to constructing a value (which requires no computational steps) rather than specifying a computation (which requires computational steps). This form is best both in terms of proof steps and in terms of computational steps. That is why it is used in the definition of length_v0.
Anton: Should we write e - 1? That seems logical enough.
Mimer: Well, - does not decrement anything if e evaluates to 0, so there is that. Also, how exactly is - defined?
Alfrothul: Should we write pred e then? I saw it done somewhere on the web, so surely that should be OK?
Mimer: Well, besides the fact that it hasn’t been introduced in the lecture notes, the same issue occurs when e evaluates to 0. Also, how exactly is pred defined? Because we will have to deal with that when reasoning about pred e.
Dana: So what should we do?
Mimer: Test e with a match-expression.
Dana: Oh. And then we would reason by case.
Mimer: Exactly.
Anton: This one is simple, we just use a match-expression with 3 branches. But you need to tweak the definition a bit so that it is accepted:
Fixpoint fib_v0 (n : nat) : nat :=
match n with
0 => 0
| 1 => 1
| S n' => fib_v0 n' + fib_v0 (n' - 1)
end.
Alfrothul: Huh, the man said something about using subtraction? Personally I used pred:
Fixpoint fib_v1 (n : nat) : nat :=
match n with
0 => 0
| 1 => 1
| S n' => fib_v1 n' + fib_v1 (pred n')
end.
Dana: Well, we know that n' cannot be 0 because of the second clause, so I started writing the following definition, but I got stuck for the first recursive call:
Fixpoint fib_v2 (n : nat) : nat :=
match n with
0 => 0
| 1 => 1
| S (S n'') => fib_v2 ??? + fib_v2 n''
end.
Mimer: That is because you are trying to go faster than the music. Go one step at a time, the way you will do it in the proof:
Fixpoint fib_v3 (n : nat) : nat :=
match n with
0 => 0
| S n' => match n' with
0 => 1
| S n'' => fib_v3 n' + fib_v3 n''
end
end.
Anton: I saw a cool way to do it on the web – by matching two values at a time:
Definition min_v1 (m n : nat) : nat :=
let fix visit (i j : nat) : nat :=
match i, j with
O, O =>
m
| O, S j' =>
m
| S i', O =>
n
| S i', S j' =>
visit i' j'
end
in visit m n.
Pablito: Wait – how does this implementation work?
Na-bong: Let’s see. Say that min_v1 is called with 2 and 3. Then this call reduces to the call visit 2 3 in a scope where m denotes 2 and n denotes 3. The call visit 2 3 reduces to the call visit 1 2, the call visit 1 2 reduces to the call visit 0 1, and the call visit 0 1 reduces to m, which denotes 2. OK. So the initial call to visit iteratively decrements its two arguments until one of them reaches 0. The first one that does is the smallest.
Anton (proudly): See how min_v1 is both lambda-dropped and tail recursive? It is lambda-dropped because the block declaring visit is scope sensitive since it refers to m and n, and it is tail recursive because all the calls to visit are tail calls. Lambda-lifting this implementation would give rise to a tail-recursive auxiliary function with four arguments.
Dana: Right. Still, I think that for now we should go with the music and write:
Definition min_v2 (m n : nat) : nat :=
let fix visit (i j : nat) : nat :=
match i with
O =>
m
| S i' =>
match j with
O =>
n
| S j' =>
visit i' j'
end
end
in visit m n.
Anton: So you are only matching one value at a time. But that’s equivalent, right?
Mimer: Yes it is. What matters here is that the definition of min_v2 makes it more clear that visit is defined by structural recursion over its first argument and by case on its second. Down the road, when we reason about it, it will be by structural induction over its first argument and by case on its second, a fruitful alignment.
Alfrothul: The second definition is simpler too, since in the O case for i, there is no need to test j.
Halcyon: On another note, why are min_v1 and min_v2 defined with Definition instead of with Fixpoint? Because that works too.
Mimer: Because they are not recursive. Only recursive functions should be defined with Fixpoint, and that will affect the way we reason about them. The more precisely our programs are written, the simpler it will be to reason about them.
Alfrothul: Here is the definition I had in mind:
Fixpoint min_v3 (m n : nat) : nat :=
match m with
0 =>
0
| S m' =>
match n with
0 =>
0
| S n' =>
S (min_v3 m' n')
end
end.
Alfrothul: It is lambda-lifted rather than lambda-dropped, and it is recursive rather than tail recursive, but otherwise it is simpler, right?
Mimer: Well it has a simpler invariant.
Pablito: Invariant?
Mimer: Characteristic property. This property is that for all integers m and n denoted by m and n, evaluating min_v3 m n yields the smallest of m and n. The invariant in the definition of min_v2 is less simple to write.
Anton: True that. Let me amend min_v2:
Definition min_v2' (m n : nat) : nat :=
let fix visit (i j : nat) : bool :=
match i with
O =>
true
| S i' =>
match j with
O =>
false
| S j' =>
visit i' j'
end
end
in if visit m n
then m
else n.
Pablito: Come again?
Anton: The invariant of visit is that forall integers i and j denoted by i and j, evaluating visit i j yields true if i is smaller than j, and false otherwise. So all we need to do with the initial call is to test it, which I wrote using an if-expression, which is syntactic sugar for:
match visit m n with
true =>
m
| false =>
n
end
Anton: Also, lambda-lifting this implementation would give rise to a tail-recursive auxiliary function with only two arguments.
Mimer: Cool. Do you think your definitions are all equivalent?
Anton: You tell us.
Mimer: Actually I won’t, but soon you will prove whether they are.
Dana: Hum. What does it mean to be equivalent?
Mimer: Now we’re getting somewhere.
Dana: Well, these definitions are definitions of functions, and functions are equal if they yield the same output when applied to the same input.
Mimer: Yes.
Dana: So here, min_v2 and min_v3 are equivalent if the two functions they denote are equal, i.e., if they yield the same number when applied to two numbers.
Mimer: Yes. Doing good, Dana!
Dana: Thank you.
Added the warning about submitting handins as a group, not as an individual, on Canvas [25 Jan 2024]
Rewrote the Interlude about implementing a function that returns the smallest of two natural numbers [21 Jan 2024]
Added the exercises [20 Jan 2024]
Created [18 Jan 2024]