[Agda] Some problems with termination checker

[Guillaume Allais]

Do you need the recursive call? I started implementing the same
function using Vec instead of List to make the size invariant
clearer and after a bit of cleaning up I got an implementation
which is just using two folds (which makes sense: the first one
performs the induction, the second one is merely used to do a
case analysis)

================================================================
open import Agda.Builtin.Nat

id : {a : _} → {A : Set a} → A → A
id x = x

data Vec {a} (A : Set a) : Nat → Set a where
 nil : Vec A 0
 cons : ∀ {n} → A → Vec A n → Vec A (suc n)

module _ {a b} {A : Set a} (B : Nat → Set b) where

 fold : ∀ {n} → Vec A n → (∀ {n} → A → Vec A n → B n → B (suc n)) → B 0
→ B n
 fold nil         c n = n
 fold (cons x xs) c n = c x xs (fold xs c n)

module _ {a b c} {A : Set a} {B : Set b} {C : Set c}  where

 zip-with : ∀ {n} → (A → B → C) → Vec A n → Vec B n → Vec C n
 zip-with f xs ys = fold P xs step base ys where

  P : Nat → Set _
  P n = Vec B n → Vec C n

  step : ∀ {n} → A → Vec A n → P n → P (suc n)
  step x xs rec yys = fold (Vec C) yys (λ y ys → cons (f x y)) nil

  base : P 0
  base _ = nil
================================================================

Cheers,


On 17/02/18 10:37, v0ιd wrote:
> Dear list,
> I try to define a zip-with function without pattern matching through
> universal constructor eliminator for Lists.
>
> id : {a : _} → {A : Set a} → A → A
> id x = x
>
> data List {a} (A : Set a) : Set a where
>  nil : List A
>  cons : A → List A → List A
>
> fold : {a b c : _} → {A : Set a} → {B : Set b} → {C : Set c} → List A
> → (A → List A → ((B → C) → B → C) → (B → C) → B → C) → (B → C) → B → C
> fold nil _ fs s = fs s
> fold (cons x xs) f = f x xs (fold xs f)
>
> zip-with : {a b c : _} → {A : Set a} → {B : Set b} → {C : Set c} → (A
> → B → C) → List A → List B → List C
> zip-with f x y = fold x (λ ξ ξs _ _ _ → fold y (λ η ηs _ _ _ → cons (f
> ξ η) (zip-with f ξs ηs)) id nil) id nil
>
> But it fails termination checking.
>
> Termination checking failed for the following functions:
>   zip-with
> Problematic calls:
>   zip-with f ξs ηs
>
> I would not want to suppress termination checking at all with {-#
> TERMINATING #-}.
> What can I do here? Maybe it makes sense somehow to
> improve termination checker for so obvious cases?
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180218/eff4c1c8/attachment.html>