[Agda] Some problems with termination checker

[v0ιd]

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?

[Arseniy Alekseyev]

The point of termination checker is roughly to "desugar" recursive
definitions with pattern matching into non-recursive definitions that use
universal eliminator.
(I think it's not quite what it does in Agda, but that's how its behavior
is justified).

Here you have no pattern matching so there's nothing to desugar, so nothing
for termination checker to do.
When you write something using universal eliminators, that's normally an
exercise in avoiding recursion altogether.

Post by v0ιd
so obvious cases

It's not so obvious: you need to know that [fold] will only ever give you
"smaller" Οs, which is maybe possible using sized types (I have no idea),
but it's not visible syntactically in the definition of [zip-with].

Post by v0ιd
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.
zip-with
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
https://lists.chalmers.se/mailman/listinfo/agda

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

Post by v0ιd
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.
  zip-with
  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
https://lists.chalmers.se/mailman/listinfo/agda