[Agda] Problem with the termination checker

[Andreas Abel]

This is rather a problem with your definition.  (See below.)

Also I do not know what is the purpose of T.  Heterogeneous streams?   
Could you not encode them as

> data T (l : Level) : Set (suc l) where
>   buildT : (A : Set l) -> (t : ∞ (T l)) -> A -> T l


(then you can even use record syntax).

Cheers
Andreas

On Sep 24, 2010, at 4:11 PM, David Leduc wrote:

> Hi,
>
> In the code below I define a datatype T and then
> define a function mylift that will lift
> a value of type T l1 into a value of type T (l1 ⊔ l2).
>
> However the termination checker rejects my function mylift :(
> How can I convince Agda that mylift terminates?
>
>
> {-# OPTIONS --universe-polymorphism #-}
>
> module test where
>
> open import Level
> open import Coinduction
>
> mutual
>
> data T (l : Level) : Set (suc l) where
>   buildT : (A : Set l) -> (t : ∞ (T l)) -> [ ♭ t ] -> T l
>
> [_] : {l : Level}(t : T l) -> Set l
> [ buildT A _ _ ] = A
>
> p2 : {l : Level} -> T l -> T l
> p2 (buildT _ t _) = ♭ t
>
> p3 : {l : Level}(t : T l) -> [ p2 t ]
> p3 (buildT _ _ x) = x
>
> mutual
>
>  mylift : (l1 l2 : Level) -> T l1 -> T (l1 ⊔ l2)
>  mylift l1 l2 t = buildT (c1 l1 l2 t) (♯ c2 l1 l2 t) (c3 l1 l2 t)
>
>  c1 : (l1 l2 : Level) -> T l1 -> Set (l1 ⊔ l2)
>  c1 l1 l2 t = Lift{l1}{l2} [ t ]
>
>  c2 : (l1 l2 : Level) -> T l1 -> T (l1 ⊔ l2)
>  c2 l1 l2 t = mylift l1 l2 t
>
>  c3 : (l1 l2 : Level)(t : T l1) -> [ c2 l1 l2 t ]
>  c3 l1 l2 t = p3 (mylift l1 l2 t)

Well, disregarding the universe levels l1 and l2 (which could be  
hidden for more readability), we have

   mylift (buildT A t y) = buildT _ _ (c3 (buildT A t y)) = buildT _ _  
(p3 (mylift (buildT A t y)))

and there is your loop!  So, the termination checker is right!

This loop is not broken by a delay \sharp, so its not a guarded  
definition.


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/