[TYPES] Progress + Preservation = Evaluation

[Philip Wadler]

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

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Too brief? Here's why: http://www.emailcharter.org/

On 6 July 2018 at 17:57, Pierre Courtieu <pierre.courtieu at gmail.com> wrote:

> Hi,
>
> I think this is now well known as the "fuel" pattern. Ideally n is
> very big and computed lazily.
>
> I am not aware of a paper specifically about this trick, it is there
> as a very useful folklore I guess.
>
> Note however that Bertot Balaa presented a more "complete" version of
> this by refining this trick: the function itself is defined by means
> of a proof that there exists a number N of iterations such that any
> greater number would give the same result. i.e. that N is a sufficient
> fuel to reach the fixpoint. This mechanism is used in the current
> implementation of the "Function" command in coq (when given a non
> structurally recursive function).
>
> http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.
> 28.601&rep=rep1&type=pdf
>
> Best,
> Pierre
> Le ven. 6 juil. 2018 à 21:28, Philip Wadler <wadler at inf.ed.ac.uk> a écrit
> :
> >
> > [ The Types Forum, http://lists.seas.upenn.edu/
> mailman/listinfo/types-list ]
> >
> > Everyone on this list will be familiar with Progress and Preservation
> > for terms in a typed calculus.  Write ∅ ⊢ M : A to indicate that term
> > M has type A for closed M.
> >
> >   Progress.  If ∅ ⊢ M : A then either M is a value or M —→ N,
> >   for some term N.
> >
> >   Preservation.  If ∅ ⊢ M : A and M —→ N then ∅ ⊢ N : A.
> >
> > It is easy to combine these two proofs into an evaluator.
> > Write —↠ for the transitive and reflexive closure of —→.
> >
> >   Evaluation.  If ∅ ⊢ M : A, then for every natural number n,
> >   either M —↠ V, where V is a value and the reduction sequence
> >   has no more than n steps, or M —↠ N, where N is not a value
> >   and the reduction sequence has n steps.
> >
> > Evaluation implies that either M —↠ V or there is an infinite
> > sequence M —→ M₁ —→ M₂ —→ ... that never reduces to a value;
> > but this last result is not constructive, as deciding which of
> > the two results holds is not decidable.
> >
> > An Agda implementation of Evaluation provides an evaluator for terms:
> > given a number n it will perform up to n steps of evaluation, stopping
> > early if a value is reached. This is entirely obvious (at least in
> > retrospect), but I have not seen it written down anywhere. For
> > instance, this approach is not exploited in Software Foundations to
> > evaluate terms (it uses a normalize tactic instead).  I have used it
> > in my draft textbook:
> >
> >   https:plfa.inf.ed.ac.uk
> >
> > Questions: What sources in the literature should one cite for this
> > technique?  How well-known is it as folklore? Cheers, -- P
> >
> >
> > .   \ Philip Wadler, Professor of Theoretical Computer Science,
> > .   /\ School of Informatics, University of Edinburgh
> > .  /  \ and Senior Research Fellow, IOHK
> > . http://homepages.inf.ed.ac.uk/wadler/
> >
> > Too brief? Here's why: http://www.emailcharter.org/
> > The University of Edinburgh is a charitable body, registered in
> > Scotland, with registration number SC005336.
>
>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-list/attachments/20180706/ca7f24fe/attachment.ksh>