Alfrothul: So two functions are equivalent if applying them to the same argument gives the same result.
Anton: Right. I remember the section about functional equality in Week 03.
Alfrothul: And two expressions e1 and e2 are observationally equivalent if we cannot determine which one was evaluated when evaluating either of them in the same environment.
Anton: Right. For example, 0 + 1 + 2 + 3 + 4 + 5 and 5 * (5 + 1) / 2 are observationally equivalent.
Pablito (precise): To 15.
Alfrothul: Yes. And more generally, if n denotes a non-negative integer, summatorial n and n * (n + 1) / 2 are also observationally equivalent.
Anton: OK, I remember the summatorial function in Week 06.
Alfrothul: For another example, if an expression represents a polynomial expressed in the standard form and if another expression represents the same polynomial in Horner form, these two expressions are observationally equivalent.
Anton: Right. For example, 9 * power x 3 + 8 * power x 2 + 7 * power x 1 + 6 and ((9 * x + 8) * x + 7) * x + 6 are observationally equivalent. I remember Exercise 16 in Week 04.
Pablito: And I also remember Exercise 21 where we debugged the power function in Week 05.
Alfrothul: Good. Now do you remember the post-rationalization in Week 03 that functions are parameterized expressions?
Anton: I do. That was our first introduction to functional abstraction as a thing. What’s your point?
Alfrothul: My point is that if we functionally abstract two expressions that are observationally equivalent, what do we get?
Anton: Two functions?
Alfrothul: Not just two functions, Anton, not just two functions. We get two functions that, when applied to an argument, will give rise to evaluating two observationally equivalent expressions in the same environment.
Anton: Oh. Then these two functions will return the same result.
Alfrothul: Yup.
Anton: Aha. So that’s why we could test fun x -> 9 * power x 3 + 8 * power x 2 + 7 * power x 1 + 6 and fun x -> ((9 * x + 8) * x + 7) * x + 6 in Exercise 16, back in Week 04.
Dana: And likewise for summatorial and fun n -> n * (n + 1) / 2, in Week 06.
Alfrothul: Yes. These OCaml functions are equivalent because their bodies are observationally equivalent.
Anton: Hum. That seems awfully relevant for the mini-project about cracking polynomial functions.
Alfrothul: You think?
Created [18 Sep 2022]