<p>It's easy enough to get the recursion pattern to work with sized types.
Hopefully the sharing is preserved through compilation![1]</p>

<pre><code>module _ where

open import Size
open import Data.Nat

data BT (i : Size) : Set where
  Leaf : BT i
  Branch : ∀ {j : Size&lt; i} → BT j → BT j → BT i

record Memo (A : Set) (i : Size) : Set where
  coinductive
  field
    leaf : A
    branch : ∀ {j : Size&lt; i} → Memo (Memo A j) j

open Memo

trie : ∀ {i} {A} → (BT i → A) → Memo A i
trie f .leaf = f Leaf
trie f .branch = trie (\ l → trie \ r → f (Branch l r))

untrie : ∀ {i A} → Memo A i → BT i → A
untrie m Leaf         = m .leaf
untrie m (Branch l r) = untrie (untrie (m .branch) l) r

memo : ∀ {i A} → (BT i → A) → BT i → A
memo f = untrie (trie f)

memoFix : ∀ {A : Set} → A → (A → A → A) → ∀ {i} → BT i → A
memoFix {A} lf br = go
 where
  go h : ∀ {i} → BT i → A
  go = memo h
  h Leaf = lf
  h (Branch l r) = br (go l) (go r)
</code></pre>

<p>[1] <a href="https://github.com/agda/agda/issues/2918" rel="nofollow noreferrer">https://github.com/agda/agda/issues/2918</a></p>

CC BY-SA 3.0
2018-04-23T23:51:20.110Z
Thanks for this. I have two worries about this code.

Firstly the `go` value is a function of a Size parameter.  In general, there is no sharing between independent function calls at the same value.  This can probably be fixed by adding a let statement in the definition of `h (Branch l r)`.

Secondly, the stratified definition of `BT` means that two, otherwise identically shaped trees, will have different values when they occur at different levels.  These distinct values won't be shared in the MemoTrie.
Russell O'Connor
CC BY-SA 3.0
2018-04-23T23:51:58.353Z
I'm impressed that Agda accepts the nested definition of `Memo` in `branch`.  Coq's positivity checker seems to reject this, making things more complicated in Coq.
Russell O'Connor
CC BY-SA 3.0
2018-04-24T08:15:11.897Z
The issue I linked to seems to conclude that the sizes are not a problem at runtime when compiled with the GHC backend, though I haven't verified this myself.
Saizan
CC BY-SA 3.0
2018-04-24T21:22:09.783Z
I see.  I'm looking for a memoization solution that can be used within the proof assistant so it can be used as part of a proof by reflection. Your solution is probably suitable for compilation assuming the `Size` types end up erased.
Russell O'Connor
CC BY-SA 3.0
2018-04-23T13:17:47.443Z
2018-04-23T13:17:47.443Z
Saizan
<p>I have created a "solution" that recursively memoizes structurally recursive functions of binary trees in Coq.  My gist is at <a href="https://gist.github.com/roconnor/286d0f21af36c2e97e74338f10a4315b" rel="nofollow noreferrer">https://gist.github.com/roconnor/286d0f21af36c2e97e74338f10a4315b</a>.</p>

<p>It operates similarly to <a href="https://cstheory.stackexchange.com/a/40645/4122">Saizan's solution</a>, by stratifying binary trees based on a size metric, in my case counting the number of internal nodes of binary trees, and producing a lazy stream of containers of all solutions for a particular size.  Sharing happens because of <a href="https://gist.github.com/roconnor/286d0f21af36c2e97e74338f10a4315b#file-memoordbintree-v-L271" rel="nofollow noreferrer">a let statement</a> in the stream generator that holds the initial part of the stream to be used in later parts of the stream.</p>

<p>Examples show that for <code>vm_compute</code>, evaluating a perfect binary tree with 8 levels after having evaluated a perfect binary tree with 9 levels is much faster than only evaluating a perfect binary tree with 8 levels.</p>

<p>However, I'm hesitant to accept this answer because the overhead of this particular solution is bad that it performs much worse than my <a href="https://gist.github.com/roconnor/52375c3a81c927c5a8234be858f9830b" rel="nofollow noreferrer">memoization without structural recursion</a> for my examples of practical inputs.  Naturally, I want a solution that performs better under reasonable inputs.</p>

<p>I have some further comments at "<a href="https://sympa.inria.fr/sympa/arc/coq-club/2018-05/msg00172.html" rel="nofollow noreferrer">[Coq-Club] How can you build a coinductive memoization table for recursive functions over binary trees?</a>".</p>

CC BY-SA 4.0
2018-05-15T13:54:34.303Z
2018-05-15T13:54:34.303Z
Russell O'Connor
<p>The <a href="https://coq.inria.fr/library/Coq.Lists.StreamMemo.html" rel="noreferrer">StreamMemo</a> library for Coq illustrates how to memoize a function <code>f : nat -&gt; A</code> over the natural numbers.  In particular when <code>f (S n) = g (f n)</code>, the <code>imemo_make</code> shares the computation of recursive calls.</p>

<p>Suppose instead of natural numbers, we want to memoize recursive functions over binary trees:</p>

<p><code>Inductive binTree : Set :=
| Leaf : binTree
| Branch : binTree -&gt; binTree -&gt; binTree.
</code></p>

<p>Suppose we have a function <code>f : binTree -&gt; A</code> that is structurally recursive, meaning that there is a function <code>g : A -&gt; A -&gt; A</code> such that <code>f (Branch x y) = g (f x) (f y)</code>.  How do we build a similar memo table for <code>f</code> in Coq such that the recursive computations are shared?</p>

<p>In Haskell, it is not too hard to build such a memo table (see <a href="https://hackage.haskell.org/package/MemoTrie" rel="noreferrer">MemoTrie</a> 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?</p>

<p>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.</p>

<dependent-type><coq><agda>
How can you build a coinductive memoization table for recursive functions over binary trees?
Russell O'Connor
# How can you build a coinductive memoization table for recursive functions over binary trees?

(Asked by: username_0 on 2018-04-20)

The [StreamMemo](https://coq.inria.fr/library/Coq.Lists.StreamMemo.html) 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](https://hackage.haskell.org/package/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.

**Tags:** dependent-type, coq, agda

---

## 2 answers

### Answer by username_1 on 2018-04-23. Score: 4

It's easy enough to get the recursion pattern to work with sized types.
Hopefully the sharing is preserved through compilation![1]
module _ where

open import Size
open import Data.Nat

data BT (i : Size) : Set where
  Leaf : BT i
  Branch : ∀ {j : Size< i} → BT j → BT j → BT i

record Memo (A : Set) (i : Size) : Set where
  coinductive
  field
    leaf : A
    branch : ∀ {j : Size< i} → Memo (Memo A j) j

open Memo

trie : ∀ {i} {A} → (BT i → A) → Memo A i
trie f .leaf = f Leaf
trie f .branch = trie (\ l → trie \ r → f (Branch l r))

untrie : ∀ {i A} → Memo A i → BT i → A
untrie m Leaf         = m .leaf
untrie m (Branch l r) = untrie (untrie (m .branch) l) r

memo : ∀ {i A} → (BT i → A) → BT i → A
memo f = untrie (trie f)

memoFix : ∀ {A : Set} → A → (A → A → A) → ∀ {i} → BT i → A
memoFix {A} lf br = go
 where
  go h : ∀ {i} → BT i → A
  go = memo h
  h Leaf = lf
  h (Branch l r) = br (go l) (go r)

[1] https://github.com/agda/agda/issues/2918

> **Comments:**
> **username_0**: Thanks for this. I have two worries about this code.  Firstly the `go` value is a function of a Size parameter.  In general, there is no sharing between independent function calls at the same value.  This can probably be fixed by adding a let statement in the definition of `h (Branch l r)`.  Secondly, the stratified definition of `BT` means that two, otherwise identically shaped trees, will have different values when they occur at different levels.  These distinct values won't be shared in the MemoTrie.  
> **username_0**: I'm impressed that Agda accepts the nested definition of `Memo` in `branch`.  Coq's positivity checker seems to reject this, making things more complicated in Coq.  
> **username_1**: The issue I linked to seems to conclude that the sizes are not a problem at runtime when compiled with the GHC backend, though I haven't verified this myself.  
> **username_0**: I see.  I'm looking for a memoization solution that can be used within the proof assistant so it can be used as part of a proof by reflection. Your solution is probably suitable for compilation assuming the `Size` types end up erased.  

---

### Answer by username_0 on 2018-05-15. Score: 0

I have created a "solution" that recursively memoizes structurally recursive functions of binary trees in Coq. My gist is at <https://gist.github.com/roconnor/286d0f21af36c2e97e74338f10a4315b>.

It operates similarly to [Saizan's solution](https://cstheory.stackexchange.com/a/40645/4122), by stratifying binary trees based on a size metric, in my case counting the number of internal nodes of binary trees, and producing a lazy stream of containers of all solutions for a particular size. Sharing happens because of [a let statement](https://gist.github.com/roconnor/286d0f21af36c2e97e74338f10a4315b#file-memoordbintree-v-L271) in the stream generator that holds the initial part of the stream to be used in later parts of the stream.

Examples show that for `vm_compute`, evaluating a perfect binary tree with 8 levels after having evaluated a perfect binary tree with 9 levels is much faster than only evaluating a perfect binary tree with 8 levels.

However, I'm hesitant to accept this answer because the overhead of this particular solution is bad that it performs much worse than my [memoization without structural recursion](https://gist.github.com/roconnor/52375c3a81c927c5a8234be858f9830b) for my examples of practical inputs. Naturally, I want a solution that performs better under reasonable inputs.

I have some further comments at "[[Coq-Club] How can you build a coinductive memoization table for recursive functions over binary trees?](https://sympa.inria.fr/sympa/arc/coq-club/2018-05/msg00172.html)".


---

