<ulclass="crumbs"><li><ahref="../webs.html">★</a></li><li><ahref="index.html">core</a></li><li><ahref="index.html#12">Chapter 12: Use of Propositions</a></li><li><b>Compile Deferred Propositions</b></li></ul><pclass="purpose">To compile the I6 routines needed to perform the tests or tasks deferred as being too difficult in their original contexts.</p>
<ulclass="toc"><li><ahref="#SP1">§1. Comment</a></li><li><ahref="#SP2">§2. Preliminaries</a></li><li><ahref="#SP2_1_6_1_1">§2.1.6.1.1. The Search</a></li><li><ahref="#SP2_1_6_1_2_1">§2.1.6.1.2.1. The R-stack</a></li><li><ahref="#SP2_1_6_1_2_3">§2.1.6.1.2.3. Compiling the search</a></li><li><ahref="#SP2_1_6_1_2_3_1">§2.1.6.1.2.3.1. Predicate runs and their negations</a></li><li><ahref="#SP2_1_6_1_2_3_5">§2.1.6.1.2.3.5. Quantifiers and the Q-stack</a></li><li><ahref="#SP2_1_6_1_2_3_8">§2.1.6.1.2.3.8. The C-stack</a></li><li><ahref="#SP2_1_5_1">§2.1.5.1. Adaptations</a></li><li><ahref="#SP2_1_6_1_3">§2.1.6.1.3. Adaptation to CONDITION</a></li><li><ahref="#SP2_1_6_1_5">§2.1.6.1.5. Adaptation to NUMBER</a></li><li><ahref="#SP2_1_6_1_8">§2.1.6.1.8. Adaptation to LIST</a></li><li><ahref="#SP2_1_6_1_10">§2.1.6.1.10. Adaptation to RANDOM</a></li><li><ahref="#SP2_1_6_1_12">§2.1.6.1.12. Adaptation to TOTAL</a></li><li><ahref="#SP2_1_6_1_14">§2.1.6.1.14. Adaptation to EXTREMAL</a></li><li><ahref="#SP2_1_6_1_16">§2.1.6.1.16. Adaptation to LOOP</a></li><li><ahref="#SP3">§3. Compiling loop headers</a></li></ul><hrclass="tocbar">
<pclass="inwebparagraph"><aid="SP1"></a><b>§1. Comment. </b>The following compiles an I6 comment noting the reason for a deferral.
<spanclass="functiontext">Emit::code_comment</span><spanclass="plain">(</span><spanclass="identifier">I</span><spanclass="string">"! True or false?"</span><spanclass="plain">); </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="functiontext">Emit::code_comment</span><spanclass="plain">(</span><spanclass="identifier">I</span><spanclass="string">"! Force this to be true via 'now':"</span><spanclass="plain">); </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="functiontext">Emit::code_comment</span><spanclass="plain">(</span><spanclass="identifier">I</span><spanclass="string">"! Find the extremal x satisfying:"</span><spanclass="plain">); </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="functiontext">Emit::code_comment</span><spanclass="plain">(</span><spanclass="identifier">I</span><spanclass="string">"! Find next x satisfying:"</span><spanclass="plain">); </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="functiontext">Emit::code_comment</span><spanclass="plain">(</span><spanclass="identifier">I</span><spanclass="string">"! Construct a list of x satisfying:"</span><spanclass="plain">); </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="functiontext">Emit::code_comment</span><spanclass="plain">(</span><spanclass="identifier">I</span><spanclass="string">"! How many x satisfy this?"</span><spanclass="plain">); </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="functiontext">Emit::code_comment</span><spanclass="plain">(</span><spanclass="identifier">I</span><spanclass="string">"! Find a total property value over all x satisfying:"</span><spanclass="plain">); </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="functiontext">Emit::code_comment</span><spanclass="plain">(</span><spanclass="identifier">I</span><spanclass="string">"! Find a random x satisfying:"</span><spanclass="plain">); </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="functiontext">Emit::code_comment</span><spanclass="plain">(</span><spanclass="identifier">I</span><spanclass="string">"! Abstraction for set of x such that:"</span><spanclass="plain">); </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<pclass="endnote">The function Calculus::Propositions::Deferred::compile_comment_about_deferral_reason is used in <ahref="#SP2_1_6">§2.1.6</a>.</p>
<pclass="inwebparagraph"><aid="SP2"></a><b>§2. Preliminaries. </b>We have seen that propositions are deferred for diverse reasons. Here we
take our medicine, and actually compile the deferred propositions into
routines. This is part of the phrase-compilation-coroutine process because
funny things can happen when we compile: we can create new text substitutions
<pclass="endnote">The function Calculus::Propositions::Deferred::compile_remaining_deferred is used in 1/htc (<ahref="1-htc.html#SP2_8">§2.8</a>).</p>
<pclass="endnote">The function Calculus::Propositions::Deferred::compilation_coroutine is used in 22/cs (<ahref="22-cs.html#SP14">§14</a>).</p>
<pclass="inwebparagraph"><aid="SP2_1"></a><b>§2.1. </b>The basic structure of a proposition routine is the same for all
of the various reasons, but with considerable variations affecting (mainly)
the initial setup and the returned value.
</p>
<pclass="inwebparagraph">Note that the unchecked array bounds of 26 are safe here because
propositions may only use 26 different variables at most (<codeclass="display"><spanclass="extract">x</span></code>, <codeclass="display"><spanclass="extract">y</span></code>, <codeclass="display"><spanclass="extract">z</span></code>,
<codeclass="display"><spanclass="extract">a</span></code>, ..., <codeclass="display"><spanclass="extract">w</span></code>). There therefore can't be more than 26 callings, or 26
<<spanclass="cwebmacro">Simplify the proposition by flipping negated quantifiers, if possible</span><spanclass="cwebmacronumber">2.1.2</span>><spanclass="plain">;</span>
<<spanclass="cwebmacro">Declare the I6 local variables which will be needed by this deferral routine</span><spanclass="cwebmacronumber">2.1.5</span>><spanclass="plain">;</span>
<<spanclass="cwebmacro">Compile the code inside this deferral routine</span><spanclass="cwebmacronumber">2.1.6</span>><spanclass="plain">;</span>
<<spanclass="cwebmacro">Issue a problem message if the table-lookup locals were needed</span><spanclass="cwebmacronumber">2.1.3</span>><spanclass="plain">;</span>
<<spanclass="cwebmacro">Issue a problem message if a negated quantifier was needed</span><spanclass="cwebmacronumber">2.1.4</span>><spanclass="plain">;</span>
<spanclass="reserved">if</span><spanclass="plain"> (</span><spanclass="identifier">pdef</span><spanclass="plain">-</span><spanclass="element">>rtp_iname</span><spanclass="plain">) </span><<spanclass="cwebmacro">Compile the constant origin text for run-time problem use</span><spanclass="cwebmacronumber">2.1.1</span>><spanclass="plain">;</span>
<spanclass="identifier">WRITE_TO</span><spanclass="plain">(</span><spanclass="identifier">COTT</span><spanclass="plain">, </span><spanclass="string">"not sure where this came from"</span><spanclass="plain">);</span>
<pclass="endnote">This code is used in <ahref="#SP2_1">§2.1</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_2"></a><b>§2.1.2. </b>Just in case this hasn't already been done:
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Simplify the proposition by flipping negated quantifiers, if possible</span><spanclass="cwebmacronumber">2.1.2</span>> =
<spanclass="string">"this involves a very complicated negative thought"</span><spanclass="plain">,</span>
<spanclass="string">"which I'm not able to untangle. Perhaps you could rephrase "</span>
<spanclass="string">"this more simply, or split it into more than one sentence?"</span><spanclass="plain">);</span>
<spanclass="plain">}</span>
</pre>
<pclass="inwebparagraph"></p>
<pclass="endnote">This code is used in <ahref="#SP2_1">§2.1</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_5"></a><b>§2.1.5. </b>Recall that an I6 function header consists of a <codeclass="display"><spanclass="extract">[</span></code>, then an identifier
name for the function — in this case always <codeclass="display"><spanclass="extract">Prop_N</span></code> for some number <codeclass="display"><spanclass="extract">N</span></code>—
and then a space-delimited list of local variable names, the initial of
which are used to receive function arguments. The order of the variables
is: any cinders (constants evaluated back at deferral time and being
handed forward on the stack as function arguments); then any variables
in the predicate calculus sense, of which the first may or may not be
being used as a function argument, depending on whether or not it is
bound; then the enumeration variables needed to compile generalised
quantifiers, if any; and finally any oddball variables needed by code
specific to particular deferral reasons.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Declare the I6 local variables which will be needed by this deferral routine</span><spanclass="cwebmacronumber">2.1.5</span>> =
<<spanclass="cwebmacro">Declare the I6 call parameters needed by adaptations to particular deferral cases</span><spanclass="cwebmacronumber">2.1.5.2</span>><spanclass="plain">;</span>
<<spanclass="cwebmacro">Declare the I6 locals needed by adaptations to particular deferral cases</span><spanclass="cwebmacronumber">2.1.5.1</span>><spanclass="plain">;</span>
</pre>
<pclass="inwebparagraph"></p>
<pclass="endnote">This code is used in <ahref="#SP2_1">§2.1</a>.</p>
<<spanclass="cwebmacro">Compile body of deferred proposition for the given reason</span><spanclass="cwebmacronumber">2.1.6.1</span>><spanclass="plain">;</span>
<<spanclass="cwebmacro">Compile body of deferred proposition for the given reason</span><spanclass="cwebmacronumber">2.1.6.1</span>><spanclass="plain">;</span>
<spanclass="plain">}</span>
</pre>
<pclass="inwebparagraph"></p>
<pclass="endnote">This code is used in <ahref="#SP2_1">§2.1</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1"></a><b>§2.1.6.1. </b>From here on, we compile the body of a routine to handle the deferral case
in the variable <codeclass="display"><spanclass="extract">reason</span></code>.
</p>
<pclass="inwebparagraph">What these different cases have in common is that each is basically a search
of all possible values of the bound variables in the expression. There will
be some initialisation, something to do with each successfully found
combination, and eventually some winding-up code. For example, "number of..."
initialises by setting <codeclass="display"><spanclass="extract">counter</span></code> to 0, on each success it performs <codeclass="display"><spanclass="extract">counter++</span></code>,
and at the end of the search it performs <codeclass="display"><spanclass="extract">return counter</span></code>.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Compile body of deferred proposition for the given reason</span><spanclass="cwebmacronumber">2.1.6.1</span>> =
<spanclass="reserved">case</span><spanclass="plain"></span><spanclass="constant">CONDITION_DEFER</span><spanclass="plain">: </span><<spanclass="cwebmacro">Initialisation before CONDITION search</span><spanclass="cwebmacronumber">2.1.6.1.3</span>><spanclass="plain">; </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="reserved">case</span><spanclass="plain"></span><spanclass="constant">EXTREMAL_DEFER</span><spanclass="plain">: </span><<spanclass="cwebmacro">Initialisation before EXTREMAL search</span><spanclass="cwebmacronumber">2.1.6.1.14</span>><spanclass="plain">; </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="reserved">case</span><spanclass="plain"></span><spanclass="constant">LOOP_DOMAIN_DEFER</span><spanclass="plain">: </span><<spanclass="cwebmacro">Initialisation before LOOP search</span><spanclass="cwebmacronumber">2.1.6.1.17</span>><spanclass="plain">; </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="reserved">case</span><spanclass="plain"></span><spanclass="constant">NUMBER_OF_DEFER</span><spanclass="plain">: </span><<spanclass="cwebmacro">Initialisation before NUMBER search</span><spanclass="cwebmacronumber">2.1.6.1.5</span>><spanclass="plain">; </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="reserved">case</span><spanclass="plain"></span><spanclass="constant">LIST_OF_DEFER</span><spanclass="plain">: </span><<spanclass="cwebmacro">Initialisation before LIST search</span><spanclass="cwebmacronumber">2.1.6.1.8</span>><spanclass="plain">; </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="reserved">case</span><spanclass="plain"></span><spanclass="constant">TOTAL_DEFER</span><spanclass="plain">: </span><<spanclass="cwebmacro">Initialisation before TOTAL search</span><spanclass="cwebmacronumber">2.1.6.1.12</span>><spanclass="plain">; </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="reserved">case</span><spanclass="plain"></span><spanclass="constant">RANDOM_OF_DEFER</span><spanclass="plain">: </span><<spanclass="cwebmacro">Initialisation before RANDOM search</span><spanclass="cwebmacronumber">2.1.6.1.10</span>><spanclass="plain">; </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="plain">}</span>
<<spanclass="cwebmacro">Compile code to search for valid combinations of variables</span><spanclass="cwebmacronumber">2.1.6.1.2</span>><spanclass="plain">;</span>
<spanclass="reserved">case</span><spanclass="plain"></span><spanclass="constant">CONDITION_DEFER</span><spanclass="plain">: </span><<spanclass="cwebmacro">Winding-up after CONDITION search</span><spanclass="cwebmacronumber">2.1.6.1.4</span>><spanclass="plain">; </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="reserved">case</span><spanclass="plain"></span><spanclass="constant">EXTREMAL_DEFER</span><spanclass="plain">: </span><<spanclass="cwebmacro">Winding-up after EXTREMAL search</span><spanclass="cwebmacronumber">2.1.6.1.15</span>><spanclass="plain">; </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="reserved">case</span><spanclass="plain"></span><spanclass="constant">LOOP_DOMAIN_DEFER</span><spanclass="plain">: </span><<spanclass="cwebmacro">Winding-up after LOOP search</span><spanclass="cwebmacronumber">2.1.6.1.18</span>><spanclass="plain">; </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="reserved">case</span><spanclass="plain"></span><spanclass="constant">NUMBER_OF_DEFER</span><spanclass="plain">: </span><<spanclass="cwebmacro">Winding-up after NUMBER search</span><spanclass="cwebmacronumber">2.1.6.1.7</span>><spanclass="plain">; </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="reserved">case</span><spanclass="plain"></span><spanclass="constant">LIST_OF_DEFER</span><spanclass="plain">: </span><<spanclass="cwebmacro">Winding-up after LIST search</span><spanclass="cwebmacronumber">2.1.6.1.9</span>><spanclass="plain">; </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="reserved">case</span><spanclass="plain"></span><spanclass="constant">TOTAL_DEFER</span><spanclass="plain">: </span><<spanclass="cwebmacro">Winding-up after TOTAL search</span><spanclass="cwebmacronumber">2.1.6.1.13</span>><spanclass="plain">; </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="reserved">case</span><spanclass="plain"></span><spanclass="constant">RANDOM_OF_DEFER</span><spanclass="plain">: </span><<spanclass="cwebmacro">Winding-up after RANDOM search</span><spanclass="cwebmacronumber">2.1.6.1.11</span>><spanclass="plain">; </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="plain">}</span>
</pre>
<pclass="inwebparagraph"></p>
<pclass="endnote">This code is used in <ahref="#SP2_1_6">§2.1.6</a> (twice).</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_1"></a><b>§2.1.6.1.1. The Search. </b>We can now begin the real work. Given φ, we compile I6 code which
contains a magic position M (for "match") such that M is visited exactly
once for every combination of possible substitutions into the bound
variables such that φ is true. For example,
∃ x: door(x)∧open(x)∧ ∃ y: room(y)∧in(x, y)
might compile to code in the form:
</p>
<pclass="inwebparagraph"></p>
<preclass="display">
<spanclass="plain">blah, blah, blah {</span>
<spanclass="plain"> M</span>
<spanclass="plain">} rhubarb, rhubarb</span>
</pre>
<pclass="inwebparagraph">such that execution reaches <codeclass="display"><spanclass="extract">M</span></code> exactly once for each combination of open
door x and room y such that x is in y. (Position <codeclass="display"><spanclass="extract">M</span></code> is where we
will place the case-dependent code for what to do on a successful match.)
In the language of model theory, this is a loop over all interpretations
in which φ is true.
</p>
<pclass="inwebparagraph">We will do this by compiling the proposition from left to right. If there
are k atoms in φ, then there are k+1 positions between atoms,
counting the start and the end. Then:
</p>
<pclass="inwebparagraph">Invariant. Let ψ be any syntactically valid subproposition
of φ (that is, a contiguous sequence of atoms from ψ which would
be a valid proposition in its own right). Then there are before and after
positions <codeclass="display"><spanclass="extract">B</span></code> and <codeclass="display"><spanclass="extract">A</span></code> in the compiled I6 code for searching φ such that
</p>
<ulclass="items"><li>(a) <codeclass="display"><spanclass="extract">A</span></code> cannot be reached except from <codeclass="display"><spanclass="extract">B</span></code>, and
</li><li>(b) at execution time, on every occasion <codeclass="display"><spanclass="extract">B</span></code> is reached, <codeclass="display"><spanclass="extract">A</span></code> is then reached
exactly once for each combination of possible substitutions into the
∃-bound variables of ψ such that ψ is then true.
</li></ul>
<pclass="inwebparagraph">In particular, in the case when ψ = φ, <codeclass="display"><spanclass="extract">B</span></code> is the start of our
compiled I6 code (before anything is done) and <codeclass="display"><spanclass="extract">A</span></code> is the magic match
position <codeclass="display"><spanclass="extract">M</span></code>.
</p>
<pclass="inwebparagraph">The restriction to syntactically valid subpropositions is important. Suppose
φ arises from "all doors are open" and is stored in memory as:
</p>
<pclass="inwebparagraph"></p>
<preclass="display">
<spanclass="plain">Forall x IN[ door(x) IN] open(x)</span>
</pre>
<pclass="inwebparagraph">Then <codeclass="display"><spanclass="extract">door(x)</span></code> and <codeclass="display"><spanclass="extract">Forall x IN[ door(x) IN]</span></code> are valid, for instance, but
<codeclass="display"><spanclass="extract">IN] open(x)</span></code> is not.
</p>
<pclass="inwebparagraph">Lemma. If the Invariant holds for two adjacent syntactically valid
subpropositions μ and ν, then it holds for the subproposition μν.
</p>
<pclass="inwebparagraph">Proof. There are now three positions in the code: <codeclass="display"><spanclass="extract">B1</span></code>, before μ;
<codeclass="display"><spanclass="extract">B2</span></code>, before ν, which is the same position as after μ; and <codeclass="display"><spanclass="extract">A</span></code>, after
ν. Execution reaches <codeclass="display"><spanclass="extract">B2</span></code> m times for each visit to <codeclass="display"><spanclass="extract">B1</span></code>, where m
is the number of combinations of viable bound variable values in μ.
Execution reaches <codeclass="display"><spanclass="extract">A</span></code> n times for each visit to <codeclass="display"><spanclass="extract">B2</span></code>, where n is the
similar number for ν. Therefore execution reaches <codeclass="display"><spanclass="extract">A</span></code> a total of nm
times for each visit to <codeclass="display"><spanclass="extract">B1</span></code>, the product of the number of variable combinations
in μ and ν, which is exactly the number of combinations in total.
</p>
<pclass="inwebparagraph">Corollary. If the Invariant holds for subpropositions in each of
the following forms, then it will hold overall.
</p>
<ulclass="items"><li>(a) <codeclass="display"><spanclass="extract">Exists v</span></code>, for some variable v, or <codeclass="display"><spanclass="extract">Q v IN[ ... IN]</span></code>, for some quantifier other than ∃.
<pclass="inwebparagraph">Proof. Because all valid subpropositions are concatenations of
these, and we then apply the Lemma.
</p>
<pclass="inwebparagraph">It follows that if we can prove our algorithm maintains the invariant in
cases (a) to (d), we can be sure it will correctly construct code leading
to the match point <codeclass="display"><spanclass="extract">M</span></code>.
</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_2"></a><b>§2.1.6.1.2. </b>We will make use of three stacks:
</p>
<pclass="inwebparagraph"></p>
<ulclass="items"><li>(a) The R-stack, which holds the current "reason": the goal being pursued
by the I6 code currently being compiled.
</li><li>(b) The Q-stack, which holds details of quantifiers being searched on.
</li><li>(c) The C-stack, which holds details of callings of variables.
</li></ul>
<pclass="inwebparagraph">Since each is tied to a quantifier, each of which is tied to a distinct
variable, and there are at most 26 variables, we need a worst-case
capacity of 27 slots on the R-stack (counting the initial <codeclass="display"><spanclass="extract">reason</span></code>) and
26 on the Q-stack and C-stack.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Compile code to search for valid combinations of variables</span><spanclass="cwebmacronumber">2.1.6.1.2</span>> =
</code></p>
<preclass="displaydefn">
<spanclass="reserved">int</span><spanclass="plain"></span><spanclass="identifier">block_nesting</span><spanclass="plain"> = 0; </span><spanclass="comment">how many <codeclass="display"><spanclass="extract">{</span></code> ... <codeclass="display"><spanclass="extract">}</span></code> blocks are open in I6 code being compiled</span>
<spanclass="reserved">pcalc_term</span><spanclass="plain"></span><spanclass="identifier">C_stack_term</span><spanclass="plain">[26]; </span><spanclass="comment">the term to which a called-name is being given</span>
<spanclass="reserved">int</span><spanclass="plain"></span><spanclass="identifier">C_stack_index</span><spanclass="plain">[26]; </span><spanclass="comment">its index in the <codeclass="display"><spanclass="extract">deferred_calling_list</span></code></span>
<spanclass="reserved">int</span><spanclass="plain"></span><spanclass="identifier">L_stack_level</span><spanclass="plain">[26]; </span><spanclass="comment">emission level at start of block</span>
<spanclass="comment">block_nesting serves at stack pointer here</span>
<<spanclass="cwebmacro">Push initial reason onto the R-stack</span><spanclass="cwebmacronumber">2.1.6.1.2.1</span>><spanclass="plain">;</span>
<spanclass="comment">we now begin compiling the search code</span>
<<spanclass="cwebmacro">Compile the proposition into a search algorithm</span><spanclass="cwebmacronumber">2.1.6.1.2.3</span>><spanclass="plain">;</span>
<spanclass="reserved">while</span><spanclass="plain"> (</span><spanclass="identifier">Q_sp</span><spanclass="plain">> 0) </span><<spanclass="cwebmacro">Pop the Q-stack</span><spanclass="cwebmacronumber">2.1.6.1.2.4</span>><spanclass="plain">;</span>
<spanclass="reserved">while</span><spanclass="plain"> (</span><spanclass="identifier">C_sp</span><spanclass="plain">> 0) </span><<spanclass="cwebmacro">Pop the C-stack</span><spanclass="cwebmacronumber">2.1.6.1.2.5</span>><spanclass="plain">;</span>
<spanclass="comment">we are now at the magic match point <codeclass="display"><spanclass="extract">M</span></code> in the search code</span>
<<spanclass="cwebmacro">Pop the R-stack</span><spanclass="cwebmacronumber">2.1.6.1.2.2</span>><spanclass="plain">;</span>
<<spanclass="cwebmacro">Close a block in the I6 code compiled to perform the search</span><spanclass="cwebmacronumber">2.1.6.1.2.6</span>><spanclass="plain">;</span>
<spanclass="comment">we have now finished compiling the search code</span>
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1">§2.1.6.1</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_2_1"></a><b>§2.1.6.1.2.1. The R-stack. </b>This is a sort of "split goals into sub-goals" mechanism. In order to
determine
</p>
<blockquote>
<p>if all but one of the closed doors are unlocked, ...</p>
</blockquote>
<pclass="inwebparagraph">our main goal is to determine the truth of the "are unlocked" part. This
is reason <codeclass="display"><spanclass="extract">CONDITION_DEFER</span></code>, and it is pushed onto the R-stack at the
start of the compilation:
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Push initial reason onto the R-stack</span><spanclass="cwebmacronumber">2.1.6.1.2.1</span>> =
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1_2">§2.1.6.1.2</a>.</p>
<pclass="inwebparagraph"><aid="SP_1"></a><b>§.1. </b>But in order to work this out, we have to work out which doors are
closed, and this is a subgoal to which we give the pseudo-reason
<codeclass="display"><spanclass="extract">FILTER_DEFER</span></code>. We push this new sub-goal onto the R-stack, leaving the
original to be resumed when we're done.
</p>
<preclass="definitions">
<spanclass="definitionkeyword">define</span><spanclass="constant">FILTER_DEFER</span><spanclass="plain"> 10000 </span><spanclass="comment">pseudo-reason value used only inside this routine</span>
</pre>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Push domain-opening onto the R-stack</span><spanclass="cwebmacronumber">.1</span>> =
<spanclass="reserved">case</span><spanclass="plain"></span><spanclass="constant">CONDITION_DEFER</span><spanclass="plain">: </span><<spanclass="cwebmacro">Act on successful match in CONDITION search</span><spanclass="cwebmacronumber">2.1.6.1.2.2.1</span>><spanclass="plain">; </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="reserved">case</span><spanclass="plain"></span><spanclass="constant">EXTREMAL_DEFER</span><spanclass="plain">: </span><<spanclass="cwebmacro">Act on successful match in EXTREMAL search</span><spanclass="cwebmacronumber">2.1.6.1.2.2.6</span>><spanclass="plain">; </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="reserved">case</span><spanclass="plain"></span><spanclass="constant">LOOP_DOMAIN_DEFER</span><spanclass="plain">: </span><<spanclass="cwebmacro">Act on successful match in LOOP search</span><spanclass="cwebmacronumber">2.1.6.1.2.2.7</span>><spanclass="plain">; </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="reserved">case</span><spanclass="plain"></span><spanclass="constant">NUMBER_OF_DEFER</span><spanclass="plain">: </span><<spanclass="cwebmacro">Act on successful match in NUMBER search</span><spanclass="cwebmacronumber">2.1.6.1.2.2.2</span>><spanclass="plain">; </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="reserved">case</span><spanclass="plain"></span><spanclass="constant">LIST_OF_DEFER</span><spanclass="plain">: </span><<spanclass="cwebmacro">Act on successful match in LIST search</span><spanclass="cwebmacronumber">2.1.6.1.2.2.3</span>><spanclass="plain">; </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="reserved">case</span><spanclass="plain"></span><spanclass="constant">TOTAL_DEFER</span><spanclass="plain">: </span><<spanclass="cwebmacro">Act on successful match in TOTAL search</span><spanclass="cwebmacronumber">2.1.6.1.2.2.5</span>><spanclass="plain">; </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="reserved">case</span><spanclass="plain"></span><spanclass="constant">RANDOM_OF_DEFER</span><spanclass="plain">: </span><<spanclass="cwebmacro">Act on successful match in RANDOM search</span><spanclass="cwebmacronumber">2.1.6.1.2.2.4</span>><spanclass="plain">; </span><spanclass="reserved">break</span><spanclass="plain">;</span>
<spanclass="plain">}</span>
</pre>
<pclass="inwebparagraph"></p>
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1_2">§2.1.6.1.2</a>, <ahref="#SP2_1_6_1_2_3">§2.1.6.1.2.3</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_2_3"></a><b>§2.1.6.1.2.3. Compiling the search. </b>In the following we run through the proposition from left to right, compiling
I6 code as we go, but preserving the Invariant.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Compile the proposition into a search algorithm</span><spanclass="cwebmacronumber">2.1.6.1.2.3</span>> =
<spanclass="reserved">int</span><spanclass="plain"></span><spanclass="identifier">no_deferred_callings</span><spanclass="plain"> = 0; </span><spanclass="comment">how many <codeclass="display"><spanclass="extract">CALLED</span></code> atoms have been found to date</span>
<<spanclass="cwebmacro">End a run of predicate-like conditions, if one is under way</span><spanclass="cwebmacronumber">2.1.6.1.2.3.3</span>><spanclass="plain">;</span>
<<spanclass="cwebmacro">End a run of predicate-like conditions, if one is under way</span><spanclass="cwebmacronumber">2.1.6.1.2.3.3</span>><spanclass="plain">;</span>
<spanclass="reserved">if</span><spanclass="plain"> (</span><spanclass="identifier">quant</span><spanclass="plain"> != </span><spanclass="identifier">exists_quantifier</span><spanclass="plain">) </span><<spanclass="cwebmacro">Push the Q-stack</span><spanclass="cwebmacronumber">2.1.6.1.2.3.7</span>><spanclass="plain">;</span>
<<spanclass="cwebmacro">Compile a loop through possible values of the variable quantified</span><spanclass="cwebmacronumber">2.1.6.1.2.3.5</span>><spanclass="plain">;</span>
<<spanclass="cwebmacro">End a run of predicate-like conditions, if one is under way</span><spanclass="cwebmacronumber">2.1.6.1.2.3.3</span>><spanclass="plain">;</span>
<<spanclass="cwebmacro">Push domain-opening onto the R-stack</span><spanclass="cwebmacronumber">.1</span>><spanclass="plain">;</span>
<<spanclass="cwebmacro">End a run of predicate-like conditions, if one is under way</span><spanclass="cwebmacronumber">2.1.6.1.2.3.3</span>><spanclass="plain">;</span>
<<spanclass="cwebmacro">Pop the R-stack</span><spanclass="cwebmacronumber">2.1.6.1.2.2</span>><spanclass="plain">;</span>
<<spanclass="cwebmacro">End a run of predicate-like conditions, if one is under way</span><spanclass="cwebmacronumber">2.1.6.1.2.3.3</span>><spanclass="plain">;</span>
</pre>
<pclass="inwebparagraph"></p>
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1_2">§2.1.6.1.2</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_2_3_1"></a><b>§2.1.6.1.2.3.1. Predicate runs and their negations. </b>Or, cheating Professor de Morgan.
</p>
<pclass="inwebparagraph">If we have a run of predicate-like atoms — say X, Y, Z — then this amounts
to a conjunction: X∧ Y∧ Z. The obvious way to compile code for this
would be to take one term at a time:
</p>
<pclass="inwebparagraph"></p>
<preclass="display">
<spanclass="plain">if (X)</span>
<spanclass="plain"> if (Y)</span>
<spanclass="plain"> if (Z)</span>
</pre>
<pclass="inwebparagraph">That satisfies the Invariant, and is clearly correct. But we want to use the
same mechanism when looking at a negation, and then it would go wrong.
</p>
<pclass="inwebparagraph">Note that if φ contains ¬(ψ) then ψ must be a
conjunction of predicate-like atoms. (Otherwise a problem message would be
issued and in that case it doesn't matter what code we compile, so long as
we don't crash: it will never be run.) Thus we can assume that between
<codeclass="display"><spanclass="extract">NEGATION_OPEN_ATOM</span></code> and <codeclass="display"><spanclass="extract">NEGATION_CLOSE_ATOM</span></code> is a predicate run.
</p>
<pclass="inwebparagraph">Between negation brackets, then, we must interpret X, Y, Z as
¬(X∧ Y∧ Z), and we need to compile that to
</p>
<pclass="inwebparagraph"></p>
<preclass="display">
<spanclass="plain">if (~~(X && Y && Z))</span>
</pre>
<pclass="inwebparagraph">rather than
</p>
<pclass="inwebparagraph"></p>
<preclass="display">
<spanclass="plain">if (~~X)</span>
<spanclass="plain"> if (~~Y)</span>
<spanclass="plain"> if (~~Z)</span>
</pre>
<pclass="inwebparagraph">which gets de Morgan's laws wrong.
</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_2_3_2"></a><b>§2.1.6.1.2.3.2. </b>That means a little fancy footwork to start and finish the compound <codeclass="display"><spanclass="extract">if</span></code>
statement properly:
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Compile code to test the atom</span><spanclass="cwebmacronumber">2.1.6.1.2.3.2</span>> =
<<spanclass="cwebmacrodefn">End a run of predicate-like conditions, if one is under way</span><spanclass="cwebmacronumber">2.1.6.1.2.3.3</span>> =
<<spanclass="cwebmacro">Open a block in the I6 code compiled to perform the search, if variant</span><spanclass="cwebmacronumber">2.1.6.1.2.3.3.1</span>><spanclass="plain">;</span>
<spanclass="plain">}</span>
</pre>
<pclass="inwebparagraph"></p>
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1_2_3">§2.1.6.1.2.3</a> (five times).</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_2_3_4"></a><b>§2.1.6.1.2.3.4. </b>The <codeclass="display"><spanclass="extract">NOW_ASSERTION_DEFER</span></code> reason is different from all of the others,
because rather than searching for a given situation it tries force it to
happen (or not to). Forcing rather than testing is easy here: we just supply
a different task when calling <codeclass="display"><spanclass="extract">Calculus::Atoms::Compile::compile</span></code>.
</p>
<pclass="inwebparagraph">In the negated case, we again cheat de Morgan, by falsifying φ more
aggressively than we need: we force ¬(X)∧¬(Y)∧¬(Z) to
be true, though strictly speaking it would be enough to falsify X alone.
(We do it that way for consistency with the same convention when asserting
about the model world.)
</p>
<pclass="inwebparagraph">We don't need to consider runs of predicates for that; we can take the atoms
one at a time.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Compile code to force the atom</span><spanclass="cwebmacronumber">2.1.6.1.2.3.4</span>> =
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1_2_3">§2.1.6.1.2.3</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_2_3_5"></a><b>§2.1.6.1.2.3.5. Quantifiers and the Q-stack. </b>It remains to deal with quantifiers, and to show that the Invariant is
preserved by them. There are two cases: ∃, and everything else.
</p>
<pclass="inwebparagraph">The existence case is the easiest. Given ∃ v: ψ(v) we compile
</p>
<pclass="inwebparagraph"></p>
<preclass="display">
<spanclass="plain">loop header for v to run through its domain set {</span>
<spanclass="plain"> ...</span>
</pre>
<pclass="inwebparagraph">and note that execution reaches the start of the loop body once for each
possible choice of v, as required by the Invariant — indeed the Invariant
pretty much requires that this is what we compile.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Compile a loop through possible values of the variable quantified</span><spanclass="cwebmacronumber">2.1.6.1.2.3.5</span>> =
<<spanclass="cwebmacro">Open a block in the I6 code compiled to perform the search</span><spanclass="cwebmacronumber">2.1.6.1.2.3.5.1</span>><spanclass="plain">;</span>
</pre>
<pclass="inwebparagraph"></p>
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1_2_3">§2.1.6.1.2.3</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_2_3_6"></a><b>§2.1.6.1.2.3.6. </b>Generalised quantifiers — "at least three", "all but four", and
so on — make quantitative statements about the number of valid or invalid
cases over a domain set. These need more elaborate code. Suppose we have
<pclass="inwebparagraph">We compile that to code in the following shape:
</p>
<pclass="inwebparagraph"></p>
<preclass="display">
<spanclass="plain">set count of domain size to 0</span>
<spanclass="plain">set count of valid cases to 0</span>
<spanclass="plain">loop header for v to run through its domain set {</span>
<spanclass="plain"> if psi holds {</span>
<spanclass="plain"> increment count of domain size</span>
<spanclass="plain"> if theta holds {</span>
<spanclass="plain"> increment count of valid cases</span>
<spanclass="plain"> }</span>
<spanclass="plain"> }</span>
<spanclass="plain">}</span>
<spanclass="plain">if the counts are such that the quantifier is satisfied {</span>
<spanclass="plain"> ...</span>
</pre>
<pclass="inwebparagraph">We don't always need both counts. For instance, to handle "at least three
doors are unlocked" we count both the domain size (the number of doors)
and the number of valid cases (the number of unlocked doors), but only need
the latter. This might be worth optimising some day, to save local variables.
</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_2_3_7"></a><b>§2.1.6.1.2.3.7. </b>The domain size and valid case counts are stored in locals called <codeclass="display"><spanclass="extract">qcn_N</span></code>
and <codeclass="display"><spanclass="extract">qcy_N</span></code> respectively, where <codeclass="display"><spanclass="extract">N</span></code> is the index of the quantifier — 0 for
the first one in the proposition, 1 for the second and so on.
</p>
<pclass="inwebparagraph">On reading a non-existence <codeclass="display"><spanclass="extract">QUANTIFIER</span></code> atom, we compile code to zero the
counts, and push details of the quantifier onto the Q-stack, so that we
can recover them later. We then compile a loop header exactly as above.
</p>
<pclass="inwebparagraph">The test of ψ, which acts as a filter on the domain set — e.g.,
only doors, not all objects — is handled by pushing a suitable goal onto
the R-stack, but we don't need to do anything to make that happen here,
because the <codeclass="display"><spanclass="extract">DOMAIN_OPEN</span></code> atom does it.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Push the Q-stack</span><spanclass="cwebmacronumber">2.1.6.1.2.3.7</span>> =
<<spanclass="cwebmacro">Handle "not exists" as "for all not"</span><spanclass="cwebmacronumber">2.1.6.1.2.3.7.1</span>><spanclass="plain">;</span>
<pclass="inwebparagraph">We zeroed the counters, compiled the loop headers and pushed details to the
Q-stack at the <codeclass="display"><spanclass="extract">QUANTIFIER</span></code> atom; pushed a filtering goal onto the R-stack
at the <codeclass="display"><spanclass="extract">DOMAIN_OPEN</span></code> atom; popped it again as accomplished at <codeclass="display"><spanclass="extract">DOMAIN_CLOSE</span></code>,
compiling a line which increments the domain size to celebrate; and then
compiled code to test θ.
</p>
<pclass="inwebparagraph">Now we are at the end of the line, and still have the quantifier code
half-done, as we know because the Q-stack is not empty. We first compile
an increment of the valid cases count, because if execution of the I6
code gets to the end of testing θ then it must have found a valid
case: in the "at least three doors are unlocked" example, it will have
found an unlocked one among the doors making up the domain. We then need
to record any "called" values for later retrieval by whoever called
this proposition routine: see below. That leaves just this part:
</p>
<pclass="inwebparagraph"></p>
<preclass="display">
<spanclass="plain"> }</span>
<spanclass="plain"> }</span>
<spanclass="plain">}</span>
<spanclass="plain">if the counts are such that the quantifier is satisfied {</span>
<spanclass="plain"> ...</span>
</pre>
<pclass="inwebparagraph">left to compile, and we will be done: execution will reach the <codeclass="display"><spanclass="extract">...</span></code> if and
only if it is true at run-time that three or more of the doors is unlocked.
</p>
<pclass="inwebparagraph">Thus this elaborate generalised-quantifier case satisfies the Invariant
because it transfers execution from before to <codeclass="display"><spanclass="extract">...</span></code> either 0 times (if the
counts don't satisfy us), or once. Unlike in the ∃ v case, it's
not a question of enumerating which v work and which do not; the whole
thing works, or doesn't, and is more like testing a single <codeclass="display"><spanclass="extract">if</span></code>.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Pop the Q-stack</span><spanclass="cwebmacronumber">2.1.6.1.2.4</span>> =
<<spanclass="cwebmacro">Close a block in the I6 code compiled to perform the search</span><spanclass="cwebmacronumber">2.1.6.1.2.6</span>><spanclass="plain">;</span>
<<spanclass="cwebmacro">Open a block in the I6 code compiled to perform the search, if variant</span><spanclass="cwebmacronumber">2.1.6.1.2.3.3.1</span>><spanclass="plain">;</span>
</pre>
<pclass="inwebparagraph"></p>
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1_2">§2.1.6.1.2</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_2_3_8"></a><b>§2.1.6.1.2.3.8. The C-stack. </b>When a CALLED atom in the proposition gives a name to a variable, we have to
transcribe that to the <codeclass="display"><spanclass="extract">deferred_calling_list</span></code> for the benefit of the code
calling this proposition routine. Each time we discover that a term t is
to be given a name, we stack it up. These are not always variables:
</p>
<blockquote>
<p>if a person (called the dupe) is in a dark room (called the lair), ...</p>
</blockquote>
<pclass="inwebparagraph">gives names to x ("dupe") and f_in(x) ("lair"), because
simplification has eliminated the variable y which appears to be being
given a name.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Push the C-stack</span><spanclass="cwebmacronumber">2.1.6.1.2.3.8</span>> =
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1_2_3">§2.1.6.1.2.3</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_2_5"></a><b>§2.1.6.1.2.5. </b>When does the compiled search code record values into <codeclass="display"><spanclass="extract">deferred_calling_list</span></code>?
In two situations:
</p>
<pclass="inwebparagraph"></p>
<ulclass="items"><li>(a) when a domain-search has successfully found a viable case for a quantifier,
the values of any variables called in that domain are recorded;
</li><li>(b) and otherwise the values of called variables are recorded just before
point <codeclass="display"><spanclass="extract">M</span></code>, that is, immediately before acting on a successful match.
</li></ul>
<pclass="inwebparagraph">For example, when reading:
</p>
<blockquote>
<p>if a person (called the dupe) is in a lighted room which is adjacent to exactly one dark room (called the lair), ...</p>
</blockquote>
<pclass="inwebparagraph">the value of "dupe" is transferred just before <codeclass="display"><spanclass="extract">M</span></code>, but the value of "lair"
is transferred as soon as a dark room is found. The code looks like this:
</p>
<pclass="inwebparagraph"></p>
<preclass="display">
<spanclass="plain">set count of domain size to 1</span>
<spanclass="plain">loop through domain (i.e., dark rooms adjacent to the person's location) {</span>
<spanclass="plain"> increment count of domain size</span>
<spanclass="plain"> record the lair value</span>
<spanclass="plain">}</span>
<spanclass="plain">if the count of domain size is 1 {</span>
<spanclass="plain"> record the dupe value</span>
<spanclass="plain"> M</span>
<spanclass="plain">}</span>
</pre>
<pclass="inwebparagraph">If we waited until point <codeclass="display"><spanclass="extract">M</span></code> to record the lair value, it would have disappeared,
because <codeclass="display"><spanclass="extract">M</span></code> is outside the loop which searches the domain of the "exactly one"
quantifier.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Pop the C-stack</span><spanclass="cwebmacronumber">2.1.6.1.2.5</span>> =
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1_2">§2.1.6.1.2</a>, <ahref="#SP2_1_6_1_2_4">§2.1.6.1.2.4</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_2_3_5_1"></a><b>§2.1.6.1.2.3.5.1. </b>That just leaves the blocking, which follows the One True Brace Style. Thus:
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Open a block in the I6 code compiled to perform the search</span><spanclass="cwebmacronumber">2.1.6.1.2.3.5.1</span>> =
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1_2_3_5">§2.1.6.1.2.3.5</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_2_3_3_1"></a><b>§2.1.6.1.2.3.3.1. </b>Not for a loop body:
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Open a block in the I6 code compiled to perform the search, if variant</span><spanclass="cwebmacronumber">2.1.6.1.2.3.3.1</span>> =
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1_2">§2.1.6.1.2</a>, <ahref="#SP2_1_6_1_2_4">§2.1.6.1.2.4</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_5_1"></a><b>§2.1.5.1. Adaptations. </b>That completes the general pattern of searching according to the proposition's
instructions. It remains to adapt it to different needs, by providing, in
each case, some setting-up code; some code to execute when a viable set
of variable values is found; and some winding-up code.
</p>
<pclass="inwebparagraph">In some of the cases, additional local variables are needed within the
<codeclass="display"><spanclass="extract">Prop_N</span></code> routine, to keep track of counters or totals. These are they:
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Declare the I6 locals needed by adaptations to particular deferral cases</span><spanclass="cwebmacronumber">2.1.5.1</span>> =
<<spanclass="cwebmacrodefn">Declare the I6 call parameters needed by adaptations to particular deferral cases</span><spanclass="cwebmacronumber">2.1.5.2</span>> =
<pclass="endnote">This code is used in <ahref="#SP2_1_5">§2.1.5</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_3"></a><b>§2.1.6.1.3. Adaptation to CONDITION. </b>The first and simplest of our cases to understand: where φ is a sentence,
with all variables bound, and we have to return <codeclass="display"><spanclass="extract">true</span></code> if it is true and
<codeclass="display"><spanclass="extract">false</span></code> if it is false. There is no initialisation:
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Initialisation before CONDITION search</span><spanclass="cwebmacronumber">2.1.6.1.3</span>> =
</code></p>
<preclass="displaydefn">
<spanclass="plain">;</span>
</pre>
<pclass="inwebparagraph"></p>
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1">§2.1.6.1</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_2_2_1"></a><b>§2.1.6.1.2.2.1. </b>As soon as we find any valid combination of the variables, we return <codeclass="display"><spanclass="extract">true</span></code>:
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Act on successful match in CONDITION search</span><spanclass="cwebmacronumber">2.1.6.1.2.2.1</span>> =
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1_2_2">§2.1.6.1.2.2</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_4"></a><b>§2.1.6.1.4. </b>So we only reach winding-up if every case failed, and then we return <codeclass="display"><spanclass="extract">false</span></code>:
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Winding-up after CONDITION search</span><spanclass="cwebmacronumber">2.1.6.1.4</span>> =
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1">§2.1.6.1</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_5"></a><b>§2.1.6.1.5. Adaptation to NUMBER. </b>In the remaining cases, φ has variable x (only) left free, but the use
we want to make will be a loop over all objects x, and we compile this
"outer loop" here: the loop opens in the initialisation code, closes in
the winding-up code, and therefore completely encloses the code generated
by the searching mechanism above.
</p>
<pclass="inwebparagraph">In the first case, we want to count the number of x for which φ(x)
is true. The local <codeclass="display"><spanclass="extract">counter</span></code> holds the count so far; it starts out automatically
at 0, since all I6 locals do.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Initialisation before NUMBER search</span><spanclass="cwebmacronumber">2.1.6.1.5</span>> =
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1">§2.1.6.1</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_2_2_2"></a><b>§2.1.6.1.2.2.2. </b>Recall that we get here for each possible way that φ(x) could
be true, that is, once for each viable set of values of bound variables in
φ. But we only want to increment <codeclass="display"><spanclass="extract">counter</span></code> once, so having done so, we
exit the searching code and continue the outer loop.
</p>
<pclass="inwebparagraph">The <codeclass="display"><spanclass="extract">jump</span></code> to a label is forced on us since I6, unlike, say, Perl, has no
syntax to break or continue a loop other than the innermost one.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Act on successful match in NUMBER search</span><spanclass="cwebmacronumber">2.1.6.1.2.2.2</span>> =
<<spanclass="cwebmacro">Jump to next outer loop for this reason</span><spanclass="cwebmacronumber">2.1.6.1.2.2.2.1</span>><spanclass="plain">;</span>
</pre>
<pclass="inwebparagraph"></p>
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1_2_2">§2.1.6.1.2.2</a>.</p>
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1_2_2_2">§2.1.6.1.2.2.2</a>, <ahref="#SP2_1_6_1_2_2_3">§2.1.6.1.2.2.3</a>, <ahref="#SP2_1_6_1_2_2_4">§2.1.6.1.2.2.4</a>, <ahref="#SP2_1_6_1_2_2_5">§2.1.6.1.2.2.5</a>, <ahref="#SP2_1_6_1_17">§2.1.6.1.17</a> (twice).</p>
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1">§2.1.6.1</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_8"></a><b>§2.1.6.1.8. Adaptation to LIST. </b>In the next case, we want to form the list of all x for which φ(x)
is true. The local <codeclass="display"><spanclass="extract">list</span></code> holds the list so far, and already exists.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Initialisation before LIST search</span><spanclass="cwebmacronumber">2.1.6.1.8</span>> =
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1">§2.1.6.1</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_2_2_3"></a><b>§2.1.6.1.2.2.3. </b>Recall that we get here for each possible way that φ(x) could
be true, that is, once for each viable set of values of bound variables in
φ. But we only want to increment <codeclass="display"><spanclass="extract">counter</span></code> once, so having done so, we
exit the searching code and continue the outer loop.
</p>
<pclass="inwebparagraph">The <codeclass="display"><spanclass="extract">jump</span></code> to a label is forced on us since I6, unlike, say, Perl, has no
syntax to break or continue a loop other than the innermost one.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Act on successful match in LIST search</span><spanclass="cwebmacronumber">2.1.6.1.2.2.3</span>> =
<<spanclass="cwebmacro">Jump to next outer loop for this reason</span><spanclass="cwebmacronumber">2.1.6.1.2.2.2.1</span>><spanclass="plain">;</span>
</pre>
<pclass="inwebparagraph"></p>
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1_2_2">§2.1.6.1.2.2</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_9"></a><b>§2.1.6.1.9. </b>The continue-outer-loop labels are marked with the reason number so that
if code is compiled for each reason in turn within a single routine — which
is what we do for multipurpose deferred propositions — the labels do
not have clashing names.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Winding-up after LIST search</span><spanclass="cwebmacronumber">2.1.6.1.9</span>> =
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1">§2.1.6.1</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_10"></a><b>§2.1.6.1.10. Adaptation to RANDOM. </b>To choose a random x such that φ(x), we essentially run the same code
as for NUMBER searches, but twice over: first to count how many such x there
are, then to run through again to find the nth of these, where n is a
uniformly random number such that 1<= n<= x.
</p>
<pclass="inwebparagraph">This avoids needing to store the full list of matches anywhere, which would
be impossible since (a) it's potentially a lot of storage and (b) it can
only safely live on the current stack frame, and I6 does not allow arrays
on the current stack frame (because of restrictions in the Z-machine).
This means that, on average, the compiled code takes 50\% longer to find
its random x than it ideally would, but we accept the trade-off.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Initialisation before RANDOM search</span><spanclass="cwebmacronumber">2.1.6.1.10</span>> =
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1">§2.1.6.1</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_2_2_4"></a><b>§2.1.6.1.2.2.4. </b>Again we exit the searcher as soon as a match is found, since that guarantees
that φ(x).
</p>
<pclass="inwebparagraph">Note that we can only return here on the second pass, since <codeclass="display"><spanclass="extract">selection</span></code> is -1
throughout the first pass, whereas <codeclass="display"><spanclass="extract">counter</span></code> is non-negative.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Act on successful match in RANDOM search</span><spanclass="cwebmacronumber">2.1.6.1.2.2.4</span>> =
<<spanclass="cwebmacro">Jump to next outer loop for this reason</span><spanclass="cwebmacronumber">2.1.6.1.2.2.2.1</span>><spanclass="plain">;</span>
</pre>
<pclass="inwebparagraph"></p>
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1_2_2">§2.1.6.1.2.2</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_11"></a><b>§2.1.6.1.11. </b>We return <codeclass="display"><spanclass="extract">nothing</span></code>— the non-object — if <codeclass="display"><spanclass="extract">counter</span></code> is zero, since that
means the set of possible x is empty. But we also return if <codeclass="display"><spanclass="extract">selection</span></code>
has been made already, because that means that the second pass has been
completed without a return — something which in theory cannot happen, but
just might do if testing part of the proposition had some side-effect changing
the state of the objects and thus the size of the set of possibilities.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Winding-up after RANDOM search</span><spanclass="cwebmacronumber">2.1.6.1.11</span>> =
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1">§2.1.6.1</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_12"></a><b>§2.1.6.1.12. Adaptation to TOTAL. </b>Here the task is to sum the values of property P attached to each object
in the domain { x| φ(x)}.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Initialisation before TOTAL search</span><spanclass="cwebmacronumber">2.1.6.1.12</span>> =
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1">§2.1.6.1</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_2_2_5"></a><b>§2.1.6.1.2.2.5. </b>The only wrinkle here is the way the compiled code knows which property it
should be totalling. If we know that ourselves, we can compile in a direct
reference. But if we are compiling a multipurpose deferred proposition, then
it might be used to total any property over the domain, and we won't know
which until runtime — when its identity will be found in the I6 variable
<<spanclass="cwebmacro">Jump to next outer loop for this reason</span><spanclass="cwebmacronumber">2.1.6.1.2.2.2.1</span>><spanclass="plain">;</span>
</pre>
<pclass="inwebparagraph"></p>
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1_2_2">§2.1.6.1.2.2</a>.</p>
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1">§2.1.6.1</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_14"></a><b>§2.1.6.1.14. Adaptation to EXTREMAL. </b>This is rather similar. We find the member of { x| φ(x)}
which either minimises, or maximises, the value of some property P. We use
two local variables: <codeclass="display"><spanclass="extract">best</span></code>, the extreme P value found so far; and <codeclass="display"><spanclass="extract">best_with</span></code>,
the member of the domain set which achieves that.
</p>
<pclass="inwebparagraph">If two or more x achieve the optimal P-value, it is deliberately left
undefined which one is returned. The user may be typing "the heaviest thing
on the table", but what he gets is "a heaviest thing on the table".
</p>
<pclass="inwebparagraph">We open the search with <codeclass="display"><spanclass="extract">best_with</span></code> equal to <codeclass="display"><spanclass="extract">nothing</span></code>, the non-object, which
is what we will return if the domain set turns out to be empty; and with
<codeclass="display"><spanclass="extract">best</span></code> set to the furthest-from-optimal value possible. For a search maximising
P, <codeclass="display"><spanclass="extract">best</span></code> starts at the lowest number representable in the virtual machine;
for a minimisation, it starts at the highest. That way, if any member of the
domain is found, its P-value must be at least as good as the starting
value of <codeclass="display"><spanclass="extract">best</span></code>.
</p>
<pclass="inwebparagraph">Again the only nuisance is that sometimes we know P, and whether we are
maximising or minimising, at compile time; but for a multipurpose routine
we don't, and have to look that up at run-time.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Initialisation before EXTREMAL search</span><spanclass="cwebmacronumber">2.1.6.1.14</span>> =
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1">§2.1.6.1</a>.</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_16"></a><b>§2.1.6.1.16. Adaptation to LOOP. </b>Here the proposition is used to iterate through the members of the domain
set { x| φ(x)}. Two local variables exist: <codeclass="display"><spanclass="extract">x</span></code> and <codeclass="display"><spanclass="extract">x_ix</span></code>.
One of the following is true:
</p>
<pclass="inwebparagraph"></p>
<ulclass="items"><li>(1) The domain set contains only objects, so that <codeclass="display"><spanclass="extract">x</span></code> is non-zero if it
represents a member of that set. In this case <codeclass="display"><spanclass="extract">x_ix</span></code> may or may not be used,
and we will not rely on it.
</li><li>(2) The domain set contains only values, and then <codeclass="display"><spanclass="extract">x</span></code> might easily be zero,
but <codeclass="display"><spanclass="extract">x_ix</span></code> is always the index within the domain set: 1 if <codeclass="display"><spanclass="extract">x</span></code> is the first
value, 2 for the second and so on.
</li></ul>
<pclass="inwebparagraph">The proposition is called with a pair of values <codeclass="display"><spanclass="extract">x</span></code>, <codeclass="display"><spanclass="extract">x_ix</span></code> and returns
the next value <codeclass="display"><spanclass="extract">x</span></code> in the domain set, or 0 if the domain is exhausted. (In
case (2) it's not safe to regard 0 as an end-of-set sentinel value because
0 can be a valid member of the set; so in looping through (2) we should
first find the size of the set using NUMBER OF, then keep calling for
members until the index reaches the size.) There is no need to return the
next <codeclass="display"><spanclass="extract">x_ix</span></code> value since it is always the present value plus 1.
</p>
<pclass="inwebparagraph">If the proposition is called with <codeclass="display"><spanclass="extract">x</span></code> set to <codeclass="display"><spanclass="extract">nothing</span></code>, in case (1), or
with <codeclass="display"><spanclass="extract">x_ix</span></code> equal to 0, in case (2), it returns the first value in the
domain.
</p>
<pclass="inwebparagraph"><aid="SP2_1_6_1_17"></a><b>§2.1.6.1.17. </b>Snarkily, this is how we do it:
</p>
<pclass="inwebparagraph"></p>
<preclass="display">
<spanclass="plain">if we're called with a valid member of the domain, go to Z</span>
<spanclass="plain">loop x over members of the domain {</span>
<spanclass="plain"> return x</span>
<spanclass="plain"> label Z is here</span>
<spanclass="plain">}</span>
</pre>
<pclass="inwebparagraph">Which is not really a loop at all, but is a cheap way to extract either the
initial value or the successor value from a loop header. (The trick actually
caused some consternation for I6 hackers when early drafts of I7 came out,
because they had been experimenting with a patch to I6 which protected
<codeclass="display"><spanclass="extract">objectloop</span></code> from object-tree rearrangements but which assumed that nobody
ever used <codeclass="display"><spanclass="extract">jump</span></code> to enter a loop body bypassing its header. But the DM4,
which defines I6, doesn't forbid this. The designer of I6 has learned his
lesson, though: I7 has no goto or jump instruction, and I7 loops can be
proved to be entered and exited cleanly.)
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Initialisation before LOOP search</span><spanclass="cwebmacronumber">2.1.6.1.17</span>> =
<<spanclass="cwebmacro">Jump to next outer loop for this reason</span><spanclass="cwebmacronumber">2.1.6.1.2.2.2.1</span>><spanclass="plain">;</span>
<<spanclass="cwebmacro">Jump to next outer loop for this reason</span><spanclass="cwebmacronumber">2.1.6.1.2.2.2.1</span>><spanclass="plain">;</span>
<pclass="endnote">This code is used in <ahref="#SP2_1_6_1">§2.1.6.1</a>.</p>
<pclass="inwebparagraph"><aid="SP3"></a><b>§3. Compiling loop headers. </b>The final task of this entire chapter is to compile an I6 loop header which
causes a given variable v to range through a domain set D — which we
have to deduce by looking at the proposition ψ in front of us.
</p>
<pclass="inwebparagraph">We want this loop to run as quickly as possible: efficiency here makes
a very big difference to the running time of compiled I7 code. Most
optimisations aren't worth the risk in added complexity — but these are.
</p>
<pclass="inwebparagraph">Loops through kinds of value are not in general optimisable. The problem cases
involve loops through objects. Consider:
</p>
<blockquote>
<p>if everyone in the Dining Room can see an animal, ...</p>
</blockquote>
<pclass="inwebparagraph">Code like this will run very slowly:
</p>
<pclass="inwebparagraph"></p>
<preclass="display">
<spanclass="plain">loop over objects (x)</span>
<spanclass="plain"> loop over objects (y)</span>
<spanclass="plain"> if x is a person</span>
<spanclass="plain"> if x is in the Dining Room</span>
<spanclass="plain"> if y is an animal</span>
<spanclass="plain"> if x can see y</span>
<spanclass="plain"> success!</span>
</pre>
<pclass="inwebparagraph">This is folly in so many ways. Most objects aren't people or animals, so
almost all combinations of x and y are wasted. We test the eligibility
of x for every possible y. And there are quick ways to find what is in
the Dining Room, so we're missing a trick there, too. What we want is:
</p>
<pclass="inwebparagraph"></p>
<preclass="display">
<spanclass="plain">loop over objects in the Dining Room (x)</span>
<spanclass="plain"> if x is a person</span>
<spanclass="plain"> loop over animals (y)</span>
<spanclass="plain"> if x can see y</span>
<spanclass="plain"> success!</span>
</pre>
<pclass="inwebparagraph"></p>
<pclass="inwebparagraph"><aid="SP4"></a><b>§4. </b>Part of the work is done already: we generate propositions with
quantifiers as far forwards as they can be, so we won't loop over y before
checking the validity of x. The rest of the work comes from two basic
optimisations:
</p>
<pclass="inwebparagraph"></p>
<ulclass="items"><li>(1) if a loop over v is such that K(v) holds in every case, where K
is a kind, then loop v over K rather than all objects, and
</li><li>(2) if a loop over v is such that R(v, t) holds in every case, then loop over
all v such that R(v, t) in cases where R has a run-time representation
making this quick and easy.
</li></ul>
<pclass="inwebparagraph">In each case we can then delete K(v) or R(v, t) from the proposition
as redundant, since the loop header has taken care of it.
</p>
<pclass="inwebparagraph">Case (1) is called "kind optimisation"; case (2), "parent
optimisation", because the prototype case is R being containment — we
exploit that the object-tree parent of v is known, and that I6 has a fast
form of <codeclass="display"><spanclass="extract">objectloop</span></code> to visit the children of a given node in the object
tree. Case (2) has to be avoided if we are compiling code to force a
proposition, rather than test it, because then R(v, t) is not an
accomplished fact but is something we have yet to make come true. This is
why the loop-compiler takes a flag <codeclass="display"><spanclass="extract">avoid_parent_optimisation</span></code>. Case (1)
doesn't suffer from this since kinds cannot be changed at run-time.
</p>
<pclass="inwebparagraph"><aid="SP5"></a><b>§5. </b>So here is the code. We write an I6 schema for the loop into <codeclass="display"><spanclass="extract">loop_schema</span></code>,
<<spanclass="cwebmacro">Scan the proposition to find the domain of the loop, and look for opportunities</span><spanclass="cwebmacronumber">5.1</span>><spanclass="plain">;</span>
<spanclass="reserved">if</span><spanclass="plain"> ((</span><spanclass="identifier">K</span><spanclass="plain">) && (</span><spanclass="identifier">parent_optimised</span><spanclass="plain"> == </span><spanclass="identifier">FALSE</span><spanclass="plain">)) { </span><spanclass="comment">parent optimisation is stronger, so we prefer that</span>
<pclass="endnote">The function Calculus::Propositions::Deferred::compile_loop_header is used in <ahref="#SP2_1_6_1_2_3_5">§2.1.6.1.2.3.5</a>, <ahref="#SP2_1_6_1_5">§2.1.6.1.5</a>, <ahref="#SP2_1_6_1_8">§2.1.6.1.8</a>, <ahref="#SP2_1_6_1_10">§2.1.6.1.10</a>, <ahref="#SP2_1_6_1_12">§2.1.6.1.12</a>, <ahref="#SP2_1_6_1_14">§2.1.6.1.14</a>, <ahref="#SP2_1_6_1_17">§2.1.6.1.17</a>.</p>
<pclass="inwebparagraph"><aid="SP5_1"></a><b>§5.1. </b>The following looks more complicated than it really is. Sometimes it's
called to compile a loop arising from a quantifier with a domain, in
which case <codeclass="display"><spanclass="extract">grouped</span></code> is set and <codeclass="display"><spanclass="extract">proposition</span></code> points to:
<pclass="inwebparagraph">so that ψ, the part in the domain group, defines the range of the
variable. But sometimes the call is to compile a loop not arising from a
quantifier, so there is no domain group to scan; instead the whole
proposition makes up ψ, and now <codeclass="display"><spanclass="extract">grouped</span></code> is clear.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Scan the proposition to find the domain of the loop, and look for opportunities</span><spanclass="cwebmacronumber">5.1</span>> =
<<spanclass="cwebmacro">Scan $\psi$, the part of the proposition establishing the domain</span><spanclass="cwebmacronumber">5.1.1</span>><spanclass="plain">;</span>
<spanclass="plain">}</span>
</pre>
<pclass="inwebparagraph"></p>
<pclass="endnote">This code is used in <ahref="#SP5">§5</a>.</p>
<pclass="inwebparagraph"><aid="SP5_1_1"></a><b>§5.1.1. </b>In either case, we scan ψ looking for K(v) atoms, which would tell
us the domain set for the variable v, or for R(v, t) atoms for
parent-optimisable relations R.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Scan $\psi$, the part of the proposition establishing the domain</span><spanclass="cwebmacronumber">5.1.1</span>> =
<<spanclass="cwebmacro">Consider parent optimisation on this binary predicate</span><spanclass="cwebmacronumber">5.1.1.1</span>><spanclass="plain">;</span>
</pre>
<pclass="inwebparagraph"></p>
<pclass="endnote">This code is used in <ahref="#SP5_1">§5.1</a>.</p>
<pclass="inwebparagraph"><aid="SP5_1_1_1"></a><b>§5.1.1.1. </b>We give the relation R an opportunity to write a loop which runs v
through all possible x such that R(x, t), by writing a schema for the
loop in which <codeclass="display"><spanclass="extract">*1</span></code> denotes the variable v and <codeclass="display"><spanclass="extract">*2</span></code> the term t.
</p>
<pclass="inwebparagraph">For example, the worn-by relation writes the schema:
</p>
<pclass="inwebparagraph"></p>
<preclass="display">
<spanclass="plain">objectloop (*1 in *2) if (WearerOf(*1)==parent(*1))</span>
</pre>
<pclass="inwebparagraph">where v runs quickly through the object-tree children of t, but items
carried rather than worn are skipped.
</p>
<pclass="inwebparagraph">We have to check three possible cases: R(v, t) direct, and then
is(f_R(v), t) or is(t, f_R(v)), which can arise from
simplifications. We set <codeclass="display"><spanclass="extract">optimise_on</span></code> to R and <codeclass="display"><spanclass="extract">parent</span></code> to t.
</p>
<pclass="macrodefinition"><codeclass="display">
<<spanclass="cwebmacrodefn">Consider parent optimisation on this binary predicate</span><spanclass="cwebmacronumber">5.1.1.1</span>> =
<pclass="endnote">This code is used in <ahref="#SP5_1_1">§5.1.1</a>.</p>
<pclass="inwebparagraph"><aid="SP6"></a><b>§6. </b>And that concludes the predicate-calculus engine at the heart of Inform.
</p>
<hrclass="tocbar">
<ulclass="toc"><li><ahref="12-cad.html">Back to 'Cinders and Deferrals'</a></li><li><i>(This section ends Chapter 12: Use of Propositions.)</i></li></ul><hrclass="tocbar">