[Agda] Termination Checking and WIthout-K

[Jesper Cockx]

Hi Joey,

I haven't tried it in this example, but in general it can help the
termination checker to introduce more (mutual) helper functions to reduce
the nesting of pattern matches so that the end result does only shallow
pattern matching. So here you could have foldsO only pattern match on the
first argument and delegate each of the cases to a helper function. I hope
that helps.

-- Jesper

On Wed, Apr 29, 2020 at 11:53 PM Joey Eremondi <joey.eremondi at gmail.com>
wrote:

> Basically, I'm wondering if there's any way to make the following file
> pass the termination checker using the --without-K
>
>
> https://github.com/JoeyEremondi/spire.github.io/blob/debe0a3ebbb4c82388f4f5b785b955fbc02b3d4f/source/_code/2014-08-04-inductive-recursive-descriptions/IDescIR.agda
>
> It's a nifty combination of Descriptions and Induction-Recursion thanks to
> Larry Diehl. However, if I add the --without-K flag, it complains about
> foldO and foldsO not terminating.
>
> I'm assuming this is because of the issues described here:
> https://agda.readthedocs.io/en/v2.6.1/language/without-k.html#restrictions-on-termination-checking
>
> So I (roughly) understand the problem, but I have no idea if there's a
> solution. Is this simply not a well-founded definition when K is disabled?
> Or is there some trick I can use to massage this into something the
> termination checker will like?
> _______________________________________________
> 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/20200430/b4ac5bcd/attachment.html>