Alfrothul: That’s funny...Halcyon: Quoting Asimov, are we?Isaac Asimov: Which is not a bad idea per se, is it?Mimer: Prof. Asimov, thanks for coming by!Halcyon: Huh, would you mind autographing my copy of “The relativity of wrong”?Isaac Asimov: Sure. I’m not the Beatles, though.Peter Landin: That’s what I told them too.
Alfrothul: Actually...
Anton: Yes?
Alfrothul: ...
Dana: Yes?
Alfrothul: Hmmmm:
let list_powermap_1_succ ns_given =
let rec visit ns =
match ns with
| [] ->
[]
| n :: ns' ->
succ n :: visit ns' (* visit is applied 1 time *)
in visit ns_given;;
Anton: Yes?
Pablito (diligent): It’s an instance of List.map. Like, if it applied to a list of 0’s, it yields a list of 1’s:
let () = assert (list_powermap_1_succ [0; 0; 0; 0; 0; 0; 0; 0; 0; 0] = [1; 1; 1; 1; 1; 1; 1; 1; 1; 1]);;
Anton: Yes.
Pablito: And we can easily generalize this test:
let () = assert (let n = Random.int 10
in list_powermap_1_succ (List.init n (fun i -> 0)) = List.init n (fun i -> 1));;
Alfrothul: Actually, what if we didn’t apply visit at all?
Anton (o_O): Not apply visit at all.
Alfrothul: Well, yes:
let list_powermap_0_succ ns_given =
let rec visit ns =
match ns with
| [] ->
[]
| n :: ns' ->
succ n :: ns' (* visit is applied 0 times *)
in visit ns_given;;
Anton: Ah, you mean that we could apply it 0 times. Well, why not twice, for that matter:
let list_powermap_2_succ ns_given =
let rec visit ns =
match ns with
| [] ->
[]
| n :: ns' ->
succ n :: visit (visit ns') (* visit is applied 2 times *)
in visit ns_given;;
Dana (playfully): Or thrice, while we are at it:
let list_powermap_3_succ ns_given =
let rec visit ns =
match ns with
| [] ->
[]
| n :: ns' ->
succ n :: visit (visit (visit ns')) (* visit is applied 3 times *)
in visit ns_given;;
Mimer: Er... Grasshoppers? You are departing from structural recursion here. Do your functions terminate?
Alfrothul: Well, list_powermap_1_succ does, since it is structurally recursive on the given list, and lists are finite.
Pablito: And list_powermap_0_succ does too since its visit function is not even recursive.
Halcyon: In FPP, there is a saying – beware of induction proofs that do not use their induction hypothesis, for they are proofs by case in disguise.
Dana: Wow, Halcyon.
Halcyon (with dignity): Well, I read.
Anton: And what does that mean here?
Halcyon: I am still working on the part where programming is proving and proving is programming, but somehow the saying seemed relevant here.
Alfrothul: And it is, since in a structurally recursive function, the recursive calls implement the induction hypotheses.
Dana: Right: in the definition of list_powermap_0_succ, visit can be declared with a let instead of with a let rec, and indeed it has two cases. It maps an empty list of integers to the empty list, and a nonempty list of integers to a nonempty list with the same tail and with the head, incremented.
Halcyon: So it is defined by cases.
Alfrothul: And the saying applies – beware of recursive functions that make no recursive calls, for they are non-recursive functions in disguise.
Anton: Which doesn’t sound as spiffy. How about: beware of recursive functions that make no recursive calls, for they are conditional functions in disguise. Naah. Non-recursive conditional functions? Conditional non-recursive functions?
Dana: Beware of recursive functions that make no recursive calls, for they are merely defined by cases? Either way, the saying was relevant, so thanks, Halcyon.
Halcyon: Well, it did seem relevant.
Dana: As to whether list_powermap_2_succ and list_powermap_3_succ terminate, they should, since they preserve the length of their input list.
Mimer: Good enough.
Pablito: Easy does it.
Implement the simple characterization of Task 1 as a simple and telling unit test (one unit test for list_powermap_0_succ, one unit test for list_powermap_2_succ, one unit test for list_powermap_3_succ, and one unit test for list_powermap_4_succ), still sticking to Pablito’s constant list of 0’s as input.
Mutatis mutandis, implement a list_powermap_5_succ function where visit is applied 5 times, implement the corresponding simple and telling unit test, and verify that your implementation passes your unit test.
Generalize the simple characterization of Task 1 when the input is not a constant list of 0’s but a constant list of any given integer, e.g.,
Implement the corresponding generalized unit test.
Generalize further the generalization of Task 4 when the input is not a constant list of any given integer but any arbitrary list. For example, given any deterministic OCaml function g : int -> int (i.e., a function that doesn’t involve the Random library), such a list could be obtained using List.init. To wit:
# List.init 5 succ;;
- : int list = [1; 2; 3; 4; 5]
# List.init 10 pred;;
- : int list = [-1; 0; 1; 2; 3; 4; 5; 6; 7; 8]
# List.init 15 (fun i -> i * i);;
- : int list = [0; 1; 4; 9; 16; 25; 36; 49; 64; 81; 100; 121; 144; 169; 196]
#
Implement the corresponding generalized generalized unit test.
Generalize the list_powermap functions into one function that is parameterized by the function to map, so that, for any given ns : int list,
(N.B.: The resulting functions are polymorphic.)
Verify that the resulting functions still pass the previous unit tests, and design some new unit tests.
As in La même chose, with a little help from OCaml from Week 05 for the factorial function, parameterize the series of definitions from Task 6 (namely list_powermap_0 and friends) with the index and conflate it into one single definition, i.e., implement a function list_powermap that is such that, for any given function f : 'a -> 'a and any vs : 'a list,
Verify that the resulting function still passes the previous unit tests, and design some new unit tests.
At the end of the day, what is the power of list_powermap (and of nested recursive calls)?
Loki (to himself): High time for a powernap.
Created [14 Oct 2022]