[Agda] normalization question

[Aaron Stump]

Thanks, Jesper, Martin, and Ulf for your replies!

Suppose we use a modification of the normal-order reduction strategy, where
to normalize

let x = t1 in t2

we first normalize t1 and then normalize t2 (and otherwise we use
normal-order reduction).  This is like being call-by-value for
let-terms, and otherwise normal-order.  Then busy n will normalize in O(n)
steps, not O(2^n).  Cedille actually implements this strategy, and sure
enough, it can normalize busy 64, for example (Haskell, Agda, and Coq
cannot).  So Martin, even though I agree that there is an
exponential-length reduction of busy n, I do not agree that all reductions
are this length.

This strategy would not help with your version, Jesper, as there we would
use call-by-name for the application of twice to busy n, and then we would
duplicate busy n (leading to exponential explosion).  So your example shows
that a cbv-let strategy would not be too robust!

I do not believe this example requires some more sophisticated memoization,
Ulf, as cbv-let (which is just a beta-reduction strategy, not some novel
machinery for reduction) is sufficient.  I have different example, based on
this one, which does need machinery more like that of optimal beta to keep
the time linear.

For that variant and a bit more discussion, see my blog post of yesterday:

https://queuea9.wordpress.com/2021/04/30/another-optimality-challenge/

Thanks again,
Aaron



On Sat, May 1, 2021 at 5:32 AM Ulf Norell <ulf.norell at gmail.com> wrote:

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