<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=Windows-1252"></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>This is a good question.</div><div><br></div><div>If we restrict ourselves to Agda w.o. codata and sized types then Agda only recognizes programs whose termination order is the lexical product of the structural order of datatypes. Let’s call such programs structurally recursive. However, the set of structurally recursive programs is not decidable and Agda only recognizes those which are “guarded on the left”. Now one concrete question would be wether any structurally recursive program can be transformed into an equivalent one which is guarded. I suspect the answer is no, because even though a program is semantically structural this may not be provable within Agda.</div><div><br></div><div>Any thoughts? </div><div><br></div><div>Thorsten</div><div><br></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> Kirill Elagin <<a href="mailto:kirelagin@gmail.com">kirelagin@gmail.com</a>><br><span style="font-weight:bold">Date: </span> Tue, 29 Jul 2014 22:26:37 +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] Theoretical limits of termination checking (reference request)<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"><div>Hello,<br><br>I was going through the great articles by Andreas Abel and I suddenly started asking myself very basic questions about theoretical limits of termination checking. The halting problem is often cited as an explanation for impossibility of sound&complete termination checker. The termination checking problem is not exactly the halting problem, but indeed it is quite easy to derive impossibility of general termination checking from impossibility of solving the halting problem.<br><br></div>But then, another question arises. When we encode proofs, say, in Agda, we often have a terminating program in mind, but we have to write it down in some specific way, so that the termination checker “sees” that the program is fine. So, is it possible to develop a “programming style” such that there is a sound&complete termination checker for programs “written in this style”, _and_ any program can be “written in this style” (the “translation” function is obviously not computable)? Formally: is there a subset of programs, such that there is an algorithm correctly checking termination of programs from this subset _and_ for any program there is an equivalent in this subset (by “equivalent” I mean “extensionally equal”)?<br><div>I used to think that it is impossible, but I recently realized that my “proof” was wrong. Turns out that when we are working with the whole universe of programs, undecidability of termination checking follows from undecidability of the halting problem. But if we restrict ourselves to a subset, it is no longer necessarily true, and sound&complete termination checking (for programs from this subset) _is_ possible for some subsets.<br><br>Then, there are more questions. How good can we become at translating arbitrary programs to equivalents from some of those good subsets? As I said, the translation function is clearly not computable. But can it be that it is not computable only for programs we don't care about? Or maybe it is not computable by algorithms, but computable by human brains? Are any of the existing means of checking termination already “perfect” in this sense, that is can I write _any_ terminating function, say, in MiniAgda, so that it passes the termination check?<br>
I haven't come up with any answers to those ones yet.<br><div><br>For some reason I couldn’t find any information on this topic. I guess that either those questions are so trivial and the answers to them are so obvious that no one even bothers to write them down, or everything about this was published long ago in 70s, so it’s somewhat difficult to find those papers now.<br>
I feel that negative results are most likely to come from the computability theory, while positive ones—from more specific fields.<br><br>Is there an ultimate source of this kind of funny, useless, purely theoretical facts?<br></div></div></div></blockquote></span>
<br><p>This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.</p><p>This message has been checked for viruses but the contents of an attachment may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.</p>
<br></body></html>