<div dir="ltr">I like the big-step normalization approach in terms of OPE's (order preserving embeddings)<div>and environment closures used in James Chapman's thesis:</div><div><a href="https://jmchapman.github.io/papers/tait2.pdf">https://jmchapman.github.io/papers/tait2.pdf</a><br></div><div><br></div><div>Chantal and Thorsten's Agda version of using hereditary substitution via a canonical</div><div>term syntax is also great, but it is more difficult to scale to additional typing constructs:</div><div><a href="http://www.cs.nott.ac.uk/~psztxa/publ/msfp10.pdf">http://www.cs.nott.ac.uk/~psztxa/publ/msfp10.pdf</a><br></div><div><br></div><div>I'm also fond of some work I did extending James' work to define weak-head</div><div>normal forms independently of expressions (by embedding other weak-head normal</div><div>forms in closures, rather than expressions, and then defining the semantics as a</div><div>version of a hereditary substituiton-based environment machine).</div><div>Here is the code, which uses a normalization function as the semantics:</div><div><a href="https://github.com/larrytheliquid/sbe/blob/master/src/SBE/Intrinsic.agda">https://github.com/larrytheliquid/sbe/blob/master/src/SBE/Intrinsic.agda</a><br></div><div>And a technical report explaining it:</div><div><a href="http://www.larrytheliquid.com/drafts/sbe.pdf">http://www.larrytheliquid.com/drafts/sbe.pdf</a></div><div><br></div><div>I also made a more serious version, closer to what appears in James' thesis,</div><div>where the semantics is presented relationally + logical relations proofs,</div><div>here is the code but I haven't had a chance to write about it:</div><div><a href="https://gist.github.com/larrytheliquid/6e7e9535d8f85f7a002f40f3d196cdc6">https://gist.github.com/larrytheliquid/6e7e9535d8f85f7a002f40f3d196cdc6</a><br></div><div><br></div><div>There is also a more efficient version that lazily computes conversion of weak-head </div><div>normal forms by only expanding closures when necessary:</div><div><a href="https://gist.github.com/larrytheliquid/b2a9171fea3aa4e461ef3181f8ca6889">https://gist.github.com/larrytheliquid/b2a9171fea3aa4e461ef3181f8ca6889</a><br></div><div><br></div><div><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial">The nice thing about this approach is that you can define weak-head normal</div><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial">forms to be your "core" language, and then expose all the primitives in terms</div><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial">of a much simpler LF-like expression "surface" language with only the function</div><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial">type intro + elim rules (then you expose the intro + elim rules of other types</div><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial">via an initial environment, which may use your core language constructs).</div><br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Mar 30, 2018 at 1:36 PM, Philip Wadler <span dir="ltr"><<a href="mailto:wadler@inf.ed.ac.uk" target="_blank">wadler@inf.ed.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Thanks very much, Nils!<div><br></div><div>No favourites from anyone else? That doesn't seem much like this list!</div><div><br></div><div>Cheers, -- P</div></div><div class="gmail_extra"><span class=""><br clear="all"><div><div class="m_-4725014655123517413gmail_signature" data-smartmail="gmail_signature"><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/<wbr>wadler/</a></span></div></div></div></div></div>
<br></span><div><div class="h5"><div class="gmail_quote">On 29 March 2018 at 12:19, 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>On 2018-03-29 14:31, Philip Wadler wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
My favourite denotational untyped solution so far is due to Nils Anders Danielsson:<br>
<br>
<a href="http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.Simplified.Delay-monad.Interpreter.html" rel="noreferrer" target="_blank">http://www.cse.chalmers.se/~na<wbr>d/listings/partiality-monad/La<wbr>mbda.Simplified.Delay-monad.In<wbr>terpreter.html</a><br>
<br>
It defines values as closures, a syntactic approach.<br>
</blockquote>
<br></span>
This definition is similar to a standard big-step operational semantics,<br>
and it is not defined compositionally (i.e. using recursion on the<br>
structure of terms). Hence I see this as an operational, rather than<br>
denotational, semantics. I made this argument in "Operational Semantics<br>
Using the Partiality Monad":<br>
<br>
<a href="http://www.cse.chalmers.se/~nad/publications/danielsson-semantics-partiality-monad.html" rel="noreferrer" target="_blank">http://www.cse.chalmers.se/~na<wbr>d/publications/danielsson-sema<wbr>ntics-partiality-monad.html</a><span><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
What would be even better is to define values semantically:<br>
<br>
data value where<br>
fun : (value -> Delay value) -> value<br>
<br>
But this does not work because value appears in a negative position.<br>
Is there a way to model a denotational description of values in Agda,<br>
perhaps by mimicking one of the constructions of domain theory?<br>
</blockquote>
<br></span>
In a typed setting you could perhaps define value by recursion on the<br>
structure of the types.<br>
<br>
Benton, Kennedy and Varming used the delay monad to define the lifting<br>
construction on ω-CPOs, and they used this to define a denotational<br>
semantics for an untyped language:<br>
<br>
Some Domain Theory and Denotational Semantics in Coq<br>
<a href="https://doi.org/10.1007/978-3-642-03359-9_10" rel="noreferrer" target="_blank">https://doi.org/10.1007/978-3-<wbr>642-03359-9_10</a><br>
<br>
There is also preliminary work in this direction that uses higher<br>
inductive types to define, roughly speaking, the delay monad quotiented<br>
by weak bisimilarity:<br>
<br>
Domain Theory in Type Theory via QIITs<br>
Altenkirch, Capriotti and Reus<br>
<a href="http://types2017.elte.hu/proc.pdf#page=24" rel="noreferrer" target="_blank">http://types2017.elte.hu/proc.<wbr>pdf#page=24</a><br>
<br>
Note that higher inductive types are not (yet?) supported directly by<br>
Agda.<br>
<br>
A different approach might be to use step-indexing. An alternative to<br>
that would be to use guarded recursive types, which would allow you to<br>
define something like value directly. However, I'm not aware of any<br>
mature implementations of guarded recursive types.<span class="m_-4725014655123517413HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
<br>
</font></span></blockquote></div><br></div></div></div>
<br>The University of Edinburgh is a charitable body, registered in<br>
Scotland, with registration number SC005336.<br>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature">Respectfully,<br>Larry Diehl<br></div>
</div>