[Agda] normalization question

[Aaron Stump]

Dear Agda community,

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.

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.

Any insights appreciated.  I observed the same behavior with Coq, by the
way.

Best,
Aaron
-----------------------------------------------
module Busy where

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

busy : ℕ → ℕ → ℕ
busy 0 = λ x → x
busy (suc n) = λ x →
  let f = busy n in
    f (f x)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210430/ff3549fc/attachment.html>