[Agda] [TYPES] Progress + Preservation = Evaluation

[Eelco Visser]

Hi Phil,

The idea of using fuel to model non-termination is pretty well known
and at least used in the following recent papers:

Type Soundness Proofs with Definitional Interpreters. Amin, Rompf
https://popl17.sigplan.org/event/popl-2017-papers-from-f-to-dot-type-soundness-proofs-with-definitional-interpreters

Intrinsically-Typed Definitional Interpreters for Imperative
Languages. Bach Poulsen, Rouvoet, Tolmach, Krebbers, Visser.
https://popl18.sigplan.org/event/popl-2018-papers-intrinsically-typed-definitional-interpreters-for-imperative-languages

See the related work of the latter for more references.

Note that the latter paper uses Agda as well.

cheers,

-- Eelco

On Fri, Jul 6, 2018 at 5:49 PM, Philip Wadler <wadler at inf.ed.ac.uk> wrote:
> [ 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.
>



-- 
Professor of Computer Science, TU Delft

http://eelcovisser.org