[Agda] Termination problems with "with" and recursion

[Dominique Devriese]

Jan, Jesper,

Note that the termination checker does seem to figure this out if you
do not use with:

The following (meaningless) function does pass the termination check,
for example:

  postulate _++_ : ∀ {X} → List X → List X → List X

  merge : List Nat → List Nat → List Nat
  merge nil       ys             = ys
  merge xs        nil            = xs
  merge (x :: xs) (y :: ys) = merge (x :: xs) ys ++ merge xs (y :: ys)
  -- merge (x :: xs) (y :: ys) with order x y
  -- merge (x :: xs) (y :: ys) | _ = merge (x :: xs) ys ++ merge xs (y
:: ys) -- doesn't work

I believe that a with-pattern-match is internally translated to a call
of a local helper function with the scrutinee as an extra argument and
an appropriate type to use the information learned from the pattern
match. Strangely, if I perform this translation manually here:
  merge′ : List Nat → List Nat → List Nat
  merge′ nil       ys             = ys
  merge′ xs        nil            = xs
  merge′ (x :: xs) (y :: ys)       = go x xs y ys (order x y)
    where go : Nat → List Nat → Nat → List Nat → Order → List Nat
          go x xs y ys le = x :: merge xs (y :: ys)
          go x xs y ys gt = y :: merge (x :: xs) ys

Then the termination checker does succeed.  It seems weird (at least
to me) that it doesn't work on the same code without the
with-desugaring.

Note by the way that in the case of Jan's code, there is no actual
reason to use with, since no type equality facts are learned from
pattern matching on the scrutinee of the with.

Regards,
Dominique

2013/10/30 Jan Stolarek <jan.stolarek at p.lodz.pl>:
>> The problem with the definition of merge is that the termination checker
>> looks for one argument to the function that becomes structurally smaller in
>> all recursive calls.
> OK, that makes sense. Well, maybe termination checker could be smarter, but now at least I can
> reasonably predict when it is going to complain.
>
> Thanks!
>
> Janek
>
>> There is no such argument for this definition, because
>> the first recursive call only reduces the size of the first argument, while
>> the second one only reduces the size of the second one. I think the
>> 'proper' way to solve this is to define your own termination order and use
>> Induction.WellFounded from the standard library, but I find this quite hard
>> to explain. Another way that works for this example is to define an
>> auxiliary merge function that takes a maximum number of recursion steps as
>> an extra argument. The real merge function can then call this one with a
>> sufficiently large number of steps (e.g. the total length of the two
>> lists). In agda:
>>
>> open import Data.Nat using (ℕ; zero; suc; _+_)
>> open import Data.List using (List; []; _∷_; length)
>>
>> data Order : Set where
>>   le ge : Order
>>
>> order : ℕ → ℕ → Order
>> order zero y = le
>> order (suc x) zero = ge
>> order (suc x) (suc y) = order x y
>>
>> merge-aux : ℕ → List ℕ → List ℕ → List ℕ
>> merge-aux _       []       ys = ys
>> merge-aux _       xs       [] = xs
>> merge-aux zero    _        _  = []
>> merge-aux (suc n) (x ∷ xs) (y ∷ ys) with order x y
>> merge-aux (suc n) (x ∷ xs) (y ∷ ys) | le = merge-aux n xs (y ∷ ys)
>> merge-aux (suc n) (x ∷ xs) (y ∷ ys) | ge = merge-aux n (x ∷ xs) ys
>>
>> merge : List ℕ → List ℕ → List ℕ
>> merge xs ys = merge-aux (length xs + length ys) xs ys
>>
>> I don't know why the termination checker doesn't complain for the version
>> that uses if_then_else_ instead of with. Maybe there is some additional
>> smartness in the termination checker that doesn't work well for 'with'?
>>
>> To the developers: In my opinion, the termination checker is one biggest
>> hurdles for people coming to Agda from other languages. How hard would it
>> be for the termination checker to detect termination of Janek's merge
>> function?
>>
>> Jesper
>>
>> On Wed, Oct 30, 2013 at 12:29 PM, Jan Stolarek <jan.stolarek at p.lodz.pl>wrote:
>> > Thanks for reply Jesper. Perhaps I ommitied something important when
>> > trying to simplify my
>> > example. Full code is below:
>> >
>> > ========== START CODE ==========
>> >
>> > module MergeSort where
>> >
>> > record Sg (S : Set)(T : S → Set) : Set where
>> >   constructor _,_
>> >   field
>> >     fst : S
>> >     snd : T fst
>> > open Sg public
>> > _×_ : Set → Set → Set
>> > S × T = Sg S λ _ → T
>> > infixr 4 _,_ _×_
>> >
>> > data Nat : Set where
>> >   zero : Nat
>> >   suc  : Nat → Nat
>> >
>> > data Order : Set where
>> >   le ge : Order
>> >
>> > data List (X : Set) : Set where
>> >   nil  : List X
>> >   _::_ : X → List X → List X
>> >
>> > order : Nat → Nat → Order
>> > order zero    y       = le
>> > order (suc x) zero    = ge
>> > order (suc x) (suc y) = order x y
>> >
>> > merge : List Nat → List Nat → List Nat
>> > merge nil       ys             = ys
>> > merge xs        nil            = xs
>> > merge (x :: xs) (y :: ys) with order x y
>> > merge (x :: xs) (y :: ys) | le = x :: merge xs (y :: ys)
>> > merge (x :: xs) (y :: ys) | ge = y :: merge (x :: xs) ys
>> >
>> > deal : {X : Set} → List X → List X × List X
>> > deal nil        = nil , nil
>> > deal (x :: nil) = x :: nil , nil
>> > deal (y :: (z :: xs)) with deal xs
>> > deal (y :: (z :: xs)) | ys , zs = y :: ys , z :: zs
>> >
>> > sort : List Nat → List Nat
>> > sort xs with deal xs
>> > sort xs | ys , nil = ys
>> > sort xs | ys , zs  = merge (sort ys) (sort zs)
>> >
>> > ========== END CODE ==========
>> >
>> > I have problems with merge and sort.
>> >
>> > Janek
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda