[Agda] Termination checker correctness proof
Nils Anders Danielsson
nad at cse.gu.se
Tue May 7 14:23:26 CEST 2013
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
More information about the Agda
mailing list