[Agda] normalization question

[Ulf Norell]

The key here is that function bodies are not shared. This is known as
memoization and not something
that you would do automatically. So even without Agda's naive treatment of
let, when you say

  let f = busy n in ...

you share the evaluation of `busy n` to `λ x → (code for body)`. Every time
this function is evaluated the
code for the body executes regardless of if you called it before.

Implementing the example in Haskell has the same exponential performance.

/ Ulf

On Sat, May 1, 2021 at 11:55 AM Martin Escardo <m.escardo at cs.bham.ac.uk>
wrote:

> 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
> _______________________________________________
> 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/c955fe64/attachment.html>