[r6rs-discuss] Re: operational or denotational semantics?

From: William D Clinger <will>
Date: Sun Feb 25 22:14:08 2007

Since Robby Findler (wisely?) declined to say much,
I'll play the fool again.

Thomas Lord wrote:
> I'm not sure if you are trying to say that the math is too hard
> or the required labor too great.

Probably both. As for the math, see below.

> 1. Denotational semantics, its "least fixpoint" approach,
> is the best account we have of meaning, in programming
> languages.

Not too many people would agree with that unqualified
statement. Denotational and least fixpoint semantics
may be the best accounts for some purposes, but SFAIK
(and I used to know quite a bit about this) they don't
work very well for languages with non-flat domains (e.g.
higher order functions) and nondeterministic semantics.
In other words, they don't work very well for Scheme.
To simplify the technical problem only slightly, it's
hard to define an adequate ordering relation that
won't conflate the possible results x and y with all
possible results that lie between x and y in the
ordering.

You can work around that somewhat by using operational
denotations, but that approach tends to have all of
the disadvantages and none of the advantages of using
an operational approach. That is why the editors
asked Robby Findler and Jacob Matthews to write an
operational semantics for R6RS, replacing the
denotational semantics of previous reports.

As for the observably sequential functions, they
form a proper subspace of the continuous function
domains that are normally used in denotational
semantics. They exclude things like parallel or,
which have to do with the failure of the obvious
denotational semantics for deterministic Lisp-like
languages to be fully abstract. Robby and Matthias
have been using observably sequential functions in
their research, and may have some results or
speculation that might bear on the problem; you'd
have to ask them, as I have just told you almost
all I know about observably sequential functions.

Will
Received on Sun Feb 25 2007 - 22:14:03 UTC