very much a beginner, working through Software Foundations in self-study. This question is about the very first part of Logical Foundations, the last part of the Basics chapter.
This assignment is about unary/binary numbers. The idea is to create a Fixpoint function to convert from binary to unary numbers. I am not sure how much I should show of my attempt, since one is not supposed to share solutions. Please let me know if I should delete something.
There is a given type bin (for binary numbers):
Inductive bin : Type :=
| Z
| B0 (n : bin)
| B1 (n : bin).
and this is my effort to convert bin to natural numbers:
Fixpoint bin_to_nat (m:bin) : nat :=
match m with
| Z => O
| B0 (n) => 2 * (bin_to_nat (n))
| B1 (n) => 1 + (bin_to_nat (B0 (n)))
end.
There seems to be a problem with the recursive call in the third branch. I get this error:
Recursive definition of bin_to_nat is ill-formed.
In environment
bin_to_nat : bin → nat
m : bin
n : bin
Recursive call to bin_to_nat has principal argument equal to
“B0 n” instead of “n”.
Recursive definition is:
“fun m : bin =>
match m with
| Z => 0
| B0 n => 2 * bin_to_nat n
| B1 n => 1 + bin_to_nat (B0 n)
end”.
bin_to_nat needs an argument of type bin. n is of type bin. I would think that B0 (n) is also of type bin. What am I missing that bin_to_nat cannot receive B0 (n) as an argument?
That is not enough, the recursion is on the structure of an inductive term, here m, and the recursive call is required to be on a term that is strictly smaller than m, which, given that inductive types (in Coq) are well-founded, guarantees termination.
So, in this case, the term structurally smaller than m is n, and the recursive call must be bin_to_nat n. While the error you get is due to the fact that B0 n in bin_to_nat (B0 n) is not strictly smaller than m.
So, you’ll have to rewrite that 1 + (bin_to_nat (B0 n)) in terms of bin_to_nat n together with only nat numbers and operations. And here is a hint: consider that B0 n, i.e. informally “prepending a 0 to the left of n”, amounts to 2*n (i.e. the encoding is binary little-endian), similarly B1 n amounts to 2*n+1…
you both have been very very helpful, thanks so much. I did not know that recursive calls must each separately be on a strictly smaller term, and I did not understand from the error message that that was the problem.
And, yes, I also figured out how to solve it along the hints given Thanks very much!
Now I am not sure if all recursive functions can be written such that each separate branch is on a smaller term. I wrote a version where the function as a whole will always move to smaller terms, even if the third branch is a recursive call to a term of identical length (because that call is guaranteed to become smaller in the next iteration). This function could be rewritten such that each recursive call is on a smaller term (thanks for the hint how!). But is such rewriting always possible for any recursive function? I am not even sure how to go about proving that that is always possible
No. Not all computable functions can be written in Coq. In particular, the normalization function for Coq terms is computable but can not be written in Coq. But for most other functions, you can usually encode them in Coq. There are some more advanced ways of making non-structurally-recursive functions work, as long as you can prove termination within Coq.
I did not know that recursive calls must each separately be on a strictly smaller term
Any recursive call must be on a smaller term, this is not just true in the context of pattern matching. (Pattern matching rather adds its own requirement for totality: that it is exhaustive, i.e. covers all possible cases.)
But is such rewriting always possible for any recursive function? I am not even sure how to go about proving that that is always possible
It is not about “possible”, this is the only way a function can be written (in Coq: there may be slightly different solutions to function totality in other languages). Indeed, in this context, strictly speaking, the function you wrote is not a function at all (it’s “ill-formed”).
A bit informally, just to give you some more concrete idea:
Should Coq be smart enough to “see” that your function as initially written is bound to eventually terminate? It cannot: whether the function terminates depends on what you are writing in the function itself, and it is a famous theorem that there is no (general) way to compute whether an arbitrary function terminates…
There is in fact also the possibility of writing a recursion based on a custom “guard” or “measure”, there are in fact several ways to achieve that, but this is a more advanced scenario that I suppose you will encounter later in the course: and it is not only overkill in this case, but also does not change the general rule that there must be some computable value (a “measure”) that is bounded below and strictly decreasing at each iteration.
(E.g. B1 n to B0 n would not work unless the strictly decreasing “measure” is the corresponding value as a natural number: except that bin_to_nat is exactly what you are writing, so that looks like a dead end anyway…)
Thanks very much!