The StreamMemo library for Coq illustrates how to memoize a function
f : nat -> A over the natural numbers. In particular when
f (S n) = g (f n), the
imemo_make shares the computation of recursive calls.
Suppose instead of natural numbers, we want to memoize recursive functions over binary trees:
Inductive binTree : Set :=
| Leaf : binTree
| Branch : binTree -> binTree -> binTree.
Suppose we have a function
f : binTree -> A that is structurally recursive, meaning that there is a function
g : A -> A -> A such that
f (Branch x y) = g (f x) (f y). How do we build a similar memo table for
f in Coq such that the recursive computations are shared?
In Haskell, it is not too hard to build such a memo table (see MemoTrie for example) and tie-the-knot. Clearly such memo tables are productive. How can we arrange things to convince a dependently typed language to accept such knot tying is productive?
Although I've specified the problem in Coq, I wouldd be happy with an answer in Agda or any other dependently typed language as well.