The language of positive RIF conditions determines what can appear as a body (the if-part) of a rule supported by the basic RIF logic. As explained in Section Overview, the Basic RIF Logic Dialect corresponds to definite Horn rules, and the bodies of such rules are conjunctions of atomic formulas without negation. However, it is well-known that disjunctions of such conditions can also be used in the bodies of rules without changing the essential properties of the rule language. This is based on the fundamental logical tautologies (h ← b ∨ c) ≡ ((h ← b) ∧ (h ← c)) and ∀ x (F ∧ G) ≡ (∀ x F ∧ ∀ x G). In other words, a rule with a disjunction in the body can be split into two or more rules that have no such disjunction.

In a later draft, positive RIF conditions will be extended to include builtins, i.e. calls to procedures defined outside the ruleset. The condition language will be shared among the bodies of the rules expressed in future RIF dialects, such as LP, FO, PR and RR. The condition language might also be used to uniformly express integrity contraints and queries. This section presents a syntax and semantics for the RIF condition language.

To make RIF dialects suitable as Web languages, RIF supports the following primitive data types: xsd:long (http://www.w3.org/2001/XMLSchema#long), xsd:string (http://www.w3.org/2001/XMLSchema#string), xsd:decimal (http://www.w3.org/2001/XMLSchema#decimal), xsd:time (http://www.w3.org/2001/XMLSchema#time), xsd:dateTime http://www.w3.org/2001/XMLSchema#dateTime), and the use of international resource identifiers (or IRIs) to refer to individuals, predicates, and functions.

To ensure extensibility and to provide for future higher-order dialects based on formalisms, such as HiLog and Common Logic, the RIF logic language does not draw sharp boundary between the symbols used to denote individuals from symbols used as names for functions or predicates. Instead, all symbols are drawn from the same universal set. RIF dialects control the contexts in which the different symbols can occur by attaching signatures to these symbols.

The Basic RIF logic dialect carefully selects signatures for the symbols so that the corresponding logic will be first-order: each symbol has a unique role as an individual, a function symbol of a particular arity, or a predicate symbol of a particular arity. However, dialects extending the basic logic will be allowed to use signatures in less restrictive fashions so that symbols could be polymorphic and be allowed to occur in several different contexts (for example, both as individuals and as predicates).

We begin by describing a syntax, which is more general than what the basic logic dialect permits. This syntax can be used in the various dialects that extend the basic RIF logic dialect. Then we introduce the notion of a signature and specify the restrictions on the way signatures are allowed to be assigned to symbols.

Syntax

Formal Syntax

The language of RIF Condition Language consists of a countably infinite set of constant symbols Const, a countably infinite set of variable symbols Var, connective symbols ∧ and ∨, quantifiers ∀ and ∃, and auxiliary symbols like (, ), and so on. The basic language construct is called term, which is formally defined as follows:

• If t ∈ Const or t ∈ Var then t is a term.

• If t and t₁, ..., t_n are terms then t(t₁ ... t_n) is a term

This definition is very general. It makes no distinction between constant symbols that represent individuals, predicates, and function symbols. The same symbol can occur in multiple contexts at the same time. For instance, p(p(a), p(a,b,c)). Even variables and general terms are allowed to occur in the position of predicates and function symbols. For instance, p(a)(p(b,c),q) is also a term. To control the context in which any given symbol can occur in RIF dialects, the language associates a signature with each symbol (both constant and variable symbols).

Signatures. Let SigNames be a non-empty finite or countably infinite set of signature names. We assume that this set includes at least the following signature names: i and bool. The signature name i is intended to represent the context where the constants that denote individual objects are allowed to appear. The name bool represents the context of atomic formulas. A signature is a statement of the form s{e₁ ... e_n ...} where s ∈ SigNames is the name of the signature and {e₁ ... e_n ...} is a set of arrow or Boolean signature expressions. This set can be empty, finite, or countably infinite. In the basic RIF logic dialect, this set will have at most one expression, but in more expressive dialects a signature can have more than one expression and in this way they can support polymorphism.

Arrow and Boolean signature expressions are defined as follows, where s₁, ..., s_n, and s are signature names from SigNames:

• (s₁ ... s_n) → s, where n≥0, is an arrow signature expression. In particular, () → i and (i) → i are arrow signature expressions.

• If s above is bool then the signature is called a Boolean signature expression.

A set S of signatures is said to be coherent if

• it contains the signatures i{ } and bool{ }, which represent the context of individual objects and atomic formulas; and

• no two different signatures in S have the same name.

Well-formed terms and formulas. RIF uses signatures to control the context in which terms can appear through the notion of well-formed terms and well-formed atomic formulas. First, as mentioned above, each symbol (constant or variable) is associated with exactly one signature from a coherent set of signatures. (Different symbols can be associated with the same signature, but one symbol cannot be associated with more than one signature.) If σ is a signature then we will use σ^# to denote the name of that signature.

• If s is a constant or variable with signature i{ } then it is a well-formed term with signature i{ }.

• A term t(t₁ ... t_n) is a well-formed term with signature σ iff

  • t is a well-formed term with signature σ₀;

  • Each t_i is a well-formed term with signature σ_j, j = 1,...,n; and

  • σ₀ contains an arrow expression of the form (σ₁^# ... σ_n^#) → σ^#

• A term t(t₁ ... t_n) is a well-formed atomic formula iff

  • it is a well-formed term with signature bool{ }.

RIF assumes that there is a special predicate, =, which denotes equality. Like other predicates, it has a signature, which includes the Boolean expression (i i) → bool and possibly other expressions of the form (s s) → bool, where s is a signature name. No other signatures are allowed for =. We note that it is a common practice to write the atomic formulas involving = using infix notation, i.e., a = b instead of =(a,b). The equality predicate has special model-theoretic semantics, as explained in Section Model Theory for Basic RIF Condition Language.

More general formulas are constructed out of atomic formulas with the help of logical connectives. The Basic RIF Condition Language defines the following general well-formed formulas.

• If φ is an atomic formula than it is also a general well-formed formula.

• φ ∧ ψ is a general well-formed formula, if so are φ and ψ.

• φ ∨ ψ is a general well-formed formula, if so are φ and ψ.

• ∃ V₁ ... V_n φ is a general well-formed formula, if so is φ and V₁, ..., V_n are variables.

Signatures in the Basic RIF Condition Language. The basic RIF condition language presents a much simpler picture to the user by restricting the set of well-formed terms with a very constraint coherent set of signatures. Namely, the signature set of the basic RIF logic language contains the following signatures:

• i{ } and bool{ }

• For every arity n, there ares signatures f_n{(i ... i) → i} and p_n{(i ... i) → bool} (there are n i's inside the parentheses), which represent function symbols of arity n and predicate symbols of arity n, respectively. The symbols f,,n,, and p`_n are reserved signature names in the basic RIF logic dialect.

In this way, each constant symbol can be either an individual, a predicate of one particular arity, or a function symbol of one particular arity.

• All variables are associated with signature i{ }, so they can range only over individuals.

• The equality symbol, =, has signature p₂{(i i) → bool}. In this way, the equality predicate can compare only individual constants and not predicates and function symbols.

Primitive data types. The set of all constant symbols in RIF has a number of predefined subsets, which correspond to XML data types and to some RIF-specific types. Namely, the following primitive data types are supported: xsd:long (http://www.w3.org/2001/XMLSchema#long), xsd:string (http://www.w3.org/2001/XMLSchema#string), xsd:decimal (http://www.w3.org/2001/XMLSchema#decimal), xsd:time (http://www.w3.org/2001/XMLSchema#time), xsd:dateTime http://www.w3.org/2001/XMLSchema#dateTime). In addition, a RIF-specific data type, called rif:iri (for international resource identifier or IRI), is supported. Constant symbols that belong to this data type have special concrete syntax and semantic structures will interpret them in a special way. For the formal syntax we only need to state that the set Const of all constant symbols has subsets Const_xsd:long, Const_xsd:string, Const_xsd:decimal, Const_xsd:time, Const_xsd:dateTime, and Const_rif:iri.

Abstract Syntax

The abstract syntax of the 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 of TERM

    subclass Uniterm

class TERM

    subclass Var
        property name: xsd:string

    subclass Const
        property name: xsd:string

    subclass Uniterm       
        property op: Const
        property arg: list of TERM

The multiplicity of the side property (role) of the Equal class is assumed to be exactly 2.

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. Automatic asn06-to-UML transformation is available.

The central class of RIF, CONDITION, is specified recursively through its subclasses and their parts. The Equal class has two side roles. Two pairs of roles distinguish between the declare and formula parts of the Exists class, and between the operation (op) and arguments (arg) of the Uniterm class, where multiple arguments are subject to an ordered constraint (the natural "left-to-right" order):

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. The EBNF syntax below, which instantiates the abstract syntax, is used throughout this document to explain and illustrate the main ideas. This syntax is similar in style to what in OWL is called the Abstract Syntax http://www.w3.org/TR/owl-semantics/syntax.html.

EBNF representation. 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
  Uniterm     ::= Const '(' TERM* ')'
  Equal       ::= TERM '=' TERM
  TERM        ::= Const | Var | Uniterm
  Const       ::= CONSTNAME | '"'CONSTNAME'"''^^'TYPENAME
  Var         ::= '?'VARNAME

The above is a standard syntax for a variant of first-order logic. The application of a symbol from Const to a sequence of terms is called Uniterm ("Universal term") since it can be used to play the role of a function term or an atomic formula depending on the syntactic context in which the application occurs. The non-terminal ATOMIC stands for (positive) atomic formula, which can later be complemented with "negated atomic formula". EXISTENTIAL stands for "existential formula", which in Horn-like conditions is the only quantified formula but in later conditions may be complemented with "universal formula" (Var+ denotes the list of free variables in CONDITION). The production CONJUNCTION defines conjunctions of conditions, and DISJUNCTION denotes disjunctions. Finally, CONDITION assembles everything into what we call RIF conditions. RIF dialects will extend these conditions in various ways.

Note that individuals, function symbols, and predicate symbols all belong to the same set of symbols (Const). This syntax is more general than what the basic RIF logic dialect actually permits. As explained in Section Formal Syntax a set of signatures restricts this syntax to allow only the terms that are allowed in standard firts-order logic.

The above EBNF, where TERM* is understood as TERM* ::= | TERM TERM*, uses spaces to indicate Lisp-like whitespace (SPACE, TAB, or NEWLINE) character sequences in the defined language; these must consist of at least one whitespace character when used as the separator between adjacent TERMs, and can consist of zero or more whitespace characters elsewhere. Where spaces are omitted from the EBNF, as between '?' and VARNAME in '?'VARNAME, there must be no whitespace character in the defined language.

At this point we do not commit to any particular vocabulary for the names of constants and variables. These are still assumed to be alphanumeric character sequences (except 'And' and 'Or').

Note that variables in the RIF Condition Language can be free and quantified. All quantification is explicit. All variables introduced by quantification should also occur in the quantified formula. Initially, only existential quantification is used. Universal quantification will be introduced later. We adopt the usual scoping rules for quantifiers from first-order logic. Variables that are not explicitly quantified are free.

Free variables arise because CONDITION can occur in an if part of a rule. When this happens, the free variables in a condition formula are precisely those variables that also occur in the then part of the rule. We shall see in Section Horn Rules that such variables are quantified universally outside of the rule, and the scope of such quantification is the entire rule. For instance, the variable ?Y in the first RIF condition of Example 1 is quantified, existentially, but ?X is free. However, when this condition occurs in the if part of the second rule in Example 1, then this variable is quantified universally outside of the rule. (The precise syntax for RIF rules will be given in Section Horn Rules.)

Example 1 (A RIF condition in and outside of a rule)

 RIF condition:
                        Exists ?Y (condition(?X ?Y)) 

 RIF Horn rule:
        Forall ?X (then(?X) :-  Exists ?Y (condition(?X ?Y)))

When RIF conditions are used as queries, their free variables carry answer bindings back to the caller.

XML serialization. The following is a possible XML-serializing mapping of the abstract syntax in Section Abstract Syntax (and of the above EBNF syntax). This XML serialization is fully striped, where positional information is optionally exploited only for the arg role elements. For example, role elements (declare and formula) are explicit within the Exists element. Following the examples of Java and RDF, we use capitalized names for class elements and names that start with lowercase for role elements.

The all-uppercase non-terminals in EBNF, such as CONDITION, become XML entities. They act like macros and are not visible in instance markup. The other non-terminals and symbols (such as Exists or =) become XML elements, as shown below.

- 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 (atomic or function-expression formula)
- op      (operation role)
- arg     (argument role, positional/non-positional without/with 'index' attribute)
- Equal   (prefix version of term equation '=')
- side    (left-hand and right-hand side role)
- Const   (individual, function symbol, or relation/predicate symbol)
- Var     (logic variable)

The following example illustrates XML serialization of RIF conditions.

Example 2 (A RIF condition and its XML serialization):

a. RIF condition:

  And ( Exists ?Buyer (purchase(?Buyer ?Seller book(?Author LeRif) USD(49))) ?Seller=?Author )

b. XML serialization:

  <And>
    <formula>
      <Exists>
        <declare><Var>Buyer</Var></declare>
        <formula>
          <Uniterm>
            <op><Const>purchase</Const></op>
            <arg><Var>Buyer</Var></arg>
            <arg><Var>Seller</Var></arg>
            <arg>
              <Uniterm>
                <op><Const>book</Const></op>
                <arg><Var>Author</Var></arg>
                <arg><Const>LeRif</Const></arg>
              </Uniterm>
            </arg>
            <arg>
              <Uniterm>
                <op><Const>USD</Const></op>
                <arg><Const>49</Const></arg>
              </Uniterm>
            </arg>
          </Uniterm>
        </formula>
      </Exists>
    </formula>
    <formula>
      <Equal>
        <side><Var>Seller</Var></side>
        <side><Var>Author</Var></side>
      </Equal>
    </formula>
  </And>

Syntax for Primitive Types. In this document we will use the following syntax, following N-Triples, to specify the constant symbols that belong to primitive data types:

   "value"^^typename

For instance, "123"^^xsd:long is a symbol that belongs to the primitive data type xsd:long, "2007-11-23T03:55:44-02:30"^^xsd:dateTime is a symbol of data type xsd:dateTime, and "ftp://example.com/foobar"^^rif:iri is a symbol that belongs to the data type rif:iri. The part of such symbols that occurs inside the double quotes is called a literal of the symbol. The surrounding double quotes are not part of the literal. If a double quote must be included as part of a literal, it must be escaped with the backslash.

The XML syntax for primitive types can utilize the type attribute associated with XML term elements such as Const. For instance, the earlier xsd:dateTime example can be represented as <Const type="xsd:dateTime">2007-11-23T03:55:44-02:30</Const>.

Many primitive types in RIF may be based on the XML Schema data types and thus it is expected that some names of RIF primitive types will be references to those XML Schema types. In this case, these IRIs will be used as type names.

In this version of the RIF Core document, we define the following primitive types, where the prefix xsd refers to the XML Schema URI and rif is the prefix for the RIF language. The syntax such as xsd:long should be understood as a compact uri, i.e., a macro, which expands to a concatenation of the character sequence denoted by the prefix xsd and the string long. In the next version of this document we will introduce a syntax for defining prefixes for compact URIs and will also expand on the syntax for the symbols that can be used to denote RIF's primitive data types.

• xsd:long. This data type corresponds to the XML data type xsd:long. Example: "123"^^xsd:long. Long integers also have a short notation, which does not require the "..."^^xsd:long wrapper. Example: 123.

• xsd:decimal. This corresponds to the XML data type xsd:decimal. Example: "123.45"^^xsd:decimal. Decimals also have an alternative short notation, which does not require the "..."^^xsd:decimal wrapper. Example: 123.45.

The type xsd:decimal is a supertype of xsd:long.

• xsd:string. This corresponds to the XML data type xsd:string. Example: "a string"^^xsd:string. Double quotes that appear inside strings are escaped with a backslash and a backslash that is supposed to appear in the string must be escaped with another backslash. Strings have also an alternative short notation. Example: 'a string'. In this notation, single quotes and backslashes that occur inside such strings are escaped with backslashes.

• xsd:time. This corresponds to the XML data type xsd:time. Example: "18:33:44.2345"^^xsd:time.

• xsd:dateTime. This type corresponds to the XML data type xsd:dateTime. Example: "2007-03-12T21:22:33.44-01:30"^^xsd:dateTime.

• rif:iri. Symbols of this type have the form "XYZ"^^rif:iri, where XYZ is an IRI as specified in RFC 3987.

Other XML data types that are likely to be incorporated in RIF include xsd:double, xsd:date, and a type for temporal duration. At present, the partial order on the above primitive data types is imposed by the XML Schema hierarchy, so the only subtype relationship is between xsd:long and xsd:decimal. This may be extended as more types are added.

The type rif:iri is intended to be used in a way similar to RDFS resources. The domain of the type rif:iri can be any set and no a priori equalities among the members of the type rif:iri are assumed. This domain is not the same as the value space of the XML primitive type anyURI.

The constant symbols that correspond to XML data types all have the signature i{ } in the basic RIF logic dialect. The symbols of type rif:iri can have any signature allowed by the basic RIF logic: i, f_n, or p_n, for n = 0,1,....

The purchase atomic formula of Example 2 can be enriched with primitive types, obtaining the EBNF version

purchase(?Buyer ?Seller book(?Author "LeRif"^^xsd:string) USD("49"^^xsd:long))

and its XML serialization

          <Uniterm>
            <op><Const>purchase</Const></op>
            <arg><Var>Buyer</Var></arg>
            <arg><Var>Seller</Var></arg>
            <arg>
              <Uniterm>
                <op><Const>book</Const></op>
                <arg><Var>Author</Var></arg>
                <arg><Const type="xsd:string">LeRif</Const></arg>
              </Uniterm>
            </arg>
            <arg>
              <Uniterm>
                <op><Const>USD</Const></op>
                <arg><Const type="xsd:long">49</Const></arg>
              </Uniterm>
            </arg>
          </Uniterm>

Specifying Signatures in RIF Dialects

We will now explain how signatures are defined in the Basic Condition Language and its extensions. In the Basic RIF Logic dialect, there is no need to declare signatures, since they can be inferred. Indeed, the basic logic dialect assumes that each symbol is associated with a unique signature. Therefore, the signature can be determined by the context in which the symbol is used. If a symbol is used in more than one context, the parser should deem it as a syntax error.

In dialects that extend the Basic RIF Condition Language, signature inference of the above kind is not possible, in general, and might not always be appropriate even when it is possible. For this reason, we intriduce the attribute signature for the XML tags Const and Var. The value of such a tag is supposed to be the signature name for the corresponding symbol. For instance, in the above example, purchase was a 4-ary predicate, so it could be specified as <Const signature="p4">purchase</Const>. Since variables in the basic condition language always have the signature i, we could write <Var signature="i">Author</Var>.

The signature attribute is optional, and its value can be inferred for the basic language. Dialects that extend the basic logic dialect can adopt their own rules for omitting this attribute and for inferring its values. The basic language does not need any special syntax for defining signatures -- all signature names are already defined: i, f0, f1, p0, p1, etc. The dialects, however, will need a special sublanguage for defining signatures. The signature

  mysig{
         (s1 s2 s3) -> bool,
         (s i) -> i
       } 

can, for example, be defined using the following XML excerpt:

  <rif:signature rif:signature-name="mysig">
      <rif:sig-expression rif:sig-head="bool">
          s1 s2 s3
      </rif:sig-expression>
      <rif:sig-expression rif:sig-head="i">
          s i
      </rif:sig-expression>
  </rif:signature>

Model Theory for the Basic RIF Condition Language

The first step in defining a model-theoretic semantics for a logic-based language is to define the notion of a semantic structure, also known as an interpretation. (See end note on the rationale.)

Semantic structures. A semantic structure, I, is a tuple of the form <D,I_C, I_V, I_F, I_R>, which determines the truth value of every formula, as explained below. Currently, by formula we mean anything produced by the CONDITION production in the EBNF. Later on this term will also include rules. Other dialects might extend this notion even further.

The set of truth values is denoted by TV. For the basic RIF logic dialect, TV includes only two values, t (true) and f (false). (See end note on truth values.)

The set TV has a total or partial order, called the truth order; it is denoted with <_t. In the basic RIF logic, f <_t t, and it is a total order. (See end note on ordering truth values.)

To define how semantic structures determine the truth values of RIF formulas, we introduce the following sets:

• D - a non-empty set of elements called the domain of I,

• Const - the set of individuals, predicate names, and function symbols,

• Var - the set of variables.

The mappings that constitute an interpretation, I, are as follows:

• I_C from Const to elements of D

• I_V from Var to elements of D

• I_F from Const to functions from D* into D (here D* is a set of all tuples of any length over the domain D)

• I_R from Const to truth-valued mappings D* → TV

It is convenient to define a more general mapping, I, based on the mappings I_C, I_V, I_F, and I_R:

• 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))

Note that f() and f can be interpreted differently by semantic structures, and the proposed XML serialization also treats them as distinct terms: the nullary function application <Uniterm><Const>f</Const></Uniterm> vs. the symbol <Const>f</Const>. Semantically, neither f() = f nor f() ≠ f are entailed a priori. However, if desirable, a particular application or a dialect may introduce axioms of the form f = f() to equate symbols and nullary terms.

Truth valuation for formulas. Observe that the notion of signatures from Section Formal Syntax is used only to constrain the syntax and does not appear in the definition of the semantic structure. This is because when we define truth valuations for formulas, below, all formulas are assumed to be well-formed.

Truth valuation for well-formed formulas in the basic RIF condition language is determined using the following function, denoted I_Truth:

• Atomic formulas: I_Truth(r(t₁ ... t_n)) = I_R(r)(I(t₁),...,I(t_n))

• Equality: I_Truth(t₁=t₂) = t iff I(t₁) = I(t₂); I_Truth(t₁=t₂) = f otherwise.

• Conjunction: I_Truth(And(c₁ ... c_n)) = min_t(I_Truth(c₁),...,I_Truth(c_n)), where min_t is minimum with respect to the truth order.

• Disjunction: I_Truth(Or(c₁ ... c_n)) = max_t(I_Truth(c₁),...,I_Truth(c_n)), where max_t is maximum with respect to the truth order.

• Quantification: I_Truth(Exists ?v₁ ... ?v_n (c)) = max_t(I*_Truth(c)), where max_t is taken over all interpretations I* of the form <D,I_C, I*_V, I_F, I_R>, where I*_V is the same as I_V except possibly on the variables ?v₁,...,?v_n (i.e., I* agrees with I everywhere except possibly in its interpretation of the variables ?v₁ ... ?v_n).

Notice that the mapping I_Truth is uniquely determined by the four mapping comprising I and, therefore, it does not need to be listed explicitly.

Interpretation of primitive data types. We now explain how primitive data types are integrated into the semantics of the basic RIF logic.

The XML Schema Part 2: Datatypes specification defines the value space for each XML data type, including the data types such as xsd:decimal, which are of interest to RIF. The value space is different from the so-called lexical space. Lexical space refers to the syntax of the constant symbols that belong to a particular primitive data type. For instance, "1.2"^^xsd:decimal and "1.20"^^xsd:decimal are two different constants in RIF and in the lexical space of the XML data types. However, these two constants are interpreted by the same element of the value space of the xsd:decimal type.

Formally, each of the XML data types supported by RIF comes with a value space, denoted by D_type (for instance, D_xsd:decimal), and a mapping, I_C: Const_type → D_type. These value spaces and the corresponding mappings are defined by the XML Schema Part 2: Datatypes specification. We assume that D_type ⊆ D for each XML data type and that D_t is disjoint from D_s for different XML primitive types s and t. For instance, for xsd:decimal this mapping is I_C: Const_xsd:decimal → D_xsd:decimal, and it follows from the aforesaid specification that, for instance, I_C("1.2"^^xsd:decimal) = I_C("1.20"^^xsd:decimal) in every semantic structure.

For the rif:iri data type, the corresponding mapping is I_C: Const_rif:iri → D, i.e., D_rif:iri = D and the interpretation mapping is allowed to map an IRI into any value in the domain of the semantic structure.