[Agda] Evaluation question

[Ulf Norell]

If we also fix the lambda-lifting issue, using case_of_, we can get it down
to 2^n:

epsilon : Nat → (Cantor → Bool) → Cantor
epsilon zero    p = λ i → false
epsilon (suc n) p =
  case p (cons false (epsilon n (p ∘ cons false))) of λ
    b → cons b (epsilon n (p ∘ cons b))

This version runs about 6 times slower than ghci, which I think isn't too
bad.

/ Ulf

On Mon, May 31, 2021 at 9:07 AM Ulf Norell <ulf.norell at gmail.com> wrote:

> I assume we are talking type-checking time evaluation and not compiling to
> Haskell.
>
> In this case, surprisingly, I don't think the lambda lifting of b is the
> problem. Rather I think
> the double exponential is because the Agda abstract machine is bad at
> evaluating lambdas.
> If you get rid of the lambda in the local α:
>
> epsilon : Nat → (Cantor → Bool) → Cantor
> epsilon zero    p = λ i → false
> epsilon (suc n) p = cons b α
>   where
>     b : Bool
>     b = p (cons false (epsilon n λ α → p (cons false α)))
>
>     α : Cantor
>     α = epsilon n (p ∘ cons b)
>
> it runs in what looks like 3^n to me. With this version I can C-c C-n
> example2 11 in 10s. Still far
> from the Haskell performance, but at least it's no longer a double
> exponential.
>
> / Ulf
>
> On Sun, May 30, 2021 at 1:41 PM Martin Escardo <m.escardo at cs.bham.ac.uk>
> wrote:
>
>> Consider the following Haskell code (also attached) and its translation
>> to Agda (not included).
>>
>> * In Agda the (good) runtime behaviour of example1 is replicated - it is
>> linear.
>>
>> * However, example2 in Haskell runs in roughly O(2^n) whereas in Agda it
>> seems to run in O(2^(2^n)). The largest I can run in Agda is n=4.
>>
>> How do I rewrite the program in Agda to get the same times as in
>> Haskell? The crucial function is "epsilon".
>>
>> --
>> *Main> example1 (nat (10^6))
>> True
>> (2.83 secs, 696,069,600 bytes)
>> *Main> example2 (nat (15))
>> False
>> (1.09 secs, 504,960,752 bytes)
>> *Main> example2 (nat 15)
>> False
>> (1.11 secs, 504,960,752 bytes)
>> *Main> example2 (nat 16)
>> False
>> (2.44 secs, 1,130,698,664 bytes)
>> *Main> example2 (nat 17)
>> False
>> (5.42 secs, 2,516,654,176 bytes)
>> *Main> example2 (nat 18)
>> False
>> (12.03 secs, 5,571,156,248 bytes)
>> --
>>
>> data Nat = Zero | Succ Nat
>>
>> type Cantor = Nat -> Bool
>>
>> cons :: Bool -> Cantor -> Cantor
>> cons b alpha Zero     = b
>> cons b alpha (Succ n) = alpha n
>>
>> epsilon :: Nat -> (Cantor -> Bool) -> Cantor
>> epsilon Zero p     = \i -> False
>> epsilon (Succ n) p = cons b alpha
>>  where
>>   b :: Bool
>>   b = p (cons False (epsilon n (\alpha -> p (cons False alpha))))
>>
>>   alpha :: Cantor
>>   alpha = epsilon n (\alpha -> p (cons b alpha))
>>
>> forevery :: Nat -> (Cantor -> Bool) -> Bool
>> forevery n p = p (epsilon n p)
>>
>> -- Examples
>>
>> nat :: Integer -> Nat
>> nat 0 = Zero
>> nat n = Succ (nat (n-1))
>>
>> p1 :: Nat -> Cantor -> Bool
>> p1 n alpha = alpha n == alpha n
>>
>> example1 :: Nat -> Bool
>> example1 n = forevery (Succ n) (p1 n)
>>
>> p2 :: Nat -> Cantor -> Bool
>> p2 Zero     alpha = True
>> p2 (Succ n) alpha = alpha Zero /= p2 n (\i -> alpha (Succ i))
>>
>> example2 :: Nat -> Bool
>> example2 n = forevery n (p2 n)
>>
>> I think that "b" in Haskell gets evaluated at most once, but in Agda it
>> is evaluated zero times or else repeatedly. But I may be wrong. I tried
>> primForce but it didn't seem to make any difference.
>>
>> How do I make example2 as fast as in Haskell?
>>
>> Martin
>>
>> _______________________________________________
>> 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/20210531/0424bc73/attachment.html>