Confusion about the operational semantics of the let binding (LET rule) in the STG language

Yes, that’s the prime drawback of big-step semantics. But fortunately you can represent infinite derivation trees via coinduction, as in [0808.0586] Coinductive big-step operational semantics.

Is this useful? It depends on what you want to achieve…

I’m currently working on so-called denotational interpreters. It’s an interpreter written in Haskell with particularly nice properties; it generates (potentially infinite) small-step traces, for example. Jump straight to Section 4 in here if that’s something you might find interesting. It’s an early draft that I haven’t really shared with anyone yet, so don’t feel discouraged if you can’t grok it (yet).

3 Likes