[Agda] Termination checker correctness proof

[Nils Anders Danielsson]

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>,
> 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