<div dir="ltr">Thank you for your answers. I hadn't seen this paper by Andreas and Thorsten before, it looks like it answers my question.<div><br></div><div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<span style="font-family:arial,sans-serif;font-size:13px">The current termination checker is more complicated than this. For<br></span><span style="font-family:arial,sans-serif;font-size:13px">instance, it uses<br></span><span style="font-family:arial,sans-serif;font-size:13px">size-change termination (see Lee, Jones and Ben-Amram,<br>
</span><span style="font-family:arial,sans-serif;font-size:13px">doi:10.1145/360204.360210), and supports corecursive definitions.</span></blockquote><div><br></div><div style>I know about the productivity checker for corecursion, but this size-change termination is new to me. I will certainly also look into this.</div>
<div><br></div><div style>Best regards,</div><div style>Jesper</div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, May 7, 2013 at 2:23 PM, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">On 2013-05-07 14:04, Jesper Cockx wrote:<br>
</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">
On the wiki page on termination<br></div>
<<a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.TerminationChecker" target="_blank">http://wiki.portal.chalmers.<u></u>se/agda/pmwiki.php?n=<u></u>ReferenceManual.<u></u>TerminationChecker</a>>,<div class="im">
<br>
there is the following definition of the termination order:<br>
<br></div>
1. Constructor elimination: if cons is a constructor, x < cons a1..an x b1..bn,<br>
2. Application: if y<x then (ya)<x where a is a vector of terms.<br>
</blockquote>
<br>
The current termination checker is more complicated than this. For<br>
instance, it uses<br>
size-change termination (see Lee, Jones and Ben-Amram,<br>
doi:10.1145/360204.360210), and supports corecursive definitions.<div class="im"><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
but I can't find a proof why this termination order is correct, i.e.<br>
why it is well-founded. Specifically rule 2 seems suspicious because<br>
evaluating ya could give something that's not smaller than x.<br>
</blockquote>
<br></div>
I think Andreas and Thorsten have discussed this definition<br>
(doi:10.1017/<u></u>S0956796801004191).<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
</font></span></blockquote></div><br></div>