[Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1

[mechvel at scico.botik.ru]

On 2020-01-01 16:18, Guillaume Allais wrote:
> 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
> ====================================================================


I see. Thank you.

We have so easily bypassed this fundamental type checker restriction.
May be, this means that the type checker is going to recover and 
prohibit this also?
:-)

--
SM


> 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
>>