[Agda] Termination checker change?

[Andreas Abel]

The structural order is not type-based, but there is eta-contraction, so 
in case of test4 it compares

   < t (br a) , (λ x → f x) >  to  < Branch a t , f >

which, since argument and pattern have the same constructor, proceeds 
with the arguments and then assumes the worst will happen.

     worstOf (compare (t (br a), Branch a f), compare (f, f))
   = worstOf (<, =)
   = <

In case test3 you get

     worstOf (compare (t (br a), Branch a f), compare (\ x -> x, f))
   = worstOf (<, ?)
   = ?

because the relationship between the identity function and f is unknown. 
  This is why test4 is accepted and test3 not.

What we had before was allowing lexicographic orderings of subterms. 
But the feature was buggy and without theoretical foundation, so we 
dropped it.

Cheers,
Andreas


On 06.06.2014 10:15, Pierre Hyvernat wrote:
>
>
>> Yes, indeed, the termination checker has changed, due to a soundness
>> issue.
>>
>> Currently, it does not look through pairs anymore, so you have to
>> curry your functions.
>>
> It looks a little subtler than that
>
>   test4 : (W × (One -> One)) -> One
>   test4 < Empty , f > = *
>   test4 < Branch a t , f > = test4 < t (br a) , (λ x → f x) >
>
> is accepted, while
>
>   test3 : (W × (One -> One)) -> One
>   test3 < Empty , f > = *
>   test3 < Branch a t , f > = test3 < t (br a) , (λ x → x) >
>
> is not...
>
> (The only difference is the second component of the pair in the
> recursive call...)
>
> Does it mean it doesn't accept any kind of deep-pattern matching?
>
>
>> I have an idea to bring uncurried functions back (in a sound way), but
>> will need some time to implement it.
>>
> Is the actual termination checker of Agda described somewhere. Last time
> I checked, the wiki
> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.TerminationChecker
>
> wasn't accurate.
>
> I once had understood that the termination checker used both a variant
> of the size-change principle, together with some sized-typed principle.
> If so, do the two notions interact in some non-trivial way?
> A quick look at the source seems to indicate they do not...
> Is that right?
>
>
>
> ===== file test.agda =====
> module test where
>
> record One : Set where constructor *
>
> record _×_ (A : Set) (B : Set) : Set where
>   constructor <_,_>
>   field
>     fst : A
>     snd : B
>
> module Problem (A : Set) (D : A -> Set) (br : (a : A) -> D a) where
>
>   data W : Set where
>     Empty : W
>     Branch : (a : A) -> (f : (d : D a) -> W) -> W
>
>   test3 : (W × (One -> One)) -> One
>   test3 < Empty , f > = *
>   test3 < Branch a t , f > = test3 < t (br a) , (λ x → x) >
>
>   test4 : (W × (One -> One)) -> One
>   test4 < Empty , f > = *
>   test4 < Branch a t , f > = test4 < t (br a) , (λ x → f x) >
>
> ==========
>
> Pierre


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

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

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