[Agda] heap mistery

[Andreas Abel]

Hi Martin,

thanks for the bug report.  If you have time, could you put it on

   http://code.google.com/p/agda/issues/list

with enough material to reproduce the behavior?

Thanks!
Andreas

On 5/19/11 5:49 PM, Martin Escardo wrote:
> This is regarding a heap-exhaustion problem I discussed earlier.
>
> I prove an existential Theorem, and then define
>
> program₁ : ₂ℕ → ℕ → ₂
> program₁ α m = ∃-witness(Theorem α m)
>
> program₂ : ₂ℕ → (m : ℕ) → (smaller(m + 1) → ℕ)
> program₂ α m = ∃-witness(∃-elim (Theorem α m))
>
> This makes Agda compilation run for some time until the heap is exhausted.
>
> Now I instead define the two programs by pattern matching rather than
> the destructors ∃-witness and ∃-elim (first and second projection):
>
> program₁ : ₂ℕ → ℕ → ₂
> program₁ α m = f(Theorem α m)
> where
> f : Finite-Pigeonhole α m → ₂
> f(∃-intro b proof) = b -- f is ∃-witness!!!
>
> program₂ : ₂ℕ → (m : ℕ) → (smaller(m + 1) → ℕ)
> program₂ α m = f(Theorem α m)
> where
> f : Finite-Pigeonhole α m → (smaller(m + 1) → ℕ)
> f(∃-intro b (∃-intro s proof)) = s -- f is ∃-witness o ∃-elim!!!
>
> Compilation is instanteneous and succeeds using neglegible memory.
>
> What is going on?
>
> This is how I defined ∃-witness and ∃-elim:
>
> data ∃ {X : Set} (A : X → Ω) : Ω where
> ∃-intro : (x₀ : X) → A x₀ → ∃ \(x : X) → A x
>
> ∃-witness : {X : Set} {A : X → Ω} → (∃ \(x : X) → A x) → X
> ∃-witness (∃-intro x a) = x
>
> ∃-elim : {X : Set} {A : X → Ω} →
> (proof : ∃ \(x : X) → A x) → A (∃-witness proof)
> ∃-elim (∃-intro x a) = a
>
> That is, using the same kind of pattern matching!!!
>
> Thanks,
> Martin
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/