<div dir="ltr">Thanks! I've saved your notes to review before revising the paper.<br><br>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.<br><br>Cheers, -- P<br></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 30 July 2018 at 19:15, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 2018-07-07 00:45, Philip Wadler wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Indeed, I considered using Delay for the evaluator in the textbook,<br>
but decided that supplying a step count was simpler, and avoided the<br>
need to explain coinduction.<br>
</blockquote>
<br></span>
In "Operational Semantics Using the Partiality Monad"<br>
(<a href="https://doi.org/10.1145/2364527.2364546" rel="noreferrer" target="_blank">https://doi.org/10.1145/23645<wbr>27.2364546</a>) I defined the semantics of an<br>
untyped language by giving a definitional interpreter, using the delay<br>
monad. Then I proved type soundness for this language as a negative<br>
statement (using a more positive lemma):<br>
<br>
  [] ⊢ t ∈ σ → ¬ (⟦ t ⟧ [] ≈ fail)<br>
<br>
Thus, instead of starting with type soundness and deriving an evaluator,<br>
I started with an evaluator and proved type soundness.<br>
<br>
This kind of exercise has also been performed using fuel, see Siek's<br>
"Type Safety in Three Easy Lemmas"<br>
(<a href="http://siek.blogspot.com/2013/05/type-safety-in-three-easy-lemmas.html" rel="noreferrer" target="_blank">http://siek.blogspot.com/2013<wbr>/05/type-safety-in-three-easy-<wbr>lemmas.html</a>)<br>
and "Functional Big-Step Semantics" by Owens et al.<br>
(<a href="https://doi.org/10.1007/978-3-662-49498-1_23" rel="noreferrer" target="_blank">https://doi.org/10.1007/978-3<wbr>-662-49498-1_23</a>).<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
<br>
</font></span></blockquote></div><br></div>