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

[Jesper Cockx]

The current restriction is quite simple: for a function to be
structurally recursive on an argument x of type T, the type T must be
a data type *before* any matching has been done. In particular, this
prohibits structural recursion on 'deep' arguments and universe-like
constructions such as the one in my previous mail. I don't know what
the current situation is on the Coq side of things, maybe someone else
can clarify?

Jesper

On 6/30/14, Dan Licata <dlicata at wesleyan.edu> wrote:
> great! is there a way to explain what the restriction is?  Has Coq fixed
> this bug yet, and if so, how does your solution compare to theirs?
>
> -Dan
>
> On Jun 27, 2014, at 12:26 PM, Jesper Cockx <Jesper at sikanda.be> wrote:
>
>> 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
>>
>>
>
>