In this section we extend Positive Conditions, defined in Section Positive Conditions, with slotted Uniterms and Frame formulas. A slot can be represented by an individual symbol or, more generally, by a Uniterm. It can be represented by an IRI or be known only locally. Semantically, a frame slot is a set-valued binary function that represents a property of an object. Such a function maps an object id to a value (or a set of values) of the property. In contrast, a uniterm slot semantically behaves like a unary function symbol. In both cases, however, the order of the slots is immaterial (in contrast to positional uniterms).
Syntactically, the extension is achieved by enriching the notion of a uniterm with slots and by complementing these with frame formulas. For uniformity and greater syntactic convenience, frame formulas can be nested inside other frame formulas. This is syntactic sugar, however, as explained later in this section.
Syntax
Abstract Syntax
The abstract syntax of the slotted condition language is given in asn06 as follows:
class CONDITION
subclass And
property formula : list of CONDITION
subclass Or
property formula : list of CONDITION
subclass Exists
property declare : list of Var
property formula : CONDITION
subclass ATOMIC
class ATOMIC
subclass Equal
property side: list TERM TERM
subclass Uniterm
subclass CLASSIFICATION
subclass Frame
class TERM
subclass Var
property name: xsd:string
subclass Const
property name: xsd:string
subclass Uniterm
property op: Const
property
subproperty arg: list of TERM
subproperty slot: list of list Const TERM
class CLASSIFICATION
subclass Instance
property oid: TERM
property op: TERM
subclass Subclass
property sub: TERM
property op: TERM
class Frame
property
subproperty oid: TERM
subproperty classinst: CLASSIFICATION
property slot: list of list TERM TERMFRAME
class TERMFRAME
subclass TERM
subclass Frame
The above asn06 is generalized with a fixed-arity list constructor (complementing the unfixed-arity list of constructor) so that the multiplicity of the side property (role) of the Equal class no longer requires the assumption of being exactly 2 (the 2 TERMs are just listed). This also allows the name and filler of a slot to be defined as a sequence of two classes. Since no set of constructor is available, list of is used to represent a set of slots, assuming that duplicates and order will not matter. Also, optional of and subproperty constructs are assumed.
The abstract syntax is visualized by a UML diagram used as a schema-level device for specifying syntactic classes with generalizations as well as multiplicity- and role-labeled associations. (***TBD***)
Upload new attachment "SlottedConditionModel.png"
The syntactic classes are partitioned into classes that will not be visible in serializations (written in all-uppercase letters) and classes that will be visible in instance markup (written with a leading uppercase letter only).
The three classes Var, CONDITION, and ATOMIC will be required in the abstract syntax of Horn Rules.
Concrete Syntax
The abstract syntax of Section Abstract Syntax can be instantiated to a concrete syntax which is an extension to the concrete syntax of Positive Conditions for slotted Uniterms. The EBNF syntax below, which instantiates the abstract syntax, is used throughout this document to explain and illustrate the main ideas.
The concrete human-readable syntax, described in this (slightly modified) EBNF, is work in progress and under discussion.
CONDITION ::= CONJUNCTION | DISJUNCTION | EXISTENTIAL | ATOMIC
CONJUNCTION ::= 'And' '(' CONDITION* ')'
DISJUNCTION ::= 'Or' '(' CONDITION* ')'
EXISTENTIAL ::= 'Exists' Var+ '(' CONDITION ')'
ATOMIC ::= Uniterm | Equal | CLASSIFICATION | Frame
Uniterm ::= Const '(' TERM* ')' | Const '(' (Const '->' TERM)* ')'
CLASSIFICATION ::= TERM '#' TERM | TERM '##' TERM
Frame ::= (TERM | CLASSIFICATION) '[' (TERM '->' (TERM | Frame))* ']'
Equal ::= TERM '=' TERM
TERM ::= Const | Var | Uniterm
Const ::= CONSTNAME | '"'CONSTNAME'"''^^'SORTNAME
Var ::= '?'VARNAME | '?'VARNAME'^^'SORTNAME
A Uniterm ()-applies a Const to positional TERM arguments or to slotted Const -> TERM arguments. A CLASSIFICATION #-associates a TERM with a typing class TERM, or ##-associates a TERM with a superclass TERM. A Frame []-applies a TERM or a CLASSIFICATION to slotted TERM -> (TERM | Frame) arguments.
Example 1 shows Uniterm and Frame conditions, the latter with variables for the three major (combinations of) syntactic categories, corresponding to the three components of RDF triples.
Example 1 (A RIF condition with bound variables)
RIF conditions using
Positional Uniterms:
book(rifwg LeRif)
Exists ?X (book(?X LeRif))
Slotted Uniterms:
book(author->rifwg title->LeRif)
Exists ?X (book(author->?X title->LeRif))
Frames:
wd1[author->rifwg title->LeRif]
Exists ?X (wd1[author->?X title->LeRif])
Exists ?X (wd1#book[author->?X title->LeRif])
Exists ?I ?X (?I[author->?X title->LeRif])
Exists ?I ?X (?I#book[author->?X title->LeRif])
Exists ?S (wd1[author->rifwg ?S->LeRif])
Exists ?X ?S (wd1[author->?X ?S->LeRif])
Exists ?I ?X ?S (?I#book[author->?X ?S->LeRif])
The following is a possible XML-serializing mapping of the abstract syntax in Section Abstract Syntax (and of the above EBNF syntax).
- And (conjunction) - Or (disjunction) - Exists (quantified formula for 'Exists', containing declare and formula roles) - declare (declare role, containing a Var) - formula (formula role, containing a CONDITION formula) - Uniterm (positional or slotted Uniterm formula) - Instance (instance-of formula) - Subclass (subclass-of formula) - Frame (slotted Frame formula) - classinst (Frame role for Subclass or Instance) - oid (Instance/Frame identifier role, containing a TERM) - op (Uniterm/Instance/Subclass predicate/class role) - sub (Subclass role for included class) - slot (Uniterm/Frame slot role, prefix version of slot infix '->') - Equal (prefix version of term equation '=') - Const (slot, individual, function, or predicate symbol) - Var (logic variable)
The following example illustrates XML serialization of Slotted RIF conditions.
Example 2 (A RIF condition and its XML serialization):
a. RIF condition:
And ( Exists ?Buyer ?P (?P#purchase[buyer->?Buyer
seller->?Seller
item->book{author->?Author title->LeRif}
price->$49])
?Seller=?Author )
b. XML serialization:
<And>
<formula>
<Exists>
<declare><Var>Buyer</Var></declare>
<declare><Var>P</Var></declare>
<formula>
<Frame>
<classinst>
<Instance>
<oid><Var>P</Const></Var>
<op><Const>purchase</Const></op>
</Instance>
</classinst>
<slot><Const>buyer</Const><Var>Buyer</Var></slot>
<slot><Const>seller</Const><Var>Seller</Var></slot>
<slot>
<Const>item</Const>
<Uniterm>
<op><Const>book</Const></op>
<slot><Const>author</Const><Var>Author</Var></slot>
<slot><Const>title</Const><Const>LeRif</Const></slot>
</Uniterm>
</slot>
<slot><Const>price</Const><Const>$49</Const></slot>
</Frame>
</formula>
</Exists>
</formula>
<formula>
<Equal>
<side><Var>Seller</Var></side>
<side><Var>Author</Var></side>
</Equal>
</formula>
</And>
Semantics
The syntax of RIF frames permits nesting of two kinds. First, a classification formula of the form obj1#obj2 or obj1##obj2 can appear in the object position of a frame. Second, a frame may appear in the value position of an attribute. This nested notation is convenient and allows succinct representation of object properties, but is no more than a shorthand notation. A nested frame represents a conjunction of flat frames. For instance,
a#b[c -> e##f[g -> h]] == a#b /\ a[c -> e] /\ e##f /\ e[g -> h]
Formally, we define the Unnest transformation and postulate that for any frame, f, it is true in a semantic structure iff Unnest(f) is true. In this way, we reduce the semantics of nested frames to that of flat frames. Then we extend the semantic structures defined in Semantics of the Multisorted RIF Conditions and define an interpretation for flat frames. The rest of the semantic definitions does not change, since it is defined in terms of atomic formulas (the ATOMIC production in the BNF syntax).
The Unnest Transformation
If a formula, f, has the form a#b or a##b then define Obj(f) to be a. If f has the form o[a->v], where o, a, and v are terms, then Obj(f) is defined to be Obj(o). Now, if f is a uniterm then we define Unnest(f) = true, where true is a formula that is always true (a tautology, a formula whose truth value is t). If f is a classification formula then Unnest(f) = f. Otherwise, if f is a frame of the form o[a->v] then
Unnest(f) = Unnest(o) /\ Obj(o)[a -> Obj(v)] /\ Unnest(v)
For instance, in case of the frame a#b[c->e##f[g->]] above, unnesting yields:
Unnest(a#b[c -> e##f[g -> h]]) = a#b /\ a[c -> e] /\ e##f /\ e[g -> h] /\ true
This is almost the same conjunction as we have seen earlier. The only difference is the trailing true, which comes from Unnest(h) and can be omitted.
Extension of Semantic Structures for Frames
A semantic structure, I, is now a tuple of the form
<D,IC, IV, IF, IR, Islot, ISR, Isub, Iisa>.
All the components except the last four, Islot, ISR, Isub, Iisa, are the same as before. The new mapping Islot is used to interpret frames; the mapping ISR interprets predicates with named arguments; Isub i gives meaning to the subclass hierarchy; and Iisa interprets class membership.
Islot is a function form D to truth-valued functions of the form D × D → TV. The intuitive meaning of frame slots is that they are functions that take objects and return sets of objects, where every member of the set has certain degree of truth. In the two-valued case, a set of objects associated with the truth value true represents the (set of) values that the slot returns when applied to an object. Formally, this is expressed by extending ITruth to flat frames as follows:
ITruth(T[slot1->V1 ... slotk->Vk]) = mini=1...k(ITruth(T[sloti->Vi])), where T, sloti, and Vi are terms.
ITruth(T[sloti->Vi]) = Islot(I(sloti))(I(T),I(V))
ISR is used to interpret predicates with slotted arguments. It is a function from Const to truth-valued mappings SetOfFiniteSubbags(D × D) → TV. This is analogous to the interpretation of regular (positional) predicates except for two differences:
-- Each pair <s,v> ∈ D × D represents a slot-value pair instead of just a value in positional predicates. -- A tuple in a slotted predicate is a finite bag of slot-value pairs rather than an ordered sequence.
Bags are used here because for slotted predicates the order of slot-value pairs does not matter, but sets cannot be used, since I may happen to map different slots into the same value in D.
We can now define ITruth for slotted predicates as follows:
ITruth(p(slot1->val1 ... slotk->valk)) = ISR(p)(<I(slot1) I(val1)>, ... , <I(slotk) I(valk)>), where p ∈ Const, and sloti and vali are terms.
Isub gives meaning to the subclass relationship. It is a truth-valued function D × D → TV. For the two valued case, Isub is required to define a partial order on D. More precisely, the set of all pairs <a,b> such that I(<a,b>) = t is required to be a partial order on D. When TV is multivalued, the restriction on Isub will depend on the corresponding multivalued logic. The truth valuation for classification formulas of the form sc##cl, where sc and cl are terms, is defined as follows:
ITruth(sc##cl) = Isub(I(sc), I(cl))
Iisa gives meaning to class membership. It is a truth-valued function D × D → TV. The truth valuation for classification formulas of the form o#cl, where o and cl are terms, is defined as follows:
ITruth(o#cl) = Iisa(I(o), I(cl))
MK: ***** The effect of sorts on all this stuff is to be filled in at a later time ********