Understanding Computation (53 page)

• Ask undecidable questions, but give up if an answer can’t be
  found. For example, to check whether a program prints a particular
  string, we can run it and wait; if it doesn’t print that string within
  a particular period of time, say 10 seconds, we just terminate the
  program and assume it’s no good. We might accidentally throw out a
  program that produces the expected output after 11 seconds, but in
  many cases that’s an acceptable risk, especially since slow programs
  can be undesirable in their own right.
  

• Ask several small questions whose answers, when taken together, provide empirical
  evidence for the answer to a larger question. When performing automated acceptance
  testing, we’re usually not able to check that a program does the right thing for every
  possible input, but we can try running it for a limited number of
  example
  inputs to see what happens. Each test run gives us
  information about how the program behaves in that specific case, and we can use that
  information to become more confident of how it’s likely to behave in general. This leaves
  open the possibility that there are other untested inputs that cause wildly different
  behavior, but we can live with that as long as our test cases do a good job of
  representing most kinds of realistic input.
  

  Another example of this approach is the use of unit tests to verify the behavior of
  small pieces of a program individually rather than trying to verify the program as a
  whole. A well-isolated unit test concentrates on checking the properties of a simple unit
  of code, and makes assumptions about other parts of the program by representing them with
  test doubles (i.e., stubs and mocks). Individual unit tests that exercise small pieces of
  well-understood code can be simple and fast, minimizing the danger that any one test will
  run forever or give a misleading answer.
  

  By unit testing all the program’s pieces in this way, we can set
  up a chain of assumptions and implications that resembles a
  mathematical proof: “if piece A works, then piece B works, and if
  piece B works, then piece C works.” Deciding whether all of these
  assumptions are justified is the responsibility of human reasoning
  rather than automated verification, although integration and
  acceptance testing can improve our confidence that the entire system
  does what it’s supposed to do.
  

• Ask decidable questions by being conservative where necessary. The above suggestions
  involve actually running parts of a program to see what happens, which always introduces
  the risk of hitting an infinite loop, but there are useful questions that can be answered
  just by inspecting a program’s source code statically. The most obvious example is “does
  this program contain any syntax errors?,” but we can answer more interesting questions if
  we’re prepared to accept safe approximations in cases where the real answer is
  undecidable.
  

  A common analysis is to look through a program’s source to see if it contains
  dead code
  that computes values that are never used, or
  unreachable code
  that
  never gets evaluated. We can’t always tell whether code is truly dead or
  unreachable, in which case we have to be conservative and assume it isn’t, but there are
  cases where it’s obvious: in some languages, we know that an assignment to a local
  variable that’s never mentioned again is definitely dead, and that a statement that
  immediately follows a
  return
is definitely unreachable.
  ^{[
  84
  ]}
  An optimizing compiler like GCC
  uses these techniques to identify and eliminate unnecessary code, making
  programs smaller and faster without affecting their behavior.
  

• Approximate a program by converting it into something simpler,
  then ask decidable questions about the approximation. This important
  idea is the subject of the
  next
  chapter
  .
  

^[
64
]
The smallest value
x
and
y
can reach is
1
, so they’ll meet there
if all else fails.

^[
65
]
Ruby already has a built-in version of Euclid’s algorithm,
Integer#gcd
, but that’s beside
the point.

^[
66
]
Lisp is really a family of programming languages—including
Common Lisp, Scheme, and Clojure—that share very similar
syntax.

^[
67
]
It would be more useful to only assign numbers to the
syntactically valid
Ruby programs, but doing
that is more complicated.

^[
68
]
Most of those numbers won’t represent syntactically valid Ruby programs, but we
can feed each potential program to the Ruby parser and reject it if it has any syntax
errors.

^[
69
]
We’re using Unix shell syntax here. On Windows, it’s necessary to omit the single
quotes around the argument to
echo
, or to put the
text in a file and feed it to
ruby
with the
<
input redirection operator.

^[
70
]
This is the shell command to run
does_it_say_no.rb
with its own source
code as input.

^[
71
]
We can only get away with this because parts B and C happen
not to contain any difficult characters like backslashes or
unbalanced curly brackets. If they did, we’d have to escape them
somehow and then undo that escaping as part of assembling the
value of
program
.

^[
72
]
Douglas Hofstadter coined the name
quine
for a program that
prints itself.

^[
73
]
Can you resist the urge to write a Ruby program that can
perform this transformation on any Ruby program? If you use
%q{}
to quote
data
’s value, how will you handle
backslashes and unbalanced curly brackets in the original
source?

^[
74
]
Briefly, for the curious: every pushdown automaton has an equivalent context-free
grammar and vice versa; any CFG can be rewritten in
Chomsky normal
form
; and any CFG in that form must take exactly 2
n
− 1
steps to generate a string of length
n
. So we can turn the original PDA
into a CFG, rewrite the CFG into Chomsky normal form, and then turn that CFG back into a
PDA. The resulting pushdown automaton recognizes the same language as the original, but
now we know exactly how many steps it’ll take to do it.

^[
75
]
The choice of the empty string is unimportant; it’s just an arbitrary fixed input.
The plan is to run
does_it_halt.rb
on
self-contained programs that don’t read anything from standard input, so it doesn’t
matter what
input
is.

^[
76
]
Faber’s million-dollar prize expired in 2002, but anyone who
produced a proof today would still be in for some serious fortune
and glory on the rock star mathematician circuit.

^[
77
]
This is reminiscent of
#evaluate_on_itself
from
Universal Systems Can Loop Forever
, with
#halts?
in place of
#evaluate
.

^[
78
]
Or equivalently: what does
#halts_on_itself?
return if we call it
with
do_the_opposite.rb
’s
source code as its argument?

^[
79
]
Surely “responsible software engineering professionals”?

^[
80
]
Again, that input might be irrelevant if the program doesn’t actually read anything
from
$stdin
, but we’re including it for the sake of
completeness and consistency.

^[
81
]
Total programming languages are a potential solution to this
problem, but so far they haven’t taken off, perhaps because they can
be more difficult to understand than conventional languages.

^[
82
]
Stephen Wolfram coined the name
computational
irreducibility
for the idea that a program’s
behavior can’t be predicted without running it.

^[
83
]
This is roughly the content of
Gödel’s
first incompleteness theorem
.

^[
84
]
The Java language specification requires the compiler to reject any program that
contains unreachable code. See
http://docs.oracle.com/javase/specs/jls/se7/html/jls-14.html#jls-14.21
for a
lengthy explanation of how a Java compiler is meant to decide which parts of a program
are potentially reachable without running any of it.

Suppose
you’re a tourist in an unfamiliar country and want to plan
a road trip to another town. How will you decide which route to take? A
direct solution is to jump into your rental car and drive in whichever
direction seems the most promising. Depending on how lucky you are, and
on how much help the foreign road signs give you, this brute-force
exploration of an unknown road network might eventually get you to your
destination. But it’s an expensive strategy, and it’s likely that you’ll
just get more and more lost until you give up completely.

Using a map to plan your trip is a much more sensible idea. A printed road atlas is an
abstraction that sacrifices a lot of the detail of the physical road network. It doesn’t
tell you what the traffic is like, which roads are currently closed, where individual
buildings are, or anything at all about the third dimension; it is, crucially, much smaller
and flatter than the real thing. But a map does retain the most important information
required for journey planning: the relative positions of all the towns, which roads lead to
each town, and how those roads are connected to each other.

Despite all of this missing detail, an accurate map is useful, because the route you
plan with it is likely to be valid in reality, not just in the abstract world of the map. A
cartographer has done the expensive work of creating a model of reality, giving you the
opportunity to perform a computation on that model by looking at a simplified representation
of the road network and planning your route on it. You can then transfer the result of that
computation back into the real world when you actually get in your car and drive to your
destination, allowing cheap decisions made in the abstract world of the map to prevent you
from having to make expensive decisions on the physical roads.

The approximations used by a map make navigational computations much easier without
fatally compromising the fidelity of their results. There are plenty of circumstances in
which decisions made with a map might turn out to be wrong—there is no guarantee that a map
has told you absolutely
everything
you need to know about your
journey—but planning your route in advance lets you rule out particular kinds of mistakes
and makes the whole problem of getting from one place to another much more
manageable.

Planning a route
with a printed map is a real application of abstract interpretation, but it’s
also very informal. For a more formal example, we can look at the multiplication of numbers;
although it’s still only a toy example, multiplication gives us a chance to start writing
code to investigate these ideas.

Pretend for a moment that multiplying two numbers is a difficult
or expensive operation, and that we’re interested in finding out some
information about the result of a multiplication without having to
actually perform it. Specifically: what is the
sign
of the result? Is it a negative number, zero, or a positive
number?

The notionally expensive way of finding out is to compute in the
concrete
world, using the
standard
interpretation
of multiplication: multiply the numbers for
real, look at the resulting number, and decide whether that result is
negative, zero, or positive. In Ruby, for example:

>>
6
*
-
9
=> -54

-54
is negative, so we’ve
learned that the product of
6
and
-9
is a negative number. Job
done.

However, it’s also possible to discover the same information by
computing in an
abstract
world, using an
abstract interpretation
of multiplication. Just
as a map uses lines on a flat page to represent roads in the real world,
we can use abstract values to represent numbers; we can plan a route on
a map instead of finding our way by trial and error on real roads, and
we can define an abstract multiplication operation on abstract values
instead of using concrete multiplication on concrete numbers.

To do this, we need to design abstract values that make the calculation simpler while
still retaining enough information to be a useful answer. We can take advantage of the fact
that the
absolute values
^[
86
]
of two multiplied numbers don’t make any difference to the sign of the
result:

>>
(
6
*
-
9
)
<
0
=> true
>>
(
1000
*
-
5
)
<
0
=> true
>>
(
1
*
-
1
)
<
0
=> true

As young children, we’re taught that it’s only the signs of the arguments that matter:
the product of two positive numbers, or two negative numbers, is always a positive number;
the product of one positive and one negative number is always negative; and the product of
zero with any other number is always zero.

So let’s use these different kinds of number—“negative,” “zero,”
and “positive”—as our abstract values. We can do this in Ruby by
defining a
Sign
class and creating
three instances of it:

class
Sign
<
Struct
.
new
(
:name
)
NEGATIVE
,
ZERO
,
POSITIVE
=
[
:negative
,
:zero
,
:positive
].
map
{
|
name
|
new
(
name
)
}
def
inspect
"##{
name
}
>"
end
end

This gives us Ruby objects that we can use as our abstract values:
Sign::NEGATIVE
represents “any
negative number,”
Sign::ZERO
represents “the number zero,” and
Sign::POSITIVE
represents “any positive
number.” These three
Sign
objects
make up the tiny abstract world where we’ll perform abstract
calculations, while our concrete world consists of the
virtually unlimited supply of Ruby integers.
^[
87
]

We can define abstract multiplication for
Sign
values by implementing just the
sign-related aspect of concrete multiplication:

class
Sign
def
*
(
other_sign
)
if
[
self
,
other_sign
].
include?
(
ZERO
)
ZERO
elsif
self
==
other_sign
POSITIVE
else
NEGATIVE
end
end
end

Instances of
Sign
can now be
“multiplied” together just like numbers, and our implementation of
Sign#*
produces answers that are
consistent with multiplication of actual numbers:

>>
Sign
::
POSITIVE
*
Sign
::
POSITIVE
=> #
>>
Sign
::
NEGATIVE
*
Sign
::
ZERO
=> #
>>
Sign
::
POSITIVE
*
Sign
::
NEGATIVE
=> #

For example, the last line above asks the question: what do we get
when we multiply any positive number by any negative number? The answer
comes back: a negative number. This is still a kind of multiplication,
but it’s much simpler than the kind we’re used to, and it only works on
“numbers” that have had almost all of their identifying information
removed. If we’re still imagining that real multiplication is expensive,
this seems like a cut-down version of multiplication that could be
considered cheap.

Armed with our abstract world of numbers and an abstract
interpretation of multiplication for those numbers, we can tackle the
original problem in a different way. Rather than multiplying two numbers
directly to find out the sign of their result, we can convert the
numbers into their abstract counterparts and multiply those instead.
First we need a way to convert concrete numbers into abstract
ones:

class
Numeric
def
sign
if
self
<
0
Sign
::
NEGATIVE
elsif
zero?
Sign
::
ZERO
else
Sign
::
POSITIVE
end
end
end

Now we can convert two numbers and do the multiplication in the
abstract world:

>>
6
.
sign
=> #
>>
-
9
.
sign
=> #
>>
6
.
sign
*
-
9
.
sign
=> #

Again we’ve calculated that
6 * -9
produces a
negative number, but this time we’ve done it without any multiplication of actual numbers.
Stepping up into the abstract world gives us an alternative way of performing the
computation, and crucially, the abstract result can be translated back down into the
concrete world so we can make sense of it, although we can only get an approximate concrete
answer because of the detail we sacrificed in making the abstraction. In this case, the
abstract result
Sign::NEGATIVE
tells us that any of the
concrete numbers
-1
,
-2
,
-3
, etc., might be the answer to
6 * -9
, but that the answer is definitely not
0
or any positive number like
1
or
500
.

Note that, because Ruby values are objects—data structures that
carry their operations with them—we can use the same Ruby expression to
perform either a concrete or an abstract computation depending on
whether we provide concrete (
Fixnum
)
or abstract (
Sign
) objects as
arguments. Take a
#calculate
method
that multiplies three numbers in a particular way:

def
calculate
(
x
,
y
,
z
)
(
x
*
y
)
*
(
x
*
z
)
end

If we call
#calculate
with
Fixnum
objects, the calculation will
be done by
Fixnum#*
and we’ll get a
concrete
Fixnum
result. If we call it
with
Sign
instances instead, the
Sign#*
operation will be used and
produce a
Sign
result.

>>
calculate
(
3
,
-
5
,
0
)
=> 0
>>
calculate
(
Sign
::
POSITIVE
,
Sign
::
NEGATIVE
,
Sign
::
ZERO
)
=> #

This gives us a limited opportunity to perform abstract
interpretation within real Ruby programs by replacing concrete arguments
with their abstract counterparts and running the rest of the code
without
modification.