[Agda] normalization question

[Aaron Stump]

Very interesting!  I did not know about primForce.
Thanks,
Aaron

On Sun, May 2, 2021 at 12:17 PM Nils Anders Danielsson <nad at cse.gu.se>
wrote:

> On 2021-05-02 06:09, Aaron Stump wrote:
> > 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).
>
> The term busy 3000 normalises quickly if you write the code in the
> following way:
>
>    open import Agda.Builtin.Nat
>    open import Agda.Builtin.Strict
>
>    busy : Nat → Nat → Nat
>    busy 0       = λ x → x
>    busy (suc n) =
>      primForce (busy n) λ f →
>      λ x → f (f x)
>
> However, this does not apply to the following piece of code:
>
>    open import Agda.Builtin.Nat
>    open import Agda.Builtin.Strict
>
>    busy : Nat → Nat → Nat
>    busy 0       = λ x → x
>    busy (suc n) = λ x →
>      primForce (busy n) λ f →
>      f (f x)
>
> --
> /NAD
> _______________________________________________
> 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/20210502/5648c711/attachment.html>