<div dir="ltr">Thanks, Pierre and Eelco. I'm well aware of "fuel" as folklore. For instance, I've heard Conor McBride describe fuel as an argument that, despite the guarantee that all programs terminate, Agda can effectively encode every recursive function. But that is different from my question; please see my second, clarifying email. I had a look at the three references cited, and I don't believe they exploit constructive proofs of progress and preservation to define an evaluator. 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 17:57, Pierre Courtieu <span dir="ltr"><<a href="mailto:pierre.courtieu@gmail.com" target="_blank">pierre.courtieu@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
I think this is now well known as the "fuel" pattern. Ideally n is<br>
very big and computed lazily.<br>
<br>
I am not aware of a paper specifically about this trick, it is there<br>
as a very useful folklore I guess.<br>
<br>
Note however that Bertot Balaa presented a more "complete" version of<br>
this by refining this trick: the function itself is defined by means<br>
of a proof that there exists a number N of iterations such that any<br>
greater number would give the same result. i.e. that N is a sufficient<br>
fuel to reach the fixpoint. This mechanism is used in the current<br>
implementation of the "Function" command in coq (when given a non<br>
structurally recursive function).<br>
<br>
<a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.28.601&rep=rep1&type=pdf" rel="noreferrer" target="_blank">http://citeseerx.ist.psu.edu/<wbr>viewdoc/download?doi=10.1.1.<wbr>28.601&rep=rep1&type=pdf</a><br>
<br>
Best,<br>
Pierre<br>
<span class="im HOEnZb">Le ven. 6 juil. 2018 à 21:28, Philip Wadler <<a href="mailto:wadler@inf.ed.ac.uk">wadler@inf.ed.ac.uk</a>> a écrit :<br>
><br>
> [ The Types Forum, <a href="http://lists.seas.upenn.edu/mailman/listinfo/types-list" rel="noreferrer" target="_blank">http://lists.seas.upenn.edu/<wbr>mailman/listinfo/types-list</a> ]<br>
><br>
</span><div class="HOEnZb"><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>
</div></div><div class="HOEnZb"><div class="h5">> The University of Edinburgh is a charitable body, registered in<br>
> Scotland, with registration number SC005336.<br>
<br>
</div></div></blockquote></div><br></div>