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.

• A slotted term is of the form t ( p1 -> v1 ... pn -> vn ), where t is a term; p1, ..., pn are terms, which represent the names of the slots; and v1 , ..., vn 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 η{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

• 1 -> κ1, ..., γ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 ( p1 -> v1 ... pn -> vn ) is a well-formed slotted term with signature σ if

• Each pi is a well-formed term with some signature γi.

• Each vi 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 (γ1 -> σ1 ... γ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 (κ1 κ2) ⇒ 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 κ1 and κ2, 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 [ p1  ->  v1 ... pn  -> vn ], where t is a well-formed term, a membership formula, or a subclass formula; p1, ..., pn are well-formed terms; and each v1 , ..., vn is either a well-formed term or a well-formed frame formula.

When t, all the pi, and all the vi are terms, such a formula should be understood as a statement that object t has properties pi, ..., pn, and for each i = 1,...,n, the value of property pi is a set that contains the object vi. When t, pi, or vi 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 fsn{(term -> term, ..., term -> term) => term} and psn{(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 p2{(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 [
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>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">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

• <D,IC, IV, IF, IR, Islot, ISF, ISR, Isub, Iisa>.

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.

• Islot is a total function from the domain D to total truth-valued functions of the form D × DTV. 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 ITruth to flat frames as follows:

• ITruth(T [ p1 -> V1 ... pk -> Vk ]) = mini=1...k(ITruth(T [ pi -> Vi ])), where T, pi, and Vi are terms.

• ITruth(T [ p -> V ]) = Islot(I(p))(I(T),I(V))

• ISF 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) = IC(k) if k is a symbol in Const

• I(?v) = IV(?v) if ?v is a variable in Var

• I(f ( t1 ... tn )) = IF(f)(I(t1),...,I(tn))

• I(f ( p1 -> t1 ... pn -> tn )) = ISF(f)({<I(p1),I(t1)>,...,<I(pn),I(tn)>})

• Here we use {...} to denote bags.
• ISR 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 ITruth for slotted predicates as follows:

• ITruth(p ( p1 -> val1 ... pk -> valk )) = ISR(p)({<I(p1) I(val1)>, ... , <I(pk) I(valk)>}), where p, piConst and vali is a term for i=1,...k.

• Isub gives meaning to the subclass relationship. It is a total truth-valued function D × DTV. 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))

• 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 Isub defines a partial order on D. More precisely,

• For all elements ec1, ec2, ec3D, the following must hold: mint(Isub(ec1, ec2), Isub(ec2,ec3))   ≤t   Isub(ec1, ec3)

where ≤t denotes the truth order on TV (see Section Model Theory for Condition Language of RIF BLD) and mint is the minimum with respect to that truth order.

• Iisa gives meaning to class membership. It is a total truth-valued function D × DTV. 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))

• 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 Iisa and Isub:

• For all elements eo, ec, esD, the following must hold:   mint(Iisa(eo, ec), Isub(ec,es))   ≤t   Iisa(eo, es)

where ≤t and mint are as before.