<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; color: rgb(0, 0, 0); font-size: 14px; font-family: Calibri, sans-serif; "><div>There is certainly our old paper:</div><div><br></div><div><a href="http://www.cs.nott.ac.uk/~txa/publ/jfp02.pdf">http://www.cs.nott.ac.uk/~txa/publ/jfp02.pdf</a></div><div><br></div><div><pre style="word-wrap: break-word; white-space: pre-wrap; ">@Article{alti:jfp02,
author = {Andreas Abel and Thorsten Altenkirch},
title = {A Predicative Analysis of Structural Recursion},
journal = {Journal of Functional Programming},
year = 2002,
volume = 12,
number = 1,
pages = {1--41},
month = {January}
}</pre><pre style="word-wrap: break-word; white-space: pre-wrap; "><span style="font-family: Calibri, sans-serif; ">Thorsten </span></pre><pre style="word-wrap: break-word; white-space: pre-wrap; "><br></pre></div><span id="OLK_SRC_BODY_SECTION"><div style="font-family:Calibri; font-size:11pt; text-align:left; color:black; BORDER-BOTTOM: medium none; BORDER-LEFT: medium none; PADDING-BOTTOM: 0in; PADDING-LEFT: 0in; PADDING-RIGHT: 0in; BORDER-TOP: #b5c4df 1pt solid; BORDER-RIGHT: medium none; PADDING-TOP: 3pt"><span style="font-weight:bold">From: </span> Jesper Cockx <<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a>><br><span style="font-weight:bold">Date: </span> Tue, 7 May 2013 13:04:29 +0100<br><span style="font-weight:bold">To: </span> "<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>" <<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>><br><span style="font-weight:bold">Subject: </span> [Agda] Termination checker correctness proof<br></div><div><br></div><blockquote id="MAC_OUTLOOK_ATTRIBUTION_BLOCKQUOTE" style="BORDER-LEFT: #b5c4df 5 solid; PADDING:0 0 0 5; MARGIN:0 0 0 5;"><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></blockquote></span>
<br><br>
<br></body></html>