Associative Commutative Pattern Matching

ASSOCIATIVE COMMUTATIVE PATTERN ~ATCHIN�

J,M, HULLOT IRIA-LABORIA

Domaine de VoZuaeau 78150 - ROCQUENCOURT FRANCE

Plotkin [10] has opened the way to the design of unification alRorithm i ncorporating equality axioms and their use in complete proof systems. In particular he gives ~omplete unificati 0n al­ gorithms for terms containing associative function s~hols and for an arithmetic theory . Huet gives in [18] a unification algorithm for ~-conversion and discusses in [19] Reneral prop ~rties of complete set of unifiers. A complete and finite alRorithm for unification with associative commutative function symbols is given in Stickel [14] and Lanyford shows in [22] how to extend it to abelian group theory. Various other specific unification problems are di scussed in [ 9,15, 23], In the case of equational theories which possess a complete set of reductions as de f ined in Knuth-Bendix [7], Fay has given in [20,21] a general unification algorithm,

We are interested in this paper in the special case of commutative associative fun~tion symbols, We first study the equivalence problem which is reduced to regognizing the equal i ty of two multiset representations. In the same way, matching reduces to generating ordered partit i ons of a multiset, This generation is carried out by two processe~ operating on tree data structures spanning the lattice of partitions. Cardinality conditions inherited from the matching pr0blem are used to cut the search drastically : our processes operate bidirectionnally in a corout i ne mauner, each one trimming sub-structures from both search spaces. The two processes are formal­ ly defined by a unique recursive definition, and their computations correspond to a call-~y­ need interpretation of this definition. The correctness of the method is proved formally. This basic organization is used to derive a new algorithm for associative commutative unification improving over Stickel [14]. 1'~e have programmed in LISP all these algorithms, using 11niversity of Vincennes's V-LISP system [3], We have applied them to the Stickel-Peterson's generali:!:ation of the Knuth and Bendix extension algorithm [7,8,16], Their alp.orithm relies on associative­ commutative unification for the computation of critical pairs, hut also most critically O il as­ sociative-commutative match, in order to reduce terms to their normal forms. ~tickel and Peterson proposed to use unification for matching, hut this leads to unnecessary inefficienci es that preclude the practical use of their method, Fe give in the Appendix running times on a DEC KLIO using the VLISP system, correspondinp, to some of their examples,

Most proofs are omitted in this version, the full paper is available as a techn i cal report [24],

I, FIRST ORDER TERMS AND EQUATIONAL THEORIES

Let V be a denumerable set of elements called variables, C a finite or denumerable set of elements called constants with Cnll·~. Ele­ ments in C are graded by an arity function a:C~N. The set of terms T is the smallest set containinp, V and closed by :

t 1 ,···,ta(f)€T + f(t 1 ,···,ta(f))€T ror every f€C A substitution is a mapping o from V to T, with o(x)=x almost everywhere. For any t €T, ll(t ) will denote the set of variables of t. An equati onal theory~ is a theory in which every axium i s the universal closure of an equality. Two terms t 1 and t 2 are equivalent in A iff : Ai-t 1 st 2 · In the remainc'ter we will write t 1 lt 2 or t 1 : t 2 when A is implicit. Let AcC with A·{f 1 ···fp} where Vi l~i~p fi is binary and fi i s an assoc i ative and commutat i ve function i.e. a) f. (x,yl:f. (y,x)

1 1

and 8) f.(x,f.(y,z))·f. (f.(x,y),z), The equal 1 1 1 tional theory of f 1 ···fp is the theory with the 2p axioms a and 8. In the remainder of this pa­ ger A will always denote the theory of f 1 ,···,fp. All terms will be in right associative form, A term t·f.(t 1 ,f.(t 2 , ... ,f.(t 1 ,t )oo·))where tk 1 1 1 n- n does'nt begin with fi is called NF-term, Ve shall abreviate such a term by f.(t 1 ,···,t ), If 1 n t·fi(t 1 ,···,tn)' O(t) will denote n.

II, EQUIVALENCE

II,I Equivalence lemma

Let T,T' be two NF-terms with head symbol fi i.e. T·fi(t 1 ,···,tn) and T'·f.(t',···,t'). Then T~T' iff n-m and there 1 I n exists a permutation n of m such that t ( . ) = t! (I s ism) · 'IT 1 1

~ : see [24].

II.2 Equivalence algorithm-EQtTIAC (t,t')

Let us now describe an equivalence al­ gorithm between terms in A. We call unificand a finite set of pairs of terms. Unificands are de­

noted by N,N 1 ··· ,

We describe this algorithm as the cons­ truction of a tree whose nodes are either a uni­ ficand consisting of pairs of NF-terms or 0 for success or(!}for failure. We first define SIMPL(N) which simplifies a unificand N Sit-fl'L(N)

Termination :by induction on< r,> N S(e), 0 e,e €

Let e·fi(t 1 ,··· 1 tn),e'·fi(t;,···,t'n)' the function Permu(e,e') given below returns a fini­ te set of unificands

11here{ 'IT .. ·'IT 1 }· set of all permutations of -1 n. {I , .. ·, n}.

The tree for <t,t'> is grown as follows

• if a node is 0, the construction is interrup­
• ted q:z:it !rut>
• to grow the successors of node N, select in N an arbitrary pair : <e,e'>

If e(e)+e(e') the only successor of N is<E), else Permu(<e,e'>) returns a finite set of uni­ ficands N.· For each Ni grow an are from N toNi 1 where

If the construction stops and all leaves are~ exit False · The equivalence lemma proves the correctness of the method.

II.3 The heuristic part

In the implementation of the equivalence al­ gorithm we do not generate all permutations for two given terms. Some structural remarks allow us to reduce the search space, The following ex­ ample shows the behavior of our algorithm.

Without loss of generality we generate now only those permutations n such that if <t.,t (')>is 1 'II 1 part of a resulting unificand, then SIMPL(<ti,tn(i)>)p{!). Thus, since SIMPL( <xI ,f 2 (b ,x 3 ) >)..(!)and SI~L(<x 1 ,f 2 (a,x 2 )>)·(!) there are only two successors :

To grow the successors of node N 1 select the first pair of NJ: say <f 2 (x 2 ,a),f 2 (b,~>, Since SIMPL(<x 2 ,b>)·QU and SI~L(<x 2 ,x 3 >)·~ 1 the only successor of N 1 is {!). To grow the succes­ sor of N 2 select <f 2 (x21a),f 2 (a,x 2 )> since SIMPL(x 2 ,a)·(!) the only successor of N 2 is N 3 ·<f 2 (b,x 3 ),f 2 (b,x 3 )>, In the same way 0 is the only successor of N 3 and the construction ter­ minates successfully.

III. MATCHING

III,I Definition

Let H be a finite sequence of subsets of a set N (resp.a multiset N), H·(A 11 ··· 1 An)' A.cN, m~l, A.p0. We say that M is an ordered 1 1 partition of N iff UAi ·N and A.nA.·0 for ipj I sisn 1 J

(resp.l:jA. ·N where l!Jdanotes union for lsi!m multisets).

III.2 A complete matching algorithm

We can extend : to substitutions by defining cr:cr' iff ~t€T crt:a't. s is a complete set of matches of <t,t'> iff S is consistent 0tcr£S,t':crt) and S is complete 0ob such that t':crt, 3cr'£S1 3 ~substitution with (cr~rV(t)):cr') where (crtv)(x)·a(x) if X€V and x otherwise), As for equivalence we shall construct a tree whose nodes are either a unificand or 0 for success or G) for failure. We first define Sil-fl'L 1 (N) which simplifies a unificand N.

Termination : as for equivalence, 0

Let e·f.(t 1 , .. ·,t) and e'·f.(t' 1 ,··· 1 t 1 ) with 1 n · 1 m m~n. The function PART(e,e') given below returns

a finite let of unificands,

Let ! ·{ordered partitions of the set m {t' ··· t'} inn non empty blocks}·{P 1 ···Pq} I' 'm where Pi are the partitions. Thus P.·{T.(I)···T.(n)} where T.(j) are the elements 1 l 1 1 1 of the partition. Then we define tk·Tk(l) if ITk(l)l·l and ~-fi(T 1 ,···,Tr) if Tk(l)·{T 1 ···Tr} with r>l, We define PART(e,e')·{{<t 1 ,t>,···,<tn,t7>} ltsisq}.

The matching tree MT for <t,t'> is grown as follows :

• -the root node is N 0 ·SI~L 1 (<t,t'>), We set a ·0 No
• node (!) is a leaf
• to grow the successors ot node N, select in N an arbitrary pair <e,e'>

if e€V then if oNe is undefined

then grow an arc labelled with <e,e'> from N to N'=N-{<e,e'>}, Set crN,·<e,e'>ucrN else if EQlliAC(e',crJIIe) then grow an arc from N to N-{<e,e'>} labelled by the empty substitution t(~N-{<e,e'>})

else grow an arc ~ (D

else 1:f B(e')<fl(e) then (lrow are N~®

else the function PART(e.e') returns a

The set of matches of t,t' is S·{oNIN=0 in~} The correctness of the algorithm is given in [24].

Remark!: As for equivalence, some structural conditions allow us to reduce the search space (using SIMPL 1 instead of SIMPL), Thus we use the function PART only when the left term has only variables as arguments.

Remark2 : One may define the function PART in using the concept of ordered partitions of a multiset, Such an improvement can be found in [24].

Let us now give an efficient way to Renerate or­ dered partitions of P set.

IV, THE UNDERLYING DATA STRUCTURE

We give in this part a basic algori­ thm which can be used to :

• generate ordered partitions of a set (detailed in ex&mple I) or a multiset (aee r24])·
• generate ordered partitions of sets or multi­ sets with cardinality constraints on the blocks (see [24])·
• -improve over Stickel's unification algorithm (see example 2 and [241 for more details),

IV,I The Basic problem

Let x·x 1 ···xn and y·y 1 ···yn be two bi­ nary vectors of size n. We define the partial ordering relation P 1 on binary vectors hy xP 1 y iff Vi ~x .~y. and 3jsuch that x.;y .· We define 1 1 J J P 0 by xP 0 y iff yP 1 x. A graph of the partial or- Throughout the remainder of this paper P 0 and P 1 will denote two predicates on binary vectors such that :

Our aim is to rlesign an algorithm for ~enerating this subset of all l·dl"Ary "ectors of size n such that p 0 (x) · True and p 1 (x) · True.

Example I : Let M be a binary vector of size mxn, M·h oo·h with h.·h. oo·h. where h .. is Oorl I n 1 1, I 10m 1tJ Let v. be the binary vector of size n, J vj·ht,j'''hn.j' We define predicates q 1,q2,q3 by :

and predicates P 0 and P 1 by P 1 (M)·q 1 (M)~q 2 (M), P 0 (t-')·q 3 (M). The set of all ordered partitions of m elements into n blocks is represented by {Mip 0 (M)·True and p 1 (M)·True} in the following . . h . th 1 . . h . th 1nterpretat1on : t e J e ement 1s 1n t e 1 block iff h .. ·1. Furthermore p 0 (resp.p 1 ) has 1tJ property A 0 (resp.A 1 ).

Fxample 2: Let M·z 1 ···zn a binary vector of size n, M 1 ···Mp some fixed such vectors and M. "'~' · some of the r·.(qsp). IJe define 11 1q 1

L<M)· number of I in M. and predicates , 0 and P 1 by B 0 (M)·True#Vi.tsi.sq. L(Mi\Mi.)st and J J J p 1 (M)·True#Vi tsisp Mi\Mi"O· p 0 (resp. p 1 ) has property A 0 (resp. A 1 ). A reader familiar with Stickel's unification algorithm [14] will reco­ gnize the basic situation of the second part of this algorithm (see [24] for more details),

IV,2, The algorithm is first conceived as a se­ quence of two passes that happen one after the other. It is then elaborated by stepwise refine­ ment in ordP.r to produce the final version. In the first pass we search only those binary vec­ tors such that ~(x)·True. We may use the search method of Balas [I], This method is equivalent to scan the combinatorial data structure called binomial tree (Vuillemin [17]) considered as a spanning tree of the graph for P 1 defined above. Binomial trees are defined by :

The B3 binomial tree T 1 associated with P 1 is pictured in Fig,2.

If for some x.p 1 (x)·False we do not have to scan the subtree rooted at x since p 1 (y)·False for ally in this subtree (property A 1 ), Similarly. we generate those binary vectors such that p 0 (x)·True. in using the binomial t~ee T 0 asso­ ciated with P 0 (T 0 is the same as T 1 except that if x·x ···x is the label of node h in T 1 · I n y·(t-x 1 )···(1-xn) is the lahel of node h in T 0 ), The final set of solutions S will be the inter­ section of these two sets. The most ahvious source of inefficiency of this al~orithm may be viewed on the followin~ example : assume n-3. P 0 (tOO)·False and begin to scan T 1 · Since. in this first pass. we do not know that the sub­ tree of T 0 rooted at IOU must be eliminated we have to test P 1 for the 4 corresponding nodes, n'.3, Our refinement will consist in generating S by an algorithm which does not begin to test P 0 or P 1 for a node x until all fathers of x in T 0 (resp. T 1 ) have been t·ested for P 0 (resp. P 1 ) . To achieve this aim. we shall represent the two bino~ial trees as one binary tree.

Let C and C' be two labele~ B binomial p trees. We define CIC' as ~ollows For any binary tree R. we define its set of oc­ currences O(B) as a finite subset of {0.1}* and the subtree of B at u denoted by B/u by : - if B·O (only the root) then O(B)·{A} and B/A·B if BA then O(B)·{t.}u{O·ulu~O(B 0 )}u B 0 B 1 {l·ulue0(B 1 )}and B/A·B· B 0 /u·B/O·u.B/I·u·R 1 /u, Thus. any occurrence u is either A or u · father(u). last(u) where father(u) is an occur­ rence and last(u) is 0 or I identified respec­ tively with False and True, Conventionnally we define last(A)·O.

~ : There is a bijective mapping from the occurrences of length n onto the labels of the non terminal nodes of the binary tree of depth n+l T 1 eT 0 · Its expression is given by : h label(u)·u·b where b· llast(u) and h=n-lul. ~ : in [24].

We C: cfir.e R .. {,_,lwdO.I}* lwl·n}, The definition n of label is extended to R by : Vw€R label(w)-w, n n Furthermore. we define :

Set · {wER ltree(w)} n n

where Vu such that lul~n

tree(u) if uEA then p(On.False)

else if tre~(father(u))

then p(label(u). llast(u))

else False.

where p(w.True) .. p 1 (w) and p(w.l"alse)·p 0 (w),

Theorem : Vw€Rn tree(w)~p 0 (w) and p 1 {w)

~ : see [24],

Our algorithm is conceived as a call hy need in­ terpretation of the recursive definition of tree, The theorem proves the correctness of this al­ gorithm.

V, GENERALIZATION OF THE KmJTH-BFNDIX ALGORITHM

It is not our purpose to present the basi~ Knuth-Een~ix's algorithm (see [7] and [6] and its generalizations ([8].[16]), Our aim is to apply our algorithms to the Stickel-P~terson's generalization of the Knuth-Rendix's extension ' algorithm. Their algorithm relies on associative­ comm~tative unification for the computation of the critical pairs. but also most critically on associative-commutative match in order to reduce terms to their normal forms. Stickel and Peterson proposed to use unification for matching. but this leads to unnecessary inefficiencies that preclude the practical use of their method. With our match algorithm a reasonable implementation is possible as shown in the Appendix where we give detailed running times on a DFC KL-10· using the V-LISP ~ystem ([3].[4]). corresponding to some of their examples,

VI, CONCLUSION

We have presented in this paper a new mat­ ching algorithm in term structures containing associative-commutative function symbols, Our experiments carried out on Stickel-Peterson's generalization of the Knuth and Bendix algorithm have shown that this algorithm together with our improvements over Stickel's algorithm provide an efficient way to implement large systems that deal with associativity and commutativity, For example we ~elieve that the multiset matching algorithm obtained is efficient enough for the practical implementation of pattern directed invocation of procedures with multiset varia­ bles (Q-LISP [11.12.15]),

Furthermore we hope that the techniques used here for the description of our partition generator can be extended to other graph algorithms,

Acknowledgements : This work is part of a thesis conducted at LRI. University Paris Sud. I would especially like to thank my supervisor G. Huet who has contributed to many ideas presented here.

I would also like to thank J, Chailloux and

P. Greussay (University of Vincennes).

Appendix

We wrote a commutative associative extension algorithm as a 1500 line LISP program. It runs interpre­ ted under the V-LISP system [3] on a DF.C KLIO computer. with 1500 storage cells, We give the same examples as in Stickel-Peterson rl6], We have two versions for simplification : inside-out and out­ side-in. The former is more efficient. hut uses more memory and therefore the latter may be prefera­ ble for large examples. The versio~ used is indicated in Fig.4. where u 1 (resp,U 2 ) denotes Stickel's unification algorithm with (resp.~thout) our improvement and ~ 1 (resp.~ 2 ) denotes matching where our algorithm (resp. unification) is used,

References :

• [I) E. BALAS: "An additive a l gorithm for solvin~ linear programs with zero one variables". Op. Roo. 13 ( 1965).
• [2) V.J. BOW/IAN & J.H. STARR : "Partial orderingl in impli­ cit enUD!eration" An. of discr. math. 1 (1977).
• [3) J. CHAILLOUX : VLISP 10.3 manuel de rfffrence Uni. Paris 8, Vincennes (1978). '
• [4) P. GREUSSAY : "Contribution 1 la dEfinition interprHa­ t i ve et .a 1 'implfmentation des lambda-lanaagea,.. Thfae n 78-2, Paris 7(1977).
• [5) G. HUET : "An algorithm to generate the basi· of solu­ tiona to hoa\Ogeneous linear diophantine equations". Inf . Proc. Let.7, 3 April 78.
• [ 6) G. HUET : "Confluent reductions : Abstract properties and Application· to tenn rewritin~ systems" In J't'oc. of the 18th Symposium on FOCS (1977).
• . [7) D. E. KNUTH & P.B. BENDIX : "~imple vord problems in uni­ versal Algebras". In Leech, J.(Ed . ), Col"p. problema in Abstract Algebras. Perga11101on Press, 1970.
• [8) D.S. LA!/KF()RD & A.M. BALLANTYNE : "Decision procedures for simple equational theories with commutative-associa­ tive axioma : co~lete sets of commutative associative reductions''. Tech. rep. MAth. dept. U. of Texas at Austin, ATP 39 (1977).
• (9] M. UVESEY & J. SIF:KJ.IMIN : "Unification of A+C-terma (hags) and A+C+I-terms (sets)". Int. Ber. Nr 3176, Inat. fur Inf. I, Universitat ~~rlsruhe.
• [10 l G. PLOTKIN : "Building in equational theories" In l'elt­ z~r & Michie(Ed) Machine Intelligence 7 ~dinburgh University Pr··· 1972. 1
• [I r l R. REBIJH & E. SACERDOTI : "A oreliminary Q-LISP l'anual". Tech . note 81, SRI, Menlo Park, 1973.
• J.F. RULIFSON, J.A. DERKSEN~ R.o! . W.4LD!NGER : "llA4 : a procedural calculus for intuitive reasonning''. ·Tech. Note 71, SRI, Menlo Park, 1972.
• [13) .!.R. SLAGlE : "Automated Theorem proving for theories with simplifiers commutativity and assoc i ativity", J, ACM 21,4 (1974).
• [14) M.E. STICKEL : "A complete unification algorithm for as­ sociative-commutative functions". Proc. of the 4th IJCAI Tbilisi (1975).
• [1 5] M.E. STICKEL : "Unification algorithms for artificial intelligence languages" Ph.D. Carnegie ~ellon, Pittsburgh, Penn (197~).
• M.F:. STICKEL & G. E. PETERSON: "Complete sets of reduc­ tions for equational theories 11 1J. of Arizone. Techn. Report ( 197a).
• J. VU:LLEMIN : "A data structure for manipulating prio­ rity queues" C. ACM Vol 21 (4)(1978).
• [18) G. HUET : "A unification Algorithm f or typed ~ -calculus" 1 Theo. Com. Science I (1975).
• G. HUET: "Resolution d'fquations dans les langages d'ordre 1,2,···,w': Thhe d'Etat II. Paris VII ( 1976).
• [ 20) M.,r. FAY : "First order unification in equational theo­ ries"Tech. Report N-78-5-002 U. of C·lifornia ~"nta-Cruz (1978).
• M.JFAY : "First order unification in equational theories!' Fourth Workahop on automated deduction ~ustin Texaa(1979~
• [ 22) D. LANKFORD : "A unification algorithm for ahelian p,roup· theory"Report MRP1. Dep. of !lath. Louisiana Tech. tJni.
• [23) M. LIVESEr, .:. SIECY.MANN, P. SZABO, F. U/IVEPEf.HT : l'nifi:.. cation problems for combinations of associativity, com- · mutativity, distributivity and idempotence axioms. Fourth Workshop on automated deduction. Austin Texas Feb.(l979)
• [24) J.M. HULLOT : "Associative-cOII'allutative pattern matching"' Report IRIA-LABORIA to appear (1979).