The Coq mailing list

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

Hi,

nothing magical. If hs-to-coq manages to handle the syntax, it would
output the same or similar Coq and run into the same problems.

Cheers,
Joachim

Am Donnerstag, den 26.04.2018, 11:48 -0400 schrieb Li-yao Xia:
> 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/>
> > > > 
> 
> 
-- 
Joachim Breitner
  
mail AT joachim-breitner.de
  http://www.joachim-breitner.de/

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