- From: Boley, Harold <Harold.Boley@nrc-cnrc.gc.ca>
- Date: Sun, 23 Apr 2006 14:21:09 -0400
- To: <public-rif-wg@w3.org>
- Message-ID: <E4D07AB09F5F044299333C8D0FEB45E90211FB37@nrccenexb1.nrc.ca>
Dear all, Michael Kifer, I, and several other RIF participants have been working on this draft of a RIF Extensible Design for the planned extensibility discussion in a telecon. Please find it below and attached. -- Harold RIF Extensible Design Draft 2006-04-23 ~~~~~~~~~~~~~~~~~~~~~ Harold Boley (NRC), Michael Kifer (Stony Brook University), Jeff Pan (University of Aberdeen), Gerd Wagner (BTU Cottbus), Alex Kozlenkov (Betfair), Jos de Bruijn (DERI), Mike Dean (BBN Technologies), Giorgos Stamou (NTUA) Summary This proposal starts with a language of conditions that can be used for positive rule bodies and then extends it with negative literals, builtins, and constructs to query OWL and RDF (via SPARQL). The rationale for focusing on this sublanguage is that it can be shared among five different sublanguages of interest to RIF. We then discuss various extensions of this sublanguage and propose an interoperation/interchange evaluation. A. RIF Condition Language This proposal develops a set of fundamental concepts shared by the rule languages of interest to the RIF WG as outlined in the Design Roadmap (http://lists.w3.org/Archives/Public/public-rif-wg/2006Feb/0255.html). Here we focus on the one part that is shared by Logic Programming rules, Production (Condition-Action) rules, Reactive (Event-Condition-Action) rules, Normative rules (Integrity Constraints), and queries. We call this part 'Conditions' and the proposed sublanguage 'RIF Condition Language' (as a working title). The RIF Condition Language is common ground for specifying syntactic fragments in several different dialects of RIF: - Rule bodies in a declarative logic programming dialect (LP) - Rule bodies in a first-order dialect (FO) - Conditions in the bodies in production rules dialects (PR) - The non-action part of the rule bodies in reactive rules dialects (RR) - Integrity constraints (IC) - Queries in LP dialects (QY) Note that for rules this sublanguage is intended to be used only in the bodies, not their heads. The various RIF dialects diverge in the way they specify rule heads and other parts of their rules. We believe that by focusing on the condition part of the rule bodies we can achieve maximum syntactic (and some semantic) reuse among RIF dialects. Since different semantics are possible for syntactically identical rule sets, we propose that the semantics of a RIF rule set be specified by a predefined attribute. We will elaborate on this proposal separately, but the idea is to organize the most important known semantic and syntactic features into a taxonomy (which could be extended to accommodate new semantics/syntax), and the values of the aforementioned attribute would come from that taxonomy. A.1 Basis: Positive Conditions The basis of the language is formed by what can appear in the bodies of Horn-like rules with equality -- conjunctions and disjunctions of atomic formulas and equations (such rules reduce to pure Horn). We later extend our proposal to include builtins. As mentioned in the introduction, the motivation is that this sublanguage can be shared among the bodies of the rules expressed in the following RIF dialects: - FO (first order) - LP (logic programming) - PR (production rules) - RR (reactive rules) This sublanguage can also be used to uniformly express: - IC (integrity constraints) - QY (queries) SYNTAX ------ Essential BNF for human-readable syntax: Data ::= value Ind ::= object Var ::= '?' name TERM ::= Data | Ind | Var | Expr Expr ::= Fun '(' TERM* ')' Atom ::= Rel '(' TERM* ')' | TERM '=' TERM LITFORM ::= Atom QUANTIF ::= 'Exists' Var+ '(' CONDIT ')' CONJ ::= 'And' '(' CONDIT* ')' DISJ ::= 'Or' '(' CONDIT* ')' CONDIT ::= LITFORM | QUANTIF | CONJ | DISJ Here LITFORM stands for Literal Formula and anticipates the introduction of negated atoms later on. QUANTIF stands for Quantified Formula, which for Horn-like conditions can only be 'Exists' Formulas (Var+ variables should occur free in the scoped CONDIT, so 'Exists' can quantify them; free variables are discussed below). More explicitly than in logic programming, CONJ expresses formula conjunctions, and DISJ expresses disjunctions. Finally, CONDIT combines everything and defines RIF conditions, which can later be extended beyond LITFORM, QUANTIF, CONJ, or DISJ. We assume that all constants (Data and Ind) belong to two different logical sorts: the sort of values and the sort of objects. This means that every constant carries with it the designation of the sort to which it belongs (indicating whether the constant is a value or an object). Values (Data) can also optionally carry a designation of their datatype (e.g., TIME, Integer). Note that there are two uses of variables in the RIF condition language: free and quantified. All quantified variables are quantified explicitly, existentially (and also universally, later). We adopt the usual scoping rules for quantification from first-order logic. Variables that are not explicitly quantified are free. The free variables are needed because we are dealing with conditions that occur in rule bodies only. When a condition occurs in such a rule body, the free variables in the condition are precisely those that also occur in the rule head. Such variables are quantified universally outside of the rule, and the scope of such quantification is the entire rule. For instance, the variable ?X in the rule below is free in the condition that occurs in the rule body, but it is universally quantified outside of the rule. Condition with a free variable ?X: ... Exists ?Y (condition(..?X..?Y..)) ... Rule using the condition in its body: Forall ?X (head(...?X...) :- ... Exists ?Y (condition(..?X..?Y..)) ...) When conditions are used as queries, their free variables are to be bound to carry the answer bindings back to the caller. The semantics of conditions that contain free variables is defined in the section SEMANTICS. Example 1 (A RIF condition in human-readable syntax): In this condition, ?Buyer is quantified existentially, while ?Seller and ?Author are free: And ( Exists ?Buyer (purchase(?Buyer ?Seller book(?Author LeRif) $49)) ?Seller=?Author ) This syntax is similar in style, and compatible to, the OWL Abstract Syntax (http://www.w3.org/TR/owl-semantics/syntax.html). An XML syntax can be obtained from the above BNF as follows. The non-terminals in all-upercase such as CONDIT become XML entities, which act like macros and will not be visible in instance markups. The other non-terminals and symbols ('=', 'Exists', etc.) become XML elements, which are adapted from RuleML as shown below. Optional attributes are added for finer distinctions. For example, an optional attribute in the Data element can point to an XML Schema Datatype. - Data (value constant, including optional attribute for a datatype IRI) - Ind (object constant; empty element with attribute, iri, for oid; e.g. global: <Ind iri="http://www.w3.org"/>, local: <Ind iri="#foo"/>) - Var (logic variable; optional type attribute, e.g. RDFS/OWL-class IRI) - Fun (n-ary function symbol; optional attribute designating interpreted [a.k.a. equation-defined] functions in contrast to uninterpreted [a.k.a. free] functions) - Rel (n-ary relation symbol [a.k.a. predicate]) - Expr (expression formula) - Atom (atomic formula; optional attribute for external atoms) - Equal (prefix version of term equation '=') - Exists (quantified formula for 'Exists') - And (conjunction; optional attribute for sequential conjunctions) - Or (disjunction; optional attribute for sequential disjunctions) Based on the FOL RuleML (http://www.w3.org/Submission/FOL-RuleML) experience, this could be directly rewritten as a DTD or an XML Schema. Example 2 (A RIF condition in XML syntax): The condition formula in Example 1 can be serialized in XML as shown: <And> <Exists> <Var>Buyer</Var> <Atom> <Rel>purchase</Rel> <Var>Buyer</Var> <Var>Seller</Var> <Expr> <Fun>book</Fun> <Var>Author</Var> <Ind>LeRif</Ind> </Expr> <Data>$49</Data> </Atom> </Exists> <Equal> <Var>Seller</Var> <Var>Author</Var> </Equal> </And> Note that the distinction between the sort of values and the sort of objects can be extended from Data vs. Ind to variables (Var) by using an optional attribute. This corresponds to the so-called d-variables and i-variables in SWRL (http://www.w3.org/Submission/SWRL). Sorts can also be optionally added to function symbols and predicates in order to support sorted languages. SEMANTICS --------- The semantics of a ruleset R is defined by a collection of intended models. In case of FOL, all models of R are intended. In LP, only some models (e.g., well-founded or stable models of R) are intended. However, here we are talking only about condition parts of the rules. So, by semantics we mean the notion of satisfaction of a formula in the interpretations of the various RIF dialects. For example, in FO, all first-order interpretations are appropriate. In LP, infinite Herbrand models are typically used. In LP with the well-founded semantics, 3-valued Herbrand models are used. Stable model semantics uses only 2-valued interpretations. The notion of satisfaction in a model is the same for all dialects of RIF, and in the 2-valued case does not depend on the semantic tags associated with the rulesets in which our conditions occur. (Well-founded interpretations, being 3-valued, are slightly different.) Given a condition formula phi(X1,...,Xn) with free variables X1, ..., Xn and an interpretation M, define M(phi(X1,...,Xn)) as the set of all bindings (a1/X1,...,an/Xn) such that M |= phi(a1,...,an). For instance, denoting the formula of Example 1 as phi(?Seller,?Author), if we use the following Herbrand interpretation: M = {purchase(Mary John book(Fred LeRif) $49), purchase(Nina Fred book(Fred LeRif) $49) purchase(Alice Floob book(Floob LeRif) $49)} then M(phi(?Seller,?Author)) is: {(Fred/?Seller,Fred/?Author), (Floob/?Seller,Floob/?Author)} The notion of M(phi(X1,...,Xn)) is independent of the semantics of the ruleset to which phi(X1,...,Xn) is posed, and it "plugs into" the model-theoretic semantics of the rulesets under FO, LP, and the operational semantics of PR. Note that integrity constraints (which are closed formulas) are simply checked against the intended models of the ruleset. Therefore, the semantics of integrity constraints is fully defined by the above notion of satisfaction in the models of rulesets. Thus, these constraints can be full first-order formulas even in case of LP rulesets. The same can be said about queries. While semantics can be defined for very general classes of constraints and queries, this does not mean that the problem of constraint satisfaction/query answering is decidable or has efficient evaluation techniques for such general classes. A.2 Extension: Negative Conditions This extension introduces two kinds of negation (Naf and Neg) to the RIF Condition Language, initially proposed for Phase 1 queries. Neg denotes classical negation as defined in first-order logic; special uses of it can be shared by FO and all dialects that support a form of classical negation (e.g., certain dialects of LP; perhaps some PR dialects). Naf denotes negation as failure in one of its incarnations (well-founded or stable-model). The actual flavor of Naf is determined by inspecting the value of a semantic tag associated with the ruleset. Naf is used in LP (and in queries and constraints over the intended models of LP); it can possibly be relevant to PR and RR. Alongside negation we can introduce explicit universal quantification. SYNTAX ------ This extension introduces two negation symbols over atoms, and one legal nesting, for which we propose to use the notation Naf/Neg, as in RuleML: LITFORM ::= Atom | 'Neg' Atom | 'Naf' Atom | 'Naf' 'Neg' Atom Note that in Phase 1 we are proposing to use negation only in queries. Phase 1 rules will all be Horn and their bodies will not have negation. Phase 2 will extend RIF to allow negation in rules as well. The next step could be to allow universal quantification: QUANTIF ::= 'Exists' Var+ '(' CONDIT ')' | 'Forall' Var+ '(' CONDIT ')' SEMANTICS --------- The semantics of atomic Neg in the models of the FO dialect is standard. For LP dialects supporting "classical" negation, Neg-negated predicates are interpreted by fresh predicates that are appropriately axiomatized. For instance, Neg of p is associated with a fresh predicate, Neg_p, and Neg p(...) is said to be true in a model iff Neg_p(...) is. It is also required that for any given tuple of ground arguments, the formulas p(...) and Neg_p(...) cannot be true in the same model. The following (Phase 2) dialects of RIF will support Neg and/or Naf: - LP/WF (the well-founded semantics) generally supports only Naf, but some variants (e.g., Courteous LP) also support Neg. - LP/SMS (stable model semantics) supports both Neg and Naf (e.g., ERDF). - FO supports Neg only. Queries and integrity constraints can use those forms of negation that are supported by the rulesets that they constrain or query. To distinguish the different possible semantics for the same ruleset, RIF will define an attribute that will explicitly specify the semantics under which the corresponding ruleset is to be interpreted. A.3 Extension: Builtins in Conditions A builtin is a relation or function for which there is a single, fixed interpretation. For instance, the relation "<" and the function "+" have fixed and unique interpretations over the domain of numbers. Although builtin functions are not strictly needed, as they can be represented by builtin relations, a practical language needs both datatype relations and datatype functions. (The equality predicate can be used to bind the result of a builtin function call to a logical variable.) Satisfaction of an atomic expression that is based on a builtin is done with respect to the concrete domain with which this builtin is associated. Some builtins may be polymorphic and have several associated domains. For instance, in the domain of strings, "<" can be viewed as lexicographics ordering and "+" as string concatenation. In that case, the proper interpretation of a builtin is determined by the arguments of the builtin predicate or function. RIF can support different sets of builtins. For instance, each builtin can be identified by an IRI, in which case support for SWRL, SPARQL, and XQuery builtins is feasible. Note that, in general, satisfiability of a conjunction of builtin predicates may be undecidable. In RIF we should probably strive to allow only those sets of builtins for which satisfiability of conjunctive formulas is decidable. A.4 Extension: Resource Conditions A special external atom can be used to support SPARQL queries to RDF. RDF facts can be represented via a dedicated ternary predicate, and bNodes can be represented using existential variables. A.5 Extension: Ontology Conditions A special external atom or an entire conjunction of such atoms can be used to achieve hybrid rule-ontology integration, allowing a query-like interface to OWL classes (including their subClassOf subsumption) and properties (including subPropertyOf subsumption). Optional typing of RIF variables (e.g., for a Sorted Horn Logic) can be regarded as the special case of such an interface for OWL-Lite classes. (Predefined classes, such as Integer, can be borrowed from XML Part 2, Datatypes.) The semantics of such integrations are different for RIF LP, FO, and PR. In case of FO, there is no semantic mismatch and the overall semantics is first-order. In case of LP, recent work by Rosati (DL+Log, KR2006) provides a semantics for a very general class of rulesets that are tightly integrated with DL-based ontologies. However, even more general, ad hoc interoperability between rules and ontologies might be needed. For PR and RR, interoperability with OWL is likely not to have model-theoretic semantics as it will be ad hoc. B. Extension: RIF Horn Rule Language This extends Horn conditions A.1-A.5 to Horn rules by adding positive literals as rule heads (cf. Charter, Phase 1). For positive conjunctive queries, FO and LP semantics coincide. For queries that involve negation or universal quantification the semantics of FO and LP diverge. C. Extension: RIF Production and Reaction Rule Languages This extends PR condition bodies A.1-A.5 to full rules by adding Production Rule conclusion actions and Reaction Rule events/actions (cf. Charter, Phase 2). D. Evaluation: Use Cases First focus on a subset of the Working Draft Use Cases for A-C (http://www.w3.org/2005/rules/wg/ucr/draft-20060323.html, http://lists.w3.org/Archives/Public/public-rif-comments): D.1 Negotiating eBusiness Contracts Across Rule Platforms D.2 Negotiating eCommerce Transactions Through Disclosure of Buyer and Seller Policies and Preferences D.3 Collaborative Policy Development for Dynamic Spectrum Access D.4 Access to Business Rules of Supply Chain Partners D.5 Managing Inter-Organizational Business Policies and Practices D.6 Ruleset Integration for Medical Decision Support D.7 Interchanging Rule Extensions to OWL D.8 Vocabulary Mapping for Data Integration E. Evaluation: Interoperation/Interchange Experiments by RIF Participants on use cases D for languages A-C: E.1 SBU <-> NRC E.2 SBU <-> NRC <-> DERI E.3 BBN <-> SBU <-> NRC <-> DERI . . . F. Mappings to Other Languages Provide normative mappings to languages discussed in the Charter (order TBD). F.1 RDF F.2 OWL F.3 SWRL F.4 RuleML F.5 OMG PRR F.6 SBVR F.7 ISO Common Logic F.8 SPARQL
Attachments
- text/plain attachment: RIF-Design-Steps-2006-04-23.txt
Received on Sunday, 23 April 2006 18:21:27 UTC