cs3110 / textbook

The CS 3110 Textbook, "OCaml Programming: Correct + Efficient + Beautiful"
Other
740 stars 134 forks source link

Remove one case of `expsq` #127

Closed favonia closed 1 year ago

favonia commented 1 year ago

We do not need a separate case for n = 1. This will also make it easier for students to prove things. :slightly_smiling_face:

clarksmr commented 1 year ago

Sorry that I haven't had a chance to reply to this yet.

@favonia @dexter-kozen If this change is accepted, the solutions repo would also need to be updated.

However, by accepting it we lose our only example of a proof with multiple base cases.

I would prefer that we keep the problem as initially stated, then state a variant follow-up problem that says "suppose you remove the n=1 case." That way we can satisfy all concerns.

clarksmr commented 1 year ago

8818386 resolves this to my satisfaction. It preserves the original exercise (thus keeping the solutions repo in synch with the textbook) while providing the version of the exercise that was proposed (which currently has no solution, but that's ok — we don't promise solutions to every exercise).

favonia commented 1 year ago

However, by accepting it we lose our only example of a proof with multiple base cases.

@clarksmr Thank you for your consideration, but the above assessment might not be completely accurate. Unless I missed something, the proof is still easier with two base cases because the calculation for n = 2k+1 implicitly assumes k > 0. The simplification is not as significant as deleting one base case, in case I set the expectation too high 😅