[Agda] Progress + Preservation = Evaluation

[Philip Wadler]

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:

Progress + Preservation = Evaluation.
>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.]

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.

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 plfa.inf.ed.ac.uk --- do have
a look!)

To repeat my 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/

On 6 July 2018 at 12:49, Philip Wadler <wadler at inf.ed.ac.uk> wrote:

> 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/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180706/88137949/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180706/88137949/attachment.ksh>