> On Feb 27, 2019, at 1:42 PM, Arthur Nunes-Harwitt <a...@cs.rit.edu> wrote:
>
> Dear Matthias,
>
> Would you be willing to share your thoughts about the history of
> denotational versus operational semantics in the report?
[[ This is probably totally off topic for the list. ]]
Denotational semantics emerged as the dominant form in the 70s and 80s,
especially in the functional/Lisp-y community, because it could express
everything and the function from Syntax to Meaning (Scott domains) looked like
an interpreter, which everybody (“”) knows how to read and possibly write.
BUT,
1. you typically want to use your semantics for something (e.g. a proof that
what you wrote down has certain properties)
2. you want your semantics to have some resemblance to the design principles
(here, “Scheme as a lambda calculus …”)
The 1980s showed that using den. sem. for many common goals was hard (e.g. type
soundness proofs of ML; see Dams and Tofte’s work). In 1991, I worked with a
student (Andrew Wright) to explain how these proofs could be done more easily
with a form of operational semantics (an actual lambda calculus element) that I
developed for my dissertation.
The cool thing was that this new form of semantics looked as simple as the
original lambda calculus, handled assignments and continuations just fine, and
possessed the same mathematical properties as the original lambda calculus
(Church-Rosser, Curry-Feys).
By the time R6RS rolled around, Robby and his students had developed the Redex
language far enough that we could use it to model all of Scheme, first R5RS and
then R6RS (minus macros). By supplying an executable operational model, we
hoped implementors could use it as an independent source of truth for their own
work. We definitely have for many special corners of Racket and time and again
Matthew finds a discrepancy between our models and the implementation.
Sometimes we don’t trust the implementation and extend the model to cover this
corner just to see whether two rather different ways of looking at things help
us find the right way of doing things.
If you’re curious, see https://www2.ccs.neu.edu/racket/pubs/#popl12-kfff for
other examples.
--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
