[RIF] Technical Design: IRL-RCL mapping

Hello,

Attached is my contribution defining a mapping from Ilog's Rule Language (IRL)
and Boley et al.'s RIF Rule Condition Language (RCL). This closes Action 22.

-hak
-- 
Hassan Aït-Kaci
ILOG, Inc. - Product Division R&D
tel/fax: +1 (604) 930-5603 - email: hak @ ilog . com

This is in fulfillment of the RIF-WG action 22 on Hassan Aït-Kaci:
http://www.w3.org/2005/rules/wg/track/actions/22 (topic: Technical
Design).

------------------------------------------------------------------------

Mapping IRL pattern-conditions to RIF Rule Condition Language (RCL).

Hassan Aït-Kaci
ILOG, Inc.

(See http://www.w3.org/2005/rules/wg/wiki/A._RIF_Condition_Language.)

IRL RULES

An IRL rule consists of a left-hand side and a right-hand side part. The
LHS consists of two distinct parts: a tuple of object patterns and
boolean conditions. The object patterns contain variables that are bound
by matching objects in the Working Memory (WM). The condition parts
consists of boolean expressions on the variables that get bound by
successful pattern matching. The boolean conditions involve basic
predicates, conjunctions, disjunctions, and negations over pattern
variables and constants.

Pattern matching precedes evaluation of the boolean conditions. Because
all objects in working memory are always ground (i.e., they may not
contain any unbound variables), it follows that verifying a rule's
boolean conditions simply amounts to expression evaluation. In other
words, no logical inference is involved in the process - conditions
simply evaluate to either true or false depending on the variable
bindings provided by the matching phase.

OBJECTS AS FORMULAE

Although, strictly speaking, a rule's object patterns are not viewed as
conditions, they are such since they specify the implicit conditions that
such objects exist in the WM. Thus, pattern matching may be construed as
a logical inference step which either fails (the existence condition
being then false), or succeeds with a binding of the pattern's variables
to values from matching objects in the WM (thus making the existence
condition true).

Therefore, in order to obtain a mapping for IRL's rules into a purely
logical language like the RIF's RCL, we must take the object pattern
matching into account. This may be done by mapping the object model into
logical form. IRL's object model is basically Java's and consists of
attributed class types and object instances. As it turns out, such a
logical rendering of the object model can be formalized as follows:

        (1) types are monadic predicates (e.g., constraining a variable
            '?x' to be of type 'Person' is equivalent to the predicate
            'Person(?x)' holding true);

        (2) subtyping is equivalent to logical implication (i.e., class
            'Customer' being a subclass of 'Person' is equivalent to
            'forall ?x, Customer(?x) -> Person(?x)');

        (3) attribute fields are uniterpreted monadic functions (i.e., if
            variable '?x' has the object 'Person(age = 20)' as value,
            this is the same as the formula 'Person(x) & age(x) = 20');

        (4) pattern matching amounts to proving that the object pattern
            formula implies a WM object formula.

IRL RULES AS CONSTRAINT-GUARDED RULES

With this translation, an IRL production rule's may be seen as a 'guarded
rule' [1][2]. Pattern-matching is formalized as 'feature structure
entailment' [3]. The RHS of such a rule may thus be viewed as:

        Guard | Condition => Action

Where 'Guard' is the formula corresponding to the object pattern after
the above translation has been applied, and 'Condition' is the boolean
expression on the Guard's variable. Informally, the operational semantics
of such a rule is:

        "IF there is a WM object-formula 'Object' such that the
        implication 'Guard -> Object' holds with variable binding \alpha,
        AND \alpha(Condition) = true, THEN perform '\alpha(Action')."

For example, consider the IRL rule:

        rule person_example {
          when {
              p: Person(age > 18);
          }
          then {
                ...
          }
        }

whose RHS requires that a Person object exists in the WM and that
person's age be more than 18. The object pattern here is:

        ?p: Person(age = ?a)

and the boolean condition is the expression:

        ?a > 18

Hence, it is equivalent to the guarded rule:

        Person(?p) & age(?p) = ?a | ?a > 18 => ...

Strictly speaking, such a translation should also involve typing
constraints from the defined class (e.g., the from class 'Person').  For
example, if the class Person defines the attribute 'age' to be of type
'int', such information should be also conjoined in the translation of
the object pattern as a guard. Deciding such implicative guards amounts
to solving a 'constraint entailment' problem for the class of formulae
making up the language of guards. For example, for attributed objects and
classes see [2] and [3] where proof-theoreretic formula simplification
rules are given to decide entailment and disentailment of featured object
guard.

CONCLUSION

In conclusion, mapping an IRL rule's RHS to the proposed RIF Rule
Condition language is achieved by keeping all boolean operators and
translating object patterns as logical constraint guards.

Incidentally, this approach follows the 'objects as constraints' view
that gives a logical reading to any data structure. Basically, a data
structure is a constraint formula. With this view, Prolog terms are also
formulas where unification is conjunction and matching is implication.
Indeed, Prolog = CLP(H), where H is the Herbrand theory axiomatizing
finite trees [4].

REFERENCES

[1] Gert Smolka, "Residuation and Guarded Rules for Constraint Logic
    Programming," in Frederic Benhamou and Alain Colmerauer (Eds.),
    Constraint Logic Programming: Selecte Research, MIT Press Series In
    Logic Programming, pp. 405 - 419, 1993. (See also
    http://www.hpl.hp.com/techreports/Compaq-DEC/PRL-RR-12.pdf.)

[2] Hassan Aït-Kaci and Andreas Podelski, "Functions as Passive
    Constraints in LIFE, ACM Transactions on Programming Languages and
    Systems (TOPLAS), 14(4), July 1994, pp. 1279 - 1318. (See also
    http://www.hpl.hp.com/techreports/Compaq-DEC/PRL-RR-13.pdf.)

[3] Hassan Aït-Kaci, Andreas Podelski, and Get Smolka, "A Feature
    Constraint System for Logic Programming with Entailment," Journal of
    Theoretical Computer Science, 122(1-2), January 1994, pp. 263-283.
   (See also http://www.hpl.hp.com/techreports/Compaq-DEC/PRL-RR-20.pdf.)

[4] Michael J. Maher. Complete axiomatizations of the algebras of the
    finite, rational, and infinite trees. Proc. 3rd IEEE LICS, 1988.
    http://www.lfcs.inf.ed.ac.uk/events/lics/1988/Maher-Completeaxiomatizat.html