Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha102/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha102/ Alpha release site authentication: User Name: maudeabuser Password: bughunter This is an alpha quality release, to allow users to experiment with a single new feature: linear associative unification. The reason for restricting our attention to linear associative unification problems is that associative unification is infinitary, and quite trivial non-linear associative unification problems have an infinite minimal complete set of unifiers. The canonical example is f(a, X) =? f(X, a) for associate f, constant a and variable X. Single linear elementary associative unification of n variables against m variables has a minimal complete set of unifiers whose size is given by the Delannoy number D(n, m): 1 1 1 1 1 1 1 1 1 1 1 3 5 7 9 11 13 15 17 19 1 5 13 25 41 61 85 113 145 181 1 7 25 63 129 231 377 575 833 1159 1 9 41 129 321 681 1289 2241 3649 5641 1 11 61 231 681 1683 3653 7183 13073 22363 1 13 85 377 1289 3653 8989 19825 40081 75517 1 15 113 575 2241 7183 19825 48639 108545 224143 1 17 145 833 3649 13073 40081 108545 265729 598417 1 19 181 1159 5641 22363 75517 224143 598417 1462563 The central Delannoy numbers D(n, n) grow slightly subexponentially but that is a lot better than inifinity. fmod A-UNIF is sorts List Elt . subsort Elt < List . op __ : List List -> List [assoc] . op f : List List -> List [assoc] . op g : List List -> List . op h : List List -> List [assoc comm] . op i : List -> List . op j : List List -> List [assoc comm id: 1] . op 1 : -> List . ops a b c d e : -> Elt . vars A B C D G H I J K L M N P Q R S T U V W X Y Z : List . vars E F : Elt . endfm unify A B =? X . unify A B =? X Y . unify A B C =? X Y . unify A B C =? X Y Z . unify A B C D =? X Y Z . unify A B C D G =? X Y Z . Simultaneous linear elementary associative unification is just the product of the unfier sets for the single linear elementary associative unification problems since linearity implies they are independent. unify A B C =? X Y Z /\ G H I =? M N . Non-linear problems are explicitly disallowed, and produce an error message: unify A B =? B C . Unfortunately, linear unification algorithms don't combine nicely since purification and the expression of unifiers from other theories (include associativity itself!) trivially introduce non-linear variables. This last point means that a binding generated by an associative unification cannot be revisited (on the same search path) since it now contains non-linear variables. Non-variable subterms are allowed below an associative symbol with a couple of provisos: (1) Each such subterm must be headed by a collapse free symbol. (2) No variable occuring directly under an associative symbol can be mentioned. unify a A a =? B a C . unify a A b =? B c C . unify a A a =? B a C a D . unify a A b =? B c C d D . unify h(A, B, B) C h(G, H) =? I h(J, i(K)) L . unify h(A, B) C h(G, H) =? I h(J, J) L h(M, M) N . unify A h(X, Y) B =? C h(U, V) D h(U, U) G . Because non-free theories introduce non-linear fresh variables for purification and expressing their unifiers, associative symbols may not appear anywhere but at the top of a term or immediately under a free theory skeleton at the top of a term. unify g(h(A, B, B) C h(G, H), X Y a Z) =? g(I h(J, i(K)) L, U b V W) If they occur below an AC symbol for example, the fresh variables introduced to solve the purified AC unification problem are necessarily non-linear (since each variable must show up on each side of the equation) which immediately breaks linear associative unification. In this case a warning is generated and unification fails: unify h(h(A, B, B) C h(G, H), X Y a Z) =? h(I h(J, i(K)) L, U b V W) . Steven