<div dir="ltr"><div>Hi Aaron,</div><div><br></div><div>Agda does inlining of let-bindings during elaboration, so your definition is equivalent to</div><div><br></div><div><div>busy (suc n) = λ x → busy n (busy n x)</div><div><br></div><div>for which it is not surprising that it's slow. However, what is surprising to me is that the following version is still slow:</div><div><br></div><div>twice : (ℕ → ℕ) → ℕ → ℕ<br>twice f x = f (f x)<br><br>busy' : ℕ → ℕ → ℕ<br>busy' 0 = λ x → x<br>busy' (suc n) = twice (busy' n)</div><div><br></div><div>Here it looks to me that lazy evaluation should kick in and make the definition fast, but apparently that's not the case. Maybe one of the other developers knows more about this.<br></div><div><br></div><div>-- Jesper<br></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, May 1, 2021 at 6:21 AM Aaron Stump <<a href="mailto:aaron-stump@uiowa.edu">aaron-stump@uiowa.edu</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 dir="ltr">Dear Agda community,<div><br></div><div>I am doing some experiments with normalization, and am getting a surprising (to me) result.  I have a function that I expected would normalize in linear time -- because I am expecting Agda will implement some kind of normal-order evaluation.  But normalization seems to take exponential time.  A self-contained version of the example is below.  Asking Agda to normalize a term like busy 30 is prohibitively slow.  </div><div><br></div><div>For any nat n, busy  n normalizes to the identity function.  It seems as though one could prove by induction on n that busy n normalizes (with normal-order reduction) in something like 3 * n + 1 beta-reductions.</div><div><br></div><div>Any insights appreciated.  I observed the same behavior with Coq, by the way.  </div><div><br></div><div>Best,</div><div>Aaron</div><div>-----------------------------------------------</div><div><div>module Busy where</div><div><br></div><div>data ℕ : Set where</div><div>  zero : ℕ </div><div>  suc : ℕ → ℕ</div><div><br></div><div>{-# BUILTIN NATURAL ℕ #-}</div><div><br></div><div>busy : ℕ → ℕ → ℕ</div><div>busy 0 = λ x → x</div><div>busy (suc n) = λ x →</div><div>  let f = busy n in</div><div>    f (f x)</div></div><div><br></div><div><br></div><div><br></div></div></div>
_______________________________________________<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>