[Agda] normalization question

[Jesper Cockx]

Hi Aaron,

Agda does inlining of let-bindings during elaboration, so your definition
is equivalent to

busy (suc n) = λ x → busy n (busy n x)

for which it is not surprising that it's slow. However, what is surprising
to me is that the following version is still slow:

twice : (ℕ → ℕ) → ℕ → ℕ
twice f x = f (f x)

busy' : ℕ → ℕ → ℕ
busy' 0 = λ x → x
busy' (suc n) = twice (busy' n)

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.

-- Jesper

On Sat, May 1, 2021 at 6:21 AM Aaron Stump <aaron-stump at uiowa.edu> wrote:

> 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)
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210501/fd8a3ea4/attachment.html>