<!--Weave of 'What This Module Does' generated by Inweb-->
<divclass="breadcrumbs">
<ulclass="crumbs"><li><ahref="../index.html">Home</a></li><li><ahref="../compiler.html">Services</a></li><li><ahref="index.html">calculus</a></li><li><ahref="index.html#P">Preliminaries</a></li><li><b>What This Module Does</b></li></ul></div>
<pclass="purpose">An overview of the calculus module's role and abilities.</p>
<pclass="commentary firstcommentary"><aid="SP1"class="paragraph-anchor"></a><b>§1. Prerequisites. </b>The calculus module is a part of the Inform compiler toolset. It is
presented as a literate program or "web". Before diving in:
</p>
<ulclass="items"><li>(a) It helps to have some experience of reading webs: see <ahref="../../../inweb/docs/index.html"class="internal">inweb</a> for more.
</li><li>(b) The module is written in C, in fact ANSI C99, but this is disguised by the
fact that it uses some extension syntaxes provided by the <ahref="../../../inweb/docs/index.html"class="internal">inweb</a> literate
programming tool, making it a dialect of C called InC. See <ahref="../../../inweb/docs/index.html"class="internal">inweb</a> for
full details, but essentially: it's C without predeclarations or header files,
and where functions have names like <spanclass="extract"><spanclass="extract-syntax">Tags::add_by_name</span></span> rather than <spanclass="extract"><spanclass="extract-syntax">add_by_name</span></span>.
</li><li>(c) This module uses other modules drawn from the <ahref="../compiler.html"class="internal">compiler</a>, and also
uses a module of utility functions called <ahref="../../../inweb/docs/foundation-module/index.html"class="internal">foundation</a>.
For more, see <ahref="../../../inweb/docs/foundation-module/P-abgtf.html"class="internal">A Brief Guide to Foundation (in foundation)</a>.
<pclass="commentary firstcommentary"><aid="SP2"class="paragraph-anchor"></a><b>§2. What predicate calculus is. </b>The word "calculus" is often used to mean differentiating and integrating
functions, but properly speaking that is "infinitesimal calculus", and there
are many others.<supid="fnref:1"><ahref="#fn:1"rel="footnote">1</a></sup> In logic, different sets of rules for making deductions
tend to be given such names, and we will use (a form of) one of the most
popular simple systems, "predicate calculus".<supid="fnref:2"><ahref="#fn:2"rel="footnote">2</a></sup>
</p>
<pclass="commentary">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).<supid="fnref:3"><ahref="#fn:3"rel="footnote">3</a></sup>
All the same, it is striking how good the fit is, considering that human language
is so haphazard at first sight.
</p>
<pclass="commentary">At any rate Inform goes along with this consensus, and converts the difficult
passages in its source text into logical "propositions" — lines written in
logical notation. This is useful partly as a tidy way to store complicated
meanings inside the program, but also because these propositions can then be
simplified by logical rules, without changing their meaning. Without such
simplifications, Inform would generate much less efficient code.
</p>
<ulclass="footnotetexts"><liclass="footnote"id="fn:1"><pclass="inwebfootnote"><supid="fnref:1"><ahref="#fn:1"rel="footnote">1</a></sup> At time of writing, <ahref="https://en.wikipedia.org/wiki/Calculus_(disambiguation)"class="external">nearly 40 can be found here</a>,
though admittedly that includes a genus of spider and a Tintin character.
<ahref="#fnref:1"title="return to text">↩</a></p></li><liclass="footnote"id="fn:2"><pclass="inwebfootnote"><supid="fnref:2"><ahref="#fn:2"rel="footnote">2</a></sup> Specifically, first order predicate calculus with equality, but with
generalised quantifiers added, and disjunction removed.
<ahref="#fnref:2"title="return to text">↩</a></p></li><liclass="footnote"id="fn:3"><pclass="inwebfootnote"><supid="fnref:3"><ahref="#fn:3"rel="footnote">3</a></sup> This is not altogether a coincidence since the pioneers of mathematical
logic, and in particular Frege and Wittgenstein, began by thinking about
natural language.
<ahref="#fnref:3"title="return to text">↩</a></p></li></ul>
<pclass="commentary firstcommentary"><aid="SP3"class="paragraph-anchor"></a><b>§3. Notation. </b>This module deals with propositions in predicate calculus, that is, with
<pclass="commentary">But a much easier way to test the functions in this module is to use the
<ahref="../calculus-test/index.html"class="internal">calculus-test</a> tool. As with <ahref="../kinds-test/index.html"class="internal">kinds-test</a>, this is a REPL: that is,
<spanclass="plain-syntax">'</span><spanclass="element-syntax"><< NOT< ^ even (x) ^ NOT>>></span><spanclass="plain-syntax">':</span><spanclass="string-syntax"><< NOT< even(x) NOT>>></span>
<spanclass="plain-syntax">'</span><spanclass="element-syntax"><< Forall x IN< kind = number (x) IN>: even (x) >></span><spanclass="plain-syntax">':</span><spanclass="string-syntax"><< ForAll x IN< kind=number(x) IN> : even(x) >></span>
<spanclass="plain-syntax">'</span><spanclass="element-syntax"><< Exists x >></span><spanclass="plain-syntax">':</span><spanclass="string-syntax"><< Exists x >></span>
<spanclass="plain-syntax">'</span><spanclass="element-syntax"><< DoesNotExist x IN< kind = number (x) IN>: even (x) >></span><spanclass="plain-syntax">':</span><spanclass="string-syntax"><< DoesNotExist x IN< kind=number(x) IN> : even(x) >></span>
<spanclass="plain-syntax">'</span><spanclass="element-syntax"><< Forall x IN< kind = number (x) IN>: even (x) >></span><spanclass="plain-syntax">':</span><spanclass="string-syntax"><< ForAll x IN< kind=number(x) IN> : even(x) >></span>
<spanclass="plain-syntax">'</span><spanclass="element-syntax"><< Card= 6 x IN< kind = number (x) IN>: even (x) >></span><spanclass="plain-syntax">':</span><spanclass="string-syntax"><< Card=6 x IN< kind=number(x) IN> : even(x) >></span>
<pclass="commentary firstcommentary"><aid="SP4"class="paragraph-anchor"></a><b>§4. Formal description. </b>1. A "term" is any of the following:
</p>
<ulclass="items"><li>● A constant, corresponding to anything which can be evaluated to Inform —
a number, a text, etc. — and which has a definite kind.
</li><li>● One of 26 variables, which we print to the debugging log as <spanclass="extract"><spanclass="extract-syntax">x</span></span>, <spanclass="extract"><spanclass="extract-syntax">y</span></span>,
</li><li>● A function \(f\) applied to another term.<supid="fnref:4"><ahref="#fn:4"rel="footnote">4</a></sup>
</li></ul>
<pclass="commentary">Note that if we have given values to the necessary variables, then any term
can be evaluated to a value, and its kind determined. For example, if <spanclass="extract"><spanclass="extract-syntax">x</span></span> is 7,
then the terms <spanclass="extract"><spanclass="extract-syntax">17</span></span>, <spanclass="extract"><spanclass="extract-syntax">x</span></span> and <spanclass="extract"><spanclass="extract-syntax">f(x)</span></span> evaluate to 17, 7 and \(f(7)\) respectively.
</p>
<pclass="commentary">2. An "atomic proposition" is any of the following:
</p>
<ulclass="items"><li>● A "unary predicate" \(U(t)\), where \(t\) is a term, which is either true or
false depending on the evaluation of \(t\).
</li><li>● A "binary predicate" \(B(t_1, t_2)\) depending on two terms.<supid="fnref:5"><ahref="#fn:5"rel="footnote">5</a></sup>
</li><li>● A "quantifier" \(Q(v, n)\) applying to a variable \(v\), optionally with a
parameter \(n\). See <ahref="../linguistics-module/2-daq.html"class="internal">Determiners and Quantifiers (in linguistics)</a> for the range
of quantifiers available.
</li></ul>
<pclass="commentary">3. A "proposition" is a sequence of 0 or more of the following:
</p>
<ulclass="items"><li>● A conjunction \(P_1\land P_2\), where \(P_1\) and \(P_2\) are propositions.
</li><li>● A negation \(\lnot P\), where \(P\) is a proposition.
</li><li>● A quantification \(Q v\in D: P\), where \(Q\) is a quantifier, optionally
also with a numerical parameter, \(v\) is a variable, \(D\) is a set
specifying the domain of \(v\), and \(P\) is a proposition.<supid="fnref:6"><ahref="#fn:6"rel="footnote">6</a></sup>
</li><li>● An existential quantification \(\exists v: P\) without a domain.
</li></ul>
<ulclass="footnotetexts"><liclass="footnote"id="fn:4"><pclass="inwebfootnote"><supid="fnref:4"><ahref="#fn:4"rel="footnote">4</a></sup> In this module we use words such as "constant", "variable" and "function" in
their predicate-calculus senses, not their Inform ones. For example, if we are
to decide whether it is true that "a container in the location of Nicole contains
the prize", we have to forget about the passage of time and think only about a
single moment. In the resultant proposition, "the location of Nicole" and
"the prize" lead to constant terms, "a container" leads to a variable term (since
we do not know its identity) and there are no functions.
<ahref="#fnref:4"title="return to text">↩</a></p></li><liclass="footnote"id="fn:5"><pclass="inwebfootnote"><supid="fnref:5"><ahref="#fn:5"rel="footnote">5</a></sup> We do not support higher arities of predicates as such, but they can be
simulated. The universal relation in Inform is in effect a ternary predicate,
but is achieved by combining two of its terms into an ordered pair.
<ahref="#fnref:5"title="return to text">↩</a></p></li><liclass="footnote"id="fn:6"><pclass="inwebfootnote"><supid="fnref:6"><ahref="#fn:6"rel="footnote">6</a></sup> Some quantifiers also carry a numerical parameter, to express, e.g.,
"at least 7" — the parameter for that being 7.
<ahref="#fnref:6"title="return to text">↩</a></p></li></ul>
<pclass="commentary firstcommentary"><aid="SP5"class="paragraph-anchor"></a><b>§5. </b>The implementation uses the term "atom" a little more loosely, to include
four punctuation marks: <spanclass="extract"><spanclass="extract-syntax">NOT<</span></span>, <spanclass="extract"><spanclass="extract-syntax">NOT></span></span>, <spanclass="extract"><spanclass="extract-syntax">IN<</span></span>, <spanclass="extract"><spanclass="extract-syntax">IN></span></span>, which act like
opening and closing parentheses. These are considered atoms purely for
convenience when building more complicated constructions — they make no sense
standing alone. Thus:
</p>
<ulclass="items"><li>● \(\lnot P\) is implemented as <spanclass="extract"><spanclass="extract-syntax">NOT< P NOT></span></span>.
</li><li>● \(Q v\in D: P\) is implemented as <spanclass="extract"><spanclass="extract-syntax">Q IN< D IN></span></span>.
</li></ul>
<pclass="commentary">Note that the domain \(D\) of a quantifier is itself expressed as a proposition.
Thus "for all numbers \(n\)" is implemented as <spanclass="extract"><spanclass="extract-syntax">ForAll n IN< kind=number(n) IN></span></span>.
</p>
<pclass="commentary">In all other cases, adjacent atoms in a sequence are considered to be conjoined:
i.e., <spanclass="extract"><spanclass="extract-syntax">X Y</span></span> means \(X\land Y\), the proposition which is true if \(X\) and \(Y\) are
both true. To emphasise this, the textual notation uses the <spanclass="extract"><spanclass="extract-syntax">^</span></span> sign. For
example, <spanclass="extract"><spanclass="extract-syntax">odd(n) ^ prime(n)</span></span> is the notation for two consecutive atoms <spanclass="extract"><spanclass="extract-syntax">odd(n)</span></span>
and <spanclass="extract"><spanclass="extract-syntax">prime(n)</span></span>.
</p>
<pclass="commentary firstcommentary"><aid="SP6"class="paragraph-anchor"></a><b>§6. Unary predicates. </b>We have a mixed bag of unary predicates, as follows.
</p>
<ulclass="items"><li>● For each adjective defined in the <ahref="../linguistics-module/index.html"class="internal">linguistics</a> module, there is a
predicate <spanclass="extract"><spanclass="extract-syntax">A(t)</span></span>, true if the adjective currently applies to \(t\).
</li><li>● For each kind \(K\), there is a predicate <spanclass="extract"><spanclass="extract-syntax">kind=K(t)</span></span>, which is true if \(t\)
</li><li>● For any wording <spanclass="extract"><spanclass="extract-syntax">W</span></span>, there is a predicate <spanclass="extract"><spanclass="extract-syntax">called=W(t)</span></span>, which asserts
that the current value of \(t\) is something named <spanclass="extract"><spanclass="extract-syntax">W</span></span>.
</li><li>●<spanclass="extract"><spanclass="extract-syntax">is-a-kind(t)</span></span> asserts that \(t\) represents a kind, not a value.
</li><li>●<spanclass="extract"><spanclass="extract-syntax">is-a-var(t)</span></span> asserts that \(t\) represents a variable, not a value.
</li><li>●<spanclass="extract"><spanclass="extract-syntax">is-a-const(t)</span></span> asserts that \(t\) represents a constant, not a value.
</li><li>●<spanclass="extract"><spanclass="extract-syntax">everywhere(t)</span></span> asserts that \(t\) is an object found everywhere.
</li><li>●<spanclass="extract"><spanclass="extract-syntax">nowhere(t)</span></span> asserts that \(t\) is an object found nowhere.
</li><li>●<spanclass="extract"><spanclass="extract-syntax">here(t)</span></span> asserts that \(t\) is an object found in the current room.
</li></ul>
<pclass="commentary">As is apparent, the <spanclass="extract"><spanclass="extract-syntax">is-a-...</span></span> predicates are a cheat: they exist purely to
make it easier to write propositions which change the state of the world,
rather than discuss that state. For example, Inform might create the kind
"animal" by asserting <spanclass="extract"><spanclass="extract-syntax">Exists x : is-a-kind(x) ^ called=animal(x)</span></span>.
</p>
<pclass="commentary firstcommentary"><aid="SP7"class="paragraph-anchor"></a><b>§7. Binary predicates. </b>By contrast all binary predicate atoms use <spanclass="extract"><spanclass="extract-syntax">PREDICATE_ATOM</span></span>, and there is only
one set of them — but with that said,
</p>
<ulclass="items"><li>(a) They can be organised into "families" with shared implementations — see
</li><li>(b) The equality predicate \(=\) is predefined by the <ahref="index.html"class="internal">calculus</a> module, and
its special meaning is used when simplifying propositions. See <ahref="2-ter.html"class="internal">The Equality Relation</a>.
It is written with the special notation <spanclass="extract"><spanclass="extract-syntax">(x == y)</span></span>, though this is just syntactic
sugar.
</li></ul>
<pclass="commentary">New BPs can be constructed with <ahref="2-bp.html#SP26"class="internal">BinaryPredicates::make_pair</a>. The term "pair"
is used because every \(B\) has a "reversal" \(B^r\), such that \(B^r(s, t)\) is true
if and only if \(B(t, s)\). \(B\) and \(B^r\) are created in pairs.<supid="fnref:7"><ahref="#fn:7"rel="footnote">7</a></sup>
</p>
<ulclass="footnotetexts"><liclass="footnote"id="fn:7"><pclass="inwebfootnote"><supid="fnref:7"><ahref="#fn:7"rel="footnote">7</a></sup> Except for equality, which is its own reversal. See <ahref="2-bp.html#SP25"class="internal">BinaryPredicates::make_equality</a>.
<ahref="#fnref:7"title="return to text">↩</a></p></li></ul>
<pclass="commentary firstcommentary"><aid="SP8"class="paragraph-anchor"></a><b>§8. Making propositions. </b>Propositions are built incrementally, like Lego, with a sequence of function
<pclass="commentary">3. Propositions are then built up from atoms or other propositions<supid="fnref:8"><ahref="#fn:8"rel="footnote">8</a></sup> by calling:
<ulclass="footnotetexts"><liclass="footnote"id="fn:8"><pclass="inwebfootnote"><supid="fnref:8"><ahref="#fn:8"rel="footnote">8</a></sup> But beware that propositions are passed by reference not value. Use
<ahref="#fnref:8"title="return to text">↩</a></p></li></ul>
<pclass="commentary firstcommentary"><aid="SP9"class="paragraph-anchor"></a><b>§9. </b>There are two senses in which it's possible to make an impossible proposition:
</p>
<ulclass="items"><li>(1) You could make a mess of the punctuation markers improperly, or fail to
give a domain set for a quantifier.
</li><li>(2) More subtly, you could concatenate two propositions in which the same
variable is used with a different meaning in each.
