<div dir="ltr"><div>Addendum: This is what I mean by Sestoft-style: <a href="http://www.itu.dk/~sestoft/papers/amlazy.pdf">http://www.itu.dk/~sestoft/papers/amlazy.pdf</a> </div><div>This describes the simplest possible small-step transition semantics for call-by-need (discounting ADTs). </div><div>If you don't care about all the transitions, it might be simpler to switch to a *contextual* semantics instead, which express stack, heap and environment simply as an evaluation context. Then you might want to look at this work by Ariola et al.: <a href="https://dl.acm.org/doi/10.1145/199448.19950">https://dl.acm.org/doi/10.1145/199448.19950</a>, who first figured out what the evaluation contexts for call-by-need are.</div><div>The advantage of contextual semantics is that you need far fewer "search transitions" that just push stack frames or add heap bindings to find the next redex. </div><div>This style harmonises well with proofs by induction on evaluation contexts, which you often do to show program equivalence. <br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Am So., 26. Mai 2024 um 14:18 Uhr schrieb Sebastian Graf <<a href="mailto:sgraf1337@gmail.com">sgraf1337@gmail.com</a>>:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>Hey Rodrigo,</div><div><br></div><div>With any kind of semantics, often the most important question is: What do you want to achieve with it?</div><div><br></div><div>Generally speaking, I think it would be tedious, but not all that hard, to define an STG-style semantics for Core that "simply" anfises on the fly.</div><div>I did that for example in my <a href="https://gitlab.haskell.org/ghc/ghc/-/blob/64ae8fff5239b7c2c58692ce3b0e03f63f01bca1/compiler/GHC/Core/Semantics.hs#L161" target="_blank">denotational interpreter for Core here</a>, generating a trace in a Sestoft-style small-step operational semantics.</div><div>It works quite well (until it encounters an import or a primop which I haven't implemented), see <a href="https://mastodon.online/@sgraf/111715016532134390" target="_blank">here</a>.</div><div>If you really insist on modelling the STG machine (the prime advantage of which is that it can be efficiently compiled to hardware), then you would need to figure out the manifest arity of functions before you put them in the heap, etc..<br></div><div>But even that should not be hard, taking the STG operational semantics from the <a href="https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/eval-apply.pdf" target="_blank">eval/apply paper</a>, which should be amenable to mechanised formalisation. It's still tedious unless you really need to observe some STG-specific detail in your work.</div><div><br></div><div>So yeah, what is your end goal here?</div><div><br></div><div>Cheers,</div><div>Sebastian<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Am So., 26. Mai 2024 um 14:03 Uhr schrieb Moritz Angermann <<a href="mailto:moritz.angermann@gmail.com" target="_blank">moritz.angermann@gmail.com</a>>:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="auto">I don’t know myself, but I would suggest reaching out to Csaba. I believe he might have a good grasp on the STG literature.</div><div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, 26 May 2024 at 7:40 PM, Rodrigo Mesquita <<a href="mailto:rodrigo.m.mesquita@gmail.com" target="_blank">rodrigo.m.mesquita@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Dear all,<br>
<br>
Do you know of any recent works on the STG?<br>
<br>
In particular, I am looking for a result connecting STG's execution and Core’s call-by-need semantics when written in structural operational semantics style.<br>
<br>
Nonetheless, I’m also interested in possibly more recent formulations of STG (e.g. a mechanized one?) beyond the original paper.<br>
<br>
Cheers<br>
Rodrigo Mesquita<br>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div></div>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>
</blockquote></div>