<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">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="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>
</div>