[Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1

[Guillaume Allais]

This is what I would have written:

====================================================================
open import Data.List.Base using (List; []; _∷_; [_])
open import Data.Nat.Base using (ℕ; _<_; _≮_; _∸_)
open import Data.Nat.Properties using (_<?_)
open import Relation.Nullary using (Dec; yes; no)

g : (x y : ℕ) → x ≮ y → ℕ
g x y _ =  x ∸ y

f : List ℕ → List ℕ → List ℕ
f []       ys       =  ys
f xs       []       =  xs
f (x ∷ xs) (y ∷ ys) with (x <? y) | f (x ∷ xs) ys | f xs (y ∷ ys)
... | yes x<y | fy | fn = y ∷ fy
... | no x≮y  | fy | fn = g x y x≮y ∷ fn
====================================================================

On 01/01/2020 12:58, mechvel at scico.botik.ru wrote:
> On 2019-12-31 21:27, mechvel at scico.botik.ru wrote:
>> On 2019-12-31 18:25, Guillaume Allais wrote:
>>> I'll add to that: if you perform all the recursive calls at the
>>> same time as `with comparePP e e'` then you should be able to get
>>> a terminating version of the function.
>>>
>>> I am saying "should" because the example is not self-contained and
>>> as such it is impossible to test.
>>>
>>
>> A sigh of releaf!
>> The following is recognized as terminating:
>>
>> ------------------------------------------------
>> open import Data.List using (List; []; _∷_)
>> open import Data.Nat using (ℕ; _<_)
>> open import Data.Nat.Properties using (_<?_)
>> open import Relation.Nullary using (Dec; yes; no)
>>
>> g : List ℕ → List ℕ → List ℕ
>> g []       ys       =  ys
>> g xs       []       =  xs
>> g (x ∷ xs) (y ∷ ys) =  aux (x <? y) (y ∷ (g (x ∷ xs) ys))
>>                                     (x ∷ (g xs (y ∷ ys)))
>>   where
>>   aux : Dec (x < y) → List ℕ → List ℕ → List ℕ
>>   aux (yes _) zs _  =  zs
>>   aux (no _)  _  us =  us
>> -----------------------------------------------
>>
>> So that we avoid a complication of introducing a counter.
> 
> 
> Still there remains a certain complication in the "dependent" case.
> Consider
> 
> -------------------------------------------------------------
> open import Data.List using (List; []; _∷_; [_])
> open import Data.Nat using (ℕ; _<_; _≮_; _∸_)
> open import Data.Nat.Properties using (_<?_)
> open import Relation.Nullary using (Dec; yes; no)
> 
> g : (x y : ℕ) → x ≮ y → ℕ
> g x y _ =  x ∸ y
> 
> f : List ℕ → List ℕ → List ℕ
> f []       ys       =  ys
> f xs       []       =  xs
> f (x ∷ xs) (y ∷ ys) =  aux (x <? y)
>   where
>   aux : Dec (x < y) → List ℕ
>   aux (yes _)  =  y ∷ (f (x ∷ xs) ys)
>   aux (no x≮y) =  (g x y x≮y) ∷ (f xs (y ∷ ys))
> -------------------------------------------------------------
> 
> The RHS of the second clause for  aux  depends on the value  x≮y.
> So that we cannot set  (g x y x≮y) ∷ (f xs (y ∷ ys))
> as the third argument for new  aux,
> because the value  x≮y  is not in the scope
> (and imagine that g analizes the value x≮y).
> However the following is type-checked:
> 
> --------------------------------------------------------------
> f : List ℕ → List ℕ → List ℕ
> f []       ys       =  ys
> f xs       []       =  xs
> f (x ∷ xs) (y ∷ ys) =  aux (x <? y) (y ∷ (f (x ∷ xs) ys))
>                                     (aux' (x <? y))
>   where
>   aux : Dec (x < y) → List ℕ → List ℕ → List ℕ
>   aux (yes _)  xs _  =  xs
>   aux (no x≮y) _  xs =  xs
> 
>   aux' : Dec (x < y) → List ℕ
>   aux' (no x≮y) =  (g x y x≮y) ∷ (f xs (y ∷ ys))
>   aux' (yes _)  =  []                           -- inaccessible
> --------------------------------------------------------------
> 
> This does not look so nice, but it is nicer that introducing a counter
> for termination proof.
> 
> What people think of this, what can be a better solution?
> 
> Thanks,
> 
> -- 
> SM
> 
> 
> 
> 
>>> On 31/12/2019 12:23, Jesper Cockx wrote:
>>>> From the changelog:
>>>>
>>>> The "with inlining" feature of the termination checker has been removed. As
>>>>> a consequence, some functions defined using with are no longer accepted as
>>>>> terminating. See Issue #59 for why this feature was originally introduced
>>>>> and #3604 for why it had to be removed.
>>>>>
>>>>
>>>> It is likely that your function no longer passes the termination checker
>>>> because this feature was removed. There were several issues with the
>>>> implementation of this feature and no-one was willing to maintain it, so
>>>> unfortunately it had to be removed.
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>