[Agda] normalization question

[Martin Escardo]

Regardless of evaluation strategy, there will be 2^n function
applications, in both busy and in busy'. Martin

On 01/05/2021 09:00, Jesper at sikanda.be wrote:
> 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
> <mailto: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 <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe