[Agda] Termination checker correctness proof

[Jesper Cockx]

Thank you for your answers. I hadn't seen this paper by Andreas and
Thorsten before, it looks like it answers my question.

The current termination checker is more complicated than this. For
> instance, it uses
> size-change termination (see Lee, Jones and Ben-Amram,
> doi:10.1145/360204.360210), and supports corecursive definitions.


I know about the productivity checker for corecursion, but this size-change
termination is new to me. I will certainly also look into this.

Best regards,
Jesper


On Tue, May 7, 2013 at 2:23 PM, Nils Anders Danielsson <nad at cse.gu.se>wrote:

> On 2013-05-07 14:04, Jesper Cockx wrote:
>
>> On the wiki page on termination
>> <http://wiki.portal.chalmers.**se/agda/pmwiki.php?n=**ReferenceManual.**
>> TerminationChecker<http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.TerminationChecker>
>> >,
>>
>> there is the following definition of the termination order:
>>
>>  1. Constructor elimination: if cons is a constructor, x < cons a1..an x
>> b1..bn,
>>  2. Application: if y<x then (ya)<x where a is a vector of terms.
>>
>
> The current termination checker is more complicated than this. For
> instance, it uses
> size-change termination (see Lee, Jones and Ben-Amram,
> doi:10.1145/360204.360210), and supports corecursive definitions.
>
>
>  but I can't find a proof why this termination order is correct, i.e.
>> why it is well-founded. Specifically rule 2 seems suspicious because
>> evaluating ya could give something that's not smaller than x.
>>
>
> I think Andreas and Thorsten have discussed this definition
> (doi:10.1017/**S0956796801004191).
>
> --
> /NAD
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130507/dd305102/attachment.html