The Coq mailing list

[roconnor AT theorem.ca]

To follow up on this thread, I have devised a "solution" to memoizing a 
structurally recursive function on binary trees.  However, it isn't 
pretty.

You can find my code MemoOrdBinTree.v @ 
<https://gist.github.com/roconnor/286d0f21af36c2e97e74338f10a4315b>

The construction in Coq is made more difficult (than in Agda, for example) 
due to Coq's positivity condition not accepting "Bushy Datatypes" (see 
<https://www.cs.ox.ac.uk/richard.bird/online/BirdMeertens98Nested.pdf>). 
I created a coinductive datatype based on Catalan's triangle for holding 
computed results 
<https://gist.github.com/roconnor/286d0f21af36c2e97e74338f10a4315b#file-memoordbintree-v-L111>. 
It bears some resemblance to Saizan's Agda code @ 
https://cstheory.stackexchange.com/a/40645 whereby the binary tree input 
is first preprocessed by decorating it with size information.  In my case 
the size of a binary tree is the number of internal (non-leaf) nodes of 
the tree.

After counting the number of internal nodes, the lookup function reaches 
that far into a coinductive stream of these Catalan-shaped containers 
<https://gist.github.com/roconnor/286d0f21af36c2e97e74338f10a4315b#file-memoordbintree-v-L252> 
to pick out the appropriate container that memoizes inputs of that size. 
Then it will traverse that container to find the location that holds the 
value for the particularly shaped tree of that size.

The sharing across recursive calls happen because a let statement 
<https://gist.github.com/roconnor/286d0f21af36c2e97e74338f10a4315b#file-memoordbintree-v-L271> 
shares an inductive list of all recursive values of smaller sized trees 
when generating the coinductive stream all all results.

This all seems to "work".  For some example tests 
<https://gist.github.com/roconnor/286d0f21af36c2e97e74338f10a4315b#file-memoordbintree-v-L380-L383>

    Time Eval vm_compute in (memoFoldOp (fullTree 9)).
    Time Eval vm_compute in (memoFoldOp (fullTree 8)).
    Time Eval vm_compute in (memoFoldOp (fullTree 9)).
    Time Eval vm_compute in (memoFoldOp (fullTree 8)).

the second call to (memoFoldOp (fullTree 9)) takes less time than the 
first call, while both calls to (memoFoldOp (fullTree 8)) take the same 
time, indicating the result for (memoFoldOp (fullTree 8)) was cached 
during the computation of (memoFoldOp (fullTree 9)).

Compare this to the non-recursively memoization of MemoBinTree.v @ 
<https://gist.github.com/roconnor/52375c3a81c927c5a8234be858f9830b#file-memobintree-v-L126-L129>

    Time Eval vm_compute in memoFoldOp (fullTree 12).
    Time Eval vm_compute in memoFoldOp (fullTree 11).
    Time Eval vm_compute in memoFoldOp (fullTree 12).
    Time Eval vm_compute in memoFoldOp (fullTree 11).

where the first call to (memoFoldOp (fullTree 11)) also take longer to 
evaluate because there is no sharing of results from the previous call to 
(memoFoldOp (fullTree 12)).

However, my recursive memoization solution is awful, as you may have 
guessed by the relative sizes of the example inputs between the recursive 
and non-recursive memoization functions.  My recursive memoization 
computation and lookup has so much overhead in it that it probably isn't 
practically beneficial over the non-recursive memoization.  The code uses 
function-definition-by-tactic throughout, which is never a good sign in a 
Coq development.  I suspect there are lots of places where there is 
quadratic time-complexity of evaluating arithmetic equalities down to 
refl_equal, which need to be transparent for the elimination of eq_rect 
statements used to align the dependent types used.  Perhaps with some care 
these can be reduced to linear-time complexity, but perhaps that isn't 
possible with this design.  Perhaps the recursive and non-recursive 
solutions can be composed where the non-recursive solution memoizes the 
expensive recursive computations, while the non-recursive solution 
memoizes the expensive lookup of the recursive memoization.

Overall, I think my solution is much too complex to be useful, and I'm 
hope that there is some better way to solve this.  With the non-recursive 
solution, the coinductive structure is simply traversed in accordance to 
the input tree shape, which is relatively elegant compared to my recursive 
solution involving computing sizes of trees and looking it up in a 
linearized coinductive stream of results.

The lazy Haskell solution works so well, that I'm still hoping that there 
is some way to capture the same operational qualities of it in a 
dependently typed language.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''