[Agda] normalization question

[Nils Anders Danielsson]

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