The Coq mailing list

[roconnor AT theorem.ca]

I've posted this question on the cstheory stack exchange at 
https://cstheory.stackexchange.com/questions/40631/how-can-you-build-a-coinductive-memoization-table-for-recursive-functions-over-b
but I'm hoping to reach a wider audience by also asking here on the Coq Club 
mailing list.  I copy my question below.

----

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?

----

Even building a memotrie data type for binary trees is difficult in Coq. The 
natural solution calls for using a Bushy Datatype (see 
https://www.cs.ox.ac.uk/richard.bird/online/BirdMeertens98Nested.pdf) which 
doesn't pass Coq's positivity check (but does seem to pass Agda's positivity 
check; maybe Christine Paulin could even further relax Coq's positivity check. 
:) ).  At the risk of prejudicing the reader, I have a gist of how I've worked 
around this to define a memotrie data type for binary trees in Coq at 
https://gist.github.com/roconnor/52375c3a81c927c5a8234be858f9830b

My above solution to building a memotrie is moderately contrived and adhoc, so 
I encourage those intrested in this problem to try a solution themselves first 
before reading my gist.  You may come up with a better solution than what I 
have.

The memotrie I build in my gist doesn't memoize recursive calls of a 
structurally recursive function over binary trees. At the end I write out the 
type of solution one would write in Haskell to build an example memotrie that 
memoizes recurive calls.  However, this definition fails that corecursive guard 
check (and rightly so I think).

I don't know how to build a memotrie to memoize recursive calls in a 
structurally recursive function.  I'm hoping someone one the mailing list might 
know a solution.

--
Russell O'Connor                                      <http://r6.ca/>