mirror of
https://github.com/ganelson/inform.git
synced 2024-06-29 05:24:57 +03:00
340 lines
28 KiB
HTML
340 lines
28 KiB
HTML
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
|
|
<html>
|
|
<head>
|
|
<title>What This Module Does</title>
|
|
<link href="../docs-assets/Breadcrumbs.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<meta name="viewport" content="width=device-width initial-scale=1">
|
|
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
|
|
<meta http-equiv="Content-Language" content="en-gb">
|
|
|
|
<link href="../docs-assets/Contents.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Progress.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Navigation.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Fonts.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Base.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<script src="http://code.jquery.com/jquery-1.12.4.min.js"
|
|
integrity="sha256-ZosEbRLbNQzLpnKIkEdrPv7lOy9C27hHQ+Xp8a4MxAQ=" crossorigin="anonymous"></script>
|
|
|
|
<script src="../docs-assets/Bigfoot.js"></script>
|
|
<link href="../docs-assets/Bigfoot.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<script>
|
|
MathJax = {
|
|
tex: {
|
|
inlineMath: '$', '$'], ['\\(', '\\)'
|
|
},
|
|
svg: {
|
|
fontCache: 'global'
|
|
}
|
|
};
|
|
</script>
|
|
<script type="text/javascript" id="MathJax-script" async
|
|
src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-svg.js">
|
|
</script>
|
|
|
|
<link href="../docs-assets/Colours.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
|
|
</head>
|
|
<body class="commentary-font">
|
|
<nav role="navigation">
|
|
<h1><a href="../index.html">
|
|
<img src="../docs-assets/Inform.png" height=72">
|
|
</a></h1>
|
|
<ul><li><a href="../index.html">home</a></li>
|
|
</ul><h2>Compiler</h2><ul>
|
|
<li><a href="../structure.html">structure</a></li>
|
|
<li><a href="../inbuildn.html">inbuild</a></li>
|
|
<li><a href="../inform7n.html">inform7</a></li>
|
|
<li><a href="../intern.html">inter</a></li>
|
|
<li><a href="../services.html">services</a></li>
|
|
<li><a href="../secrets.html">secrets</a></li>
|
|
</ul><h2>Other Tools</h2><ul>
|
|
<li><a href="../inblorbn.html">inblorb</a></li>
|
|
<li><a href="../indocn.html">indoc</a></li>
|
|
<li><a href="../inform6.html">inform6</a></li>
|
|
<li><a href="../inpolicyn.html">inpolicy</a></li>
|
|
<li><a href="../inrtpsn.html">inrtps</a></li>
|
|
</ul><h2>Resources</h2><ul>
|
|
<li><a href="../extensions.html">extensions</a></li>
|
|
<li><a href="../kits.html">kits</a></li>
|
|
</ul><h2>Repository</h2><ul>
|
|
<li><a href="https://github.com/ganelson/inform"><img src="../docs-assets/github.png" height=18> github</a></li>
|
|
</ul><h2>Related Projects</h2><ul>
|
|
<li><a href="../../../inweb/index.html">inweb</a></li>
|
|
<li><a href="../../../intest/index.html">intest</a></li>
|
|
|
|
</ul>
|
|
</nav>
|
|
<main role="main">
|
|
<!--Weave of 'What This Module Does' generated by Inweb-->
|
|
<div class="breadcrumbs">
|
|
<ul class="crumbs"><li><a href="../index.html">Home</a></li><li><a href="../services.html">Services</a></li><li><a href="index.html">calculus</a></li><li><a href="index.html#P">Preliminaries</a></li><li><b>What This Module Does</b></li></ul></div>
|
|
<p class="purpose">An overview of the calculus module's role and abilities.</p>
|
|
|
|
<ul class="toc"><li><a href="P-wtmd.html#SP1">§1. Prerequisites</a></li><li><a href="P-wtmd.html#SP2">§2. What predicate calculus is</a></li><li><a href="P-wtmd.html#SP3">§3. Notation</a></li><li><a href="P-wtmd.html#SP4">§4. Formal description</a></li><li><a href="P-wtmd.html#SP6">§6. Unary predicates</a></li><li><a href="P-wtmd.html#SP7">§7. Binary predicates</a></li><li><a href="P-wtmd.html#SP8">§8. Making propositions</a></li><li><a href="P-wtmd.html#SP11">§11. Sentences</a></li></ul><hr class="tocbar">
|
|
|
|
<p class="commentary firstcommentary"><a id="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>
|
|
|
|
<ul class="items"><li>(a) It helps to have some experience of reading webs: see <a href="../../../inweb/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 <a href="../../../inweb/index.html" class="internal">inweb</a> literate
|
|
programming tool, making it a dialect of C called InC. See <a href="../../../inweb/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 <span class="extract"><span class="extract-syntax">Tags::add_by_name</span></span> rather than <span class="extract"><span class="extract-syntax">add_by_name</span></span>.
|
|
</li><li>(c) This module uses other modules drawn from the compiler (see <a href="../structure.html" class="internal">structure</a>), and also
|
|
uses a module of utility functions called <a href="../../../inweb/foundation-module/index.html" class="internal">foundation</a>.
|
|
For more, see <a href="../../../inweb/foundation-module/P-abgtf.html" class="internal">A Brief Guide to Foundation (in foundation)</a>.
|
|
</li></ul>
|
|
<p class="commentary firstcommentary"><a id="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.<sup id="fnref:1"><a href="#fn:1" rel="footnote">1</a></sup> In particular, any set of rules for making deductions
|
|
tends to be called a "calculus", and we will use a form of one of the most
|
|
popular, "predicate calculus".<sup id="fnref:2"><a href="#fn:2" rel="footnote">2</a></sup>
|
|
</p>
|
|
|
|
<p class="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).<sup id="fnref:3"><a href="#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>
|
|
|
|
<p class="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>
|
|
|
|
<ul class="footnotetexts"><li class="footnote" id="fn:1"><p class="inwebfootnote"><sup id="fnref:1"><a href="#fn:1" rel="footnote">1</a></sup> At time of writing, <a href="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.
|
|
<a href="#fnref:1" title="return to text"> ↩</a></p></li><li class="footnote" id="fn:2"><p class="inwebfootnote"><sup id="fnref:2"><a href="#fn:2" rel="footnote">2</a></sup> Specifically, first order predicate calculus with equality, but with
|
|
generalised quantifiers added, and disjunction removed.
|
|
<a href="#fnref:2" title="return to text"> ↩</a></p></li><li class="footnote" id="fn:3"><p class="inwebfootnote"><sup id="fnref:3"><a href="#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.
|
|
<a href="#fnref:3" title="return to text"> ↩</a></p></li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP3" class="paragraph-anchor"></a><b>§3. Notation. </b>This module deals with propositions in predicate calculus, that is, with
|
|
logical statements which are normally written in mathematical notation. To
|
|
the end user of Inform, these are invisible: they exist only inside the
|
|
compiler and are never typed in or printed out. But for the debugging log,
|
|
for unit testing, and for the literate source, we need to do both of these.
|
|
</p>
|
|
|
|
<p class="commentary">A glimpse of the propositions generated by Inform can be had by running this
|
|
test, whose output uses our notation:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">Laboratory</span><span class="plain-syntax"> </span><span class="identifier-syntax">is</span><span class="plain-syntax"> </span><span class="identifier-syntax">a</span><span class="plain-syntax"> </span><span class="identifier-syntax">room</span><span class="plain-syntax">. </span><span class="identifier-syntax">The</span><span class="plain-syntax"> </span><span class="identifier-syntax">box</span><span class="plain-syntax"> </span><span class="identifier-syntax">is</span><span class="plain-syntax"> </span><span class="identifier-syntax">a</span><span class="plain-syntax"> </span><span class="identifier-syntax">container</span><span class="plain-syntax">.</span>
|
|
<span class="identifier-syntax">Test</span><span class="plain-syntax"> </span><span class="identifier-syntax">sentence</span><span class="plain-syntax"> (</span><span class="identifier-syntax">internal</span><span class="plain-syntax">) </span><span class="identifier-syntax">with</span><span class="plain-syntax"> </span><span class="identifier-syntax">a</span><span class="plain-syntax"> </span><span class="identifier-syntax">man</span><span class="plain-syntax"> </span><span class="identifier-syntax">can</span><span class="plain-syntax"> </span><span class="identifier-syntax">see</span><span class="plain-syntax"> </span><span class="identifier-syntax">the</span><span class="plain-syntax"> </span><span class="identifier-syntax">box</span><span class="plain-syntax"> </span><span class="identifier-syntax">in</span><span class="plain-syntax"> </span><span class="identifier-syntax">the</span><span class="plain-syntax"> </span><span class="identifier-syntax">Laboratory</span><span class="plain-syntax">.</span>
|
|
<span class="identifier-syntax">Test</span><span class="plain-syntax"> </span><span class="identifier-syntax">description</span><span class="plain-syntax"> (</span><span class="identifier-syntax">internal</span><span class="plain-syntax">) </span><span class="identifier-syntax">with</span><span class="plain-syntax"> </span><span class="identifier-syntax">animals</span><span class="plain-syntax"> </span><span class="identifier-syntax">which</span><span class="plain-syntax"> </span><span class="identifier-syntax">are</span><span class="plain-syntax"> </span><span class="identifier-syntax">in</span><span class="plain-syntax"> </span><span class="identifier-syntax">lighted</span><span class="plain-syntax"> </span><span class="identifier-syntax">rooms</span><span class="plain-syntax">.</span>
|
|
</pre>
|
|
<p class="commentary">But a much easier way to test the functions in this module is to use the
|
|
<a href="../calculus-test/index.html" class="internal">calculus-test</a> tool. As with <a href="../kinds-test/index.html" class="internal">kinds-test</a>, this is a REPL: that is,
|
|
a read-evaluate-print-loop tool, which reads in calculations, performs them,
|
|
and prints the result.
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< >></span><span class="plain-syntax">':</span><span class="string-syntax"> << >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< kind = number (x) >></span><span class="plain-syntax">':</span><span class="string-syntax"> << kind=number(x) >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">new unary even</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< even (12) >></span><span class="plain-syntax">':</span><span class="string-syntax"> << even('12') >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< even (x) >></span><span class="plain-syntax">':</span><span class="string-syntax"> << even(x) >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< (x == 7) >></span><span class="plain-syntax">':</span><span class="string-syntax"> << (x == '7') >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">new binary sees (none, sees-f1)</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< sees (x, y) >></span><span class="plain-syntax">':</span><span class="string-syntax"> << sees(x, y) >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< NOT< ^ even (x) ^ NOT> >></span><span class="plain-syntax">':</span><span class="string-syntax"> << NOT< even(x) NOT> >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< Forall x IN< kind = number (x) IN>: even (x) >></span><span class="plain-syntax">':</span><span class="string-syntax"> << ForAll x IN< kind=number(x) IN> : even(x) >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< Exists x >></span><span class="plain-syntax">':</span><span class="string-syntax"> << Exists x >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< DoesNotExist x IN< kind = number (x) IN>: even (x) >></span><span class="plain-syntax">':</span><span class="string-syntax"> << DoesNotExist x IN< kind=number(x) IN> : even(x) >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< Forall x IN< kind = number (x) IN>: even (x) >></span><span class="plain-syntax">':</span><span class="string-syntax"> << ForAll x IN< kind=number(x) IN> : even(x) >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< Card= 6 x IN< kind = number (x) IN>: even (x) >></span><span class="plain-syntax">':</span><span class="string-syntax"> << Card=6 x IN< kind=number(x) IN> : even(x) >></span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP4" class="paragraph-anchor"></a><b>§4. Formal description. </b>1. A "term" is any of the following:
|
|
</p>
|
|
|
|
<ul class="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 <span class="extract"><span class="extract-syntax">x</span></span>, <span class="extract"><span class="extract-syntax">y</span></span>,
|
|
<span class="extract"><span class="extract-syntax">z</span></span>, <span class="extract"><span class="extract-syntax">a</span></span>, <span class="extract"><span class="extract-syntax">b</span></span>, <span class="extract"><span class="extract-syntax">c</span></span>, ..., <span class="extract"><span class="extract-syntax">w</span></span>.
|
|
</li><li>● A function \(f\) applied to another term.<sup id="fnref:4"><a href="#fn:4" rel="footnote">4</a></sup>
|
|
</li></ul>
|
|
<p class="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 <span class="extract"><span class="extract-syntax">x</span></span> is 7,
|
|
then the terms <span class="extract"><span class="extract-syntax">17</span></span>, <span class="extract"><span class="extract-syntax">x</span></span> and <span class="extract"><span class="extract-syntax">f(x)</span></span> evaluate to 17, 7 and \(f(7)\) respectively.
|
|
</p>
|
|
|
|
<p class="commentary">2. An "atomic proposition" is any of the following:
|
|
</p>
|
|
|
|
<ul class="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.<sup id="fnref:5"><a href="#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 <a href="../linguistics-module/2-daq.html" class="internal">Determiners and Quantifiers (in linguistics)</a> for the range
|
|
of quantifiers available.
|
|
</li></ul>
|
|
<p class="commentary">3. A "proposition" is a sequence of 0 or more of the following:
|
|
</p>
|
|
|
|
<ul class="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.<sup id="fnref:6"><a href="#fn:6" rel="footnote">6</a></sup>
|
|
</li><li>● An existential quantification \(\exists v: P\) without a domain.
|
|
</li></ul>
|
|
<ul class="footnotetexts"><li class="footnote" id="fn:4"><p class="inwebfootnote"><sup id="fnref:4"><a href="#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.
|
|
<a href="#fnref:4" title="return to text"> ↩</a></p></li><li class="footnote" id="fn:5"><p class="inwebfootnote"><sup id="fnref:5"><a href="#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.
|
|
<a href="#fnref:5" title="return to text"> ↩</a></p></li><li class="footnote" id="fn:6"><p class="inwebfootnote"><sup id="fnref:6"><a href="#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.
|
|
<a href="#fnref:6" title="return to text"> ↩</a></p></li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP5" class="paragraph-anchor"></a><b>§5. </b>The implementation uses the term "atom" a little more loosely, to include
|
|
four punctuation marks: <span class="extract"><span class="extract-syntax">NOT<</span></span>, <span class="extract"><span class="extract-syntax">NOT></span></span>, <span class="extract"><span class="extract-syntax">IN<</span></span>, <span class="extract"><span class="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>
|
|
|
|
<ul class="items"><li>● \(\lnot P\) is implemented as <span class="extract"><span class="extract-syntax">NOT< P NOT></span></span>.
|
|
</li><li>● \(Q v\in D: P\) is implemented as <span class="extract"><span class="extract-syntax">Q IN< D IN></span></span>.
|
|
</li></ul>
|
|
<p class="commentary">Note that the domain \(D\) of a quantifier is itself expressed as a proposition.
|
|
Thus "for all numbers \(n\)" is implemented as <span class="extract"><span class="extract-syntax">ForAll n IN< kind=number(n) IN></span></span>.
|
|
</p>
|
|
|
|
<p class="commentary">In all other cases, adjacent atoms in a sequence are considered to be conjoined:
|
|
i.e., <span class="extract"><span class="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 <span class="extract"><span class="extract-syntax">^</span></span> sign. For
|
|
example, <span class="extract"><span class="extract-syntax">odd(n) ^ prime(n)</span></span> is the notation for two consecutive atoms <span class="extract"><span class="extract-syntax">odd(n)</span></span>
|
|
and <span class="extract"><span class="extract-syntax">prime(n)</span></span>.
|
|
</p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP6" class="paragraph-anchor"></a><b>§6. Unary predicates. </b>The <a href="index.html" class="internal">calculus</a> module aims to be agnostic about what unary predicates will
|
|
exist. They are grouped into "families" — see <a href="2-upf.html" class="internal">Unary Predicate Families</a>
|
|
for details — which loosely group them by implementation. So, for example,
|
|
Inform has a family of unary predicates in the form <span class="extract"><span class="extract-syntax">calling='whatever'(x)</span></span>
|
|
which assert that <span class="extract"><span class="extract-syntax">x</span></span> represents something of a given name. But <a href="index.html" class="internal">calculus</a>
|
|
is not concerned with the details. Only one family is built in:
|
|
</p>
|
|
|
|
<ul class="items"><li>● For each kind \(K\), there is a predicate <span class="extract"><span class="extract-syntax">kind=K(t)</span></span>, which is true if \(t\)
|
|
is of the kind \(K\).
|
|
</li></ul>
|
|
<p class="commentary">New UPs can be constructed with <a href="2-up.html#SP2" class="internal">UnaryPredicates::new</a>.
|
|
</p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP7" class="paragraph-anchor"></a><b>§7. Binary predicates. </b>Similarly, <a href="index.html" class="internal">calculus</a> allows the user to create as many families of binary
|
|
predicates as are wanted. See <a href="3-bpf.html" class="internal">Binary Predicate Families</a>. For example,
|
|
the "same property value as" relations all belong to a single family. This
|
|
module builds in only one family:
|
|
</p>
|
|
|
|
<ul class="items"><li>● The equality predicate \(=\), whose special meaning is used when simplifying
|
|
propositions. See <a href="3-ter.html" class="internal">The Equality Relation</a>. It is written with the special
|
|
notation <span class="extract"><span class="extract-syntax">(x == y)</span></span>, though this is just syntactic sugar.
|
|
</li></ul>
|
|
<p class="commentary">Binary predicates are of central importance to us because they allow complex
|
|
sentences to be written which talk about more than one thing at a time,
|
|
with some connection between them. In excerpts of Inform source like "an animal
|
|
inside something" or "a man who wears the top hat", the meanings of the two
|
|
connecting pieces of text — "inside" and "who wears" — are binary predicates:
|
|
the containment relation and the wearing relation. To avoid scaring the horses,
|
|
binary predicates are called "relations" in all of the Inform documentation.
|
|
</p>
|
|
|
|
<p class="commentary">New BPs can be constructed with <a href="3-bp.html#SP10" 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.<sup id="fnref:7"><a href="#fn:7" rel="footnote">7</a></sup>
|
|
</p>
|
|
|
|
<ul class="footnotetexts"><li class="footnote" id="fn:7"><p class="inwebfootnote"><sup id="fnref:7"><a href="#fn:7" rel="footnote">7</a></sup> Except for equality, which is its own reversal. See <a href="3-bp.html#SP9" class="internal">BinaryPredicates::make_equality</a>.
|
|
<a href="#fnref:7" title="return to text"> ↩</a></p></li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP8" class="paragraph-anchor"></a><b>§8. Making propositions. </b>Propositions are built incrementally, like Lego, with a sequence of function
|
|
calls.
|
|
</p>
|
|
|
|
<p class="commentary">1. Terms are made using the functions <a href="4-trm.html#SP4" class="internal">Terms::new_constant</a>,
|
|
<a href="4-trm.html#SP4" class="internal">Terms::new_variable</a> and <a href="4-trm.html#SP4" class="internal">Terms::new_function</a>.
|
|
</p>
|
|
|
|
<p class="commentary">2. Unary predicate atoms are made using <a href="4-ap.html#SP10" class="internal">Atoms::binary_PREDICATE_new</a>.
|
|
Binary predicate atoms are made using <a href="4-ap.html#SP10" class="internal">Atoms::binary_PREDICATE_new</a>.
|
|
</p>
|
|
|
|
<p class="commentary">3. Propositions are then built up from atoms or other propositions<sup id="fnref:8"><a href="#fn:8" rel="footnote">8</a></sup> by calling:
|
|
</p>
|
|
|
|
<ul class="items"><li>● <a href="4-prp.html#SP15" class="internal">Propositions::conjoin</a>.
|
|
</li><li>● <a href="4-prp.html#SP16" class="internal">Propositions::negate</a>.
|
|
</li><li>● <a href="4-prp.html#SP16" class="internal">Propositions::quantify</a>.
|
|
</li></ul>
|
|
<ul class="footnotetexts"><li class="footnote" id="fn:8"><p class="inwebfootnote"><sup id="fnref:8"><a href="#fn:8" rel="footnote">8</a></sup> But beware that propositions are passed by reference not value. Use
|
|
<a href="4-prp.html#SP13" class="internal">Propositions::copy</a> before changing one, if you need to use it
|
|
again.
|
|
<a href="#fnref:8" title="return to text"> ↩</a></p></li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP9" class="paragraph-anchor"></a><b>§9. </b>There are two senses in which it's possible to make an impossible proposition:
|
|
</p>
|
|
|
|
<ul class="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) You could concatenate two propositions in which the same variable is
|
|
used with a different meaning in each.
|
|
</li></ul>
|
|
<p class="commentary">The functions <a href="4-prp.html#SP10" class="internal">Propositions::is_syntactically_valid</a> and
|
|
<a href="4-bas.html#SP2" class="internal">Binding::is_well_formed</a> test that (1) and (2) have not happened.
|
|
It's because of (2) that it's important to use <a href="4-prp.html#SP15" class="internal">Propositions::conjoin</a>
|
|
and not the simpler <a href="4-prp.html#SP14" class="internal">Propositions::concatenate</a>.
|
|
</p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP10" class="paragraph-anchor"></a><b>§10. </b>Making propositions is a largely syntactic game, but in the end they will
|
|
have meanings. Terms will have kinds, and relations will only apply to certain
|
|
kinds. This means that some propositions which make syntactic sense will
|
|
nevertheless be "bad": for example, \({\it contains}(7, x)\) is not just untrue
|
|
but at some level meaningless — a number cannot contain things.
|
|
</p>
|
|
|
|
<p class="commentary">Throughout Inform, then, all propositions have to be type-checked before use,
|
|
and this is done by <a href="4-tcp.html#SP4" class="internal">TypecheckPropositions::type_check</a>.
|
|
</p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP11" class="paragraph-anchor"></a><b>§11. Sentences. </b>Our whole interest in propositions is to use them to provide a meaning for
|
|
a sentence of natural language: we evaluate text like "Peter is in the car"
|
|
into a proposition.<sup id="fnref:9"><a href="#fn:9" rel="footnote">9</a></sup> This task is central to how Inform works, and occupies
|
|
the whole of <a href="5-sc.html" class="internal">Sentence Conversions</a>.
|
|
</p>
|
|
|
|
<p class="commentary">On the face of it, this is a simple matter of conjoining propositions for
|
|
the subject (Peter) and the object (the car) together with a binary predicate
|
|
(is-in). But most cases are not so simple, and if we did only that then we
|
|
would often end up with a much longer proposition than necessary, which it
|
|
would be inefficient to test or assert at run-time. So the sentence converter
|
|
makes use of logical deductions to "simplify" its output, and these tactics
|
|
form roughly 20 functions in the <a href="5-smp.html" class="internal">Simplifications</a> section.
|
|
</p>
|
|
|
|
<ul class="footnotetexts"><li class="footnote" id="fn:9"><p class="inwebfootnote"><sup id="fnref:9"><a href="#fn:9" rel="footnote">9</a></sup> In fact, a proposition with no free variables. It's not a coincidence that
|
|
logicians call such propositions "sentences".
|
|
<a href="#fnref:9" title="return to text"> ↩</a></p></li></ul>
|
|
<nav role="progress"><div class="progresscontainer">
|
|
<ul class="progressbar"><li class="progressprevoff">❮</li><li class="progresscurrentchapter">P</li><li class="progresscurrent">wtmd</li><li class="progresssection"><a href="P-htitm.html">htitm</a></li><li class="progresschapter"><a href="1-cm.html">1</a></li><li class="progresschapter"><a href="2-up.html">2</a></li><li class="progresschapter"><a href="3-bpf.html">3</a></li><li class="progresschapter"><a href="4-trm.html">4</a></li><li class="progresschapter"><a href="5-sc.html">5</a></li><li class="progressnext"><a href="P-htitm.html">❯</a></li></ul></div>
|
|
</nav><!--End of weave-->
|
|
|
|
</main>
|
|
</body>
|
|
</html>
|
|
|