This section specifies the language of expressions that is used to represent the different components of a rule supported by RIF-PRD. The language is called the language of conditions, because it extends the language of conditions of [ RIF-Core], that determines what can appear as a condition in a rule supported by RIF-Core. The language plays a similar role in RIF-PRD.
In the first part of this section, the syntax of RIF-PRD condition language is specified non-normatively: the normative reference for the XML syntax is the [ XML schema].
In the second part, the normative semantics of RIF-PRD condition language is specified.
Syntax
The overall structure of the syntax used to represent the condition part of production rules in RIF-PRD condition sublanguage is depicted on the following diagram.
*** Should we have structural diagrams in PRD, or should we rather align on BLD and not have them (or should we align BLD and add them in BLD)? ***
The most basic construct in RIF is the TERM. The TERM is an abstract construct, concretly visible, in RIF-PRD, as a Const, a Var or an ExtTerm.
The ATOMIC is the basic building block of RIF. ATOMIC is an abstract class: it is visible in RIF-PRD as either an Uniterm, an ExtTerm, an Equal, a Member, a Subclass or a Frame. Notice that, for clarity, only the basic form of the Frame construct is represented in the diagram: in addition, the syntax of RIF-PRD condition language allows the representation of nested and composite Frames. However, a nested and composite Frame can always be represented as a conjunction of basic Frames and other ATOMIC constructs. Each kind of ATOMIC is a composition of TERMs.
The next level of constructs are assemblies of ATOMICs. Together, the various kinds of assemblies form the abstract construct CONDITION. RIF-PRD knows five kinds of CONDITIONs: the single ATOMIC, and the recursively specified And, Or, Naf and Exists.
The Exists construct also belongs to the QUANTIFICATION abstract class, that specifies the notions of variable binding and of an Aggregation.
The following sections specify each construct separately, grouped by abstract syntactic classes. Each element is given an XML syntax, in the form of a BNF pseudo schema; a presentation syntax, in the form of an EBNF production; and a description of the intended use of each construct, that is, informally, of its semantics. None of these is normative: the normative XML syntax is given in the [ RIF-PRD XML schema] and the normative semantics is given in the section [ Operational semantics].
TERM
The TERM class of constructs is used to represent constants, variables and the application of function symbols to other TERMs.
XML syntax. As an abstract class, TERM is not associated with specific XML markup in RIF-PRD instance documents. It is specified in the normative schema as a substitution group.
*** ...Substitution group or another construct, depending on how we handle extensibility in the XML schema. ***
[ Const | Var | ExtTerm ]
*** Difference wrt RIF-BLD: in RIF-PRD, there are no logic functions => a TERM cannot be a (non evaluated) Uniterm. ***
*** Difference wrt RIF-BLD: The latest version of BLD seems to allow any COUMPOUND (ex-ATOMIC) as TERM. As this has not been discussed yet, that idfference is not commented here. ***
Presentation syntax.
TERM ::= Const | Var | ExtTerm
Const
In RIF, the Const construct is used to represent a constant. The constant is represented by a character string; it is associated with an identifier of the constant's type and, optionally where permitted, a language identifier.
XML syntax. The Const element has a required type attribute and an optional xml:lang attribute:
The value of the type attribute is the name of the Const type. It must be an absolute IRI;
The xml:lang attribute, as defined by 2.12 Language Identification of XML 1.0 or its successor specifications in the W3C recommandation track, is optionally used to identify the language for the presentation of the Const to the user. It is allowed only in association with constants of the type rif:text. A compliant implementation MUST ignore the xml:lang attribute if the type of the Const is not rif:text.
The content of the Const element is the constant's symbol, which can be any Unicode character string.
*** Or should constant litterals be limited to xs:NormalizedString instead? ***
<Const type="IRI" [xml:lang="xs:language"]? > Any Unicode string </Const>
Presentation syntax.
Const ::= LITERAL '^^' TYPE [ '@' LANGUAGE_ID ]
Constant types. RIF-PRD conformant implementations MUST support the following builtin constant types:
xsd:long (http://www.w3.org/2001/XMLSchema#long), as defined in the document XML Schema Part 2: Datatypes;
xsd:string (http://www.w3.org/2001/XMLSchema#string), as defined in the document XML Schema Part 2: Datatypes;
xsd:integer (http://www.w3.org/2001/XMLSchema#integer), as defined in the document XML Schema Part 2: Datatypes;
xsd:decimal (http://www.w3.org/2001/XMLSchema#decimal), as defined in the document XML Schema Part 2: Datatypes;
xsd:time (http://www.w3.org/2001/XMLSchema#time), as defined in the document XML Schema Part 2: Datatypes;
xsd:dateTime (http://www.w3.org/2001/XMLSchema#dateTime), as defined in the document XML Schema Part 2: Datatypes;
rdf:XMLLiteral (http://www.w3.org/1999/02/22-rdf-syntax-ns#XMLLiteral), as defined in the document Resource Description Framework (RDF): Concepts and Abstract Syntax;
rif:text, for text strings with language tags attached. The language tag requires a special treatment of rif:text constants with respect to the XML syntax;
rif:iri, for internationalized resource identifier or IRI. This type is used to represent constants that are intended to be used in a way similar to RDF resources. The lexical space consists of all absolute IRIs as specified in RFC 3987; it is unrelated to the XML primitive type anyURI. A rif:iri constant is supposed to be interpreted as a reference to one and the same object regardless of the context in which that constant occurs.
rif:local, for constant symbols that are not visible outside of a particular set of rules interchanged in RIF. Constants of this type are used locally in their respective rule sets. This means that occurrences of the same rif:local-constant in different rule sets are viewed as unrelated distinct constants, but occurrences of the same constant in the same rule set must refer to the same object. The lexical space of rif:local is the same as the lexical space of xsd:string.
Symbols with an ill-formed lexical part. Constants that are represented in RIF in one of the aforesaid builtin types must be well-formed, i.e., their representation must belong to the lexical space associated with the type. For instance, 123^^xsd:long (that is, <Const type="xsd:long">123</Const>) has a correct lexical part, since 123 belongs to the lexical space of the data type xsd:long. In contrast, abc^^xsd:long (<Const type="xsd:long">abc</Const>) is ill-formed, as it does not have a correct lexical part. A compliant RIF-PRD translator MUST reject ill-formed symbols.
Symbols with non-standard types. RIF-PRD builtin types are meant to be used for the interchange of constants that belong to the corresponding XML and RDF types. They can also be used for the interchange of constants with non builtin, application specific types with overlaping lexical and value spaces or similar behaviours: this may require additional translations steps and may result in unexpected or incorrect results; in addition, the information regarding the original types is lost in RIF-PRD, which may affect round-tripping.
Constants that do not belong or cannot be cast in one of RIF builtin types for interchange purposes, can be represented using the same LITERAL^^TYPE (i.e. <Const type="TYPE">LITERAL</Const>) syntax, where TYPE is not one of the RIF builtin types. RIF does not ascribe any specific lexical space to these types and any Unicode string should be considered a well-formed constant symbol as far as RIF is concerned. In the same way, RIF does not ascribe any particular semantics to such non-builtin TYPEs: it is the responsibility of the producers and consumers of RIF-PRD rulesets that reference types that are not built in RIF-PRD to agree on their lexical space and on their semantics.
Dialects that extend RIF-PRD might define additional builtin types, give them special semantics and appropriate the names of some non-standard types to name them.
Informal semantics. The LITERAL of a constant represents the value of that constant according to its TYPE.
Examples. In each of the examples below, a constant is first described, followed by its represented in RIF XML syntax (left) and in RIF presentation syntax (right).
a. A constant with builtin type xsd:integer and value 123:
<Const type="xsd:integer"> 123 </Const> | 123^^xsd:integer |
b. A constant with non-builtin type xsd:int and value 123:
<Const type="xsd:int"> 123 </Const> | 123^^xsd:int |
c. A constant whose symbol myConst is defined in the namespace identified by the prefix myXs:
<Const type="rif:iri"> myXs:myConst </Const> | myXs:myConst^^rif:iri |
d. A constant with symbol myLocalCst that is local to the set of rules where it appears:
<Const type="rif:local"> myLocalCst </Const> | myLocalCst^^rif:local |
Var
In RIF, the Var construct is used to represent variables.
XML syntax. The content of the Var element is the variable's name, represented as an Unicode character string.
*** Shouldn't variable's names rather be limited to be, e.g. xs:NMTOKEN? ***
<Var> xs:NMTOKEN </Var>
*** Or should Var have a type attribute (and we could, maybe, get rid of the Member construct)? ***
*** Difference wrt RIF-BLD: RIF-BLD says only that a Var element contains a VARNAME. However, most implemented rule languages enforce some syntactic restrictions on the name of variables and requiring all RIF implementations to support any Unicode string as VARNAMEs might be an additional burden with little benefits associated. This is a proposed alternative: whatever the decision, BLD and PRD should use the same definition. ***
Presentation syntax.
Var ::= VARNAME
*** Difference wrt RIF-BLD: BLD says Var ::= '?' VARNAME: according to that production, wouldn't a variable that is named ?X in a rule become ??x in RIF? This is a proposed alternative: whatever the decision, BLD and PRD should use the same definition. ***
Informal semantics. The semantics of the variable that is represented by a Var element is specified by a variable binding that maps the variable to a value or an individual.
*** What about binding to variables too? (AdrianP) ***
ExtTerm
As a TERM, an ExtTerm is used to represent an evaluated function.
*** builtin function, evaluated function, or fixed interpretation function... need consistent terminology (Gary) ***
As explained in the Overview, for compatibility reasons, individuals, function symbols and predicate symbols in RIF, all belong to the same set of constants. As a consequence, the same ExtTerm construct is used to represent both evaluated functions and evaluated predicates (or relations).
However, this is more general than what is needed in RIF-PRD: in RIF-PRD, the ExtTerm construct can only be used to represents an evaluated function when it is a TERM (that is, in particular, when it appears in a place where a TERM is required).
XML syntax. The ExtTerm element contains one op element, followed by zero or more arg elements:
The content of the op element must be a construct from the TERM abstract class. When the ExtTerm is a TERM, the content of the op element represents a function symbol;
*** Or should the op element be restricted to contain a Const element only? ***
The content of the arg elements must be constructs from the TERM abstract class. The order of the arg elements is significant and MUST be preserved.
<ExtTerm> <op> TERM </op> <arg> TERM </arg>* </ExtTerm>
*** Difference wrt RIF-BLD: The construct for representing builtins does not seem to be included in RIF-BLD yet. The label ExtTerm is used in the syntax proposals in the List of BLD built-ins. This is a proposal: whatever the decision, BLD and PRD should use the same definition.***
Presentation syntax.
ExtTerm ::= ' Builtin( ' TERM ' ( ' TERM* ' )) '
*** The problem with the "Builin" notation is that all fixed interpretation functions need not be builtin... ***
Builtin functions. RIF-PRD specifies a subset of XPath/XQuery Functions and Operators [X F&O] that any conformant RIF-PRD implementation MUST support. The RIF-PRD builtin functions are listed in the appendix [ List of Builtin Functions and Operators].
Informal semantics. ExtTerms are used to represent procedural attachments: their semantics is always specified outside of a RIF instance document where they appear.
The op TERM must represent a constant symbol of type rif:iri that must uniquely identify the evaluated function to be applied to the arg TERMs. It can be one of the builtin functions specified for RIF-PRD, or it can be application specific. In the latter case, it is the responsibility of the producers and consumers of RIF-PRD rulesets that reference non-builtin functions to agree on their semantics.
An evaluated function applied to arguments in its domain of definition evaluates to a constant value in its range: subject to the binding of its variable arguments, the external call represented by an ExtTerm TERM is another equivalent representation of that constant.
Arguments out of the domain of definition. For arguments out of its domain of definition, the value of an evaluated function is not defined. RIF-PRD does not specify any expected behaviour for that case: it is the responsibility of the consummer of a RIF-PRD ruleset to know the expected behaviour or to handle the error.
Examples. The example below shows one way to represent, in RIF-PRD, the sum of integer 1 and variable ?X, where the addition conforms to the specification of the builtin fn:numeric-add.
The prefix fn is associated with the namespace http://www.w3.org/2005/xpath-functions.
XML syntax.
<ExtTerm> <op> <Const type="rif:iri"> fn:numeric-add </Const> </op> <arg> <Const type="xsd:integer"> 1 </Const> </arg> <arg> <Var> ?X </Var> </arg> </ExtTerm>
Presentation syntax.
Builtin(fn:numeric-add^^rif:iri(1^^xsd:integer ?X))
ATOMIC
The ATOMIC class is used to represent atomic truth-valued statements. RIF-PRD covers rule languages in which the truth values of atomic statements can only be "true" or "false": that is, ATOMICs represent boolean statements. Dialects extending RIF-PRD may support additional truth values.
XML syntax. As an abstract class, ATOMIC is not associated with specific XML markup in RIF-PRD instance documents. It is specified in the normative schema as a substitution group.
*** ...Substitution group or another construct, depending on how we handle extensibility in the XML schema. ***
[ Uniterm | ExtTerm | Equal | Member | Subclass | Frame ]
*** Difference wrt RIF-BLD: The lates version of BLD changed the name of ATOMIC to COMPOUND. As no decision has been made about this yet (nor about naming in general), this draft keeps by the previous name. Whatever the decision, BLD and PRD should use the same definition. ***
Presentation syntax.
ATOMIC ::= [ Uniterm | ExtTerm | Equal | Member | Subclass | Frame ]
Uniterm
As explained in the Overview, for compatibility reasons, individuals, function symbols and predicate symbols in RIF, all belong to the same set of constants. As a consequence, the same Uniterm construct could potentially be used to represent functions as well as predicates (or relations). However, this is more general than what is needed in RIF-PRD: in RIF-PRD, an Uniterm is always used to represent a predicate, and it is always an ATOMIC. Other dialects, including extensions of RIF-PRD, may extend this.
XML syntax. The Uniterm element contains one op element, followed by zero or more arg arguments:
The content of the op element must be a Const element that represents the predicate symbol (the name of a relation);
*** Or should the op element be allowed to be any TERM instead? ***
The content of the arg elements must be constructs from the TERM abstract class. The order of the arg elements is significant and MUST be preserved.
<Uniterm> <op> Const </op> <arg> TERM </arg>* </Uniterm>
*** Difference wrt RIF-BLD: Not sure what is the support for relational atoms where the predicate would not be a constant, among production rule languages. Hence the question above. Depending on the answer, it might make sense for PRD to differ from BLD here. The benefits and drawbacks (e.g. wrt the definition of Core) have to be weighted. ***
*** Difference wrt RIF-BLD: Named arguments Uniterms do not seem to have much support in production rule languages => They are not included in this draft. PRD and BLD might differ in this respect. A consequence would be that Core would not have named argument Uniterms. ***
Presentation syntax.
Uniterm ::= Const ' ( ' TERM* ' ) '
Informal semantics. The Uniterm ATOMIC is used to represent an atomic statement that is true iff the individuals or values represented by the args elements are known to satisfy the predicate (relation) represented by the op element.
ExtTerm
As an ATOMIC, an ExtTerm is used to represent an evaluated relation.
As explained in the Overview, for compatibility reasons, individuals, function symbols and predicate symbols in RIF, all belong to the same set of constants. As a consequence, the same ExtTerm construct is used to represent both evaluated functions and evaluated predicates (or relations). However, this is more general than what is needed in RIF-PRD.
In RIF-PRD, an ExtTerm represents always an evaluated predicate when it is an ATOMIC (that is, in particular, when it appears in a place where an ATOMIC is required).
XML syntax. The ExtTerm element contains one op element, followed by zero or more arg arguments:
When the ExtTerm is an ATOMIC, the content of the op element must be a construct from the TERM abstract class. When the ExtTerm is an ATOMIC, the content of the op sub-element represents a predicate symbol;
*** Or should the op element be restricted to contain a Const element only? ***
The content of the arg elements must be constructs from the TERM abstract class. The order of the arg elements is significant and MUST be preserved.
<ExtTerm> <op> TERM </op> <arg> TERM </arg>* </ExtTerm>
*** Difference wrt RIF-BLD: Same remark as wrt the TERM ÈxtTerm`. ***
Presentation syntax.
ExtTerm ::= ' Builtin( ' TERM ' ( ' TERM* ' )) '
*** In addition to the problem with the "Builtin" notation applying to fct that may be user-defined, is not the ExtTerm ::= ' Builtin( ' Uniterm ' ) ' kind of confusing? I know that they are equivalent, but I prefer to keep by the developed production (CSMA) ***
Builtin predicates. RIF-PRD specifies a subset of XPath/XQuery Functions and Operators [X F&O] that any conformant RIF-PRD implementation MUST support. The RIF-PRD builtin predicates are listed in the appendix [ List of Builtin Functions and Operators].
Informal semantics. ExtTerms are used to represent procedural attachments: their semantics is always specified outside of a RIF instance document where they appear.
The op TERM must represent a constant symbol of type rif:iri that must uniquely identify the evaluated predicate to be applied to the arg TERMs. It can be one of the builtin predicates specified for RIF-PRD, or it can be application specific. In the latter case, it is up to the producers and consumers of RIF-PRD rulesets that reference non-builtin predicates to agree on their semantics.
Arguments out of the domain of definition. An evaluated predicate applied to arguments within its domain of definition evaluates to a truth value. For arguments out of its domain of definition, the truth value of an evaluated predicate is not defined.
RIF-PRD does not specify any expected behaviour for that case: it is the responsibility of the consummer of a RIF-PRD ruleset to know the expected behaviour or to handle the error.
Equal
In RIF, Equal is used to represent equality relations.
*** Or should RIF-PRD have only evaluated (builtin + application specific) equality relations? ***
XML syntax. The Equal element must contain two unordered side elements. The content of each side element must be a construct from the TERM abstract class. The order of the side elements is not significant and must not be preserved.
<Equal> <side> TERM </side> <side> TERM </side> </Equal>
Presentation syntax.
Equal ::= TERM ' = ' TERM
Informal semantics. The Equal element is used to represent a predicate that is is true iff the values or individuals represented by the Equal's side TERMs are equal.
Member
In RIF, the Member element is used to represent membership relations.
*** Or should RIF-PRD have only evaluated (builtin + application specific) membership relations? ***
XML syntax. The Member element contains two sub-elements:
the object elements must be a construct from the TERM abstract class. It is required;
the class element must be a construct from the TERM abstract class. It is required as well.
<Member> <object> TERM </object> <class> TERM </class> </Member>
*** Difference wrt RIF-BLD: object and class make more sense to me as the roles in a membership relation than BLD's lower and upper. But, as noticed earlier, the discussion about naming is still to be had, and I do not care that much about label's names anyway... This is a proposed alternative: whatever the decision, BLD and PRD should use the same definition. ***
Presentation syntax.
Member ::= TERM ' # ' TERM
Informal semantics. The Member construct is used to represent predicates that are true iff there is a known classification according to which the argument that is represented by the class TERM is a class and the value or individual that is represented by the object TERM is a member of that class.
Subclass
In RIF, the Subclass element is used to represent class inclusion relations.
*** Or should RIF-PRD have only evaluated (builtin + application specific) subclass relations? ***
XML syntax. The Subclass element contains two sub-elements:
the subClass element must be a construct from the TERM abstract class. It is required as well;
the class elements must be a construct from the TERM abstract class. It is required.
<Subclass> <subClass> TERM </subClass> <class> TERM </class> </Subclass>
*** Difference wrt RIF-BLD: BLD's lower and upper make more sense. I kept class for the upper element for consistency with the Member element, and subClass seemmed to make more sense, associated with class than lower would. But, again, I am not religious about tags. This is a proposed alternative: whatever the decision, BLD and PRD should use the same definition. ***
Presentation syntax.
Subclass ::= TERM ' ## ' TERM
Informal semantics. The Subclass construct is used to represent predicates that are true iff there is a known classification according to which the arguments represented by the TERMs in the subClass and class sub-elements are both classes and the former is a sub-class of the latter.
Frame
In RIF, the Frame construct is used to represent relations that hold between an individual, also called an object, and the value of one of its properties or attributes: that is, object-attribute-value triples.
XML syntax. Accordingly, in its basic form, a Frame element must contain:
an object element, that contains an element of the TERM abstract class, the content of which represents the individual;
a slotKey element, that contains a Const element that represents the name of the attribute (or property);
*** Or should the slotKey element be allowed to contain any TERM instead? ***
a slotValue element, that contains an element of the TERM abstract class, the content of which represents the attribute's value.
*** Or should empty frames be allowed (and, thus, the slotKey-slotValue pair optional)? If yes: how to forbid a slotKey element without a slotValue, or reciprocally, without breaking the striping? ***
<Frame> <!-- Basic form --> <object> TERM</object> <slotKey> Const </slotKey> <slotValue> TERM </slotValue> </Frame>
*** Difference wrt RIF-BLD: in RIF-BLD, a basic Frame has only two sub-elements: object and slot; where slot has two contents: the key and the filler. Although the XML syntax has not been discussed yet, I suppose that the rationale is to preserve the association of the value to the key, but, on the other hand, it seems to break the stripping. So, here is an alternative proposal, that preserve the stripping, but where the association of value to key has to be preserved by the implementation. This is a proposed alternative: whatever the decision, BLD and PRD should use the same definition. ***
*** Difference wrt RIF-BLD: Not sure what is the support for Frames where the slot name would not be a constant, among production rule languages. Hence the question above. Depending on the answer, whether PRD and BLD should differ will be considered. ***
*** Difference wrt RIF-BLD: Not sure about the semantics of an empty Frame (no slot/value pair); and not sure that it would be the same in BLD and PRD. Hence the question. Not sure about PRD and BLD differeng on this one, either. ***
However, the syntax of the Frame element allows also to represent compactly the predication of multiple object-attribute-value triples for the same object. In that compact form, the frame element contains one single object element and one or more ordered pairs of slotKey-slotValue elements.
In addition, Frame elements can be nested, that is, a complete Frame element is allowed as the content of a slotValue element, instead of a TERM: this allows to represent in a compact way object-attribute-value triples where the value is itself qualified.
Finally, the syntax of the Frame element allows the object element to contain a Member or a Subclass element instead of a TERM: this permits the direct representation in RIF of compact atomic statements that contain classification information about the subject individual within object-attribute-value triples. In that form, the Frame is about the individual represented by the content of the object sub-element within the Member element or the subClass sub-element within the Subclass element.
As a consequence, the Frame element, in its most complete form, contains:
a single object element, that is required. The content of the object element can be a construct of the TERM abstract class, a Member element, or a Subclass element;
- one or more ordered pair of
a slotKey element, that must contain a Const element;
*** Ditto: should the slotKey element be allowed to contain any TERM instead? ***
a slotValue element. The content of the slotValue element can be a construct of the TERM abstract class or a Frame element.
The pairs are not ordered, but within each pair, the order slotKey-slotValue MUST be preserved.
<Frame> <!-- Complete specification --> <object> [ TERM | Member| Subclass ]</object> [ <slotKey> Const </slotKey> <slotValue> [ TERM | Frame ] </slotValue> ]+ </Frame>
Presentation syntax.
Frame ::= [TERM | Member | Subclass] ' [ ' (Const ' -> ' (TERM | Frame))+ ' ] '
Informal semantics. The basic Frame construct is used to represent object-attribute-value triples that are true iff the individual that is represented by the TERM in the object sub-element of the Frame is known to have the value represented by the TERM in its slotValue sub-element for the property, or attribute, represented by the Const in its slotKey sub-element.
A nested or combined Frame is used to represent a statement that is true if all the atomic statements represented by the ATOMICs that are nested and combined in the Frame are true.
CONDITION
The CONDITION class is used to represent any truth-valued statement, atomic or not, that is allowed in the condition part of a rule covered by RIF-PRD. In rule languages covered by RIF-PRD, the truth values of statements can be "true" or "false": that is, CONDITIONs can only represent boolean statements.
Dialects extending RIF-PRD may support additional truth values.
XML syntax. As an abstract class, CONDITION is not associated with specific XML markup in RIF-PRD instance documents. It is specified in the normative schema as a substitution group.
*** ...Substitution group or another construct, depending on how we handle extensibility in the XML schema. ***
[ ATOMIC | And | Or | Naf | Exists ]
*** Difference wrt RIF-BLD: a RIF-PRD without a construct for closed-world negation would not make mush sense; hence the addition of the Naf construct wrt BLD. This construct is specific to PRD. ***
Presentation syntax.
CONDITION ::= ATOMIC | And | Or | Naf | Exists
ATOMIC
A CONDITION can be a single ATOMIC statement. See specification of [ ATOMIC], above.
And
A CONDITION can represent the conjunction of zero of more statements, each of them represented by a CONDITION. This is represented by the And construct.
XML syntax. The And element contains zero or more formula elements, each containing an element of the CONDITION group.
<And> <formula> CONDITION </formula>* </And>
Presentation syntax.
And ::= 'AND ( ' CONDITION* ' ) '
Informal semantics. The And construct is used to represent a statements that is true iff:
it is an empty conjunction, represented by an empty And element;
or all the sub-statements represented by the CONDITIONs in the And's formula sub-elements are true.
Or
A CONDITION can represent the disjunction of zero of more statements, each of them represented by a CONDITION. This is represented by the Or construct.
XML syntax. The Or element contains zero or more formula elements, each containing an element of the CONDITION group.
<Or> <formula> CONDITION </formula>* </Or>
Presentation syntax.
Or ::= ' OR ( ' CONDITION* ' ) '
Informal semantics. The Or construct is used to represent a statements that is true iff:
it is not an empty disjunction, that is, if it has at least one non-empty formula sub-element;
and at least one of the sub-statements represented by the CONDITIONs in the Or's formula sub-elements is true.
Naf
A CONDITION can represent the non-monotonic negation of a statement, itself represented by a CONDITION: this is represenetd by the NAF construct.
XML syntax. The Naf element contains exactly one formula element. The formula element contains an element of the CONDITION group, that represents the negated statement.
<Naf> <formula> CONDITION </formula> </Naf>
*** Difference wrt RIF-BLD: that construct is specific to RIF-PRD. ***
Presentation syntax.
Naf ::= ' NAF ( ' CONDITION ' ) '
Informal semantics. The Naf construct is used to represent statements that are true iff the statement represented by the CONDITION formula is not known to be true.
*** What is the truth value of an empty NAF? ***
Exists
*** is this needed in addition to 2.1.4.2.? (Gary) ***
A CONDITION can represent an existentially quantified formula of the CONDITION class: this is represented by the Exists construct.
*** Difference wrt RIF-BLD: The notion of an aggregate variable is rather basic in production rule languages, much more than in logic languages, I guess. Therefore, due to the different semantics of Var in BLD and PRD, aggregation should be at least considered for inclusion in PRD, even if it is not in BLD. See also the remark under the specification of Exists, in the QUANTIFICATION Section, below. ***
In addition of being a CONDITION, Exists is also a concrete construct of the QUANTIFICATION class. It is further specified under that class, below.
QUANTIFICATION
The QUANTIFICATION class is used to represent any quantified formula that is allowed in rules covered by RIF-PRD. In rule languages covered by RIF-PRD, only existential quantification, represented by the Exists construct, is allowed in the condition language. RIF-PRD allows universal quantification, represented by the Forall construct, only at the rule level [ Rule section].
Dialects extending RIF-PRD may support the use of these quantifiers in additional positions, as well as additional quantifiers.
The overall structure of the syntax used to represent quantification in RIF-PRD is depicted on the following diagram.
QUANTIFICATION is an abstract class: it is visible in RIF-PRD as either an Exists or a Forall.
*** Difference wrt RIF-BLD: The abstract QUANTIFICATION class has been added as a didactic device, to make the specification of aggregation easier. It might also be useful as an extension point in the future. ***
All the constructs of the QUANTIFICATION class share a common structure. They have:
one or more declare sub-elements, each containing either:
a Var element that represents one of the quantified variables;
or, if a quantified variable is to be bound to an aggregate value, an Aggregation elements that represents the quantified variable and that specifies how the aggregate value is computed;
one required formula sub-element that represents the formula in the scope of the quantifier. What is allowed as the content of the formula sub-element may depend on the quantifier: RIF-PRD allows only a CONDITION as the formula in the scope of an Exists, and a RULE as the formula in the scope of a Forall.
In the following, the Aggregation construct, that is used by all the constructs of the QUANTIFICATION class, is specified, before the concrete constructs of the class themselves.
XML syntax. As an abstract class, QUANTIFICATION is not associated with specific XML markup in RIF-PRD instance documents. It is specified in the normative schema as a substitution group.
*** ...Substitution group or another construct, depending on how we handle extensibility in the XML schema. ***
*** Difference wrt RIF-BLD: QUANTIFICATION could be omitted from the schema, if it does not seem useful as an extension point. In that case, the specification of that class in PRD would not add any concrete syntactic difference with BLD. If, on the other hand, the abstract construct is considered useful, the proposal would to include it in BLD's schema as well (not necessarily requiring that the text be changed, though. ***
[ Exists | Forall ]
Presentation syntax.
QUANTIFICATION ::= [ Exists | Forall ]
Aggregation
The Aggregation construct is used to represent a variable that is to be bound to an aggregate value, and to specify how that aggregate value is to be computed. In RIF-PRD, it is associated with the quantification of a variable.
XML syntax. An Aggregation element contains four required sub-elements:
the binds sub-element contains a Var element that represents the variable to be bound to the aggregate value;
the aggregates sub-element contains a Var elements that represents the variable that is the target of the aggregation;
the aggregationMode sub-element contains an element from the AGGREGATIONMODE class of constructs, that represents the aggregation function to be applied to the collection of values to be aggregated;
*** What are the allowed AGGREGATIONMODEs? An enumeration of QNames, each identifying an aggregation mode, e.g. "collect", "sum", whatever; an ExtTerm, thus allowing arbitrary aggregation functions; both? In extensions, probably both; in RIF-PRD, only a (very) limited enumeration? ***
the pattern sub-element contains an element from the CONDITION class of constructs, that represents a condition on the binding values of the target variable for being taken into account in the aggregation.
*** The pattern sub-element has to be required in RIF-PRD, since the dialect does not allow the direct typing of variables... ***
<Aggregation> <binds> Var </binds> <aggregationMode> AGGREGATIONMODE </aggregationMode> <aggregates> Var </aggregates> <pattern> CONDITION </pattern> </Aggregation>
*** Difference wrt RIF-BLD: that construct is specific to RIF-PRD. ***
Presentation syntax. The first Var represents the variable to be bound; that is, the content of the binds sub-element of the Aggregation element. The second Var represents the target of the aggregation; that is, the content of the aggregates sub-element of the Aggregation element.
Aggregation ::= Var ' : ' AGGREGATIONMODE Var ' SUCH THAT ( ' CONDITION ' ) '
Informal semantics. The Aggregation construct is used to indicated that the variable that is represented by the binds Var is to be bound to a single value that aggregates all the accepted binding values of a target variable, represented by the aggregates Var, that verify the condition represented by the pattern CONDITION, subject to the bindings of any other variables that are referenced in the condition.
The aggregationMode sub-element is used to indicate how the binding values of the target variable that satisfy the condition are to be aggregated.
This version of RIF-PRD covers a single aggregation mode: collect, where the binding values of the target variable that satisfy the condition pattern are simply collected, and the collection bound as a single value to the variable represented by the binds Var.
*** Or do we want a more open class of aggregation modes? ***
Exists
A QUANTIFICATION can represent an existentially quantified formula: this is represented by the Exists construct.
RIF-PRD covers existentially quantified formulae of the CONDITION class only.
XML syntax. The Exists element contains:
one or more declare elements, each containing either:
a Var element that represent one of the existentially quantified variable;
or, if an existentially quantified variable is to be bound to an aggregate value, an Aggregation elements that represents the quantified variable and that specifies how the aggregate value is computed;
exactly one formula element that contains an element of the CONDITION group that represents the formula in the scope of the quantifier.
<Exists> <declare> [ Var | Aggregation ] </declare>+ <formula> CONDITION </formula> </Exists>
*** Difference wrt RIF-BLD: the choice between a Var and and Aggregation for the content of a declare is specific to RIF-PRD. ***
Presentation syntax.
Exists ::= ' EXISTS ' [ Var | Aggregation ]+ ' ( ' CONDITION ' ) '
Informal semantics. The Exists construct is used to represent statements that are true iff there is at least one combination of bindings of the variables represented in the Exists's declare sub-elements, that makes the statement represented by the CONDITION formula true.
Forall
A QUANTIFICATION can represent an universally quantified formula: this is represented by the Forall construct.
RIF-PRD covers universally quantified formulae of the RULE class only.
In addition to being a QUANTIFICATION, Forall is also a concrete construct of the RULE class. It is further specified under that class, in section [ Rule].
Operational semantics
Data sources
The operational semantics of the RIF-PRD condition language rests on the notion of a data source (or, more generally, of data sources) against which CONDITIONs are matched.
For the purpose of specifying the operational semantics of RIF-PRD, the data sources are considered collectively to be a collection of ground ATOMICs named WM, where a ground ATOMIC, also called a fact, is an ATOMIC in which all the TERM are Consts. The WM is assumed to represent explicitely, in the form of ground ATOMICs, all the relevant information and knowledge that is available to the consumer of a RIF-PRD instance document, including, in particular, ground equality, membership and subclass relations, as well as the specification of all evaluated functions and predicates.
*** Must be more specific about the semantics of Equal, Member and Subclass, e.g. that Equal is a relation of equivalence, Subclass a pre-order etc. But also wrt what MUST be equal, e.g. litterals that map to the same value in the value space, objects that have the same address etc (or require that a specific equality predicate be define ofr each different equality relation); ditto wrt Member, Subclass. ***
More specifically, the WM is assumed to contain, for each tuple of constant arguments in an evaluated function's domain, an Equal ATOMIC where one of the side sub-elements contains the ground ExtTerm that represent the application of that function to that tuple of arguments, and the other side sub-element contains the Const that represents its value.
As regards the specification of evaluated predicates, the WM is assumed to contain a special Not element, defined, for the purpose of specifying the operational semantics of the RIF-PRD condition language only, to contain zero or more ground ATOMIC ExtTerm sub-elements. Furthermore:
the WM is assumed to contain, for each tuple of ground arguments in an evaluated predicate's domain that makes it true, the ground ATOMIC ExtTerm representing that evaluated predicate with these argument values; and
the Not element in the WM is assumed to contain, for each tuple of ground arguments in an evaluated predicate's domain that makes it false, a ground ATOMIC ExtTerm sub-element representing that evaluated predicate with these argument values.
Furthermore, the WM is assumed to contain only basic Frames.
*** How do we reference data sources? At what level: ATOMIC? CONDITION/ACTION? RULE? RuleSet? RIF instance document? ***
Implementors are responsible for making sure that the RIF-PRD translation of condition statements preserves their native semantics, according to the operational semantics for RIF-PRD CONDITIONs that is specified below, and subject to a consistent translation of the specified data sources.
Conformant implementations MUST translate CONDITIONs retrieved from RIF-PRD in such a way that their native evaluation against the specified data sources preserves their semantics, according to the operational semantics for RIF-PRD CONDITIONs that is specified below, and subject to a consistent translation of the specified data sources.
The following sections specify the normative operational semantics of each construct separately, grouped by abstract syntactic classes.
TERM
The operational semantics of TERMs specifies how arbitrary TERMs match Consts.
The sections below specifies the operational semantics of the constructs of the TERM class, where they have one.
Const
A Const matches itself and any other Const to which it is equal, where two Const c_1 and c_2 are equal if there is a ground Equal ATOMIC in the WM such that c_1 mactches the Const content of one of the side sub-elements and c_2 matches the Const content of the other side sub-element.
Var
A binding associates a Var to a Const. A bound Var matches any Const that the Const to which it is bound matches.
An unbound Var does not have an operational semantics in RIF-PRD.
*** What happens when a Var "does not have an operational semantics in RIF-PRD"? ***
*** Binding Vars to Vars? (AdrianP) ***
ExtTerm
The semantics of an ExtTerm TERM is determined by the specification of the evaluated function that is identified by a Const that the TERM in the op sub-element matches.
Therefore, an ExtTerm TERM t matches any Const that matches the Const contained in one side sub-element of an Equal ATOMIC where the other side sub-element contains a ground ExtTerm t_g such that:
the TERM content of the op sub-element of t matches any Const that matches the Const content of the op sub-element of t_g;
and the TERM content of each of the arg sub-elements of t matches any Const that matches the Const content of the same position arg sub-element of t_g.
An ExtTerm TERM does not have an operational semantics in RIF-PRD if:
the TERM content of one of its sub-elements does not have an operational semantics in RIF-PRD;
or it does not match any Const according to the above definition.
*** The implication being that, either the op does not match any known evaluated predicate, or one of the arguments if out of the predicate's domain ***
*** What happens when a TERM "does not have an operational semantics in RIF-PRD"? ***
ATOMIC
The operational semantics of ATOMICs specifies the truth value of arbitrary ATOMIC with respect to the WM by specifying how arbitrary ATOMICs match ground ATOMICs: an arbitrary ATOMIC is true iff it matches a ground ATOMIC from the WM.
The sections below specifies the operational semantics of the constructs of the ATOMIC class, where they have one.
Uniterm
An Uniterm matches any ground Uniterm such that:
the TERM content of the op sub-element of the matching Uniterm matches any Const that matches the Const content of the op sub-element of the ground Uniterm; and
the TERM content of each of the arg sub-elements of the matching Uniterm matches any Const that matches the Const content of the arg sub-element with the same position in the ordered list of the ground Uniterm's arg sub-elements.
An Uniterm does not have an operational semantics in RIF-PRD if the TERM content of one of its sub-elements does not have an operational semantics in RIF-PRD.
*** What happens when an Uniterm "does not have an operational semantics in RIF-PRD"? ***
An Uniterm is true iff it matches a ground Uniterm from the WM.
ExtTerm
The semantics of an ExtTerm ATOMIC is determined by the specification of the evaluated predicate that is identified by a Const that the TERM in the op sub-element matches.
Therefore, an ATOMIC Exterm matches any ground ATOMIC Exterm such that:
the TERM content of the op sub-element of the matching ExtTerm matches any Const that matches the Const content of the op sub-element of the ground ExtTerm; and
the TERM content of each of the arg sub-elements of the matching ExtTerm matches any Const that matches the Const content of the arg sub-element with the same position in the ordered list of the ground ExtTerm's arg sub-elements.
An ATOMIC ExtTerm does not have an operational semantics in RIF-PRD if:
the TERM content of one of its sub-elements does not have an operational semantics in RIF-PRD;
or it does not match any ground ATOMIC ExtTerm in the WM nor any ground ATOMIC ExtTerm sub-element of the Not element in the WM.
*** The implication being that, either the op does not match any known evaluated function, or one of the arguments if out of the function's domain ***
*** What happens when an ExtTerm "does not have an operational semantics in RIF-PRD"? ***
An ExtTerm is true iff it matches a ground ExtTerm from the WM.
Equal
An Equal matches any ground Equal such that the TERM content of one of the matching Equal's side sub-elements matches any Const that matches the Const content of one of the ground Equal's side sub-elements and the TERM content of the other matching Equal's side sub-element matches any Const that matches the Const content of the other ground Equal's side sub-element.
An Equal does not have an operational semantics in RIF-PRD if the TERM content of one of its sub-elements does not have an operational semantics in RIF-PRD.
*** What happens when an Equal "does not have an operational semantics in RIF-PRD"? ***
An Equal is true iff it matches a ground Equal from the WM.
Member
A Member matches any ground Member such that the TERM content of the matching Member's object sub-element matches any Const that matches the Const content of the ground Member's object sub-element and the TERM content of the matching Member's class sub-element matches any Const that matches the Const content of the ground Member's class sub-element.
A Member does not have an operational semantics in RIF-PRD if the TERM content of one of its sub-elements does not have an operational semantics in RIF-PRD.
*** What happens when an Member "does not have an operational semantics in RIF-PRD"? ***
A Member is true iff it matches a ground Member from the WM.
Subclass
A Subclass matches any ground Subclass such that the TERM content of the matching Subclass's subClass sub-element matches any Const that matches the Const content of the ground Subclass's subClass sub-element and the TERM content of the matching Subclass's class sub-element matches any Const that matches the Const content of the ground Subclass's class sub-element.
An Subclass does not have an operational semantics in RIF-PRD if the TERM content of one of its sub-elements does not have an operational semantics in RIF-PRD.
*** What happens when an Subclass "does not have an operational semantics in RIF-PRD"? ***
A Subclass is true iff it matches a ground Subclass from the WM.
Frame
A basic Frame matches any ground basic Frame such that the TERM contents of the matching Frame's object, slotKey and slotValue sub-elements match any Const that match the Const contents of, respectively, the ground Frame's object, slotKey and slotValue sub-elements.
A basic Frame does not have an operational semantics in RIF-PRD if the TERM content of one of its sub-elements does not have an operational semantics in RIF-PRD.
A basic Frame is true iff it matches a ground Frame from the WM.
Unnesting frames. The semantics of a nested or combined Frame is specified recusively, based on the semantics of its components:
A Frame with multiple slotKey-slotValue pairs is true iff all the Frames formed with the same object sub-element and each of the slotKey-slotValue pairs are true.
A Frame where the object element contains a Member element is true iff the Member element is true and the Frame element with the content of the object element replaced with the content of the Member's object sub-element is true.
A Frame where the object element contains a Subclass element is true iff the Subclass element is true and the Frame element with the content of the object element replaced with the content of the Subclass's subClass sub-element is true.
A Frame where a slotValue sub-element contains a Frame is true iff the Frame in the slotValue element is true and the enclosing Frame is true with the content of the slotValue sub-element replaced by:
the content of the object sub-element of the enclosed Frame, if it is a TERM;
the content of the Member's object sub-element, if the object sub-element of the enclosed Frame contains a Member element;
the content of the Subclass's subClass sub-element, if the object sub-element of the enclosed Frame contains a Subclass element;
A nested Frame does not have an operational semantics in RIF-PRD if one of its component ATOMICs does not have an operational semantics in RIF-PRD.
*** What happens when a Frame "does not have an operational semantics in RIF-PRD"? ***
CONDITION
The operational semantics of CONDITIONs specifies the truth value of arbitrary CONDITIONs, based on the truth values of its component ATOMICs.
A CONDITION does not have an operational semantics in RIF-PRD if one of its component ATOMICs does not have an operational semantics in RIF-PRD.
*** What happens when a CONDITION "does not have an operational semantics in RIF-PRD"? ***
The sections below specifies the operational semantics of the constructs of the CONDITION class, where they have one.
ATOMIC
An ATOMIC CONDITION is true iff it matches a ground ATOMIC from the WM.
And
An And CONDITION is true iff it has no formula sub-element or all the CONDITIONs in its formula sub-elements are true.
Unnesting frames. A nested Frame element can always be replaced by an And element where the conjoined formulas are the basic Frame and, possibly, Member elements obtained when unnesting it. Reciprocally, conjuncts formulas in an And element can be combined into a nested or combined Frame element as follows:
Iff the content of the object sub-element of a Frame element is a TERM and it is syntactically identical to the TERM content of the object sub-element of a Member element, the Member and Frame elements can be replaced by a single combined Frame element where the content of the object sub-element of the Frame has been replaced by the Member element;
Iff the content of the object sub-element of a Frame element is a TERM and it is syntactically identical to the TERM content of the subClass sub-element of a Subclass element, the Subclass and Frame elements can be replaced by a single combined Frame element where the content of the object sub-element of the Frame has been replaced by the Subclass element;
Iff the content of a slotValue sub-element of a Frame is a TERM that is syntactically identical to the TERM content of the object sub-element of another Frame, the two Frame elements can be replaced by a single nested element where the latter Frame replaces the content of the slotValue sub-element in the former Frame;
Iff the content of a slotValue sub-element of a Frame is a TERM that is syntactically identical to the TERM content of the object sub-element of the Member element that is the content of the object sub-element of another Frame, the two Frame elements can be replaced by a single nested element where the latter Frame replaces the content of the slotValue sub-element in the former Frame;
Iff the content of a slotValue sub-element of a Frame is a TERM that is syntactically identical to the TERM content of the subClass sub-element of the Subclass element that is the content of the object sub-element of another Frame, the two Frame elements can be replaced by a single nested element where the latter Frame replaces the content of the slotValue sub-element in the former Frame;
Two Frame elements can be replaced by a single Frame that combines their slotKey-slotValue pairs of sub-elements iff:
the object sub-elements of Frames are syntactically identical:
the object sub-element of one of the original Frames contains a TERM and the object sub-element of the other one contains a Member element and the content of the object sub-element of that Member is syntactically identical to that TERM. In that case, the Member element becomes the content of the object sub-element of the resulting combined Frame;
the object sub-element of one of the original Frames contains a TERM and the object sub-element of the other one contains a Subclass element and the content of the subClass sub-element of that Subclass is syntactically identical to that TERM. In that case, the Subclass element becomes the content of the object sub-element of the resulting combined Frame.
Or
An Or CONDITION is true iff it has at least one formula sub-element and the CONDITION in at least one of its formula sub-elements is true.
Naf
A Naf CONDITION is true iff the CONDITION in its formula sub-element is not true, but does have an operational semantics in RIF-PRD.
Exists
An Exists CONDITION is true iff it has at least one instance and at least one of its instances is true.
The notions of instance is specific to the constructs of the QUANTIFICATION class, to which the Exists element belongs as well. It is further specified under that class, below.
QUANTIFICATION
The operational semantics of QUANTIFICATIONs specifies the notion of instance of a formula, based on the notions of the accepted bindings of a Var and of a combination of bindings of a set of Vars, and on the operational semantics of the Aggregation construct.
Var binding. As already defined earlier, a binding of a Var is the association of that Var and a Const. Only bound Vars have an operational semantics in RIF-PRD and, as a consequence, any construct that contains a Var has an operational semantics only when that Var is bound.
In the following, a Var is said to be declared by a QUANTIFICATION if it is either:
the content of a declare sub-element of that QUANTIFICATION; or
the content of the binds sub-element of an Aggregation element that is the content of a declare sub-element of the QUANTIFICATION.
A Var is declared by an Aggregation if it is the content of the aggregates sub-element of that Aggregation.
Vars are declared for the purpose of binding: all the sub-elements of the construct where it is declared, and only those elements, are in the scope of a Var's binding.
Candidate and accepted bindings. Any Const that can be found in the WM is a candidate binding for any Var.
Constructs that declare Vars may allow the representation of additional conditions on the bindings of the declared Vars. The candidate bindings for a Var that satisfy these additional conditions are called, for the purpose of this specification: accepted bindings. In the absence of such additional conditions, any candidate binding for a Var is also an accepted binding for that Var.
In this version of RIF-PRD, the constructs that allow the representation of such additional conditions on the bindings of a Var that they declare are, exclusively:
the Forall QUANTIFICATION, that will be further specified in the [ Rule section];
and the Aggregation construct, where an additional condition on the bindings of the Var that is declared by the Aggregation (that is, the Var content of the Aggregation's aggregates sub-element) is represented by the CONDITION content of the Aggregation's pattern sub-element.
The accepted bindings for the Var that is declared by an Aggregation are those possible bindings of the Var that make true the CONDITION content of the Aggregation's pattern sub-element, subject to the bindings of any other Var in that CONDITION that are declared by an enclosing construct, if any.
The accepted bindings for a Var that is declared by an Exists are, therefore, all the candidate bindings for those Vars.
*** The latter sentence is not meant to imply that implementations must actually consider or have the capability to bind any variable to any constant in the specified data source(s); but rather that it must not consider bindings to constants that are not in the data sources (and thus not matchable), provided, of course, that it considers at least all the bindings that would satisfy the formula (thus not missing any successful match). Should that be made explicit in the text? ***
A Var that is declared by a QUANTIFICATION as the content of the binds sub-element of an Aggregation element that is contained in the declare sub-element of a QUANTIFICATION has one single candidate binding, called an aggregate binding, that is the single value computed by the aggregation function that is specified by the content of the Aggregation's aggregationMode sub-element, applied to the set of the accepted bindings of the Var content of the Aggregation's aggregates sub-element.
*** A candidate aggregate binding is computed by aggregation of the accepted bindings of the aggregation's target variable. That candidate aggregate binding is an accepted aggregate binding iff it makes any additional conditions true, that may be set by the QUANTIFICATION that declares the aggregate Var. Is that clear or should it be made explict? ***
Combination of bindings. A combination of bindings for a set of Vars is an element of the cartesian product of the sets of the bindings considered for each Var in the set.
*** For the determination of the set of Vars to be bound, two syntactically identical Var are the same Var, even if they are contained in two different declares. Should that be made explicit in the text? ***
A combination of accepted bindings for a set of Vars is a combination of bindings taken from the combinations of all the accepted bindings for each of the Vars in the set.
*** So, a combination of accepted bindings contains one and only one binding for each of the Var in the considered set; and the set of the combinations of accepted bindings is empty if one of the Vars does not have any accepted binding. Is that obvious, or should it be made explicit? ***
Instances of a formula. An instance of a QUANTIFICATION Q is defined recursively as the association to an instance of the formula that is contained in the formula sub-element of Q, for the purpose of truth valuation, of a combination of accepted bindings for the set of the Vars that are declared by Q, possibly appended to the combination of bindings that is associated to Q, if Q is within the scope of some Vars binding (e.g. if it is itself the formula contained in the formula sub-element of an enclosing QUANTIFICATION being instantiated).
An instance of a formula that is not a QUANTIFICATION is the formula itself.
A QUANTIFICATION does not have any instance is one of the Vars that it declares does not have any accepted binding, or if the formula contained in its formula sub-element does not have any instance.
Two instances are said to be equal iff their formula are syntactically identical, and the associated combinations of bindings contain bindings for the same set of Vars, and the Const to which any Var is bound in one instance matches the Const to which it is bound in the other instance.
An instance of a formula does not have an operational semantics in RIF-PRD if the combination of accepted bindings contains more than one binding for the same Var.
*** Or is there another way we should deal with that case when a Var is redeclared by a construct that is within the scope of another construct that already declared that Var? ***