<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">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>