mirror of
https://github.com/ganelson/inform.git
synced 2024-07-08 18:14:21 +03:00
401 lines
20 KiB
HTML
401 lines
20 KiB
HTML
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
|
|
<html>
|
|
<head>
|
|
<title>10/cap</title>
|
|
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
|
|
<meta http-equiv="Content-Language" content="en-gb">
|
|
<link href="inweb.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
</head>
|
|
<body>
|
|
|
|
<!--Weave of '11/itpc' generated by 7-->
|
|
<ul class="crumbs"><li><a href="../webs.html">★</a></li><li><a href="index.html">core</a></li><li><a href="index.html#11">Chapter 11: Predicate Calculus</a></li><li><b>Introduction to Predicate Calculus</b></li></ul><p class="purpose">An exposition of the form of predicate calculus used by Inform.</p>
|
|
|
|
<ul class="toc"><li><a href="#SP2">§2. Why predicate calculus</a></li><li><a href="#SP4">§4. Formal description</a></li><li><a href="#SP7">§7. Free and bound variables, well-formedness</a></li><li><a href="#SP8">§8. The scope of quantifiers</a></li><li><a href="#SP10">§10. What is not in our calculus</a></li></ul><hr class="tocbar">
|
|
|
|
<p class="inwebparagraph"><a id="SP1"></a><b>§1. </b>"Again and again Haddon thought he had found the key to the strange writings,
|
|
but always he was disappointed. And then one day — he was an old man of seventy
|
|
now — he fed a trial programme into his computer, and for the first time a
|
|
translated sentence was delivered — his life-long task was rewarded. Yes,
|
|
but for the fact that one man had been prepared to devote every spare hour of
|
|
his life to solving the riddle, the amazing story of the Trigan Empire would
|
|
never have been given to the world. WHAT FOLLOWS IS THAT STORY."
|
|
("The Rise and Fall of the Trigan Empire", 1965)
|
|
</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2"></a><b>§2. Why predicate calculus. </b>Most attempts to codify the meaning of sentences in any systematic way
|
|
involve predicate calculus, and most people generally seem to agree
|
|
that linguistic concepts (like verbs, adjectives, and determiners)
|
|
correspond uncannily well with logical ones (like binary predicates,
|
|
unary predicates, and quantifiers). Since today's mathematical logic
|
|
has its roots in work on the philosophy of language (chiefly by Frege and
|
|
Wittgenstein), this is not altogether a coincidence. All the same, it is
|
|
striking how good the fit is, considering that human language is so
|
|
haphazard and logic so regular.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">At any rate Inform goes along with this consensus, and converts the
|
|
difficult passages in its source text into mathematical propositions
|
|
— lines written in logical notation. This is useful partly as a
|
|
well-defined way to store complicated meanings inside the program, but
|
|
also because these propositions can then be simplified by logical
|
|
rules. We can change their form so long as we do not change their
|
|
meaning, in the hope of finding ways to carry out the same tasks but
|
|
more efficiently than a simple-minded reading of the text would
|
|
suggest.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">There are four main tasks to perform:
|
|
</p>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<ul class="items"><li>(a) Building propositions from the other Inform data structures;
|
|
</li></ul>
|
|
<ul class="items"><li>(b) Simplifying, rearranging and type-checking propositions;
|
|
</li></ul>
|
|
<ul class="items"><li>(c) Asserting that certain propositions are true at the start of play;
|
|
</li></ul>
|
|
<ul class="items"><li>(d) Compiling certain propositions to I6 code which can test them, make them
|
|
true, or make them false.
|
|
</li></ul>
|
|
<p class="inwebparagraph">In this chapter, we take these tasks in order. Because it contains all
|
|
of Inform's predicate calculus lore in one place, it necessarily contains
|
|
little pieces of algorithms from other chapters: a piece of the
|
|
type-checker, a piece of the code for asserting the initial state of
|
|
play, and so on. Well: but the overlap had to go somewhere.
|
|
</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP3"></a><b>§3. </b>A glimpse of Inform's inner workings can be made by writing a test
|
|
instruction like so:
|
|
</p>
|
|
|
|
<blockquote>
|
|
<p>Laboratory is a room. The box is a container.</p>
|
|
|
|
</blockquote>
|
|
|
|
<blockquote>
|
|
<p>Test sentence (internal) with a man can see the box in the Laboratory.</p>
|
|
|
|
</blockquote>
|
|
|
|
<p class="inwebparagraph">At the start of play, the compiled story file will print a textual form of
|
|
the proposition in predicate calculus which that became:
|
|
</p>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
|
|
<pre class="display">
|
|
<span class="plain">1. a man can see the box in the Laboratory</span>
|
|
<span class="plain">[ Exists x : man(x) & thing('box') & is('laboratory', ContainerOf('box')) & can-see(x, 'box') ]</span>
|
|
<span class="plain">x - object.</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph">(The <code class="display"><span class="extract">intest</span></code> test case <code class="display"><span class="extract">Calculus</span></code> runs about 200 sentences like this.)
|
|
One can similarly "Test description (internal) with..." for any description,
|
|
such as "animals which are in lighted rooms".
|
|
</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP4"></a><b>§4. Formal description. </b>There are many flavours of predicate calculus, and though they behave in
|
|
broadly similar ways, the details vary in practice. Inform's calculus
|
|
is unusual in several respects, so here is its definition.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">The terms "constant", "variable" and "function" below are used in
|
|
their predicate-calculus senses, not their Inform ones. In the excerpt
|
|
</p>
|
|
|
|
<blockquote>
|
|
<p>a container in the location of Nicole contains the second noun</p>
|
|
|
|
</blockquote>
|
|
|
|
<p class="inwebparagraph">the text "location of Nicole" is a phrase deciding an object — a function —
|
|
and "the second noun" is an object that varies — a variable. But if we are
|
|
looking at the sentence only for its logical meaning, we have to forget about
|
|
the passage of time and think about what the sentence means at any single
|
|
moment. "Location of Nicole" and "the second noun" are both fixed, in
|
|
this instant; the only thing which varies is the identity of the possible
|
|
container, because we might have to look at hundreds of different containers
|
|
to see if the sentence is true. One logical translation might be
|
|
∃ x: container(x)∧ in(x, C_1) ∧ in(C_2, x)
|
|
where C_1 and C_2 are constants ("location of Nicole" and "second noun"
|
|
respectively), while the only variable is x, the mysterious container.
|
|
(The symbol ∃ means "there exists".) Because objects move
|
|
around in play, and C_1 and C_2 have different values at different
|
|
moments, this sentence is sometimes true and sometimes false. But its
|
|
meaning does not change.
|
|
</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP5"></a><b>§5. </b>The propositions in our predicate calculus are those which can be made
|
|
using the following ingredients and recipes.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">1. There are 26 variables, which we print to the debugging log as <code class="display"><span class="extract">x</span></code>, <code class="display"><span class="extract">y</span></code>,
|
|
<code class="display"><span class="extract">z</span></code>, <code class="display"><span class="extract">a</span></code>, <code class="display"><span class="extract">b</span></code>, <code class="display"><span class="extract">c</span></code>, ..., <code class="display"><span class="extract">w</span></code>.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">2. The constants are specifications with family <code class="display"><span class="extract">VALUE</span></code> — that
|
|
is, all literal constants, variables, list and table entries, or phrases
|
|
which decide values.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">3. A "predicate" P is a statement P(a, b, c, ...) which is
|
|
either true or false for any given combination a, b, c, .... The
|
|
"arity" of a predicate is the number of terms it looks at. There is
|
|
speculative talk of allowing higher-order predicates in future (and Inform's
|
|
data structures have been built with one eye on this), but for now
|
|
we use only unary predicates U(x) or binary predicates B(x, y), of
|
|
arity 1 and 2 respectively. The predicates in our calculus are as follows:
|
|
</p>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<ul class="items"><li>(a) The special binary predicate is(x, y), true if and only if x=y.
|
|
</li><li>(b) Every kind K (of value or of object) corresponds to a unary
|
|
predicate K(x).
|
|
</li><li>(c) Every state of an either/or property corresponds to a unary
|
|
predicate, e.g., open(x).
|
|
</li><li>(d) Every possible value of an enumerated kind of value which
|
|
corresponds to a property similarly corresponds to a unary predicate:
|
|
e.g., if we have defined "colour" as a kind of value and made it a
|
|
property of things, then green(x), red(x), and
|
|
blue(x) might all be unary predicates.
|
|
</li><li>(e) Every adjectival phrase, to which a definition has been
|
|
supplied in the source, likewise produces a unary predicate: for
|
|
example, visible(x).
|
|
</li><li>(f) An adjective given a definition which involves a threshold for
|
|
a numeric property also produces a binary predicate for its comparative
|
|
form: for instance, a definition for "tall" gives not only a unary
|
|
predicate tall(x) (as in (e) above) but also a binary predicate
|
|
taller(x, y).
|
|
</li><li>(g) A special unary predicate everywhere(x) which asserts that
|
|
the backdrop x can be found in every room.
|
|
</li><li>(h) Each table column name C gives rise to a binary predicate
|
|
listed-in-C(x, y), which tests whether value x is listed in
|
|
the C column of table y. (This looks as if it should really be a
|
|
single ternary predicate, but since we never need to quantify over
|
|
choice of column, nothing would be gained by that.)
|
|
</li><li>(i) Every value property P gives rise to a binary predicate
|
|
same-P-value(x, y), testing whether objects x and y
|
|
have the same value of P. (Again, it would not be useful to quantify
|
|
over P.)
|
|
</li><li>(j) Every direction D gives rise to a binary predicated
|
|
mapped-D(x, y), testing whether there is a map connection
|
|
from x to y in direction D.
|
|
</li><li>(k) Each new relation defined in the source text is a binary
|
|
predicate.
|
|
</li><li>(l) The basic stock of spatial containment relations built into
|
|
Inform — in(x, y), on(x, y), etc. — are similarly
|
|
binary predicates.
|
|
</li><li>(m) If P is a binary predicate present in Inform then so automatically
|
|
is its "reversal" R, defined by R(x, y) if and only if P(y, x).
|
|
For instance, the existence of carries(x, y) ensures that we
|
|
also have carried-by(x, y), its reversal. The equality predicate
|
|
x=y is its own reversal, but all other binary predicates are formally
|
|
different from their reversals, even if they always mean the same in
|
|
practice. (The reversal of same-carrying-capacity-as(x, y) is
|
|
true if and only if the original is true, but we regard them as different
|
|
predicates just the same.)
|
|
</li></ul>
|
|
<p class="inwebparagraph">4. If a binary predicate B has the property that for any x there
|
|
is at most one y such that B(x, y) (for instance, carried-by
|
|
has this property) then we write f_B for the function which maps x
|
|
to either the unique value y such that B(x, y), or else to a zero
|
|
value. (In the case where y is an object, we interpret this as "nothing",
|
|
which for logical purposes is treated as if it were a valid object, so
|
|
that f_B maps the set of objects to itself.) Another way of saying
|
|
this is that f_B, if it exists, is defined by:
|
|
B(x, y) <=> y = f_B(x).
|
|
</p>
|
|
|
|
<p class="inwebparagraph">These are the only functions allowed in our predicate calculus, and they
|
|
are always functions of just one variable.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">5. A "quantifier" Qx is a logical expression for the range of values
|
|
of a given variable x: for instance, ∀ x (read "for all x")
|
|
implies that x can have any value, whereas ∃ x (read "there
|
|
exists an x") means only that at least one value works for x. In
|
|
our calculus, we allow not only these quantifiers but also the following
|
|
generalised quantifiers, where n is a non-negative integer:
|
|
</p>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<ul class="items"><li>(a) The quantifier V_{=n} x —
|
|
meaning "for exactly n values of x".
|
|
</li><li>(b) The quantifier V_{>= n} x —
|
|
meaning "for at least n values of x".
|
|
</li><li>(c) The quantifier V_{<= n} x —
|
|
meaning "for at most n values of x".
|
|
</li><li>(d) The quantifier P_{>= n} x —
|
|
meaning "for at least a percentage of n values of x".
|
|
</li><li>(e) The quantifier P_{<= n} x —
|
|
meaning "for at most a percentage of n values of x".
|
|
</li></ul>
|
|
<p class="inwebparagraph">Note that "for all x" corresponds to P_{>= 100} x, and "there exists
|
|
x" to V_{>= 1} x, so the above scheme does indeed generalise the
|
|
standard pair of quantifiers ∀ and ∃.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">6. A "term" must be a constant, a variable or a function f_B(t) of
|
|
another term t. So x, "Miss Marple", f_B(x) and f_A(f_B(f_C(6)))
|
|
are all examples of terms. We are only allowed to apply functions a finite
|
|
number of times, so any term has the form:
|
|
f_{B_1}(f_{B_2}(... f_{B_n}(s)...))
|
|
for at most a finite number n of function usages (possibly n=0), where
|
|
at bottom s must be either a constant or a variable.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">7. A proposition is defined by the following rules:
|
|
</p>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<ul class="items"><li>(a) The empty expression is a proposition. This is always true, so in these
|
|
notes it will be written T.
|
|
</li><li>(b) For any unary predicate U and any term t, U(t) is a proposition.
|
|
</li><li>(c) For any binary predicate B and any terms s, t, B(s, t)
|
|
is a proposition.
|
|
</li><li>(d) For any proposition φ, the negation ¬(φ) is a
|
|
proposition. This is by definition true if and only if φ is false.
|
|
</li><li>(e) For any propositions φ and ψ, the conjunction
|
|
φ∧ψ — true if and only if both are true — is a proposition
|
|
so long as it is well-formed (see below).
|
|
</li><li>(f) For any variable v, the quantifier ∃ v is a proposition.
|
|
</li><li>(g) For any variable v, any quantifier Q other than ∃, and any
|
|
proposition φ in which v is a "free" variable (see below),
|
|
Qv∈{ v| φ(v)} is a proposition. The set denotes all
|
|
possible values of v matching the condition φ(v), and this specifies
|
|
the range of the quantifier.
|
|
</li></ul>
|
|
<p class="inwebparagraph"><a id="SP6"></a><b>§6. </b>Note that there are two ways in which propositions can appear in brackets
|
|
in a bigger proposition: negation (d), and specifying a quantification
|
|
domain (g). We sometimes call the bracketed part a "subexpression" of the
|
|
whole.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">In particular, note that — unusually — we do not bracket quantification
|
|
itself. Most definitions would say that given v and a proposition
|
|
φ(v), we can form ∃ v: (φ(v)) — in other words that
|
|
quantification is a way to modify an already created proposition, but that
|
|
∃ v is not a proposition in its own right, just as ¬ is not a
|
|
proposition. Inform disagrees. Here ∃ v is a meaningful sentence:
|
|
it means "an object exists". We can form "there is a door" by rule (e),
|
|
conjoining ∃ x and door(x) to form ∃ x: door(x).
|
|
(As a nod to conventional mathematical notation, we write a colon after
|
|
a quantifier instead of a conjunction sign ∧. But Inform stores it
|
|
as just another conjunction.)
|
|
</p>
|
|
|
|
<p class="inwebparagraph">We do bracket the domain of quantification. Most simple predicate
|
|
calculuses (predicates calculus?) have no need, since their only quantifiers
|
|
are ∀ and ∃, and there is a single universe set from which
|
|
all values are drawn. But in Inform, some quantifiers range over doors,
|
|
some over numbers, and so on. In most cases, a quantifier must specify its
|
|
domain. For example,
|
|
∀ x∈ { x| number(x)} : even(x)
|
|
("all numbers are even" — false, of course) specifies the domain of
|
|
∀ as the set of all x such that number(x).
|
|
</p>
|
|
|
|
<p class="inwebparagraph">∃ is the one exception to this. The statement
|
|
∃ x∈ { x| number(x)} : even(x)
|
|
("a number is even" — true this time) could equally be written
|
|
∃ x: number(x)∧ even(x)
|
|
("there is an even number"). We take advantage of this, and Inform never
|
|
specifies a domain for a ∃ quantifier.
|
|
</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP7"></a><b>§7. Free and bound variables, well-formedness. </b>In any proposition φ, we say that a variable v is "bound" if it
|
|
appears as the variable governed by a quantifier: it is "free" if it
|
|
does appear somewhere in φ — either directly as a term or indirectly
|
|
through a function application — and is not bound. For instance, in
|
|
∀ x : K(x) ∧ B(x, f_C(y))
|
|
the variable x is bound and the variable y is free. In most accounts
|
|
of predicate calculus we say that a proposition is a "sentence" if all
|
|
of its variables are bound, but Inform often needs to parse English text to
|
|
a proposition with one free variable remaining in it, so we are not too
|
|
picky about this.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">A well-formed proposition is one in which a variable v is quantified
|
|
at most once: and in which, if it is quantified, then it occurs only
|
|
after (to the right of) its quantifier, and only within the subexpression
|
|
containing its quantifier. Thus the following are not well-formed:
|
|
∃ v: open(v)∧ ∃ v : closed(v)
|
|
(v is quantified twice),
|
|
open(v)∧ ∃ v : closed(v)
|
|
(v occurs before its quantifier),
|
|
¬ ( ∃ v : closed(v) ) ∧ openable(v)
|
|
(v occurs outside the subexpression containing the quantifier — in this
|
|
case, outside the negation brackets).
|
|
</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP8"></a><b>§8. The scope of quantifiers. </b>A quantifier introduces a variable into a proposition which would not
|
|
otherwise be there, and it exists only for a limited range. For instance, in
|
|
the proposition
|
|
open(x)∧¬(∃ y: in(x, y))∧ container(x)
|
|
the variable y exists only within the negation brackets; it ceases to exist
|
|
as soon as we move back out to the container atom. This range is called
|
|
the "scope" of the quantifier. In general, scopes are always as large as
|
|
possible in Inform: a variable lasts until the end of the subexpression in
|
|
which it is created. If the quantifier is outside of any brackets, then the
|
|
variable lasts until the end of the proposition.
|
|
</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP9"></a><b>§9. </b>Earlier drafts of Inform played games with moving quantifiers around, in
|
|
order to try to achieve more efficiently compiled propositions. The same
|
|
thing is now done by building propositions in a way which places quantifiers
|
|
as far forwards as possible, so we no longer actively move them once they
|
|
are in place. But it seems still worth preserving the rule which says when
|
|
this can be done:
|
|
</p>
|
|
|
|
<p class="inwebparagraph">Lemma. Suppose that x is a variable; φ is a proposition in
|
|
which x is unused; ψ(x) is a proposition in which x is free; and that
|
|
Q is a generalised quantifier. Then
|
|
φ∧ Qx : ψ(x) <=> Qx : φ∧ψ(x)
|
|
provided that Q requires at least one case in its range to be satisfied.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">Proof. In any given evaluation, either φ is true, or it is false.
|
|
Suppose it is true. Since T∧ θ <=> θ, both sides
|
|
reduce to the same expression, Qx : ψ(x). On the other hand, suppose φ
|
|
is false. Then φ∧ Qx : ψ(x) is false, since F∧θ = F
|
|
for any θ. But the other side is Qx : F. Since we know that Q can
|
|
only be satisfied if at least one case of x works, and here every case of
|
|
x results in falsity, Qx : F is also false. So the two expressions have
|
|
the same evaluation in this case, too.
|
|
</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP10"></a><b>§10. What is not in our calculus. </b>The significant thing missing is disjunction. In general, the
|
|
disjunction φ∨ψ — "at least one of φ and ψ
|
|
holds" — is not a proposition.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">Natural language does not seem to share the general even-handedness of
|
|
Boolean logic as between "and" and "or", perhaps because of the
|
|
way that speech is essentially a one-dimensional stream of discourse.
|
|
Talking makes it easier to reel off a linear list of requirements than
|
|
to describe a deep tree structure.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">Of course, the operations "not" and "and" are between them sufficient
|
|
to express all other operations, and in particular we could imitate
|
|
disjunction like so:
|
|
¬ (¬(φ)∧¬(ψ))
|
|
("they are not both false" being equivalent to "at least one is true"),
|
|
but Inform does not at present make use of this.
|
|
</p>
|
|
|
|
<hr class="tocbar">
|
|
<ul class="toc"><li><i>(This section begins Chapter 11: Predicate Calculus.)</i></li><li><a href="11-tr.html">Continue with 'Terms'</a></li></ul><hr class="tocbar">
|
|
<!--End of weave-->
|
|
</body>
|
|
</html>
|
|
|