The Coq mailing list

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

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/
(* Default settings (from HsToCoq.Coq.Preamble) *)

Generalizable All Variables.

Unset Implicit Arguments.
Set Maximal Implicit Insertion.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Require Coq.Program.Tactics.
Require Coq.Program.Wf.

(* Preamble *)

Require Coq.NArith.BinNat.
Require Psatz.


(* There is [Coq.NArith.BinNat.N.lt_wf_0], but it is Opauqe, so we cannot
   compute with Program Fixpoint that recurse on [N].
   Until this is fixed (in https://github.com/coq/coq/pull/7060), we
   we reprove this lemma and close it with [Defined].
*)
Require Import Coq.NArith.BinNat.
Theorem N_lt_wf : well_founded N.lt.
Proof.
  assert (well_founded (fun n1 n2 => (N.to_nat n1) < (N.to_nat n2)))
    by (apply Wf_nat.well_founded_ltof).

  intro x.
  specialize (H x).
  induction H.
  constructor.
  intros y Hy.
  apply H0.
  Psatz.lia.
Defined.

Ltac solve_lookupTrie :=
  Coq.Program.Tactics.program_simplify;
  try apply Wf.measure_wf;
  try apply N_lt_wf;
  try match goal with  H : _  = false |- _ => apply Coq.NArith.BinNat.N.eqb_neq in H end;
  apply Coq.NArith.BinNat.N.div_lt;
  Psatz.lia.

Ltac solve_fib := Coq.Program.Tactics.program_simplify;
  try apply N_lt_wf;
  repeat match goal with  H : _ = false |- _ => apply Coq.NArith.BinNat.N.eqb_neq in H end;
  Psatz.lia.

(* Converted imports: *)

Require Coq.NArith.BinNat.
Require Coq.Numbers.BinNums.
Require GHC.Base.
Require GHC.Num.
Require GHC.Real.
Import GHC.Base.Notations.
Import GHC.Num.Notations.

(* Converted type declarations: *)

CoInductive NatTrie a : Type
  := TrieNode : a -> NatTrie a -> NatTrie a -> NatTrie a.

Arguments TrieNode {_} _ _ _.
(* Converted value declarations: *)

Program Fixpoint lookupTrie {a} (arg_0__ : NatTrie a) (arg_1__
                              : Coq.Numbers.BinNums.N) {measure arg_1__ (Coq.NArith.BinNat.N.lt)} : a
                   := match arg_0__, arg_1__ with
                      | TrieNode here div2 minus1div2, n =>
                          if Bool.Sumbool.sumbool_of_bool (n GHC.Base.== #0) then here else
                          if Bool.Sumbool.sumbool_of_bool (GHC.Real.odd n)
                          then lookupTrie minus1div2 (GHC.Real.div n #2) else
                          lookupTrie div2 (GHC.Real.div n #2)
                      end.
Solve Obligations with (solve_lookupTrie).

Definition mkTrie {a} : (Coq.Numbers.BinNums.N -> a) -> NatTrie a :=
  cofix mkTrie f
          := TrieNode (f #0) (mkTrie (f GHC.Base.∘ (fun arg_0__ => arg_0__ GHC.Num.* #2)))
                      (mkTrie (f GHC.Base.∘
                               ((fun arg_1__ => arg_1__ GHC.Num.+ #1) GHC.Base.∘
                                (fun arg_2__ => arg_2__ GHC.Num.* #2)))).

Program Fixpoint slowFib (arg_0__ : Coq.Numbers.BinNums.N)
                         {measure arg_0__ (Coq.NArith.BinNat.N.lt)} : Coq.Numbers.BinNums.N
                   := let 'num_1__ := arg_0__ in
                      if Bool.Sumbool.sumbool_of_bool (num_1__ GHC.Base.== #0) then #0 else
                      let 'num_2__ := arg_0__ in
                      if Bool.Sumbool.sumbool_of_bool (num_2__ GHC.Base.== #1) then #1 else
                      let 'n := arg_0__ in
                      slowFib (n GHC.Num.- #1) GHC.Num.+ slowFib (n GHC.Num.- #2).
Solve Obligations with (solve_fib).

Definition cachedFib : Coq.Numbers.BinNums.N -> Coq.Numbers.BinNums.N :=
  lookupTrie (mkTrie slowFib).

(* External variables:
     Bool.Sumbool.sumbool_of_bool Coq.NArith.BinNat.N.lt Coq.Numbers.BinNums.N
     GHC.Base.op_z2218U__ GHC.Base.op_zeze__ GHC.Num.fromInteger GHC.Num.op_zm__
     GHC.Num.op_zp__ GHC.Num.op_zt__ GHC.Real.div GHC.Real.odd
*)

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