<div dir="ltr">Thanks, Sam and Andreas, for the elegant examples of how to encode general recursion in a language that guarantees termination. Sam, am I right in thinking Conor's paper does not touch on the idea of combining constructive proofs of progress and preservation to derive a constructive evaluator? (But I could apply Conor's technique or a trampoline to express such an evaluator. Indeed, I considered using Delay for the evaluator in the textbook, but decided that supplying a step count was simpler, and avoided the need to explain coinduction.) Cheers, -- P</div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr"><br></div><div>Too brief? Here's why: <a href="http://www.emailcharter.org/" target="_blank">http://www.emailcharter.org/</a></div></div></div></div></div></div>
<br><div class="gmail_quote">On 6 July 2018 at 19:23, Sam Lindley <span dir="ltr"><<a href="mailto:Sam.Lindley@ed.ac.uk" target="_blank">Sam.Lindley@ed.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">You should certainly cite Conor McBride's MPC 2015 paper "Turing-Completeness Totally Free":<br>
<br>
  <a href="https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree.pdf" rel="noreferrer" target="_blank">https://personal.cis.strath.ac<wbr>.uk/conor.mcbride/TotallyFree.<wbr>pdf</a><span class="HOEnZb"><font color="#888888"><br>
<br>
Sam</font></span><span class=""><br>
<br>
On 06/07/18 17:49, Philip Wadler wrote:<br>
</span><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">
[ The Types Forum, <a href="http://lists.seas.upenn.edu/mailman/listinfo/types-list" rel="noreferrer" target="_blank">http://lists.seas.upenn.edu/ma<wbr>ilman/listinfo/types-list</a> ]<br>
<br>
<br>
<br>
<br></span><div><div class="h5">
Everyone on this list will be familiar with Progress and Preservation<br>
for terms in a typed calculus.  Write ∅ ⊢ M : A to indicate that term<br>
M has type A for closed M.<br>
<br>
   Progress.  If ∅ ⊢ M : A then either M is a value or M —→ N,<br>
   for some term N.<br>
<br>
   Preservation.  If ∅ ⊢ M : A and M —→ N then ∅ ⊢ N : A.<br>
<br>
It is easy to combine these two proofs into an evaluator.<br>
Write —↠ for the transitive and reflexive closure of —→.<br>
<br>
   Evaluation.  If ∅ ⊢ M : A, then for every natural number n,<br>
   either M —↠ V, where V is a value and the reduction sequence<br>
   has no more than n steps, or M —↠ N, where N is not a value<br>
   and the reduction sequence has n steps.<br>
<br>
Evaluation implies that either M —↠ V or there is an infinite<br>
sequence M —→ M₁ —→ M₂ —→ ... that never reduces to a value;<br>
but this last result is not constructive, as deciding which of<br>
the two results holds is not decidable.<br>
<br>
An Agda implementation of Evaluation provides an evaluator for terms:<br>
given a number n it will perform up to n steps of evaluation, stopping<br>
early if a value is reached. This is entirely obvious (at least in<br>
retrospect), but I have not seen it written down anywhere. For<br>
instance, this approach is not exploited in Software Foundations to<br>
evaluate terms (it uses a normalize tactic instead).  I have used it<br>
in my draft textbook:<br>
<br>
   https:<a href="http://plfa.inf.ed.ac.uk" rel="noreferrer" target="_blank">plfa.inf.ed.ac.uk</a><br>
<br>
Questions: What sources in the literature should one cite for this<br>
technique?  How well-known is it as folklore? Cheers, -- P<br>
<br>
<br>
.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>
.   /\ School of Informatics, University of Edinburgh<br>
.  /  \ and Senior Research Fellow, IOHK<br>
. <a href="http://homepages.inf.ed.ac.uk/wadler/" rel="noreferrer" target="_blank">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a><br>
<br>
Too brief? Here's why: <a href="http://www.emailcharter.org/" rel="noreferrer" target="_blank">http://www.emailcharter.org/</a><br>
<br>
<br>
<br></div></div><span class="">
The University of Edinburgh is a charitable body, registered in<br>
Scotland, with registration number SC005336.<br>
<br>
</span></blockquote>
<br>
-- <br><div class="HOEnZb"><div class="h5">
The University of Edinburgh is a charitable body, registered in<br>
Scotland, with registration number SC005336.<br>
<br>
<br>
</div></div></blockquote></div><br></div>