<div dir="ltr">Dear Agda mailing list,<div><br></div><div>I'm currently writing my master thesis on pattern matching with dependent types, and I have a question about the termination checker in Agda.</div><div>
<br></div><div>On the <a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.TerminationChecker" target="_blank">wiki page on termination</a>, there is the following definition of the termination order:</div>
<div>
<br></div><div><ol style="line-height:1.5em;font-size:13px;font-family:sans-serif;margin:0.3em 0px 0px 3.2em;padding:0px"><li style="margin-bottom:0.1em">Constructor elimination: if cons is a constructor, x < cons a1..an x b1..bn,<div style="margin-top:1.33em">
</div></li><li style="margin-bottom:0.1em">Application: if y<x then (ya)<x where a is a vector of terms.</li></ol><div><font color="#000000" face="sans-serif"><span style="line-height:19.5px"><br></span></font></div>
<div><font color="#000000" face="sans-serif"><span style="line-height:19.5px">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.</span></font></div>
<div><br></div><div><font color="#000000" face="sans-serif"><span style="line-height:19.5px">A proof would certainly need the fact that data types are strictly positive, otherwise we get non-termination problems like </span></font><a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.BadInHaskell" target="_blank">the type Bad</a>.</div>
<div><br></div><div>One way to argue correctness of the termination checker would be that pattern matching can be translated to a case tree, which can be translated to eliminators, which are terminating by some type theoretic metatheory. But I would like to have a more direct proof that doesn't use the equivalence with case trees.</div>
<div><br></div><div>Can someone give me an argument or a reference which shows that this termination order is well-founded? This would be much appreciated.</div><div><br></div><div>Best regards,</div>
<div>Jesper</div></div></div>