[Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?

[Jesper Cockx]

Yes, this restriction is to address the incompatibility of the termination
checker with univalence. As a side-effect, many functions on universes no
longer pass the termination check, for example (by Andreas):

T : Bool -> Set
T true = Nat
T false = List Nat

f : (x : Bool) -> T x -> Set
f true zero = Nat
f true (suc x) = f true x
f false nil = Nat
f false (x :: xs) = f false xs

For the moment, such definitions have to be unfolded manually:

f : (x : Bool) -> T x -> Set
f true = ftrue
  where
    ftrue : Nat -> Set
    ftrue zero = Nat
    ftrue (suc x) = ftrue x
f false = ffalse
  where
    ffalse : List Nat -> Set
    ffalse nil = Nat
    ffalse (x :: xs) = ffalse xs

However, due to a mistake I made in the fix, the termination checker a
complains much more than necessary when --without-K is enabled. This has
now been fixed in the development version:
https://code.google.com/p/agda/issues/detail?id=1214&can=1. I'll check the
other errors in Nils' library later. If you have any specific examples that
you think should be accepted, please send them to me and I'll see what I
can do.

Jesper


On Fri, Jun 27, 2014 at 6:52 AM, Dan Licata <dlicata at wesleyan.edu> wrote:

> Is this restriction addressing the "termination checker + propositional
> univalence inconsistency" issue, or something else?
>
> -Dan
>
> On Jun 21, 2014, at 1:44 PM, Jesper Cockx <Jesper at sikanda.be> wrote:
>
> I suppose by 'people working on this issue', you mean Andreas and me? I'm
> not currently working on this problem, but I could be convinced to if the
> current hack turns out to be too inconvenient. However, I have two problems
> before I can start working on a fix:
>
> - The current theory of pattern matching doesn't allow induction on 'deep'
> arguments, i.e. ones that only get an inductive type after pattern matching
> on some other arguments. So the theory would have to be extended.
>
> - I don't have a lot of experience with the termination checker, so I'm
> not confident to mess with it. It seems that in order to fix this problem,
> the termination checker would need some type information, as well as
> information about the substitutions performed by the previous case splits.
>
> If anyone can help me with (one of) these problems, I'd like to work
> together on it. Otherwise I'll try to get a better understanding by myself,
> but then it might take a long time.
>
> Jesper
>
>
> On Fri, Jun 20, 2014 at 7:13 PM, Andrés Sicard-Ramírez <asr at eafit.edu.co>
> wrote:
>
>>
>> On 20 June 2014 09:07, Brent Yorgey <byorgey at seas.upenn.edu> wrote:
>>
>>> but is the code I linked now expected to
>>> fail termination checking?
>>>
>>
>> Using the --without-K option? I don't know. This is an open issue and
>> people working on this issue know that the current behaviour is too
>> restrictive. I don't know if they are working in a better solution
>> right now.
>>
>> --
>> Andrés
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
> _______________________________________________
> 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/20140627/5289ce6b/attachment.html