In this section we extend Positive Conditions, defined in Section Positive Conditions, with *slotted Uniterm*s 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

is of the form**slotted term**`t ( p`_{1}`->``v`_{1}...`p`_{n}`->``v`_{n}`)`, where`t`is a term;`p`_{1}, ...,`p`_{n}are terms, which represent the names of the slots; and`v`_{1}, ...,`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`

_{1}, ...,

`e`

_{n}, ...} where η ∈

`SigNames`is the name of the signature and {

`e`

_{1}, ...,

`e`

_{n}, ...} is a countable set of

*slotted arrow expressions*. A

*is a statement of the form*

**slotted arrow expression**(γ

_{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. For instance, (**slotted Boolean expression**`term -> term`,`term -> term`)`=>``atomic`is a slotted Boolean signature expression.

A term `t ( p`_{1} `->` `v`_{1} ... `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 (γ_{1}`->`σ_{1}... γ_{n}`->`σ_{n})`=>`σ.The aforesaid term

`t`is aif σ is**well-formed slotted atomic formula**`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 [ p`_{1}`-> v`_{1}...`p`_{n}`-> v`_{n}`]`, where`t`is a well-formed term, a membership formula, or a subclass formula;`p`_{1}, ...,`p`_{n}are well-formed terms; and each`v`_{1}, ...,`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.

In frame formulas, all terms must have the signature

`term`and`#`,`##`must have the signature`p`_{2}{`(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 |
---|---|

| <Uniterm> <op> |

| <Frame> <object> |

| <Frame> <object> <Member> <lower> |

| <Frame> <object> <Subclass> <lower> |

| <Member> <lower> |

| <Subclass> <lower> |

## 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

*is a formula that is always true (a tautology). If*

**true**`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*,

*, is a tuple of the form*

**I**<

,**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 domainto total truth-valued functions of the form**D**×**D**→**D**. The intuitive meaning of frame slots is that they are functions that take objects and return**TV***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`_{1}`-> V`_{1}`... 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**. This is analogous to the interpretation of regular (positional) terms with two differences:**D**Each argument

`<s,v>`∈×**D**represents a slot-name/slot-value pair instead of just a value in positional terms.**D**- 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

may happen to map different slots into the same value in**I**.**D**We can now extend the mapping

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****I**_{C}(k) if k is a symbol in`Const`(?v) =**I****I**_{V}(?v) if ?v is a variable in`Var`(f ( t**I**_{1}... t_{n})) =**I**_{F}(f)((t**I**_{1}),...,(t**I**_{n}))(f (**I**`p`_{1}`-> t`_{1}...`p`_{n}`-> t`_{n})) =**I**_{SF}(f)({`<`(**I**`p`_{1}),(t**I**_{1})`>`,...,`<`(**I**`p`_{n}),(t**I**_{n})`>`})

- Here we use {...} to denote bags.

**I**_{SR}is used to interpret predicates with slottedarguments. It is a total function from

`Const`to total truth-valued mappings`SetOfFiniteSubbags`(×**D**) →**D**. This is analogous to the interpretation of regular (positional) predicates except for two differences:**TV**Each pair

`<s,v>`∈×**D**represents a slot-name/slot-value pair instead of just a value in positional predicates.**D**- 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, sincemay happen to map different slots into the same value in**I**.**D**

We can now define

**I**_{Truth}for slotted predicates as follows:**I**_{Truth}(p (`p`_{1}`-> val`_{1}...`p`_{k}`-> val`_{k})) =**I**_{SR}(p)({`<`(**I**`p`_{1})(**I**`val`_{1})`>`, ... ,`<`(**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**. The truth valuation for classification formulas of the form**TV**`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. More precisely,**D**For all elements

`ec1`,`ec2`,`ec3`∈, the following must hold: min**D**_{t}(**I**_{sub}(`ec1`,`ec2`),**I**_{sub}(`ec2`,`ec3`)) ≤_{t}**I**_{sub}(`ec1`,`ec3`)

where ≤

_{t}denotes the truth order on(see Section Model Theory for Condition Language of RIF BLD) and min**TV**_{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**. The truth valuation for classification formulas of the form**TV**`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`∈, the following must hold: min**D**_{t}(**I**_{isa}(`eo`,`ec`),**I**_{sub}(`ec`,`es`)) ≤_{t}**I**_{isa}(`eo`,`es`)

where ≤

_{t}and min_{t}are as before.