<div dir="ltr"><div dir="ltr">Thanks, Jesper, Martin, and Ulf for your replies!<div><br></div><div>Suppose we use a modification of the normal-order reduction strategy, where to normalize</div><div><br></div><div>let x = t1 in t2</div><div><br></div><div>we first normalize t1 and then normalize t2 (and otherwise we use normal-order reduction).  This is like being call-by-value for let-terms, and otherwise normal-order.  Then busy n will normalize in O(n) steps, not O(2^n).  Cedille actually implements this strategy, and sure enough, it can normalize busy 64, for example (Haskell, Agda, and Coq cannot).  So Martin, even though I agree that there is an exponential-length reduction of busy n, I do not agree that all reductions are this length.</div><div><br></div><div>This strategy would not help with your version, Jesper, as there we would use call-by-name for the application of twice to busy n, and then we would duplicate busy n (leading to exponential explosion).  So your example shows that a cbv-let strategy would not be too robust!</div><div><br></div><div>I do not believe this example requires some more sophisticated memoization, Ulf, as cbv-let (which is just a beta-reduction strategy, not some novel machinery for reduction) is sufficient.  I have different example, based on this one, which does need machinery more like that of optimal beta to keep the time linear.</div><div><br></div><div>For that variant and a bit more discussion, see my blog post of yesterday:</div><div><br></div><div><a href="https://queuea9.wordpress.com/2021/04/30/another-optimality-challenge/">https://queuea9.wordpress.com/2021/04/30/another-optimality-challenge/</a><br></div><div><br></div><div>Thanks again,</div><div>Aaron</div><div><br></div><div><br></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, May 1, 2021 at 5:32 AM Ulf Norell <<a href="mailto:ulf.norell@gmail.com">ulf.norell@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>The key here is that function bodies are not shared. This is known as memoization and not something</div><div>that you would do automatically. So even without Agda's naive treatment of let, when you say<br></div><div><br></div><div>  let f = busy n in ...</div><div><br></div><div>you share the evaluation of `busy n` to `λ x → (code for body)`. Every time this function is evaluated the</div><div>code for the body executes regardless of if you called it before.</div><div><br></div><div>Implementing the example in Haskell has the same exponential performance.</div><div><br></div><div>/ Ulf<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, May 1, 2021 at 11:55 AM Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Regardless of evaluation strategy, there will be 2^n function<br>
applications, in both busy and in busy'. Martin<br>
<br>
On 01/05/2021 09:00, <a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a> wrote:<br>
> Hi Aaron,<br>
> <br>
> Agda does inlining of let-bindings during elaboration, so your<br>
> definition is equivalent to<br>
> <br>
> busy (suc n) = λ x → busy n (busy n x)<br>
> <br>
> for which it is not surprising that it's slow. However, what is<br>
> surprising to me is that the following version is still slow:<br>
> <br>
> twice : (ℕ → ℕ) → ℕ → ℕ<br>
> twice f x = f (f x)<br>
> <br>
> busy' : ℕ → ℕ → ℕ<br>
> busy' 0 = λ x → x<br>
> busy' (suc n) = twice (busy' n)<br>
> <br>
> Here it looks to me that lazy evaluation should kick in and make the<br>
> definition fast, but apparently that's not the case. Maybe one of the<br>
> other developers knows more about this.<br>
> <br>
> -- Jesper<br>
> <br>
> On Sat, May 1, 2021 at 6:21 AM Aaron Stump <<a href="mailto:aaron-stump@uiowa.edu" target="_blank">aaron-stump@uiowa.edu</a><br>
> <mailto:<a href="mailto:aaron-stump@uiowa.edu" target="_blank">aaron-stump@uiowa.edu</a>>> wrote:<br>
> <br>
>     Dear Agda community,<br>
> <br>
>     I am doing some experiments with normalization, and am getting a<br>
>     surprising (to me) result.  I have a function that I expected would<br>
>     normalize in linear time -- because I am expecting Agda will<br>
>     implement some kind of normal-order evaluation.  But normalization<br>
>     seems to take exponential time.  A self-contained version of the<br>
>     example is below.  Asking Agda to normalize a term like busy 30 is<br>
>     prohibitively slow.  <br>
> <br>
>     For any nat n, busy  n normalizes to the identity function.  It<br>
>     seems as though one could prove by induction on n that busy n<br>
>     normalizes (with normal-order reduction) in something like 3 * n + 1<br>
>     beta-reductions.<br>
> <br>
>     Any insights appreciated.  I observed the same behavior with Coq, by<br>
>     the way.  <br>
> <br>
>     Best,<br>
>     Aaron<br>
>     -----------------------------------------------<br>
>     module Busy where<br>
> <br>
>     data ℕ : Set where<br>
>       zero : ℕ <br>
>       suc : ℕ → ℕ<br>
> <br>
>     {-# BUILTIN NATURAL ℕ #-}<br>
> <br>
>     busy : ℕ → ℕ → ℕ<br>
>     busy 0 = λ x → x<br>
>     busy (suc n) = λ x →<br>
>       let f = busy n in<br>
>         f (f x)<br>
> <br>
> <br>
> <br>
>     _______________________________________________<br>
>     Agda mailing list<br>
>     <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>><br>
>     <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
>     <<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a>><br>
> <br>
> <br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> <br>
<br>
-- <br>
Martin Escardo<br>
<a href="http://www.cs.bham.ac.uk/~mhe" rel="noreferrer" target="_blank">http://www.cs.bham.ac.uk/~mhe</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>
</blockquote></div>