ifhub/inform7
1
0
Fork 0
mirror of https://github.com/ganelson/inform.git synced 2024-07-08 18:14:21 +03:00
Code Issues Projects Releases Wiki Activity
inform7/docs/core-module/11-sm.html
Graham Nelson fd4a46ddd8 Modernised use of extracts
2020-04-07 01:06:09 +01:00

1575 lines
192 KiB
HTML
Raw Blame History

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<title>11/sc</title>
<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="../inweb.css" rel="stylesheet" rev="stylesheet" type="text/css">
</head>
<body>
<nav role="navigation">
<h1><a href="../webs.html">Sources</a></h1>
<ul>
<li><a href="../compiler.html"><b>compiler tools</b></a></li>
<li><a href="../other.html">other tools</a></li>
<li><a href="../extensions.html">extensions and kits</a></li>
<li><a href="../units.html">unit test tools</a></li>
</ul>
<h2>Compiler Webs</h2>
<ul>
<li><a href="../inbuild/index.html">inbuild</a></li>
<li><a href="../inform7/index.html">inform7</a></li>
<li><a href="../inter/index.html">inter</a></li>
</ul>
<h2>Inbuild Modules</h2>
<ul>
<li><a href="../inbuild-module/index.html">inbuild</a></li>
<li><a href="../arch-module/index.html">arch</a></li>
<li><a href="../words-module/index.html">words</a></li>
<li><a href="../syntax-module/index.html">syntax</a></li>
<li><a href="../html-module/index.html">html</a></li>
</ul>
<h2>Inform7 Modules</h2>
<ul>
<li><a href="../core-module/index.html">core</a></li>
<li><a href="../problems-module/index.html">problems</a></li>
<li><a href="../inflections-module/index.html">inflections</a></li>
<li><a href="../linguistics-module/index.html">linguistics</a></li>
<li><a href="../kinds-module/index.html">kinds</a></li>
<li><a href="../if-module/index.html">if</a></li>
<li><a href="../multimedia-module/index.html">multimedia</a></li>
<li><a href="../index-module/index.html">index</a></li>
</ul>
<h2>Inter Modules</h2>
<ul>
<li><a href="../inter-module/index.html">inter</a></li>
<li><a href="../building-module/index.html">building</a></li>
<li><a href="../codegen-module/index.html">codegen</a></li>
</ul>
<h2>Foundation</h2>
<ul>
<li><a href="../../../inweb/docs/foundation-module/index.html">foundation</a></li>
</ul>
</nav>
<main role="main">
<!--Weave of '11/sm' generated by 7-->
<ul class="crumbs"><li><a href="../webs.html">Source</a></li><li><a href="../compiler.html">Compiler Modules</a></li><li><a href="index.html">core</a></li><li><a href="index.html#11">Chapter 11: Predicate Calculus</a></li><li><b>Simplifications</b></li></ul><p class="purpose">A set of operations each of which takes a proposition and either leaves it unchanged or replaces it with a simpler one logically equivalent to the original.</p>
<ul class="toc"><li><a href="#SP1">&#167;1. Definitions</a></li><li><a href="#SP3">&#167;3. Simplify the nothing constant (fudge)</a></li><li><a href="#SP4">&#167;4. Use listed-in predicates (deduction)</a></li><li><a href="#SP5">&#167;5. Simplify negated determiners (deduction)</a></li><li><a href="#SP7">&#167;7. Simplify negated satisfiability (deduction)</a></li><li><a href="#SP8">&#167;8. Make kind requirements explicit (deduction)</a></li><li><a href="#SP9">&#167;9. Remove redundant kind predicates (deduction)</a></li><li><a href="#SP11">&#167;11. Turn binary predicates the right way round (deduction)</a></li><li><a href="#SP12">&#167;12. Simplify region containment (fudge)</a></li><li><a href="#SP13">&#167;13. Reduce binary predicates (deduction)</a></li><li><a href="#SP14">&#167;14. Eliminating determined variables (deduction)</a></li><li><a href="#SP15">&#167;15. Simplify non-relation (deduction)</a></li><li><a href="#SP16">&#167;16. Convert gerunds to nouns (deduction)</a></li><li><a href="#SP17">&#167;17. Eliminate to have meaning property ownership (fudge)</a></li><li><a href="#SP19">&#167;19. Turn all rooms to everywhere (fudge)</a></li></ul><hr class="tocbar">
<p class="inwebparagraph"><a id="SP1"></a><b>&#167;1. Definitions. </b></p>
<p class="inwebparagraph"><a id="SP2"></a><b>&#167;2. </b>Recall the three rules for simplification routines: they take a proposition
Σ (which they are allowed to destroy or modify) and return Σ',
but such that:
</p>
<p class="inwebparagraph"></p>
<ul class="items"><li>(i) Σ' remains a syntactically correct proposition with well-formed
quantifiers,
</li><li>(ii) Σ' has the same number of free variables as Σ, and
</li><li>(iii) in all situations and for all possible values of any free variables,
Σ' is true if and only if Σ is.
</li></ul>
<p class="inwebparagraph">Rules (i) and (ii) are always strictly obeyed. A simplification which obeys (iii)
in its purely logical sense is called a "deduction"; one which bends (iii)
to change the proposition from what the user wrote, to what he meant to write,
is called a "fudge". Fudges are needed because English is quirky, and does
not correspond perfectly to predicate logic.
</p>
<p class="inwebparagraph">What we mean by simpler is not shorter, or with less exotic contents: often
the simplified form of a proposition is longer and uses relations or
determiners less obviously derived from the original text. Instead, simpler
means simpler to test and assert. Our ideal is a conjunction of a sequence
of predicates, using the smallest possible number of variables (and hence
quantifiers).
</p>
<p class="inwebparagraph"><a id="SP3"></a><b>&#167;3. Simplify the nothing constant (fudge). </b>The word "nothing" is sometimes a noun ("the holder of the oak tree is
nothing"), sometimes a determiner ("nothing is in the box"). This
doesn't arise with the other no- words, nowhere and nobody, since those are
not allowed as nouns in Inform.
</p>
<p class="inwebparagraph">Here we look for the noun form as one term in a binary predicate, and convert
it to the determiner form unless the predicate is equality. Thus "X is nothing"
is allowed to use the noun form, "X contains nothing" has to use the
determiner form. (In particular "nothing is nothing" compares two identical
nouns and is always true. I thought this was a sentence nobody would write,
but Google finds 223,000 hits for it.)
</p>
<pre class="display">
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="functiontext">Calculus::Simplifications::nothing_constant</span><span class="plain">(</span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">prop</span><span class="plain">, </span><span class="reserved">int</span><span class="plain"> *</span><span class="identifier">changed</span><span class="plain">) {</span>
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
<span class="plain">*</span><span class="identifier">changed</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">)</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="functiontext">Calculus::Atoms::is_binary_predicate</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">)) &amp;&amp; (</span><span class="functiontext">Calculus::Atoms::is_equality_predicate</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">) == </span><span class="identifier">FALSE</span><span class="plain">)) {</span>
<span class="reserved">binary_predicate</span><span class="plain"> *</span><span class="identifier">bp</span><span class="plain"> = </span><span class="identifier">RETRIEVE_POINTER_binary_predicate</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">predicate</span><span class="plain">);</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">i</span><span class="plain">;</span>
<span class="reserved">for</span><span class="plain"> (</span><span class="identifier">i</span><span class="plain">=0; </span><span class="identifier">i</span><span class="plain">&lt;2; </span><span class="identifier">i</span><span class="plain">++) {</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Rvalues::is_nothing_object_constant</span><span class="plain">(</span><span class="functiontext">Calculus::Terms::constant_underlying</span><span class="plain">(&amp;(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[</span><span class="identifier">i</span><span class="plain">])))) {</span>
&lt;<span class="cwebmacro">Substitute for the term and quantify with does-not-exist</span> <span class="cwebmacronumber">3.2</span>&gt;<span class="plain">;</span>
<span class="identifier">PROPOSITION_EDITED</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">);</span>
<span class="reserved">break</span><span class="plain">;</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="reserved">return</span><span class="plain"> </span><span class="identifier">prop</span><span class="plain">;</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">The function Calculus::Simplifications::nothing_constant is used in 11/sc (<a href="11-sc.html#SP1_14">&#167;1.14</a>, <a href="11-sc.html#SP2">&#167;2</a>).</p>
<p class="inwebparagraph"><a id="SP3_1"></a><b>&#167;3.1. </b>Formally, if B is a predicate other than equality,
Σ = ... B(t, f_X(f_Y(...(<code class="display"><span class="extract">nothing</span></code>))))... --&gt;
Σ' = ... ∄ v∈{ v| K_1(v)}: B(t, f_X(f_Y(...(v))))...
where v is unused in Σ, and &mdash; note the difference in placing &mdash;
Σ = ... B(f_X(f_Y(...(<code class="display"><span class="extract">nothing</span></code>))), t)... --&gt;
Σ' = ∄ v∈{ v| K_2(v)}: ... B(f_X(f_Y(...(v))), t)...
where K_1 and K_2 are the kinds of terms 1 and 2 in the predicate B.
</p>
<p class="inwebparagraph">The difference in where we place the quantifier is important in double-negative
sentences. Consider these:
</p>
<blockquote>
<p>[1] the box does not contain nothing</p>
</blockquote>
<p class="inwebparagraph">which produces Σ = ¬(contains(<code class="display"><span class="extract">box</span></code>, <code class="display"><span class="extract">nothing</span></code>)). Here,
<code class="display"><span class="extract">nothing</span></code> is part of the object phrase, not the subject phrase, and we need
to quantify it within the OP &mdash; which means, within the negation, because our
recipe for negated sentences was (roughly) SP ∧¬( OP ∧ VP).
We thus make Σ' = ¬(∄ x:contains(<code class="display"><span class="extract">box</span></code>, x)),
although later simplification converts that to ∃ x: contains(<code class="display"><span class="extract">box</span></code>, x),
just as if the original sentence had been "the box contains something".
On the other hand,
</p>
<blockquote>
<p>[2] nothing does not annoy Peter</p>
</blockquote>
<p class="inwebparagraph">produces Σ = ¬(annoys(<code class="display"><span class="extract">nothing</span></code>, <code class="display"><span class="extract">Peter</span></code>)), and now we have
to quantify as Σ' = ∄ x: ¬(annoys(x, <code class="display"><span class="extract">Peter</span></code>)).
</p>
<p class="inwebparagraph">Double-negatives are a little odd. If natural language were really the same as
predicate logic with some grunting sounds for decoration, then a double negative
would always be a positive. But in 18th-century English, that wasn't true: it
was a way of emphasising the negation, just as characters in Aaron Sorkin's
"The West Wing" scripts are always saying "not for nothing, but..." when
their meaning is equivalent to "this is nothing, but...". Still, Inform takes
the view that a double negative is a positive.
</p>
<p class="inwebparagraph"><a id="SP3_2"></a><b>&#167;3.2. </b>The code is simpler than the explanation:
</p>
<p class="macrodefinition"><code class="display">
&lt;<span class="cwebmacrodefn">Substitute for the term and quantify with does-not-exist</span> <span class="cwebmacronumber">3.2</span>&gt; =
</code></p>
<pre class="displaydefn">
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">nv</span><span class="plain"> = </span><span class="functiontext">Calculus::Variables::find_unused</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">);</span>
<span class="reserved">pcalc_term</span><span class="plain"> </span><span class="identifier">new_var</span><span class="plain"> = </span><span class="functiontext">Calculus::Terms::new_variable</span><span class="plain">(</span><span class="identifier">nv</span><span class="plain">);</span>
<span class="functiontext">Calculus::Variables::substitute_nothing_in_term</span><span class="plain">(&amp;(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[</span><span class="identifier">i</span><span class="plain">]), &amp;</span><span class="identifier">new_var</span><span class="plain">);</span>
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">position</span><span class="plain"> = </span><span class="identifier">NULL</span><span class="plain">; </span><span class="comment">at the front if <code class="display"><span class="extract">nothing</span></code> is the SP...</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">i</span><span class="plain"> == </span><span class="constant">1</span><span class="plain">) </span><span class="identifier">position</span><span class="plain"> = </span><span class="identifier">pl_prev</span><span class="plain">; </span><span class="comment">...but up close to the predicate if it's the OP</span>
<span class="comment">insert four atoms, in reverse order, at this position:</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::insert_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">position</span><span class="plain">, </span><span class="functiontext">Calculus::Atoms::new</span><span class="plain">(</span><span class="constant">DOMAIN_CLOSE_ATOM</span><span class="plain">));</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">BinaryPredicates::term_kind</span><span class="plain">(</span><span class="identifier">bp</span><span class="plain">, </span><span class="identifier">i</span><span class="plain">))</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::insert_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">position</span><span class="plain">,</span>
<span class="functiontext">Calculus::Atoms::KIND_new</span><span class="plain">(</span><span class="functiontext">BinaryPredicates::term_kind</span><span class="plain">(</span><span class="identifier">bp</span><span class="plain">, </span><span class="identifier">i</span><span class="plain">), </span><span class="identifier">new_var</span><span class="plain">));</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::insert_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">position</span><span class="plain">, </span><span class="functiontext">Calculus::Atoms::new</span><span class="plain">(</span><span class="constant">DOMAIN_OPEN_ATOM</span><span class="plain">));</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::insert_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">position</span><span class="plain">, </span><span class="functiontext">Calculus::Atoms::QUANTIFIER_new</span><span class="plain">(</span><span class="identifier">not_exists_quantifier</span><span class="plain">, </span><span class="identifier">nv</span><span class="plain">, </span><span class="constant">0</span><span class="plain">));</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">This code is used in <a href="#SP3">&#167;3</a>.</p>
<p class="inwebparagraph"><a id="SP4"></a><b>&#167;4. Use listed-in predicates (deduction). </b>Specifications for entries in tables have a variety of forms (well, four
of them), and one is by implication a condition: this is the 2-reference form
of <code class="display"><span class="extract">TABLE_ENTRY_NT</span></code> specification. Suppose the source text reads
</p>
<blockquote>
<p>if X is a density listed in the Table of Solid Stuff, ...</p>
</blockquote>
<p class="inwebparagraph">Inform parses "a density listed in the Table of Solid Stuff" as a single
specification, with references to the density column and the Solid Stuff
table. In logical terms, this is just another constant, which we'll call L.
At this point the sentence looks like:
is(X, L)
The trouble is that L is really a predicate, acting on some free variable v,
because it stands for any value v found in the density column. We could try
to interpret is so as to accommodate this, but it is much better to
use Inform's regular predicate apparatus.
</p>
<p class="inwebparagraph">So we must make its nature explicit. Every table column has an associated binary
predicate, and we rewrite:
∃ v: number(v)∧ {listed-in-density-column}(v, T)∧ is(v, X)
This looks extravagant, but later simplification will reduce it to
{listed-in-density-column}(X, T).
</p>
<p class="inwebparagraph">More formally suppose we write L(C, T) for the constant representing "a
C listed in T", and suppose we use the notation P(... t...) for any
predicate containing a term underlying which is t. Let v be a variable
unused in Σ, and let K be the kind of value of entries in the C
column. Then:
Σ = ... P(... L(C, T)...) ... --&gt;
Σ' = ... ∃ v: K(v)∧ {listed-in-C-column}(v, T)∧ P(... v...) ...
where the variable v has replaced the constant L(C, T) underlying one
of the terms of P.
</p>
<p class="inwebparagraph">Note that this can act twice on the same predicate, if such terms occur
twice. For example,
</p>
<blockquote>
<p>if a crispiness listed in the Table of Salad Stuff is a density listed in the Table of Solid Stuff, ...</p>
</blockquote>
<p class="inwebparagraph">generates is(L(C_1, T_1), L(C_2, T_2)). As it happens, Inform can't
compile this efficiently and will produce a problem message to say so, but
it's important that our code here should generate the correct proposition,
∃ x: number(x)∧ {listed-in-PM_-column}(x, T_1)∧
{listed-in-PM_-column}(x, T_2).
</p>
<pre class="display">
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="functiontext">Calculus::Simplifications::use_listed_in</span><span class="plain">(</span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">prop</span><span class="plain">, </span><span class="reserved">int</span><span class="plain"> *</span><span class="identifier">changed</span><span class="plain">) {</span>
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
<span class="plain">*</span><span class="identifier">changed</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">) {</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">j</span><span class="plain">;</span>
<span class="reserved">for</span><span class="plain"> (</span><span class="identifier">j</span><span class="plain">=0; </span><span class="identifier">j</span><span class="plain">&lt;</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">arity</span><span class="plain">; </span><span class="identifier">j</span><span class="plain">++) {</span>
<span class="identifier">parse_node</span><span class="plain"> *</span><span class="identifier">spec</span><span class="plain"> = </span><span class="functiontext">Calculus::Terms::constant_underlying</span><span class="plain">(&amp;(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">]));</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">spec</span><span class="plain">) &amp;&amp; (</span><span class="functiontext">Lvalues::get_storage_form</span><span class="plain">(</span><span class="identifier">spec</span><span class="plain">) == </span><span class="constant">TABLE_ENTRY_NT</span><span class="plain">) &amp;&amp;</span>
<span class="plain">(</span><span class="identifier">ParseTree::no_children</span><span class="plain">(</span><span class="identifier">spec</span><span class="plain">) == </span><span class="constant">2</span><span class="plain">)) {</span>
<span class="identifier">parse_node</span><span class="plain"> *</span><span class="identifier">col</span><span class="plain"> = </span><span class="identifier">spec</span><span class="plain">-&gt;</span><span class="element">down</span><span class="plain">;</span>
<span class="identifier">parse_node</span><span class="plain"> *</span><span class="identifier">tab</span><span class="plain"> = </span><span class="identifier">spec</span><span class="plain">-&gt;</span><span class="element">down</span><span class="plain">-&gt;</span><span class="element">next</span><span class="plain">;</span>
<span class="reserved">table_column</span><span class="plain"> *</span><span class="identifier">tc</span><span class="plain"> = </span><span class="functiontext">Rvalues::to_table_column</span><span class="plain">(</span><span class="identifier">col</span><span class="plain">);</span>
<span class="identifier">kind</span><span class="plain"> *</span><span class="identifier">K</span><span class="plain"> = </span><span class="functiontext">Tables::Columns::get_kind</span><span class="plain">(</span><span class="identifier">tc</span><span class="plain">);</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">K_understanding</span><span class="plain">) &amp;&amp; (</span><span class="identifier">Kinds::Compare::eq</span><span class="plain">(</span><span class="identifier">K</span><span class="plain">, </span><span class="identifier">K_understanding</span><span class="plain">))) </span><span class="identifier">K</span><span class="plain"> = </span><span class="identifier">K_snippet</span><span class="plain">;</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">nv</span><span class="plain"> = </span><span class="functiontext">Calculus::Variables::find_unused</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">);</span>
<span class="reserved">pcalc_term</span><span class="plain"> </span><span class="identifier">nv_term</span><span class="plain"> = </span><span class="functiontext">Calculus::Terms::new_variable</span><span class="plain">(</span><span class="identifier">nv</span><span class="plain">);</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::insert_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">,</span>
<span class="functiontext">Calculus::Atoms::binary_PREDICATE_new</span><span class="plain">(</span><span class="functiontext">Tables::Columns::get_listed_in_predicate</span><span class="plain">(</span><span class="identifier">tc</span><span class="plain">),</span>
<span class="identifier">nv_term</span><span class="plain">, </span><span class="functiontext">Calculus::Terms::new_constant</span><span class="plain">(</span><span class="identifier">tab</span><span class="plain">)));</span>
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">new_KIND</span><span class="plain"> = </span><span class="functiontext">Calculus::Atoms::KIND_new</span><span class="plain">(</span><span class="identifier">K</span><span class="plain">, </span><span class="identifier">nv_term</span><span class="plain">);</span>
<span class="identifier">new_KIND</span><span class="plain">-&gt;</span><span class="identifier">predicate</span><span class="plain"> =</span>
<span class="identifier">STORE_POINTER_binary_predicate</span><span class="plain">(</span><span class="functiontext">Tables::Columns::get_listed_in_predicate</span><span class="plain">(</span><span class="identifier">tc</span><span class="plain">));</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::insert_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">, </span><span class="identifier">new_KIND</span><span class="plain">);</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::insert_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">,</span>
<span class="functiontext">Calculus::Atoms::QUANTIFIER_new</span><span class="plain">(</span><span class="identifier">exists_quantifier</span><span class="plain">, </span><span class="identifier">nv</span><span class="plain">, </span><span class="constant">0</span><span class="plain">));</span>
<span class="functiontext">Calculus::Variables::substitute_term_in_term</span><span class="plain">(&amp;(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">]), &amp;</span><span class="identifier">nv_term</span><span class="plain">);</span>
<span class="functiontext">LocalVariables::add_table_lookup</span><span class="plain">();</span>
<span class="identifier">PROPOSITION_EDITED</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">);</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="reserved">return</span><span class="plain"> </span><span class="identifier">prop</span><span class="plain">;</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">The function Calculus::Simplifications::use_listed_in is used in 11/sc (<a href="11-sc.html#SP1_14">&#167;1.14</a>, <a href="11-sc.html#SP2">&#167;2</a>).</p>
<p class="inwebparagraph"><a id="SP5"></a><b>&#167;5. Simplify negated determiners (deduction). </b>The negation atom is worth removing wherever possible, since we want to
keep propositions in a flat conjunction form if we can, and the negation
of a string of atoms is therefore a bad thing. We therefore change thus:
Σ = ... ¬ (Qv∈{ v| φ(v)}: ψ)... --&gt; Σ' = ... Q'v∈{ v| φ(v)}: ψ...
where Q' is the negation of the generalised quantifier Q:
for instance, V_{&lt;5} y becomes V_{&gt;= 5} y.
</p>
<p class="inwebparagraph">A curiosity here is that when simplifying during sentence conversion, we
choose not to apply this deduction in the case of Q = ∃. This saves us
having to make difficult decisions about the domain set of Q (see below),
and also preserves ∃ v atoms in Σ, which are useful since
they make some of our later simplifications more applicable.
</p>
<pre class="display">
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="functiontext">Calculus::Simplifications::negated_determiners_nonex</span><span class="plain">(</span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">prop</span><span class="plain">, </span><span class="reserved">int</span><span class="plain"> *</span><span class="identifier">changed</span><span class="plain">) {</span>
<span class="reserved">return</span><span class="plain"> </span><span class="functiontext">Calculus::Simplifications::negated_determiners</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">changed</span><span class="plain">, </span><span class="identifier">FALSE</span><span class="plain">);</span>
<span class="plain">}</span>
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="functiontext">Calculus::Simplifications::negated_determiners</span><span class="plain">(</span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">prop</span><span class="plain">, </span><span class="reserved">int</span><span class="plain"> *</span><span class="identifier">changed</span><span class="plain">,</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">negate_existence_too</span><span class="plain">) {</span>
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
<span class="plain">*</span><span class="identifier">changed</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">) {</span>
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">quant_atom</span><span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Propositions::match</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="constant">2</span><span class="plain">,</span>
<span class="constant">NEGATION_OPEN_ATOM</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">, </span><span class="constant">QUANTIFIER_ATOM</span><span class="plain">, &amp;</span><span class="identifier">quant_atom</span><span class="plain">)) {</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">negate_existence_too</span><span class="plain">) ||</span>
<span class="plain">((</span><span class="functiontext">Calculus::Atoms::is_existence_quantifier</span><span class="plain">(</span><span class="identifier">quant_atom</span><span class="plain">) == </span><span class="identifier">FALSE</span><span class="plain">))) {</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Simplifications::prop_ungroup_and_negate_determiner</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">, </span><span class="identifier">TRUE</span><span class="plain">);</span>
<span class="identifier">PROPOSITION_EDITED</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">);</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="reserved">return</span><span class="plain"> </span><span class="identifier">prop</span><span class="plain">;</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">The function Calculus::Simplifications::negated_determiners_nonex is used in 11/sc (<a href="11-sc.html#SP1_14">&#167;1.14</a>, <a href="11-sc.html#SP2">&#167;2</a>).</p>
<p class="endnote">The function Calculus::Simplifications::negated_determiners is used in 12/cdp (<a href="12-cdp.html#SP2_1_2">&#167;2.1.2</a>).</p>
<p class="inwebparagraph"><a id="SP6"></a><b>&#167;6. </b>And the following useful routine actually performs the change. The only
tricky point here is that we store ∃ v without domain brackets; so
if Q happens to be ∃ v then we have to turn ¬(∃ v: ...)
into ∄ v∈ { v| ...}..., and it's not
obvious where to place the }. While there's no logical difference &mdash;
the proposition means the same wherever we put it &mdash; the assert-propositions
code is better at handling ∃ v∈ X: φ(v) than ∃ v∈ Y.
So we want the braces to enclose fixed, unassertable matter &mdash; v being
a container, say &mdash; and the φ outside the braces should then contain
predicates which can be asserted.
</p>
<p class="inwebparagraph">In practice that's way too hard for this routine to handle. If <code class="display"><span class="extract">add_domain_brackets</span></code>
is set, then it converts
¬(∃ v: ...) --&gt;
∄ v∈ { v| ...}
&mdash; that is, it will make the entire negated subproposition the domain of the
quantifier. If <code class="display"><span class="extract">add_domain_brackets</span></code> is clear, the routine will return a
syntactically incorrect proposition lacking the domain brackets, and it's
the caller's responsibility to put that right.
</p>
<pre class="display">
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="functiontext">Calculus::Simplifications::prop_ungroup_and_negate_determiner</span><span class="plain">(</span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">prop</span><span class="plain">, </span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">after</span><span class="plain">,</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">add_domain_brackets</span><span class="plain">) {</span>
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">quant_atom</span><span class="plain">, *</span><span class="identifier">last</span><span class="plain">;</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">fnd</span><span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">after</span><span class="plain"> == </span><span class="identifier">NULL</span><span class="plain">)</span>
<span class="identifier">fnd</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::match</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="constant">2</span><span class="plain">,</span>
<span class="constant">NEGATION_OPEN_ATOM</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">, </span><span class="constant">QUANTIFIER_ATOM</span><span class="plain">, &amp;</span><span class="identifier">quant_atom</span><span class="plain">);</span>
<span class="reserved">else</span>
<span class="identifier">fnd</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::match</span><span class="plain">(</span><span class="identifier">after</span><span class="plain">, </span><span class="constant">3</span><span class="plain">, </span><span class="constant">ANY_ATOM_HERE</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">,</span>
<span class="constant">NEGATION_OPEN_ATOM</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">, </span><span class="constant">QUANTIFIER_ATOM</span><span class="plain">, &amp;</span><span class="identifier">quant_atom</span><span class="plain">);</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">fnd</span><span class="plain">) {</span>
<span class="identifier">quantifier</span><span class="plain"> *</span><span class="identifier">quant</span><span class="plain"> = </span><span class="identifier">RETRIEVE_POINTER_quantifier</span><span class="plain">(</span><span class="identifier">quant_atom</span><span class="plain">-&gt;</span><span class="element">predicate</span><span class="plain">);</span>
<span class="identifier">quantifier</span><span class="plain"> *</span><span class="identifier">antiquant</span><span class="plain"> = </span><span class="identifier">Quantifiers::get_negation</span><span class="plain">(</span><span class="identifier">quant</span><span class="plain">);</span>
<span class="identifier">quant_atom</span><span class="plain">-&gt;</span><span class="element">predicate</span><span class="plain"> = </span><span class="identifier">STORE_POINTER_quantifier</span><span class="plain">(</span><span class="identifier">antiquant</span><span class="plain">);</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::ungroup_after</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">after</span><span class="plain">, &amp;</span><span class="identifier">last</span><span class="plain">); </span><span class="comment">remove negation group brackets</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">quant</span><span class="plain"> == </span><span class="identifier">exists_quantifier</span><span class="plain">) &amp;&amp; (</span><span class="identifier">add_domain_brackets</span><span class="plain">)) {</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::insert_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">quant_atom</span><span class="plain">, </span><span class="functiontext">Calculus::Atoms::new</span><span class="plain">(</span><span class="constant">DOMAIN_OPEN_ATOM</span><span class="plain">));</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::insert_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">last</span><span class="plain">, </span><span class="functiontext">Calculus::Atoms::new</span><span class="plain">(</span><span class="constant">DOMAIN_CLOSE_ATOM</span><span class="plain">));</span>
<span class="plain">}</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">antiquant</span><span class="plain"> == </span><span class="identifier">exists_quantifier</span><span class="plain">) {</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::ungroup_after</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">quant_atom</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">); </span><span class="comment">remove domain group brackets</span>
<span class="plain">}</span>
<span class="identifier">LOGIF</span><span class="plain">(</span><span class="identifier">PREDICATE_CALCULUS_WORKINGS</span><span class="plain">, </span><span class="string">"Calculus::Simplifications::prop_ungroup_and_negate_determiner: $D\n"</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">);</span>
<span class="plain">} </span><span class="reserved">else</span><span class="plain"> </span><span class="identifier">internal_error</span><span class="plain">(</span><span class="string">"not a negate-group-determiner"</span><span class="plain">);</span>
<span class="reserved">return</span><span class="plain"> </span><span class="identifier">prop</span><span class="plain">;</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">The function Calculus::Simplifications::prop_ungroup_and_negate_determiner is used in <a href="#SP5">&#167;5</a>, <a href="#SP7">&#167;7</a>.</p>
<p class="inwebparagraph"><a id="SP7"></a><b>&#167;7. Simplify negated satisfiability (deduction). </b>When simplifying converted sentences, we chose not to use the
<code class="display"><span class="extract">Calculus::Simplifications::negated_determiners</span></code> tactic on existence quantifiers ∃ v,
partly because it's tricky to establish their domain in a way helpful to
the rest of Inform.
</p>
<p class="inwebparagraph">Here we handle a simple case which occurs frequently and where we can indeed
identify the domain well:
Σ = ¬ (∃ v: K(v)∧ P) --&gt;
Σ' = ∄ v∈{ v| K(v)}: P
where K is a kind, and P is any single predicate other than equality.
(In the case of equality, we'd rather leave matters as they stand, because
substitution will later eliminate all of this anyway.)
</p>
<pre class="display">
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="functiontext">Calculus::Simplifications::negated_satisfiable</span><span class="plain">(</span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">prop</span><span class="plain">, </span><span class="reserved">int</span><span class="plain"> *</span><span class="identifier">changed</span><span class="plain">) {</span>
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">quant_atom</span><span class="plain">, *</span><span class="identifier">predicate_atom</span><span class="plain">, *</span><span class="identifier">kind_atom</span><span class="plain">;</span>
<span class="plain">*</span><span class="identifier">changed</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="functiontext">Calculus::Propositions::match</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="constant">6</span><span class="plain">,</span>
<span class="constant">NEGATION_OPEN_ATOM</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">,</span>
<span class="constant">QUANTIFIER_ATOM</span><span class="plain">, &amp;</span><span class="identifier">quant_atom</span><span class="plain">,</span>
<span class="constant">KIND_ATOM</span><span class="plain">, &amp;</span><span class="identifier">kind_atom</span><span class="plain">,</span>
<span class="constant">PREDICATE_ATOM</span><span class="plain">, &amp;</span><span class="identifier">predicate_atom</span><span class="plain">,</span>
<span class="constant">NEGATION_CLOSE_ATOM</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">,</span>
<span class="constant">END_PROP_HERE</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">)) &amp;&amp;</span>
<span class="plain">(</span><span class="functiontext">Calculus::Atoms::is_existence_quantifier</span><span class="plain">(</span><span class="identifier">quant_atom</span><span class="plain">)) &amp;&amp;</span>
<span class="plain">(</span><span class="functiontext">Calculus::Atoms::is_equality_predicate</span><span class="plain">(</span><span class="identifier">predicate_atom</span><span class="plain">) == </span><span class="identifier">FALSE</span><span class="plain">) &amp;&amp;</span>
<span class="plain">(</span><span class="identifier">kind_atom</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[0].</span><span class="element">variable</span><span class="plain"> == </span><span class="identifier">quant_atom</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[0].</span><span class="element">variable</span><span class="plain">)) {</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Simplifications::prop_ungroup_and_negate_determiner</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">, </span><span class="identifier">FALSE</span><span class="plain">);</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::insert_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">quant_atom</span><span class="plain">, </span><span class="functiontext">Calculus::Atoms::new</span><span class="plain">(</span><span class="constant">DOMAIN_OPEN_ATOM</span><span class="plain">));</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::insert_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">kind_atom</span><span class="plain">, </span><span class="functiontext">Calculus::Atoms::new</span><span class="plain">(</span><span class="constant">DOMAIN_CLOSE_ATOM</span><span class="plain">));</span>
<span class="plain">*</span><span class="identifier">changed</span><span class="plain"> = </span><span class="identifier">TRUE</span><span class="plain">;</span>
<span class="plain">}</span>
<span class="reserved">return</span><span class="plain"> </span><span class="identifier">prop</span><span class="plain">;</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">The function Calculus::Simplifications::negated_satisfiable is used in 11/sc (<a href="11-sc.html#SP1_14">&#167;1.14</a>, <a href="11-sc.html#SP2">&#167;2</a>).</p>
<p class="inwebparagraph"><a id="SP8"></a><b>&#167;8. Make kind requirements explicit (deduction). </b>Many predicates contain implicit requirements about the kinds of their terms.
For instance, if R relates a door to a number, then R(x,y) can only be
true if x is a door and y is a number. We insert these requirements
explicitly in order to defend the code testing R; it ensures we never have
to test bogus values. We need do this only for variables, as with more
constants and functions type-checking will certainly be able to test their
kind in any event (whereas a free variable is anonymous enough that we can't
necessarily know by other means).
</p>
<p class="inwebparagraph">Formally, let K_1 and K_2 be the kinds of value of terms 1 and 2 of the
binary predicate R. Let v be a variable. Then:
Σ = ... R(v, t)... --&gt;
Σ' = ... K_1(v)∧ R(v, t)
Σ = ... R(t, v)... --&gt;
Σ' = ... K_2(v)∧ R(t, v)
and therefore, if both cases occur,
Σ = ... R(v, w)... --&gt;
Σ' = ... K_1(v)∧ K_2(w)∧ R(v, w)
</p>
<p class="inwebparagraph">Some of these new kind atoms are unnecessary, but <code class="display"><span class="extract">Calculus::Simplifications::redundant_kinds</span></code> will
detect and remove those.
</p>
<p class="inwebparagraph">Why do we do this for binary predicates, but not unary predicates? The answer
is that there's no need, and it's impracticable anyway, because adjectives
are allowed to have multiple definitions for different kinds of value, and
because the code testing them is written to cope properly with bogus values.
</p>
<pre class="display">
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="functiontext">Calculus::Simplifications::make_kinds_of_value_explicit</span><span class="plain">(</span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">prop</span><span class="plain">, </span><span class="reserved">int</span><span class="plain"> *</span><span class="identifier">changed</span><span class="plain">) {</span>
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">)</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::is_binary_predicate</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">)) {</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">i</span><span class="plain">;</span>
<span class="reserved">binary_predicate</span><span class="plain"> *</span><span class="identifier">bp</span><span class="plain"> = </span><span class="identifier">RETRIEVE_POINTER_binary_predicate</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">predicate</span><span class="plain">);</span>
<span class="reserved">for</span><span class="plain"> (</span><span class="identifier">i</span><span class="plain">=1; </span><span class="identifier">i</span><span class="plain">&gt;=0; </span><span class="identifier">i</span><span class="plain">--) {</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">v</span><span class="plain"> = </span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[</span><span class="identifier">i</span><span class="plain">].</span><span class="element">variable</span><span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">v</span><span class="plain"> &gt;= </span><span class="constant">0</span><span class="plain">) {</span>
<span class="identifier">kind</span><span class="plain"> *</span><span class="identifier">K</span><span class="plain"> = </span><span class="functiontext">BinaryPredicates::term_kind</span><span class="plain">(</span><span class="identifier">bp</span><span class="plain">, </span><span class="identifier">i</span><span class="plain">);</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">K</span><span class="plain">) {</span>
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">new_KIND</span><span class="plain"> = </span><span class="functiontext">Calculus::Atoms::KIND_new</span><span class="plain">(</span><span class="identifier">K</span><span class="plain">, </span><span class="functiontext">Calculus::Terms::new_variable</span><span class="plain">(</span><span class="identifier">v</span><span class="plain">));</span>
<span class="identifier">new_KIND</span><span class="plain">-&gt;</span><span class="identifier">predicate</span><span class="plain"> = </span><span class="identifier">STORE_POINTER_binary_predicate</span><span class="plain">(</span><span class="identifier">bp</span><span class="plain">);</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::insert_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">, </span><span class="identifier">new_KIND</span><span class="plain">);</span>
<span class="plain">}</span>
<span class="plain">*</span><span class="identifier">changed</span><span class="plain"> = </span><span class="identifier">TRUE</span><span class="plain">;</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="reserved">return</span><span class="plain"> </span><span class="identifier">prop</span><span class="plain">;</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">The function Calculus::Simplifications::make_kinds_of_value_explicit is used in 11/tc (<a href="11-tc.html#SP3">&#167;3</a>), 11/sc (<a href="11-sc.html#SP1_14">&#167;1.14</a>, <a href="11-sc.html#SP2">&#167;2</a>).</p>
<p class="inwebparagraph"><a id="SP9"></a><b>&#167;9. Remove redundant kind predicates (deduction). </b>Propositions often contain more <code class="display"><span class="extract">KIND</span></code> atoms than they need, not least as a
result of <code class="display"><span class="extract">Calculus::Simplifications::make_kinds_of_value_explicit</span></code>. Here we remove (some of)
those, and move the survivors to what we consider the best positions within
the line. For reasons to be revealed below, we run this process twice over:
</p>
<pre class="display">
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="functiontext">Calculus::Simplifications::redundant_kinds</span><span class="plain">(</span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">prop</span><span class="plain">, </span><span class="reserved">int</span><span class="plain"> *</span><span class="identifier">changed</span><span class="plain">) {</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">c1</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">, </span><span class="identifier">c2</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Simplifications::simp_redundant_kinds_dash</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">, </span><span class="constant">1</span><span class="plain">, &amp;</span><span class="identifier">c1</span><span class="plain">);</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Simplifications::simp_redundant_kinds_dash</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">, </span><span class="constant">1</span><span class="plain">, &amp;</span><span class="identifier">c2</span><span class="plain">);</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">c1</span><span class="plain">) || (</span><span class="identifier">c2</span><span class="plain">)) *</span><span class="identifier">changed</span><span class="plain"> = </span><span class="identifier">TRUE</span><span class="plain">; </span><span class="reserved">else</span><span class="plain"> *</span><span class="identifier">changed</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
<span class="reserved">return</span><span class="plain"> </span><span class="identifier">prop</span><span class="plain">;</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">The function Calculus::Simplifications::redundant_kinds is used in 11/sc (<a href="11-sc.html#SP1_14">&#167;1.14</a>, <a href="11-sc.html#SP2">&#167;2</a>).</p>
<p class="inwebparagraph"><a id="SP10"></a><b>&#167;10. </b>This routine works recursively on subexpressions within the main
proposition. These all begin and end with matched <code class="display"><span class="extract">*_OPEN_ATOM</span></code> and
<code class="display"><span class="extract">*_CLOSED_ATOM</span></code> brackets, with one exception: the main proposition itself.
<code class="display"><span class="extract">start_group</span></code> represents the first atom of the expression (the open
bracket, in most cases) and <code class="display"><span class="extract">start_level</span></code> the level of bracket nesting
at that point. This is 1 for the main proposition, but 0 for subexpressions,
so that inside the brackets the main content will be at level 1.
</p>
<p class="inwebparagraph">This would all go wrong if the proposition were not well-formed, but we
know that it is &mdash; an internal error would have been thrown if not.
</p>
<pre class="display">
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="functiontext">Calculus::Simplifications::simp_redundant_kinds_dash</span><span class="plain">(</span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">prop</span><span class="plain">, </span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">start_group</span><span class="plain">,</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">start_level</span><span class="plain">, </span><span class="reserved">int</span><span class="plain"> *</span><span class="identifier">changed</span><span class="plain">) {</span>
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">optimal_kind_placings_domain</span><span class="plain">[26], *</span><span class="identifier">optimal_kind_placings_statement</span><span class="plain">[26];</span>
&lt;<span class="cwebmacro">Recursively simplify all subexpressions first</span> <span class="cwebmacronumber">10.1</span>&gt;<span class="plain">;</span>
&lt;<span class="cwebmacro">Find optimal positions for kind predicates</span> <span class="cwebmacronumber">10.2</span>&gt;<span class="plain">;</span>
&lt;<span class="cwebmacro">Strike out redundant kind predicates applied to variables</span> <span class="cwebmacronumber">10.3</span>&gt;<span class="plain">;</span>
&lt;<span class="cwebmacro">Strike out tautological kind predicates applied to constants</span> <span class="cwebmacronumber">10.4</span>&gt;<span class="plain">;</span>
<span class="reserved">return</span><span class="plain"> </span><span class="identifier">prop</span><span class="plain">;</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">The function Calculus::Simplifications::simp_redundant_kinds_dash is used in <a href="#SP9">&#167;9</a>, <a href="#SP10_1">&#167;10.1</a>.</p>
<p class="inwebparagraph"><a id="SP10_1"></a><b>&#167;10.1. </b>For all of the atoms in the body of the group we're working on, the bracket
level will be 1. When it raises to 2, then, we begin a subexpression, and
we recurse into it. (We don't recurse at levels 3 and up because the level 2
call will already have taken care of those sub-sub-expressions.)
</p>
<p class="macrodefinition"><code class="display">
&lt;<span class="cwebmacrodefn">Recursively simplify all subexpressions first</span> <span class="cwebmacronumber">10.1</span>&gt; =
</code></p>
<pre class="displaydefn">
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">blevel</span><span class="plain"> = </span><span class="identifier">start_level</span><span class="plain">;</span>
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">start_group</span><span class="plain">) {</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::element_get_group</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">element</span><span class="plain">) == </span><span class="constant">OPEN_OPERATORS_GROUP</span><span class="plain">) {</span>
<span class="identifier">blevel</span><span class="plain">++;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">blevel</span><span class="plain"> == </span><span class="constant">2</span><span class="plain">) </span><span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Simplifications::simp_redundant_kinds_dash</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl</span><span class="plain">, </span><span class="constant">0</span><span class="plain">, </span><span class="identifier">changed</span><span class="plain">);</span>
<span class="plain">}</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::element_get_group</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">element</span><span class="plain">) == </span><span class="constant">CLOSE_OPERATORS_GROUP</span><span class="plain">) </span><span class="identifier">blevel</span><span class="plain">--;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">blevel</span><span class="plain"> == </span><span class="constant">0</span><span class="plain">) </span><span class="reserved">break</span><span class="plain">;</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">This code is used in <a href="#SP10">&#167;10</a>.</p>
<p class="inwebparagraph"><a id="SP10_2"></a><b>&#167;10.2. </b>Suppose we have a kind predicate K(v) applied to a variable. What would
be the best place to put this? Generally speaking, we want it as early as
possible, because tests of K are cheap and this will keep running time
low in compiled code. On the other hand we must not move it outside the
current subexpression. The doctrine is:
</p>
<p class="inwebparagraph"></p>
<ul class="items"><li>(i) if v is unbound within the subexpression then K(v) should
move right to the front;
</li><li>(ii) if v is bound by ∃, then K(v) should move immediately
after ∃ v;
</li><li>(iii) if v is bound by Q v∈{ v| φ(v)} then any
K(v) occurring in the domain φ(v) should move to the front of v,
whereas any later K(v) should move after the domain closing, except
</li><li>(iv) where v is bound by ∄ v∈{ v| φ(v)},
when K(v) should move into the domain set, even if it occurs in the
statement.
</li></ul>
<p class="inwebparagraph">Rule (iv) there looks a little surprising. For instance, it causes
Σ = ∄ x∈{ x| thing(x)∧contains(<code class="display"><span class="extract">Ballroom</span></code>, x)} :
container(x)∧ open(x)
--&gt;
Σ' = ∄ x∈{ x| container(x)∧thing(x)∧contains(<code class="display"><span class="extract">Ballroom</span></code>, x)} :
open(x).
These are logically equivalent because ∄ behaves that way &mdash;
they wouldn't be equivalent for other quantifiers. Rule (iii) would have
said no movement was necessary; the reason we made the move is that it
makes Σ' possible to assert with "now", as in the phrase "now
nothing in the Ballroom is an open container".
</p>
<p class="inwebparagraph">The following calculates two arrays: <code class="display"><span class="extract">optimal_kind_placings_domain</span></code> marks the
start of φ for each variable v, while <code class="display"><span class="extract">optimal_kind_placings_statement</span></code>
marks the start of the statement following the quantifier.
</p>
<p class="macrodefinition"><code class="display">
&lt;<span class="cwebmacrodefn">Find optimal positions for kind predicates</span> <span class="cwebmacronumber">10.2</span>&gt; =
</code></p>
<pre class="displaydefn">
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">bvsp</span><span class="plain"> = </span><span class="constant">0</span><span class="plain">, </span><span class="identifier">bound_vars_stack</span><span class="plain">[26];</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">blevel</span><span class="plain"> = </span><span class="identifier">start_level</span><span class="plain">, </span><span class="identifier">j</span><span class="plain">;</span>
<span class="reserved">for</span><span class="plain"> (</span><span class="identifier">j</span><span class="plain">=0; </span><span class="identifier">j</span><span class="plain">&lt;26; </span><span class="identifier">j</span><span class="plain">++) {</span>
<span class="identifier">optimal_kind_placings_domain</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">] = (</span><span class="identifier">start_level</span><span class="plain"> == </span><span class="constant">1</span><span class="plain">)?</span><span class="identifier">NULL:start_group</span><span class="plain">;</span>
<span class="identifier">optimal_kind_placings_statement</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">] = </span><span class="identifier">optimal_kind_placings_domain</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">];</span>
<span class="plain">}</span>
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">start_group</span><span class="plain">) {</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::element_get_group</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">element</span><span class="plain">) == </span><span class="constant">OPEN_OPERATORS_GROUP</span><span class="plain">) </span><span class="identifier">blevel</span><span class="plain">++;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::element_get_group</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">element</span><span class="plain">) == </span><span class="constant">CLOSE_OPERATORS_GROUP</span><span class="plain">) </span><span class="identifier">blevel</span><span class="plain">--;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">blevel</span><span class="plain"> == </span><span class="constant">0</span><span class="plain">) </span><span class="reserved">break</span><span class="plain">;</span>
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">dom</span><span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Propositions::match</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="constant">2</span><span class="plain">,</span>
<span class="constant">QUANTIFIER_ATOM</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">, </span><span class="constant">DOMAIN_OPEN_ATOM</span><span class="plain">, &amp;</span><span class="identifier">dom</span><span class="plain">)) {</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="functiontext">Calculus::Atoms::is_existence_quantifier</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">)) ||</span>
<span class="plain">(</span><span class="functiontext">Calculus::Atoms::is_nonexistence_quantifier</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">)))</span>
<span class="identifier">bound_vars_stack</span><span class="plain">[</span><span class="identifier">bvsp</span><span class="plain">++] = -1;</span>
<span class="reserved">else</span>
<span class="identifier">bound_vars_stack</span><span class="plain">[</span><span class="identifier">bvsp</span><span class="plain">++] = </span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[0].</span><span class="element">variable</span><span class="plain">;</span>
<span class="identifier">optimal_kind_placings_domain</span><span class="plain">[</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="identifier">terms</span><span class="plain">[0].</span><span class="element">variable</span><span class="plain">] = </span><span class="identifier">dom</span><span class="plain">;</span>
<span class="identifier">optimal_kind_placings_statement</span><span class="plain">[</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[0].</span><span class="element">variable</span><span class="plain">] = </span><span class="identifier">dom</span><span class="plain">;</span>
<span class="plain">} </span><span class="reserved">else</span><span class="plain"> </span><span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::is_existence_quantifier</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">)) {</span>
<span class="identifier">optimal_kind_placings_domain</span><span class="plain">[</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="identifier">terms</span><span class="plain">[0].</span><span class="element">variable</span><span class="plain">] = </span><span class="identifier">pl</span><span class="plain">;</span>
<span class="identifier">optimal_kind_placings_statement</span><span class="plain">[</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[0].</span><span class="element">variable</span><span class="plain">] = </span><span class="identifier">pl</span><span class="plain">;</span>
<span class="plain">}</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">element</span><span class="plain"> == </span><span class="constant">DOMAIN_CLOSE_ATOM</span><span class="plain">) {</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">v</span><span class="plain"> = </span><span class="identifier">bound_vars_stack</span><span class="plain">[--</span><span class="identifier">bvsp</span><span class="plain">];</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">v</span><span class="plain"> &gt;= </span><span class="constant">0</span><span class="plain">) </span><span class="identifier">optimal_kind_placings_statement</span><span class="plain">[</span><span class="identifier">v</span><span class="plain">] = </span><span class="identifier">pl</span><span class="plain">;</span>
<span class="plain">}</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">This code is used in <a href="#SP10">&#167;10</a>.</p>
<p class="inwebparagraph"><a id="SP10_3"></a><b>&#167;10.3. </b>The following looks at the predicates K(v) applied to variables which
are in the subexpression at the top level. It then does two things:
</p>
<p class="inwebparagraph">Suppose K and L are kinds of value such that L⊆ K, and let
ψ be a well-formed proposition. Then
Σ = ψ ∧ L(v) ... K(v) ...
--&gt;
Σ' = ψ ∧ L(v) ...
(that is, K(v) is eliminated). This is clearly valid since L(v)=&gt; K(v)
and L(v) is valid throughout the subexpression after its appearance.
</p>
<p class="inwebparagraph">Secondly, and it's not worth finding a logical notation for this, the kind
is moved back to its optimal position, as calculated above.
</p>
<p class="inwebparagraph">At first sight, this process only removes redundancies when the stronger
kind appears before the weaker one. What if they occur the other way around?
This is why the simplification is run twice, and why it's important that
the process of moving predicates back to their optimal position reverses
their order. Suppose we start with person(x)∧vehicle(y)∧woman(x).
</p>
<p class="inwebparagraph"></p>
<ul class="items"><li>(1a) On pass 1, person occurs before woman, but it is weaker &mdash;
every woman is a person, but not necessarily vice versa &mdash; so neither is
deleted.
</li><li>(1b) But pass 1 also moves the kinds back, and this produces
woman(x)∧vehicle(y)∧person(x).
</li><li>(2a) On pass 2, the stronger woman now occurs before person, so
we eliminate to get woman(x)∧vehicle(y).
</li><li>(2b) And pass 2 again moves kinds back, producing vehicle(y)∧woman(x).
</li></ul>
<p class="inwebparagraph">(Because the order is reversed twice, any surviving kind predicates continue
to appear in the same order as they did in the original proposition. This
doesn't matter, but it's tidy.)
</p>
<p class="macrodefinition"><code class="display">
&lt;<span class="cwebmacrodefn">Strike out redundant kind predicates applied to variables</span> <span class="cwebmacronumber">10.3</span>&gt; =
</code></p>
<pre class="displaydefn">
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">domain_passed</span><span class="plain">[26], </span><span class="identifier">j</span><span class="plain">;</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">blevel</span><span class="plain"> = </span><span class="identifier">start_level</span><span class="plain">;</span>
<span class="reserved">for</span><span class="plain"> (</span><span class="identifier">j</span><span class="plain">=0; </span><span class="identifier">j</span><span class="plain">&lt;26; </span><span class="identifier">j</span><span class="plain">++) </span><span class="identifier">domain_passed</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">] = </span><span class="identifier">FALSE</span><span class="plain">;</span>
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">start_group</span><span class="plain">) {</span>
<span class="reserved">for</span><span class="plain"> (</span><span class="identifier">j</span><span class="plain">=0; </span><span class="identifier">j</span><span class="plain">&lt;26; </span><span class="identifier">j</span><span class="plain">++)</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">pl</span><span class="plain"> == </span><span class="identifier">optimal_kind_placings_statement</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">])</span>
<span class="identifier">domain_passed</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">] = </span><span class="identifier">TRUE</span><span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::element_get_group</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">element</span><span class="plain">) == </span><span class="constant">OPEN_OPERATORS_GROUP</span><span class="plain">) </span><span class="identifier">blevel</span><span class="plain">++;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::element_get_group</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">element</span><span class="plain">) == </span><span class="constant">CLOSE_OPERATORS_GROUP</span><span class="plain">) </span><span class="identifier">blevel</span><span class="plain">--;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">blevel</span><span class="plain"> == </span><span class="constant">1</span><span class="plain">) {</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">element</span><span class="plain"> == </span><span class="constant">KIND_ATOM</span><span class="plain">) {</span>
<span class="identifier">kind</span><span class="plain"> *</span><span class="identifier">early_kind</span><span class="plain"> = </span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">assert_kind</span><span class="plain">;</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">v</span><span class="plain"> = </span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[0].</span><span class="element">variable</span><span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">v</span><span class="plain"> &gt;= </span><span class="constant">0</span><span class="plain">) &amp;&amp; (</span><span class="identifier">early_kind</span><span class="plain">)) {</span>
&lt;<span class="cwebmacro">Strike out any subsequent but weaker kind predicate on the same variable</span> <span class="cwebmacronumber">10.3.1</span>&gt;<span class="plain">;</span>
&lt;<span class="cwebmacro">Move this predicate backwards to its optimal position</span> <span class="cwebmacronumber">10.3.2</span>&gt;<span class="plain">;</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">blevel</span><span class="plain"> == </span><span class="constant">0</span><span class="plain">) </span><span class="reserved">break</span><span class="plain">;</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">This code is used in <a href="#SP10">&#167;10</a>.</p>
<p class="inwebparagraph"><a id="SP10_3_1"></a><b>&#167;10.3.1. </b>The noteworthy thing here is that we continue through the subexpression,
deleting any weaker form of K(v) that we find, but also allow ourselves
to continue beyond the subexpression in one case. Suppose we have
Qv∈{ v| K(v) ∧... } : L(v)
and we are working on the K(v) term. If we continue only to the end of
the current subexpression, that runs out at the }, the end of
the domain specification. So in that one case alone we allow ourselves
to sidestep the <code class="display"><span class="extract">DOMAIN_CLOSE_ATOM</span></code> and continue looking for L(v) in the
outer subexpression &mdash; the one which is governed by the quantifier.
</p>
<p class="macrodefinition"><code class="display">
&lt;<span class="cwebmacrodefn">Strike out any subsequent but weaker kind predicate on the same variable</span> <span class="cwebmacronumber">10.3.1</span>&gt; =
</code></p>
<pre class="displaydefn">
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">gpl</span><span class="plain">);</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">glevel</span><span class="plain"> = </span><span class="constant">1</span><span class="plain">;</span>
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">gpl</span><span class="plain">, </span><span class="identifier">pl</span><span class="plain">) {</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::element_get_group</span><span class="plain">(</span><span class="identifier">gpl</span><span class="plain">-&gt;</span><span class="element">element</span><span class="plain">) == </span><span class="constant">OPEN_OPERATORS_GROUP</span><span class="plain">) </span><span class="identifier">glevel</span><span class="plain">++;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">gpl</span><span class="plain">-&gt;</span><span class="element">element</span><span class="plain"> == </span><span class="constant">DOMAIN_CLOSE_ATOM</span><span class="plain">) {</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">glevel</span><span class="plain"> &gt; </span><span class="constant">1</span><span class="plain">) </span><span class="identifier">glevel</span><span class="plain">--;</span>
<span class="plain">} </span><span class="reserved">else</span><span class="plain"> </span><span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::element_get_group</span><span class="plain">(</span><span class="identifier">gpl</span><span class="plain">-&gt;</span><span class="element">element</span><span class="plain">) == </span><span class="constant">CLOSE_OPERATORS_GROUP</span><span class="plain">) </span><span class="identifier">glevel</span><span class="plain">--;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">glevel</span><span class="plain"> == </span><span class="constant">0</span><span class="plain">) </span><span class="reserved">break</span><span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">gpl</span><span class="plain"> != </span><span class="identifier">pl</span><span class="plain">) &amp;&amp; (</span><span class="identifier">gpl</span><span class="plain">-&gt;</span><span class="element">element</span><span class="plain"> == </span><span class="constant">KIND_ATOM</span><span class="plain">) &amp;&amp; (</span><span class="identifier">v</span><span class="plain"> == </span><span class="identifier">gpl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[0].</span><span class="element">variable</span><span class="plain">)) {</span>
<span class="comment">i.e., <code class="display"><span class="extract">gpl</span></code> now points to a different kind atom on the same variable</span>
<span class="identifier">kind</span><span class="plain"> *</span><span class="identifier">later_kind</span><span class="plain"> = </span><span class="identifier">gpl</span><span class="plain">-&gt;</span><span class="element">assert_kind</span><span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">later_kind</span><span class="plain">) &amp;&amp; (</span><span class="identifier">Kinds::Compare::le</span><span class="plain">(</span><span class="identifier">early_kind</span><span class="plain">, </span><span class="identifier">later_kind</span><span class="plain">))) {</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">gpl_prev</span><span class="plain">);</span>
<span class="identifier">PROPOSITION_EDITED_REPEATING_CURRENT</span><span class="plain">(</span><span class="identifier">gpl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">);</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">This code is used in <a href="#SP10_3">&#167;10.3</a>.</p>
<p class="inwebparagraph"><a id="SP10_3_2"></a><b>&#167;10.3.2. </b><code class="display">
&lt;<span class="cwebmacrodefn">Move this predicate backwards to its optimal position</span> <span class="cwebmacronumber">10.3.2</span>&gt; =
</code></p>
<pre class="displaydefn">
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">best_place</span><span class="plain"> = </span><span class="identifier">optimal_kind_placings_domain</span><span class="plain">[</span><span class="identifier">v</span><span class="plain">];</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">domain_passed</span><span class="plain">[</span><span class="identifier">v</span><span class="plain">]) </span><span class="identifier">best_place</span><span class="plain"> = </span><span class="identifier">optimal_kind_placings_statement</span><span class="plain">[</span><span class="identifier">v</span><span class="plain">];</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">pl_prev</span><span class="plain"> != </span><span class="identifier">best_place</span><span class="plain">) {</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">state</span><span class="plain"> = </span><span class="functiontext">Calculus::Atoms::is_unarticled</span><span class="plain">(</span><span class="identifier">pl_prev</span><span class="plain">);</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">); </span><span class="comment">that is, delete the current K(v)</span>
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">new_K</span><span class="plain"> = </span><span class="functiontext">Calculus::Atoms::KIND_new</span><span class="plain">(</span><span class="identifier">early_kind</span><span class="plain">,</span>
<span class="functiontext">Calculus::Terms::new_variable</span><span class="plain">(</span><span class="identifier">v</span><span class="plain">));</span>
<span class="functiontext">Calculus::Atoms::set_unarticled</span><span class="plain">(</span><span class="identifier">new_K</span><span class="plain">, </span><span class="identifier">state</span><span class="plain">);</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::insert_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">best_place</span><span class="plain">, </span><span class="identifier">new_K</span><span class="plain">); </span><span class="comment">insert a new one</span>
<span class="identifier">PROPOSITION_EDITED_REPEATING_CURRENT</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">);</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">This code is used in <a href="#SP10_3">&#167;10.3</a>.</p>
<p class="inwebparagraph"><a id="SP10_4"></a><b>&#167;10.4. </b>Suppose we find a term K(C), where C is a constant in the sense of
predicate calculus &mdash; that is, a <code class="display"><span class="extract">specification</span></code>. There is no need to
perform such a test at run-time because we can determine the kind of C
and compare it against K right now. For instance, number(<code class="display"><span class="extract">score</span></code>)
is necessarily true at all times.
</p>
<p class="inwebparagraph">Formally, suppose C is a constant which, when evaluated, has kind of value
L. Suppose that L⊆ K and that K is not a kind of object. Then
Σ = ... K(C)... --&gt; Σ' = ......
(That is, we eliminate the K(C) term.)
</p>
<p class="inwebparagraph">We could clearly go further than this:
</p>
<ul class="items"><li>(a) Why don't we eliminate K(C) when K is an object, too? Logically this
would be fine, but we choose not to, for two reasons: people sometimes write
phrases in I6 which claim to return a room, say, but sometimes return <code class="display"><span class="extract">nothing</span></code>.
Technically this is a violation of type safety. If t is a term representing
a call to this function, then room(t) ought to be redundant. But in
practice it will protect against the <code class="display"><span class="extract">nothing</span></code> value. The other reason is
to ensure that text like "Peter is a man" is not simplified all the way
down to the null proposition (as it clearly can be, if Peter is indeed a man).
That might seem harmless, but means that "now Peter is a man" doesn't produce
the problem message saying that kinds can't be asserted &mdash; a common mistake
made by beginners. It's better consistently to reject all such attempts than
to be clever and allow the ones which are logically redundant.
</li><li>(b) Why don't we reduce K(C) to falsity when C is a constant clearly not
of the kind K, such as text(4)? Again, it would make it harder to
issue a good problem message later, in type-checking; and besides our
calculus lacks a "falsity" atom, so there's no way to store the universally
false proposition which would result if we eliminated every atom this way.
(It also doesn't matter what the running time of compiled code will be if
the proposition is going to fail type-checking anyway.)
</li></ul>
<p class="macrodefinition"><code class="display">
&lt;<span class="cwebmacrodefn">Strike out tautological kind predicates applied to constants</span> <span class="cwebmacronumber">10.4</span>&gt; =
</code></p>
<pre class="displaydefn">
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">blevel</span><span class="plain"> = </span><span class="identifier">start_level</span><span class="plain">;</span>
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">start_group</span><span class="plain">) {</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::element_get_group</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">element</span><span class="plain">) == </span><span class="constant">OPEN_OPERATORS_GROUP</span><span class="plain">) </span><span class="identifier">blevel</span><span class="plain">++;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::element_get_group</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">element</span><span class="plain">) == </span><span class="constant">CLOSE_OPERATORS_GROUP</span><span class="plain">) </span><span class="identifier">blevel</span><span class="plain">--;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">blevel</span><span class="plain"> == </span><span class="constant">1</span><span class="plain">) {</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">element</span><span class="plain"> == </span><span class="constant">KIND_ATOM</span><span class="plain">) {</span>
<span class="identifier">kind</span><span class="plain"> *</span><span class="identifier">early_kind</span><span class="plain"> = </span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">assert_kind</span><span class="plain">;</span>
<span class="identifier">parse_node</span><span class="plain"> *</span><span class="identifier">spec</span><span class="plain"> = </span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[0].</span><span class="element">constant</span><span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">ParseTreeUsage::is_rvalue</span><span class="plain">(</span><span class="identifier">spec</span><span class="plain">)) {</span>
<span class="identifier">kind</span><span class="plain"> *</span><span class="identifier">K</span><span class="plain"> = </span><span class="functiontext">Rvalues::to_kind</span><span class="plain">(</span><span class="identifier">spec</span><span class="plain">);</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">K</span><span class="plain">) &amp;&amp; (</span><span class="identifier">Kinds::Compare::lt</span><span class="plain">(</span><span class="identifier">early_kind</span><span class="plain">, </span><span class="identifier">K_object</span><span class="plain">) == </span><span class="identifier">FALSE</span><span class="plain">) &amp;&amp;</span>
<span class="plain">(</span><span class="identifier">Kinds::Compare::le</span><span class="plain">(</span><span class="identifier">early_kind</span><span class="plain">, </span><span class="identifier">K</span><span class="plain">))) {</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">);</span>
<span class="identifier">PROPOSITION_EDITED_REPEATING_CURRENT</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">);</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">This code is used in <a href="#SP10">&#167;10</a>.</p>
<p class="inwebparagraph"><a id="SP11"></a><b>&#167;11. Turn binary predicates the right way round (deduction). </b>Recall that BPs are manufactured in pairs, each being the reversal of
the other, in the sense of transposing their terms. Of each pair, one is
considered the canonical way to represent the relation, and is "the right
way round". This routine turns all BPs in the proposition the right way
round, if they aren't already.
</p>
<p class="inwebparagraph">Suppose B is a binary predicate which is marked as the wrong way round,
and R is its reversal. Then we change:
Σ = ... B(t_1, t_2)... --&gt;
Σ' = ... R(t_2, t_1) ...
</p>
<p class="inwebparagraph">(Note that the equality predicate "is" only has one way round, and it's
the right one &mdash; this is the only exception to the rule that BPs come in
pairs &mdash; so equality predicates won't be turned around here, not that it
would matter if they were.)
</p>
<pre class="display">
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="functiontext">Calculus::Simplifications::turn_right_way_round</span><span class="plain">(</span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">prop</span><span class="plain">, </span><span class="reserved">int</span><span class="plain"> *</span><span class="identifier">changed</span><span class="plain">) {</span>
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
<span class="plain">*</span><span class="identifier">changed</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">) {</span>
<span class="reserved">binary_predicate</span><span class="plain"> *</span><span class="identifier">bp</span><span class="plain"> = </span><span class="functiontext">Calculus::Atoms::is_binary_predicate</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">bp</span><span class="plain">) &amp;&amp; (</span><span class="functiontext">BinaryPredicates::is_the_wrong_way_round</span><span class="plain">(</span><span class="identifier">bp</span><span class="plain">))) {</span>
<span class="reserved">pcalc_term</span><span class="plain"> </span><span class="identifier">pt</span><span class="plain"> = </span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[0];</span>
<span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[0] = </span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[1];</span>
<span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[1] = </span><span class="identifier">pt</span><span class="plain">;</span>
<span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">predicate</span><span class="plain"> = </span><span class="identifier">STORE_POINTER_binary_predicate</span><span class="plain">(</span><span class="functiontext">BinaryPredicates::get_reversal</span><span class="plain">(</span><span class="identifier">bp</span><span class="plain">));</span>
<span class="identifier">PROPOSITION_EDITED</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">);</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="reserved">return</span><span class="plain"> </span><span class="identifier">prop</span><span class="plain">;</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">The function Calculus::Simplifications::turn_right_way_round is used in 11/sc (<a href="11-sc.html#SP1_14">&#167;1.14</a>, <a href="11-sc.html#SP2">&#167;2</a>).</p>
<p class="inwebparagraph"><a id="SP12"></a><b>&#167;12. Simplify region containment (fudge). </b>Most of Inform's prepositions are unambiguous, but "in" can mean two quite
different relations. Usually it means (direct) containment, but there is an
alternative interpretation as regional containment. "The diamond is in the
teddy bear" is direct containment, but "The diamond is in Northumberland"
is regional containment. We need to separate out these ideas into two
different binary predicates because direct containment has a function f_D
allowing simplification of many common sentences, but regional containment
allows no such simplification. Basically: you can be directly contained by
only one thing at a time, but might be in many regions at once.
</p>
<p class="inwebparagraph">So far we assume every "in" means the <code class="display"><span class="extract">R_containment</span></code>. This is the
point where we choose to divert some uses to <code class="display"><span class="extract">R_regional_containment</span></code>.
If R is a constant region name, and C_D, C_R are the predicates for
direct and region containment, then
Σ = ... C_D(t, R)... --&gt;
Σ' = ... C_R(t, R)...
Σ = ... C_D(R, t)... --&gt;
Σ' = ... C_R(R, t)...
(Note that a region cannot directly contain any object, except a backdrop.)
</p>
<pre class="display">
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="functiontext">Calculus::Simplifications::region_containment</span><span class="plain">(</span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">prop</span><span class="plain">, </span><span class="reserved">int</span><span class="plain"> *</span><span class="identifier">changed</span><span class="plain">) {</span>
<span class="plain">*</span><span class="identifier">changed</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
<span class="plain">#</span><span class="identifier">ifdef</span><span class="plain"> </span><span class="identifier">IF_MODULE</span>
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">) {</span>
<span class="reserved">binary_predicate</span><span class="plain"> *</span><span class="identifier">bp</span><span class="plain"> = </span><span class="functiontext">Calculus::Atoms::is_binary_predicate</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">bp</span><span class="plain"> == </span><span class="identifier">R_containment</span><span class="plain">) {</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">j</span><span class="plain">;</span>
<span class="reserved">for</span><span class="plain"> (</span><span class="identifier">j</span><span class="plain">=0; </span><span class="identifier">j</span><span class="plain">&lt;2; </span><span class="identifier">j</span><span class="plain">++) {</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">regionality</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">, </span><span class="identifier">backdropping</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">].</span><span class="element">constant</span><span class="plain">) {</span>
<span class="identifier">kind</span><span class="plain"> *</span><span class="identifier">KR</span><span class="plain"> = </span><span class="functiontext">Specifications::to_kind</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">].</span><span class="element">constant</span><span class="plain">);</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">Kinds::Compare::le</span><span class="plain">(</span><span class="identifier">KR</span><span class="plain">, </span><span class="identifier">K_region</span><span class="plain">)) {</span>
<span class="identifier">regionality</span><span class="plain"> = </span><span class="identifier">TRUE</span><span class="plain">;</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[1-</span><span class="identifier">j</span><span class="plain">].</span><span class="element">constant</span><span class="plain">) {</span>
<span class="identifier">kind</span><span class="plain"> *</span><span class="identifier">KB</span><span class="plain"> = </span><span class="functiontext">Specifications::to_kind</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[1-</span><span class="identifier">j</span><span class="plain">].</span><span class="element">constant</span><span class="plain">);</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">Kinds::Compare::le</span><span class="plain">(</span><span class="identifier">KB</span><span class="plain">, </span><span class="identifier">K_backdrop</span><span class="plain">)) </span><span class="identifier">backdropping</span><span class="plain"> = </span><span class="identifier">TRUE</span><span class="plain">;</span>
<span class="plain">}</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">regionality</span><span class="plain">) &amp;&amp; (!</span><span class="identifier">backdropping</span><span class="plain">)) {</span>
<span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">predicate</span><span class="plain"> = </span><span class="identifier">STORE_POINTER_binary_predicate</span><span class="plain">(</span><span class="identifier">R_regional_containment</span><span class="plain">);</span>
<span class="identifier">PROPOSITION_EDITED</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">);</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">#</span><span class="identifier">endif</span>
<span class="reserved">return</span><span class="plain"> </span><span class="identifier">prop</span><span class="plain">;</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">The function Calculus::Simplifications::region_containment is used in 11/sc (<a href="11-sc.html#SP1_14">&#167;1.14</a>, <a href="11-sc.html#SP2">&#167;2</a>).</p>
<p class="inwebparagraph"><a id="SP13"></a><b>&#167;13. Reduce binary predicates (deduction). </b>If we are able to reduce a binary to a unary predicate, we will probably
gain considerably by being able to eliminate a variable altogether. For
instance, suppose we have "Mme Cholet is in a burrow". This will
initially come out as
∃ x: burrow(x)∧ in(<code class="display"><span class="extract">Cholet</span></code>, x)
To test that proposition requires trying all possible burrows x.
But exploiting the fact that Mme Cholet can only be in one place at a
time, we can reduce the binary predicate to equality, thus:
∃ x: burrow(x)∧ is(<code class="display"><span class="extract">ContainerOf(Cholet)</span></code>, x)
A later simplification can then observe that this tells us what x must be,
and eliminate both quantifier and variable.
</p>
<p class="inwebparagraph">Formally, suppose B is a predicate with a function f_B such that B(x, y)
is true if and only y = f_B(x). Then:
Σ = ... B(t_1, t_2) ... --&gt;
Σ' = ... is(f_B(t_1), t_2) ...
Similarly, if there is a function g_B such that B(x, y) if and only if
x = g_B(y) then
Σ = ... B(t_1, t_2) ... --&gt;
Σ' = ... is(t_1, g_B(t_2)) ...
Not all BPs have these: the reason for our fudge on regional containment (above)
is that direct containment does, but region containment doesn't, and this is
why it was necessary to separate the two out.
</p>
<pre class="display">
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="functiontext">Calculus::Simplifications::reduce_predicates</span><span class="plain">(</span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">prop</span><span class="plain">, </span><span class="reserved">int</span><span class="plain"> *</span><span class="identifier">changed</span><span class="plain">) {</span>
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
<span class="plain">*</span><span class="identifier">changed</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">) {</span>
<span class="reserved">binary_predicate</span><span class="plain"> *</span><span class="identifier">bp</span><span class="plain"> = </span><span class="functiontext">Calculus::Atoms::is_binary_predicate</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">bp</span><span class="plain">) {</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">j</span><span class="plain">;</span>
<span class="reserved">for</span><span class="plain"> (</span><span class="identifier">j</span><span class="plain">=0; </span><span class="identifier">j</span><span class="plain">&lt;2; </span><span class="identifier">j</span><span class="plain">++)</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="functiontext">BinaryPredicates::get_term_as_function_of_other</span><span class="plain">(</span><span class="identifier">bp</span><span class="plain">, </span><span class="identifier">j</span><span class="plain">)) &amp;&amp;</span>
<span class="plain">(</span><span class="functiontext">BinaryPredicates::allows_function_simplification</span><span class="plain">(</span><span class="identifier">bp</span><span class="plain">))) {</span>
<span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[1-</span><span class="identifier">j</span><span class="plain">] = </span><span class="functiontext">Calculus::Terms::new_function</span><span class="plain">(</span><span class="identifier">bp</span><span class="plain">, </span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[1-</span><span class="identifier">j</span><span class="plain">], </span><span class="constant">1</span><span class="plain">-</span><span class="identifier">j</span><span class="plain">);</span>
<span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">predicate</span><span class="plain"> = </span><span class="identifier">STORE_POINTER_binary_predicate</span><span class="plain">(</span><span class="identifier">R_equality</span><span class="plain">);</span>
<span class="identifier">PROPOSITION_EDITED</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">);</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="reserved">return</span><span class="plain"> </span><span class="identifier">prop</span><span class="plain">;</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">The function Calculus::Simplifications::reduce_predicates is used in 11/sc (<a href="11-sc.html#SP1_14">&#167;1.14</a>, <a href="11-sc.html#SP2">&#167;2</a>).</p>
<p class="inwebparagraph"><a id="SP14"></a><b>&#167;14. Eliminating determined variables (deduction). </b>The above operations will try to get as many variables as possible into a
form which makes their values explicit with a predicate is(v, t).
We detect such equations and use them to eliminate the variable concerned,
where this is safe.
</p>
<pre class="definitions">
<span class="definitionkeyword">define</span> <span class="constant">NOT_BOUND_AT_ALL</span><span class="plain"> </span><span class="constant">1</span>
<span class="definitionkeyword">define</span> <span class="constant">BOUND_BY_EXISTS</span><span class="plain"> </span><span class="constant">2</span>
<span class="definitionkeyword">define</span> <span class="constant">BOUND_BY_SOMETHING_ELSE</span><span class="plain"> </span><span class="constant">3</span>
</pre>
<pre class="display">
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="functiontext">Calculus::Simplifications::eliminate_redundant_variables</span><span class="plain">(</span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">prop</span><span class="plain">, </span><span class="reserved">int</span><span class="plain"> *</span><span class="identifier">changed</span><span class="plain">) {</span>
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">level</span><span class="plain">, </span><span class="identifier">binding_status</span><span class="plain">[26], </span><span class="identifier">binding_level</span><span class="plain">[26], </span><span class="identifier">binding_sequence</span><span class="plain">[26];</span>
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">position_of_binding</span><span class="plain">[26];</span>
<span class="plain">*</span><span class="identifier">changed</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
<span class="identifier">EliminateVariables:</span>
&lt;<span class="cwebmacro">Find out where and how variables are bound</span> <span class="cwebmacronumber">14.1</span>&gt;<span class="plain">;</span>
<span class="identifier">level</span><span class="plain"> = </span><span class="constant">0</span><span class="plain">;</span>
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">) {</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::element_get_group</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">element</span><span class="plain">) == </span><span class="constant">OPEN_OPERATORS_GROUP</span><span class="plain">) </span><span class="identifier">level</span><span class="plain">++;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::element_get_group</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">element</span><span class="plain">) == </span><span class="constant">CLOSE_OPERATORS_GROUP</span><span class="plain">) </span><span class="identifier">level</span><span class="plain">--;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::is_equality_predicate</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">)) {</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">j</span><span class="plain">;</span>
<span class="reserved">for</span><span class="plain"> (</span><span class="identifier">j</span><span class="plain">=1; </span><span class="identifier">j</span><span class="plain">&gt;=0; </span><span class="identifier">j</span><span class="plain">--) {</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">var_to_sub</span><span class="plain"> = </span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">].</span><span class="element">variable</span><span class="plain">;</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">var_in_other_term</span><span class="plain"> = </span><span class="functiontext">Calculus::Terms::variable_underlying</span><span class="plain">(&amp;(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[1-</span><span class="identifier">j</span><span class="plain">]));</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">var_is_redundant</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">, </span><span class="identifier">value_can_be_subbed</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
&lt;<span class="cwebmacro">Decide if the variable is redundant, and if its value can safely be subbed</span> <span class="cwebmacronumber">14.2</span>&gt;<span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">var_is_redundant</span><span class="plain">) &amp;&amp; (</span><span class="identifier">value_can_be_subbed</span><span class="plain">)) {</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">permitted</span><span class="plain">;</span>
<span class="functiontext">Calculus::Variables::substitute_term</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">var_to_sub</span><span class="plain">, </span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[1-</span><span class="identifier">j</span><span class="plain">],</span>
<span class="identifier">TRUE</span><span class="plain">, &amp;</span><span class="identifier">permitted</span><span class="plain">, </span><span class="identifier">changed</span><span class="plain">);</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">permitted</span><span class="plain">) {</span>
<span class="identifier">LOGIF</span><span class="plain">(</span><span class="identifier">PREDICATE_CALCULUS_WORKINGS</span><span class="plain">, </span><span class="string">"Substituting %c &lt;-- $0\n"</span><span class="plain">,</span>
<span class="identifier">pcalc_vars</span><span class="plain">[</span><span class="identifier">var_to_sub</span><span class="plain">], &amp;(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[1-</span><span class="identifier">j</span><span class="plain">]));</span>
<span class="comment">first delete the is(v, t) predicate</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">);</span>
<span class="comment">then unbind the variable, by deleting its ∃ v quantifier</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">position_of_binding</span><span class="plain">[</span><span class="identifier">var_to_sub</span><span class="plain">]);</span>
<span class="identifier">LOGIF</span><span class="plain">(</span><span class="identifier">PREDICATE_CALCULUS_WORKINGS</span><span class="plain">, </span><span class="string">"After deletion: $D\n"</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">);</span>
<span class="identifier">binding_status</span><span class="plain">[</span><span class="identifier">var_to_sub</span><span class="plain">] = </span><span class="constant">NOT_BOUND_AT_ALL</span><span class="plain">;</span>
<span class="comment">then substitute for all other occurrences of v</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Variables::substitute_term</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">var_to_sub</span><span class="plain">, </span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[1-</span><span class="identifier">j</span><span class="plain">],</span>
<span class="identifier">FALSE</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">, </span><span class="identifier">changed</span><span class="plain">);</span>
<span class="plain">*</span><span class="identifier">changed</span><span class="plain"> = </span><span class="identifier">TRUE</span><span class="plain">;</span>
<span class="comment">since the proposition is now shorter by 2 atoms, this loop terminates</span>
<span class="reserved">goto</span><span class="plain"> </span><span class="identifier">EliminateVariables</span><span class="plain">;</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="functiontext">Calculus::Variables::renumber</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">); </span><span class="comment">for the sake of tidiness</span>
<span class="reserved">return</span><span class="plain"> </span><span class="identifier">prop</span><span class="plain">;</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">The function Calculus::Simplifications::eliminate_redundant_variables is used in 11/sc (<a href="11-sc.html#SP1_14">&#167;1.14</a>, <a href="11-sc.html#SP2">&#167;2</a>).</p>
<p class="inwebparagraph"><a id="SP14_1"></a><b>&#167;14.1. </b>The information-gathering stage:
</p>
<p class="macrodefinition"><code class="display">
&lt;<span class="cwebmacrodefn">Find out where and how variables are bound</span> <span class="cwebmacronumber">14.1</span>&gt; =
</code></p>
<pre class="displaydefn">
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">j</span><span class="plain">, </span><span class="identifier">c</span><span class="plain"> = </span><span class="constant">0</span><span class="plain">, </span><span class="identifier">level</span><span class="plain"> = </span><span class="constant">0</span><span class="plain">;</span>
<span class="reserved">for</span><span class="plain"> (</span><span class="identifier">j</span><span class="plain">=0; </span><span class="identifier">j</span><span class="plain">&lt;26; </span><span class="identifier">j</span><span class="plain">++) {</span>
<span class="identifier">binding_status</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">] = </span><span class="constant">NOT_BOUND_AT_ALL</span><span class="plain">;</span>
<span class="identifier">binding_level</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">] = </span><span class="constant">0</span><span class="plain">; </span><span class="identifier">binding_sequence</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">] = </span><span class="constant">0</span><span class="plain">; </span><span class="identifier">position_of_binding</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">] = </span><span class="identifier">NULL</span><span class="plain">;</span>
<span class="plain">}</span>
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">) {</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::element_get_group</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">element</span><span class="plain">) == </span><span class="constant">OPEN_OPERATORS_GROUP</span><span class="plain">) </span><span class="identifier">level</span><span class="plain">++;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::element_get_group</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">element</span><span class="plain">) == </span><span class="constant">CLOSE_OPERATORS_GROUP</span><span class="plain">) </span><span class="identifier">level</span><span class="plain">--;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::is_quantifier</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">)) {</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">v</span><span class="plain"> = </span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[0].</span><span class="element">variable</span><span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::is_existence_quantifier</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">)) </span><span class="identifier">binding_status</span><span class="plain">[</span><span class="identifier">v</span><span class="plain">] = </span><span class="constant">BOUND_BY_EXISTS</span><span class="plain">;</span>
<span class="reserved">else</span><span class="plain"> </span><span class="identifier">binding_status</span><span class="plain">[</span><span class="identifier">v</span><span class="plain">] = </span><span class="constant">BOUND_BY_SOMETHING_ELSE</span><span class="plain">;</span>
<span class="identifier">binding_level</span><span class="plain">[</span><span class="identifier">v</span><span class="plain">] = </span><span class="identifier">level</span><span class="plain">;</span>
<span class="identifier">binding_sequence</span><span class="plain">[</span><span class="identifier">v</span><span class="plain">] = </span><span class="identifier">c</span><span class="plain">;</span>
<span class="identifier">position_of_binding</span><span class="plain">[</span><span class="identifier">v</span><span class="plain">] = </span><span class="identifier">pl_prev</span><span class="plain">;</span>
<span class="plain">}</span>
<span class="identifier">c</span><span class="plain">++;</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">This code is used in <a href="#SP14">&#167;14</a>.</p>
<p class="inwebparagraph"><a id="SP14_2"></a><b>&#167;14.2. </b>At this point we have a predicate is(t, f_A(f_B(... s))). Should
the term t be a variable v, which is bound by an ∃ v atom at the
same level in its subexpression, then we can consider eliminating v by
substituting v = f_A(f_B(... s)).
</p>
<p class="inwebparagraph">But only if the term s underneath those functions does not make the equation
is(v, f_A(f_B(... s))) implicit. Suppose s depends
on a variable w which is bound and occurs after the binding of v.
The value of such a variable w can depend on the value of v. Saying that
v=s may therefore not determine a unique value of v at all: it may be
a subtle condition passed by a whole class of possible values, or none.
</p>
<p class="inwebparagraph">The simplest example of such circularity is is(v, v), true for all v.
More problematic is is(v, f_C(v)), "v is the container of v",
which is never true. Still worse is
∃ v: V_{=2} w: is(v, w)
which literally says there is a value of v equal to two different things &mdash;
certainly false. But if we were allowed to eliminate v, we would get just
V_{=2} w
which asserts "there are exactly two objects" &mdash; which is certainly not a
valid deduction, and might even be true.
</p>
<p class="inwebparagraph">Here <code class="display"><span class="extract">var_to_sub</span></code> is v and <code class="display"><span class="extract">var_in_other_term</span></code> is w, or else they are -1
if no variables are present in their respective terms.
</p>
<p class="macrodefinition"><code class="display">
&lt;<span class="cwebmacrodefn">Decide if the variable is redundant, and if its value can safely be subbed</span> <span class="cwebmacronumber">14.2</span>&gt; =
</code></p>
<pre class="displaydefn">
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">var_to_sub</span><span class="plain"> &gt;= </span><span class="constant">0</span><span class="plain">)</span>
<span class="plain">&amp;&amp; (</span><span class="identifier">binding_status</span><span class="plain">[</span><span class="identifier">var_to_sub</span><span class="plain">] == </span><span class="constant">BOUND_BY_EXISTS</span><span class="plain">)</span>
<span class="plain">&amp;&amp; (</span><span class="identifier">binding_level</span><span class="plain">[</span><span class="identifier">var_to_sub</span><span class="plain">] == </span><span class="identifier">level</span><span class="plain">))</span>
<span class="identifier">var_is_redundant</span><span class="plain"> = </span><span class="identifier">TRUE</span><span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">var_in_other_term</span><span class="plain"> &lt; </span><span class="constant">0</span><span class="plain">)</span>
<span class="plain">|| (</span><span class="identifier">binding_status</span><span class="plain">[</span><span class="identifier">var_in_other_term</span><span class="plain">] == </span><span class="constant">NOT_BOUND_AT_ALL</span><span class="plain">)</span>
<span class="plain">|| (</span><span class="identifier">binding_sequence</span><span class="plain">[</span><span class="identifier">var_in_other_term</span><span class="plain">] &lt; </span><span class="identifier">binding_sequence</span><span class="plain">[</span><span class="identifier">var_to_sub</span><span class="plain">]))</span>
<span class="identifier">value_can_be_subbed</span><span class="plain"> = </span><span class="identifier">TRUE</span><span class="plain">;</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">This code is used in <a href="#SP14">&#167;14</a>.</p>
<p class="inwebparagraph"><a id="SP15"></a><b>&#167;15. Simplify non-relation (deduction). </b>As a result of the previous simplifications, it fairly often happens that we
find a term like
¬(thing(t<code class="display"><span class="extract">.component_parent</span></code>))
in the proposition. This comes out of text such as "... not part of something",
asserting first that there is no y such that t is a part of y, and then
simplifying to remove the y variable. A term like the one above is then
left behind. But the negation is cumbersome, and makes the proposition harder
to assert or test. Exploiting the fact that <code class="display"><span class="extract">component_parent</span></code> is a property
which is either the part-parent or else <code class="display"><span class="extract">nothing</span></code>, we can simplify to:
is(t<code class="display"><span class="extract">.component_parent</span></code>, <code class="display"><span class="extract">nothing</span></code>)
And similar tricks can be pulled for other various-to-one-object predicates.
</p>
<p class="inwebparagraph">Formally, let B be a binary predicate supporting either a function f_B
such that B(x, y) iff f_B(x) = y, or else such that B(x, y) iff f_B(y) = x;
and such that the values of f_B are objects. Let K be a kind of object.
Then:
Σ = ... ¬( K(f_B(t))) ... --&gt;
Σ' = ... is(f_B(t), <code class="display"><span class="extract">nothing</span></code>) ...
</p>
<p class="inwebparagraph">A similar trick for kinds of value is not possible, because &mdash; unlike objects &mdash;
they have no "not a valid case" value analogous to the non-object <code class="display"><span class="extract">nothing</span></code>.
</p>
<pre class="display">
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="functiontext">Calculus::Simplifications::not_related_to_something</span><span class="plain">(</span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">prop</span><span class="plain">, </span><span class="reserved">int</span><span class="plain"> *</span><span class="identifier">changed</span><span class="plain">) {</span>
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
<span class="plain">*</span><span class="identifier">changed</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">) {</span>
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">kind_atom</span><span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Propositions::match</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="constant">3</span><span class="plain">,</span>
<span class="constant">NEGATION_OPEN_ATOM</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">,</span>
<span class="constant">KIND_ATOM</span><span class="plain">, &amp;</span><span class="identifier">kind_atom</span><span class="plain">,</span>
<span class="constant">NEGATION_CLOSE_ATOM</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">)) {</span>
<span class="identifier">kind</span><span class="plain"> *</span><span class="identifier">K</span><span class="plain"> = </span><span class="identifier">kind_atom</span><span class="plain">-&gt;</span><span class="element">assert_kind</span><span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">Kinds::Compare::lt</span><span class="plain">(</span><span class="identifier">K</span><span class="plain">, </span><span class="identifier">K_object</span><span class="plain">)) {</span>
<span class="reserved">binary_predicate</span><span class="plain"> *</span><span class="identifier">bp</span><span class="plain"> = </span><span class="identifier">NULL</span><span class="plain">;</span>
<span class="reserved">pcalc_term</span><span class="plain"> </span><span class="identifier">KIND_term</span><span class="plain"> = </span><span class="identifier">kind_atom</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[0];</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">KIND_term</span><span class="plain">.</span><span class="element">function</span><span class="plain">) </span><span class="identifier">bp</span><span class="plain"> = </span><span class="identifier">KIND_term</span><span class="plain">.</span><span class="element">function</span><span class="plain">-&gt;</span><span class="element">bp</span><span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">bp</span><span class="plain">) &amp;&amp; (</span><span class="identifier">Kinds::Compare::eq</span><span class="plain">(</span><span class="identifier">K</span><span class="plain">, </span><span class="functiontext">BinaryPredicates::term_kind</span><span class="plain">(</span><span class="identifier">bp</span><span class="plain">, </span><span class="constant">1</span><span class="plain">)))) {</span>
<span class="identifier">parse_node</span><span class="plain"> *</span><span class="identifier">new_nothing</span><span class="plain"> =</span>
<span class="functiontext">Lvalues::new_actual_NONLOCAL_VARIABLE</span><span class="plain">(</span><span class="identifier">i6_nothing_VAR</span><span class="plain">);</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::ungroup_after</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">); </span><span class="comment">remove negation grouping</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">); </span><span class="comment">remove <code class="display"><span class="extract">KIND_ATOM</span></code></span>
<span class="comment">now insert equality predicate:</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::insert_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">,</span>
<span class="functiontext">Calculus::Atoms::binary_PREDICATE_new</span><span class="plain">(</span><span class="identifier">R_equality</span><span class="plain">,</span>
<span class="identifier">KIND_term</span><span class="plain">, </span><span class="functiontext">Calculus::Terms::new_constant</span><span class="plain">(</span><span class="identifier">new_nothing</span><span class="plain">)));</span>
<span class="identifier">PROPOSITION_EDITED</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">);</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="reserved">return</span><span class="plain"> </span><span class="identifier">prop</span><span class="plain">;</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">The function Calculus::Simplifications::not_related_to_something is used in 11/sc (<a href="11-sc.html#SP1_14">&#167;1.14</a>, <a href="11-sc.html#SP2">&#167;2</a>).</p>
<p class="inwebparagraph"><a id="SP16"></a><b>&#167;16. Convert gerunds to nouns (deduction). </b>Suppose we write:
</p>
<blockquote>
<p>The funky thing to do is a stored action that varies.</p>
</blockquote>
<p class="inwebparagraph">and subsequently:
</p>
<blockquote>
<p>the funky thing to do is waiting</p>
</blockquote>
<p class="inwebparagraph">Here "waiting" is a gerund, and although it describes an action it is a
noun (thus a value) rather than a condition. We coerce its constant value
accordingly.
</p>
<pre class="display">
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="functiontext">Calculus::Simplifications::convert_gerunds</span><span class="plain">(</span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">prop</span><span class="plain">, </span><span class="reserved">int</span><span class="plain"> *</span><span class="identifier">changed</span><span class="plain">) {</span>
<span class="plain">*</span><span class="identifier">changed</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">)</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">element</span><span class="plain"> == </span><span class="constant">PREDICATE_ATOM</span><span class="plain">) &amp;&amp; (</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">arity</span><span class="plain"> == </span><span class="constant">2</span><span class="plain">))</span>
<span class="reserved">for</span><span class="plain"> (</span><span class="reserved">int</span><span class="plain"> </span><span class="identifier">i</span><span class="plain">=0; </span><span class="identifier">i</span><span class="plain">&lt;2; </span><span class="identifier">i</span><span class="plain">++)</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Conditions::is_TEST_ACTION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[</span><span class="identifier">i</span><span class="plain">].</span><span class="element">constant</span><span class="plain">))</span>
<span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[</span><span class="identifier">i</span><span class="plain">].</span><span class="element">constant</span><span class="plain"> = </span><span class="functiontext">Conditions::action_tested</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[</span><span class="identifier">i</span><span class="plain">].</span><span class="element">constant</span><span class="plain">);</span>
<span class="reserved">return</span><span class="plain"> </span><span class="identifier">prop</span><span class="plain">;</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">The function Calculus::Simplifications::convert_gerunds is used in 11/sc (<a href="11-sc.html#SP1_14">&#167;1.14</a>, <a href="11-sc.html#SP2">&#167;2</a>).</p>
<p class="inwebparagraph"><a id="SP17"></a><b>&#167;17. Eliminate to have meaning property ownership (fudge). </b>The verb "to have" normally means ownership of a physical thing, but it
can also arise from text such as
</p>
<blockquote>
<p>the balloon has weight at most 1</p>
</blockquote>
<p class="inwebparagraph">where it's the numerical "weight" property which is owned by the balloon.
(The language of abstract "property" always echoes that of real physical
things &mdash; consider how the iTunes Music Store invites you to "buy" what
is at best a lease of temporary, partial and revocable rights to make use
of something with no physical essence. This isn't a con trick, or not
altogether so. We like the word "buy"; we immediately understand it.)
At this stage of simplification, the above has produced
{at-most}(<code class="display"><span class="extract">weight</span></code>, 1)∧ is(<code class="display"><span class="extract">balloon</span></code>, f_H(<code class="display"><span class="extract">weight</span></code>))
where H is the predicate <code class="display"><span class="extract">a_has_b_predicate</span></code>. As it stands, this
proposition will fail type-checking, because it contains an implicit
free variable &mdash; the object which owns the weight. We make this explicit
by removing is(<code class="display"><span class="extract">balloon</span></code>, f_H(<code class="display"><span class="extract">weight</span></code>)) and replacing all other
references to <code class="display"><span class="extract">weight</span></code> with "the weight of <code class="display"><span class="extract">balloon</span></code>".
</p>
<p class="inwebparagraph">This is a fudge because it assumes &mdash; possibly wrongly &mdash; that all
references to the weight are to the weight of the same thing. In
sufficiently contrived sentences, this wouldn't be true.
</p>
<pre class="display">
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="functiontext">Calculus::Simplifications::eliminate_to_have</span><span class="plain">(</span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">prop</span><span class="plain">, </span><span class="reserved">int</span><span class="plain"> *</span><span class="identifier">changed</span><span class="plain">) {</span>
<span class="plain">*</span><span class="identifier">changed</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">) {</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::is_equality_predicate</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">)) {</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">i</span><span class="plain">;</span>
<span class="reserved">for</span><span class="plain"> (</span><span class="identifier">i</span><span class="plain">=0; </span><span class="identifier">i</span><span class="plain">&lt;2; </span><span class="identifier">i</span><span class="plain">++)</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[</span><span class="identifier">i</span><span class="plain">].</span><span class="element">function</span><span class="plain">) &amp;&amp;</span>
<span class="plain">(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[</span><span class="identifier">i</span><span class="plain">].</span><span class="element">function</span><span class="plain">-&gt;</span><span class="element">bp</span><span class="plain"> == </span><span class="identifier">a_has_b_predicate</span><span class="plain">) &amp;&amp;</span>
<span class="plain">(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[</span><span class="identifier">i</span><span class="plain">].</span><span class="element">function</span><span class="plain">-&gt;</span><span class="element">fn_of</span><span class="plain">.</span><span class="element">constant</span><span class="plain">) &amp;&amp; (</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[1-</span><span class="identifier">i</span><span class="plain">].</span><span class="element">constant</span><span class="plain">)) {</span>
<span class="identifier">parse_node</span><span class="plain"> *</span><span class="identifier">spec</span><span class="plain"> = </span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[</span><span class="identifier">i</span><span class="plain">].</span><span class="element">function</span><span class="plain">-&gt;</span><span class="element">fn_of</span><span class="plain">.</span><span class="element">constant</span><span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Rvalues::is_CONSTANT_construction</span><span class="plain">(</span><span class="identifier">spec</span><span class="plain">, </span><span class="identifier">CON_property</span><span class="plain">))</span>
&lt;<span class="cwebmacro">Found an indication of who owns a property</span> <span class="cwebmacronumber">17.1</span>&gt;<span class="plain">;</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="reserved">return</span><span class="plain"> </span><span class="identifier">prop</span><span class="plain">;</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">The function Calculus::Simplifications::eliminate_to_have is used in 11/sc (<a href="11-sc.html#SP1_14">&#167;1.14</a>, <a href="11-sc.html#SP2">&#167;2</a>).</p>
<p class="inwebparagraph"><a id="SP17_1"></a><b>&#167;17.1. </b>So the current atom is is(f_H(P), C) or is(C, f_H(P))
(according to whether i is 0 or 1), for a property P and a constant
term C.
</p>
<p class="macrodefinition"><code class="display">
&lt;<span class="cwebmacrodefn">Found an indication of who owns a property</span> <span class="cwebmacronumber">17.1</span>&gt; =
</code></p>
<pre class="displaydefn">
<span class="reserved">property</span><span class="plain"> *</span><span class="identifier">prn</span><span class="plain"> = </span><span class="functiontext">Rvalues::to_property</span><span class="plain">(</span><span class="identifier">spec</span><span class="plain">);</span>
<span class="identifier">parse_node</span><span class="plain"> *</span><span class="identifier">po_spec</span><span class="plain"> =</span>
<span class="functiontext">Lvalues::new_PROPERTY_VALUE</span><span class="plain">(</span><span class="identifier">spec</span><span class="plain">, </span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[1-</span><span class="identifier">i</span><span class="plain">].</span><span class="element">constant</span><span class="plain">);</span>
<span class="identifier">ParseTree::set_text</span><span class="plain">(</span><span class="identifier">po_spec</span><span class="plain">, </span><span class="identifier">prn</span><span class="plain">-&gt;</span><span class="element">name</span><span class="plain">);</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">no_substitutions_made</span><span class="plain">;</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Simplifications::prop_substitute_prop_cons</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">prn</span><span class="plain">, </span><span class="identifier">po_spec</span><span class="plain">, &amp;</span><span class="identifier">no_substitutions_made</span><span class="plain">, </span><span class="identifier">pl</span><span class="plain">);</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">no_substitutions_made</span><span class="plain"> &gt; </span><span class="constant">0</span><span class="plain">) {</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">);</span>
<span class="identifier">PROPOSITION_EDITED_REPEATING_CURRENT</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">);</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">This code is used in <a href="#SP17">&#167;17</a>.</p>
<p class="inwebparagraph"><a id="SP18"></a><b>&#167;18. </b>Here we make the necessary substitution of "P" with "the P of C",
where P is a property and C the constant value of its owner. We make
this to every occurrence throughout the proposition, except for the one
in the original is(f_H(P), C) atom, and we count the number of
changes made.
</p>
<pre class="display">
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="functiontext">Calculus::Simplifications::prop_substitute_prop_cons</span><span class="plain">(</span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">prop</span><span class="plain">, </span><span class="reserved">property</span><span class="plain"> *</span><span class="identifier">prn</span><span class="plain">,</span>
<span class="identifier">parse_node</span><span class="plain"> *</span><span class="identifier">po_spec</span><span class="plain">, </span><span class="reserved">int</span><span class="plain"> *</span><span class="identifier">count</span><span class="plain">, </span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">not_this</span><span class="plain">) {</span>
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">j</span><span class="plain">, </span><span class="identifier">c</span><span class="plain"> = </span><span class="constant">0</span><span class="plain">;</span>
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">)</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">pl</span><span class="plain"> != </span><span class="identifier">not_this</span><span class="plain">)</span>
<span class="reserved">for</span><span class="plain"> (</span><span class="identifier">j</span><span class="plain">=0; </span><span class="identifier">j</span><span class="plain">&lt;</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">arity</span><span class="plain">; </span><span class="identifier">j</span><span class="plain">++) {</span>
<span class="reserved">pcalc_term</span><span class="plain"> *</span><span class="identifier">pt</span><span class="plain"> = &amp;(</span><span class="identifier">pl</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">]);</span>
<span class="reserved">while</span><span class="plain"> (</span><span class="identifier">pt</span><span class="plain">-&gt;</span><span class="identifier">function</span><span class="plain">) </span><span class="identifier">pt</span><span class="plain"> = &amp;(</span><span class="identifier">pt</span><span class="plain">-&gt;</span><span class="element">function</span><span class="plain">-&gt;</span><span class="element">fn_of</span><span class="plain">);</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">pt</span><span class="plain">-&gt;</span><span class="element">constant</span><span class="plain"> == </span><span class="identifier">NULL</span><span class="plain">) </span><span class="reserved">continue</span><span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Rvalues::is_CONSTANT_construction</span><span class="plain">(</span><span class="identifier">pt</span><span class="plain">-&gt;</span><span class="element">constant</span><span class="plain">, </span><span class="identifier">CON_property</span><span class="plain">)) {</span>
<span class="reserved">property</span><span class="plain"> *</span><span class="identifier">tprn</span><span class="plain">;</span>
<span class="identifier">tprn</span><span class="plain"> = </span><span class="functiontext">Rvalues::to_property</span><span class="plain">(</span><span class="identifier">pt</span><span class="plain">-&gt;</span><span class="element">constant</span><span class="plain">);</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">tprn</span><span class="plain"> == </span><span class="identifier">prn</span><span class="plain">) {</span>
<span class="identifier">pt</span><span class="plain">-&gt;</span><span class="element">constant</span><span class="plain"> = </span><span class="identifier">po_spec</span><span class="plain">;</span>
<span class="identifier">c</span><span class="plain">++;</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">*</span><span class="identifier">count</span><span class="plain"> = </span><span class="identifier">c</span><span class="plain">;</span>
<span class="reserved">return</span><span class="plain"> </span><span class="identifier">prop</span><span class="plain">;</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">The function Calculus::Simplifications::prop_substitute_prop_cons is used in <a href="#SP17_1">&#167;17.1</a>.</p>
<p class="inwebparagraph"><a id="SP19"></a><b>&#167;19. Turn all rooms to everywhere (fudge). </b>This rather special rule handles the consequences of the English word
"everywhere". Inform reads that as "all rooms", literally "every where",
which is logical but loses the connotation of place &mdash; by "everywhere", we
usually mean "in all rooms", so that the sentence
</p>
<blockquote>
<p>The sky is everywhere.</p>
</blockquote>
<p class="inwebparagraph">means the sky is in every room, not that the sky is equal to every room.
Since the literal reading would make no useful sense, Inform fudges the
proposition to change it to the idiomatic one.
Σ = ... ∀ v∈{ v|room(v)}} : is(v, t) --&gt;
Σ' = ... everywhere(t)
Σ = ... ∀ v∈{ v|room(v)}} : is(t, v) --&gt;
Σ' = ... everywhere(t)
Σ = ... ¬∀ v∈{ v|room(v)}} : is(v, t) --&gt;
Σ' = ... ¬(everywhere(t))
Σ = ... ¬∀ v∈{ v|room(v)}} : is(t, v) --&gt;
Σ' = ... ¬(everywhere(t))
</p>
<p class="inwebparagraph">Note that we match this only at the end of a proposition, where v can
have no other consequence.
</p>
<pre class="display">
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="functiontext">Calculus::Simplifications::is_all_rooms</span><span class="plain">(</span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">prop</span><span class="plain">, </span><span class="reserved">int</span><span class="plain"> *</span><span class="identifier">changed</span><span class="plain">) {</span>
<span class="plain">*</span><span class="identifier">changed</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
<span class="reserved">return</span><span class="plain"> </span><span class="identifier">prop</span><span class="plain">;</span>
<span class="plain">#</span><span class="identifier">ifdef</span><span class="plain"> </span><span class="identifier">IF_MODULE</span>
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">) {</span>
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">q_atom</span><span class="plain">, *</span><span class="identifier">k_atom</span><span class="plain">, *</span><span class="identifier">bp_atom</span><span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="functiontext">Calculus::Propositions::match</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="constant">6</span><span class="plain">,</span>
<span class="constant">QUANTIFIER_ATOM</span><span class="plain">, &amp;</span><span class="identifier">q_atom</span><span class="plain">,</span>
<span class="constant">DOMAIN_OPEN_ATOM</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">,</span>
<span class="constant">KIND_ATOM</span><span class="plain">, &amp;</span><span class="identifier">k_atom</span><span class="plain">,</span>
<span class="constant">DOMAIN_CLOSE_ATOM</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">,</span>
<span class="constant">PREDICATE_ATOM</span><span class="plain">, &amp;</span><span class="identifier">bp_atom</span><span class="plain">,</span>
<span class="constant">END_PROP_HERE</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">)) &amp;&amp;</span>
<span class="plain">((</span><span class="functiontext">Calculus::Atoms::is_forall_quantifier</span><span class="plain">(</span><span class="identifier">q_atom</span><span class="plain">)) || (</span><span class="functiontext">Calculus::Atoms::is_notall_quantifier</span><span class="plain">(</span><span class="identifier">q_atom</span><span class="plain">))) &amp;&amp;</span>
<span class="plain">(</span><span class="identifier">Kinds::Compare::eq</span><span class="plain">(</span><span class="identifier">k_atom</span><span class="plain">-&gt;</span><span class="element">assert_kind</span><span class="plain">, </span><span class="identifier">K_room</span><span class="plain">)) &amp;&amp;</span>
<span class="plain">(</span><span class="identifier">bp_atom</span><span class="plain">-&gt;</span><span class="identifier">arity</span><span class="plain"> == </span><span class="constant">2</span><span class="plain">) &amp;&amp;</span>
<span class="plain">(</span><span class="identifier">RETRIEVE_POINTER_binary_predicate</span><span class="plain">(</span><span class="identifier">bp_atom</span><span class="plain">-&gt;</span><span class="element">predicate</span><span class="plain">) == </span><span class="identifier">R_equality</span><span class="plain">)) {</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">j</span><span class="plain">, </span><span class="identifier">v</span><span class="plain"> = </span><span class="identifier">k_atom</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[0].</span><span class="element">variable</span><span class="plain">;</span>
<span class="reserved">for</span><span class="plain"> (</span><span class="identifier">j</span><span class="plain">=0; </span><span class="identifier">j</span><span class="plain">&lt;2; </span><span class="identifier">j</span><span class="plain">++) {</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">bp_atom</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[1-</span><span class="identifier">j</span><span class="plain">].</span><span class="element">variable</span><span class="plain"> == </span><span class="identifier">v</span><span class="plain">) &amp;&amp; (</span><span class="identifier">v</span><span class="plain"> &gt;= </span><span class="constant">0</span><span class="plain">)) {</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">); </span><span class="comment">remove <code class="display"><span class="extract">QUANTIFIER_ATOM</span></code></span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">); </span><span class="comment">remove <code class="display"><span class="extract">DOMAIN_OPEN_ATOM</span></code></span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">); </span><span class="comment">remove <code class="display"><span class="extract">KIND_ATOM</span></code></span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">); </span><span class="comment">remove <code class="display"><span class="extract">DOMAIN_CLOSE_ATOM</span></code></span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">); </span><span class="comment">remove <code class="display"><span class="extract">PREDICATE_ATOM</span></code></span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::is_notall_quantifier</span><span class="plain">(</span><span class="identifier">q_atom</span><span class="plain">))</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::insert_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">, </span><span class="functiontext">Calculus::Atoms::new</span><span class="plain">(</span><span class="constant">NEGATION_CLOSE_ATOM</span><span class="plain">));</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::insert_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">,</span>
<span class="functiontext">Calculus::Atoms::EVERYWHERE_new</span><span class="plain">(</span><span class="identifier">bp_atom</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">]));</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::is_notall_quantifier</span><span class="plain">(</span><span class="identifier">q_atom</span><span class="plain">))</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::insert_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">, </span><span class="functiontext">Calculus::Atoms::new</span><span class="plain">(</span><span class="constant">NEGATION_OPEN_ATOM</span><span class="plain">));</span>
<span class="identifier">PROPOSITION_EDITED</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">);</span>
<span class="reserved">break</span><span class="plain">;</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="functiontext">Calculus::Propositions::match</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="constant">6</span><span class="plain">,</span>
<span class="constant">QUANTIFIER_ATOM</span><span class="plain">, &amp;</span><span class="identifier">q_atom</span><span class="plain">,</span>
<span class="constant">DOMAIN_OPEN_ATOM</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">,</span>
<span class="constant">KIND_ATOM</span><span class="plain">, &amp;</span><span class="identifier">k_atom</span><span class="plain">,</span>
<span class="constant">DOMAIN_CLOSE_ATOM</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">,</span>
<span class="constant">PREDICATE_ATOM</span><span class="plain">, &amp;</span><span class="identifier">bp_atom</span><span class="plain">,</span>
<span class="constant">END_PROP_HERE</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">)) &amp;&amp;</span>
<span class="plain">(</span><span class="functiontext">Calculus::Atoms::is_nonexistence_quantifier</span><span class="plain">(</span><span class="identifier">q_atom</span><span class="plain">)) &amp;&amp;</span>
<span class="plain">(</span><span class="identifier">Kinds::Compare::eq</span><span class="plain">(</span><span class="identifier">k_atom</span><span class="plain">-&gt;</span><span class="element">assert_kind</span><span class="plain">, </span><span class="identifier">K_room</span><span class="plain">)) &amp;&amp;</span>
<span class="plain">(</span><span class="functiontext">Calculus::Atoms::is_composited</span><span class="plain">(</span><span class="identifier">k_atom</span><span class="plain">)) &amp;&amp;</span>
<span class="plain">(</span><span class="identifier">bp_atom</span><span class="plain">-&gt;</span><span class="identifier">arity</span><span class="plain"> == </span><span class="constant">2</span><span class="plain">) &amp;&amp;</span>
<span class="plain">(</span><span class="identifier">RETRIEVE_POINTER_binary_predicate</span><span class="plain">(</span><span class="identifier">bp_atom</span><span class="plain">-&gt;</span><span class="element">predicate</span><span class="plain">) == </span><span class="identifier">R_equality</span><span class="plain">)) {</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">j</span><span class="plain">, </span><span class="identifier">v</span><span class="plain"> = </span><span class="identifier">k_atom</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[0].</span><span class="element">variable</span><span class="plain">;</span>
<span class="reserved">for</span><span class="plain"> (</span><span class="identifier">j</span><span class="plain">=0; </span><span class="identifier">j</span><span class="plain">&lt;2; </span><span class="identifier">j</span><span class="plain">++) {</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">bp_atom</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[1-</span><span class="identifier">j</span><span class="plain">].</span><span class="element">variable</span><span class="plain"> == </span><span class="identifier">v</span><span class="plain">) &amp;&amp; (</span><span class="identifier">v</span><span class="plain"> &gt;= </span><span class="constant">0</span><span class="plain">)) {</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">); </span><span class="comment">remove <code class="display"><span class="extract">QUANTIFIER_ATOM</span></code></span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">); </span><span class="comment">remove <code class="display"><span class="extract">DOMAIN_OPEN_ATOM</span></code></span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">); </span><span class="comment">remove <code class="display"><span class="extract">KIND_ATOM</span></code></span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">); </span><span class="comment">remove <code class="display"><span class="extract">DOMAIN_CLOSE_ATOM</span></code></span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">); </span><span class="comment">remove <code class="display"><span class="extract">PREDICATE_ATOM</span></code></span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::insert_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">,</span>
<span class="functiontext">Calculus::Atoms::NOWHERE_new</span><span class="plain">(</span><span class="identifier">bp_atom</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">]));</span>
<span class="identifier">PROPOSITION_EDITED</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">);</span>
<span class="reserved">break</span><span class="plain">;</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="reserved">return</span><span class="plain"> </span><span class="identifier">prop</span><span class="plain">;</span>
<span class="plain">#</span><span class="identifier">endif</span>
<span class="plain">}</span>
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="functiontext">Calculus::Simplifications::everywhere_and_nowhere</span><span class="plain">(</span><span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">prop</span><span class="plain">, </span><span class="reserved">int</span><span class="plain"> *</span><span class="identifier">changed</span><span class="plain">) {</span>
<span class="plain">*</span><span class="identifier">changed</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
<span class="plain">#</span><span class="identifier">ifdef</span><span class="plain"> </span><span class="identifier">IF_MODULE</span>
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">) {</span>
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">q_atom</span><span class="plain">, *</span><span class="identifier">k_atom</span><span class="plain">, *</span><span class="identifier">bp_atom</span><span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="functiontext">Calculus::Propositions::match</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="constant">6</span><span class="plain">,</span>
<span class="constant">QUANTIFIER_ATOM</span><span class="plain">, &amp;</span><span class="identifier">q_atom</span><span class="plain">,</span>
<span class="constant">DOMAIN_OPEN_ATOM</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">,</span>
<span class="constant">KIND_ATOM</span><span class="plain">, &amp;</span><span class="identifier">k_atom</span><span class="plain">,</span>
<span class="constant">DOMAIN_CLOSE_ATOM</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">,</span>
<span class="constant">PREDICATE_ATOM</span><span class="plain">, &amp;</span><span class="identifier">bp_atom</span><span class="plain">,</span>
<span class="constant">END_PROP_HERE</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">)) &amp;&amp;</span>
<span class="plain">((</span><span class="functiontext">Calculus::Atoms::is_forall_quantifier</span><span class="plain">(</span><span class="identifier">q_atom</span><span class="plain">)) ||</span>
<span class="plain">(</span><span class="functiontext">Calculus::Atoms::is_notall_quantifier</span><span class="plain">(</span><span class="identifier">q_atom</span><span class="plain">)) ||</span>
<span class="plain">(</span><span class="functiontext">Calculus::Atoms::is_nonexistence_quantifier</span><span class="plain">(</span><span class="identifier">q_atom</span><span class="plain">))) &amp;&amp;</span>
<span class="plain">(</span><span class="identifier">Kinds::Compare::eq</span><span class="plain">(</span><span class="identifier">k_atom</span><span class="plain">-&gt;</span><span class="element">assert_kind</span><span class="plain">, </span><span class="identifier">K_room</span><span class="plain">)) &amp;&amp;</span>
<span class="plain">(</span><span class="identifier">bp_atom</span><span class="plain">-&gt;</span><span class="identifier">arity</span><span class="plain"> == </span><span class="constant">2</span><span class="plain">)) {</span>
<span class="reserved">binary_predicate</span><span class="plain"> *</span><span class="identifier">bp</span><span class="plain"> = </span><span class="identifier">RETRIEVE_POINTER_binary_predicate</span><span class="plain">(</span><span class="identifier">bp_atom</span><span class="plain">-&gt;</span><span class="element">predicate</span><span class="plain">);</span>
<span class="reserved">if</span><span class="plain"> (((</span><span class="functiontext">Calculus::Atoms::is_nonexistence_quantifier</span><span class="plain">(</span><span class="identifier">q_atom</span><span class="plain">) == </span><span class="identifier">FALSE</span><span class="plain">) &amp;&amp; (</span><span class="identifier">bp</span><span class="plain"> == </span><span class="identifier">R_containment</span><span class="plain">)) ||</span>
<span class="plain">(</span><span class="identifier">bp</span><span class="plain"> == </span><span class="identifier">room_containment_predicate</span><span class="plain">)) {</span>
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">j</span><span class="plain">, </span><span class="identifier">v</span><span class="plain"> = </span><span class="identifier">k_atom</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[0].</span><span class="element">variable</span><span class="plain">;</span>
<span class="reserved">for</span><span class="plain"> (</span><span class="identifier">j</span><span class="plain">=0; </span><span class="identifier">j</span><span class="plain">&lt;2; </span><span class="identifier">j</span><span class="plain">++) {</span>
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">bp_atom</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[1-</span><span class="identifier">j</span><span class="plain">].</span><span class="element">variable</span><span class="plain"> == </span><span class="identifier">v</span><span class="plain">) &amp;&amp; (</span><span class="identifier">v</span><span class="plain"> &gt;= </span><span class="constant">0</span><span class="plain">)) {</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">); </span><span class="comment">remove <code class="display"><span class="extract">QUANTIFIER_ATOM</span></code></span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">); </span><span class="comment">remove <code class="display"><span class="extract">DOMAIN_OPEN_ATOM</span></code></span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">); </span><span class="comment">remove <code class="display"><span class="extract">KIND_ATOM</span></code></span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">); </span><span class="comment">remove <code class="display"><span class="extract">DOMAIN_CLOSE_ATOM</span></code></span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::delete_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">); </span><span class="comment">remove <code class="display"><span class="extract">PREDICATE_ATOM</span></code></span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::is_notall_quantifier</span><span class="plain">(</span><span class="identifier">q_atom</span><span class="plain">))</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::insert_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">, </span><span class="functiontext">Calculus::Atoms::new</span><span class="plain">(</span><span class="constant">NEGATION_CLOSE_ATOM</span><span class="plain">));</span>
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">new_atom</span><span class="plain">;</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::is_nonexistence_quantifier</span><span class="plain">(</span><span class="identifier">q_atom</span><span class="plain">))</span>
<span class="identifier">new_atom</span><span class="plain"> = </span><span class="functiontext">Calculus::Atoms::NOWHERE_new</span><span class="plain">(</span><span class="identifier">bp_atom</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">]);</span>
<span class="reserved">else</span>
<span class="identifier">new_atom</span><span class="plain"> = </span><span class="functiontext">Calculus::Atoms::EVERYWHERE_new</span><span class="plain">(</span><span class="identifier">bp_atom</span><span class="plain">-&gt;</span><span class="element">terms</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">]);</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::insert_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">, </span><span class="identifier">new_atom</span><span class="plain">);</span>
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext">Calculus::Atoms::is_notall_quantifier</span><span class="plain">(</span><span class="identifier">q_atom</span><span class="plain">))</span>
<span class="identifier">prop</span><span class="plain"> = </span><span class="functiontext">Calculus::Propositions::insert_atom</span><span class="plain">(</span><span class="identifier">prop</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">, </span><span class="functiontext">Calculus::Atoms::new</span><span class="plain">(</span><span class="constant">NEGATION_OPEN_ATOM</span><span class="plain">));</span>
<span class="identifier">PROPOSITION_EDITED</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">prop</span><span class="plain">);</span>
<span class="reserved">break</span><span class="plain">;</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">}</span>
<span class="plain">#</span><span class="identifier">endif</span>
<span class="reserved">return</span><span class="plain"> </span><span class="identifier">prop</span><span class="plain">;</span>
<span class="plain">}</span>
</pre>
<p class="inwebparagraph"></p>
<p class="endnote">The function Calculus::Simplifications::is_all_rooms is used in 11/sc (<a href="11-sc.html#SP1_14">&#167;1.14</a>, <a href="11-sc.html#SP2">&#167;2</a>).</p>
<p class="endnote">The function Calculus::Simplifications::everywhere_and_nowhere is used in 11/sc (<a href="11-sc.html#SP1_14">&#167;1.14</a>, <a href="11-sc.html#SP2">&#167;2</a>).</p>
<hr class="tocbar">
<ul class="toc"><li><a href="11-sc.html">Back to 'Sentence Conversions'</a></li><li><a href="11-tcp.html">Continue with 'Type Check Propositions'</a></li></ul><hr class="tocbar">
<!--End of weave-->
</main>
</body>
</html>
Reference in a new issue View git blame Copy permalink