- From: Francois Bry <bry@ifi.lmu.de>
- Date: Fri, 12 May 2006 10:16:00 +0200
- To: public-rif-wg@w3.org
To the best of my undserstanding, the RIF WG can learn from Hassan (very nice) brief survey that specifying an Equational Theory for a RIF rule set would make much sense. Hanssan, a warm thank to you for your email. It is a great pleasure to read it and some might, like myself, learn from it. By the way, Hassan, i6t would be *great* if you would spend a few hours on this email you sent us and turn it into a survey on the subject. If this survey would keep the style of the email, then it would be extremely informative and pleasant to read. I have no doubts that such a survey would be easy to publish in a good jopurnal (maybe JAR?). Francois Hassan Aït-Kaci wrote: > > Hello, > > This is regarding dealing with equality in Herbrand models. Here are > some facts that may be known to many but not all among this WG. > > As Michael mentioned, the simplest and most natural way to model > equality in algebraic models is indeed using congruences. Recall that a > first-order Equational Theory (ET) is a conjunction of equations, each > being a pair of functional first-order terms - which may, or not, > contain variables, each pair defining its own (universally quantified) > variable scope. An ET engenders a congruence relation on the term > algebra (the set of Herbrand terms - i.e., ground). Quotient algebras > are formed modulo such a congrence. Unification modulo such a theory in > one way to operationalize specific ETs for which an efficient method is > known (e.g., AC, ACI, Distributive, etc., ... - see the archives of the > UNIF conference for the last 25 years). Theory unification + Resolution > (e.g.) gives a means to have a clean algebraic semantics for several > collection types such as sets (ACI), multisets - or bags (AC), or > sequences (empty theory). Another substantial advantage of unification > modulo is that it is more efficient that using equational rewriting and > even converges where rewriting would diverge - e.g., for commutativity). > > Anyway, all this take its roots in the works of Knuth and Bendix (KB) > (1970). In their seminal paper, they address the problem of computing > modulo an equational theory. Basically, each element in the quotient > Herbrand model is a set of Herbrand terms all congruent modulo the > equations. The best way to deal operationally with a congruence class is > to find a way to compute a unique canonical representative of the > class. KB proposed using equations as rewrite rules. Namely, given a > Herbrand (i.e., ground) term and an equational theory, this term may be > reduced to normal (or canonical) form by repeatedly rewriting it > replacing any part of it that matches the LHS of an equation with > substitution \sigma by the RHS\sigma. To do so and not run into circles > (think of commutativity) one needs to "orient" the equations (i.e., turn > "t_1 = t_2" into either "t_1 -> t_2" or "t_2 -> t_1"). If this can be > done in such that simplifying from left to right is done according to a > well-founded ordering on the Herbrand terms for this signature, and if > such an ordering is at hand, then the famous Knuth-Bendix completion > algorithm is a semi-decidable procedure to compute a complete and > confluent set of rewrite-rules for an equational theory. Note that the > KB algorithm is parameterized on the term ordering that orients the > equations. In their original paper, KB themselves proposed a clever > term weighing ordering, where the weights of terms were computed from > those weights on function symbols in some clever way as to give lesser > weights to the "simpler" side of an equation if possible. Better term > orderings were proposed later, most notably the Recursive Path Ordering > based on multiset orderings (Nachum Dershowitz) and later extended and > improved into the Recursive Decomposition Ordering and Path of Subterms > Ordering by the Nancy Equation and Rewrite Rule School (Jean-Peierre > Jouannaud, Claude and Hélène Kirchner, Pierre Lescanne, Michaël > Rusinovitch, etc., ...). Again, look up each conference such as RTA, > UNIF, CADE, LPAR, ... in the last 25 years. The KB completion method was > later extended to using unification modulo theory for theories that have > such an algorithm (ACI, etc...), and even further to using general > constraint-solving rather than just Herbrand-term unification in > computing so-called critical pairs (the heart of the KB procedure which > consists of finding two potentially conflicting rules by successful > superposition of a pair of subterms, each from a different rule's LHS, > using unification). Indeed, Herbrand-term maching and unification are > but specific instances of constraint entailment and conjunction, > respectively. Since the critical pairs computed by the KB method by > unification denote intersection of the set of ground instances of the > unified terms, one could replace unification by any complete > constraint-solving method checking the consistency of the conjuction of > two constraints since a solved form for the conjunction denotes the > intersection of the solutions of each. And so was the KB completion > further extended using general constraint solving rather than just > computing Herbrand substitutions (which happen to be solved forms for > the particular constraint system of conjunction of equations among > Herbrand terms). These extensions were done by the Kirchners in the > 1990's in Nancy, France. More recently, Claude Kirchner also extended > term-rewriting (using just Herbrand matching) into constraint-driven > rewriting (by replacing terms with constraints and matching with > constraint entailment) - the \rho-Calculus. > > [Incidentally, the KB method is also just an instance of a larger family > of decision procedures based on subterm superposition. E.g., > Buchberger's algorithm is the analog of the KB method in Polynomial > Ideal Algebra.] > > Back to reasoning with equality in Herbrand models ... > > If one is given an equational theory for which a complete and confluent > rewrite rules is available (as produced by the KB method, for example), > one acn then operationalize reasoning modulo such a quotient Herbrand > model (i.e., dealing with syntactically different but semantically equal > terms). Thus, the most general method to do automatic reasoning in FOL > modulo an equational theory while still having a clean declarative > quotient model semantics, is Equational Narrowing ("Surréduction", en > Français). Basically, Narrowing is Term-Rewriting using unification > instead of matching ("filtrage", en Français). This has for effect to > allow inverting functions, whereas Rewriting cannot. For example, take > the one-equation theory: > > f(a) = b. > > which gets oriented as: > > f(a) -> b. > > With matching, this can only rewrite the term "f(a)" to "b". Therefore, > reasoning using rewriting solves the equation "f(b) =?= a". However, > since Rewriting uses only matching cannot solve more general equations > with variables in position arguments such as "f(Y) =?= a" since no term > in this equation matches any rule's LHS. However, Narrowing uses > unification and can solve any such equation (provided the set of rules > in complete and confluent and the subterm selection strategy - e.g., > innermost/outermost - is complete). Indeed, Narrowing, thanks to > unification, allows "guessing" the argument (thus effectively inverting > the function) whereas matching does not. Because of this power similar > to that of resolution-based model of computation exhibited by Prolog, > and its pure model semantics, Narrowing has been adopted as the choice > computational method by a growing family of Functional Logic Programming > languages (see, to name just one, the Curry language and the work of > Michael Hanus). > > Another method for dealing with ET's is not by using Narrowing which may > be costly (as in Prolog, to be complete, general Narrowing is not a > non-deterministic procedure since equations may have several solutions - > e.g., inverting a non-injective functions). If one wishes to retain > determinacy of function reduction while allows Herbrand unification of > terms containing both constructors and interpreted function symbols, > where such interpreted symbol are defined by rewrite rules, then one can > use "residuation". It consists of delaying solving an equation as long > as an interpreted function has all its arguments instantiated enough to > match (rather than unify with) a rule's RHS. This method is used by the > Functional Logic Programming langage LIFE that I have designed and > developed with colleagues over several years (LIFE stands for Logic, > Inheritance, Functions, Equations). Using residuation vs. narrowing has > the advantage of keeping functional reduction determinate at the expense > of being an incomplete equation solver (since it does not invert > functions). However, it allows more declarative logic programs (since > order of unification is unimportant, one can change prohibitively > inefficient generate-and-test logic programs into surprisingly efficient > test-and-generate programs simply by inverting the order of constraints > and value labeling - the equations delayed by residuation in the test > phase (still missing there value labels) act as powerful search space > pruners. So we prefer LP with equality using residuation rather than > narrowing because it is more declarative than Prolog (which cannot deal > with syntactically different but sematically equal terms) and more > efficient to boot! [In other words, as my late father used to say, "I'd > rather be wealthy and healthy than poor and sickly! ..." :-)] > > Thank you for your attention. > > -hak > > > PS/ I did not put any links or given any specific references, but used > enough buzzwords and cited enough names for anyone to use on Google > for more information of any notion or person mentioned in this > message... :-) > >
Received on Friday, 12 May 2006 08:16:09 UTC