This is an archive of an inactive wiki and cannot be modified.

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.

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 η{e1, ..., en, ...} where η ∈ SigNames is the name of the signature and {e1, ..., en, ...} is a countable set of slotted arrow expressions. A slotted arrow expression is a statement of the form

A term t ( p1 -> v1 ... pn -> vn ) is a well-formed slotted term with signature σ if

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:

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

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:

In addition, RIF-BLD imposes the following restrictions:

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 SyntaxXML Syntax
predfunc (
  key1 -> filler1
  . . .
  keyn -> fillern
         )
<Uniterm>
  <op>predfunc</op>
  <slot>key1 filler1</slot>
   . . .
  <slot>keyn fillern</slot>
</Uniterm>
inst [
  key1 -> filler1
  . . .
  keyn -> fillern
     ]
<Frame>
  <object>inst</object>
  <slot>key1 filler1</slot>
   . . .
  <slot>keyn fillern</slot>
</Frame>
inst # class [
  key1 -> filler1
  . . .
  keyn -> fillern
             ]
<Frame>
  <object>
    <Member>
      <lower>inst</lower>
      <upper>class</upper>
    </Member>
  </object>
  <slot>key1 filler1</slot>
   . . .
  <slot>keyn fillern</slot>
</Frame>
sub ## super [
  key1 -> filler1
  . . .
  keyn -> fillern
             ]
<Frame>
  <object>
    <Subclass>
      <lower>sub</lower>
      <upper>super</upper>
    </Subclass>
  </object>
  <slot>key1 filler1</slot>
   . . .
  <slot>keyn fillern</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

All the components except the last five, Islot, ISF, ISR, Isub, Iisa, are the same as before. The new mapping Islot is used to interpret frames; the mappings ISF and ISR interpret terms and predicates with named arguments, respectively; Isub gives meaning to the subclass hierarchy; and Iisa interprets class membership.