The Semantics of RIF-BLD as a Specialization of RIF-FLD
This section defines the precise relationship between the semantics of RIF-BLD and the semantic framework of RIF-FLD. The remaining sections describe the semantics of RIF-BLD without referring to the general framework -- except for Primitive Data Types whose definition is not duplicated here.
The semantics of the RIF Basic Logic Dialect is defined by specialization from the semantics of the [:FLD/Semantics:Semantic Framework for Logic Dialects] of RIF. Section [:FLD/Semantics#sec-rif-dialect-semantics:Semantics of a RIF Dialect as a Specialization of RIF-FLD] in that document lists the parameters of the semantic framework, which we need to specialize for RIF-BLD.
Recall that the semantics of a dialect is derived from these notions by specializing the following parameters.
The effect of the syntax.
- RIF-BLD does not support negation. This is the only obvious simplification with respect to RIF-FLD as far as the semantics is concerned.
Truth values.
The set TV of truth values in RIF-BLD consists of just two values, t and f such that f <t t. Clearly, <t is a total order here.
Data types.
RIF-BLD supports all the data types listed in Section Primitive Data Types of RIF-FLD:
xsd:long
xsd:integer
xsd:decimal
xsd:string
xsd:time
xsd:dateTime
rdf:XMLLiteral
rif:text
Logical entailment.
- Recall that logical entailment in RIF-FLD is defined with respect to an unspecified set of intended semantic structures and that dialects of RIF must make this notion concrete. For RIF-BLD, this set is defined in one of the two following equivalent ways:
- as a set of all models; or
- as the unique minimal model.
These two definitions are equivalent for entailment of RIF-BLD conditions by RIF-BLD rulesets, since all rules in RIF-BLD are Horn -- it is a classical result of Van Emden and Kowalski [vEK76].
- Recall that logical entailment in RIF-FLD is defined with respect to an unspecified set of intended semantic structures and that dialects of RIF must make this notion concrete. For RIF-BLD, this set is defined in one of the two following equivalent ways:
Truth Values
The set TV of truth values in RIF-BLD consists of just two values, t and f. This set has a total order, called truth order, such that f <t t.
Semantic Structures
A semantic structure, I, is a tuple of the form <TV, DTS, D, IC, IV, IF, Iframe, ISF, Isub, Iisa, I=, ITruth>. Here D is a non-empty set of elements called the domain of I, and there is a proper subset, Dind ⊂D, which is used to interpret individuals. We use Const to refer to the set of all constant symbols and Var to refer to the set of all variable symbols. TV denotes the set of truth values that the semantic structure uses and DTS is the set of primitive data types used in I (please refer to Section Primitive Data Types of RIF-FLD for the semantics of data types).
The other components of I are total mappings defined as follows:
IC maps Const to elements of D.
- This mapping interprets constant symbols.
If a constant, c ∈ Const, occurs in the position of an individual then it is required that IC(c) ∈ Dind.
- This mapping interprets constant symbols.
IV maps Var to elements of Dind.
- This mapping interprets variable symbols.
IF maps D to functions D* → D (here D* is a set of all sequences of any finite length over the domain D)
- This mapping interprets positional terms.
ISF interprets terms with named arguments. It is a total mapping from Const to the set of total functions of the form SetOfFiniteBags(ArgNames × D) → D. This is analogous to the interpretation of positional terms with two differences:
Each pair <s,v> ∈ ArgNames × D represents a argument/value pair instead of just a value in the case of a positional term.
- The arguments of a term with named arguments constitute a finite bag of argument/value pairs rather than a finite ordered sequence of simple elements.
Bags (multisets) are used here because the order of the argument/value pairs in a term with named arguments is immaterial and the pairs may repeat. For instance, p(a->b a->b).
Iframe is a total mapping from D to total functions of the form SetOfFiniteBags(D × D) → D.
This mapping interprets frame terms. An argument, d ∈ D, to Iframe represent an object and the finite bag {<a1,v1>, ..., <ak,vk>} represents a bag of attribute-value pairs for d. We will see shortly how Iframe is used to determine the truth valuation of frame terms.
Bags are used here because the order of the attribute/value pairs in a frame is immaterial and pairs may repeat. For instance, o[a->b a->b].
Isub gives meaning to the subclass relationship. It is a total function D × D → D.
The operator ## is required to be transitive, i.e., c1 ## c2 and c2 ## c3 must imply c1 ## c3. This is ensured by a restriction in Section Interpretation of Formulas.
Iisa gives meaning to class membership. It is a total function D × D → D.
The relationships # and ## are required to have the usual property that all members of a subclass are also members of the superclass, i.e., o # cl and cl ## scl must imply o # scl. This is ensured by a restriction in Section Interpretation of Formulas.
I= gives meaning to the equality. It is a total function D × D → D.
ITruth is a total mapping D → TV.
- It is used to define truth valuation of formulas.
We also define the following mapping 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(I(f))(I(t1),...,I(tn))
I(f(s1->v1 ... sn->vn)) = ISF(I(f))({<s1,I(v1)>,...,<sn,I(vn)>})
- Here we use {...} to denote a bag of argument/value pairs.
I(o[a1->v1 ... ak->vk]) = Iframe(I(o))({<I(a1),I(v1)>, ..., <I(an),I(vn)>})
- Here {...} denotes a bag of attribute/value pairs.
I(c1##c2) = Isub(I(c1), I(c2))
I(o#c) = Iisa(I(o), I(c))
I(x=y) = I=(I(x), I(y))
The effect of data types. The data types in DTS impose the following restrictions. If dt is a symbol space identifier of a data type, let LSdt denote the lexical space of dt, VSdt denote its value space, and Ldt: LSdt → VSdt the lexical-to-value-space mapping (for the definitions of these concepts, see Section Primitive Data Types of RIF-FLD). Then the following must hold:
VSdt ⊆ D; and
For each constant lit^^dt ∈ LSdt, IC(lit^^dt) = Ldt(lit).
That is, IC must map the constants of a data type dt in accordance with Ldt.
RIF-BLD does not impose restrictions on IC for constants in the lexical spaces that do not correspond to primitive datatypes in DTS.
Interpretation of Formulas
Truth valuation for well-formed formulas in RIF-BLD is determined using the following function, denoted TValI:
Positional atomic formulas: TValI(r(t1 ... tn)) = ITruth(I(r(t1 ... tn)))
Atomic formulas with named arguments: TValI(p(s1->v1 ... sk->vk)) = ITruth(I(p(s1-> v1 ... sk->vk))).
Equality: TValI(x = y) = ITruth(I(x = y)).
To ensure that equality has precisely the expected properties, it is required that ITruth(I(x = y)) = t if and only if I(x) = I(y) and that ITruth(I(x = y)) = f otherwise.
Subclass: TValI(sc ## cl) = ITruth(I(sc ## cl)).
To ensure that the operator ## is transitive, i.e., c1 ## c2 and c2 ## c3 imply c1 ## c3, the following is required: For all c1, c2, c3 ∈ D, mint(TValI(c1 ## c2), TValI(c2 ## c3)) ≤t TValI(c1 ## c3).
Membership: TValI(o # cl) = ITruth(I(o # cl)).
To ensure that all members of a subclass are also members of the superclass, i.e., o # cl and cl ## scl implies o # scl, the following is required: For all o, cl, scl ∈ D, mint(TValI(o # cl), TValI(cl ## scl)) ≤t TValI(o # scl).
Frame: TValI(o[a1->v1 ... ak->vk]) = ITruth(I(o[a1->v1 ... ak->vk])).
- Since the different attribute/value pairs are supposed to be understood as conjunctions, the following is required:
TValI(o[a1->v1 ... ak->vk]) = mint(TValI(o[a1->v1]), ..., TValI(o[ak->vk]))
- Since the different attribute/value pairs are supposed to be understood as conjunctions, the following is required:
Conjunction: TValI(And(c1 ... cn)) = mint(TValI(c1), ..., TValI(cn)).
Disjunction: TValI(Or(c1 ... cn)) = maxt(TValI(c1), ..., TValI(cn)).
Quantification: TValI(Exists ?v1 ... ?vn (φ)) = maxt(TValI*(φ)) and TValI(Forall ?v1 ... ?vn (φ)) = mint(TValI*(φ)).
Here maxt (respectively, mint) is taken over all interpretations I* of the form <TV, DTS, D, IC, I*V, IF, Iframe, ISF, Isub, Iisa, ITruth>, which are exactly like I, except that the mapping I*V, is used instead of IV. I*V is defined to coincide with IV on all variables except, possibly, on ?v1,...,?vn.
Rules: TValI(conclusion :- condition) = t, if TValI(conclusion) ≥t TValI(condition); TValI(conclusion :- condition) = f otherwise.
A model of a set Ψ of formulas is a semantic structure I such that TValI(φ) = t for every φ∈Ψ. In this case, we write I |= Ψ.
Logical Entailment
We now define what it means for a set of RIF-BLD rules to entail a RIF-BLD condition.
Let R be a set of RIF-BLD rules and φ an existentially closed RIF-BLD condition formula. We say that R entails φ, written as R |= φ, if and only if for every semantic structure I of R and every ψ ∈ R, it is the case that TValI(ψ) ≤ TValI(φ).
Equivalently, we can say that R |= φ holds iff whenever I |= R it follows that also I |= φ.