Understanding Computation (9 page)

We can
specify the denotational semantics of statements in a
similar way, although remember from the operational semantics that
evaluating a statement produces a new environment rather than a value.
This means that
Assign#to_ruby
needs
to produce code for a proc whose result is an updated environment
hash:

class
Assign
def
to_ruby
"-> e { e.merge({
#{
name
.
inspect
}
=> (
#{
expression
.
to_ruby
}
).call(e) }) }"
end
end

Again, we can check this on the console:

>>
statement
=
Assign
.
new
(
:y
,
Add
.
new
(
Variable
.
new
(
:x
),
Number
.
new
(
1
)))
=> «y = x + 1»
>>
statement
.
to_ruby
=> "-> e { e.merge({ :y => (-> e { (-> e { e[:x] }).call(e) + (-> e { 1 }).call(e) })
.call(e) }) }"
>>
proc
=
eval
(
statement
.
to_ruby
)
=> #
>>
proc
.
call
({
x
:
3
})
=> {:x=>3, :y=>4}

As always, the semantics of
DoNothing
is very simple:

class
DoNothing
def
to_ruby
'-> e { e }'
end
end

For conditional statements, we can translate
Simple
’s
«
if (
…
) {
…
} else {
…
}
» into a Ruby
if
…
then
…
else
…
end
, making sure that the environment gets to all
the places where it’s needed:

class
If
def
to_ruby
"-> e { if (
#{
condition
.
to_ruby
}
).call(e)"
+
" then (
#{
consequence
.
to_ruby
}
).call(e)"
+
" else (
#{
alternative
.
to_ruby
}
).call(e)"
+
" end }"
end
end

As in big-step operational semantics, we need to be careful about
specifying the sequence statement: the result of evaluating the first
statement is used as the environment for evaluating the second.

class
Sequence
def
to_ruby
"-> e { (
#{
second
.
to_ruby
}
).call((
#{
first
.
to_ruby
}
).call(e)) }"
end
end

And lastly, as with conditionals, we can
translate «
while
»
statements into procs that use Ruby
while
to repeatedly execute the body before
returning the final environment:

class
While
def
to_ruby
"-> e {"
+
" while (
#{
condition
.
to_ruby
}
).call(e); e = (
#{
body
.
to_ruby
}
).call(e); end;"
+
" e"
+
" }"
end
end

Even a simple «
while
» can have
quite a verbose denotation, so it’s worth getting the Ruby interpreter
to check that its meaning is
correct:

>>
statement
=
While
.
new
(
LessThan
.
new
(
Variable
.
new
(
:x
),
Number
.
new
(
5
)),
Assign
.
new
(
:x
,
Multiply
.
new
(
Variable
.
new
(
:x
),
Number
.
new
(
3
)))
)
=> «while (x < 5) { x = x * 3 }»
>>
statement
.
to_ruby
=> "-> e { while (-> e { (-> e { e[:x] }).call(e) < (-> e { 5 }).call(e) }).call(e);
e = (-> e { e.merge({ :x => (-> e { (-> e { e[:x] }).call(e) * (-> e { 3 }).call(e)
}).call(e) }) }).call(e); end; e }"
>>
proc
=
eval
(
statement
.
to_ruby
)
=> #
>>
proc
.
call
({
x
:
1
})
=> {:x=>9}

Having done
all this work, what does this denotational semantics
achieve? Its main purpose is to show how to translate
Simple
into Ruby, using the latter as a tool
to explain what various language constructs mean. This happens to give
us a way to execute
Simple
programs—because we’ve written the rules of the denotational semantics
in executable Ruby, and because the rules’ output is itself executable
Ruby—but that’s incidental, since we could have given the rules in plain
English and used some mathematical language for the denotations. The
important part is that we’ve taken an arbitrary language of our own
devising and converted it into a language that someone or something else
can understand.

To give this translation some explanatory power, it’s helpful to bring parts of the
language’s meaning to the surface instead of allowing them to remain implicit. For example,
this semantics makes the environment explicit by representing it as a tangible Ruby object—a
hash that’s passed in and out of procs—instead of denoting variables as real Ruby variables
and relying on Ruby’s own subtle scoping rules to specify how variable access works. In this
respect the semantics is doing more than just offloading all the explanatory effort onto
Ruby; it uses Ruby as a simple foundation, but does some extra work on top to show exactly
how environments are used and changed by different program constructs.

We saw earlier that operational semantics is about explaining a
language’s meaning by designing an interpreter for it. By contrast, the
language-to-language translation of denotational semantics is
like
a
compiler
: in this case, our
implementations of
#to_ruby
effectively compile
Simple
into Ruby.
None of these styles of semantics necessarily says anything about how to
efficiently
implement an interpreter or compiler
for a language, but they do provide an official baseline against which
the correctness of any efficient implementation can be judged.

These denotational definitions also show up in the wild. Older
versions of the Scheme standard use
denotational
semantics
to specify the core language, unlike the current
standard’s small-step operational semantics, and the development of
the XSLT document-transformation language was guided by
Philip Wadler’s denotational definitions of
XSLT
patterns
and
XPath
expressions
.

See
Semantics
for a
practical example of using denotational semantics to specify the meaning
of regular
expressions.

Our tour of formal
semantics hasn’t been especially formal. We haven’t paid
any serious attention to mathematical notation, and using Ruby as a
metalanguage has meant we’ve focused more on different ways of executing
programs than on ways of understanding them. Proper denotational
semantics is concerned with getting to the heart of programs’ meanings
by turning them into well-defined mathematical objects, with none of the
evasiveness of representing a
Simple
«
while
» loop
with a Ruby
while
loop.

On the other hand, while we only vaguely sketched denotational
semantics in Ruby, our approach to operational semantics is closer in
spirit to its formal presentation: our definitions of
#reduce
and
#evaluate
methods are really just Ruby
translations of
mathematical inference rules.

An important
application of formal semantics is to give an unambiguous specification of the
meaning of a programming language, rather than relying on more informal approaches like
natural-language specification documents and “specification by implementation.” A formal
specification has other uses too, such as proving properties of the language in general and
of specific programs in particular, proving equivalences between programs in the language,
and investigating ways of safely transforming programs to make them more efficient without
changing their behavior.

For example, since an operational semantics corresponds quite closely to the
implementation of an
interpreter, computer scientists can treat a suitable interpreter as an
operational semantics for a language, and then prove its correctness with respect to a
denotational semantics for that language—this means proving that there is a sensible
connection between the meanings given by the interpreter and those given by the denotational
semantics.

Denotational semantics has the advantage of being more abstract than operational
semantics, by ignoring the detail of how a program executes and concentrating instead on how
to convert it into a different representation. For example, this makes it possible to
compare two programs written in different languages, if a denotational semantics exists to
translate both languages into some shared representation.

This degree of abstraction can make denotational semantics seem
circuitous. If the problem is how to explain the meaning of a
programming language, how does translating one language into another get
us any closer to a solution? A denotation is only as good as its
meaning; in particular, a denotational semantics only gets us closer to
being able to actually execute a program if the denotation language has
some
operational
meaning, a semantics of its own
that shows how it may be executed instead of how to translate it into
yet another language.

Formal denotational semantics uses abstract mathematical objects, usually functions, to
denote programming language constructs like expressions and statements, and because
mathematical convention dictates how to do things like evaluate functions, this gives a
direct way of thinking about the denotation in an operational sense. We’ve taken the less
formal approach of thinking of a denotational semantics as a compiler from one language into
another, and in reality, this is how most programming languages ultimately get executed: a
Java program will get compiled into bytecode by
javac
,
the bytecode will get just-in-time compiled into x86 instructions by the Java virtual
machine, then a CPU will decode each x86 instruction into RISC-like microinstructions for
execution on a core…where does it end? Is it compilers, or virtual machines, all the way
down?

Of course programs do eventually execute, because the tower of
semantics finally bottoms out at an
actual
machine:
electrons in semiconductors, obeying the laws of
physics.
^[
19
]
A computer is a device for maintaining this precarious
structure, many complex layers of interpretation balanced on top of one
another, allowing human-scale ideas like multitouch gestures and
while
loops to be gradually
translated down into the physical universe of silicon and
electricity.

The semantic styles seen in this chapter go by many different
names. Small-step semantics is also known
as
structural operational
semantics
and
transition semantics
;
big-step semantics is more often called
natural semantics
or
relational semantics
; and denotational semantics
is also
called
fixed-point semantics
or
mathematical semantics
.

Other styles of formal semantics are available. One alternative is
axiomatic
semantics
,
which describes the meaning of a statement by making assertions about the state
of the abstract machine before and after that statement executes: if one assertion (the
precondition
) is initially true before the statement is executed,
then the other assertion (the
postcondition
) will be true afterward.
Axiomatic semantics is useful for verifying the correctness of programs: as statements are
plugged together to make larger programs, their corresponding assertions can be plugged
together to make larger assertions, with the goal of showing that an overall assertion about
a program matches up with its intended specification.

Although the details are different, axiomatic semantics is the
style that best characterizes the
RubySpec project
, an “executable
specification for the Ruby programming language” that uses RSpec-style
assertions to describe the behavior of Ruby’s built-in language
constructs, as well as its core and standard libraries. For example,
here’s a fragment of RubySpec’s description
of the
Array#<<
method:

describe
"Array#<<"
do
it
"correctly resizes the Array"
do
a
=
[]
a
.
size
.
should
==
0
a
<<
:foo
a
.
size
.
should
==
1
a
<<
:bar
<<
:baz
a
.
size
.
should
==
3
a
=
[
1
,
2
,
3
]
a
.
shift
a
.
shift
a
.
shift
a
<<
:foo
a
.
should
==
[
:foo
]
end
end