2019-03-17 14:40:57 +02:00
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
< html >
< head >
2020-04-14 19:56:54 +03:00
< title > Atomic Propositions< / title >
2020-05-03 03:20:55 +03:00
< link href = "../docs-assets/Breadcrumbs.css" rel = "stylesheet" rev = "stylesheet" type = "text/css" >
2020-03-19 02:11:25 +02:00
< meta name = "viewport" content = "width=device-width initial-scale=1" >
2019-03-17 14:40:57 +02:00
< meta http-equiv = "Content-Type" content = "text/html; charset=utf-8" >
< meta http-equiv = "Content-Language" content = "en-gb" >
2020-05-03 03:01:21 +03:00
2020-05-03 03:20:55 +03:00
< link href = "../docs-assets/Contents.css" rel = "stylesheet" rev = "stylesheet" type = "text/css" >
< link href = "../docs-assets/Progress.css" rel = "stylesheet" rev = "stylesheet" type = "text/css" >
< link href = "../docs-assets/Navigation.css" rel = "stylesheet" rev = "stylesheet" type = "text/css" >
< link href = "../docs-assets/Fonts.css" rel = "stylesheet" rev = "stylesheet" type = "text/css" >
< link href = "../docs-assets/Base.css" rel = "stylesheet" rev = "stylesheet" type = "text/css" >
2020-05-03 03:01:21 +03:00
< script >
MathJax = {
tex: {
inlineMath: '$', '$'], ['\\(', '\\)'
},
svg: {
fontCache: 'global'
}
};
< / script >
< script type = "text/javascript" id = "MathJax-script" async
src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-svg.js">
< / script >
< script >
function togglePopup(material_id) {
var popup = document.getElementById(material_id);
popup.classList.toggle("show");
}
< / script >
2020-05-03 03:20:55 +03:00
< link href = "../docs-assets/Popups.css" rel = "stylesheet" rev = "stylesheet" type = "text/css" >
2020-08-23 14:00:56 +03:00
< 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" >
2020-05-03 03:20:55 +03:00
< link href = "../docs-assets/Colours.css" rel = "stylesheet" rev = "stylesheet" type = "text/css" >
2020-04-14 19:56:54 +03:00
2019-03-17 14:40:57 +02:00
< / head >
2020-05-03 03:01:21 +03:00
< body class = "commentary-font" >
2020-03-19 02:11:25 +02:00
< nav role = "navigation" >
2020-04-14 19:56:54 +03:00
< h1 > < a href = "../index.html" >
2020-05-03 18:34:53 +03:00
< img src = "../docs-assets/Inform.png" height = 72" >
2020-04-14 19:56:54 +03:00
< / a > < / h1 >
< ul > < li > < a href = "../compiler.html" > compiler tools< / a > < / li >
2020-03-19 02:11:25 +02:00
< li > < a href = "../other.html" > other tools< / a > < / li >
< li > < a href = "../extensions.html" > extensions and kits< / a > < / li >
< li > < a href = "../units.html" > unit test tools< / a > < / li >
2020-04-14 19:56:54 +03:00
< / ul > < h2 > Compiler Webs< / h2 > < ul >
2020-03-19 02:11:25 +02:00
< li > < a href = "../inbuild/index.html" > inbuild< / a > < / li >
< li > < a href = "../inform7/index.html" > inform7< / a > < / li >
< li > < a href = "../inter/index.html" > inter< / a > < / li >
2020-04-14 19:56:54 +03:00
< / ul > < h2 > Inbuild Modules< / h2 > < ul >
< li > < a href = "../supervisor-module/index.html" > supervisor< / a > < / li >
< / ul > < h2 > Inform7 Modules< / h2 > < ul >
2020-08-20 01:36:18 +03:00
< li > < a href = "../core-module/index.html" > core< / a > < / li >
2020-03-19 02:11:25 +02:00
< li > < a href = "../if-module/index.html" > if< / a > < / li >
< li > < a href = "../multimedia-module/index.html" > multimedia< / a > < / li >
< li > < a href = "../index-module/index.html" > index< / a > < / li >
2020-04-14 19:56:54 +03:00
< / ul > < h2 > Inter Modules< / h2 > < ul >
< li > < a href = "../bytecode-module/index.html" > bytecode< / a > < / li >
2020-03-19 02:11:25 +02:00
< li > < a href = "../building-module/index.html" > building< / a > < / li >
< li > < a href = "../codegen-module/index.html" > codegen< / a > < / li >
2020-05-20 02:02:28 +03:00
< / ul > < h2 > Services< / h2 > < ul >
2020-04-14 19:56:54 +03:00
< li > < a href = "../arch-module/index.html" > arch< / a > < / li >
2020-08-20 01:36:18 +03:00
< li > < a href = "index.html" > < span class = "selectedlink" > calculus< / span > < / a > < / li >
2020-04-14 19:56:54 +03:00
< li > < a href = "../html-module/index.html" > html< / a > < / li >
2020-05-20 02:02:28 +03:00
< li > < a href = "../inflections-module/index.html" > inflections< / a > < / li >
2020-08-20 01:36:18 +03:00
< li > < a href = "../kinds-module/index.html" > kinds< / a > < / li >
2020-05-20 02:02:28 +03:00
< li > < a href = "../linguistics-module/index.html" > linguistics< / a > < / li >
< li > < a href = "../problems-module/index.html" > problems< / a > < / li >
2020-08-20 01:36:18 +03:00
< li > < a href = "../syntax-module/index.html" > syntax< / a > < / li >
< li > < a href = "../words-module/index.html" > words< / a > < / li >
2020-03-19 02:11:25 +02:00
< li > < a href = "../../../inweb/docs/foundation-module/index.html" > foundation< / a > < / li >
2020-04-14 19:56:54 +03:00
< / ul >
2020-03-19 02:11:25 +02:00
< / nav >
< main role = "main" >
2020-05-03 03:01:21 +03:00
<!-- Weave of 'Atomic Propositions' generated by Inweb -->
< div class = "breadcrumbs" >
2020-08-22 00:58:58 +03:00
< ul class = "crumbs" > < li > < a href = "../index.html" > Home< / a > < / li > < li > < a href = "../compiler.html" > Services< / a > < / li > < li > < a href = "index.html" > calculus< / a > < / li > < li > < a href = "index.html#3" > Chapter 3: Propositions< / a > < / li > < li > < b > Atomic Propositions< / b > < / li > < / ul > < / div >
2020-05-03 03:01:21 +03:00
< p class = "purpose" > To build and modify atoms, the syntactic pieces from which propositions are built up.< / p >
2019-03-17 14:40:57 +02:00
2020-08-24 13:21:17 +03:00
< ul class = "toc" > < li > < a href = "3-ap.html#SP1" > § 1. Elements and groups< / a > < / li > < li > < a href = "3-ap.html#SP5" > § 5. The STRUCTURAL group< / a > < / li > < li > < a href = "3-ap.html#SP17" > § 17. Validating atoms< / a > < / li > < li > < a href = "3-ap.html#SP18" > § 18. Writing to text< / a > < / li > < / ul > < hr class = "tocbar" >
2019-03-17 14:40:57 +02:00
2020-08-23 14:00:56 +03:00
< p class = "commentary firstcommentary" > < a id = "SP1" class = "paragraph-anchor" > < / a > < b > § 1. Elements and groups. < / b > Propositions are built up from "atoms": see < a href = "P-wtmd.html" class = "internal" > What This Module Does< / a > for
more. Those atoms are themselves < a href = "3-ap.html#SP1" class = "internal" > pcalc_prop< / a > objects: what makes them
atomic is simply that their < span class = "extract" > < span class = "extract-syntax" > next< / span > < / span > links lead nowhere yet.
2019-03-17 14:40:57 +02:00
< / p >
2020-08-23 14:00:56 +03:00
< pre class = "definitions code-font" > < span class = "definition-keyword" > define< / span > < span class = "constant-syntax" > MAX_ATOM_ARITY< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > 2< / span >
2019-03-17 14:40:57 +02:00
< / pre >
2020-05-03 03:01:21 +03:00
< pre class = "displayed-code all-displayed-code code-font" >
< span class = "reserved-syntax" > typedef< / span > < span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > struct< / span > < span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > pcalc_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" > element< / span > < span class = "plain-syntax" > ; < / span > < span class = "comment-syntax" > one of the constants below: always 1 or greater< / span >
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > arity< / span > < span class = "plain-syntax" > ; < / span > < span class = "comment-syntax" > 1 for quantifiers and unary predicates; 2 for BPs; 0 otherwise< / span >
2020-07-01 02:58:55 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > struct< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > general_pointer< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > predicate< / span > < span class = "plain-syntax" > ; < / span > < span class = "comment-syntax" > indicates which predicate structure is meant< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > struct< / span > < span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > pcalc_term< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > terms< / span > < span class = "plain-syntax" > [< / span > < span class = "constant-syntax" > MAX_ATOM_ARITY< / span > < span class = "plain-syntax" > ]; < / span > < span class = "comment-syntax" > terms to which the predicate applies< / span >
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > struct< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > kind< / span > < span class = "plain-syntax" > *< / span > < span class = "identifier-syntax" > assert_kind< / span > < span class = "plain-syntax" > ; < / span > < span class = "comment-syntax" > < / span > < span class = "extract" > < span class = "extract-syntax" > KIND_ATOM< / span > < / span > < span class = "comment-syntax" > : the kind of value of a variable< / span >
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > composited< / span > < span class = "plain-syntax" > ; < / span > < span class = "comment-syntax" > < / span > < span class = "extract" > < span class = "extract-syntax" > KIND_ATOM< / span > < / span > < span class = "comment-syntax" > : arises from a composite determiner/noun like "somewhere"< / span >
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > unarticled< / span > < span class = "plain-syntax" > ; < / span > < span class = "comment-syntax" > < / span > < span class = "extract" > < span class = "extract-syntax" > KIND_ATOM< / span > < / span > < span class = "comment-syntax" > : arises from an unarticled usage like "vehicle", not "a vehicle"< / span >
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > struct< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > wording< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > calling_name< / span > < span class = "plain-syntax" > ; < / span > < span class = "comment-syntax" > < / span > < span class = "extract" > < span class = "extract-syntax" > CALLED_ATOM< / span > < / span > < span class = "comment-syntax" > : text of the name this is called< / span >
2020-07-01 02:58:55 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > struct< / 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 = "comment-syntax" > < / span > < span class = "extract" > < span class = "extract-syntax" > QUANTIFIER_ATOM< / span > < / span > < span class = "comment-syntax" > : which one< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > quantification_parameter< / span > < span class = "plain-syntax" > ; < / span > < span class = "comment-syntax" > < / span > < span class = "extract" > < span class = "extract-syntax" > QUANTIFIER_ATOM< / span > < / span > < span class = "comment-syntax" > : e.g., the 3 in "all three"< / span >
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > struct< / span > < span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > pcalc_prop< / span > < span class = "plain-syntax" > *< / span > < span class = "identifier-syntax" > next< / span > < span class = "plain-syntax" > ; < / span > < span class = "comment-syntax" > next atom in the list for this proposition< / span >
< span class = "plain-syntax" > } < / span > < span class = "reserved-syntax" > pcalc_prop< / span > < span class = "plain-syntax" > ;< / span >
2019-03-17 14:40:57 +02:00
< / pre >
2020-08-24 13:21:17 +03:00
< ul class = "endnotetexts" > < li > The structure pcalc_prop is accessed in 2/up, 2/tap, 2/tcp, 2/enah, 3/prp, 3/bas and here.< / li > < / ul >
2020-08-23 14:00:56 +03:00
< p class = "commentary firstcommentary" > < a id = "SP2" class = "paragraph-anchor" > < / a > < b > § 2. < / b > Each atom is an instance of an "element", and its < span class = "extract" > < span class = "extract-syntax" > element< / span > < / span > field is one
of the < span class = "extract" > < span class = "extract-syntax" > *_ATOM< / span > < / span > numbers below. Those elements in turn occur in "groups".
2019-03-17 14:40:57 +02:00
< / p >
2020-08-23 14:00:56 +03:00
< pre class = "definitions code-font" > < span class = "definition-keyword" > define< / span > < span class = "constant-syntax" > QUANTIFIERS_GROUP< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > 10< / span >
< span class = "definition-keyword" > define< / span > < span class = "constant-syntax" > QUANTIFIER_ATOM< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > 1< / span > < span class = "plain-syntax" > < / span > < span class = "comment-syntax" > any generalised quantifier< / span >
< span class = "definition-keyword" > define< / span > < span class = "constant-syntax" > PREDICATES_GROUP< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > 20< / span >
< span class = "definition-keyword" > define< / span > < span class = "constant-syntax" > PREDICATE_ATOM< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > 10< / span > < span class = "plain-syntax" > < / span > < span class = "comment-syntax" > a regular predicate, rather than these special cases — < / span >
< span class = "definition-keyword" > define< / span > < span class = "constant-syntax" > KIND_ATOM< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > 11< / span > < span class = "plain-syntax" > < / span > < span class = "comment-syntax" > a unary predicate asserting that < / span > \(x\)< span class = "comment-syntax" > has kind < / span > \(K\)
2020-05-03 03:01:21 +03:00
< span class = "definition-keyword" > define< / span > < span class = "constant-syntax" > CALLED_ATOM< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > 18< / span > < span class = "plain-syntax" > < / span > < span class = "comment-syntax" > to keep track of "(called the intruder)"-style names< / span >
2020-08-23 14:00:56 +03:00
< span class = "definition-keyword" > define< / span > < span class = "constant-syntax" > OPEN_OPERATORS_GROUP< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > 30< / span >
2020-05-03 03:01:21 +03:00
< span class = "definition-keyword" > define< / span > < span class = "constant-syntax" > NEGATION_OPEN_ATOM< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > 20< / span > < span class = "plain-syntax" > < / span > < span class = "comment-syntax" > logical negation < / span > \(\lnot\)< span class = "comment-syntax" > applied to contents of group< / span >
2020-08-22 20:52:28 +03:00
< span class = "definition-keyword" > define< / span > < span class = "constant-syntax" > DOMAIN_OPEN_ATOM< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > 21< / span > < span class = "plain-syntax" > < / span > < span class = "comment-syntax" > this holds the domain of a quantifier< / span >
2020-05-03 03:01:21 +03:00
< span class = "definition-keyword" > define< / span > < span class = "constant-syntax" > CLOSE_OPERATORS_GROUP< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > 40< / span >
2020-08-23 14:00:56 +03:00
< span class = "definition-keyword" > define< / span > < span class = "constant-syntax" > NEGATION_CLOSE_ATOM< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > 30< / span > < span class = "plain-syntax" > < / span > < span class = "comment-syntax" > end of logical negation < / span > \(\lnot\)
< span class = "definition-keyword" > define< / span > < span class = "constant-syntax" > DOMAIN_CLOSE_ATOM< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > 31< / span > < span class = "plain-syntax" > < / span > < span class = "comment-syntax" > end of quantifier domain< / span >
2019-03-17 14:40:57 +02:00
< / pre >
2020-05-03 03:01:21 +03:00
< pre class = "displayed-code all-displayed-code code-font" >
2020-08-24 13:21:17 +03:00
< span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "function-syntax" > Atoms::group< / 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" > Atoms::group< / span > < / span > :< br / > < a href = "3-ap.html#SP17" > § 17< / a > < br / > Propositions - < a href = "3-prp.html#SP2" > § 2< / a > , < a href = "3-prp.html#SP10" > § 10< / a > , < a href = "3-prp.html#SP31" > § 31< / a > < br / > Binding and Substitution - < a href = "3-bas.html#SP1" > § 1< / a > < / span > < / button > < span class = "plain-syntax" > (< / span > < span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > element< / span > < span class = "plain-syntax" > ) {< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > element< / span > < span class = "plain-syntax" > < = < / span > < span class = "constant-syntax" > 0< / span > < span class = "plain-syntax" > ) < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > 0< / span > < span class = "plain-syntax" > ;< / span >
2020-08-23 14:00:56 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > element< / span > < span class = "plain-syntax" > < < / span > < span class = "constant-syntax" > QUANTIFIERS_GROUP< / span > < span class = "plain-syntax" > ) < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > QUANTIFIERS_GROUP< / span > < span class = "plain-syntax" > ;< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > element< / span > < span class = "plain-syntax" > < < / span > < span class = "constant-syntax" > PREDICATES_GROUP< / span > < span class = "plain-syntax" > ) < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > PREDICATES_GROUP< / 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" > element< / span > < span class = "plain-syntax" > < < / span > < span class = "constant-syntax" > OPEN_OPERATORS_GROUP< / span > < span class = "plain-syntax" > ) < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > OPEN_OPERATORS_GROUP< / 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" > element< / span > < span class = "plain-syntax" > < < / span > < span class = "constant-syntax" > CLOSE_OPERATORS_GROUP< / span > < span class = "plain-syntax" > ) < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > CLOSE_OPERATORS_GROUP< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > 0< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2019-03-17 14:40:57 +02:00
< / pre >
2020-08-23 14:00:56 +03:00
< p class = "commentary firstcommentary" > < a id = "SP3" class = "paragraph-anchor" > < / a > < b > § 3. < / b > Some atoms occur in pairs, which have to match like opening and closing
2019-03-17 14:40:57 +02:00
parentheses. The following returns 0 for an element code which does not behave
like this, or else returns the opposite number to any element code which does.
< / p >
2020-05-03 03:01:21 +03:00
< pre class = "displayed-code all-displayed-code code-font" >
2020-08-23 18:54:14 +03:00
< span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "function-syntax" > Atoms::counterpart< / 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" > Atoms::counterpart< / span > < / span > :< br / > Propositions - < a href = "3-prp.html#SP10" > § 10< / a > , < a href = "3-prp.html#SP31" > § 31< / a > , < a href = "3-prp.html#SP34" > § 34< / a > < / span > < / button > < span class = "plain-syntax" > (< / span > < span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > element< / span > < span class = "plain-syntax" > ) {< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > switch< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > element< / span > < span class = "plain-syntax" > ) {< / span >
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > case< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > NEGATION_OPEN_ATOM:< / span > < span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < 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" > case< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > NEGATION_CLOSE_ATOM:< / span > < span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < 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 = "reserved-syntax" > case< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > DOMAIN_OPEN_ATOM:< / span > < span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / 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" > case< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > DOMAIN_CLOSE_ATOM:< / span > < span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < 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" > default:< / span > < span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > 0< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
< span class = "plain-syntax" > }< / span >
2019-03-17 14:40:57 +02:00
< / pre >
2020-08-23 14:00:56 +03:00
< p class = "commentary firstcommentary" > < a id = "SP4" class = "paragraph-anchor" > < / a > < b > § 4. < / b > Every atom is created by the following routine:
2020-05-03 03:01:21 +03:00
< / p >
< pre class = "displayed-code all-displayed-code code-font" >
2020-08-24 13:21:17 +03:00
< span class = "reserved-syntax" > pcalc_prop< / span > < span class = "plain-syntax" > *< / span > < span class = "function-syntax" > Atoms::new< / 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" > Atoms::new< / span > < / span > :< br / > < a href = "3-ap.html#SP6" > § 6< / a > , < a href = "3-ap.html#SP9" > § 9< / a > , < a href = "3-ap.html#SP10" > § 10< / a > , < a href = "3-ap.html#SP11" > § 11< / a > , < a href = "3-ap.html#SP13" > § 13< / a > , < a href = "3-ap.html#SP14" > § 14< / a > < br / > Propositions - < a href = "3-prp.html#SP13" > § 13< / a > , < a href = "3-prp.html#SP16" > § 16< / a > < / span > < / button > < span class = "plain-syntax" > (< / span > < span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > element< / span > < span class = "plain-syntax" > ) {< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "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" > CREATE< / span > < span class = "plain-syntax" > (< / span > < span class = "reserved-syntax" > pcalc_prop< / span > < span class = "plain-syntax" > );< / span >
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "identifier-syntax" > next< / 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 > < span class = "identifier-syntax" > element< / 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" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "identifier-syntax" > assert_kind< / 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 > < span class = "identifier-syntax" > composited< / 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 > < span class = "identifier-syntax" > unarticled< / 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 > < span class = "identifier-syntax" > arity< / 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 > < span class = "identifier-syntax" > predicate< / span > < span class = "plain-syntax" > = < / span > < span class = "identifier-syntax" > NULL_GENERAL_POINTER< / span > < span class = "plain-syntax" > ;< / span >
2020-07-01 02:58:55 +03:00
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "identifier-syntax" > quant< / span > < span class = "plain-syntax" > = < / span > < span class = "identifier-syntax" > NULL< / span > < span class = "plain-syntax" > ;< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2019-03-17 14:40:57 +02:00
< / pre >
2020-08-23 14:00:56 +03:00
< p class = "commentary firstcommentary" > < a id = "SP5" class = "paragraph-anchor" > < / a > < b > § 5. The STRUCTURAL group. < / b > This group contains only < span class = "extract" > < span class = "extract-syntax" > QUANTIFIER< / span > < / span > atoms. These have arity 1, and the single
term must always be a variable, the one which is being bound.< sup id = "fnref:1" > < a href = "#fn:1" rel = "footnote" > 1< / a > < / sup > The parameter
is a number needed for some < span class = "extract" > < span class = "extract-syntax" > quantifier< / span > < / span > types to identify the range: for
instance, it would be 7 in the case of < span class = "extract" > < span class = "extract-syntax" > Card= 7< / span > < / span > .
2019-03-17 14:40:57 +02:00
< / p >
2020-08-23 14:00:56 +03:00
< 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 > Tying specific variables to quantifiers seems to be out of fashion in
2019-03-17 14:40:57 +02:00
modern computer science. Contemporary theorem-proving assistants mostly
use de Bruijn's numbering scheme, in which numbers 1, 2, 3, ..., refer
to variables being quantified in an indirect way. The advantage is that
propositions are easier to construct, since the same numbers can be used
in different subexpressions of the same proposition, and there's no
worrying about clashes. But it all just moves the difficulty elsewhere,
by making it less obvious how to pair up the numbers with variables at
compilation time, and less obvious even how many variables are needed.
2020-08-23 14:00:56 +03:00
< a href = "#fnref:1" title = "return to text" > ↩ < / a > < / p > < / li > < / ul >
< p class = "commentary firstcommentary" > < a id = "SP6" class = "paragraph-anchor" > < / a > < b > § 6. < / b > < / p >
2019-03-17 14:40:57 +02:00
2020-05-03 03:01:21 +03:00
< pre class = "displayed-code all-displayed-code code-font" >
2020-08-23 18:54:14 +03:00
< span class = "reserved-syntax" > pcalc_prop< / span > < span class = "plain-syntax" > *< / span > < span class = "function-syntax" > Atoms::QUANTIFIER_new< / 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" > Atoms::QUANTIFIER_new< / span > < / span > :< br / > Propositions - < a href = "3-prp.html#SP16" > § 16< / a > < br / > Binding and Substitution - < a href = "3-bas.html#SP10" > § 10< / a > < / span > < / button > < 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 = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > v< / span > < span class = "plain-syntax" > , < / span > < span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > parameter< / span > < span class = "plain-syntax" > ) {< / span >
2020-08-23 14:00:56 +03:00
< 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 > < a href = "3-ap.html#SP4" class = "function-link" > < span class = "function-syntax" > Atoms::new< / span > < / a > < span class = "plain-syntax" > (< / span > < span class = "constant-syntax" > QUANTIFIER_ATOM< / span > < span class = "plain-syntax" > );< / span >
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "identifier-syntax" > terms< / span > < span class = "plain-syntax" > [< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > arity< / span > < span class = "plain-syntax" > ++] = < / span > < a href = "3-trm.html#SP4" class = "function-link" > < span class = "function-syntax" > Terms::new_variable< / span > < / a > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > v< / span > < span class = "plain-syntax" > );< / span >
2020-07-01 02:58:55 +03:00
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "identifier-syntax" > quant< / span > < span class = "plain-syntax" > = < / span > < span class = "identifier-syntax" > quant< / span > < span class = "plain-syntax" > ;< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "identifier-syntax" > quantification_parameter< / span > < span class = "plain-syntax" > = < / span > < span class = "identifier-syntax" > parameter< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2019-03-17 14:40:57 +02:00
< / pre >
2020-08-23 14:00:56 +03:00
< p class = "commentary firstcommentary" > < a id = "SP7" class = "paragraph-anchor" > < / a > < b > § 7. < / b > Quantifier atoms can be detected as follows:
2020-05-03 03:01:21 +03:00
< / p >
< pre class = "displayed-code all-displayed-code code-font" >
2020-08-23 18:54:14 +03:00
< span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "function-syntax" > Atoms::is_quantifier< / 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" > Atoms::is_quantifier< / span > < / span > :< br / > Propositions - < a href = "3-prp.html#SP10" > § 10< / 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 >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > ((< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > ) & & (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > element< / span > < span class = "plain-syntax" > == < / span > < span class = "constant-syntax" > QUANTIFIER_ATOM< / span > < span class = "plain-syntax" > )) < / span > < span class = "reserved-syntax" > return< / 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" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > FALSE< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2020-08-23 14:00:56 +03:00
< span class = "identifier-syntax" > quantifier< / span > < span class = "plain-syntax" > *< / span > < span class = "function-syntax" > Atoms::get_quantifier< / 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 >
2020-07-01 02:58:55 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < 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 = "element-syntax" > element< / span > < span class = "plain-syntax" > == < / span > < span class = "constant-syntax" > QUANTIFIER_ATOM< / 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 = "element-syntax" > quant< / span > < span class = "plain-syntax" > ;< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > NULL< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2020-08-23 14:00:56 +03:00
< span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "function-syntax" > Atoms::get_quantification_parameter< / 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 >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > ((< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > ) & & (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > element< / span > < span class = "plain-syntax" > == < / span > < span class = "constant-syntax" > QUANTIFIER_ATOM< / 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 = "element-syntax" > quantification_parameter< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > 0< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2020-08-23 18:54:14 +03:00
< span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "function-syntax" > Atoms::is_existence_quantifier< / 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" > Atoms::is_existence_quantifier< / span > < / span > :< br / > Propositions - < a href = "3-prp.html#SP10" > § 10< / a > , < a href = "3-prp.html#SP29" > § 29< / 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 >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > ((< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > ) & & (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > element< / span > < span class = "plain-syntax" > == < / span > < span class = "constant-syntax" > QUANTIFIER_ATOM< / span > < span class = "plain-syntax" > ) & & < / span >
2020-07-01 02:58:55 +03:00
< span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > quant< / span > < span class = "plain-syntax" > == < / span > < span class = "identifier-syntax" > exists_quantifier< / span > < span class = "plain-syntax" > ))< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > TRUE< / 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" > FALSE< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2020-08-23 14:00:56 +03:00
< span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "function-syntax" > Atoms::is_nonexistence_quantifier< / 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 >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > ((< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > ) & & (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > element< / span > < span class = "plain-syntax" > == < / span > < span class = "constant-syntax" > QUANTIFIER_ATOM< / span > < span class = "plain-syntax" > ) & & < / span >
2020-07-01 02:58:55 +03:00
< span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > quant< / span > < span class = "plain-syntax" > == < / span > < span class = "identifier-syntax" > not_exists_quantifier< / span > < span class = "plain-syntax" > ))< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > TRUE< / 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" > FALSE< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2020-08-23 14:00:56 +03:00
< span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "function-syntax" > Atoms::is_forall_quantifier< / 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 >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > ((< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > ) & & (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > element< / span > < span class = "plain-syntax" > == < / span > < span class = "constant-syntax" > QUANTIFIER_ATOM< / span > < span class = "plain-syntax" > ) & & < / span >
2020-07-01 02:58:55 +03:00
< span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > quant< / span > < span class = "plain-syntax" > == < / span > < span class = "identifier-syntax" > for_all_quantifier< / span > < span class = "plain-syntax" > ))< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > TRUE< / 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" > FALSE< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2020-08-23 14:00:56 +03:00
< span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "function-syntax" > Atoms::is_notall_quantifier< / 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 >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > ((< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > ) & & (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > element< / span > < span class = "plain-syntax" > == < / span > < span class = "constant-syntax" > QUANTIFIER_ATOM< / span > < span class = "plain-syntax" > ) & & < / span >
2020-07-01 02:58:55 +03:00
< span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > quant< / span > < span class = "plain-syntax" > == < / span > < span class = "identifier-syntax" > not_for_all_quantifier< / span > < span class = "plain-syntax" > ))< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > TRUE< / 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" > FALSE< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2020-08-23 18:54:14 +03:00
< span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "function-syntax" > Atoms::is_for_all_x< / 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" > Atoms::is_for_all_x< / span > < / span > :< br / > Propositions - < a href = "3-prp.html#SP35" > § 35< / 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 >
2020-08-23 14:00:56 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > ((< / span > < a href = "3-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" > prop< / span > < span class = "plain-syntax" > )) & & < / span >
< span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / 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 = "constant-syntax" > 0< / span > < span class = "plain-syntax" > )) < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > TRUE< / span > < span class = "plain-syntax" > ;< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > FALSE< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2019-03-17 14:40:57 +02:00
< / pre >
2020-08-23 14:00:56 +03:00
< p class = "commentary firstcommentary" > < a id = "SP8" class = "paragraph-anchor" > < / a > < b > § 8. < / b > See < a href = "../linguistics-module/2-daq.html" class = "internal" > Determiners and Quantifiers (in linguistics)< / a > for what a now-assertable
quantifier is:
2019-03-17 14:40:57 +02:00
< / p >
2020-05-03 03:01:21 +03:00
< pre class = "displayed-code all-displayed-code code-font" >
2020-08-23 14:00:56 +03:00
< span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "function-syntax" > Atoms::is_now_assertable_quantifier< / 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 >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > element< / span > < span class = "plain-syntax" > != < / span > < span class = "constant-syntax" > QUANTIFIER_ATOM< / span > < span class = "plain-syntax" > ) < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > FALSE< / span > < span class = "plain-syntax" > ;< / span >
2020-07-01 02:58:55 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > Quantifiers::is_now_assertable< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > quant< / span > < span class = "plain-syntax" > );< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > }< / span >
2019-03-17 14:40:57 +02:00
< / pre >
2020-08-24 13:21:17 +03:00
< p class = "commentary firstcommentary" > < a id = "SP9" class = "paragraph-anchor" > < / a > < b > § 9. < / b > < span class = "extract" > < span class = "extract-syntax" > CALLED< / span > < / span > atoms are interesting because they exist only for their side-effects:
2019-03-17 14:40:57 +02:00
they have no effect at all on the logical status of a proposition (well, except
that they should not be applied to free variables referred to nowhere else).
They can therefore be added or removed freely. In the phrase
< / p >
< blockquote >
< p > if a woman is in a lighted room (called the den), ...< / p >
< / blockquote >
2020-05-03 03:01:21 +03:00
< p class = "commentary" > we need to note that the value of the bound variable corresponding to the
2019-03-17 14:40:57 +02:00
lighted room will need to be kept and to have a name ("the den"): this
2020-05-03 03:01:21 +03:00
will probably mean the inclusion of a < span class = "extract" > < span class = "extract-syntax" > CALLED=den(y)< / span > < / span > atom.
2019-03-17 14:40:57 +02:00
< / p >
2020-05-03 03:01:21 +03:00
< p class = "commentary" > The calling data for a < span class = "extract" > < span class = "extract-syntax" > CALLED< / span > < / span > atom is the textual name by which the variable
2019-03-17 14:40:57 +02:00
will be called.
< / p >
2020-05-03 03:01:21 +03:00
< pre class = "displayed-code all-displayed-code code-font" >
2020-08-24 13:21:17 +03:00
< span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "function-syntax" > Atoms::is_CALLED< / 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" > Atoms::is_CALLED< / span > < / span > :< br / > < a href = "3-ap.html#SP18" > § 18< / a > < br / > Propositions - < a href = "3-prp.html#SP24" > § 24< / 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 >
2020-08-24 02:22:48 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > element< / span > < span class = "plain-syntax" > == < / span > < span class = "constant-syntax" > CALLED_ATOM< / span > < span class = "plain-syntax" > ) < / span > < span class = "reserved-syntax" > return< / 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" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > FALSE< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2020-08-23 14:00:56 +03:00
< span class = "reserved-syntax" > pcalc_prop< / span > < span class = "plain-syntax" > *< / span > < span class = "function-syntax" > Atoms::CALLED_new< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > wording< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > W< / 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" > 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 = "reserved-syntax" > pcalc_prop< / span > < span class = "plain-syntax" > *< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > = < / span > < a href = "3-ap.html#SP4" class = "function-link" > < span class = "function-syntax" > Atoms::new< / span > < / a > < span class = "plain-syntax" > (< / span > < span class = "constant-syntax" > CALLED_ATOM< / span > < span class = "plain-syntax" > );< / span >
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "identifier-syntax" > terms< / span > < span class = "plain-syntax" > [< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > arity< / span > < span class = "plain-syntax" > ++] = < / span > < span class = "identifier-syntax" > pt< / span > < span class = "plain-syntax" > ;< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "identifier-syntax" > calling_name< / span > < span class = "plain-syntax" > = < / span > < span class = "identifier-syntax" > W< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "identifier-syntax" > assert_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 = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2019-03-17 14:40:57 +02:00
2020-08-24 13:21:17 +03:00
< span class = "identifier-syntax" > wording< / span > < span class = "plain-syntax" > < / span > < span class = "function-syntax" > Atoms::CALLED_get_name< / 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" > Atoms::CALLED_get_name< / span > < / span > :< br / > < a href = "3-ap.html#SP18" > § 18< / 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 >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > calling_name< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2019-03-17 14:40:57 +02:00
< / pre >
2020-08-24 13:21:17 +03:00
< p class = "commentary firstcommentary" > < a id = "SP10" class = "paragraph-anchor" > < / a > < b > § 10. < / b > Now for a < span class = "extract" > < span class = "extract-syntax" > KIND< / span > < / span > atom. At first sight, it looks odd that a unary
2019-03-17 14:40:57 +02:00
predicate for a kind is represented differently from other predicates.
2020-08-23 14:00:56 +03:00
Isn't it a unary predicate just like any other? Well: it is, but has the
special property that its truth does not change over time. If a value < span class = "extract" > < span class = "extract-syntax" > v< / span > < / span >
satisfies < span class = "extract" > < span class = "extract-syntax" > kind=K(v)< / span > < / span > at then start of execution, it will do so throughout.
That is not true of, say, adjectival predicates like < span class = "extract" > < span class = "extract-syntax" > open(v)< / span > < / span > . Not only
is < span class = "extract" > < span class = "extract-syntax" > kind=K(v)< / span > < / span > unchanging over time, but we can determine its truth or
falsity (if we know < span class = "extract" > < span class = "extract-syntax" > v< / span > < / span > ) even at compile time. We can exploit this in many
ways.
2019-03-17 14:40:57 +02:00
< / p >
2020-05-03 03:01:21 +03:00
< pre class = "displayed-code all-displayed-code code-font" >
2020-08-23 14:00:56 +03:00
< span class = "reserved-syntax" > pcalc_prop< / span > < span class = "plain-syntax" > *< / span > < span class = "function-syntax" > Atoms::KIND_new< / 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 = "reserved-syntax" > pcalc_term< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > pt< / 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" > prop< / span > < span class = "plain-syntax" > = < / span > < a href = "3-ap.html#SP4" class = "function-link" > < span class = "function-syntax" > Atoms::new< / span > < / a > < span class = "plain-syntax" > (< / span > < span class = "constant-syntax" > KIND_ATOM< / span > < span class = "plain-syntax" > );< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "identifier-syntax" > arity< / span > < span class = "plain-syntax" > = < / span > < span class = "constant-syntax" > 1< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "identifier-syntax" > assert_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 > < span class = "identifier-syntax" > terms< / span > < span class = "plain-syntax" > [0] = < / span > < span class = "identifier-syntax" > pt< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2020-08-23 14:00:56 +03:00
< span class = "identifier-syntax" > kind< / span > < span class = "plain-syntax" > *< / span > < span class = "function-syntax" > Atoms::get_asserted_kind< / 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 = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / 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 = "element-syntax" > assert_kind< / 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" > NULL< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
< / pre >
2020-08-24 13:21:17 +03:00
< p class = "commentary firstcommentary" > < a id = "SP11" class = "paragraph-anchor" > < / a > < b > § 11. < / b > Composited < span class = "extract" > < span class = "extract-syntax" > KIND< / span > < / span > atoms are special in that they represent composites
2020-08-23 14:00:56 +03:00
of quantifiers with common nouns — for example, "everyone" is a composite
meaning "every person".
< / 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" > Atoms::KIND_new_composited< / 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 = "reserved-syntax" > pcalc_term< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > pt< / 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" > prop< / span > < span class = "plain-syntax" > = < / span > < a href = "3-ap.html#SP4" class = "function-link" > < span class = "function-syntax" > Atoms::new< / span > < / a > < span class = "plain-syntax" > (< / span > < span class = "constant-syntax" > KIND_ATOM< / span > < span class = "plain-syntax" > );< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "identifier-syntax" > arity< / span > < span class = "plain-syntax" > = < / span > < span class = "constant-syntax" > 1< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "identifier-syntax" > assert_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 > < span class = "identifier-syntax" > terms< / span > < span class = "plain-syntax" > [0] = < / span > < span class = "identifier-syntax" > pt< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "identifier-syntax" > composited< / 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" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2020-08-23 14:00:56 +03:00
< span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "function-syntax" > Atoms::is_composited< / 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 >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > ((< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > ) & & (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > composited< / span > < span class = "plain-syntax" > )) < / span > < span class = "reserved-syntax" > return< / 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" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > FALSE< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2020-08-23 14:00:56 +03:00
< span class = "reserved-syntax" > void< / span > < span class = "plain-syntax" > < / span > < span class = "function-syntax" > Atoms::set_composited< / 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" > state< / span > < span class = "plain-syntax" > ) {< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > ) < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > composited< / span > < span class = "plain-syntax" > = < / span > < span class = "identifier-syntax" > state< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2019-03-17 14:40:57 +02:00
< / pre >
2020-08-24 13:21:17 +03:00
< p class = "commentary firstcommentary" > < a id = "SP12" class = "paragraph-anchor" > < / a > < b > § 12. < / b > Unarticled kinds are those which were introduced without an article, in
2020-08-23 14:00:56 +03:00
the linguistic sense.
2019-03-17 14:40:57 +02:00
< / p >
2020-05-03 03:01:21 +03:00
< pre class = "displayed-code all-displayed-code code-font" >
2020-08-23 14:00:56 +03:00
< span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "function-syntax" > Atoms::is_unarticled< / 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 >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > ((< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > ) & & (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > unarticled< / span > < span class = "plain-syntax" > )) < / span > < span class = "reserved-syntax" > return< / 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" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > FALSE< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2019-03-17 14:40:57 +02:00
2020-08-23 14:00:56 +03:00
< span class = "reserved-syntax" > void< / span > < span class = "plain-syntax" > < / span > < span class = "function-syntax" > Atoms::set_unarticled< / 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" > state< / span > < span class = "plain-syntax" > ) {< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > ) < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > unarticled< / span > < span class = "plain-syntax" > = < / span > < span class = "identifier-syntax" > state< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2019-03-17 14:40:57 +02:00
< / pre >
2020-08-24 13:21:17 +03:00
< p class = "commentary firstcommentary" > < a id = "SP13" class = "paragraph-anchor" > < / a > < b > § 13. < / b > That just leaves the general sort of unary predicate. In principle we ought
2020-04-14 19:56:54 +03:00
to be able to create \(U(t)\) for any term \(t\), but in practice we only ever
need \(t=x\), that is, variable 0.
2019-03-17 14:40:57 +02:00
< / p >
2020-05-03 03:01:21 +03:00
< pre class = "displayed-code all-displayed-code code-font" >
2020-08-24 13:21:17 +03:00
< span class = "reserved-syntax" > pcalc_prop< / span > < span class = "plain-syntax" > *< / span > < span class = "function-syntax" > Atoms::unary_PREDICATE_new< / 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" > Atoms::unary_PREDICATE_new< / span > < / span > :< br / > The Creation Predicates - < a href = "2-tcp.html#SP3" > § 3< / a > < br / > Everywhere, Nowhere and Here - < a href = "2-enah.html#SP3" > § 3< / a > < / span > < / button > < span class = "plain-syntax" > (< / span > < span class = "reserved-syntax" > unary_predicate< / span > < span class = "plain-syntax" > *< / span > < span class = "identifier-syntax" > up< / span > < span class = "plain-syntax" > , < / span > < span class = "reserved-syntax" > pcalc_term< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > t< / span > < span class = "plain-syntax" > ) {< / span >
2020-08-23 14:00:56 +03:00
< 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 > < a href = "3-ap.html#SP4" class = "function-link" > < span class = "function-syntax" > Atoms::new< / span > < / a > < span class = "plain-syntax" > (< / span > < span class = "constant-syntax" > PREDICATE_ATOM< / span > < span class = "plain-syntax" > );< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "identifier-syntax" > arity< / span > < span class = "plain-syntax" > = < / span > < span class = "constant-syntax" > 1< / span > < span class = "plain-syntax" > ;< / span >
2020-08-22 14:59:50 +03:00
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "identifier-syntax" > terms< / span > < span class = "plain-syntax" > [0] = < / span > < span class = "identifier-syntax" > t< / span > < span class = "plain-syntax" > ;< / span >
2020-08-24 12:34:23 +03:00
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "identifier-syntax" > predicate< / span > < span class = "plain-syntax" > = < / span > < span class = "identifier-syntax" > STORE_POINTER_unary_predicate< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > up< / span > < span class = "plain-syntax" > );< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2019-03-17 14:40:57 +02:00
2020-08-24 12:34:23 +03:00
< span class = "reserved-syntax" > pcalc_prop< / span > < span class = "plain-syntax" > *< / span > < span class = "function-syntax" > Atoms::from_adjective< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > adjective< / span > < span class = "plain-syntax" > *< / span > < span class = "identifier-syntax" > aph< / span > < span class = "plain-syntax" > , < / span > < span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > negated< / span > < span class = "plain-syntax" > , < / span > < span class = "reserved-syntax" > pcalc_term< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > t< / span > < span class = "plain-syntax" > ) {< / span >
2020-08-24 13:21:17 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < a href = "3-ap.html#SP13" class = "function-link" > < span class = "function-syntax" > Atoms::unary_PREDICATE_new< / span > < / a > < span class = "plain-syntax" > (< / span > < a href = "2-up.html#SP2" class = "function-link" > < span class = "function-syntax" > UnaryPredicates::new< / span > < / a > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > aph< / span > < span class = "plain-syntax" > , (< / span > < span class = "identifier-syntax" > negated< / span > < span class = "plain-syntax" > )?< / span > < span class = "identifier-syntax" > FALSE:TRUE< / span > < span class = "plain-syntax" > ), < / span > < span class = "identifier-syntax" > t< / span > < span class = "plain-syntax" > );< / span >
2020-08-24 12:34:23 +03:00
< span class = "plain-syntax" > }< / span >
2020-08-23 18:54:14 +03:00
< span class = "reserved-syntax" > pcalc_prop< / span > < span class = "plain-syntax" > *< / span > < span class = "function-syntax" > Atoms::from_adjective_on_x< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > adjective< / span > < span class = "plain-syntax" > *< / span > < span class = "identifier-syntax" > aph< / span > < span class = "plain-syntax" > , < / span > < span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > negated< / span > < span class = "plain-syntax" > ) {< / span >
2020-08-24 13:21:17 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < a href = "3-ap.html#SP13" class = "function-link" > < span class = "function-syntax" > Atoms::from_adjective< / span > < / a > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > aph< / span > < span class = "plain-syntax" > , < / span > < span class = "identifier-syntax" > negated< / span > < span class = "plain-syntax" > , < / span > < a href = "3-trm.html#SP4" class = "function-link" > < span class = "function-syntax" > Terms::new_variable< / span > < / a > < span class = "plain-syntax" > (0));< / span >
2020-08-22 14:59:50 +03:00
< span class = "plain-syntax" > }< / span >
2020-08-24 12:34:23 +03:00
< span class = "reserved-syntax" > unary_predicate< / span > < span class = "plain-syntax" > *< / span > < span class = "function-syntax" > Atoms::to_adjectival_usage< / 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" > Atoms::to_adjectival_usage< / span > < / span > :< br / > Propositions - < a href = "3-prp.html#SP30" > § 30< / 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 >
2020-07-01 02:58:55 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > RETRIEVE_POINTER_unary_predicate< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > predicate< / span > < span class = "plain-syntax" > );< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > }< / span >
2019-03-17 14:40:57 +02:00
< / pre >
2020-08-24 13:21:17 +03:00
< p class = "commentary firstcommentary" > < a id = "SP14" class = "paragraph-anchor" > < / a > < b > § 14. < / b > And binary predicates are pretty well the same:
2020-05-03 03:01:21 +03:00
< / p >
< pre class = "displayed-code all-displayed-code code-font" >
2020-08-24 13:21:17 +03:00
< span class = "reserved-syntax" > pcalc_prop< / span > < span class = "plain-syntax" > *< / span > < span class = "function-syntax" > Atoms::binary_PREDICATE_new< / 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" > Atoms::binary_PREDICATE_new< / span > < / span > :< br / > < a href = "3-ap.html#SP15" > § 15< / a > < / span > < / button > < 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 >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > pcalc_term< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > pt1< / span > < span class = "plain-syntax" > , < / span > < span class = "reserved-syntax" > pcalc_term< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > pt2< / span > < span class = "plain-syntax" > ) {< / span >
2020-08-23 14:00:56 +03:00
< 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 > < a href = "3-ap.html#SP4" class = "function-link" > < span class = "function-syntax" > Atoms::new< / span > < / a > < span class = "plain-syntax" > (< / span > < span class = "constant-syntax" > PREDICATE_ATOM< / span > < span class = "plain-syntax" > );< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "identifier-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" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "identifier-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" > bp< / span > < span class = "plain-syntax" > );< / span >
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "identifier-syntax" > terms< / span > < span class = "plain-syntax" > [0] = < / span > < span class = "identifier-syntax" > pt1< / span > < span class = "plain-syntax" > ; < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > terms< / span > < span class = "plain-syntax" > [1] = < / span > < span class = "identifier-syntax" > pt2< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2020-08-23 14:00:56 +03:00
< span class = "reserved-syntax" > binary_predicate< / span > < span class = "plain-syntax" > *< / span > < span class = "function-syntax" > Atoms::is_binary_predicate< / 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 >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > == < / span > < span class = "identifier-syntax" > NULL< / span > < span class = "plain-syntax" > ) < / span > < span class = "reserved-syntax" > return< / 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" > if< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / 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 = "reserved-syntax" > return< / 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" > if< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / 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 = "reserved-syntax" > return< / 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" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > RETRIEVE_POINTER_binary_predicate< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > predicate< / span > < span class = "plain-syntax" > );< / span >
< span class = "plain-syntax" > }< / span >
2020-08-24 13:21:17 +03:00
< span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "function-syntax" > Atoms::is_equality_predicate< / 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" > Atoms::is_equality_predicate< / span > < / span > :< br / > < a href = "3-ap.html#SP16" > § 16< / a > < br / > Propositions - < a href = "3-prp.html#SP11" > § 11< / a > , < a href = "3-prp.html#SP26" > § 26< / 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" > binary_predicate< / span > < span class = "plain-syntax" > *< / span > < span class = "identifier-syntax" > bp< / span > < span class = "plain-syntax" > = < / span > < a href = "3-ap.html#SP14" class = "function-link" > < span class = "function-syntax" > Atoms::is_binary_predicate< / span > < / a > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > );< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "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_equality< / span > < span class = "plain-syntax" > ) < / span > < span class = "reserved-syntax" > return< / 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" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > FALSE< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2019-03-17 14:40:57 +02:00
< / pre >
2020-08-24 13:21:17 +03:00
< p class = "commentary firstcommentary" > < a id = "SP15" class = "paragraph-anchor" > < / a > < b > § 15. < / b > Given \(C\), return the proposition < span class = "extract" > < span class = "extract-syntax" > (x == C)< / span > < / span > :
2019-03-17 14:40:57 +02:00
< / p >
2020-05-03 03:01:21 +03:00
< pre class = "displayed-code all-displayed-code code-font" >
2020-08-23 18:54:14 +03:00
< span class = "reserved-syntax" > pcalc_prop< / span > < span class = "plain-syntax" > *< / span > < span class = "function-syntax" > Atoms::prop_x_is_constant< / 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 >
2020-08-24 13:21:17 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < a href = "3-ap.html#SP14" 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 >
2020-08-23 14:00:56 +03:00
< span class = "plain-syntax" > < / span > < a href = "3-trm.html#SP4" class = "function-link" > < span class = "function-syntax" > Terms::new_variable< / span > < / a > < span class = "plain-syntax" > (0), < / span > < a href = "3-trm.html#SP4" class = "function-link" > < span class = "function-syntax" > Terms::new_constant< / span > < / a > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > C< / span > < span class = "plain-syntax" > ));< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > }< / span >
2019-03-17 14:40:57 +02:00
< / pre >
2020-08-24 13:21:17 +03:00
< p class = "commentary firstcommentary" > < a id = "SP16" class = "paragraph-anchor" > < / a > < b > § 16. < / b > And conversely:
2019-03-17 14:40:57 +02:00
< / p >
2020-05-03 03:01:21 +03:00
< pre class = "displayed-code all-displayed-code code-font" >
2020-08-23 14:00:56 +03:00
< span class = "reserved-syntax" > pcalc_term< / span > < span class = "plain-syntax" > *< / span > < span class = "function-syntax" > Atoms::is_x_equals< / 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 >
2020-08-24 13:21:17 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > (< / span > < a href = "3-ap.html#SP14" class = "function-link" > < span class = "function-syntax" > Atoms::is_equality_predicate< / span > < / a > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > ) == < / span > < span class = "identifier-syntax" > FALSE< / span > < span class = "plain-syntax" > ) < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > NULL< / span > < span class = "plain-syntax" > ;< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / 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 = "constant-syntax" > 0< / span > < span class = "plain-syntax" > ) < / span > < span class = "reserved-syntax" > return< / 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" > return< / span > < span class = "plain-syntax" > & (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > terms< / span > < span class = "plain-syntax" > [1]);< / span >
< span class = "plain-syntax" > }< / span >
2019-03-17 14:40:57 +02:00
< / pre >
2020-08-24 13:21:17 +03:00
< p class = "commentary firstcommentary" > < a id = "SP17" class = "paragraph-anchor" > < / a > < b > § 17. Validating atoms. < / b > < / p >
2020-05-03 03:01:21 +03:00
< pre class = "displayed-code all-displayed-code code-font" >
2020-08-24 12:34:23 +03:00
< span class = "reserved-syntax" > char< / span > < span class = "plain-syntax" > *< / span > < span class = "function-syntax" > Atoms::validate< / 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" > Atoms::validate< / span > < / span > :< br / > Propositions - < a href = "3-prp.html#SP10" > § 10< / 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 >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > group< / 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" > prop< / span > < span class = "plain-syntax" > == < / span > < span class = "identifier-syntax" > NULL< / span > < span class = "plain-syntax" > ) < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > NULL< / span > < span class = "plain-syntax" > ;< / span >
2020-08-23 14:00:56 +03:00
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > group< / span > < span class = "plain-syntax" > = < / span > < a href = "3-ap.html#SP2" class = "function-link" > < span class = "function-syntax" > Atoms::group< / span > < / a > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > element< / span > < span class = "plain-syntax" > );< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > group< / span > < span class = "plain-syntax" > == < / span > < span class = "constant-syntax" > 0< / span > < span class = "plain-syntax" > ) < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "string-syntax" > "atom of undiscovered element"< / 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" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > arity< / span > < span class = "plain-syntax" > > < / span > < span class = "constant-syntax" > MAX_ATOM_ARITY< / span > < span class = "plain-syntax" > ) < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "string-syntax" > "atom with overly large arity"< / 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" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > arity< / span > < span class = "plain-syntax" > < < / span > < span class = "constant-syntax" > 0< / span > < span class = "plain-syntax" > ) < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "string-syntax" > "atom with negative arity"< / 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" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > arity< / 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" > group< / span > < span class = "plain-syntax" > == < / span > < span class = "constant-syntax" > PREDICATES_GROUP< / span > < span class = "plain-syntax" > ) < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "string-syntax" > "predicate without terms"< / 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" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > element< / span > < span class = "plain-syntax" > == < / span > < span class = "constant-syntax" > QUANTIFIER_ATOM< / span > < span class = "plain-syntax" > ) < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "string-syntax" > "quantifier without variable"< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > } < / span > < span class = "reserved-syntax" > else< / 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" > prop< / 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" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > arity< / 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" > return< / span > < span class = "plain-syntax" > < / span > < span class = "string-syntax" > "unary atom with other than one term"< / 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" > group< / span > < span class = "plain-syntax" > == < / span > < span class = "constant-syntax" > OPEN_OPERATORS_GROUP< / span > < span class = "plain-syntax" > ) || (< / span > < span class = "identifier-syntax" > group< / span > < span class = "plain-syntax" > == < / span > < span class = "constant-syntax" > CLOSE_OPERATORS_GROUP< / span > < span class = "plain-syntax" > ))< / span >
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "string-syntax" > "parentheses with terms"< / 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" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > element< / span > < span class = "plain-syntax" > == < / span > < span class = "constant-syntax" > QUANTIFIER_ATOM< / span > < span class = "plain-syntax" > ) & & (< / span > < span class = "identifier-syntax" > prop< / 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" > == -1))< / span >
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > < / span > < span class = "string-syntax" > "missing variable in quantification"< / 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" > NULL< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
2019-03-17 14:40:57 +02:00
< / pre >
2020-08-24 13:21:17 +03:00
< p class = "commentary firstcommentary" > < a id = "SP18" class = "paragraph-anchor" > < / a > < b > § 18. Writing to text. < / b > Logging atomic propositions divides into cases:
2020-05-03 03:01:21 +03:00
< / p >
< pre class = "displayed-code all-displayed-code code-font" >
2020-08-24 12:34:23 +03:00
< span class = "reserved-syntax" > void< / span > < span class = "plain-syntax" > < / span > < span class = "function-syntax" > Atoms::log< / 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" > Atoms::log< / span > < / span > :< br / > Calculus Module - < a href = "1-cm.html#SP3" > § 3< / 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 >
2020-08-24 13:21:17 +03:00
< span class = "plain-syntax" > < / span > < a href = "3-ap.html#SP18" class = "function-link" > < span class = "function-syntax" > Atoms::write< / span > < / a > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > DL< / span > < span class = "plain-syntax" > , < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > );< / span >
2020-08-07 12:39:22 +03:00
< span class = "plain-syntax" > }< / span >
2020-08-24 12:34:23 +03:00
< span class = "reserved-syntax" > void< / span > < span class = "plain-syntax" > < / span > < span class = "function-syntax" > Atoms::write< / 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" > Atoms::write< / span > < / span > :< br / > Propositions - < a href = "3-prp.html#SP7" > § 7< / a > < / span > < / button > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > text_stream< / span > < span class = "plain-syntax" > *< / span > < span class = "identifier-syntax" > OUT< / 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 >
2020-08-07 12:39:22 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < 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" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-syntax" > "< null-atom> "< / span > < span class = "plain-syntax" > ); < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > ; }< / span >
2020-08-24 13:21:17 +03:00
< span class = "plain-syntax" > < / span > < span class = "named-paragraph-container code-font" > < a href = "3-ap.html#SP18_1" class = "named-paragraph-link" > < span class = "named-paragraph" > Use a special notation for equality< / span > < span class = "named-paragraph-number" > 18.1< / span > < / a > < / 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-ap.html#SP9" class = "function-link" > < span class = "function-syntax" > Atoms::is_CALLED< / 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 = "identifier-syntax" > wording< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > W< / span > < span class = "plain-syntax" > = < / span > < a href = "3-ap.html#SP9" class = "function-link" > < span class = "function-syntax" > Atoms::CALLED_get_name< / span > < / a > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > );< / span >
2020-08-24 02:22:48 +03:00
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-syntax" > "called='%W'"< / span > < span class = "plain-syntax" > , < / span > < span class = "identifier-syntax" > W< / 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" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > assert_kind< / span > < span class = "plain-syntax" > ) {< / span >
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-syntax" > "("< / span > < span class = "plain-syntax" > );< / span >
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > Kinds::Textual::write< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > OUT< / span > < span class = "plain-syntax" > , < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > assert_kind< / span > < span class = "plain-syntax" > );< / span >
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-syntax" > ")"< / span > < span class = "plain-syntax" > );< / span >
< span class = "plain-syntax" > }< / span >
< span class = "plain-syntax" > } < / span > < span class = "reserved-syntax" > else< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > switch< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > element< / span > < span class = "plain-syntax" > ) {< / span >
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > case< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > PREDICATE_ATOM:< / span >
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > switch< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > arity< / span > < span class = "plain-syntax" > ) {< / span >
2020-08-24 13:21:17 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > case< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > 1< / span > < span class = "plain-syntax" > : < / span > < span class = "named-paragraph-container code-font" > < a href = "3-ap.html#SP18_2" class = "named-paragraph-link" > < span class = "named-paragraph" > Log some suitable textual name for this unary predicate< / span > < span class = "named-paragraph-number" > 18.2< / span > < / a > < / 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" > case< / span > < span class = "plain-syntax" > < / span > < span class = "constant-syntax" > 2< / span > < span class = "plain-syntax" > : < / span > < span class = "named-paragraph-container code-font" > < a href = "3-ap.html#SP18_3" class = "named-paragraph-link" > < span class = "named-paragraph" > Log some suitable textual name for this binary predicate< / span > < span class = "named-paragraph-number" > 18.3< / span > < / a > < / span > < span class = "plain-syntax" > ; < / span > < span class = "reserved-syntax" > break< / span > < span class = "plain-syntax" > ;< / span >
2020-08-07 12:39:22 +03:00
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > default:< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-syntax" > "?exotic-predicate-arity=%d?"< / span > < span class = "plain-syntax" > , < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > arity< / span > < span class = "plain-syntax" > ); < / span > < span class = "reserved-syntax" > break< / span > < span class = "plain-syntax" > ;< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > }< / span >
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > break< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > case< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > QUANTIFIER_ATOM:< / span > < span class = "plain-syntax" > {< / span >
2020-07-01 02:58:55 +03:00
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > quantifier< / span > < span class = "plain-syntax" > *< / span > < span class = "identifier-syntax" > quant< / span > < span class = "plain-syntax" > = < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > quant< / span > < span class = "plain-syntax" > ;< / span >
2020-08-07 12:39:22 +03:00
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > Quantifiers::log< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > OUT< / span > < span class = "plain-syntax" > , < / span > < span class = "identifier-syntax" > quant< / span > < span class = "plain-syntax" > , < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > quantification_parameter< / span > < span class = "plain-syntax" > );< / span >
2020-08-24 13:21:17 +03:00
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-syntax" > " "< / span > < span class = "plain-syntax" > ); < / span > < span class = "named-paragraph-container code-font" > < a href = "3-ap.html#SP18_4" class = "named-paragraph-link" > < span class = "named-paragraph" > Log a comma-separated list of terms for this atomic proposition< / span > < span class = "named-paragraph-number" > 18.4< / span > < / a > < / span > < span class = "plain-syntax" > ;< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > return< / span > < span class = "plain-syntax" > ;< / span >
< span class = "plain-syntax" > }< / span >
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > case< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > KIND_ATOM:< / span >
2020-08-07 12:39:22 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > Streams::I6_escapes_enabled< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > DL< / span > < span class = "plain-syntax" > ) == < / span > < span class = "identifier-syntax" > FALSE< / span > < span class = "plain-syntax" > ) < / span > < span class = "identifier-syntax" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-syntax" > "kind="< / span > < span class = "plain-syntax" > );< / span >
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > Kinds::Textual::write< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > OUT< / span > < span class = "plain-syntax" > , < / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > assert_kind< / 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" > Streams::I6_escapes_enabled< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > DL< / span > < span class = "plain-syntax" > ) == < / span > < span class = "identifier-syntax" > FALSE< / span > < span class = "plain-syntax" > ) & & (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > composited< / span > < span class = "plain-syntax" > )) < / span > < span class = "identifier-syntax" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-syntax" > "_c"< / 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" > Streams::I6_escapes_enabled< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > DL< / span > < span class = "plain-syntax" > ) == < / span > < span class = "identifier-syntax" > FALSE< / span > < span class = "plain-syntax" > ) & & (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > unarticled< / span > < span class = "plain-syntax" > )) < / span > < span class = "identifier-syntax" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-syntax" > "_u"< / span > < span class = "plain-syntax" > );< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > break< / span > < span class = "plain-syntax" > ;< / span >
2020-08-22 20:52:28 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > case< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > NEGATION_OPEN_ATOM:< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-syntax" > "NOT< "< / 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" > case< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > NEGATION_CLOSE_ATOM:< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-syntax" > "NOT> "< / 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" > case< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > DOMAIN_OPEN_ATOM:< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-syntax" > "IN< "< / 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" > case< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > DOMAIN_CLOSE_ATOM:< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-syntax" > "IN> "< / span > < span class = "plain-syntax" > ); < / span > < span class = "reserved-syntax" > break< / span > < span class = "plain-syntax" > ;< / span >
2020-08-07 12:39:22 +03:00
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > default:< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-syntax" > "?bad-atom?"< / span > < span class = "plain-syntax" > ); < / span > < span class = "reserved-syntax" > break< / span > < span class = "plain-syntax" > ;< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > }< / span >
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > arity< / span > < span class = "plain-syntax" > > < / span > < span class = "constant-syntax" > 0< / span > < span class = "plain-syntax" > ) {< / span >
2020-08-23 14:00:56 +03:00
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-syntax" > "("< / span > < span class = "plain-syntax" > );< / span >
2020-08-24 13:21:17 +03:00
< span class = "plain-syntax" > < / span > < span class = "named-paragraph-container code-font" > < a href = "3-ap.html#SP18_4" class = "named-paragraph-link" > < span class = "named-paragraph" > Log a comma-separated list of terms for this atomic proposition< / span > < span class = "named-paragraph-number" > 18.4< / span > < / a > < / span > < span class = "plain-syntax" > ;< / span >
2020-08-23 14:00:56 +03:00
< span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-syntax" > ")"< / span > < span class = "plain-syntax" > );< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > }< / span >
< span class = "plain-syntax" > }< / span >
2019-03-17 14:40:57 +02:00
< / pre >
2020-08-24 13:21:17 +03:00
< p class = "commentary firstcommentary" > < a id = "SP18_1" class = "paragraph-anchor" > < / a > < b > § 18.1. < / b > < span class = "named-paragraph-container code-font" > < span class = "named-paragraph-defn" > Use a special notation for equality< / span > < span class = "named-paragraph-number" > 18.1< / span > < / span > < span class = "comment-syntax" > =< / span >
2020-08-23 14:00:56 +03:00
< / 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" > prop< / 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" > prop< / 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" > prop< / 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 = "identifier-syntax" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-syntax" > "("< / span > < span class = "plain-syntax" > );< / span >
< span class = "plain-syntax" > < / span > < a href = "3-trm.html#SP12" class = "function-link" > < span class = "function-syntax" > Terms::write< / span > < / a > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > OUT< / span > < span class = "plain-syntax" > , & (< / span > < span class = "identifier-syntax" > prop< / 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" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-syntax" > " == "< / span > < span class = "plain-syntax" > );< / span >
< span class = "plain-syntax" > < / span > < a href = "3-trm.html#SP12" class = "function-link" > < span class = "function-syntax" > Terms::write< / span > < / a > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > OUT< / span > < span class = "plain-syntax" > , & (< / span > < span class = "identifier-syntax" > prop< / 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" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-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 = "plain-syntax" > }< / span >
< / pre >
2020-08-24 13:21:17 +03:00
< ul class = "endnotetexts" > < li > This code is used in < a href = "3-ap.html#SP18" > § 18< / a > .< / li > < / ul >
< p class = "commentary firstcommentary" > < a id = "SP18_2" class = "paragraph-anchor" > < / a > < b > § 18.2. < / b > < span class = "named-paragraph-container code-font" > < span class = "named-paragraph-defn" > Log some suitable textual name for this unary predicate< / span > < span class = "named-paragraph-number" > 18.2< / span > < / span > < span class = "comment-syntax" > =< / span >
2020-05-03 03:01:21 +03:00
< / p >
2019-03-17 14:40:57 +02:00
2020-05-03 03:01:21 +03:00
< pre class = "displayed-code all-displayed-code code-font" >
2020-07-01 02:58:55 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > unary_predicate< / span > < span class = "plain-syntax" > *< / span > < span class = "identifier-syntax" > tr< / span > < span class = "plain-syntax" > = < / span > < span class = "identifier-syntax" > RETRIEVE_POINTER_unary_predicate< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > predicate< / span > < span class = "plain-syntax" > );< / span >
2020-08-24 02:22:48 +03:00
< span class = "plain-syntax" > < / span > < a href = "2-upf.html#SP8" class = "function-link" > < span class = "function-syntax" > UnaryPredicateFamilies::log< / span > < / a > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > OUT< / span > < span class = "plain-syntax" > , < / span > < span class = "identifier-syntax" > tr< / span > < span class = "plain-syntax" > );< / span >
2019-03-17 14:40:57 +02:00
< / pre >
2020-08-24 13:21:17 +03:00
< ul class = "endnotetexts" > < li > This code is used in < a href = "3-ap.html#SP18" > § 18< / a > .< / li > < / ul >
< p class = "commentary firstcommentary" > < a id = "SP18_3" class = "paragraph-anchor" > < / a > < b > § 18.3. < / b > < span class = "named-paragraph-container code-font" > < span class = "named-paragraph-defn" > Log some suitable textual name for this binary predicate< / span > < span class = "named-paragraph-number" > 18.3< / span > < / span > < span class = "comment-syntax" > =< / span >
2020-05-03 03:01:21 +03:00
< / p >
2019-03-17 14:40:57 +02:00
2020-05-03 03:01:21 +03:00
< pre class = "displayed-code all-displayed-code code-font" >
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > 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" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > predicate< / span > < span class = "plain-syntax" > );< / span >
2020-08-22 00:38:20 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > bp< / span > < span class = "plain-syntax" > == < / span > < span class = "identifier-syntax" > NULL< / span > < span class = "plain-syntax" > ) < / span > < span class = "identifier-syntax" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-syntax" > "?bad-bp?"< / span > < span class = "plain-syntax" > ); < / span > < span class = "reserved-syntax" > else< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-syntax" > "%S"< / span > < span class = "plain-syntax" > , < / span > < a href = "2-bp.html#SP33" class = "function-link" > < span class = "function-syntax" > BinaryPredicates::get_log_name< / span > < / a > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > bp< / span > < span class = "plain-syntax" > ));< / span >
2019-03-17 14:40:57 +02:00
< / pre >
2020-08-24 13:21:17 +03:00
< ul class = "endnotetexts" > < li > This code is used in < a href = "3-ap.html#SP18" > § 18< / a > .< / li > < / ul >
< p class = "commentary firstcommentary" > < a id = "SP18_4" class = "paragraph-anchor" > < / a > < b > § 18.4. < / b > < span class = "named-paragraph-container code-font" > < span class = "named-paragraph-defn" > Log a comma-separated list of terms for this atomic proposition< / span > < span class = "named-paragraph-number" > 18.4< / span > < / span > < span class = "comment-syntax" > =< / span >
2020-05-03 03:01:21 +03:00
< / p >
2019-03-17 14:40:57 +02:00
2020-05-03 03:01:21 +03:00
< pre class = "displayed-code all-displayed-code code-font" >
2020-08-23 14:00:56 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > for< / span > < span class = "plain-syntax" > (< / span > < span class = "reserved-syntax" > int< / span > < span class = "plain-syntax" > < / span > < span class = "identifier-syntax" > t< / span > < span class = "plain-syntax" > =0; < / span > < span class = "identifier-syntax" > t< / span > < span class = "function-syntax" > < prop-> < / span > < span class = "element-syntax" > arity< / span > < span class = "plain-syntax" > ; < / span > < span class = "identifier-syntax" > t< / span > < span class = "plain-syntax" > ++) {< / span >
2020-08-07 12:39:22 +03:00
< span class = "plain-syntax" > < / span > < span class = "reserved-syntax" > if< / span > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > t< / span > < span class = "plain-syntax" > > 0) < / span > < span class = "identifier-syntax" > WRITE< / span > < span class = "plain-syntax" > (< / span > < span class = "string-syntax" > ", "< / span > < span class = "plain-syntax" > );< / span >
2020-08-23 14:00:56 +03:00
< span class = "plain-syntax" > < / span > < a href = "3-trm.html#SP12" class = "function-link" > < span class = "function-syntax" > Terms::write< / span > < / a > < span class = "plain-syntax" > (< / span > < span class = "identifier-syntax" > OUT< / span > < span class = "plain-syntax" > , & (< / span > < span class = "identifier-syntax" > prop< / span > < span class = "plain-syntax" > -> < / span > < span class = "element-syntax" > terms< / span > < span class = "plain-syntax" > [< / span > < span class = "identifier-syntax" > t< / span > < span class = "plain-syntax" > ]));< / span >
2020-05-03 03:01:21 +03:00
< span class = "plain-syntax" > }< / span >
2019-03-17 14:40:57 +02:00
< / pre >
2020-08-24 13:21:17 +03:00
< ul class = "endnotetexts" > < li > This code is used in < a href = "3-ap.html#SP18" > § 18< / a > (twice).< / li > < / ul >
2020-05-03 03:01:21 +03:00
< nav role = "progress" > < div class = "progresscontainer" >
2020-08-22 00:58:58 +03:00
< ul class = "progressbar" > < li class = "progressprev" > < a href = "3-trm.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-cs.html" > 2< / a > < / li > < li class = "progresscurrentchapter" > 3< / li > < li class = "progresssection" > < a href = "3-trm.html" > trm< / a > < / li > < li class = "progresscurrent" > ap< / li > < li class = "progresssection" > < a href = "3-prp.html" > prp< / a > < / li > < li class = "progresssection" > < a href = "3-bas.html" > bas< / a > < / li > < li class = "progressnext" > < a href = "3-prp.html" > ❯ < / a > < / li > < / ul > < / div >
2020-05-03 03:01:21 +03:00
< / nav > <!-- End of weave -->
2019-03-17 14:40:57 +02:00
2020-03-19 02:11:25 +02:00
< / main >
2019-03-17 14:40:57 +02:00
< / body >
< / html >
