Suppose both k and f are functions of type int -> int. If we know k(l-1)=f(l) holds for all l of type int, can we be certain that k is the function v->f(v+1) ?
I have this question while doing an exercise of functional programming: to transform a length function
let rec len xs =
match xs with
| [] -> 0
| x:xr -> 1 + len xr;;
to a continuation-passing version. My answer to the exercise would be
let rec lenc xs k =
match xs with
| [] -> k 0
| x:xr -> lenc xr (fun v -> k(v+1))
but I am unsure if the (fun v -> k(v+1)) part can be replaced by other solutions. To know this, we would need to determine a unique "k", given that k(l-1)=f(l) holds for all function f of type int->int and l of type int?
Do you want mathematical proof?
(1) k(i - 1) = f(i)
(2) j = i - 1
from (1) & (2):
(3) k(j) = f(i)
from (2):
(4) i = j + 1
from (3) & (4)
(5) k(j) = f(j + 1)
q.e.d.
Of course (fun v -> k(v+1)) is your k and the inside k is f