Core/Slotted Conditions - W3C RIF-WG Wiki

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 function that represents a property of an object. Such a function maps an object id to a set of values of the property. This can be a singleton set or even an empty set. In contrast, a uniterm slot semantically behaves like a unary uninterpreted function symbol. In both cases, however, the order of the slots is immaterial (in contrast to positional uniterms).

Syntactically, the extension is achieved by extending the notion of a uniterm with slots and by adding a new kind of formula, called frame formula. For uniformity and greater syntactic convenience, frame formulas can be nested inside other frame formulas. However, this feature is just a syntactic sugar that does not extend the expressive power.

Syntax

Slotted Terms and Frames

The alphabet of the language is extended with symbols ->, #, and ##, and the language of positive conditions in Section Symbols and Signatures is extended with slotted terms, slotted predicates, and frames.

Slotted terms. A term is either a term in the sense of Section Symbols and Signatures or a slotted term.

A slotted term is of the form t ( p₁ -> v₁ ... p_n -> v_n ), where t is a term; p₁, ..., p_n are terms, which represent the names of the slots; and v₁ , ..., v_n are terms. Slotted terms are like regular terms except that the arguments are named and their order is considered to be immaterial.

In order to talk about the slotted terms that are also well-formed, we need to extend the notion of a signature to include slots. As before, a slotted signature is a statement of the form η{e₁, ..., e_n, ...} where η ∈ SigNames is the name of the signature and {e₁, ..., e_n, ...} is a countable set of slotted arrow expressions. A slotted arrow expression is a statement of the form

(γ₁ -> κ₁, ..., γ_n -> κ_n) => κ, where n≥0. The order of the arguments in a slotted arrow expression is assumed to be immaterial, so any permutation of arguments is assumed to yield the same expression. For instance, (term -> term, term -> term) => term is a slotted arrow signature expression. By analogy with earlier definitions, if κ is atomic then the expression is also a slotted Boolean expression. For instance, (term -> term, term -> term) => atomic is a slotted Boolean signature expression.

A term t ( p₁ -> v₁ ... p_n -> v_n ) is a well-formed slotted term with signature σ if

Each p_i is a well-formed term with some signature γ_i.
Each v_i is a well-formed term (slotted or non-slotted) with some signature σ_i, i=1, ..., n.
The signature of t includes a slotted arrow expression of the form (γ₁ -> σ₁ ... γ_n -> σ_n) => σ.
The aforesaid term t is a well-formed slotted atomic formula if σ is atomic.
A slotted atomic formula is just like an atomic formula of Section Symbols and Signatures except that the arguments of the predicate are named and their order is considered immaterial. This is analogous to names of columns in tables in relational databases.

Editor's Note: The use of slotted terms is an open issue in the current draft http://www.w3.org/2005/rules/wg/track/issues/44.

Frames. A well-formed frame formula is one of the following:

Membership formula: Depending on the dialect, the symbol # can have different signatures, but they can contain only the arrow expression of the form (κ₁ κ₂) ⇒ atomic. A membership formula o # c is well-formed and has the signature atomic, if o, c are well-formed terms that have the signatures κ₁ and κ₂, respectively.
Informally, such a formula says that object o is a member of class c. A RIF class is an object, which can have other classes as members, as specified by membership formulas. Thus, classes are also objects and they can be members of some other classes. (In object-oriented languages these latter classes are sometimes known as meta-classes.)
Subclass formula: Depending on the dialect, the symbol ## can have different signatures, but they can contain only the arrow expression of the form (κ κ) ⇒ atomic. A subclass formula s ## c is well-formed and has the signature atomic, if s and c are well-formed terms with signature κ.
Informally, this formula states that class s is a subclass of class c. Note that both arguments must have the same signature, since the subclass relationship is supposed to be transitive.
Frame: t [ p₁ -> v₁ ... p_n -> v_n ], where t is a well-formed term, a membership formula, or a subclass formula; p₁, ..., p_n are well-formed terms; and each v₁ , ..., v_n is either a well-formed term or a well-formed frame formula.
When t, all the p_i, and all the v_i are terms, such a formula should be understood as a statement that object t has properties p_i, ..., p_n, and for each i = 1,...,n, the value of property p_i is a set that contains the object v_i. When t, p_i, or v_i are not just terms but frame formulas themselves, the above is treated as a conjunction of simpler frame formulas, as defined by the unnest transformation in the section on semantics (below).

Editor's Note: The use of membership and subclass formulas is an open issue in the current draft http://www.w3.org/2005/rules/wg/track/issues/41.

Atomic formulas and general condition formulas. The syntax for atomic formulas is extended with slotted formulas and frame formulas. More precisely, an atomic well-formed formula is

An atomic well-formed formula as defined in Section Symbols and Signatures; or
A well-formed slotted atomic formula; or
A well-formed frame formula.

The notion of well-formed condition formulas needs no adjustments with respect to the earlier definition (without frames or slots). As before, such formulas are constructed from well-formed atomic formulas using the logical connectives And, Or, and the quantifier Exists.

Slotted signatures for RIF-BLD. Section Symbols and Signatures defined the allowed signatures for RIF-BLD. With the introduction of slotted signatures, we add the following signatures to those already defined for RIF-BLD:

For every n≥0 there are signatures fs_n{(term -> term, ..., term -> term) => term} and ps_n{(term -> term, ..., term -> term) => atomic} (in both cases the number of arguments inside the parentheses is n).

In addition, RIF-BLD imposes the following restrictions:

The terms that are allowed as slot names in slotted terms
- must have the signature term{ }; and
- they must be constant symbols.
This means that RIF-BLD does not allow variables or complex terms (like f(), f(a,b)) as slot names in slotted uniterms (but there are no such restrictions on slots in frames).
In frame formulas, all terms must have the signature term and #, ## must have the signature p₂{(term term)⇒atomic}.
Therefore, in the frame formulas t # s, t ## s, or t [ r -> s ], the terms t, s, and r cannot have the signature atomic -- they can represent individuals, but not predicates.

EBNF for the Presentation Syntax

We now extend the presentation syntax of Positive Conditions to a presentation syntax for slotted terms and frames.

EBNF grammar

  CONDITION      ::= 'And' ' ( ' CONDITION* ' ) ' |
                     'Or' ' ( ' CONDITION* ' ) ' |
                     'Exists' Var+ ' ( ' CONDITION ' ) ' |
                     ATOMIC
  ATOMIC         ::= Uniterm | Equal | CLASSIFICATION | Frame
  Uniterm        ::= Const ' ( ' (TERM* | (Const ' -> ' TERM)*) ' ) '
  Equal          ::= TERM '=' TERM
  CLASSIFICATION ::= TERM ' # ' TERM | TERM ' ## ' TERM
  Frame          ::= (TERM | CLASSIFICATION) ' [ ' (TERM ' -> ' (TERM | Frame))* ' ] '
  TERM           ::= Const | Var | Uniterm
  Const          ::= LITERAL '^^' SYMSPACE
  Var            ::= '?' VARNAME

A Uniterm applies a symbolic constant (from Const) to positional TERM arguments or to slotted Const -> TERM arguments. A CLASSIFICATION specifies that one object is a member (in case of the #-connective) or a subclass (in case of the ##-connective) of another object. A Frame is a TERM or a CLASSIFICATION applied to slotted TERM -> (TERM | Frame) arguments.

Example 3 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 3 (A RIF condition with bound variables)
   We use the prefix bks to abbreviate http://example.com/books#
   and the prefix auth for http://example.com/authors#.

RIF conditions using

   Positional Uniterms:
                        book^^rif:local ( auth:rifwg^^rif:iri bks:LeRif^^rif:iri )

                        Exists ?X ( book^^rif:local ( ?X LeRif^^rif:local ) )

   Slotted Uniterms:
                        book^^rif:local ( author^^rif:local -> auth:rifwg^^rif:iri
                                          title^^rif:local -> bks:LeRif^^rif:iri )

                        Exists ?X ( book^^rif:local ( author^^rif:local -> ?X
                                                      title^^rif:local -> bks:LeRif^^rif:iri ) )

   Frames:
                        wd1^^rif:local [ author^^rif:local -> auth:rifwg^^rif:iri
                                         title^^rif:local -> bks:LeRif^^rif:iri ]

                        Exists ?X ( wd2^^rif:local [ author^^rif:local -> ?X
                                                     title^^rif:local -> bks:LeRif^^rif:iri ] )

                        Exists ?X ( wd2^^rif:local # book^^rif:local [ author^^rif:local -> ?X
                                                                       title^^rif:local -> bks:LeRif^^rif:iri ] )

                        Exists ?I ?X ( ?I [ author^^rif:local -> ?X
                                            title^^rif:local -> bks:LeRif^^rif:iri ] )

                        Exists ?I ?X ( ?I # book^^rif:local [ author^^rif:local -> ?X
                                                              title^^rif:local -> bks:LeRif^^rif:iri ] )

                        Exists ?S ( wd2^^rif:local [ author^^rif:local -> auth:rifwg^^rif:iri
                                                     ?S -> bks:LeRif^^rif:iri ] )

                        Exists ?X ?S ( wd2^^rif:local [ author^^rif:local -> ?X
                                                        ?S -> bks:LeRif^^rif:iri ] )

                        Exists ?I ?X ?S ( ?I # book^^rif:local [ author -> ?X
                                                                 ?S -> bks:LeRif^^rif:iri ] )

XML Syntax

The following is an XML-serializing mapping of the presentation syntax in Section EBNF for the Presentation Syntax, extending the one in Section Positive Conditions.

Classes, roles and their intended meaning

- 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)
- Member    (member formula)
- Subclass  (subclass formula)
- Frame     (Frame formula)
- object    (Member/Frame role containing a TERM or an object description)
- op        (Uniterm function/predicate role)
- upper     (Member/Subclass upper class role)
- lower     (Member/Subclass lower instance/class role)
- slot      (Uniterm/Frame slot role, prefix version of slot infix ' -> ')
- Equal     (prefix version of term equation '=')
- side      (Equal left-hand and right-hand side role)
- Const     (slot, individual, function, or predicate symbol)
- Var       (logic variable)

For the XML Schema Definition (XSD) of the RIF-BLD slotted condition language see Appendix Specification.

The following example illustrates XML serialization of Slotted RIF conditions.

Example 4 (A RIF condition and its XML serialization):
   We use the prefix bks to abbreviate http://example.com/books#,
   the prefix auth for http://example.com/authors#, and
   curr for http://example.com/currencies#,

a. RIF condition:

  And ( Exists ?Buyer ?P ( ?P # purchase^^rif:local [
                                      buyer^^rif:local -> ?Buyer
                                      seller^^rif:local -> ?Seller
                                      item^^rif:local -> book^^rif:local ( author^^rif:local -> ?Author
                                                                           title^^rif:local -> bks:LeRif^^rif:iri )
                                      price^^rif:local -> 49^^xsd:integer
                                      currency^^rif:local -> curr:USD^^rif:iri ] )
        ?Seller=?Author )

b. XML serialization:

  <And>
    <formula>
      <Exists>
        <declare><Var>Buyer</Var></declare>
        <declare><Var>P</Var></declare>
        <formula>
          <Frame>
            <object>
              <Member>
                <lower><Var>P</Var></lower>
                <upper><Const type="rif:local">purchase</Const></upper>
              </Member>
            </object>
            <slot><Const type="rif:local">buyer</Const><Var>Buyer</Var></slot>
            <slot><Const type="rif:local">seller</Const><Var>Seller</Var></slot>
            <slot>
              <Const type="rif:local">item</Const>
              <Uniterm>
                <op><Const type="rif:local">book</Const></op>
                <slot><Const type="rif:local">author</Const><Var>Author</Var></slot>
                <slot><Const type="rif:local">title</Const><Const type="rif:iri">bks:LeRif</Const></slot>
              </Uniterm>
            </slot>
            <slot><Const type="rif:local">price</Const><Const type="xsd:integer">49</Const></slot>
            <slot><Const type="rif:local">currency</Const><Const type="rif:iri">curr:USD</Const></slot>
          </Frame>
        </formula>
      </Exists>
    </formula>
    <formula>
      <Equal>
        <side><Var>Seller</Var></side>
        <side><Var>Author</Var></side>
      </Equal>
    </formula>
  </And>

Translation Between the Presentation and the XML Syntaxes

The translation from the presentation syntax to the XML syntax is given by a table, below, which extends the translation table of Positive Conditions.

Presentation Syntax	XML Syntax
predfunc ( key₁ -> filler₁ . . . key_n -> filler_n )	<Uniterm> <op>predfunc</op> <slot>key₁ filler₁</slot> . . . <slot>key_n filler_n</slot> </Uniterm>
inst [ key₁ -> filler₁ . . . key_n -> filler_n ]	<Frame> <object>inst</object> <slot>key₁ filler₁</slot> . . . <slot>key_n filler_n</slot> </Frame>
inst # class [ key₁ -> filler₁ . . . key_n -> filler_n ]	<Frame> <object> <Member> <lower>inst</lower> <upper>class</upper> </Member> </object> <slot>key₁ filler₁</slot> . . . <slot>key_n filler_n</slot> </Frame>
sub ## super [ key₁ -> filler₁ . . . key_n -> filler_n ]	<Frame> <object> <Subclass> <lower>sub</lower> <upper>super</upper> </Subclass> </object> <slot>key₁ filler₁</slot> . . . <slot>key_n filler_n</slot> </Frame>
inst # class	<Member> <lower>inst</lower> <upper>class</upper> </Member>
sub ## super	<Subclass> <lower>sub</lower> <upper>super</upper> </Subclass>

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 a slot. 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 ] ]   =    And ( a # b  a [ c -> e ]  e ## f  e [ g -> h ] )

Formally, given a frame, f, we define the Unnest transformation and postulate f to be 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 basic semantic structures defined in Model Theory for the Core RIF Condition Language and define an interpretation for flat frames. The rest of the semantic definition 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). If f is a term then Obj(f) = f. Now, if f is a term then we define Unnest(f) = true, where true is a formula that is always true (a tautology). 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) = And(Unnest(o)  Obj(o) [ a -> Obj(v) ]  Unnest(v))

For instance, in case of the frame a # b [ c -> e ## f [ g -> h ] ] above, unnesting yields:

   Unnest(a # b [ c -> e ## f [ g -> h ] ])    =    And(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 conjunct, which comes from Unnest(h) and can be omitted.

Extension of Semantic Structures for Frames

A semantic structure, I, is a tuple of the form

<D,I_C, I_V, I_F, I_R, I_slot, I_SF, I_SR, I_sub, I_isa>.

All the components except the last five, I_slot, I_SF, I_SR, I_sub, I_isa, are the same as before. The new mapping I_slot is used to interpret frames; the mappings I_SF and I_SR interpret terms and predicates with named arguments, respectively; I_sub gives meaning to the subclass hierarchy; and I_isa interprets class membership.

I_slot is a total function from the domain D to total 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 a 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 I_Truth to flat frames as follows:
- I_Truth(T [ p₁ -> V₁ ... p_k -> V_k ]) = min_i=1...k(I_Truth(T [ p_i -> V_i ])), where T, p_i, and V_i are terms.
- I_Truth(T [ p -> V ]) = I_slot(I(p))(I(T),I(V))

I_SF interprets terms with named arguments. It is a total function from Const to the total mappings SetOfFiniteSubbags(D × D) → D. This is analogous to the interpretation of regular (positional) terms with two differences:
- Each argument <s,v> ∈ D × D represents a slot-name/slot-value pair instead of just a value in positional terms.
- The argument to a slotted term is a finite bag of slot/value pairs rather than an ordered sequence.
  Bags are used here because, for slotted terms, the order of slot/value pairs is immaterial, but sets cannot be used, since I may happen to map different slots into the same value in D.
  We can now extend the mapping I from Section Model Theory for Condition Language of RIF BLD as follows (where only the last item is new with respect to the earlier definition of I):
- I(k) = I_C(k) if k is a symbol in Const
- I(?v) = I_V(?v) if ?v is a variable in Var
- I(f ( t₁ ... t_n )) = I_F(f)(I(t₁),...,I(t_n))
- I(f ( p₁ -> t₁ ... p_n -> t_n )) = I_SF(f)({<I(p₁),I(t₁)>,...,<I(p_n),I(t_n)>})
- Here we use {...} to denote bags.
I_SR is used to interpret predicates with slotted
- arguments. It is a total function from Const to total 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-name/slot-value pair instead of just a value in positional predicates.
- The argument to a slotted predicate is a finite bag of slot/value pairs rather than an ordered sequence.
  Bags (also known as multisets) 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 I_Truth for slotted predicates as follows:
  - I_Truth(p ( p₁ -> val₁ ... p_k -> val_k )) = I_SR(p)({<I(p₁) I(val₁)>, ... , <I(p_k) I(val_k)>}), where p, p_i ∈ Const and val_i is a term for i=1,...k.
I_sub gives meaning to the subclass relationship. It is a total truth-valued function D × D → TV. The truth valuation for classification formulas of the form sc ## cl, where sc and cl are terms, is defined as follows:
- I_Truth(sc ## cl) = I_sub(I(sc), I(cl))
- In addition, we want the operator ## to be transitive, i.e., we would like c1 ## c2 and c2 ## c3 to imply c1 ## c3. To this end, we require that the mapping I_sub defines a partial order on D. More precisely,
  - For all elements ec1, ec2, ec3 ∈ D, the following must hold: min_t(I_sub(ec1, ec2), I_sub(ec2,ec3)) ≤_t I_sub(ec1, ec3)
  where ≤_t denotes the truth order on TV (see Section Model Theory for Condition Language of RIF BLD) and min_t is the minimum with respect to that truth order.
I_isa gives meaning to class membership. It is a total 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:
- I_Truth(o # cl) = I_isa(I(o), I(cl))
- We also want # and ## to have the usual property that all members of a subclass are also members of the superclass, i.e., we want o # cl and cl ## scl to imply o # scl. To this end, we introduce the following restriction on the mappings I_isa and I_sub:
  - For all elements eo, ec, es ∈ D, the following must hold: min_t(I_isa(eo, ec), I_sub(ec,es)) ≤_t I_isa(eo, es)
  where ≤_t and min_t are as before.