The Coq mailing list

[Benjamin Gregoire <Benjamin.Gregoire AT sophia.inria.fr>]

Georges Gonthier wrote:

> > I would not have used a value as large as 10^100, but you got me
> > curious. So I tested some large values. As expected, it has no impact on
> > "lazy". For "compute" and "vm_compute", it starts to be noticeable at
> > 10^20; and at 10^30, Coq is lost in hell.
> >    
>
>  
>
> > I'm surprised Coq is able to go that far with the call-by-value
> > evaluation scheme. I must be missing something about the way your
> > "guard" function is expanded. How many constructors are explicitly
> > created for 10^20 in call-by-value?
> >    
>
>  What Bruno had in mind was that call-by-value only does weak reduction in 
> arguments, so by putting a lambda around the doubling call, he hopes to stop 
> compute from expanding the whole binary call tree before producing a single 
> constructor.
>  Unfortunately, he doesn't quite get it right. The wfR lambdas aren't real: they get 
> expanded as soon as "guard" is applied. In contrast, the lambdas in the 
> second argument of Acc_intro can only be expanded when the client comsumes the 
> Acc_intro. The upshot is that the recursion for the xO case is essentially unguarded, 
> while the one for xI is; so (guard (2^60 - 1) well) should work quite well, whereas 
> (guard (2^30) well) might well crash ;-)
>  Perhaps the easiest fix would simply be to pass the exponent to guard, as a 
> Peano integer:
>
> Fixpoint guard (n : nat) (wfR : well_founded R) {struct n}
>     : well_founded R :=
>   match n with
>   | 0 => wfR
>   | S n' =>
>     fun x => Acc_intro x (fun y _ => guard n' (guard n' wfR) y))
>   end.
>
>   Georges
>  
   Or to guard also the case of xO :
    

Fixpoint guard (p:positive) : well_founded R -> well_founded R :=
 match p with
 | xH => fun wfR x => Acc_intro x (fun y _ => wfR y)
 | xO p' => fun wfR x => let F := guard p' in Acc_intro x (fun y _ => F (F 
wfR) y)
 | xI p' => fun wfR x => let F := guard p' in Acc_intro x (fun y _ => F (F 
wfR) y)
 end.



> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>