Understanding Computation (55 page)

Now we can check for safety by seeing whether each concrete
computation’s result falls within the abstract computation’s
prediction:

>>
(
6
*
-
9
)
.
sign
<=
(
6
.
sign
*
-
9
.
sign
)
=> true
>>
(
-
5
+
0
)
.
sign
<=
(
-
5
.
sign
+
0
.
sign
)
=> true
>>
(
6
+
-
9
)
.
sign
<=
(
6
.
sign
+
-
9
.
sign
)
=> true

This safety property holds for any computation involving addition
and multiplication, because we’ve designed an abstraction that falls
back to a safe approximation when it can’t give a precise answer.

Incidentally, having access to this abstraction lets us do simple
analysis of Ruby code that adds and multiplies numbers. As an example,
here’s a method that sums the squares of its arguments:

def
sum_of_squares
(
x
,
y
)
(
x
*
x
)
+
(
y
*
y
)
end

If we want to automatically analyze this method to learn something about how it behaves,
we have a choice: we can treat it as a black box and run it for all possible arguments,
which would take forever, or we can inspect its source code and try to use mathematical
reasoning to deduce some of its properties, which is complicated. (And, in the general case,
doomed to failure because of Rice’s theorem
.) Abstract interpretation gives us the third option of calling the method with
abstract values to see what outputs are produced by an abstract version of the computation,
and it’s practical to do this for all possible inputs, because there are only a small number
of potential combinations of abstract values.

Each of the arguments
x
and
y
can be a negative, zero, or
positive number, so let’s see what the possible outputs can be:

>>
inputs
=
Sign
::
NEGATIVE
,
Sign
::
ZERO
,
Sign
::
POSITIVE
=> [#, #, #]
>>
outputs
=
inputs
.
product
(
inputs
)
.
map
{
|
x
,
y
|
sum_of_squares
(
x
,
y
)
}
=> [
#, #, #,
#, #, #,
#, #, #
]
>>
outputs
.
uniq
=> [#, #]

Without having done any clever analysis, this tells us that
#sum_of_squares
can only produce zero or positive numbers, never negative
numbers—a fairly boring property that’s obvious to an educated human reading the source
code, but not something that would be immediately evident to a machine. Of course, this kind
of trick only works for very simple code, but despite being a toy, it shows how abstraction
can make a difficult problem more
tractable.

Let’s make these ideas
concrete by building a type system for the
Simple
language from
Chapter 2
. Superficially,
this will look like a big-step operational semantics from
Big-Step Semantics
: we’ll implement a method on each of the classes representing the syntax of
Simple
programs (
Number
,
Add
, and so on), and calling the method will return a
final result. In the dynamic semantics, that method is called
#evaluate
, and its result is either a fully evaluated
Simple
value or an environment associating names with
Simple
values, depending on whether we evaluate an expression or a
statement:

>>
expression
=
Add
.
new
(
Variable
.
new
(
:x
),
Number
.
new
(
1
))
=> «x + 1»
>>
expression
.
evaluate
({
x
:
Number
.
new
(
2
)
})
=> «3»
>>
statement
=
Assign
.
new
(
:y
,
Number
.
new
(
3
))
=> «y = 3»
>>
statement
.
evaluate
({
x
:
Number
.
new
(
1
)
})
=> {:x=>«1», :y=>«3»}

For our static semantics, we’ll implement a different method that does less work and
returns a more abstract result. Instead of concrete values and environments, our abstract
values will be
types
. A type represents many possible values: a
Simple
expression can evaluate to a number or a Boolean,
so for expressions, our types will be “any number” and “any Boolean.” These types are
similar to the
Sign
values we saw earlier, especially
Sign::UNKNOWN
, which really does mean “any number.” As
with
Sign
, we can introduce types by defining a class
called
Type
and creating some instances:

class
Type
<
Struct
.
new
(
:name
)
NUMBER
,
BOOLEAN
=
[
:number
,
:boolean
].
map
{
|
name
|
new
(
name
)
}
def
inspect
"##{
name
}
>"
end
end

Our new method will return a type, so let’s call it
#type
. It’s supposed to answer a question: when this
Simple
syntax is evaluated, what type of value will it return? This is very easy
to implement for
Simple
’s
Number
and
Boolean
syntax classes, because
numbers and Booleans evaluate to themselves, so we know exactly what type of value we’ll
get:

class
Number
def
type
Type
::
NUMBER
end
end
class
Boolean
def
type
Type
::
BOOLEAN
end
end

For operations like
Add
,
Multiply
, and
LessThan
, it’s slightly more
complicated. We know that evaluating
Add
returns a
number, for example, but we also know that evaluation will only succeed if both arguments to
Add
also evaluate to a number, otherwise the
Simple
interpreter will fail with an error:

>>
Add
.
new
(
Number
.
new
(
1
),
Number
.
new
(
2
))
.
evaluate
({})
=> «3»
>>
Add
.
new
(
Number
.
new
(
1
),
Boolean
.
new
(
true
))
.
evaluate
({})
TypeError: true can't be coerced into Fixnum

How can we find out whether an argument will evaluate to a number? That’s what its type
tells us. So for
Add
, the rule is something like: if the
type of both arguments is
Type::NUMBER
, the type of the
overall result is
Type::NUMBER
; otherwise, the result is
no type at all, because the evaluation of any expression that tries to add nonnumeric values
will fail before it can return anything. For simplicity, we’ll let the
#type
method return
nil
to
indicate this failure, although in other circumstances, we might have chosen to raise an
exception or return some special error value instead (
Type::ERROR
, for instance) if that made the overall implementation more
convenient.

The code for
Add
looks like
this:

class
Add
def
type
if
left
.
type
==
Type
::
NUMBER
&&
right
.
type
==
Type
::
NUMBER
Type
::
NUMBER
end
end
end

The implementation of
Multiply#type
is identical, and
LessThan#type
is very similar, except that it returns
Type::BOOLEAN
instead of
Type::NUMBER
:

class
LessThan
def
type
if
left
.
type
==
Type
::
NUMBER
&&
right
.
type
==
Type
::
NUMBER
Type
::
BOOLEAN
end
end
end

On the console, we can see that this is enough to distinguish between expressions that
will evaluate successfully and those that won’t, even though the syntax of
Simple
allows both:

>>
Add
.
new
(
Number
.
new
(
1
),
Number
.
new
(
2
))
.
type
=> #
>>
Add
.
new
(
Number
.
new
(
1
),
Boolean
.
new
(
true
))
.
type
=> nil
>>
LessThan
.
new
(
Number
.
new
(
1
),
Number
.
new
(
2
))
.
type
=> #
>>
LessThan
.
new
(
Number
.
new
(
1
),
Boolean
.
new
(
true
))
.
type
=> nil

>>
bad_expression
=
Add
.
new
(
Number
.
new
(
true
),
Number
.
new
(
1
))
=> «true + 1»
>>
bad_expression
.
type
=> #
>>
bad_expression
.
evaluate
({})
NoMethodError: undefined method `+' for true:TrueClass