[Agda] [TYPES] Progress + Preservation = Evaluation

[Philip Wadler]

Thanks! I've saved your notes to review before revising the paper.

In "Functional Big-Step Semantics", one of the advantages is that one
immediately obtains an evaluator for terms. They note that sometimes a
small-step semantics also immediately gives an evaluator for terms, and
cite K and Redex as examples---suggesting, again, a lack of recognition
that any constructive proof of progress and preservation immediately gives
rise to 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 30 July 2018 at 19:15, Nils Anders Danielsson <nad at cse.gu.se> wrote:

> On 2018-07-07 00:45, Philip Wadler wrote:
>
>> Indeed, I considered using Delay for the evaluator in the textbook,
>> but decided that supplying a step count was simpler, and avoided the
>> need to explain coinduction.
>>
>
> In "Operational Semantics Using the Partiality Monad"
> (https://doi.org/10.1145/2364527.2364546) I defined the semantics of an
> untyped language by giving a definitional interpreter, using the delay
> monad. Then I proved type soundness for this language as a negative
> statement (using a more positive lemma):
>
>   [] ⊢ t ∈ σ → ¬ (⟦ t ⟧ [] ≈ fail)
>
> Thus, instead of starting with type soundness and deriving an evaluator,
> I started with an evaluator and proved type soundness.
>
> This kind of exercise has also been performed using fuel, see Siek's
> "Type Safety in Three Easy Lemmas"
> (http://siek.blogspot.com/2013/05/type-safety-in-three-easy-lemmas.html)
> and "Functional Big-Step Semantics" by Owens et al.
> (https://doi.org/10.1007/978-3-662-49498-1_23).
>
> --
> /NAD
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180731/77f0a749/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180731/77f0a749/attachment.ksh>