<div dir="ltr">My previous question must not have been clear, since I received two answers from top-notch researchers that missed my point. My question is not about progress and preservation or step indexing. My question is about the following observation:<div><br></div><div>Progress + Preservation = Evaluation.</div><div>From a constructive proof of progress and preservation, we can assemble a constructive evaluator which, for any given number n, will either reduce the term to a value (in less than n steps) or show that after n steps of reduction the term is not a value. [The key word here is *constructive*. Once one has proved progress and preservation constructively, one has implemented a constructive evaluator for terms.]</div><div><br></div><div>Pierce et al's text Software Foundations presents constructive proofs of progress and preservation. From these, one may immediately derive an evaluator for terms. But the text does not do so; instead it presents a separate normalisation tactic. (To be fair, that tactic is given prior to the proofs of progress and preservation. Nonetheless, after the proofs are given there is no observation that they might be applied to replace the normalisation tactic.) I also could not spot this observation in Harper's Practical Foundations for Programming Languages.</div><div><br></div><div>Indeed, in every presentation I can recall the act of proving progress and preservation is separated from the act of writing code that can evaluate a term, even though the former trivially implies the latter. (The one exception is my new textbook. It's located at <a href="http://plfa.inf.ed.ac.uk">plfa.inf.ed.ac.uk</a> --- do have a look!)</div><div><br></div><div><div style="font-size:12.8px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial">To repeat my questions: What sources in the literature should one cite for this technique? How well-known is it as folklore? <span style="font-size:small">Cheers, -- P</span></div></div><div><br></div><div><br></div></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 12:49, Philip Wadler <span dir="ltr"><<a href="mailto:wadler@inf.ed.ac.uk" target="_blank">wadler@inf.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"><div dir="ltr"><div><div>Everyone on this list will be familiar with Progress and Preservation</div><div>for terms in a typed calculus.  Write ∅ ⊢ M : A to indicate that term</div><div>M has type A for closed M.</div><div><br></div><div>  Progress.  If ∅ ⊢ M : A then either M is a value or M —→ N,</div><div>  for some term N.</div><div><br></div><div>  Preservation.  If ∅ ⊢ M : A and M —→ N then ∅ ⊢ N : A.</div><div><br></div><div>It is easy to combine these two proofs into an evaluator.</div><div>Write —↠ for the transitive and reflexive closure of —→.</div><div><br></div><div>  Evaluation.  If ∅ ⊢ M : A, then for every natural number n,</div><div>  either M —↠ V, where V is a value and the reduction sequence</div><div>  has no more than n steps, or M —↠ N, where N is not a value</div><div>  and the reduction sequence has n steps.</div><div><br></div><div>Evaluation implies that either M —↠ V or there is an infinite</div><div>sequence M —→ M₁ —→ M₂ —→ ... that never reduces to a value;</div><div>but this last result is not constructive, as deciding which of</div><div>the two results holds is not decidable.</div><div><br></div><div>An Agda implementation of Evaluation provides an evaluator for terms:</div><div>given a number n it will perform up to n steps of evaluation, stopping</div><div>early if a value is reached. This is entirely obvious (at least in</div><div>retrospect), but I have not seen it written down anywhere. For</div><div>instance, this approach is not exploited in Software Foundations to</div><div>evaluate terms (it uses a normalize tactic instead).  I have used it</div><div>in my draft textbook:</div><div><br></div><div>  https:<a href="http://plfa.inf.ed.ac.uk" target="_blank">plfa.inf.ed.ac.uk</a></div><div><br></div><div>Questions: What sources in the literature should one cite for this</div><div>technique?  How well-known is it as folklore? Cheers, -- P</div><div><br></div></div><br clear="all"><div><div class="m_-7027798386994020313gmail_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/<wbr>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.<wbr>org/</a></div></div></div></div></div></div>
</div>
</blockquote></div><br></div>