The Coq mailing list

[Jean-Francois Monin <jeanfrancois.monin AT rd.francetelecom.com>]

I just want Eval Compute (flog O (all_acc_div2 O)) to provide the result.
After all, STRONG normalization is not crucial here (and may be
overestimated or misleading).

As Extraction is supposed to work, Coq should be able to perform
the evaluation of (flog O (all_acc_div2 O)) without computing
(all_acc_div2 O). In other words, common strategies like Lazy
and preferably CBV should not have the pathological behavior you mention.

Is there any result on this topic?

  Jean-Francois

Pierre Courtieu wrote:
 > 
 > Suppose you allow the Fix to be reduced in the term:
 > 
 > (flog O (all_acc_div2 n)).
 > 
 > You obtain:
 > 
 > Cases (test_O_1_else O) of
 >    | (C0 _) => O
 >    | (C1 _) => O
 >    | (C2 p) => (S (flog (div2 O) (inv_acc_div2 O a p)))
 > end.
 > 
 > and then you can reduce (div2 O) into O:
 > 
 > Cases (test_O_1_else O) of
 >    | (C0 _) => O
 >    | (C1 _) => O
 >    | (C2 p) => (S (flog O (inv_acc_div2 O a p)))
 > end.
 > 
 > and then you can reduce again the Fix infinitely ! You lost SN. This
 > seems to be a consequence of Fix/Case duality.