[Agda] Some problems with termination checker

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

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

On 17 February 2018 at 09:37, v0ιd <igorzsci at gmail.com> 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/20180217/be377eba/attachment.html>