This is an archive of an inactive wiki and cannot be modified.

A Constraint-Logic Programming (CLP) Formulation for a Rule Interchange Format (RIF) Extensible Design

HassanAitKaci hak@ilog.com ILOG, Inc.

Contents

  1. A Constraint-Logic Programming (CLP) Formulation for a Rule Interchange Format (RIF) Extensible Design
  2. CLP Formulation
  3. A Core Logical Calculus
    1. Hereditary Harrop Formulae
  4. Effective Rule Interchange
  5. Glossary
    1. Entries

This a suggested amendment to the original RIF Extensible Design Proposal (from here on RED.0) submitted to the W3C RIF WG by HaroldBoley et al., from the REWERSE Group. Its purpose is to reconcile the contents of what was proposed by this author's email message in fulfillment of ACTION-87 with RED.0 (see also ACTION-163 on HaroldBoley):

  1. to reformulate the aforementioned REWERSE proposal using a slightly more general scheme based on Constraint Logic Programming;

  2. to characterize the proposed extensions to the basic technical design using proof-theoretic concepts in formal adequation with its model theory;

  3. to propose a methodology based on the thus-reformulated proposal that could lead to designing an effective Rule Interchange Format using known formal reasoning techniques compatible with extant W3C formalisms (XML/S, RDF/S, OWL, ...).

Point (2) above is essential since issues of semantics have been approached so far mainly through a model-theoretic viewpoint. As relevant as this may be for a RIF to be well designed and understood, it is perhaps as important, if not more, that one may operationalize the RIF by characterizing its computational as well as it denotational semantics.

CLP Formulation

The RIF Charter clearly stipulates that Horn Rules (HRs) should be considered as a first attempt to enable rule interchange. The rationale for this presumably being that, since several LP systems are more or less loosely based on HRs, it would be sensible to start first with exchanging Horn Rules. Be that as it may, this imposes a design constraint on the RIF WG. This constraint was addressed by RED.0: its most basic contribution is a RIF Condition Language (RCL) encompassing a class of formulae thought to be common not only to Horn Rule systems alone, but also to a large set of Rule Languages of the kind this WG's members have in mind - e.g., Production Rules, Reactive rules, ECA Rules. The authors of RED.0 proposed extensions (RED.1) to the basic design including a richer family of condition language (e.g., accommodating explicit existential or universal quantification, two kinds of negations - NOT and NAF, etc...), and a Horn Rule language (HRL) using condition expressions expressed using the (full or partial) RCL language. The core kind of rules that the RIF will be used to represent has already been recognized (whether for Phase I or Phase II). Indeed, the RIF Charter has made the choice to focus first on Horn Rules, then extend the scheme to Production and Reactive Rules. So, focusing on Horn Rules alone, RED.0 proposes a specific family of logical (condition and rule) languages, including - of course - Horn Rules. Although this is a sensible approach, I personally think that "Horn Rules" is too complex a concept making several undue assumptions.

For starters, it forces a specific data model (viz., Herbrand terms) where such a data model should be abstract at this level. While it can be easily agreed that, indeed, Horn Rules make up a substantial bulk of rulesets that would be interchanged through the RIF (e.g., all extant Prolog systems), many rule systems do not use this data model (e.g., production rule systems, reactive rule systems, and even some logical rule systems such as LIFE). I contend that there is no need to set the level of abtraction so low as to systematically "build in" Herbrand terms into a rule system whether relevant or not. Instead, a formal scheme that encompasses, among others, Horn Rules (i.e., Definite Clauses over Herbrand Terms), but also other deductive rule systems based on Definite Clauses over data models.

In fact, such a formal scheme exists: Constraint Logic Programming (CLP). I claim that it lies at a better level of abstraction than Horn Rules in that:

  1. it allows dealing with a wider set of rules,
  2. it does not demand a commitment to any specific data model, while
  3. it covers Horn Rules as a simple instantiation of the constraint component of the scheme to equations over Herbrand Terms.

Indeed, the main idea behind CLP is to abstract the data model from the rule scheme using (logical) variables as the interface between the world of Rules and the world of Data. Please refer to the CLP scheme's technical summary I am providing as attachment to this for a better idea.

Thus, this suggests that, rather than a 2-part entity (a RHS and a LHS) over arguments from a specific data model, a better rule representation is a 3-part entity consisting of the two sides together with a constraint. Viz., the simplest and most general rule is made of: 

   Atom :- Goal | Constraint.

where:

Instantiating the nature of the constraints to specific forms yields specific rule systems over specific data models:

Using CLP to express rules gives a better level abstraction in that:

  1. The semantics of a ruleset is parameterized with that of the constraint system expressing the data model and is inherited for free with preciously little that need be assumed by the data model.
  2. This clean separation of concerns between rule and data allows a modular approach to classifying rule systems.

  3. Going beyond Definite Clauses (which deal only with conjunctions of positive retational atoms) is also possible as it is for classical Horn Rules, by extending it with negation, disjunction, and nested quantification (i.e., as was proposed for the Core RIF Condition Language).

Indeed, abstracting the data model as constraints alleviates the need for ad-hockerry even for sorted or typed objects which may thus use the logical reading of constraints as an effective means to formalize logically non-logical RL features such as graph pattern-matching.

A Core Logical Calculus

Basically, RED.0 starts with a basic CORE logical language, starting with Basic Positive Conditions, and then extending the design with Horn Rules. Presumably, such a design will be extensible in the sense that shall enable extensions to richer calculi meant to capture features of other kinds of rules besides Horn (see Phase II).

What we propose is similar in that:

The logic in question is that of Hereditary Harrop Formulae (or H2F for short).

Hereditary Harrop Formulae

Informally, an H2F may be viewed as a Horn Clause whose body may be extended with:

  1. Universally quantified goals
  2. Implications

Operationally, the first extension amounts to solving a goal with locally scoped variables, and the second amounts to making a temporary assumption while proving a goal. Such an H2F (also called an H2 goal) is characterized syntactically by the following (partial) BNF rooted at Goal: 

Goal
   : Atom
   | Goal '/\' Goal
   | Goal '\/' Goal
   | 'Exists' VAR Goal
   | Knowledge 'Implies' Goal
   | 'Forall' VAR Goal
   ;

Knowledge
   : Atom
   | Goal 'Implies' Atom
   | Knowledge '/\' Knowledge
   | 'Forall' VAR Knowledge
   ;

H2F have nice proof-theoretic properties such as being computable by a Basic Sequent Calculus. A Proof Procedure for the Logic of Hereditary Harrop Formulas. Gopalan Nadathur. Journal of Automated Reasoning 11: 115-145, 1993.

Note that the above language is close to the full RCL extensions in RED.0. Like the latter, H2F allow atoms, disjunctions and conjunctions, existential and universal quantification. (In fact Existentials and Disjunctions can be eliminated).

Unlike it, it does not include negation, but allows implications. Note however that in H2F implications are supported in goals. This allows for hypothetical reasoning and thus modelling of such features in Production and Reactive Rules that are at odds with the static world semantics of F.O. Model Theory. Indeed, it may be argued that, although conforming to Phase I, some commitments may be "hard to undo" to accommodate more operational and not purely model-theoretic features such a mutable state, reactivity, etc., needed to express the semantics of some rule systems. It is here suggested that H2F offer a better hinge of abstraction for expressing a notion of Rule as Logical Formula.

In addition, the H2F calculus is amenable to a CLP formulation of Constrained Rules over parameterized data models expressed as constraints, just like basic Horn Rules. For example, efficient handling of multiple nesting of quantifiers is elegantly formulated as a constraint-solving process known as Labelled Unification.

Effective Rule Interchange

Model Theory is great to express immutable truth. Other formal logical formalisms are better suited to express change and other non-model theoretic notions. We stress here the operational approach of Proof Theory vs. Model Theory not to infuriate most of this WG's members :-? but rather to keep in mind the fact that eventually the RIF is about systems that run.

I have a nice funny story as a metaphor for not using Model Theory for purposes that it is not meant for:

Using Model Theory for, say, Production Rules, is akin to looking for the keys under the light where they are not!

There are many critical features that are needed by actual rule systems meaning to use the RIF. Here are some non-model theoretic features of rule systems addressed by H2F:

[TO BE COMPLETED...]

Glossary

Here are some definitions making some important concepts of our technical vocabulary more precise. It is mostly empty for now, but it will be populated with appropraite links as time goes by as as this document evolves. For now this glossary is intended to be for internal WG use. Don't worry about making it make sense outside. Later on we can rework it for inclusion into a publication, if we want.

To add an entry:

  1. Edit this page, adding your term to the list like ["Some Term"] (unless it happens to be a WikiName)

  2. Click on the term to follow the link
  3. You should get a message about the page not existsing

  4. Select "GlossaryEntryTemplate" from the list of page templates

  5. Fill in the new page as much as you like. Others may then notice and refine the entry.

Entries