The Coq mailing list

[Li-yao Xia <lysxia AT gmail.com>]

What happens if you write Russel's memoOpX at the end in Haskell and run 
hs-to-coq on it?

Li-yao

On 04/26/2018 11:43 AM, Joachim Breitner wrote:
> …but then again, this is not at all addressing the question on how to
> memoize recursive functions, so I guess my response is just noise …
> sorry
>
> Joachim
>
> Am Donnerstag, den 26.04.2018, 11:41 -0400 schrieb Joachim Breitner:
> > Hi,
> >
> > you might enjoy looking at
> > https://github.com/antalsz/hs-to-coq/tree/master/examples/coinduction
> > where I implement such a memo table in Haskell, convert it to Coq using
> > hs-to-coq (the generated file is not in the git repo, so I attached it
> > to this mail), and then in MemoProofs.v show that it preserves the
> > semantics of the memoized functions.
> >
> > The Time commands at the end of this function show that memoization
> > actually works in Coq!
> >
> > Time Eval vm_compute in slowFib 25. (* Finished transaction in 2.248 secs *)
> > Time Eval vm_compute in slowFib 25. (* Finished transaction in 2.233 secs *)
> > Time Eval vm_compute in cachedFib 25. (* Finished transaction in 2.203 secs *)
> > Time Eval vm_compute in cachedFib 25. (* Finished transaction in 0. secs *)
> > Time Eval vm_compute in cachedFib 26. (* Finished transaction in 3.579 secs *)
> > Time Eval vm_compute in cachedFib 26. (* Finished transaction in 0. secs *)
> >
> > Cheers,
> > Joachim
> >
> > Am Mittwoch, den 25.04.2018, 12:11 -0700 schrieb 
> > 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/>