mirror of
https://github.com/ganelson/inform.git
synced 2024-07-05 00:24:22 +03:00
1402 lines
246 KiB
HTML
1402 lines
246 KiB
HTML
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
|
|
<html>
|
|
<head>
|
|
<title>Simplifications</title>
|
|
<link href="../docs-assets/Breadcrumbs.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<meta name="viewport" content="width=device-width initial-scale=1">
|
|
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
|
|
<meta http-equiv="Content-Language" content="en-gb">
|
|
|
|
<link href="../docs-assets/Contents.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Progress.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Navigation.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Fonts.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Base.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<script>
|
|
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 src="http://code.jquery.com/jquery-1.12.4.min.js"
|
|
integrity="sha256-ZosEbRLbNQzLpnKIkEdrPv7lOy9C27hHQ+Xp8a4MxAQ=" crossorigin="anonymous"></script>
|
|
|
|
<script src="../docs-assets/Bigfoot.js"></script>
|
|
<link href="../docs-assets/Bigfoot.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<script>
|
|
function togglePopup(material_id) {
|
|
var popup = document.getElementById(material_id);
|
|
popup.classList.toggle("show");
|
|
}
|
|
</script>
|
|
|
|
<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">
|
|
|
|
</head>
|
|
<body class="commentary-font">
|
|
<nav role="navigation">
|
|
<h1><a href="../index.html">
|
|
<img src="../docs-assets/Inform.png" height=72">
|
|
</a></h1>
|
|
<ul><li><a href="../index.html">home</a></li>
|
|
</ul><h2>Compiler</h2><ul>
|
|
<li><a href="../structure.html">structure</a></li>
|
|
<li><a href="../inbuildn.html">inbuild</a></li>
|
|
<li><a href="../inform7n.html">inform7</a></li>
|
|
<li><a href="../intern.html">inter</a></li>
|
|
<li><a href="../services.html">services</a></li>
|
|
<li><a href="../secrets.html">secrets</a></li>
|
|
</ul><h2>Other Tools</h2><ul>
|
|
<li><a href="../inblorbn.html">inblorb</a></li>
|
|
<li><a href="../indocn.html">indoc</a></li>
|
|
<li><a href="../inform6.html">inform6</a></li>
|
|
<li><a href="../inpolicyn.html">inpolicy</a></li>
|
|
<li><a href="../inrtpsn.html">inrtps</a></li>
|
|
</ul><h2>Resources</h2><ul>
|
|
<li><a href="../extensions.html">extensions</a></li>
|
|
<li><a href="../kits.html">kits</a></li>
|
|
</ul><h2>Repository</h2><ul>
|
|
<li><a href="https://github.com/ganelson/inform"><img src="../docs-assets/github.png" height=18> github</a></li>
|
|
</ul><h2>Related Projects</h2><ul>
|
|
<li><a href="../../../inweb/index.html">inweb</a></li>
|
|
<li><a href="../../../intest/index.html">intest</a></li>
|
|
|
|
</ul>
|
|
</nav>
|
|
<main role="main">
|
|
<!--Weave of 'Simplifications' generated by Inweb-->
|
|
<div class="breadcrumbs">
|
|
<ul class="crumbs"><li><a href="../index.html">Home</a></li><li><a href="../services.html">Services</a></li><li><a href="index.html">calculus</a></li><li><a href="index.html#5">Chapter 5: Sentences</a></li><li><b>Simplifications</b></li></ul></div>
|
|
<p class="purpose">A set of operations which rewrite propositions to make them easier or quicker to test at run-time without changing their meaning.</p>
|
|
|
|
<ul class="toc"><li><a href="5-smp.html#SP1">§1. Golden rules</a></li><li><a href="5-smp.html#SP2">§2. Simplify the nothing constant (fudge)</a></li><li><a href="5-smp.html#SP3">§3. Use listed-in predicates (deduction)</a></li><li><a href="5-smp.html#SP4">§4. Simplify negated determiners (deduction)</a></li><li><a href="5-smp.html#SP6">§6. Simplify negated satisfiability (deduction)</a></li><li><a href="5-smp.html#SP7">§7. Make kind requirements explicit (deduction)</a></li><li><a href="5-smp.html#SP8">§8. Remove redundant kind predicates (deduction)</a></li><li><a href="5-smp.html#SP10">§10. Turn binary predicates the right way round (deduction)</a></li><li><a href="5-smp.html#SP11">§11. Simplify region containment (fudge)</a></li><li><a href="5-smp.html#SP12">§12. Reduce binary predicates (deduction)</a></li><li><a href="5-smp.html#SP13">§13. Eliminating determined variables (deduction)</a></li><li><a href="5-smp.html#SP14">§14. Simplify non-relation (deduction)</a></li><li><a href="5-smp.html#SP15">§15. Convert gerunds to nouns (deduction)</a></li><li><a href="5-smp.html#SP16">§16. Eliminate to have meaning property ownership (fudge)</a></li><li><a href="5-smp.html#SP18">§18. Turn all rooms to everywhere (fudge)</a></li><li><a href="5-smp.html#SP19">§19. Everywhere and nowhere (fudge)</a></li></ul><hr class="tocbar">
|
|
|
|
<p class="commentary firstcommentary"><a id="SP1" class="paragraph-anchor"></a><b>§1. Golden rules. </b>The following functions all take a propeosition \(\Sigma\) in the parameter
|
|
<span class="extract"><span class="extract-syntax">prop</span></span>, and return \(\Sigma'\); they set the flag pointed to by <span class="extract"><span class="extract-syntax">changed</span></span> if
|
|
they in fact change something. (They are allowed to modify or destroy the
|
|
data structure pointed to by <span class="extract"><span class="extract-syntax">prop</span></span>, or indeed to change it in place and
|
|
return the same pointer.)
|
|
</p>
|
|
|
|
<ul class="items"><li>(1) \(\Sigma'\) must remain a syntactically correct proposition;
|
|
</li><li>(2) \(\Sigma'\) has the same number of free variables as \(\Sigma\), and
|
|
</li><li>(3) \(\Sigma\) semantically entails \(\Sigma'\) and vice versa, that is, for
|
|
all possible values of any free variables \(\Sigma'\) is true if and only
|
|
if \(\Sigma\) is.
|
|
</li></ul>
|
|
<p class="commentary">Rules (1) and (2) are always strictly obeyed. If (3) is also strictly obeyed,
|
|
we call the function a "deduction": but if we bend rule (3) to accommodate
|
|
the quirky nature of language, we call it a "fudge".
|
|
</p>
|
|
|
|
<p class="commentary">Note that we do not require \(\Sigma'\) to be simpler than \(\Sigma\) in any
|
|
crude sense (say, its number of atoms). We want it to be more convenient
|
|
to test at run-time than \(\Sigma\) would have been, that's all. But usually
|
|
it's a good idea to reduce the number of different variables occurring in it.
|
|
</p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP2" class="paragraph-anchor"></a><b>§2. Simplify the nothing constant (fudge). </b>The word "nothing" is sometimes a noun ("the holder of the oak tree is
|
|
nothing"), sometimes a determiner ("nothing is in the box"). This
|
|
doesn't arise with other no- words, such as "nowhere" and "nobody", since
|
|
those are not allowed as nouns in Inform.
|
|
</p>
|
|
|
|
<p class="commentary">Here we look for the noun form as one term in a binary predicate, and convert
|
|
it to the determiner form unless the predicate is equality. Thus "X is nothing"
|
|
is allowed to use the noun form, "X contains nothing" has to use the
|
|
determiner form.<sup id="fnref:1"><a href="#fn:1" rel="footnote">1</a></sup>
|
|
</p>
|
|
|
|
<ul class="footnotetexts"><li class="footnote" id="fn:1"><p class="inwebfootnote"><sup id="fnref:1"><a href="#fn:1" rel="footnote">1</a></sup> 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, for example in Peter Hammill's lyrics to "Flight": "He say nothing
|
|
is quite what it seems / I say nothing is nothing."
|
|
<a href="#fnref:1" title="return to text"> ↩</a></p></li></ul>
|
|
<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">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">Simplifications::nothing_constant</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">§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="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">DETECT_NOTHING_CALCULUS_CALLBACK</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_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><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>
|
|
<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">-></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"><2; </span><span class="identifier-syntax">i</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">C</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">(&(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-></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="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">DETECT_NOTHING_CALCULUS_CALLBACK</span><span class="plain-syntax">(</span><span class="identifier-syntax">C</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>
|
|
<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="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>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP2_1" class="paragraph-anchor"></a><b>§2.1. </b>Formally, if \(B\) is a predicate other than equality, and \(N\) is the "nothing" constant,
|
|
$$ \Sigma = \cdots B(t, f_X(f_Y(\cdots(N))))\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 $$
|
|
where \(v\) is unused in \(\Sigma\), and — note the difference in placing —
|
|
$$ \Sigma = \cdots B(f_X(f_Y(\cdots(N))), 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 $$
|
|
where \(K_1\) and \(K_2\) are the kinds of terms 1 and 2 in the predicate \(B\).
|
|
</p>
|
|
|
|
<p class="commentary">The difference in where we place the quantifier is important in double-negative
|
|
sentences. Consider these:
|
|
</p>
|
|
|
|
<blockquote>
|
|
<p>[1] the box does not contain nothing</p>
|
|
</blockquote>
|
|
|
|
<p class="commentary">which produces \(\Sigma = \lnot({\it contains}(B, N))\). Here,
|
|
<span class="extract"><span class="extract-syntax">nothing</span></span> is part of the object phrase, not the subject phrase, and we need
|
|
to quantify it within the OP — which means, within the negation, because our
|
|
recipe for negated sentences was (roughly) SP \(\land\lnot(\) OP \(\land\) VP\()\).
|
|
We thus make \(\Sigma' = \lnot(\not\exists x:{\it contains}(B, x))\),
|
|
although later simplification converts that to \(\exists x: {\it contains}(B, x)\),
|
|
just as if the original sentence had been "the box contains something".
|
|
On the other hand,
|
|
</p>
|
|
|
|
<blockquote>
|
|
<p>[2] nothing does not annoy Peter</p>
|
|
</blockquote>
|
|
|
|
<p class="commentary">produces \(\Sigma = \lnot({\it annoys}(N, P))\), and now we have
|
|
to quantify as \(\Sigma' = \not\exists x: \lnot({\it annoys}(x, P))\).
|
|
</p>
|
|
|
|
<p class="commentary">Double-negatives are a little odd. If natural language were really the same as
|
|
predicate logic with some grunting sounds for decoration, then a double negative
|
|
would always be a positive. In fact that isn't always quite true,<sup id="fnref:2"><a href="#fn:2" rel="footnote">2</a></sup> but Inform
|
|
does consider a double negative to be a positive.
|
|
</p>
|
|
|
|
<ul class="footnotetexts"><li class="footnote" id="fn:2"><p class="inwebfootnote"><sup id="fnref:2"><a href="#fn:2" rel="footnote">2</a></sup> In 18th-century English, for example, the double negative was a way to
|
|
emphasise rather than undo negation, just as characters in Aaron Sorkin dramas
|
|
are always saying "not for nothing, but..." to mean "it's nothing, but...".
|
|
<a href="#fnref:2" title="return to text"> ↩</a></p></li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP2_2" class="paragraph-anchor"></a><b>§2.2. </b>The code is simpler than the explanation:
|
|
</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>
|
|
</p>
|
|
|
|
<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">(&(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-></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">new_var</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">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>
|
|
<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>
|
|
<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>
|
|
</pre>
|
|
<ul class="endnotetexts"><li>This code is used in <a href="5-smp.html#SP2">§2</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP3" class="paragraph-anchor"></a><b>§3. Use listed-in predicates (deduction). </b>Suppose the source text reads:
|
|
</p>
|
|
|
|
<blockquote>
|
|
<p>if X is a density listed in the Table of Solid Stuff, ...</p>
|
|
</blockquote>
|
|
|
|
<p class="commentary">Inform parses "a density listed in the Table of Solid Stuff" as a single
|
|
specification, with references to the density column and the Solid Stuff
|
|
table. In terms of our calculus, this is just another constant, which we'll call \(L\).
|
|
At this point the sentence looks like:
|
|
$$ {\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. So we must make
|
|
its nature explicit. Every table column has an associated binary predicate,
|
|
and we rewrite:
|
|
$$ \exists v: {\it number}(v)\land {\it listed}_{\it density}(v, T)\land {\it is}(v, X) $$
|
|
This looks extravagant, but later simplification will reduce it to
|
|
\({\it listed}_{\it density}(X, T)\).
|
|
</p>
|
|
|
|
<p class="commentary">More formally suppose we write \(L(C, T)\) for the constant representing "a
|
|
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\)
|
|
column. Then:
|
|
$$ \Sigma = \cdots P(\dots L(C, T)\dots) \cdots \quad \longrightarrow \quad \Sigma' = \cdots \exists v: K(v)\land {\it listed}_C(v, T)\land P(\dots v\dots) \cdots $$
|
|
where the variable \(v\) has replaced the constant \(L(C, T)\) underlying one
|
|
of the terms of \(P\).
|
|
</p>
|
|
|
|
<p class="commentary">Note that this can act twice on the same predicate, if such terms occur
|
|
twice. For example,
|
|
</p>
|
|
|
|
<blockquote>
|
|
<p>if a crispiness listed in the Table of Salad Stuff is a density listed in the Table of Solid Stuff, ...</p>
|
|
</blockquote>
|
|
|
|
<p class="commentary">generates \({\it is}(L(C_1, T_1), L(C_2, T_2))\). As it happens, Inform can't
|
|
compile this efficiently and will produce a problem message to say so, but
|
|
the code here does generate the correct proposition,
|
|
$$ \exists x: {\it number}(x)\land {\it listed}_{\it Salad}(x, T_1)\land {\it listed}_{\it Solid}(x, T_2). $$
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<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">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">Simplifications::use_listed_in</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">§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="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>
|
|
<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"><pl-></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">(&(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-></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><span class="identifier-syntax">spec</span><span class="plain-syntax">) && (</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">) &&</span>
|
|
<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>
|
|
<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">-></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">-></span><span class="identifier-syntax">down</span><span class="plain-syntax">-></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">) && (</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>
|
|
<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">-></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">(&(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-></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">nv_term</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">LocalVariables::add_table_lookup</span><span class="plain-syntax">();</span>
|
|
<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>
|
|
<span class="plain-syntax">#</span><span class="identifier-syntax">endif</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP4" class="paragraph-anchor"></a><b>§4. Simplify negated determiners (deduction). </b>The negation atom is worth removing wherever possible, since we want to
|
|
keep propositions in a flat conjunction form if we can, and the negation
|
|
of a string of atoms is therefore a bad thing. We therefore change thus:
|
|
$$ \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_{<5} y\) becomes \(V_{\geq 5} y\).
|
|
</p>
|
|
|
|
<p class="commentary">A curiosity here is that when simplifying during sentence conversion, we
|
|
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
|
|
they make some of our later simplifications more applicable.
|
|
</p>
|
|
|
|
<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">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">Simplifications::negated_determiners_nonex</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">§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">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>
|
|
<span class="plain-syntax">}</span>
|
|
|
|
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">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>
|
|
<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>
|
|
<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>
|
|
<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">, &</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><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">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>
|
|
<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>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP5" class="paragraph-anchor"></a><b>§5. </b>And the following useful function actually performs the change. The only
|
|
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 —
|
|
the proposition means the same wherever we put it — the assert-propositions
|
|
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 — \(v\) being
|
|
a container, say — and the \(\phi\) outside the braces should then contain
|
|
predicates which can be asserted.
|
|
</p>
|
|
|
|
<p class="commentary">In practice that's way too hard for this function to handle. If <span class="extract"><span class="extract-syntax">add_domain_brackets</span></span>
|
|
is true, then it converts
|
|
$$ \lnot(\exists v: \cdots) \quad\longrightarrow\quad \not\exists v\in \lbrace v\mid \cdots\rbrace $$
|
|
— that is, it will make the entire negated subproposition the domain of the
|
|
quantifier. If <span class="extract"><span class="extract-syntax">add_domain_brackets</span></span> is false, the function will return a
|
|
syntactically incorrect proposition lacking the domain brackets, and it's
|
|
the caller's responsibility to put that right.
|
|
</p>
|
|
|
|
<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">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">Simplifications::prop_ungroup_and_negate_determiner</span></span>:<br/><a href="5-smp.html#SP4">§4</a>, <a href="5-smp.html#SP6">§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="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><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">add_domain_brackets</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">quant_atom</span><span class="plain-syntax">, *</span><span class="identifier-syntax">last</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">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>
|
|
<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">, &</span><span class="identifier-syntax">quant_atom</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">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>
|
|
<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">, &</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><span class="identifier-syntax">fnd</span><span class="plain-syntax">) {</span>
|
|
<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">-></span><span class="element-syntax">quant</span><span class="plain-syntax">;</span>
|
|
<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>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">quant_atom</span><span class="plain-syntax">-></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">, &</span><span class="identifier-syntax">last</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove negation brackets</span>
|
|
<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">) && (</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>
|
|
<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 brackets</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="plain-syntax"> </span><span class="string-syntax">"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>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP6" class="paragraph-anchor"></a><b>§6. Simplify negated satisfiability (deduction). </b>When simplifying converted sentences, we chose not to use the
|
|
<span class="extract"><span class="extract-syntax">Simplifications::negated_determiners</span></span> tactic on existence quantifiers \(\exists v\),
|
|
partly because it's tricky to establish their domain in a way helpful to
|
|
the rest of Inform.
|
|
</p>
|
|
|
|
<p class="commentary">Here we handle a simple case which occurs frequently and where we can indeed
|
|
identify the domain well:
|
|
$$ \Sigma = \lnot (\exists v: K(v)\land P) \quad \longrightarrow \quad \Sigma' = \not\exists v\in\lbrace v\mid K(v)\rbrace: P $$
|
|
where \(K\) is a kind, and \(P\) is any single predicate other than equality.
|
|
(In the case of equality, we'd rather leave matters as they stand, because
|
|
substitution will later eliminate all of this anyway.)
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">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">Simplifications::negated_satisfiable</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">§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">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>
|
|
<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>
|
|
<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">, &</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">, &</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">, &</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">)) &&</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="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">) &&</span>
|
|
<span class="plain-syntax"> (</span><span class="identifier-syntax">kind_atom</span><span class="plain-syntax">-></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">-></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">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>
|
|
<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>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP7" class="paragraph-anchor"></a><b>§7. Make kind requirements explicit (deduction). </b>Many predicates contain implicit requirements about the kinds of their terms.
|
|
For instance, if \(R\) relates a door to a number, then \(R(x,y)\) can only be
|
|
true if \(x\) is a door and \(y\) is a number. We insert these requirements
|
|
explicitly in order to defend the code testing \(R\); it ensures we never have
|
|
to test bogus values. We need do this only for variables, as with more
|
|
constants and functions type-checking will certainly be able to test their
|
|
kind in any event (whereas a free variable is anonymous enough that we can't
|
|
necessarily know by other means).
|
|
</p>
|
|
|
|
<p class="commentary">Formally, let \(K_1\) and \(K_2\) be the kinds of value of terms 1 and 2 of the
|
|
binary predicate \(R\). Let \(v\) be a variable. Then:
|
|
$$ \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) $$
|
|
and therefore, if both cases occur,
|
|
$$ \Sigma = \cdots R(v, w)\cdots \quad \longrightarrow \quad \Sigma' = \cdots K_1(v)\land K_2(w)\land R(v, w) $$
|
|
</p>
|
|
|
|
<p class="commentary">Some of these new kind atoms are unnecessary, but <span class="extract"><span class="extract-syntax">Simplifications::redundant_kinds</span></span> will
|
|
detect and remove those.
|
|
</p>
|
|
|
|
<p class="commentary">Why do we do this for binary predicates, but not unary predicates? The answer
|
|
is that there's no need, and it's impracticable anyway, because adjectives
|
|
are allowed to have multiple definitions for different kinds of value, and
|
|
because the code testing them is written to cope properly with bogus values.
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">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">Simplifications::make_kinds_of_value_explicit</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">§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="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>
|
|
<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>
|
|
<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">-></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="identifier-syntax">i</span><span class="plain-syntax">=1; </span><span class="identifier-syntax">i</span><span class="plain-syntax">>=0; </span><span class="identifier-syntax">i</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">-></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>
|
|
<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"> >= </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>
|
|
<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>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">new_KIND</span><span class="plain-syntax">-></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>
|
|
<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>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP8" class="paragraph-anchor"></a><b>§8. Remove redundant kind predicates (deduction). </b>Propositions often contain more kind predicates than they need, not least as a
|
|
result of <span class="extract"><span class="extract-syntax">Simplifications::make_kinds_of_value_explicit</span></span>. Here we remove some of
|
|
those, and move the survivors to what we consider the best positions within
|
|
the line. For reasons to be revealed below, we run this process twice over:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">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">Simplifications::redundant_kinds</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">§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">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">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">, &</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">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">, &</span><span class="identifier-syntax">c2</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">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>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP9" class="paragraph-anchor"></a><b>§9. </b>This function works recursively on subexpressions within the main
|
|
proposition. These all begin and end with matched open and close brackets,
|
|
with one exception: the main proposition itself.
|
|
</p>
|
|
|
|
<p class="commentary"><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
|
|
at that point. This is 1 for the main proposition, but 0 for subexpressions,
|
|
so that inside the brackets the main content will be at level 1.
|
|
</p>
|
|
|
|
<p class="commentary">This would all go wrong if the proposition were not well-formed, but we
|
|
know that it is — an internal error would have been thrown if not.
|
|
</p>
|
|
|
|
<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">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">Simplifications::simp_redundant_kinds_dash</span></span>:<br/><a href="5-smp.html#SP8">§8</a>, <a href="5-smp.html#SP9_1">§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="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><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>
|
|
<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>
|
|
|
|
<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>
|
|
|
|
<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>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP9_1" class="paragraph-anchor"></a><b>§9.1. </b>For all of the atoms in the body of the group we're working on, the bracket
|
|
level will be 1. When it raises to 2, then, we begin a subexpression, and
|
|
we recurse into it. (We don't recurse at levels 3 and up because the level 2
|
|
call will already have taken care of those sub-sub-expressions.)
|
|
</p>
|
|
|
|
<p class="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>
|
|
</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">-></span><span class="identifier-syntax">element</span><span class="plain-syntax">)) {</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><span class="identifier-syntax">blevel</span><span class="plain-syntax"> == </span><span class="constant-syntax">2</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">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>
|
|
<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">-></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><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>
|
|
</pre>
|
|
<ul class="endnotetexts"><li>This code is used in <a href="5-smp.html#SP9">§9</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP9_2" class="paragraph-anchor"></a><b>§9.2. </b>Suppose we have a kind predicate \(K(v)\) applied to a variable. What would
|
|
be the best place to put this? Generally speaking, we want it as early as
|
|
possible, because tests of \(K\) are cheap and this will keep running time
|
|
low in compiled code. On the other hand we must not move it outside the
|
|
current subexpression. The doctrine is:
|
|
</p>
|
|
|
|
<ul class="items"><li>(i) if \(v\) is unbound {\it within the subexpression} then \(K(v)\) should
|
|
move right to the front;
|
|
</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
|
|
statement.
|
|
</li></ul>
|
|
<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}(B, x)\rbrace : {\it container}(x)\land {\it open(x)} \quad \longrightarrow \quad $$
|
|
$$ \Sigma' = \not\exists x\in\lbrace x\mid {\it container}(x)\land{\it thing}(x)\land{\it contains}(B, x)\rbrace : {\it open(x)}. $$
|
|
These are logically equivalent because \(\not\exists\) behaves that way —
|
|
they wouldn't be equivalent for other quantifiers. Rule (iii) would have
|
|
said no movement was necessary; the reason we made the move is that it
|
|
makes \(\Sigma'\) possible to assert with "now", as in the phrase "now
|
|
nothing in the Ballroom is an open container".
|
|
</p>
|
|
|
|
<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>
|
|
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>
|
|
</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"><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">-></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">-></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><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><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>
|
|
<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">, &</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>
|
|
<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>
|
|
<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">-></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">-></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">-></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>
|
|
<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">-></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">-></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="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="element-syntax">element</span><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">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"> >= </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>
|
|
</pre>
|
|
<ul class="endnotetexts"><li>This code is used in <a href="5-smp.html#SP9">§9</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP9_3" class="paragraph-anchor"></a><b>§9.3. </b>The following looks at the predicates \(K(v)\) applied to variables which
|
|
are in the subexpression at the top level. It then does two things:
|
|
</p>
|
|
|
|
<p class="commentary">Suppose \(K\) and \(L\) are kinds of value such that \(L\subseteq K\), and let
|
|
\(\psi\) be a well-formed proposition. Then
|
|
$$ \Sigma = \psi \land L(v) \cdots K(v) \cdots \quad \longrightarrow \quad \Sigma' = \psi \land L(v) \cdots $$
|
|
(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.
|
|
</p>
|
|
|
|
<p class="commentary">Secondly, and it's not worth finding a logical notation for this, the kind
|
|
is moved back to its optimal position, as calculated above.
|
|
</p>
|
|
|
|
<p class="commentary">At first sight, this process only removes redundancies when the stronger
|
|
kind appears before the weaker one. What if they occur the other way around?
|
|
This is why the simplification is run twice, and why it's important that
|
|
the process of moving predicates back to their optimal position reverses
|
|
their order. Suppose we start with \({\it person}(x)\land{\it vehicle}(y)\land{\it woman}(x)\).
|
|
</p>
|
|
|
|
<ul class="items"><li>(1a) On pass 1, "person" occurs before "woman", but it is weaker —
|
|
every woman is a person, but not necessarily vice versa — so neither is
|
|
deleted.
|
|
</li><li>(1b) But pass 1 also moves the kinds back, and this produces
|
|
\({\it woman}(x)\land{\it vehicle}(y)\land{\it person}(x)\).
|
|
</li><li>(2a) On pass 2, the stronger "woman" now occurs before "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)\).
|
|
</li></ul>
|
|
<p class="commentary">(Because the order is reversed twice, any surviving kind predicates continue
|
|
to appear in the same order as they did in the original proposition. This
|
|
doesn't matter, but it's tidy.)
|
|
</p>
|
|
|
|
<p class="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>
|
|
</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"><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"><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">-></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">-></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><span class="identifier-syntax">blevel</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">) {</span>
|
|
<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">-></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="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">v</span><span class="plain-syntax"> >= </span><span class="constant-syntax">0</span><span class="plain-syntax">) && (</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>
|
|
<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>
|
|
</pre>
|
|
<ul class="endnotetexts"><li>This code is used in <a href="5-smp.html#SP9">§9</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP9_3_1" class="paragraph-anchor"></a><b>§9.3.1. </b>The noteworthy thing here is that we continue through the subexpression,
|
|
deleting any weaker form of \(K(v)\) that we find, but also allow ourselves
|
|
to continue beyond the subexpression in one case. Suppose we have
|
|
$$ Qv\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
|
|
the domain specification. So in that one case alone we allow ourselves
|
|
to sidestep the domain closure and continue looking for \(L(v)\) in the
|
|
outer subexpression — 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>
|
|
</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">-></span><span class="element-syntax">element</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">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">gpl</span><span class="plain-syntax">-></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>
|
|
<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">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">-></span><span class="element-syntax">element</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">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>
|
|
<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">) && (</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">)) && (</span><span class="identifier-syntax">v</span><span class="plain-syntax"> == </span><span class="identifier-syntax">gpl</span><span class="plain-syntax">-></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="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>
|
|
<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">) && (</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>
|
|
<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>
|
|
</pre>
|
|
<ul class="endnotetexts"><li>This code is used in <a href="5-smp.html#SP9_3">§9.3</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP9_3_2" class="paragraph-anchor"></a><b>§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>
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<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>
|
|
<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>
|
|
<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)\)
|
|
<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>
|
|
<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>
|
|
<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>
|
|
</pre>
|
|
<ul class="endnotetexts"><li>This code is used in <a href="5-smp.html#SP9_3">§9.3</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP9_4" class="paragraph-anchor"></a><b>§9.4. </b>Suppose we find a term \(K(C)\), where \(C\) is a constant in the sense of
|
|
predicate calculus. Then there is no need to perform such a test at run-time
|
|
because we can determine the kind of \(C\) right now and simply compare it.
|
|
and compare it against \(K\) right now. For instance, \({\it number}(17)\)
|
|
is bound to be true.
|
|
</p>
|
|
|
|
<p class="commentary">Formally, suppose \(C\) is a constant which, when evaluated, has kind of value
|
|
\(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.)
|
|
</p>
|
|
|
|
<p class="commentary">We could clearly go further than this:
|
|
</p>
|
|
|
|
<ul class="items"><li>(a) Why don't we eliminate \(K(C)\) when \(K\) is an object, too? Logically this
|
|
would be fine, but we choose not to, for two reasons: people sometimes write
|
|
phrases in I7 which claim to return a room, say, but sometimes return <span class="extract"><span class="extract-syntax">nothing</span></span>.
|
|
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
|
|
practice it will protect against the <span class="extract"><span class="extract-syntax">nothing</span></span> value. The other reason is
|
|
to ensure that text like "Peter is a man" is not simplified all the way
|
|
down to the null proposition (as it clearly can be, if Peter is indeed a man).
|
|
That might seem harmless, but means that "now Peter is a man" doesn't produce
|
|
the problem message saying that kinds can't be asserted — a common mistake
|
|
made by beginners. It's better consistently to reject all such attempts than
|
|
to be clever and allow the ones which are logically redundant.
|
|
</li><li>(b) Why don't we reduce \(K(C)\) to falsity when \(C\) is a constant clearly not
|
|
of the kind \(K\), such as \({\it text}(4)\)? Again, it would make it harder to
|
|
issue a good problem message later, in type-checking; and besides our
|
|
calculus lacks a "falsity" atom, so there's no way to store the universally
|
|
false proposition which would result if we eliminated every atom this way.
|
|
(It also doesn't matter what the running time of compiled code will be if
|
|
the proposition is going to fail type-checking anyway.)
|
|
</li></ul>
|
|
<p class="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>
|
|
</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">-></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">-></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><span class="identifier-syntax">blevel</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">) {</span>
|
|
<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">-></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">) && (</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">) &&</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>
|
|
<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>
|
|
<span class="plain-syntax"> }</span>
|
|
<span class="plain-syntax"> }</span>
|
|
<span class="plain-syntax"> }</span>
|
|
</pre>
|
|
<ul class="endnotetexts"><li>This code is used in <a href="5-smp.html#SP9">§9</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP10" class="paragraph-anchor"></a><b>§10. Turn binary predicates the right way round (deduction). </b>Recall that BPs are manufactured in pairs, each being the reversal of
|
|
the other, in the sense of transposing their terms. Of each pair, one is
|
|
considered the canonical way to represent the relation, and is "the right
|
|
way round". This function turns all BPs in the proposition the right way
|
|
round, if they aren't already. (Equality is always the right way round, so
|
|
that is never altered.)
|
|
</p>
|
|
|
|
<p class="commentary">Suppose \(B\) is a binary predicate which is marked as the wrong way round,
|
|
and \(R\) is its reversal. Then we change:
|
|
$$ \Sigma = \cdots B(t_1, t_2)\cdots \quad \longrightarrow \quad \Sigma' = \cdots R(t_2, t_1) \cdots $$
|
|
</p>
|
|
|
|
<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">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">Simplifications::turn_right_way_round</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">§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="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">) && (</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>
|
|
<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">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[0];</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[0] = </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-></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">-></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">-></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>
|
|
<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>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP11" class="paragraph-anchor"></a><b>§11. Simplify region containment (fudge). </b>Most of Inform's prepositions are unambiguous, but "in" can mean two quite
|
|
different relations. Usually it means (direct) containment, but there is an
|
|
alternative interpretation as regional containment. "The diamond is in the
|
|
teddy bear" is direct containment, but "The diamond is in Northumberland"
|
|
is regional containment. We need to separate out these ideas into two
|
|
different binary predicates because direct containment has a function \(f_D\)
|
|
allowing simplification of many common sentences, but regional containment
|
|
allows no such simplification. Basically: you can be directly contained by
|
|
only one thing at a time, but might be in many regions at once.
|
|
</p>
|
|
|
|
<p class="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>.
|
|
If \(R\) is a constant region name, and \(C_D\), \(C_R\) are the predicates for
|
|
direct and region containment, then
|
|
$$ \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 $$
|
|
Note that a region cannot directly contain any object, except a backdrop.
|
|
</p>
|
|
|
|
<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">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">Simplifications::region_containment</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">§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="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>
|
|
<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"><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">-></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>
|
|
<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">-></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>
|
|
<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>
|
|
<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="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">-></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="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>
|
|
<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">) && (!</span><span class="identifier-syntax">backdropping</span><span class="plain-syntax">)) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-></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>
|
|
<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>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP12" class="paragraph-anchor"></a><b>§12. Reduce binary predicates (deduction). </b>If we are able to reduce a binary to a unary predicate, we will probably
|
|
gain considerably by being able to eliminate a variable altogether. For
|
|
instance, suppose we have "Mme Cholet is in a burrow". This will
|
|
initially come out as
|
|
$$ \exists x: {\it burrow}(x)\land {\it in}(C, x) $$
|
|
To test that proposition requires trying all possible burrows \(x\).
|
|
But exploiting the fact that Mme Cholet can only be in one place at a
|
|
time, we can reduce the binary predicate to equality, thus:
|
|
$$ \exists x: {\it burrow}(x)\land {\it is}(f(C), x) $$
|
|
where \(f\) is the function determining the location of something. A later
|
|
simplification can then observe that this tells us what \(x\) must be,
|
|
and eliminate both quantifier and variable.
|
|
</p>
|
|
|
|
<p class="commentary">Formally, suppose \(B\) is a predicate with a function \(f_B\) such that \(B(x, y)\)
|
|
is true if and only \(y = f_B(x)\). Then:
|
|
$$ \Sigma = \cdots B(t_1, t_2) \cdots \quad \longrightarrow \quad \Sigma' = \cdots {\it is}(f_B(t_1), t_2) \cdots $$
|
|
Similarly, if there is a function \(g_B\) such that \(B(x, y)\) if and only if
|
|
\(x = g_B(y)\) then
|
|
$$ \Sigma = \cdots B(t_1, t_2) \cdots \quad \longrightarrow \quad \Sigma' = \cdots {\it is}(t_1, g_B(t_2)) \cdots $$
|
|
Not all BPs have these: the reason for our fudge on regional containment (above)
|
|
is that direct containment does, but region containment doesn't, and this is
|
|
why it was necessary to separate the two out.
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">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">Simplifications::reduce_predicates</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">§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="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">)</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"><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">-></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">-></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>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-></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>
|
|
<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>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP13" class="paragraph-anchor"></a><b>§13. Eliminating determined variables (deduction). </b>The above operations will try to get as many variables as possible into a
|
|
form which makes their values explicit with a predicate \({\it is}(v, t)\).
|
|
We detect such equations and use them to eliminate the variable concerned,
|
|
where this is safe.
|
|
</p>
|
|
|
|
<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>
|
|
</pre>
|
|
<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">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">Simplifications::eliminate_redundant_variables</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">§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="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>
|
|
<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>
|
|
|
|
<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>
|
|
<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">-></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">-></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>
|
|
<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">>=0; </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">var_to_sub</span><span class="plain-syntax"> = </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-></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">(&(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-></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="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>
|
|
<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">) && (</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">-></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="identifier-syntax">TRUE</span><span class="plain-syntax">, &</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 <-- $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">], &(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-></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 is(v, t) 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>
|
|
<span class="plain-syntax"> </span><span class="comment-syntax"> then unbind the variable, by deleting its exists v 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>
|
|
<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 v</span>
|
|
<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">-></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="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>
|
|
<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>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP13_1" class="paragraph-anchor"></a><b>§13.1. </b>The information-gathering stage:
|
|
</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>
|
|
</p>
|
|
|
|
<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>
|
|
|
|
<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"><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>
|
|
|
|
<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">-></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">-></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>
|
|
<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">-></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>
|
|
<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>
|
|
</pre>
|
|
<ul class="endnotetexts"><li>This code is used in <a href="5-smp.html#SP13">§13</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP13_2" class="paragraph-anchor"></a><b>§13.2. </b>At this point we have a predicate \({\it is}(t, f_A(f_B(\cdots s)))\). Should
|
|
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))\).
|
|
</p>
|
|
|
|
<p class="commentary">But only if the term \(s\) underneath those functions does not make the equation
|
|
\({\it is}(v, f_A(f_B(\cdots s)))\) implicit. Suppose \(s\) depends
|
|
on a variable \(w\) which is bound and occurs after the binding of \(v\).
|
|
The value of such a variable \(w\) can depend on the value of \(v\). Saying that
|
|
\(v=s\) may therefore not determine a unique value of \(v\) at all: it may be
|
|
a subtle condition passed by a whole class of possible values, or none.
|
|
</p>
|
|
|
|
<p class="commentary">The simplest example of such circularity is \({\it is}(v, v)\), true for all \(v\).
|
|
More problematic is \({\it is}(v, f_C(v))\), "\(v\) is the container of \(v\)",
|
|
which is never true. Still worse is
|
|
$$ \exists v: V_{=2} w: {\it is}(v, w) $$
|
|
which literally says there is a value of \(v\) equal to two different things —
|
|
certainly false. But if we eliminated \(v\), we would get just
|
|
$$ V_{=2} w $$
|
|
which asserts "there are exactly two objects" — which is certainly not a
|
|
valid deduction.
|
|
</p>
|
|
|
|
<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\)
|
|
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>
|
|
</p>
|
|
|
|
<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"> >= </span><span class="constant-syntax">0</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">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"> && (</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>
|
|
|
|
<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"> < </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">] < </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>
|
|
<span class="plain-syntax"> }</span>
|
|
</pre>
|
|
<ul class="endnotetexts"><li>This code is used in <a href="5-smp.html#SP13">§13</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP14" class="paragraph-anchor"></a><b>§14. Simplify non-relation (deduction). </b>As a result of the previous simplifications, it fairly often happens that we
|
|
find a term like
|
|
$$ \lnot({\it thing}(f_P(t))) $$
|
|
where \(f_P\) is the function determining what, if anything, the object \(t\) is
|
|
a component part of. This comes out of text such as "... not part of something",
|
|
asserting first that there is no \(y\) such that \(t\) is a part of \(y\), and then
|
|
simplifying to remove the \(y\) variable. A term like the one above is then
|
|
left behind. But the negation is cumbersome, and makes the proposition harder
|
|
to assert or test. Exploiting the fact that \(f_P(t)\) is a property
|
|
which is either the part-parent or else \(N =\) <span class="extract"><span class="extract-syntax">nothing</span></span>, we can simplify to:
|
|
$$ {\it is}(f_P(t), N) $$
|
|
And similar tricks can be pulled for other various-to-one-object predicates.
|
|
</p>
|
|
|
|
<p class="commentary">Formally, let \(B\) be a binary predicate supporting either a function \(f_B\)
|
|
such that \(B(x, y)\) iff \(f_B(x) = y\), or else such that \(B(x, y)\) iff \(f_B(y) = x\);
|
|
and such that the values of \(f_B\) are objects. Let \(K\) be a kind of object.
|
|
Then:
|
|
$$ \Sigma = \cdots \lnot( K(f_B(t))) \cdots \quad \longrightarrow \quad \Sigma' = \cdots {\it is}(f_B(t), N) \cdots $$
|
|
</p>
|
|
|
|
<p class="commentary">A similar trick for kinds of value is not possible, because — unlike objects —
|
|
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">
|
|
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">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">Simplifications::not_related_to_something</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">§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="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">PRODUCE_NOTHING_VALUE_CALCULUS_CALLBACK</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">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>
|
|
<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">, &</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>
|
|
<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>
|
|
<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">-></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">-></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">) && (</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="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#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="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="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_CALCULUS_CALLBACK</span><span class="plain-syntax">())));</span>
|
|
<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>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP15" class="paragraph-anchor"></a><b>§15. Convert gerunds to nouns (deduction). </b>Suppose we write:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">The</span><span class="plain-syntax"> </span><span class="identifier-syntax">funky</span><span class="plain-syntax"> </span><span class="identifier-syntax">thing</span><span class="plain-syntax"> </span><span class="identifier-syntax">to</span><span class="plain-syntax"> </span><span class="identifier-syntax">do</span><span class="plain-syntax"> </span><span class="identifier-syntax">is</span><span class="plain-syntax"> </span><span class="identifier-syntax">a</span><span class="plain-syntax"> </span><span class="identifier-syntax">stored</span><span class="plain-syntax"> </span><span class="identifier-syntax">action</span><span class="plain-syntax"> </span><span class="identifier-syntax">that</span><span class="plain-syntax"> </span><span class="identifier-syntax">varies</span><span class="plain-syntax">.</span>
|
|
<span class="identifier-syntax">The</span><span class="plain-syntax"> </span><span class="identifier-syntax">funky</span><span class="plain-syntax"> </span><span class="identifier-syntax">thing</span><span class="plain-syntax"> </span><span class="identifier-syntax">to</span><span class="plain-syntax"> </span><span class="identifier-syntax">do</span><span class="plain-syntax"> </span><span class="identifier-syntax">is</span><span class="plain-syntax"> </span><span class="identifier-syntax">waiting</span><span class="plain-syntax">.</span>
|
|
</pre>
|
|
<p class="commentary">Here "waiting" is a gerund, and although it describes an action it is a
|
|
noun (thus a value) rather than a condition. We coerce its constant value
|
|
accordingly.
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<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="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">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">Simplifications::convert_gerunds</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">§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="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><span class="identifier-syntax">pl</span><span class="plain-syntax">-></span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">) && (</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-></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">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"><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">AConditions::is_action_TEST_VALUE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-></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">-></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="plain-syntax"> </span><span class="identifier-syntax">AConditions::gerund_from_TEST_VALUE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-></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="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="plain-syntax">#</span><span class="identifier-syntax">endif</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP16" class="paragraph-anchor"></a><b>§16. Eliminate to have meaning property ownership (fudge). </b>The verb "to have" normally means ownership of a physical thing, but it
|
|
can also arise from text such as
|
|
</p>
|
|
|
|
<blockquote>
|
|
<p>the balloon has weight at most 1</p>
|
|
</blockquote>
|
|
|
|
<p class="commentary">where it's the numerical "weight" property which is owned by the balloon.
|
|
At this stage of simplification, the above has produced
|
|
$$ {\it atmost}(w, 1)\land {\it is}(B, f_H(w)) $$
|
|
where \(H\) is the predicate <span class="extract"><span class="extract-syntax">a_has_b_predicate</span></span>. As it stands, this proposition
|
|
will fail type-checking, because it contains an implicit free variable — the
|
|
object which owns the weight. We make this explicit by removing
|
|
\({\it is}(B, f_H(w))\) and replacing all other references to \(w\) with "the
|
|
weight of \(B\)".
|
|
</p>
|
|
|
|
<p class="commentary">This is a fudge because it assumes — possibly wrongly — that all references
|
|
to the weight are to the weight of the same thing. In sufficiently contrived
|
|
sentences, this wouldn't be true. No bugs have ever been reported which suggest
|
|
that real users run into this.
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<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">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">Simplifications::eliminate_to_have</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">§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="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>
|
|
<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"><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">pl</span><span class="plain-syntax">-></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">) &&</span>
|
|
<span class="plain-syntax"> (</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-></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">-></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">) &&</span>
|
|
<span class="plain-syntax"> (</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-></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">-></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="identifier-syntax">pl</span><span class="plain-syntax">-></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">-></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">-></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>
|
|
<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="plain-syntax">#</span><span class="identifier-syntax">endif</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP16_1" class="paragraph-anchor"></a><b>§16.1. </b>So the current atom is \({\it is}(f_H(P), C)\) or \({\it is}(C, f_H(P))\)
|
|
(according to whether \(i\) is 0 or 1), for a property \(P\) and a constant
|
|
term \(C\).
|
|
</p>
|
|
|
|
<p class="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>
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<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>
|
|
<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="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">-></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">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">-></span><span class="identifier-syntax">name</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">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">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">,</span>
|
|
<span class="plain-syntax"> &</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>
|
|
<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"> > </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="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>
|
|
</pre>
|
|
<ul class="endnotetexts"><li>This code is used in <a href="5-smp.html#SP16">§16</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP17" class="paragraph-anchor"></a><b>§17. </b>Here we make the necessary substitution of "P" with "the P of C",
|
|
where \(P\) is a property and \(C\) the constant value of its owner. We make
|
|
this to every occurrence throughout the proposition, except for the one
|
|
in the original \({\it is}(f_H(P), C)\) atom, and we count the number of
|
|
changes made.
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<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">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">Simplifications::prop_substitute_prop_cons</span></span>:<br/><a href="5-smp.html#SP16_1">§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>
|
|
<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>
|
|
<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>
|
|
<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"><pl-></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"> = &(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-></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">-></span><span class="element-syntax">function</span><span class="plain-syntax">) </span><span class="identifier-syntax">pt</span><span class="plain-syntax"> = &(</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-></span><span class="element-syntax">function</span><span class="plain-syntax">-></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">-></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">-></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">-></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">tprn</span><span class="plain-syntax"> == </span><span class="identifier-syntax">prn</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">pt</span><span class="plain-syntax">-></span><span class="element-syntax">constant</span><span class="plain-syntax"> = </span><span class="identifier-syntax">po_spec</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>
|
|
<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>
|
|
<span class="plain-syntax">#</span><span class="identifier-syntax">endif</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP18" class="paragraph-anchor"></a><b>§18. Turn all rooms to everywhere (fudge). </b>This rather special rule handles the consequences of the English word
|
|
"everywhere". Inform reads that as "all rooms", literally "every where",
|
|
which is logical but loses the connotation of place — by "everywhere", we
|
|
usually mean "in all rooms", so that the sentence
|
|
</p>
|
|
|
|
<blockquote>
|
|
<p>The sky is everywhere.</p>
|
|
</blockquote>
|
|
|
|
<p class="commentary">means the sky is in every room, not that the sky is equal to every room.
|
|
Since the literal reading would make no useful sense, Inform fudges the
|
|
proposition to change it to the idiomatic one.
|
|
$$ \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)) $$
|
|
Note that we match this only at the end of a proposition, where \(v\) can
|
|
have no other consequence.
|
|
</p>
|
|
|
|
<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">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">Simplifications::is_all_rooms</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">§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="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>
|
|
<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>
|
|
<span class="plain-syntax"> </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">, &</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">, &</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">, &</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">)) &&</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">))) &&</span>
|
|
<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">)) &&</span>
|
|
<span class="plain-syntax"> (</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-></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="identifier-syntax">RETRIEVE_POINTER_binary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-></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">-></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="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"><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><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-></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">) && (</span><span class="identifier-syntax">v</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">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>
|
|
<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">-></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>
|
|
<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>
|
|
<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>
|
|
<span class="plain-syntax"> </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">, &</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">, &</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">, &</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">)) &&</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">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">)) &&</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">)) &&</span>
|
|
<span class="plain-syntax"> (</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-></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="identifier-syntax">RETRIEVE_POINTER_binary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-></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">-></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="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"><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><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-></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">) && (</span><span class="identifier-syntax">v</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">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">-></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">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>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP19" class="paragraph-anchor"></a><b>§19. Everywhere and nowhere (fudge). </b>Similarly, if the proposition expresses the idea of "nowhere" or "everywhere"
|
|
by spelling this out in quantifiers about being no place or every place, then
|
|
replace those with uses of the special unary predicates for "nowhere" and
|
|
"everywhere".
|
|
</p>
|
|
|
|
<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">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">Simplifications::everywhere_and_nowhere</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">§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="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">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>
|
|
<span class="plain-syntax"> </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">, &</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">, &</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">, &</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">)) &&</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">))) &&</span>
|
|
<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">)) &&</span>
|
|
<span class="plain-syntax"> (</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-></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">-></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">) && (</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="identifier-syntax">bp</span><span class="plain-syntax"> == </span><span class="identifier-syntax">room_containment_predicate</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">-></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="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"><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><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-></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">) && (</span><span class="identifier-syntax">v</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">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>
|
|
<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="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">-></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">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">-></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>
|
|
<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>
|
|
<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>
|
|
</pre>
|
|
<nav role="progress"><div class="progresscontainer">
|
|
<ul class="progressbar"><li class="progressprev"><a href="5-sc.html">❮</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">❯</li></ul></div>
|
|
</nav><!--End of weave-->
|
|
|
|
</main>
|
|
</body>
|
|
</html>
|
|
|