We began the rational-number implementation in
section 2.1.1 by implementing the
rational-number operations
add_rat,
sub_rat,
and so on in terms of three unspecified
functions:
make_rat,
numer, and
denom. At that point, we could think of the
operations as being defined in terms of data objects—numerators,
denominators, and rational numbers—whose behavior was specified
by the latter three
functions.
But exactly what is meant by data? It is not enough to say
whatever is implemented by the given selectors and
constructors. Clearly, not every arbitrary set of three
functions
can serve as an appropriate basis for the rational-number
implementation. We need to guarantee that,
if we construct a rational number x from a
pair of integers n and
d, then extracting the
numer and the
denom of x and
dividing them should yield the same result as dividing
n by d. In
other words,
make_rat,
numer, and
denom must satisfy the condition that, for
any integer n and any nonzero
integer d, if x is
make_rat(n, d),
then
In fact, this is the only condition
make_rat,
numer, and
denom must fulfill in order to form a
suitable basis for a rational-number representation. In general, we can
think of data as defined by some collection of selectors and
constructors, together with specified conditions that these
functions
must fulfill in order to be a valid
representation.
This point of view can serve to define not only
high-level data objects, such as rational numbers, but
lower-level objects as well.
Consider the notion of a
Consider the notion of a
pair, which we used in order to define our
rational numbers. We never actually said what a pair was, only that
the language supplied
functions
pair,
head,
and
tail
for operating on pairs. But the only thing we need to know about these
three operations
is that if we glue two objects together using
pair
we can retrieve the objects using
head
and
tail.
That is, the operations satisfy the condition that, for any objects
x and y, if
z is
pair(x, y)
then
head(z)
is x and
tail(z)
is y. Indeed, we mentioned that these three
functions
are included as primitives in our language. However, any triple of
functions
that satisfies the above condition can be used as the basis for
implementing pairs. This point is illustrated strikingly by the fact
that we could implement
pair,
head,
and
tail
without using any data structures at all but only using
functions.
Here are the definitions:
function pair(x, y) {
function dispatch(m) {
return m === 0
? x
: m === 1
? y
: error(m, "argument not 0 or 1 -- pair");
}
return dispatch;
}
function head(z) { return z(0); }
function tail(z) { return z(1); }
This use of
functions
corresponds to nothing like our intuitive notion of what data should be.
Nevertheless, all we need to do to show that this is a valid way to
represent pairs is to verify that these
functions
satisfy the condition given above.
The subtle point to notice is that the value returned by
pair(x, y)
is a
function—namely
the internally defined
function
dispatch, which takes one argument and returns
either x or y
depending on whether the argument is 0 or 1. Correspondingly,
head(z)
is defined to apply z to 0. Hence, if
z is the
function
formed by
pair(x, y),
then z applied to 0 will yield
x. Thus, we have shown that
head(pair(x, y))
yields x, as desired. Similarly,
tail(pair(x, y))
applies the
function
returned by
pair(x, y)
to 1, which returns y.
Therefore, this
functional
implementation of pairs is a valid
implementation, and if we access pairs using only
pair,
head,
and
tail
we cannot distinguish this implementation from one that uses
real data structures.
The point of exhibiting the
functional
representation of pairs is not that our language works this way
(an efficient implementation of pairs
might use JavaScript's native
vector data structure)
but that it could work this way. The
functional
representation, although obscure, is a perfectly adequate way to represent
pairs, since it fulfills the only conditions that pairs need to fulfill.
This example also demonstrates that the ability to manipulate
functions
as objects automatically provides the ability to represent compound data.
This may seem a curiosity now, but
functional
representations of data will play a central role in our programming
repertoire. This style of programming is often called
message passing, and we will be using it as a basic tool in
chapter 3 when we address the issues of modeling and simulation.
Show that we can represent pairs of nonnegative integers using only
numbers and arithmetic operations if we represent the pair
$a$ and $b$ as the
integer that is the product $2^a 3^b$. Give the
corresponding definitions of the
functions
pair,
head,
and
tail.
In case representing pairs as
functions
(exercise 2.4)
wasn't mind-boggling enough, consider that, in a language that can
manipulate
functions,
we can get by without numbers (at least insofar as nonnegative integers
are concerned) by implementing 0 and the operation of adding 1 as
const zero = f => x => x;
function add_1(n) {
return f => x => f(n(f)(x));
}
This representation is known as
Church numerals, after its inventor,
Alonzo Church, the logician who invented the
$\lambda$ calculus.
この表現は、$\lambda$計算を発明した論理学者
Alonzo Church にちなんで、
チャーチ数として知られています。
Define one and two
directly (not in terms of zero and
add_1).
(Hint: Use substitution to evaluate
add_1(zero)).
Give a direct definition of the addition
function plus
(not in terms of repeated application of
add_1).
const one = f => x => f(x);
const two = f => x => f(f(x));
function plus(n, m) {
return f => x => n(f)(m(f)(x));
}
// testing
const three = plus(one, two);
function church_to_number(c) {
return c(n => n + 1)(0);
}
church_to_number(three);
Surprisingly, this idea is very difficult to
formulate rigorously. There are two approaches to giving such a
formulation. One, pioneered by
C. A. R. Hoare (1972), is known as the method of
abstract models. It formalizes the
functions plus conditions
specification as outlined in the rational-number example above. Note
that the condition on the rational-number representation was stated in
terms of facts about integers (equality and division). In general,
abstract models define new kinds of data objects in terms of previously
defined types of data objects. Assertions about data objects can
therefore be checked by reducing them to assertions about previously
defined data objects. Another approach, introduced by
Zilles at MIT, by
Goguen,
Thatcher,
Wagner, and
Wright at IBM (see Thatcher, Wagner, and Wright
1978), and by
Guttag at Toronto (see Guttag 1977),
is called
algebraic specification. It regards the
functions
as elements of an abstract algebraic system whose behavior is
specified by axioms that correspond to our conditions,
and uses the techniques of abstract algebra to check assertions about
data objects. Both methods are surveyed in the paper by
Liskov and Zilles
(1975).
驚くべきことに、この考えを厳密に定式化するのは非常に困難です。そのような定式化には2つのアプローチがあります。1つは、
C. A. R. Hoare(1972)が開拓した、
抽象モデルの方法として知られるものです。これは、上記の有理数の例で概説した関数と条件の仕様を形式化します。有理数の表現に対する条件は、整数に関する事実(等値と除算)の観点から述べられていたことに注目してください。一般に、抽象モデルは、以前に定義されたデータオブジェクトの型の観点から新しい種類のデータオブジェクトを定義します。したがって、データオブジェクトに関する表明は、以前に定義されたデータオブジェクトに関する表明に帰着することで検証できます。もう1つのアプローチは、MIT の
Zilles、IBM の
Goguen、
Thatcher、
Wagner、
Wright(Thatcher, Wagner, and Wright 1978を参照)、およびトロントの
Guttag(Guttag 1977を参照)によって導入された、
代数的仕様と呼ばれるものです。これは関数を、条件に対応する公理で振る舞いが指定される抽象代数系の要素とみなし、抽象代数の手法を使ってデータオブジェクトに関する表明を検証します。両方の方法は、
Liskov と Zilles の論文(1975)で概観されています。
The function
error introduced in
section 1.3.3
takes as optional second argument
a string that gets displayed before the first argument—for example, if
m is 42: