Denotaional Semantics
Peter Keller
I'm learning more deeply denotational/operational/axiomatic semantics
and have a question.
What kind of language bugs are discovered by using these methods? For
example, if someone wrote a denotational semantics for perl, what kind
of a problem could be discovered by doing so?
Thank you.
-pete
William D Clinger
First, I don't think formal semantics should be regarded
technique for debugging languages; it's more of a tool
for designing languages, and especially for enabling all
sorts of desirable things.
For example, you'd like to have some basis for believing
that a programmer's intent bears some relationship to an
implementation's behavior, or that multiple implementations
of the language have something in common. That's pretty
basic.
But formal semantics can help to uncover some bugs in
language designs, such as:
* inconsistencies within informal specifications
* inconsistencies within informal expectations
* unintended ambiguities or unspecified behavior
* redundant or unnecessarily complex features
* unanticipated or hidden complexity
For an example of hidden complexity within a real language,
see The Java Language Specification, Third Edition,
chapter 17, especially section 17.4 [1].
Then consider all the other languages that have similar
features but no formal specification of them. The absence
of a formal semantics doesn't make the complexity go away;
it just hides the truth from programmers and implementors.
In particular, programmers who have no formal semantics to
go by probably have no clear idea of which behaviors they
can rely upon, so they mistakenly rely on behaviors that
are not actually guaranteed by the language and its
implementations. Then they wonder why their code stops
working when there's a new version of the hardware or OS
or compiler or interpreter.
Will
Peter Keller
> First, I don't think formal semantics should be regarded
> technique for debugging languages; it's more of a tool
> for designing languages, and especially for enabling all
> sorts of desirable things.
I agree with you in your statement, but it seems (from a moderate glance
at google) that most denotational semantic descriptions for languages
happens after the fact if at all. Is this usually the case?
> Then consider all the other languages that have similar
> features but no formal specification of them. The absence
> of a formal semantics doesn't make the complexity go away;
> it just hides the truth from programmers and implementors.
> In particular, programmers who have no formal semantics to
> go by probably have no clear idea of which behaviors they
> can rely upon, so they mistakenly rely on behaviors that
> are not actually guaranteed by the language and its
> implementations. Then they wonder why their code stops
> working when there's a new version of the hardware or OS
> or compiler or interpreter.
I see. So it would be fair to say that the purpose of a denotational
semantics for a language is that it formally encompases *ALL* meaning
of every possible construct of the language? Would it be true that if an
implementation did not constrain itself to the denotational semantics,
therefore adding/subtracting meaning from the language, the implementation
would be in error?
Thank you.
-pete
William D Clinger
> I agree with you in your statement, but it seems (from a moderate glance
> at google) that most denotational semantic descriptions for languages
> happens after the fact if at all. Is this usually the case?
Yes, but the evolving design of Scheme and several other
languages has been influenced by a denotational or other
formal semantics.
The first denotational semantics for Scheme was developed
by Muchnik and Pleban and published at the 1980 Lisp
Conference. That semantics and its successors have had a
lot of influence. That's why most Scheme programmers have
at least some understanding of environments, continuations,
and the distinctions between locations, denoted values, and
expressed values. Without that shared vocabulary, it would
be hard even to talk about some of the design choices that
came up during the R6RS process.
> I see. So it would be fair to say that the purpose of a denotational
> semantics for a language is that it formally encompases *ALL* meaning
> of every possible construct of the language?
That's *a* purpose, certainly, although it is sometimes
more of an aspiration than a reality.
> Would it be true that if an implementation did not constrain
> itself to the denotational semantics, therefore
> adding/subtracting meaning from the language, the
> implementation would be in error?
Not necessarily, and not usually. For that purpose, a
mathematical semantics must be combined with some kind
of prescriptive statement.
Consider, for example, a simple operational semantics.
It may specify several possible results for a program,
and it may describe several possible derivations of each
result. Must every implementation deliver every possible
result? Must every implementation mimic every possible
derivation of every possible result? Maybe it's enough
for implementations to deliver one of the many possible
results, and maybe it's unimportant whether they get the
result through mimicry or some completely different
computational process. Someone has to explain how the
semantics is intended to constrain implementations.
Will
Peter Keller
>> Would it be true that if an implementation did not constrain
>> itself to the denotational semantics, therefore
>> adding/subtracting meaning from the language, the
>> implementation would be in error?
>
> Not necessarily, and not usually. For that purpose, a
> mathematical semantics must be combined with some kind
> of prescriptive statement.
>
> Consider, for example, a simple operational semantics.
> It may specify several possible results for a program,
> and it may describe several possible derivations of each
> result. Must every implementation deliver every possible
> result? Must every implementation mimic every possible
> derivation of every possible result? Maybe it's enough
> for implementations to deliver one of the many possible
> results, and maybe it's unimportant whether they get the
> result through mimicry or some completely different
> computational process. Someone has to explain how the
> semantics is intended to constrain implementations.
I understand.
So, given a denotational/operational semantics for a programming language,
is there an analogous semantics for the implementation of the semantics?
What I mean specifically is suppose I have something (roughly) like this:
I is a member of domain Location, (or variables names)
c is a member of domain CMD, the domain of commands/statements
<c,s> -> s'
So, given this derivation:
<I := 5, s> -> s[5/I]
(Hopefully the symbols and syntax I'm using is familiar to you! I've
just barely learned them.)
Notice the semantics say nothing of the actual representation of s or
how it gets changed, only that 5 should be substituted for I in s.
s could be implemented as a hash table (in the tiny example from above)
with elements of domain Location as keys and elements of domain Values
as values. Or, it could be implemented in some completely other way that
functionally behaves the same way.
Is there some formal method of writing down the implementation of the
semantics? At a 10,000 foot level, how can I be sure that I'm implementing
the semantics correctly, and can I prove an implementation follows the
semantics?
The reason I ask is because if I implement the semantics in a language like
C, which has undefined sections in the language (and suppose I hit them
unintentionally), then how did the original denotational/operational semantics
help me? In the end, I get unexpected meaning/behavior anyway....
I'm sorry if these are odd questions, but I'm just trying to get a handle
on why formal semantics is important and how it really helps language
designers and implementors.
Thank you.
-pete
William D Clinger
> So, given a denotational/operational semantics for a programming
> language, is there an analogous semantics for the implementation
> of the semantics?
Yes. The implementation's semantics is usually more specific
and more detailed than the language's semantics, but there
should be one or more theorems that relate the two semantics.
Your example of treating a state as a function in the language's
semantics, but as a hash table in an implementation's semantics,
is exactly the sort of difference we're talking about.
> Is there some formal method of writing down the implementation of the
> semantics? At a 10,000 foot level, how can I be sure that I'm implementing
> the semantics correctly, and can I prove an implementation follows the
> semantics?
Let me recommend four papers:
Oliver Danvy. Towards compatible and interderivable semantic
specifications for the Scheme programming language, part I:
abstract machines, natural semantics, and denotational semantics.
Online at http://www.schemeworkshop.org/2008/program.html
Małgorzata Biernacka, Olivier Danvy. Towards compatible and
interderivable semantic specifications for the Scheme programming
language, part II: reduction semantics and abstract machines.
Online at http://www.schemeworkshop.org/2008/program.html
William Clinger. The Scheme 311 compiler: an exercise in
denotational semantics. In the conference record of the
1984 ACM symposium on Lisp and Functional Programming, pages
356-364. http://portal.acm.org/citation.cfm?id=800055.802052
Joshua D Guttman and Mitchell Wand, editors. VLISP: a Verified
Implementation of Scheme. Kluwer, Boston, 1995. Originally
published as a special double issue of Lisp and Symbolic
Computation, 1995, Volume 8, Issue 1/2. May be online at
ftp://ftp.ccs.neu.edu/pub/people/wand/vlisp/lasc
The first two papers above were presented at last year's Scheme
workshop. I'm presenting an updated version of the third paper
at the MitchFest on Sunday, so this stuff happens to be on my
mind at the moment.
Will
Peter Keller
>> So, given a denotational/operational semantics for a programming
>> language, is there an analogous semantics for the implementation
>> of the semantics?
>
> Yes. The implementation's semantics is usually more specific
> and more detailed than the language's semantics, but there
> should be one or more theorems that relate the two semantics.
>
> Your example of treating a state as a function in the language's
> semantics, but as a hash table in an implementation's semantics,
> is exactly the sort of difference we're talking about.
>
>> Is there some formal method of writing down the implementation of the
>> semantics? At a 10,000 foot level, how can I be sure that I'm implementing
>> the semantics correctly, and can I prove an implementation follows the
>> semantics?
>
> Let me recommend four papers:
[snip]
Those look very interesting! Thank you very much and I appreciate your
time and responses.
This is the book from which I've begun learning formal semantics:
I mention it so you know what viewpoint I have on the subject.
My goal in learning this material is two fold: A) to understand how
to take two different language's semantics and write a "translation
semantics" which dictate formally how to translate the meaning of one
language into another language, and B) to be able to take a concrete
denotational semantics of a language, and add annotation denotions which
describe the meanings/symbols used for auto-generation of a symbolic
debugger for the language.
It is for some hobby compiler work I'm doing.
Thank you.
-pete