The Coq mailing list

[Joachim Breitner <mail AT joachim-breitner.de>]

…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/>
> > 
-- 
Joachim Breitner
  
mail AT joachim-breitner.de
  http://www.joachim-breitner.de/

Attachment: signature.asc
Description: This is a digitally signed message part