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