1
0
Fork 0
mirror of https://github.com/ganelson/inform.git synced 2024-07-17 14:34:25 +03:00
inform7/docs/calculus-module/5-smp.html

1430 lines
247 KiB
HTML
Raw Normal View History

2019-03-17 14:40:57 +02:00
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
2020-04-14 19:56:54 +03:00
<title>Simplifications</title>
2020-05-03 03:20:55 +03:00
<link href="../docs-assets/Breadcrumbs.css" rel="stylesheet" rev="stylesheet" type="text/css">
2020-03-19 02:11:25 +02:00
<meta name="viewport" content="width=device-width initial-scale=1">
2019-03-17 14:40:57 +02:00
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta http-equiv="Content-Language" content="en-gb">
2020-05-03 03:01:21 +03:00
2020-05-03 03:20:55 +03:00
<link href="../docs-assets/Contents.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Progress.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Navigation.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Fonts.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Base.css" rel="stylesheet" rev="stylesheet" type="text/css">
2020-05-03 03:01:21 +03:00
<script>
MathJax = {
tex: {
inlineMath: '$', '$'], ['\\(', '\\)'
},
svg: {
fontCache: 'global'
}
};
</script>
<script type="text/javascript" id="MathJax-script" async
src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-svg.js">
</script>
<script>
function togglePopup(material_id) {
var popup = document.getElementById(material_id);
popup.classList.toggle("show");
}
</script>
2020-05-03 03:20:55 +03:00
<link href="../docs-assets/Popups.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Colours.css" rel="stylesheet" rev="stylesheet" type="text/css">
2020-04-14 19:56:54 +03:00
2019-03-17 14:40:57 +02:00
</head>
2020-05-03 03:01:21 +03:00
<body class="commentary-font">
2020-03-19 02:11:25 +02:00
<nav role="navigation">
2020-04-14 19:56:54 +03:00
<h1><a href="../index.html">
2020-05-03 18:34:53 +03:00
<img src="../docs-assets/Inform.png" height=72">
2020-04-14 19:56:54 +03:00
</a></h1>
<ul><li><a href="../compiler.html">compiler tools</a></li>
2020-03-19 02:11:25 +02:00
<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>
2020-04-14 19:56:54 +03:00
</ul><h2>Compiler Webs</h2><ul>
2020-03-19 02:11:25 +02:00
<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>
2020-04-14 19:56:54 +03:00
</ul><h2>Inbuild Modules</h2><ul>
<li><a href="../supervisor-module/index.html">supervisor</a></li>
</ul><h2>Inform7 Modules</h2><ul>
2020-08-25 01:11:39 +03:00
<li><a href="../core-module/index.html">core</a></li>
2020-08-27 17:50:24 +03:00
<li><a href="../assertions-module/index.html">assertions</a></li>
<li><a href="../values-module/index.html">values</a></li>
<li><a href="../knowledge-module/index.html">knowledge</a></li>
<li><a href="../imperative-module/index.html">imperative</a></li>
<li><a href="../runtime-module/index.html">runtime</a></li>
2020-03-19 02:11:25 +02:00
<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>
2020-04-14 19:56:54 +03:00
</ul><h2>Inter Modules</h2><ul>
<li><a href="../bytecode-module/index.html">bytecode</a></li>
2020-03-19 02:11:25 +02:00
<li><a href="../building-module/index.html">building</a></li>
<li><a href="../codegen-module/index.html">codegen</a></li>
2020-05-20 02:02:28 +03:00
</ul><h2>Services</h2><ul>
2020-04-14 19:56:54 +03:00
<li><a href="../arch-module/index.html">arch</a></li>
2020-08-25 01:11:39 +03:00
<li><a href="index.html"><span class="selectedlink">calculus</span></a></li>
2020-04-14 19:56:54 +03:00
<li><a href="../html-module/index.html">html</a></li>
2020-05-20 02:02:28 +03:00
<li><a href="../inflections-module/index.html">inflections</a></li>
2020-08-20 01:36:18 +03:00
<li><a href="../kinds-module/index.html">kinds</a></li>
2020-05-20 02:02:28 +03:00
<li><a href="../linguistics-module/index.html">linguistics</a></li>
<li><a href="../problems-module/index.html">problems</a></li>
2020-08-20 01:36:18 +03:00
<li><a href="../syntax-module/index.html">syntax</a></li>
<li><a href="../words-module/index.html">words</a></li>
2020-03-19 02:11:25 +02:00
<li><a href="../../../inweb/docs/foundation-module/index.html">foundation</a></li>
2020-04-14 19:56:54 +03:00
</ul>
2020-03-19 02:11:25 +02:00
</nav>
<main role="main">
2020-05-03 03:01:21 +03:00
<!--Weave of 'Simplifications' generated by Inweb-->
<div class="breadcrumbs">
2021-02-03 11:32:42 +02:00
<ul class="crumbs"><li><a href="../index.html">Home</a></li><li><a href="../compiler.html">Services</a></li><li><a href="index.html">calculus</a></li><li><a href="index.html#5">Chapter 5: Sentences</a></li><li><b>Simplifications</b></li></ul></div>
2020-05-03 03:01:21 +03:00
<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>
2019-03-17 14:40:57 +02:00
<ul class="toc"><li><a href="5-smp.html#SP2">&#167;2. Simplify the nothing constant (fudge)</a></li><li><a href="5-smp.html#SP3">&#167;3. Use listed-in predicates (deduction)</a></li><li><a href="5-smp.html#SP4">&#167;4. Simplify negated determiners (deduction)</a></li><li><a href="5-smp.html#SP6">&#167;6. Simplify negated satisfiability (deduction)</a></li><li><a href="5-smp.html#SP7">&#167;7. Make kind requirements explicit (deduction)</a></li><li><a href="5-smp.html#SP8">&#167;8. Remove redundant kind predicates (deduction)</a></li><li><a href="5-smp.html#SP10">&#167;10. Turn binary predicates the right way round (deduction)</a></li><li><a href="5-smp.html#SP11">&#167;11. Simplify region containment (fudge)</a></li><li><a href="5-smp.html#SP12">&#167;12. Reduce binary predicates (deduction)</a></li><li><a href="5-smp.html#SP13">&#167;13. Eliminating determined variables (deduction)</a></li><li><a href="5-smp.html#SP14">&#167;14. Simplify non-relation (deduction)</a></li><li><a href="5-smp.html#SP15">&#167;15. Convert gerunds to nouns (deduction)</a></li><li><a href="5-smp.html#SP16">&#167;16. Eliminate to have meaning property ownership (fudge)</a></li><li><a href="5-smp.html#SP18">&#167;18. Turn all rooms to everywhere (fudge)</a></li></ul><hr class="tocbar">
2019-03-17 14:40:57 +02:00
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP1" class="paragraph-anchor"></a><b>&#167;1. </b>Recall the three rules for simplification routines: they take a proposition
2020-04-14 19:56:54 +03:00
\(\Sigma\) (which they are allowed to destroy or modify) and return \(\Sigma'\),
2019-03-17 14:40:57 +02:00
but such that:
</p>
2020-04-14 19:56:54 +03:00
<ul class="items"><li>(i) \(\Sigma'\) remains a syntactically correct proposition with well-formed
2019-03-17 14:40:57 +02:00
quantifiers,
2020-04-14 19:56:54 +03:00
</li><li>(ii) \(\Sigma'\) has the same number of free variables as \(\Sigma\), and
2019-03-17 14:40:57 +02:00
</li><li>(iii) in all situations and for all possible values of any free variables,
2020-04-14 19:56:54 +03:00
\(\Sigma'\) is true if and only if \(\Sigma\) is.
2019-03-17 14:40:57 +02:00
</li></ul>
2020-05-03 03:01:21 +03:00
<p class="commentary">Rules (i) and (ii) are always strictly obeyed. A simplification which obeys (iii)
2019-03-17 14:40:57 +02:00
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>
2020-05-03 03:01:21 +03:00
<p class="commentary">What we mean by simpler is not shorter, or with less exotic contents: often
2019-03-17 14:40:57 +02:00
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>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP2" class="paragraph-anchor"></a><b>&#167;2. Simplify the nothing constant (fudge). </b>The word "nothing" is sometimes a noun ("the holder of the oak tree is
2019-03-17 14:40:57 +02:00
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>
2020-05-03 03:01:21 +03:00
<p class="commentary">Here we look for the noun form as one term in a binary predicate, and convert
2019-03-17 14:40:57 +02:00
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>
2020-05-03 03:01:21 +03:00
<pre class="displayed-code all-displayed-code code-font">
2021-02-03 11:32:42 +02:00
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Simplifications::nothing_constant</span><button class="popup" onclick="togglePopup('usagePopup1')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup1">Usage of <span class="code-font"><span class="function-syntax">Calculus::Simplifications::nothing_constant</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">&#167;2.14</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax">) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> #</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">DETECT_NOTHING_VALUE</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">)</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><a href="4-ap.html#SP10" class="function-link"><span class="function-syntax">Atoms::is_binary_predicate</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">)) &amp;&amp; (</span><a href="4-ap.html#SP10" class="function-link"><span class="function-syntax">Atoms::is_equality_predicate</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">)) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">binary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">bp</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RETRIEVE_POINTER_binary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">predicate</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">i</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">i</span><span class="plain-syntax">&lt;2; </span><span class="identifier-syntax">i</span><span class="plain-syntax">++) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">DETECT_NOTHING_VALUE</span><span class="plain-syntax">(</span><a href="4-trm.html#SP8" class="function-link"><span class="function-syntax">Terms::constant_underlying</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">])))) {</span>
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="5-smp.html#SP2_2" class="named-paragraph-link"><span class="named-paragraph">Substitute for the term and quantify with does-not-exist</span><span class="named-paragraph-number">2.2</span></a></span><span class="plain-syntax">;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">PROPOSITION_EDITED</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> #</span><span class="identifier-syntax">endif</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
2019-03-17 14:40:57 +02:00
</pre>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP2_1" class="paragraph-anchor"></a><b>&#167;2.1. </b>Formally, if \(B\) is a predicate other than equality,
2020-05-03 03:01:21 +03:00
\(\) \Sigma = \cdots B(t, f_X(f_Y(\cdots(<span class="extract"><span class="extract-syntax">nothing</span></span>))))\cdots \quad \longrightarrow \quad
\Sigma' = \cdots \not\exists v\in\lbrace v\mid K_1(v)\rbrace: B(t, f_X(f_Y(\cdots(v))))\cdots \(\)
2020-04-14 19:56:54 +03:00
where \(v\) is unused in \(\Sigma\), and &mdash; note the difference in placing &mdash;
2020-05-03 03:01:21 +03:00
\(\) \Sigma = \cdots B(f_X(f_Y(\cdots(<span class="extract"><span class="extract-syntax">nothing</span></span>))), t)\cdots \quad \longrightarrow \quad
\Sigma' = \not\exists v\in\lbrace v\mid K_2(v)\rbrace: \cdots B(f_X(f_Y(\cdots(v))), t)\cdots \(\)
2020-04-14 19:56:54 +03:00
where \(K_1\) and \(K_2\) are the kinds of terms 1 and 2 in the predicate \(B\).
2019-03-17 14:40:57 +02:00
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">The difference in where we place the quantifier is important in double-negative
2019-03-17 14:40:57 +02:00
sentences. Consider these:
</p>
<blockquote>
<p>[1] the box does not contain nothing</p>
</blockquote>
2020-05-03 03:01:21 +03:00
<p class="commentary">which produces $\Sigma = \lnot({\it contains}(<span class="extract"><span class="extract-syntax">box</span></span>, <span class="extract"><span class="extract-syntax">nothing</span></span>))$. Here,
<span class="extract"><span class="extract-syntax">nothing</span></span> is part of the object phrase, not the subject phrase, and we need
2019-03-17 14:40:57 +02:00
to quantify it within the OP &mdash; which means, within the negation, because our
2020-04-14 19:56:54 +03:00
recipe for negated sentences was (roughly) SP \(\land\lnot(\) OP \(\land\) VP\()\).
2020-05-03 03:01:21 +03:00
We thus make $\Sigma' = \lnot(\not\exists x:{\it contains}(<span class="extract"><span class="extract-syntax">box</span></span>, x))$,
although later simplification converts that to $\exists x: {\it contains}(<span class="extract"><span class="extract-syntax">box</span></span>, x)$,
2019-03-17 14:40:57 +02:00
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>
2020-05-03 03:01:21 +03:00
<p class="commentary">produces $\Sigma = \lnot({\it annoys}(<span class="extract"><span class="extract-syntax">nothing</span></span>, <span class="extract"><span class="extract-syntax">Peter</span></span>))$, and now we have
to quantify as $\Sigma' = \not\exists x: \lnot({\it annoys}(x, <span class="extract"><span class="extract-syntax">Peter</span></span>))$.
2019-03-17 14:40:57 +02:00
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">Double-negatives are a little odd. If natural language were really the same as
2019-03-17 14:40:57 +02:00
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>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP2_2" class="paragraph-anchor"></a><b>&#167;2.2. </b>The code is simpler than the explanation:
2019-03-17 14:40:57 +02:00
</p>
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Substitute for the term and quantify with does-not-exist</span><span class="named-paragraph-number">2.2</span></span><span class="comment-syntax"> =</span>
2020-05-03 03:01:21 +03:00
</p>
2019-03-17 14:40:57 +02:00
2020-05-03 03:01:21 +03:00
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">nv</span><span class="plain-syntax"> = </span><a href="4-bas.html#SP5" class="function-link"><span class="function-syntax">Binding::find_unused</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">new_var</span><span class="plain-syntax"> = </span><a href="4-trm.html#SP4" class="function-link"><span class="function-syntax">Terms::new_variable</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">nv</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><a href="4-bas.html#SP11" class="function-link"><span class="function-syntax">Binding::substitute_nothing_in_term</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">]), &amp;</span><span class="identifier-syntax">new_var</span><span class="plain-syntax">);</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">position</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">; </span><span class="comment-syntax"> at the front if </span><span class="extract"><span class="extract-syntax">nothing</span></span><span class="comment-syntax"> is the SP...</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">i</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">) </span><span class="identifier-syntax">position</span><span class="plain-syntax"> = </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">; </span><span class="comment-syntax"> ...but up close to the predicate if it's the OP</span>
<span class="plain-syntax"> </span><span class="comment-syntax"> insert four atoms, in reverse order, at this position:</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">position</span><span class="plain-syntax">, </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">DOMAIN_CLOSE_ATOM</span><span class="plain-syntax">));</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="3-bp.html#SP7" class="function-link"><span class="function-syntax">BinaryPredicates::term_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="identifier-syntax">i</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">position</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::new_atom</span></a><span class="plain-syntax">(</span><a href="3-bp.html#SP7" class="function-link"><span class="function-syntax">BinaryPredicates::term_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="identifier-syntax">i</span><span class="plain-syntax">), </span><span class="identifier-syntax">new_var</span><span class="plain-syntax">));</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">position</span><span class="plain-syntax">, </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">));</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">position</span><span class="plain-syntax">, </span><a href="4-ap.html#SP6" class="function-link"><span class="function-syntax">Atoms::QUANTIFIER_new</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">not_exists_quantifier</span><span class="plain-syntax">, </span><span class="identifier-syntax">nv</span><span class="plain-syntax">, </span><span class="constant-syntax">0</span><span class="plain-syntax">));</span>
2019-03-17 14:40:57 +02:00
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="5-smp.html#SP2">&#167;2</a>.</li></ul>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP3" class="paragraph-anchor"></a><b>&#167;3. Use listed-in predicates (deduction). </b>Specifications for entries in tables have a variety of forms (well, four
2019-03-17 14:40:57 +02:00
of them), and one is by implication a condition: this is the 2-reference form
2020-05-03 03:01:21 +03:00
of <span class="extract"><span class="extract-syntax">TABLE_ENTRY_NT</span></span> specification. Suppose the source text reads
2019-03-17 14:40:57 +02:00
</p>
<blockquote>
<p>if X is a density listed in the Table of Solid Stuff, ...</p>
</blockquote>
2020-05-03 03:01:21 +03:00
<p class="commentary">Inform parses "a density listed in the Table of Solid Stuff" as a single
2019-03-17 14:40:57 +02:00
specification, with references to the density column and the Solid Stuff
2020-04-14 19:56:54 +03:00
table. In logical terms, this is just another constant, which we'll call \(L\).
2019-03-17 14:40:57 +02:00
At this point the sentence looks like:
2020-04-14 19:56:54 +03:00
$$ {\it 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 \({\it is}\) so as to accommodate this, but it is much better to
2019-03-17 14:40:57 +02:00
use Inform's regular predicate apparatus.
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">So we must make its nature explicit. Every table column has an associated binary
2019-03-17 14:40:57 +02:00
predicate, and we rewrite:
2020-04-14 19:56:54 +03:00
$$ \exists v: {\it number}(v)\land {\hbox{\it listed-in-density-column}}(v, T)\land {\it is}(v, X) $$
2019-03-17 14:40:57 +02:00
This looks extravagant, but later simplification will reduce it to
2020-04-14 19:56:54 +03:00
$$ {\hbox{\it listed-in-density-column}}(X, T). $$
2019-03-17 14:40:57 +02:00
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">More formally suppose we write \(L(C, T)\) for the constant representing "a
2020-04-14 19:56:54 +03:00
C listed in T", and suppose we use the notation \(P(\dots t\dots)\) for any
predicate containing a term underlying which is \(t\). Let \(v\) be a variable
unused in \(\Sigma\), and let \(K\) be the kind of value of entries in the \(C\)
2019-03-17 14:40:57 +02:00
column. Then:
2020-05-03 03:01:21 +03:00
\(\) \Sigma = \cdots P(\dots L(C, T)\dots) \cdots \quad \longrightarrow \quad
\Sigma' = \cdots \exists v: K(v)\land {\hbox{\it listed-in-C-column}}(v, T)\land P(\dots v\dots) \cdots \(\)
2020-04-14 19:56:54 +03:00
where the variable \(v\) has replaced the constant \(L(C, T)\) underlying one
of the terms of \(P\).
2019-03-17 14:40:57 +02:00
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">Note that this can act twice on the same predicate, if such terms occur
2019-03-17 14:40:57 +02:00
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>
2020-05-03 03:01:21 +03:00
<p class="commentary">generates \({\it is}(L(C_1, T_1), L(C_2, T_2))\). As it happens, Inform can't
2019-03-17 14:40:57 +02:00
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,
2020-05-03 03:01:21 +03:00
\(\) \exists x: {\it number}(x)\land {\hbox{\it listed-in-PM_-column}}(x, T_1)\land
{\hbox{\it listed-in-PM_-column}}(x, T_2). \(\)
</p>
<pre class="displayed-code all-displayed-code code-font">
2020-08-25 01:11:39 +03:00
<span class="plain-syntax">#</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">CORE_MODULE</span>
2021-02-03 11:32:42 +02:00
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Simplifications::use_listed_in</span><button class="popup" onclick="togglePopup('usagePopup2')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup2">Usage of <span class="code-font"><span class="function-syntax">Calculus::Simplifications::use_listed_in</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">&#167;2.14</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax">) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">j</span><span class="plain-syntax">;</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="function-syntax">&lt;pl-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax">; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="identifier-syntax">spec</span><span class="plain-syntax"> = </span><a href="4-trm.html#SP8" class="function-link"><span class="function-syntax">Terms::constant_underlying</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">]));</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">spec</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">Lvalues::get_storage_form</span><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">) == </span><span class="identifier-syntax">TABLE_ENTRY_NT</span><span class="plain-syntax">) &amp;&amp;</span>
2020-05-11 17:21:29 +03:00
<span class="plain-syntax"> (</span><span class="identifier-syntax">Node::no_children</span><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">) == </span><span class="constant-syntax">2</span><span class="plain-syntax">)) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="identifier-syntax">col</span><span class="plain-syntax"> = </span><span class="identifier-syntax">spec</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">down</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="identifier-syntax">tab</span><span class="plain-syntax"> = </span><span class="identifier-syntax">spec</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">down</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">table_column</span><span class="plain-syntax"> *</span><span class="identifier-syntax">tc</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Rvalues::to_table_column</span><span class="plain-syntax">(</span><span class="identifier-syntax">col</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Tables::Columns::get_kind</span><span class="plain-syntax">(</span><span class="identifier-syntax">tc</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">K_understanding</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">Kinds::eq</span><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_understanding</span><span class="plain-syntax">))) </span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><span class="identifier-syntax">K_snippet</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">nv</span><span class="plain-syntax"> = </span><a href="4-bas.html#SP5" class="function-link"><span class="function-syntax">Binding::find_unused</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">nv_term</span><span class="plain-syntax"> = </span><a href="4-trm.html#SP4" class="function-link"><span class="function-syntax">Terms::new_variable</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">nv</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><a href="4-ap.html#SP10" class="function-link"><span class="function-syntax">Atoms::binary_PREDICATE_new</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">Tables::Columns::get_listed_in_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">tc</span><span class="plain-syntax">),</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">nv_term</span><span class="plain-syntax">, </span><a href="4-trm.html#SP4" class="function-link"><span class="function-syntax">Terms::new_constant</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">tab</span><span class="plain-syntax">)));</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">new_KIND</span><span class="plain-syntax"> = </span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::new_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><span class="identifier-syntax">nv_term</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">new_KIND</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">saved_bp</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Tables::Columns::get_listed_in_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">tc</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">, </span><span class="identifier-syntax">new_KIND</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><a href="4-ap.html#SP6" class="function-link"><span class="function-syntax">Atoms::QUANTIFIER_new</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">exists_quantifier</span><span class="plain-syntax">, </span><span class="identifier-syntax">nv</span><span class="plain-syntax">, </span><span class="constant-syntax">0</span><span class="plain-syntax">));</span>
<span class="plain-syntax"> </span><a href="4-bas.html#SP11" class="function-link"><span class="function-syntax">Binding::substitute_term_in_term</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">]), &amp;</span><span class="identifier-syntax">nv_term</span><span class="plain-syntax">);</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">LocalVariables::add_table_lookup</span><span class="plain-syntax">();</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">PROPOSITION_EDITED</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax">#</span><span class="identifier-syntax">endif</span>
2019-03-17 14:40:57 +02:00
</pre>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP4" class="paragraph-anchor"></a><b>&#167;4. Simplify negated determiners (deduction). </b>The negation atom is worth removing wherever possible, since we want to
2019-03-17 14:40:57 +02:00
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:
2020-04-14 19:56:54 +03:00
$$ \Sigma = \cdots \lnot (Qv\in\lbrace v\mid \phi(v)\rbrace: \psi)\cdots \quad \longrightarrow \quad \Sigma' = \cdots Q'v\in\lbrace v\mid \phi(v)\rbrace: \psi\cdots $$
where \(Q'\) is the negation of the generalised quantifier \(Q\):
for instance, \(V_{&lt;5} y\) becomes \(V_{\geq 5} y\).
2019-03-17 14:40:57 +02:00
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">A curiosity here is that when simplifying during sentence conversion, we
2020-04-14 19:56:54 +03:00
choose not to apply this deduction in the case of \(Q = \exists\). This saves us
having to make difficult decisions about the domain set of \(Q\) (see below),
and also preserves \(\exists v\) atoms in \(\Sigma\), which are useful since
2019-03-17 14:40:57 +02:00
they make some of our later simplifications more applicable.
</p>
2020-05-03 03:01:21 +03:00
<pre class="displayed-code all-displayed-code code-font">
2021-02-03 11:32:42 +02:00
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Simplifications::negated_determiners_nonex</span><button class="popup" onclick="togglePopup('usagePopup3')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup3">Usage of <span class="code-font"><span class="function-syntax">Calculus::Simplifications::negated_determiners_nonex</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">&#167;2.14</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="5-smp.html#SP4" class="function-link"><span class="function-syntax">Calculus::Simplifications::negated_determiners</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">changed</span><span class="plain-syntax">, </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax">}</span>
2020-08-25 01:11:39 +03:00
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Simplifications::negated_determiners</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax">,</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">negate_existence_too</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">quant_atom</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-prp.html#SP22" class="function-link"><span class="function-syntax">Propositions::match</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="constant-syntax">2</span><span class="plain-syntax">,</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="constant-syntax">NEGATION_OPEN_ATOM</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">quant_atom</span><span class="plain-syntax">)) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">negate_existence_too</span><span class="plain-syntax">) ||</span>
<span class="plain-syntax"> ((</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_existence_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">quant_atom</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">))) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="5-smp.html#SP5" class="function-link"><span class="function-syntax">Calculus::Simplifications::prop_ungroup_and_negate_determiner</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">, </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">PROPOSITION_EDITED</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
2019-03-17 14:40:57 +02:00
</pre>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP5" class="paragraph-anchor"></a><b>&#167;5. </b>And the following useful routine actually performs the change. The only
2020-04-14 19:56:54 +03:00
tricky point here is that we store \(\exists v\) without domain brackets; so
if \(Q\) happens to be \(\exists v\) then we have to turn \(\lnot(\exists v: \cdots)\)
into \(\not\exists v\in \lbrace v\mid \cdots\rbrace\cdots\), and it's not
obvious where to place the \(\rbrace\). While there's no logical difference &mdash;
2019-03-17 14:40:57 +02:00
the proposition means the same wherever we put it &mdash; the assert-propositions
2020-04-14 19:56:54 +03:00
code is better at handling \(\exists v\in X: \phi(v)\) than \(\exists v\in Y\).
So we want the braces to enclose fixed, unassertable matter &mdash; \(v\) being
a container, say &mdash; and the \(\phi\) outside the braces should then contain
2019-03-17 14:40:57 +02:00
predicates which can be asserted.
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">In practice that's way too hard for this routine to handle. If <span class="extract"><span class="extract-syntax">add_domain_brackets</span></span>
2019-03-17 14:40:57 +02:00
is set, then it converts
2020-05-03 03:01:21 +03:00
\(\) \lnot(\exists v: \cdots) \quad\longrightarrow\quad
\not\exists v\in \lbrace v\mid \cdots\rbrace \(\)
2019-03-17 14:40:57 +02:00
&mdash; that is, it will make the entire negated subproposition the domain of the
2020-05-03 03:01:21 +03:00
quantifier. If <span class="extract"><span class="extract-syntax">add_domain_brackets</span></span> is clear, the routine will return a
2019-03-17 14:40:57 +02:00
syntactically incorrect proposition lacking the domain brackets, and it's
the caller's responsibility to put that right.
</p>
2020-05-03 03:01:21 +03:00
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Simplifications::prop_ungroup_and_negate_determiner</span><button class="popup" onclick="togglePopup('usagePopup4')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup4">Usage of <span class="code-font"><span class="function-syntax">Calculus::Simplifications::prop_ungroup_and_negate_determiner</span></span>:<br/><a href="5-smp.html#SP4">&#167;4</a>, <a href="5-smp.html#SP6">&#167;6</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">after</span><span class="plain-syntax">,</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">add_domain_brackets</span><span class="plain-syntax">) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">quant_atom</span><span class="plain-syntax">, *</span><span class="identifier-syntax">last</span><span class="plain-syntax">;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">fnd</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">after</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">)</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">fnd</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP22" class="function-link"><span class="function-syntax">Propositions::match</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="constant-syntax">2</span><span class="plain-syntax">,</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="constant-syntax">NEGATION_OPEN_ATOM</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">quant_atom</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">else</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">fnd</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP22" class="function-link"><span class="function-syntax">Propositions::match</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">after</span><span class="plain-syntax">, </span><span class="constant-syntax">3</span><span class="plain-syntax">, </span><span class="constant-syntax">ANY_ATOM_HERE</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="constant-syntax">NEGATION_OPEN_ATOM</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">quant_atom</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">fnd</span><span class="plain-syntax">) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">quantifier</span><span class="plain-syntax"> *</span><span class="identifier-syntax">quant</span><span class="plain-syntax"> = </span><span class="identifier-syntax">quant_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">quant</span><span class="plain-syntax">;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">quantifier</span><span class="plain-syntax"> *</span><span class="identifier-syntax">antiquant</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Quantifiers::get_negation</span><span class="plain-syntax">(</span><span class="identifier-syntax">quant</span><span class="plain-syntax">);</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">quant_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">quant</span><span class="plain-syntax"> = </span><span class="identifier-syntax">antiquant</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP34" class="function-link"><span class="function-syntax">Propositions::ungroup_after</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">after</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">last</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove negation group brackets</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">quant</span><span class="plain-syntax"> == </span><span class="identifier-syntax">exists_quantifier</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">add_domain_brackets</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">quant_atom</span><span class="plain-syntax">, </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">));</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">last</span><span class="plain-syntax">, </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">DOMAIN_CLOSE_ATOM</span><span class="plain-syntax">));</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">antiquant</span><span class="plain-syntax"> == </span><span class="identifier-syntax">exists_quantifier</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP34" class="function-link"><span class="function-syntax">Propositions::ungroup_after</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">quant_atom</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove domain group brackets</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">PREDICATE_CALCULUS_WORKINGS</span><span class="plain-syntax">, </span><span class="string-syntax">"Calculus::Simplifications::prop_ungroup_and_negate_determiner: $D\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> } </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"not a negate-group-determiner"</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
2019-03-17 14:40:57 +02:00
</pre>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP6" class="paragraph-anchor"></a><b>&#167;6. Simplify negated satisfiability (deduction). </b>When simplifying converted sentences, we chose not to use the
2020-05-03 03:01:21 +03:00
<span class="extract"><span class="extract-syntax">Calculus::Simplifications::negated_determiners</span></span> tactic on existence quantifiers \(\exists v\),
2019-03-17 14:40:57 +02:00
partly because it's tricky to establish their domain in a way helpful to
the rest of Inform.
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">Here we handle a simple case which occurs frequently and where we can indeed
2019-03-17 14:40:57 +02:00
identify the domain well:
2020-05-03 03:01:21 +03:00
\(\) \Sigma = \lnot (\exists v: K(v)\land P) \quad \longrightarrow \quad
\Sigma' = \not\exists v\in\lbrace v\mid K(v)\rbrace: P \(\)
2020-04-14 19:56:54 +03:00
where \(K\) is a kind, and \(P\) is any single predicate other than equality.
2019-03-17 14:40:57 +02:00
(In the case of equality, we'd rather leave matters as they stand, because
substitution will later eliminate all of this anyway.)
</p>
2020-05-03 03:01:21 +03:00
<pre class="displayed-code all-displayed-code code-font">
2021-02-03 11:32:42 +02:00
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Simplifications::negated_satisfiable</span><button class="popup" onclick="togglePopup('usagePopup5')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup5">Usage of <span class="code-font"><span class="function-syntax">Calculus::Simplifications::negated_satisfiable</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">&#167;2.14</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax">) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">quant_atom</span><span class="plain-syntax">, *</span><span class="identifier-syntax">predicate_atom</span><span class="plain-syntax">, *</span><span class="identifier-syntax">kind_atom</span><span class="plain-syntax">;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><a href="4-prp.html#SP22" class="function-link"><span class="function-syntax">Propositions::match</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="constant-syntax">6</span><span class="plain-syntax">,</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="constant-syntax">NEGATION_OPEN_ATOM</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">quant_atom</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">kind_atom</span><span class="plain-syntax">, </span><span class="identifier-syntax">kind_up_family</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">predicate_atom</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">NEGATION_CLOSE_ATOM</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">END_PROP_HERE</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">)) &amp;&amp;</span>
<span class="plain-syntax"> (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_existence_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">quant_atom</span><span class="plain-syntax">)) &amp;&amp;</span>
<span class="plain-syntax"> (</span><a href="4-ap.html#SP10" class="function-link"><span class="function-syntax">Atoms::is_equality_predicate</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">predicate_atom</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">) &amp;&amp;</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> (</span><span class="identifier-syntax">kind_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">variable</span><span class="plain-syntax"> == </span><span class="identifier-syntax">quant_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">variable</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="5-smp.html#SP5" class="function-link"><span class="function-syntax">Calculus::Simplifications::prop_ungroup_and_negate_determiner</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">quant_atom</span><span class="plain-syntax">, </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">));</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">kind_atom</span><span class="plain-syntax">, </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">DOMAIN_CLOSE_ATOM</span><span class="plain-syntax">));</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
2019-03-17 14:40:57 +02:00
</pre>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP7" class="paragraph-anchor"></a><b>&#167;7. Make kind requirements explicit (deduction). </b>Many predicates contain implicit requirements about the kinds of their terms.
2020-04-14 19:56:54 +03:00
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
2019-03-17 14:40:57 +02:00
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>
2020-05-03 03:01:21 +03:00
<p class="commentary">Formally, let \(K_1\) and \(K_2\) be the kinds of value of terms 1 and 2 of the
2020-04-14 19:56:54 +03:00
binary predicate \(R\). Let \(v\) be a variable. Then:
2020-05-03 03:01:21 +03:00
\(\) \Sigma = \cdots R(v, t)\cdots \quad \longrightarrow \quad
\Sigma' = \cdots K_1(v)\land R(v, t) \(\)
\(\) \Sigma = \cdots R(t, v)\cdots \quad \longrightarrow \quad
\Sigma' = \cdots K_2(v)\land R(t, v) \(\)
2019-03-17 14:40:57 +02:00
and therefore, if both cases occur,
2020-05-03 03:01:21 +03:00
\(\) \Sigma = \cdots R(v, w)\cdots \quad \longrightarrow \quad
\Sigma' = \cdots K_1(v)\land K_2(w)\land R(v, w) \(\)
2019-03-17 14:40:57 +02:00
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">Some of these new kind atoms are unnecessary, but <span class="extract"><span class="extract-syntax">Calculus::Simplifications::redundant_kinds</span></span> will
2019-03-17 14:40:57 +02:00
detect and remove those.
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">Why do we do this for binary predicates, but not unary predicates? The answer
2019-03-17 14:40:57 +02:00
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>
2020-05-03 03:01:21 +03:00
<pre class="displayed-code all-displayed-code code-font">
2021-02-03 11:32:42 +02:00
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Simplifications::make_kinds_of_value_explicit</span><button class="popup" onclick="togglePopup('usagePopup6')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup6">Usage of <span class="code-font"><span class="function-syntax">Calculus::Simplifications::make_kinds_of_value_explicit</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">&#167;2.14</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax">) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">)</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP10" class="function-link"><span class="function-syntax">Atoms::is_binary_predicate</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">)) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">i</span><span class="plain-syntax">;</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">binary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">bp</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RETRIEVE_POINTER_binary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">predicate</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">i</span><span class="plain-syntax">=1; </span><span class="identifier-syntax">i</span><span class="plain-syntax">&gt;=0; </span><span class="identifier-syntax">i</span><span class="plain-syntax">--) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">v</span><span class="plain-syntax"> = </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">].</span><span class="element-syntax">variable</span><span class="plain-syntax">;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">v</span><span class="plain-syntax"> &gt;= </span><span class="constant-syntax">0</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><a href="3-bp.html#SP7" class="function-link"><span class="function-syntax">BinaryPredicates::term_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="identifier-syntax">i</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">K</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">new_KIND</span><span class="plain-syntax"> = </span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::new_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><a href="4-trm.html#SP4" class="function-link"><span class="function-syntax">Terms::new_variable</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">v</span><span class="plain-syntax">));</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">new_KIND</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">saved_bp</span><span class="plain-syntax"> = </span><span class="identifier-syntax">bp</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">, </span><span class="identifier-syntax">new_KIND</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
2019-03-17 14:40:57 +02:00
</pre>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP8" class="paragraph-anchor"></a><b>&#167;8. Remove redundant kind predicates (deduction). </b>Propositions often contain more <span class="extract"><span class="extract-syntax">KIND</span></span> atoms than they need, not least as a
2020-05-03 03:01:21 +03:00
result of <span class="extract"><span class="extract-syntax">Calculus::Simplifications::make_kinds_of_value_explicit</span></span>. Here we remove (some of)
2019-03-17 14:40:57 +02:00
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>
2020-05-03 03:01:21 +03:00
<pre class="displayed-code all-displayed-code code-font">
2021-02-03 11:32:42 +02:00
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Simplifications::redundant_kinds</span><button class="popup" onclick="togglePopup('usagePopup7')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup7">Usage of <span class="code-font"><span class="function-syntax">Calculus::Simplifications::redundant_kinds</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">&#167;2.14</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax">) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">c1</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">, </span><span class="identifier-syntax">c2</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="5-smp.html#SP9" class="function-link"><span class="function-syntax">Calculus::Simplifications::simp_redundant_kinds_dash</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="constant-syntax">1</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">c1</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="5-smp.html#SP9" class="function-link"><span class="function-syntax">Calculus::Simplifications::simp_redundant_kinds_dash</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="constant-syntax">1</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">c2</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">c1</span><span class="plain-syntax">) || (</span><span class="identifier-syntax">c2</span><span class="plain-syntax">)) *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">; </span><span class="reserved-syntax">else</span><span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
2019-03-17 14:40:57 +02:00
</pre>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP9" class="paragraph-anchor"></a><b>&#167;9. </b>This routine works recursively on subexpressions within the main
2020-05-03 03:01:21 +03:00
proposition. These all begin and end with matched <span class="extract"><span class="extract-syntax">*_OPEN_ATOM</span></span> and
<span class="extract"><span class="extract-syntax">*_CLOSED_ATOM</span></span> brackets, with one exception: the main proposition itself.
<span class="extract"><span class="extract-syntax">start_group</span></span> represents the first atom of the expression (the open
bracket, in most cases) and <span class="extract"><span class="extract-syntax">start_level</span></span> the level of bracket nesting
2019-03-17 14:40:57 +02:00
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>
2020-05-03 03:01:21 +03:00
<p class="commentary">This would all go wrong if the proposition were not well-formed, but we
2019-03-17 14:40:57 +02:00
know that it is &mdash; an internal error would have been thrown if not.
</p>
2020-05-03 03:01:21 +03:00
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Simplifications::simp_redundant_kinds_dash</span><button class="popup" onclick="togglePopup('usagePopup8')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup8">Usage of <span class="code-font"><span class="function-syntax">Calculus::Simplifications::simp_redundant_kinds_dash</span></span>:<br/><a href="5-smp.html#SP8">&#167;8</a>, <a href="5-smp.html#SP9_1">&#167;9.1</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">start_group</span><span class="plain-syntax">,</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">start_level</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax">) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">optimal_kind_placings_domain</span><span class="plain-syntax">[26], *</span><span class="identifier-syntax">optimal_kind_placings_statement</span><span class="plain-syntax">[26];</span>
2019-03-17 14:40:57 +02:00
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="5-smp.html#SP9_1" class="named-paragraph-link"><span class="named-paragraph">Recursively simplify all subexpressions first</span><span class="named-paragraph-number">9.1</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="5-smp.html#SP9_2" class="named-paragraph-link"><span class="named-paragraph">Find optimal positions for kind predicates</span><span class="named-paragraph-number">9.2</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="5-smp.html#SP9_3" class="named-paragraph-link"><span class="named-paragraph">Strike out redundant kind predicates applied to variables</span><span class="named-paragraph-number">9.3</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="5-smp.html#SP9_4" class="named-paragraph-link"><span class="named-paragraph">Strike out tautological kind predicates applied to constants</span><span class="named-paragraph-number">9.4</span></a></span><span class="plain-syntax">;</span>
2019-03-17 14:40:57 +02:00
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
2019-03-17 14:40:57 +02:00
</pre>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP9_1" class="paragraph-anchor"></a><b>&#167;9.1. </b>For all of the atoms in the body of the group we're working on, the bracket
2019-03-17 14:40:57 +02:00
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="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Recursively simplify all subexpressions first</span><span class="named-paragraph-number">9.1</span></span><span class="comment-syntax"> =</span>
2020-05-03 03:01:21 +03:00
</p>
2019-03-17 14:40:57 +02:00
2020-05-03 03:01:21 +03:00
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">blevel</span><span class="plain-syntax"> = </span><span class="identifier-syntax">start_level</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">start_group</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_opener</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">element</span><span class="plain-syntax">)) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">blevel</span><span class="plain-syntax">++;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">blevel</span><span class="plain-syntax"> == </span><span class="constant-syntax">2</span><span class="plain-syntax">) </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="5-smp.html#SP9" class="function-link"><span class="function-syntax">Calculus::Simplifications::simp_redundant_kinds_dash</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="constant-syntax">0</span><span class="plain-syntax">, </span><span class="identifier-syntax">changed</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_closer</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">element</span><span class="plain-syntax">)) </span><span class="identifier-syntax">blevel</span><span class="plain-syntax">--;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">blevel</span><span class="plain-syntax"> == </span><span class="constant-syntax">0</span><span class="plain-syntax">) </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> }</span>
2019-03-17 14:40:57 +02:00
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="5-smp.html#SP9">&#167;9</a>.</li></ul>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP9_2" class="paragraph-anchor"></a><b>&#167;9.2. </b>Suppose we have a kind predicate \(K(v)\) applied to a variable. What would
2019-03-17 14:40:57 +02:00
be the best place to put this? Generally speaking, we want it as early as
2020-04-14 19:56:54 +03:00
possible, because tests of \(K\) are cheap and this will keep running time
2019-03-17 14:40:57 +02:00
low in compiled code. On the other hand we must not move it outside the
current subexpression. The doctrine is:
</p>
2020-04-14 19:56:54 +03:00
<ul class="items"><li>(i) if \(v\) is unbound {\it within the subexpression} then \(K(v)\) should
2019-03-17 14:40:57 +02:00
move right to the front;
2020-04-14 19:56:54 +03:00
</li><li>(ii) if \(v\) is bound by \(\exists\), then \(K(v)\) should move immediately
after \(\exists v\);
</li><li>(iii) if \(v\) is bound by \(Q v\in\lbrace v\mid \phi(v)\rbrace\) then any
\(K(v)\) occurring in the domain \(\phi(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 \(\not\exists v\in\lbrace v\mid \phi(v)\rbrace\),
when \(K(v)\) should move into the domain set, even if it occurs in the
2019-03-17 14:40:57 +02:00
statement.
</li></ul>
2020-05-03 03:01:21 +03:00
<p class="commentary">Rule (iv) there looks a little surprising. For instance, it causes
\(\) \Sigma = \not\exists x\in\lbrace x\mid {\it thing}(x)\land{\it contains}(<span class="extract"><span class="extract-syntax">Ballroom</span></span>, x)\rbrace :
2020-04-14 19:56:54 +03:00
{\it container}(x)\land {\it open(x)}
2020-05-03 03:01:21 +03:00
\quad \longrightarrow \quad \(\)
\(\) \Sigma' = \not\exists x\in\lbrace x\mid {\it container}(x)\land{\it thing}(x)\land{\it contains}(<span class="extract"><span class="extract-syntax">Ballroom</span></span>, x)\rbrace :
{\it open(x)}. \(\)
2020-04-14 19:56:54 +03:00
These are logically equivalent because \(\not\exists\) behaves that way &mdash;
2019-03-17 14:40:57 +02:00
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
2020-04-14 19:56:54 +03:00
makes \(\Sigma'\) possible to assert with "now", as in the phrase "now
2019-03-17 14:40:57 +02:00
nothing in the Ballroom is an open container".
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">The following calculates two arrays: <span class="extract"><span class="extract-syntax">optimal_kind_placings_domain</span></span> marks the
start of \(\phi\) for each variable \(v\), while <span class="extract"><span class="extract-syntax">optimal_kind_placings_statement</span></span>
2019-03-17 14:40:57 +02:00
marks the start of the statement following the quantifier.
</p>
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Find optimal positions for kind predicates</span><span class="named-paragraph-number">9.2</span></span><span class="comment-syntax"> =</span>
2020-05-03 03:01:21 +03:00
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">bvsp</span><span class="plain-syntax"> = </span><span class="constant-syntax">0</span><span class="plain-syntax">, </span><span class="identifier-syntax">bound_vars_stack</span><span class="plain-syntax">[26];</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">blevel</span><span class="plain-syntax"> = </span><span class="identifier-syntax">start_level</span><span class="plain-syntax">, </span><span class="identifier-syntax">j</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="plain-syntax">&lt;26; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">optimal_kind_placings_domain</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] = (</span><span class="identifier-syntax">start_level</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">)?</span><span class="identifier-syntax">NULL:start_group</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">optimal_kind_placings_statement</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] = </span><span class="identifier-syntax">optimal_kind_placings_domain</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">];</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">start_group</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_opener</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">element</span><span class="plain-syntax">)) </span><span class="identifier-syntax">blevel</span><span class="plain-syntax">++;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_closer</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">element</span><span class="plain-syntax">)) </span><span class="identifier-syntax">blevel</span><span class="plain-syntax">--;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">blevel</span><span class="plain-syntax"> == </span><span class="constant-syntax">0</span><span class="plain-syntax">) </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">dom</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-prp.html#SP22" class="function-link"><span class="function-syntax">Propositions::match</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="constant-syntax">2</span><span class="plain-syntax">,</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">dom</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_existence_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">)) ||</span>
<span class="plain-syntax"> (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_nonexistence_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">)))</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">bound_vars_stack</span><span class="plain-syntax">[</span><span class="identifier-syntax">bvsp</span><span class="plain-syntax">++] = -1;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">else</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">bound_vars_stack</span><span class="plain-syntax">[</span><span class="identifier-syntax">bvsp</span><span class="plain-syntax">++] = </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">variable</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">optimal_kind_placings_domain</span><span class="plain-syntax">[</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">variable</span><span class="plain-syntax">] = </span><span class="identifier-syntax">dom</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">optimal_kind_placings_statement</span><span class="plain-syntax">[</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">variable</span><span class="plain-syntax">] = </span><span class="identifier-syntax">dom</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> } </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_existence_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">)) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">optimal_kind_placings_domain</span><span class="plain-syntax">[</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">variable</span><span class="plain-syntax">] = </span><span class="identifier-syntax">pl</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">optimal_kind_placings_statement</span><span class="plain-syntax">[</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">variable</span><span class="plain-syntax">] = </span><span class="identifier-syntax">pl</span><span class="plain-syntax">;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> }</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">DOMAIN_CLOSE_ATOM</span><span class="plain-syntax">) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">v</span><span class="plain-syntax"> = </span><span class="identifier-syntax">bound_vars_stack</span><span class="plain-syntax">[--</span><span class="identifier-syntax">bvsp</span><span class="plain-syntax">];</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">v</span><span class="plain-syntax"> &gt;= </span><span class="constant-syntax">0</span><span class="plain-syntax">) </span><span class="identifier-syntax">optimal_kind_placings_statement</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">] = </span><span class="identifier-syntax">pl</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
2019-03-17 14:40:57 +02:00
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="5-smp.html#SP9">&#167;9</a>.</li></ul>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP9_3" class="paragraph-anchor"></a><b>&#167;9.3. </b>The following looks at the predicates \(K(v)\) applied to variables which
2019-03-17 14:40:57 +02:00
are in the subexpression at the top level. It then does two things:
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">Suppose \(K\) and \(L\) are kinds of value such that \(L\subseteq K\), and let
2020-04-14 19:56:54 +03:00
\(\psi\) be a well-formed proposition. Then
2020-05-03 03:01:21 +03:00
\(\) \Sigma = \psi \land L(v) \cdots K(v) \cdots
2020-04-14 19:56:54 +03:00
\quad \longrightarrow \quad
2020-05-03 03:01:21 +03:00
\Sigma' = \psi \land L(v) \cdots \(\)
2020-04-14 19:56:54 +03:00
(that is, \(K(v)\) is eliminated). This is clearly valid since \(L(v)\Rightarrow K(v)\)
and \(L(v)\) is valid throughout the subexpression after its appearance.
2019-03-17 14:40:57 +02:00
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">Secondly, and it's not worth finding a logical notation for this, the kind
2019-03-17 14:40:57 +02:00
is moved back to its optimal position, as calculated above.
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">At first sight, this process only removes redundancies when the stronger
2019-03-17 14:40:57 +02:00
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
2020-04-14 19:56:54 +03:00
their order. Suppose we start with \({\it person}(x)\land{\it vehicle}(y)\land{\it woman}(x)\).
2019-03-17 14:40:57 +02:00
</p>
2020-04-14 19:56:54 +03:00
<ul class="items"><li>(1a) On pass 1, {\it person} occurs before {\it woman}, but it is weaker &mdash;
2019-03-17 14:40:57 +02:00
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
2020-04-14 19:56:54 +03:00
\({\it woman}(x)\land{\it vehicle}(y)\land{\it person}(x)\).
</li><li>(2a) On pass 2, the stronger {\it woman} now occurs before {\it person}, so
we eliminate to get \({\it woman}(x)\land{\it vehicle}(y)\).
</li><li>(2b) And pass 2 again moves kinds back, producing \({\it vehicle}(y)\land{\it woman}(x)\).
2019-03-17 14:40:57 +02:00
</li></ul>
2020-05-03 03:01:21 +03:00
<p class="commentary">(Because the order is reversed twice, any surviving kind predicates continue
2019-03-17 14:40:57 +02:00
to appear in the same order as they did in the original proposition. This
doesn't matter, but it's tidy.)
</p>
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Strike out redundant kind predicates applied to variables</span><span class="named-paragraph-number">9.3</span></span><span class="comment-syntax"> =</span>
2020-05-03 03:01:21 +03:00
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">domain_passed</span><span class="plain-syntax">[26], </span><span class="identifier-syntax">j</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">blevel</span><span class="plain-syntax"> = </span><span class="identifier-syntax">start_level</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="plain-syntax">&lt;26; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++) </span><span class="identifier-syntax">domain_passed</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">start_group</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="plain-syntax">&lt;26; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++)</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pl</span><span class="plain-syntax"> == </span><span class="identifier-syntax">optimal_kind_placings_statement</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">])</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">domain_passed</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_opener</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">element</span><span class="plain-syntax">)) </span><span class="identifier-syntax">blevel</span><span class="plain-syntax">++;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_closer</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">element</span><span class="plain-syntax">)) </span><span class="identifier-syntax">blevel</span><span class="plain-syntax">--;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">blevel</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::is_kind_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">early_kind</span><span class="plain-syntax"> = </span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::get_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">v</span><span class="plain-syntax"> = </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">variable</span><span class="plain-syntax">;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">v</span><span class="plain-syntax"> &gt;= </span><span class="constant-syntax">0</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">early_kind</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="5-smp.html#SP9_3_1" class="named-paragraph-link"><span class="named-paragraph">Strike out any subsequent but weaker kind predicate on the same variable</span><span class="named-paragraph-number">9.3.1</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="5-smp.html#SP9_3_2" class="named-paragraph-link"><span class="named-paragraph">Move this predicate backwards to its optimal position</span><span class="named-paragraph-number">9.3.2</span></a></span><span class="plain-syntax">;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">blevel</span><span class="plain-syntax"> == </span><span class="constant-syntax">0</span><span class="plain-syntax">) </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> }</span>
2019-03-17 14:40:57 +02:00
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="5-smp.html#SP9">&#167;9</a>.</li></ul>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP9_3_1" class="paragraph-anchor"></a><b>&#167;9.3.1. </b>The noteworthy thing here is that we continue through the subexpression,
2020-04-14 19:56:54 +03:00
deleting any weaker form of \(K(v)\) that we find, but also allow ourselves
2019-03-17 14:40:57 +02:00
to continue beyond the subexpression in one case. Suppose we have
2020-04-14 19:56:54 +03:00
$$ Qv\in\lbrace v\mid K(v) \land... \rbrace : 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 \(\rbrace\), the end of
2019-03-17 14:40:57 +02:00
the domain specification. So in that one case alone we allow ourselves
2020-05-03 03:01:21 +03:00
to sidestep the <span class="extract"><span class="extract-syntax">DOMAIN_CLOSE_ATOM</span></span> and continue looking for \(L(v)\) in the
2019-03-17 14:40:57 +02:00
outer subexpression &mdash; the one which is governed by the quantifier.
</p>
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Strike out any subsequent but weaker kind predicate on the same variable</span><span class="named-paragraph-number">9.3.1</span></span><span class="comment-syntax"> =</span>
2020-05-03 03:01:21 +03:00
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">gpl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">glevel</span><span class="plain-syntax"> = </span><span class="constant-syntax">1</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">gpl</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_opener</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">gpl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax">)) </span><span class="identifier-syntax">glevel</span><span class="plain-syntax">++;</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">gpl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">DOMAIN_CLOSE_ATOM</span><span class="plain-syntax">) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">glevel</span><span class="plain-syntax"> &gt; </span><span class="constant-syntax">1</span><span class="plain-syntax">) </span><span class="identifier-syntax">glevel</span><span class="plain-syntax">--;</span>
<span class="plain-syntax"> } </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_closer</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">gpl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax">)) </span><span class="identifier-syntax">glevel</span><span class="plain-syntax">--;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">glevel</span><span class="plain-syntax"> == </span><span class="constant-syntax">0</span><span class="plain-syntax">) </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">gpl</span><span class="plain-syntax"> != </span><span class="identifier-syntax">pl</span><span class="plain-syntax">) &amp;&amp; (</span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::is_kind_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">gpl</span><span class="plain-syntax">)) &amp;&amp; (</span><span class="identifier-syntax">v</span><span class="plain-syntax"> == </span><span class="identifier-syntax">gpl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">variable</span><span class="plain-syntax">)) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="comment-syntax"> i.e., </span><span class="extract"><span class="extract-syntax">gpl</span></span><span class="comment-syntax"> now points to a different kind atom on the same variable</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">later_kind</span><span class="plain-syntax"> = </span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::get_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">gpl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">later_kind</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">Kinds::conforms_to</span><span class="plain-syntax">(</span><span class="identifier-syntax">early_kind</span><span class="plain-syntax">, </span><span class="identifier-syntax">later_kind</span><span class="plain-syntax">))) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">gpl_prev</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">PROPOSITION_EDITED_REPEATING_CURRENT</span><span class="plain-syntax">(</span><span class="identifier-syntax">gpl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
2019-03-17 14:40:57 +02:00
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="5-smp.html#SP9_3">&#167;9.3</a>.</li></ul>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP9_3_2" class="paragraph-anchor"></a><b>&#167;9.3.2. </b><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Move this predicate backwards to its optimal position</span><span class="named-paragraph-number">9.3.2</span></span><span class="comment-syntax"> =</span>
2020-05-03 03:01:21 +03:00
</p>
<pre class="displayed-code all-displayed-code code-font">
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">best_place</span><span class="plain-syntax"> = </span><span class="identifier-syntax">optimal_kind_placings_domain</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">];</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">domain_passed</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">]) </span><span class="identifier-syntax">best_place</span><span class="plain-syntax"> = </span><span class="identifier-syntax">optimal_kind_placings_statement</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">];</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax"> != </span><span class="identifier-syntax">best_place</span><span class="plain-syntax">) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">state</span><span class="plain-syntax"> = </span><a href="2-kp.html#SP5" class="function-link"><span class="function-syntax">KindPredicates::is_unarticled_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> that is, delete the current </span>\(K(v)\)
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">new_K</span><span class="plain-syntax"> = </span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::new_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">early_kind</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><a href="4-trm.html#SP4" class="function-link"><span class="function-syntax">Terms::new_variable</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">v</span><span class="plain-syntax">));</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><a href="2-kp.html#SP5" class="function-link"><span class="function-syntax">KindPredicates::set_unarticled</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">new_K</span><span class="plain-syntax">, </span><span class="identifier-syntax">state</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">best_place</span><span class="plain-syntax">, </span><span class="identifier-syntax">new_K</span><span class="plain-syntax">); </span><span class="comment-syntax"> insert a new one</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">PROPOSITION_EDITED_REPEATING_CURRENT</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> }</span>
2019-03-17 14:40:57 +02:00
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="5-smp.html#SP9_3">&#167;9.3</a>.</li></ul>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP9_4" class="paragraph-anchor"></a><b>&#167;9.4. </b>Suppose we find a term \(K(C)\), where \(C\) is a constant in the sense of
2020-05-03 03:01:21 +03:00
predicate calculus &mdash; that is, a <span class="extract"><span class="extract-syntax">specification</span></span>. There is no need to
2020-04-14 19:56:54 +03:00
perform such a test at run-time because we can determine the kind of \(C\)
2020-05-03 03:01:21 +03:00
and compare it against \(K\) right now. For instance, ${\it number}(<span class="extract"><span class="extract-syntax">score</span></span>)$
2019-03-17 14:40:57 +02:00
is necessarily true at all times.
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">Formally, suppose \(C\) is a constant which, when evaluated, has kind of value
2020-04-14 19:56:54 +03:00
\(L\). Suppose that \(L\subseteq K\) and that \(K\) is not a kind of object. Then
$$ \Sigma = \cdots K(C)\cdots \quad \longrightarrow \quad \Sigma' = \cdots\cdots $$
(That is, we eliminate the \(K(C)\) term.)
2019-03-17 14:40:57 +02:00
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">We could clearly go further than this:
2019-03-17 14:40:57 +02:00
</p>
2020-04-14 19:56:54 +03:00
<ul class="items"><li>(a) Why don't we eliminate \(K(C)\) when \(K\) is an object, too? Logically this
2019-03-17 14:40:57 +02:00
would be fine, but we choose not to, for two reasons: people sometimes write
2020-05-03 03:01:21 +03:00
phrases in I6 which claim to return a room, say, but sometimes return <span class="extract"><span class="extract-syntax">nothing</span></span>.
2020-04-14 19:56:54 +03:00
Technically this is a violation of type safety. If \(t\) is a term representing
a call to this function, then \({\it room}(t)\) ought to be redundant. But in
2020-05-03 03:01:21 +03:00
practice it will protect against the <span class="extract"><span class="extract-syntax">nothing</span></span> value. The other reason is
2019-03-17 14:40:57 +02:00
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.
2020-04-14 19:56:54 +03:00
</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 \({\it text}(4)\)? Again, it would make it harder to
2019-03-17 14:40:57 +02:00
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="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Strike out tautological kind predicates applied to constants</span><span class="named-paragraph-number">9.4</span></span><span class="comment-syntax"> =</span>
2020-05-03 03:01:21 +03:00
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">blevel</span><span class="plain-syntax"> = </span><span class="identifier-syntax">start_level</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">start_group</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_opener</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">element</span><span class="plain-syntax">)) </span><span class="identifier-syntax">blevel</span><span class="plain-syntax">++;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_closer</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">element</span><span class="plain-syntax">)) </span><span class="identifier-syntax">blevel</span><span class="plain-syntax">--;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">blevel</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::is_kind_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">early_kind</span><span class="plain-syntax"> = </span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::get_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="identifier-syntax">spec</span><span class="plain-syntax"> = </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">constant</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RVALUE_TO_KIND_FUNCTION</span><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">K</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">Kinds::Behaviour::is_subkind_of_object</span><span class="plain-syntax">(</span><span class="identifier-syntax">early_kind</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">) &amp;&amp;</span>
<span class="plain-syntax"> (</span><span class="identifier-syntax">Kinds::conforms_to</span><span class="plain-syntax">(</span><span class="identifier-syntax">early_kind</span><span class="plain-syntax">, </span><span class="identifier-syntax">K</span><span class="plain-syntax">))) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">);</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">PROPOSITION_EDITED_REPEATING_CURRENT</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
2019-03-17 14:40:57 +02:00
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="5-smp.html#SP9">&#167;9</a>.</li></ul>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP10" class="paragraph-anchor"></a><b>&#167;10. Turn binary predicates the right way round (deduction). </b>Recall that BPs are manufactured in pairs, each being the reversal of
2019-03-17 14:40:57 +02:00
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>
2020-05-03 03:01:21 +03:00
<p class="commentary">Suppose \(B\) is a binary predicate which is marked as the wrong way round,
2020-04-14 19:56:54 +03:00
and \(R\) is its reversal. Then we change:
2020-05-03 03:01:21 +03:00
\(\) \Sigma = \cdots B(t_1, t_2)\cdots \quad \longrightarrow \quad
\Sigma' = \cdots R(t_2, t_1) \cdots \(\)
2019-03-17 14:40:57 +02:00
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">(Note that the equality predicate "is" only has one way round, and it's
2019-03-17 14:40:57 +02:00
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>
2020-05-03 03:01:21 +03:00
<pre class="displayed-code all-displayed-code code-font">
2021-02-03 11:32:42 +02:00
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Simplifications::turn_right_way_round</span><button class="popup" onclick="togglePopup('usagePopup9')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup9">Usage of <span class="code-font"><span class="function-syntax">Calculus::Simplifications::turn_right_way_round</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">&#167;2.14</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax">) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">binary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">bp</span><span class="plain-syntax"> = </span><a href="4-ap.html#SP10" class="function-link"><span class="function-syntax">Atoms::is_binary_predicate</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">bp</span><span class="plain-syntax">) &amp;&amp; (</span><a href="3-bp.html#SP16" class="function-link"><span class="function-syntax">BinaryPredicates::is_the_wrong_way_round</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">bp</span><span class="plain-syntax">))) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">pt</span><span class="plain-syntax"> = </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0];</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0] = </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1];</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1] = </span><span class="identifier-syntax">pt</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">predicate</span><span class="plain-syntax"> = </span><span class="identifier-syntax">STORE_POINTER_binary_predicate</span><span class="plain-syntax">(</span><a href="3-bp.html#SP16" class="function-link"><span class="function-syntax">BinaryPredicates::get_reversal</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">bp</span><span class="plain-syntax">));</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">PROPOSITION_EDITED</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
2019-03-17 14:40:57 +02:00
</pre>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP11" class="paragraph-anchor"></a><b>&#167;11. Simplify region containment (fudge). </b>Most of Inform's prepositions are unambiguous, but "in" can mean two quite
2019-03-17 14:40:57 +02:00
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
2020-04-14 19:56:54 +03:00
different binary predicates because direct containment has a function \(f_D\)
2019-03-17 14:40:57 +02:00
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>
2020-05-03 03:01:21 +03:00
<p class="commentary">So far we assume every "in" means the <span class="extract"><span class="extract-syntax">R_containment</span></span>. This is the
point where we choose to divert some uses to <span class="extract"><span class="extract-syntax">R_regional_containment</span></span>.
2020-04-14 19:56:54 +03:00
If \(R\) is a constant region name, and \(C_D\), \(C_R\) are the predicates for
2019-03-17 14:40:57 +02:00
direct and region containment, then
2020-05-03 03:01:21 +03:00
\(\) \Sigma = \cdots C_D(t, R)\cdots \quad \longrightarrow \quad
\Sigma' = \cdots C_R(t, R)\cdots \(\)
\(\) \Sigma = \cdots C_D(R, t)\cdots \quad \longrightarrow \quad
\Sigma' = \cdots C_R(R, t)\cdots \(\)
2019-03-17 14:40:57 +02:00
(Note that a region cannot directly contain any object, except a backdrop.)
</p>
2020-05-03 03:01:21 +03:00
<pre class="displayed-code all-displayed-code code-font">
2021-02-03 11:32:42 +02:00
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Simplifications::region_containment</span><button class="popup" onclick="togglePopup('usagePopup10')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup10">Usage of <span class="code-font"><span class="function-syntax">Calculus::Simplifications::region_containment</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">&#167;2.14</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax">) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> #</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">IF_MODULE</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">binary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">bp</span><span class="plain-syntax"> = </span><a href="4-ap.html#SP10" class="function-link"><span class="function-syntax">Atoms::is_binary_predicate</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">bp</span><span class="plain-syntax"> == </span><span class="identifier-syntax">R_containment</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">j</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="plain-syntax">&lt;2; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">regionality</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">, </span><span class="identifier-syntax">backdropping</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">].</span><span class="identifier-syntax">constant</span><span class="plain-syntax">) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">KR</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Specifications::to_kind</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">].</span><span class="element-syntax">constant</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Kinds::Behaviour::is_object_of_kind</span><span class="plain-syntax">(</span><span class="identifier-syntax">KR</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_region</span><span class="plain-syntax">)) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">regionality</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1-</span><span class="identifier-syntax">j</span><span class="plain-syntax">].</span><span class="element-syntax">constant</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">KB</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Specifications::to_kind</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1-</span><span class="identifier-syntax">j</span><span class="plain-syntax">].</span><span class="element-syntax">constant</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Kinds::Behaviour::is_object_of_kind</span><span class="plain-syntax">(</span><span class="identifier-syntax">KB</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_backdrop</span><span class="plain-syntax">)) </span><span class="identifier-syntax">backdropping</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">regionality</span><span class="plain-syntax">) &amp;&amp; (!</span><span class="identifier-syntax">backdropping</span><span class="plain-syntax">)) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">predicate</span><span class="plain-syntax"> = </span><span class="identifier-syntax">STORE_POINTER_binary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">R_regional_containment</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">PROPOSITION_EDITED</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> #</span><span class="identifier-syntax">endif</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
2019-03-17 14:40:57 +02:00
</pre>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP12" class="paragraph-anchor"></a><b>&#167;12. Reduce binary predicates (deduction). </b>If we are able to reduce a binary to a unary predicate, we will probably
2019-03-17 14:40:57 +02:00
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
2020-05-03 03:01:21 +03:00
\(\) \exists x: {\it burrow}(x)\land {\it in}(<span class="extract"><span class="extract-syntax">Cholet</span></span>, x) \(\)
2020-04-14 19:56:54 +03:00
To test that proposition requires trying all possible burrows \(x\).
2019-03-17 14:40:57 +02:00
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:
2020-05-03 03:01:21 +03:00
\(\) \exists x: {\it burrow}(x)\land {\it is}(<span class="extract"><span class="extract-syntax">ContainerOf(Cholet)</span></span>, x) \(\)
2020-04-14 19:56:54 +03:00
A later simplification can then observe that this tells us what \(x\) must be,
2019-03-17 14:40:57 +02:00
and eliminate both quantifier and variable.
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">Formally, suppose \(B\) is a predicate with a function \(f_B\) such that \(B(x, y)\)
2020-04-14 19:56:54 +03:00
is true if and only \(y = f_B(x)\). Then:
2020-05-03 03:01:21 +03:00
\(\) \Sigma = \cdots B(t_1, t_2) \cdots \quad \longrightarrow \quad
\Sigma' = \cdots {\it is}(f_B(t_1), t_2) \cdots \(\)
2020-04-14 19:56:54 +03:00
Similarly, if there is a function \(g_B\) such that \(B(x, y)\) if and only if
\(x = g_B(y)\) then
2020-05-03 03:01:21 +03:00
\(\) \Sigma = \cdots B(t_1, t_2) \cdots \quad \longrightarrow \quad
\Sigma' = \cdots {\it is}(t_1, g_B(t_2)) \cdots \(\)
2019-03-17 14:40:57 +02:00
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>
2020-05-03 03:01:21 +03:00
<pre class="displayed-code all-displayed-code code-font">
2021-02-03 11:32:42 +02:00
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Simplifications::reduce_predicates</span><button class="popup" onclick="togglePopup('usagePopup11')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup11">Usage of <span class="code-font"><span class="function-syntax">Calculus::Simplifications::reduce_predicates</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">&#167;2.14</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax">) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">binary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">bp</span><span class="plain-syntax"> = </span><a href="4-ap.html#SP10" class="function-link"><span class="function-syntax">Atoms::is_binary_predicate</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
2020-08-23 14:00:56 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">bp</span><span class="plain-syntax">)</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="plain-syntax">&lt;2; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++)</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="3-bp.html#SP7" class="function-link"><span class="function-syntax">BinaryPredicates::get_term_as_fn_of_other</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="identifier-syntax">j</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1-</span><span class="identifier-syntax">j</span><span class="plain-syntax">] = </span><a href="4-trm.html#SP4" class="function-link"><span class="function-syntax">Terms::new_function</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1-</span><span class="identifier-syntax">j</span><span class="plain-syntax">], </span><span class="constant-syntax">1</span><span class="plain-syntax">-</span><span class="identifier-syntax">j</span><span class="plain-syntax">);</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">predicate</span><span class="plain-syntax"> = </span><span class="identifier-syntax">STORE_POINTER_binary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">R_equality</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">PROPOSITION_EDITED</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
2019-03-17 14:40:57 +02:00
</pre>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP13" class="paragraph-anchor"></a><b>&#167;13. Eliminating determined variables (deduction). </b>The above operations will try to get as many variables as possible into a
2020-04-14 19:56:54 +03:00
form which makes their values explicit with a predicate \({\it is}(v, t)\).
2019-03-17 14:40:57 +02:00
We detect such equations and use them to eliminate the variable concerned,
where this is safe.
</p>
2020-05-03 03:01:21 +03:00
<pre class="definitions code-font"><span class="definition-keyword">define</span> <span class="constant-syntax">NOT_BOUND_AT_ALL</span><span class="plain-syntax"> </span><span class="constant-syntax">1</span>
<span class="definition-keyword">define</span> <span class="constant-syntax">BOUND_BY_EXISTS</span><span class="plain-syntax"> </span><span class="constant-syntax">2</span>
<span class="definition-keyword">define</span> <span class="constant-syntax">BOUND_BY_SOMETHING_ELSE</span><span class="plain-syntax"> </span><span class="constant-syntax">3</span>
2019-03-17 14:40:57 +02:00
</pre>
2020-05-03 03:01:21 +03:00
<pre class="displayed-code all-displayed-code code-font">
2021-02-03 11:32:42 +02:00
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Simplifications::eliminate_redundant_variables</span><button class="popup" onclick="togglePopup('usagePopup12')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup12">Usage of <span class="code-font"><span class="function-syntax">Calculus::Simplifications::eliminate_redundant_variables</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">&#167;2.14</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax">) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">level</span><span class="plain-syntax">, </span><span class="identifier-syntax">binding_status</span><span class="plain-syntax">[26], </span><span class="identifier-syntax">binding_level</span><span class="plain-syntax">[26], </span><span class="identifier-syntax">binding_sequence</span><span class="plain-syntax">[26];</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">position_of_binding</span><span class="plain-syntax">[26];</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">EliminateVariables:</span>
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="5-smp.html#SP13_1" class="named-paragraph-link"><span class="named-paragraph">Find out where and how variables are bound</span><span class="named-paragraph-number">13.1</span></a></span><span class="plain-syntax">;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">level</span><span class="plain-syntax"> = </span><span class="constant-syntax">0</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_opener</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">element</span><span class="plain-syntax">)) </span><span class="identifier-syntax">level</span><span class="plain-syntax">++;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_closer</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">element</span><span class="plain-syntax">)) </span><span class="identifier-syntax">level</span><span class="plain-syntax">--;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP10" class="function-link"><span class="function-syntax">Atoms::is_equality_predicate</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">)) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">j</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">j</span><span class="plain-syntax">=1; </span><span class="identifier-syntax">j</span><span class="plain-syntax">&gt;=0; </span><span class="identifier-syntax">j</span><span class="plain-syntax">--) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">var_to_sub</span><span class="plain-syntax"> = </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">].</span><span class="element-syntax">variable</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">var_in_other_term</span><span class="plain-syntax"> = </span><a href="4-trm.html#SP8" class="function-link"><span class="function-syntax">Terms::variable_underlying</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1-</span><span class="identifier-syntax">j</span><span class="plain-syntax">]));</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">var_is_redundant</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">, </span><span class="identifier-syntax">value_can_be_subbed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="5-smp.html#SP13_2" class="named-paragraph-link"><span class="named-paragraph">Decide if the variable is redundant, and if its value can safely be subbed</span><span class="named-paragraph-number">13.2</span></a></span><span class="plain-syntax">;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">var_is_redundant</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">value_can_be_subbed</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">permitted</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><a href="4-bas.html#SP13" class="function-link"><span class="function-syntax">Binding::substitute_term</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">var_to_sub</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1-</span><span class="identifier-syntax">j</span><span class="plain-syntax">],</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">permitted</span><span class="plain-syntax">, </span><span class="identifier-syntax">changed</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">permitted</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">PREDICATE_CALCULUS_WORKINGS</span><span class="plain-syntax">, </span><span class="string-syntax">"Substituting %c &lt;-- $0\n"</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">pcalc_vars</span><span class="plain-syntax">[</span><span class="identifier-syntax">var_to_sub</span><span class="plain-syntax">], &amp;(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1-</span><span class="identifier-syntax">j</span><span class="plain-syntax">]));</span>
<span class="plain-syntax"> </span><span class="comment-syntax"> first delete the </span>\({\it is}(v, t)\)<span class="comment-syntax"> predicate</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="comment-syntax"> then unbind the variable, by deleting its </span>\(\exists v\)<span class="comment-syntax"> quantifier</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">position_of_binding</span><span class="plain-syntax">[</span><span class="identifier-syntax">var_to_sub</span><span class="plain-syntax">]);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">PREDICATE_CALCULUS_WORKINGS</span><span class="plain-syntax">, </span><span class="string-syntax">"After deletion: $D\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">binding_status</span><span class="plain-syntax">[</span><span class="identifier-syntax">var_to_sub</span><span class="plain-syntax">] = </span><span class="constant-syntax">NOT_BOUND_AT_ALL</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="comment-syntax"> then substitute for all other occurrences of </span>\(v\)
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-bas.html#SP13" class="function-link"><span class="function-syntax">Binding::substitute_term</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">var_to_sub</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1-</span><span class="identifier-syntax">j</span><span class="plain-syntax">],</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">changed</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="comment-syntax"> since the proposition is now shorter by 2 atoms, this loop terminates</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">goto</span><span class="plain-syntax"> </span><span class="identifier-syntax">EliminateVariables</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> </span><a href="4-bas.html#SP7" class="function-link"><span class="function-syntax">Binding::renumber</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">); </span><span class="comment-syntax"> for the sake of tidiness</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
2019-03-17 14:40:57 +02:00
</pre>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP13_1" class="paragraph-anchor"></a><b>&#167;13.1. </b>The information-gathering stage:
2019-03-17 14:40:57 +02:00
</p>
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Find out where and how variables are bound</span><span class="named-paragraph-number">13.1</span></span><span class="comment-syntax"> =</span>
2020-05-03 03:01:21 +03:00
</p>
2019-03-17 14:40:57 +02:00
2020-05-03 03:01:21 +03:00
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">j</span><span class="plain-syntax">, </span><span class="identifier-syntax">c</span><span class="plain-syntax"> = </span><span class="constant-syntax">0</span><span class="plain-syntax">, </span><span class="identifier-syntax">level</span><span class="plain-syntax"> = </span><span class="constant-syntax">0</span><span class="plain-syntax">;</span>
2019-03-17 14:40:57 +02:00
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="plain-syntax">&lt;26; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">binding_status</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] = </span><span class="constant-syntax">NOT_BOUND_AT_ALL</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">binding_level</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] = </span><span class="constant-syntax">0</span><span class="plain-syntax">; </span><span class="identifier-syntax">binding_sequence</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] = </span><span class="constant-syntax">0</span><span class="plain-syntax">; </span><span class="identifier-syntax">position_of_binding</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> }</span>
2019-03-17 14:40:57 +02:00
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_opener</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">element</span><span class="plain-syntax">)) </span><span class="identifier-syntax">level</span><span class="plain-syntax">++;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_closer</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">element</span><span class="plain-syntax">)) </span><span class="identifier-syntax">level</span><span class="plain-syntax">--;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">)) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">v</span><span class="plain-syntax"> = </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="identifier-syntax">variable</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_existence_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">)) </span><span class="identifier-syntax">binding_status</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">] = </span><span class="constant-syntax">BOUND_BY_EXISTS</span><span class="plain-syntax">;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="identifier-syntax">binding_status</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">] = </span><span class="constant-syntax">BOUND_BY_SOMETHING_ELSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">binding_level</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">] = </span><span class="identifier-syntax">level</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">binding_sequence</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">] = </span><span class="identifier-syntax">c</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">position_of_binding</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">] = </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">c</span><span class="plain-syntax">++;</span>
<span class="plain-syntax"> }</span>
2019-03-17 14:40:57 +02:00
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="5-smp.html#SP13">&#167;13</a>.</li></ul>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP13_2" class="paragraph-anchor"></a><b>&#167;13.2. </b>At this point we have a predicate \({\it is}(t, f_A(f_B(\cdots s)))\). Should
2020-04-14 19:56:54 +03:00
the term \(t\) be a variable \(v\), which is bound by an \(\exists v\) atom at the
same level in its subexpression, then we can consider eliminating \(v\) by
substituting \(v = f_A(f_B(\cdots s))\).
2019-03-17 14:40:57 +02:00
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">But only if the term \(s\) underneath those functions does not make the equation
2020-04-14 19:56:54 +03:00
\({\it is}(v, f_A(f_B(\cdots s)))\) implicit. Suppose \(s\) depends
on a variable \(w\) which is bound and occurs {\it 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
2019-03-17 14:40:57 +02:00
a subtle condition passed by a whole class of possible values, or none.
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">The simplest example of such circularity is \({\it is}(v, v)\), true for all \(v\).
2020-04-14 19:56:54 +03:00
More problematic is \({\it is}(v, f_C(v))\), "\(v\) is the container of \(v\)",
2019-03-17 14:40:57 +02:00
which is never true. Still worse is
2020-04-14 19:56:54 +03:00
$$ \exists v: V_{=2} w: {\it 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 $$
2019-03-17 14:40:57 +02:00
which asserts "there are exactly two objects" &mdash; which is certainly not a
valid deduction, and might even be true.
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">Here <span class="extract"><span class="extract-syntax">var_to_sub</span></span> is \(v\) and <span class="extract"><span class="extract-syntax">var_in_other_term</span></span> is \(w\), or else they are \(-1\)
2019-03-17 14:40:57 +02:00
if no variables are present in their respective terms.
</p>
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Decide if the variable is redundant, and if its value can safely be subbed</span><span class="named-paragraph-number">13.2</span></span><span class="comment-syntax"> =</span>
2020-05-03 03:01:21 +03:00
</p>
2019-03-17 14:40:57 +02:00
2020-05-03 03:01:21 +03:00
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">var_to_sub</span><span class="plain-syntax"> &gt;= </span><span class="constant-syntax">0</span><span class="plain-syntax">)</span>
<span class="plain-syntax"> &amp;&amp; (</span><span class="identifier-syntax">binding_status</span><span class="plain-syntax">[</span><span class="identifier-syntax">var_to_sub</span><span class="plain-syntax">] == </span><span class="constant-syntax">BOUND_BY_EXISTS</span><span class="plain-syntax">)</span>
<span class="plain-syntax"> &amp;&amp; (</span><span class="identifier-syntax">binding_level</span><span class="plain-syntax">[</span><span class="identifier-syntax">var_to_sub</span><span class="plain-syntax">] == </span><span class="identifier-syntax">level</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">var_is_redundant</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
2019-03-17 14:40:57 +02:00
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">var_in_other_term</span><span class="plain-syntax"> &lt; </span><span class="constant-syntax">0</span><span class="plain-syntax">)</span>
<span class="plain-syntax"> || (</span><span class="identifier-syntax">binding_status</span><span class="plain-syntax">[</span><span class="identifier-syntax">var_in_other_term</span><span class="plain-syntax">] == </span><span class="constant-syntax">NOT_BOUND_AT_ALL</span><span class="plain-syntax">)</span>
<span class="plain-syntax"> || (</span><span class="identifier-syntax">binding_sequence</span><span class="plain-syntax">[</span><span class="identifier-syntax">var_in_other_term</span><span class="plain-syntax">] &lt; </span><span class="identifier-syntax">binding_sequence</span><span class="plain-syntax">[</span><span class="identifier-syntax">var_to_sub</span><span class="plain-syntax">]))</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">value_can_be_subbed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
2019-03-17 14:40:57 +02:00
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="5-smp.html#SP13">&#167;13</a>.</li></ul>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP14" class="paragraph-anchor"></a><b>&#167;14. Simplify non-relation (deduction). </b>As a result of the previous simplifications, it fairly often happens that we
2019-03-17 14:40:57 +02:00
find a term like
2020-05-03 03:01:21 +03:00
\(\) \lnot({\it thing}(t<span class="extract"><span class="extract-syntax">.component_parent</span></span>)) \(\)
2019-03-17 14:40:57 +02:00
in the proposition. This comes out of text such as "... not part of something",
2020-04-14 19:56:54 +03:00
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
2019-03-17 14:40:57 +02:00
left behind. But the negation is cumbersome, and makes the proposition harder
2020-05-03 03:01:21 +03:00
to assert or test. Exploiting the fact that <span class="extract"><span class="extract-syntax">component_parent</span></span> is a property
which is either the part-parent or else <span class="extract"><span class="extract-syntax">nothing</span></span>, we can simplify to:
\(\) {\it is}(t<span class="extract"><span class="extract-syntax">.component_parent</span></span>, <span class="extract"><span class="extract-syntax">nothing</span></span>) \(\)
2019-03-17 14:40:57 +02:00
And similar tricks can be pulled for other various-to-one-object predicates.
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">Formally, let \(B\) be a binary predicate supporting either a function \(f_B\)
2020-04-14 19:56:54 +03:00
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.
2019-03-17 14:40:57 +02:00
Then:
2020-05-03 03:01:21 +03:00
\(\) \Sigma = \cdots \lnot( K(f_B(t))) \cdots \quad \longrightarrow \quad
\Sigma' = \cdots {\it is}(f_B(t), <span class="extract"><span class="extract-syntax">nothing</span></span>) \cdots \(\)
</p>
<p class="commentary">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 <span class="extract"><span class="extract-syntax">nothing</span></span>.
</p>
<pre class="displayed-code all-displayed-code code-font">
2021-02-03 11:32:42 +02:00
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Simplifications::not_related_to_something</span><button class="popup" onclick="togglePopup('usagePopup13')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup13">Usage of <span class="code-font"><span class="function-syntax">Calculus::Simplifications::not_related_to_something</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">&#167;2.14</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax">) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> #</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">PRODUCE_NOTHING_VALUE</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">kind_atom</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-prp.html#SP22" class="function-link"><span class="function-syntax">Propositions::match</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="constant-syntax">3</span><span class="plain-syntax">,</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="constant-syntax">NEGATION_OPEN_ATOM</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">kind_atom</span><span class="plain-syntax">, </span><span class="identifier-syntax">kind_up_family</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">NEGATION_CLOSE_ATOM</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::get_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">kind_atom</span><span class="plain-syntax">);</span>
2020-08-11 17:07:58 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Kinds::Behaviour::is_subkind_of_object</span><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">)) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">binary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">bp</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">KIND_term</span><span class="plain-syntax"> = </span><span class="identifier-syntax">kind_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0];</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">KIND_term</span><span class="plain-syntax">.</span><span class="element-syntax">function</span><span class="plain-syntax">) </span><span class="identifier-syntax">bp</span><span class="plain-syntax"> = </span><span class="identifier-syntax">KIND_term</span><span class="plain-syntax">.</span><span class="element-syntax">function</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">bp</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">bp</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">Kinds::eq</span><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><a href="3-bp.html#SP7" class="function-link"><span class="function-syntax">BinaryPredicates::term_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="constant-syntax">1</span><span class="plain-syntax">)))) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP34" class="function-link"><span class="function-syntax">Propositions::ungroup_after</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove negation grouping</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove </span><span class="extract"><span class="extract-syntax">kind=K</span></span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="comment-syntax"> now insert equality predicate:</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><a href="4-ap.html#SP10" class="function-link"><span class="function-syntax">Atoms::binary_PREDICATE_new</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">R_equality</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">KIND_term</span><span class="plain-syntax">, </span><a href="4-trm.html#SP4" class="function-link"><span class="function-syntax">Terms::new_constant</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">PRODUCE_NOTHING_VALUE</span><span class="plain-syntax">())));</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">PROPOSITION_EDITED</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> #</span><span class="identifier-syntax">endif</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
2019-03-17 14:40:57 +02:00
</pre>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP15" class="paragraph-anchor"></a><b>&#167;15. Convert gerunds to nouns (deduction). </b>Suppose we write:
2019-03-17 14:40:57 +02:00
</p>
<blockquote>
<p>The funky thing to do is a stored action that varies.</p>
</blockquote>
2020-05-03 03:01:21 +03:00
<p class="commentary">and subsequently:
2019-03-17 14:40:57 +02:00
</p>
<blockquote>
<p>the funky thing to do is waiting</p>
</blockquote>
2020-05-03 03:01:21 +03:00
<p class="commentary">Here "waiting" is a gerund, and although it describes an action it is a
2019-03-17 14:40:57 +02:00
noun (thus a value) rather than a condition. We coerce its constant value
accordingly.
</p>
2020-05-03 03:01:21 +03:00
<pre class="displayed-code all-displayed-code code-font">
2020-08-25 01:11:39 +03:00
<span class="plain-syntax">#</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">IF_MODULE</span>
2021-02-03 11:32:42 +02:00
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Simplifications::convert_gerunds</span><button class="popup" onclick="togglePopup('usagePopup14')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup14">Usage of <span class="code-font"><span class="function-syntax">Calculus::Simplifications::convert_gerunds</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">&#167;2.14</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax">) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
2019-03-17 14:40:57 +02:00
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">)</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">2</span><span class="plain-syntax">))</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">i</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">i</span><span class="plain-syntax">&lt;2; </span><span class="identifier-syntax">i</span><span class="plain-syntax">++)</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Conditions::is_TEST_ACTION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">].</span><span class="element-syntax">constant</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">].</span><span class="identifier-syntax">constant</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Conditions::action_tested</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">].</span><span class="element-syntax">constant</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax">#</span><span class="identifier-syntax">endif</span>
2019-03-17 14:40:57 +02:00
</pre>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP16" class="paragraph-anchor"></a><b>&#167;16. Eliminate to have meaning property ownership (fudge). </b>The verb "to have" normally means ownership of a physical thing, but it
2019-03-17 14:40:57 +02:00
can also arise from text such as
</p>
<blockquote>
<p>the balloon has weight at most 1</p>
</blockquote>
2020-05-03 03:01:21 +03:00
<p class="commentary">where it's the numerical "weight" property which is owned by the balloon.
2019-03-17 14:40:57 +02:00
(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
2020-05-03 03:01:21 +03:00
\(\) {\hbox{\it at-most}}(<span class="extract"><span class="extract-syntax">weight</span></span>, 1)\land {\it is}(<span class="extract"><span class="extract-syntax">balloon</span></span>, f_H(<span class="extract"><span class="extract-syntax">weight</span></span>)) \(\)
where \(H\) is the predicate <span class="extract"><span class="extract-syntax">a_has_b_predicate</span></span>. As it stands, this
2019-03-17 14:40:57 +02:00
proposition will fail type-checking, because it contains an implicit
free variable &mdash; the object which owns the weight. We make this explicit
2020-05-03 03:01:21 +03:00
by removing ${\it is}(<span class="extract"><span class="extract-syntax">balloon</span></span>, f_H(<span class="extract"><span class="extract-syntax">weight</span></span>))$ and replacing all other
references to <span class="extract"><span class="extract-syntax">weight</span></span> with "the weight of <span class="extract"><span class="extract-syntax">balloon</span></span>".
2019-03-17 14:40:57 +02:00
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">This is a fudge because it assumes &mdash; possibly wrongly &mdash; that all
2019-03-17 14:40:57 +02:00
references to the weight are to the weight of the same thing. In
sufficiently contrived sentences, this wouldn't be true.
</p>
2020-05-03 03:01:21 +03:00
<pre class="displayed-code all-displayed-code code-font">
2020-08-25 01:11:39 +03:00
<span class="plain-syntax">#</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">CORE_MODULE</span>
2021-02-03 11:32:42 +02:00
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Simplifications::eliminate_to_have</span><button class="popup" onclick="togglePopup('usagePopup15')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup15">Usage of <span class="code-font"><span class="function-syntax">Calculus::Simplifications::eliminate_to_have</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">&#167;2.14</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax">) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP10" class="function-link"><span class="function-syntax">Atoms::is_equality_predicate</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">)) {</span>
2020-08-23 14:00:56 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">i</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">i</span><span class="plain-syntax">&lt;2; </span><span class="identifier-syntax">i</span><span class="plain-syntax">++)</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">].</span><span class="element-syntax">function</span><span class="plain-syntax">) &amp;&amp;</span>
<span class="plain-syntax"> (</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">].</span><span class="element-syntax">function</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">bp</span><span class="plain-syntax"> == </span><span class="identifier-syntax">a_has_b_predicate</span><span class="plain-syntax">) &amp;&amp;</span>
<span class="plain-syntax"> (</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">].</span><span class="element-syntax">function</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">fn_of</span><span class="plain-syntax">.</span><span class="element-syntax">constant</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1-</span><span class="identifier-syntax">i</span><span class="plain-syntax">].</span><span class="element-syntax">constant</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="identifier-syntax">spec</span><span class="plain-syntax"> = </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">].</span><span class="element-syntax">function</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">fn_of</span><span class="plain-syntax">.</span><span class="element-syntax">constant</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Rvalues::is_CONSTANT_construction</span><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">, </span><span class="identifier-syntax">CON_property</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="5-smp.html#SP16_1" class="named-paragraph-link"><span class="named-paragraph">Found an indication of who owns a property</span><span class="named-paragraph-number">16.1</span></a></span><span class="plain-syntax">;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax">#</span><span class="identifier-syntax">endif</span>
2019-03-17 14:40:57 +02:00
</pre>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP16_1" class="paragraph-anchor"></a><b>&#167;16.1. </b>So the current atom is \({\it is}(f_H(P), C)\) or \({\it is}(C, f_H(P))\)
2020-04-14 19:56:54 +03:00
(according to whether \(i\) is 0 or 1), for a property \(P\) and a constant
term \(C\).
2019-03-17 14:40:57 +02:00
</p>
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Found an indication of who owns a property</span><span class="named-paragraph-number">16.1</span></span><span class="comment-syntax"> =</span>
2020-05-03 03:01:21 +03:00
</p>
2019-03-17 14:40:57 +02:00
2020-05-03 03:01:21 +03:00
<pre class="displayed-code all-displayed-code code-font">
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">property</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prn</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Rvalues::to_property</span><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="identifier-syntax">po_spec</span><span class="plain-syntax"> =</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">Lvalues::new_PROPERTY_VALUE</span><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1-</span><span class="identifier-syntax">i</span><span class="plain-syntax">].</span><span class="element-syntax">constant</span><span class="plain-syntax">);</span>
2020-05-11 17:21:29 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">Node::set_text</span><span class="plain-syntax">(</span><span class="identifier-syntax">po_spec</span><span class="plain-syntax">, </span><span class="identifier-syntax">prn</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">name</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">no_substitutions_made</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="5-smp.html#SP17" class="function-link"><span class="function-syntax">Calculus::Simplifications::prop_substitute_prop_cons</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">prn</span><span class="plain-syntax">, </span><span class="identifier-syntax">po_spec</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">no_substitutions_made</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">no_substitutions_made</span><span class="plain-syntax"> &gt; </span><span class="constant-syntax">0</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">PROPOSITION_EDITED_REPEATING_CURRENT</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> }</span>
2019-03-17 14:40:57 +02:00
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="5-smp.html#SP16">&#167;16</a>.</li></ul>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP17" class="paragraph-anchor"></a><b>&#167;17. </b>Here we make the necessary substitution of "P" with "the P of C",
2020-04-14 19:56:54 +03:00
where \(P\) is a property and \(C\) the constant value of its owner. We make
2019-03-17 14:40:57 +02:00
this to every occurrence throughout the proposition, except for the one
2020-04-14 19:56:54 +03:00
in the original \({\it is}(f_H(P), C)\) atom, and we count the number of
2019-03-17 14:40:57 +02:00
changes made.
</p>
2020-05-03 03:01:21 +03:00
<pre class="displayed-code all-displayed-code code-font">
2020-08-25 01:11:39 +03:00
<span class="plain-syntax">#</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">CORE_MODULE</span>
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Simplifications::prop_substitute_prop_cons</span><button class="popup" onclick="togglePopup('usagePopup16')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup16">Usage of <span class="code-font"><span class="function-syntax">Calculus::Simplifications::prop_substitute_prop_cons</span></span>:<br/><a href="5-smp.html#SP16_1">&#167;16.1</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">property</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prn</span><span class="plain-syntax">,</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="identifier-syntax">po_spec</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">count</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">not_this</span><span class="plain-syntax">) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">j</span><span class="plain-syntax">, </span><span class="identifier-syntax">c</span><span class="plain-syntax"> = </span><span class="constant-syntax">0</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">)</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pl</span><span class="plain-syntax"> != </span><span class="identifier-syntax">not_this</span><span class="plain-syntax">)</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="function-syntax">&lt;pl-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax">; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> *</span><span class="identifier-syntax">pt</span><span class="plain-syntax"> = &amp;(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">]);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">while</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">function</span><span class="plain-syntax">) </span><span class="identifier-syntax">pt</span><span class="plain-syntax"> = &amp;(</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">function</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">fn_of</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">constant</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="reserved-syntax">continue</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Rvalues::is_CONSTANT_construction</span><span class="plain-syntax">(</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">constant</span><span class="plain-syntax">, </span><span class="identifier-syntax">CON_property</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">property</span><span class="plain-syntax"> *</span><span class="identifier-syntax">tprn</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">tprn</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Rvalues::to_property</span><span class="plain-syntax">(</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">constant</span><span class="plain-syntax">);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">tprn</span><span class="plain-syntax"> == </span><span class="identifier-syntax">prn</span><span class="plain-syntax">) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">constant</span><span class="plain-syntax"> = </span><span class="identifier-syntax">po_spec</span><span class="plain-syntax">;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">c</span><span class="plain-syntax">++;</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> *</span><span class="identifier-syntax">count</span><span class="plain-syntax"> = </span><span class="identifier-syntax">c</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax">#</span><span class="identifier-syntax">endif</span>
2019-03-17 14:40:57 +02:00
</pre>
2020-08-18 00:57:45 +03:00
<p class="commentary firstcommentary"><a id="SP18" class="paragraph-anchor"></a><b>&#167;18. Turn all rooms to everywhere (fudge). </b>This rather special rule handles the consequences of the English word
2019-03-17 14:40:57 +02:00
"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>
2020-05-03 03:01:21 +03:00
<p class="commentary">means the sky is in every room, not that the sky is equal to every room.
2019-03-17 14:40:57 +02:00
Since the literal reading would make no useful sense, Inform fudges the
proposition to change it to the idiomatic one.
2020-05-03 03:01:21 +03:00
\(\) \Sigma = \cdots \forall v\in\lbrace v\mid{\it room}(v)}\rbrace : {\it is}(v, t) \quad \longrightarrow \quad
\Sigma' = \cdots {\it everywhere}(t) \(\)
\(\) \Sigma = \cdots \forall v\in\lbrace v\mid{\it room}(v)}\rbrace : {\it is}(t, v) \quad \longrightarrow \quad
\Sigma' = \cdots {\it everywhere}(t) \(\)
\(\) \Sigma = \cdots \not\forall v\in\lbrace v\mid{\it room}(v)}\rbrace : {\it is}(v, t) \quad \longrightarrow \quad
\Sigma' = \cdots \lnot({\it everywhere}(t)) \(\)
\(\) \Sigma = \cdots \not\forall v\in\lbrace v\mid{\it room}(v)}\rbrace : {\it is}(t, v) \quad \longrightarrow \quad
\Sigma' = \cdots \lnot({\it everywhere}(t)) \(\)
2019-03-17 14:40:57 +02:00
</p>
2020-05-03 03:01:21 +03:00
<p class="commentary">Note that we match this only at the end of a proposition, where \(v\) can
2019-03-17 14:40:57 +02:00
have no other consequence.
</p>
2020-05-03 03:01:21 +03:00
<pre class="displayed-code all-displayed-code code-font">
2021-02-03 11:32:42 +02:00
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Simplifications::is_all_rooms</span><button class="popup" onclick="togglePopup('usagePopup17')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup17">Usage of <span class="code-font"><span class="function-syntax">Calculus::Simplifications::is_all_rooms</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">&#167;2.14</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax">) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> #</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">IF_MODULE</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">, *</span><span class="identifier-syntax">k_atom</span><span class="plain-syntax">, *</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><a href="4-prp.html#SP22" class="function-link"><span class="function-syntax">Propositions::match</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="constant-syntax">6</span><span class="plain-syntax">,</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">k_atom</span><span class="plain-syntax">, </span><span class="identifier-syntax">kind_up_family</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">DOMAIN_CLOSE_ATOM</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">END_PROP_HERE</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">)) &amp;&amp;</span>
<span class="plain-syntax"> ((</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_forall_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">)) || (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_notall_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">))) &amp;&amp;</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> (</span><span class="identifier-syntax">Kinds::eq</span><span class="plain-syntax">(</span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::get_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">k_atom</span><span class="plain-syntax">), </span><span class="identifier-syntax">K_room</span><span class="plain-syntax">)) &amp;&amp;</span>
<span class="plain-syntax"> (</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">2</span><span class="plain-syntax">) &amp;&amp;</span>
<span class="plain-syntax"> (</span><span class="identifier-syntax">RETRIEVE_POINTER_binary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">predicate</span><span class="plain-syntax">) == </span><span class="identifier-syntax">R_equality</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">j</span><span class="plain-syntax">, </span><span class="identifier-syntax">v</span><span class="plain-syntax"> = </span><span class="identifier-syntax">k_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">variable</span><span class="plain-syntax">;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="plain-syntax">&lt;2; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1-</span><span class="identifier-syntax">j</span><span class="plain-syntax">].</span><span class="element-syntax">variable</span><span class="plain-syntax"> == </span><span class="identifier-syntax">v</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">v</span><span class="plain-syntax"> &gt;= </span><span class="constant-syntax">0</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove </span><span class="extract"><span class="extract-syntax">QUANTIFIER_ATOM</span></span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove </span><span class="extract"><span class="extract-syntax">DOMAIN_OPEN_ATOM</span></span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove </span><span class="extract"><span class="extract-syntax">kind=K</span></span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove </span><span class="extract"><span class="extract-syntax">DOMAIN_CLOSE_ATOM</span></span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove </span><span class="extract"><span class="extract-syntax">PREDICATE_ATOM</span></span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_notall_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">, </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">NEGATION_CLOSE_ATOM</span><span class="plain-syntax">));</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">WherePredicates::everywhere_up</span><span class="plain-syntax">(</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">]));</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_notall_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">, </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">NEGATION_OPEN_ATOM</span><span class="plain-syntax">));</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">PROPOSITION_EDITED</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><a href="4-prp.html#SP22" class="function-link"><span class="function-syntax">Propositions::match</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="constant-syntax">6</span><span class="plain-syntax">,</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">k_atom</span><span class="plain-syntax">, </span><span class="identifier-syntax">kind_up_family</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">DOMAIN_CLOSE_ATOM</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">END_PROP_HERE</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">)) &amp;&amp;</span>
<span class="plain-syntax"> (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_nonexistence_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">)) &amp;&amp;</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> (</span><span class="identifier-syntax">Kinds::eq</span><span class="plain-syntax">(</span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::get_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">k_atom</span><span class="plain-syntax">), </span><span class="identifier-syntax">K_room</span><span class="plain-syntax">)) &amp;&amp;</span>
<span class="plain-syntax"> (</span><a href="2-kp.html#SP4" class="function-link"><span class="function-syntax">KindPredicates::is_composited_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">k_atom</span><span class="plain-syntax">)) &amp;&amp;</span>
<span class="plain-syntax"> (</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">2</span><span class="plain-syntax">) &amp;&amp;</span>
<span class="plain-syntax"> (</span><span class="identifier-syntax">RETRIEVE_POINTER_binary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">predicate</span><span class="plain-syntax">) == </span><span class="identifier-syntax">R_equality</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">j</span><span class="plain-syntax">, </span><span class="identifier-syntax">v</span><span class="plain-syntax"> = </span><span class="identifier-syntax">k_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">variable</span><span class="plain-syntax">;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="plain-syntax">&lt;2; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1-</span><span class="identifier-syntax">j</span><span class="plain-syntax">].</span><span class="element-syntax">variable</span><span class="plain-syntax"> == </span><span class="identifier-syntax">v</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">v</span><span class="plain-syntax"> &gt;= </span><span class="constant-syntax">0</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove </span><span class="extract"><span class="extract-syntax">QUANTIFIER_ATOM</span></span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove </span><span class="extract"><span class="extract-syntax">DOMAIN_OPEN_ATOM</span></span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove </span><span class="extract"><span class="extract-syntax">kind=K</span></span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove </span><span class="extract"><span class="extract-syntax">DOMAIN_CLOSE_ATOM</span></span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove </span><span class="extract"><span class="extract-syntax">PREDICATE_ATOM</span></span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">WherePredicates::nowhere_up</span><span class="plain-syntax">(</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">]));</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">PROPOSITION_EDITED</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> #</span><span class="identifier-syntax">endif</span>
<span class="plain-syntax">}</span>
2021-02-03 11:32:42 +02:00
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Simplifications::everywhere_and_nowhere</span><button class="popup" onclick="togglePopup('usagePopup18')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup18">Usage of <span class="code-font"><span class="function-syntax">Calculus::Simplifications::everywhere_and_nowhere</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">&#167;2.14</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax">) {</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> #</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">IF_MODULE</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">, *</span><span class="identifier-syntax">k_atom</span><span class="plain-syntax">, *</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><a href="4-prp.html#SP22" class="function-link"><span class="function-syntax">Propositions::match</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="constant-syntax">6</span><span class="plain-syntax">,</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">k_atom</span><span class="plain-syntax">, </span><span class="identifier-syntax">kind_up_family</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">DOMAIN_CLOSE_ATOM</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="constant-syntax">END_PROP_HERE</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">)) &amp;&amp;</span>
<span class="plain-syntax"> ((</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_forall_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">)) ||</span>
<span class="plain-syntax"> (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_notall_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">)) ||</span>
<span class="plain-syntax"> (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_nonexistence_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">))) &amp;&amp;</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> (</span><span class="identifier-syntax">Kinds::eq</span><span class="plain-syntax">(</span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::get_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">k_atom</span><span class="plain-syntax">), </span><span class="identifier-syntax">K_room</span><span class="plain-syntax">)) &amp;&amp;</span>
<span class="plain-syntax"> (</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">2</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">binary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">bp</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RETRIEVE_POINTER_binary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">predicate</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (((</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_nonexistence_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">bp</span><span class="plain-syntax"> == </span><span class="identifier-syntax">R_containment</span><span class="plain-syntax">)) ||</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> (</span><span class="identifier-syntax">bp</span><span class="plain-syntax"> == </span><span class="identifier-syntax">room_containment_predicate</span><span class="plain-syntax">)) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">j</span><span class="plain-syntax">, </span><span class="identifier-syntax">v</span><span class="plain-syntax"> = </span><span class="identifier-syntax">k_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">variable</span><span class="plain-syntax">;</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="plain-syntax">&lt;2; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++) {</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1-</span><span class="identifier-syntax">j</span><span class="plain-syntax">].</span><span class="element-syntax">variable</span><span class="plain-syntax"> == </span><span class="identifier-syntax">v</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">v</span><span class="plain-syntax"> &gt;= </span><span class="constant-syntax">0</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove </span><span class="extract"><span class="extract-syntax">QUANTIFIER_ATOM</span></span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove </span><span class="extract"><span class="extract-syntax">DOMAIN_OPEN_ATOM</span></span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove </span><span class="extract"><span class="extract-syntax">kind=K</span></span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove </span><span class="extract"><span class="extract-syntax">DOMAIN_CLOSE_ATOM</span></span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove </span><span class="extract"><span class="extract-syntax">PREDICATE_ATOM</span></span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_notall_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">, </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">NEGATION_CLOSE_ATOM</span><span class="plain-syntax">));</span>
2020-08-25 01:11:39 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">new_atom</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_nonexistence_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">new_atom</span><span class="plain-syntax"> = </span><span class="identifier-syntax">WherePredicates::nowhere_up</span><span class="plain-syntax">(</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">]);</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="reserved-syntax">else</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">new_atom</span><span class="plain-syntax"> = </span><span class="identifier-syntax">WherePredicates::everywhere_up</span><span class="plain-syntax">(</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">]);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">, </span><span class="identifier-syntax">new_atom</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_notall_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">, </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">NEGATION_OPEN_ATOM</span><span class="plain-syntax">));</span>
2020-05-03 03:01:21 +03:00
<span class="plain-syntax"> </span><span class="identifier-syntax">PROPOSITION_EDITED</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> #</span><span class="identifier-syntax">endif</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
2019-03-17 14:40:57 +02:00
</pre>
2020-05-03 03:01:21 +03:00
<nav role="progress"><div class="progresscontainer">
2021-02-03 11:32:42 +02:00
<ul class="progressbar"><li class="progressprev"><a href="5-sc.html">&#10094;</a></li><li class="progresschapter"><a href="P-wtmd.html">P</a></li><li class="progresschapter"><a href="1-cm.html">1</a></li><li class="progresschapter"><a href="2-up.html">2</a></li><li class="progresschapter"><a href="3-bpf.html">3</a></li><li class="progresschapter"><a href="4-trm.html">4</a></li><li class="progresscurrentchapter">5</li><li class="progresssection"><a href="5-sc.html">sc</a></li><li class="progresscurrent">smp</li><li class="progressnextoff">&#10095;</li></ul></div>
2020-05-03 03:01:21 +03:00
</nav><!--End of weave-->
2019-03-17 14:40:57 +02:00
2020-03-19 02:11:25 +02:00
</main>
2019-03-17 14:40:57 +02:00
</body>
</html>