[Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1

[mechvel at scico.botik.ru]

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