(*^ ::[automaticGrouping; currentKernel; fontset = title, inactive, noPageBreakBelow, nohscroll, preserveAspect, groupLikeTitle, center, M7, bold, L1, e8, 24, "Times"; ; fontset = subtitle, inactive, noPageBreakBelow, nohscroll, preserveAspect, groupLikeTitle, center, M7, bold, L1, e6, 18, "Times"; ; fontset = subsubtitle, inactive, noPageBreakBelow, nohscroll, preserveAspect, groupLikeTitle, center, M7, italic, L1, e6, 14, "Times"; ; fontset = section, inactive, noPageBreakBelow, nohscroll, preserveAspect, groupLikeSection, grayBox, M22, bold, L1, a20, 18, "Times"; ; fontset = subsection, inactive, noPageBreakBelow, nohscroll, preserveAspect, groupLikeSection, blackBox, M19, bold, L1, a15, 14, "Times"; ; fontset = subsubsection, inactive, noPageBreakBelow, nohscroll, preserveAspect, groupLikeSection, whiteBox, M18, bold, L1, a12, 12, "Times"; ; fontset = text, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 12; fontset = smalltext, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 10, "Times"; ; fontset = input, noPageBreakBelow, nowordwrap, preserveAspect, groupLikeInput, M42, N23, bold, L1, 12, "Courier"; ; fontset = output, output, inactive, noPageBreakBelow, nowordwrap, preserveAspect, groupLikeOutput, M42, N23, L-5, 12, "Courier"; ; fontset = message, inactive, noPageBreakBelow, nowordwrap, preserveAspect, groupLikeOutput, M42, N23, L1, 12, "Courier"; ; fontset = print, inactive, noPageBreakBelow, nowordwrap, preserveAspect, groupLikeOutput, M42, N23, L1, 12, "Courier"; ; fontset = info, inactive, noPageBreakBelow, nowordwrap, preserveAspect, groupLikeOutput, M42, N23, L1, 12, "Courier"; ; fontset = postscript, PostScript, formatAsPostScript, output, inactive, noPageBreakBelow, nowordwrap, preserveAspect, groupLikeGraphics, M7, l34, w282, h287, L1, 12, "Courier"; ; fontset = name, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, italic, L1, 10, "Times"; ; fontset = header, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 12; fontset = Left Header, nohscroll, cellOutline, 12; fontset = footer, inactive, nohscroll, noKeepOnOnePage, preserveAspect, center, M7, L1, 12; fontset = Left Footer, cellOutline, blackBox, 12; fontset = help, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 10, "Times"; ; fontset = clipboard, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 12; fontset = completions, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 12, "Courier"; ; fontset = special1, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 12; fontset = special2, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 12; fontset = special3, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 12; fontset = special4, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 12; fontset = special5, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 12;] :[font = title; inactive; preserveAspect; startGroup; ] The Peterson-Stickel Completion Algorithm :[font = subsubtitle; inactive; preserveAspect; ] Roberto Virga Department of Mathematics, Carnegie Mellon University rvirga+@andrew.cmu.edu :[font = subsubtitle; inactive; preserveAspect; ] Disclaimer: this work is still experimental, and not meant for public distribution. If you use this notebook, please notify the author at the address above. Bug reports and/or suggestions are highly welcome. :[font = text; inactive; preserveAspect; ] This notebook implements Peterson-Stickel completion, as decribed in [6], an extension of Knuth-Bendix method [5] to theories containing associative-commutative (AC) operators.; the algorithm used is basicly the one presented in [4]. Two term orderings are provided with this implementation: Recursive Path, and Lexicographic Path; for further details on these orderings, see [2, 3]. :[font = section; inactive; Cclosed; preserveAspect; startGroup; ] Syntax :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Variables :[font = text; inactive; preserveAspect; ] While Mathematica can represent (uninterpreted) funtion symbols and costants, it doesn't have a builtin notion of (free) variable. This section offers one of many possible implementations of first order variables. ;[s] 3:0,0;6,1;17,2;213,-1; 3:1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0; :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Variables :[font = text; inactive; preserveAspect; ] A variable is, by covention, any symbol beginning with "x", "y", "z", "u", "v", "w". :[font = input; initialization; preserveAspect; endGroup; ] *) VariableQ[t_Symbol] := MemberQ[ {"x", "y", "z", "u", "v", "w"}, First[Characters[ToString[t]]]]; VariableQ[t_] = False; (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Free variables :[font = text; inactive; preserveAspect; ] The list of free variables of a term is obtained by looking at the terminal nodes of a term. :[font = input; initialization; preserveAspect; ] *) FreeVariables[term_] := Select[Level[{term}, -1], VariableQ] (* :[font = text; inactive; preserveAspect; ] A term is ground if it contains no variables. :[font = input; initialization; preserveAspect; endGroup; ] *) GroundQ[term_] := FreeVariables[term] == {} (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = input; preserveAspect; startGroup; ] VariableQ[x11] :[font = output; output; inactive; preserveAspect; endGroup; ] True ;[o] True :[font = input; preserveAspect; startGroup; ] VariableQ[c1] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; ] False ;[o] False :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Remark :[font = text; inactive; preserveAspect; endGroup; endGroup; ] By this definition, any symbol beginnning with an uppercase character is a constant. If you want, for example, consider "X11" a variable, you can do so by extending the previous definition. :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Patterns :[font = text; inactive; preserveAspect; ] We use the builtin primitives to implement rewriting. This requires, however, that we turn the lhs of a rule into a Mathematica pattern. Conversely, given a pattern, we will want to obtain the corresponding term. ;[s] 3:0,0;116,1;127,2;213,-1; 3:1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0; :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] From term to pattern :[font = input; initialization; preserveAspect; endGroup; ] *) TermToPattern[term_] := term /. {v_Symbol?VariableQ :> Apply[Pattern, {v, Blank[]}]} (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] From pattern to term :[font = input; initialization; preserveAspect; endGroup; ] *) PatternToTerm[pattern_] := pattern /. {v_Pattern :> First[v]} (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = input; preserveAspect; startGroup; ] TermToPattern[f[g[a, x], y]] :[font = output; output; inactive; preserveAspect; endGroup; ] f[g[a, x_], y_] ;[o] f[g[a, x_], y_] :[font = input; preserveAspect; startGroup; ] PatternToTerm[f[g[a, x_], y_]] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; ] f[g[a, x], y] ;[o] f[g[a, x], y] :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Remark :[font = text; inactive; preserveAspect; endGroup; endGroup; ] Note that not all the Mathematica patterns correspond to valid terms. ;[s] 3:0,0;22,1;33,2;70,-1; 3:1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0; :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Renaming :[font = text; inactive; preserveAspect; ] Sometime it is useful to rename all the variables of a given term or rewrite rule. We assign variables new names of the form "xm", ..., "xn", where m, n are positive integers, n >= m. Unless specified otherwise, it is assumed m = 1. ;[s] 17:0,0;127,1;128,2;129,3;131,4;138,5;139,6;148,7;149,8;151,9;152,10;176,11;177,12;182,13;183,14;227,15;228,16;235,-1; 17:1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0; :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] New variables :[font = input; initialization; preserveAspect; endGroup; ] *) NewVariable[n_] := ToExpression[StringJoin["x", ToString[n]]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Renamimg :[font = input; initialization; preserveAspect; endGroup; ] *) Rename[expr_, start_Integer:1] := Block[ {n = start}, expr /. Map[ (# -> NewVariable[n++])&, Union[FreeVariables[expr]]]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = input; preserveAspect; startGroup; ] Rename[f[x1, x, x]] :[font = output; output; inactive; preserveAspect; endGroup; ] f[x2, x1, x1] ;[o] f[x2, x1, x1] :[font = input; preserveAspect; startGroup; ] Rename[f[x1, x, x], 3] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; endGroup; ] f[x4, x3, x3] ;[o] f[x4, x3, x3] :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Variable Generation :[font = text; inactive; preserveAspect; ] On some occasions, it will be necessary to generate new variable names, never used before. By convention, these will have names starting with "xnew". :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Initialization :[font = text; inactive; preserveAspect; ] Removes all the new variable names generated so far. :[font = input; initialization; preserveAspect; endGroup; ] *) Restart[] := Remove["xnew*"] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Generate a variable :[font = text; inactive; preserveAspect; ] Generates a new variable name. :[font = input; initialization; preserveAspect; endGroup; endGroup; ] *) GenerateVariable[] := Unique["xnew"] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] AC Operators :[font = text; inactive; preserveAspect; ] Mathematica has the builtin notion of AC operators. An operator is AC if it has the attributes Flat, and Orderless, and OneIdentity. For brevity, we define here a test for AC operators. ;[s] 8:0,0;11,1;95,2;99,3;105,4;114,5;120,6;131,7;185,-1; 8:1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Courier,1,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Courier,1,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Courier,1,12,0,0,0;1,11,8,Times,0,12,0,0,0; :[font = input; initialization; preserveAspect; endGroup; endGroup; ] *) ACOperatorQ[f_Symbol] := And[ MemberQ[Attributes[f], Flat], MemberQ[Attributes[f], Orderless], MemberQ[Attributes[f], OneIdentity]]; ACOperatorQ[f_] = False; (* :[font = section; inactive; Cclosed; preserveAspect; startGroup; ] Unification :[font = text; inactive; preserveAspect; ] Mathematica implements matching (of patterns). However we will also need unification. Two terms are said to unify if there is a substitution that makes them equal. In case two terms are unifiable, we will also interested in the most general of these substitutions. ;[s] 2:0,0;11,1;264,-1; 2:1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0; :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Diophantine Equations :[font = text; inactive; preserveAspect; ] A diophantine equation is associated to the unification problem by considering terms as integer variables. Common occurences of a term on both sides of the quation are automatically simplified. :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Occurrences Count :[font = text; inactive; preserveAspect; ] Counts the occurrences of the list of terms in term1, discarding common occurences with the list term2. ;[s] 5:0,0;47,1;52,2;97,3;102,4;104,-1; 5:1,11,8,Times,0,12,0,0,0;1,10,8,Courier,1,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Courier,1,12,0,0,0;1,11,8,Times,0,12,0,0,0; :[font = input; initialization; preserveAspect; endGroup; ] *) OccurrencesCount[terms1_List, terms2_List] := Select[ Map[ {#, Count[terms1, #] - Count[terms2, #]}&, Union[terms1]], Positive[Last[#]]& ] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = input; preserveAspect; startGroup; ] OccurrencesCount[{x1, x1, x2, x3}, {y1, y1, y2}] :[font = output; output; inactive; preserveAspect; endGroup; ] {{x1, 2}, {x2, 1}, {x3, 1}} ;[o] {{x1, 2}, {x2, 1}, {x3, 1}} :[font = input; preserveAspect; startGroup; ] OccurrencesCount[{y1, y1, y2}, {x1, x1, x2, x3}] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; endGroup; ] {{y1, 2}, {y2, 1}} ;[o] {{y1, 2}, {y2, 1}} :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Base Solutions of a Diophantine Equation :[font = text; inactive; preserveAspect; ] In [7], Stickel observed that all the base solutions to the diophantine equation are bounded in sum, and this bound is easily computed. Hence, one way to obtain the set of base solution is to equate all the linear combinations of the lhs and rhs which have a common sum less than or equal to the bound, and remove from this set all those combiations which are linear dependent from other (smaller) ones. :[font = subsubsection; inactive; preserveAspect; startGroup; ] Base Solutions Bound :[font = text; inactive; preserveAspect; ] Compute a bound to the sum of any base solution, as described in [7]. :[font = input; initialization; preserveAspect; endGroup; ] *) BaseSolutionsBound[count1_, count2_] := Times[ Max[ Map[ Function[c1, Max[ Map[ Function[c2, LCM[c1, c2]], Map[Last, count2]]]], Map[Last, count1]]], Max[Length[count1], Length[count2]]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Linear Combinations of a Given Sum :[font = text; inactive; preserveAspect; ] Computes all the nonnegative linear combinations which produce a given sum. :[font = input; initialization; preserveAspect; endGroup; ] *) LinearCombinationSum[{}, n_] := If[n == 0, {{}}, {}]; LinearCombinationSum[count_List, n_] := With[ {k = First[count][[2]]}, Apply[ Union, Table[ Map[ Prepend[#, i]&, LinearCombinationSum[Rest[count], n - i*k]], {i, 0,Quotient[n, k]}]]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Decomposable Combination :[font = text; inactive; preserveAspect; ] Returns True if and only if the linear combination given can be decomposed as the sum of one of the given linear combinations and some other (nonnegative) linear combination of smaller sum. :[font = input; initialization; preserveAspect; endGroup; ] *) DecomposableCombination[lc_, lcs_] := Apply[ Or, Map[MatchQ[lc - #, {__Integer?NonNegative}]&, lcs]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Base Solutions :[font = text; inactive; preserveAspect; ] Computes all the base solutions to the diophantine equation :[font = input; initialization; preserveAspect; endGroup; ] *) BaseSolutions[{}, count2_, n_] = {}; BaseSolutions[count1_, {}, n_] = {}; BaseSolutions[count1_, count2_, n_] := Fold[ Function[{oldsols, i}, Block[ {oldlcs1 = Map[(#[[1]])&, oldsols], oldlcs2 = Map[(#[[2]])&, oldsols], newlcs1 = LinearCombinationSum[count1, i], newlcs2 = LinearCombinationSum[count2, i], indlcs1, indlcs2}, indlcs1 = Select[ newlcs1, Not[ DecomposableCombination[ #, oldlcs1]]& ]; indlcs2 = Select[ newlcs2, Not[ DecomposableCombination[ #, oldlcs2]]& ]; Union[ oldsols, Apply[ Union, Map[ Function[lc1, Map[ Function[lc2, {lc1, lc2}], newlcs2]], indlcs1]], Apply[ Union, Map[ Function[lc1, Map[ Function[lc2, {lc1, lc2}], indlcs2]], newlcs1]]]]], {}, Table[i, {i, n}]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = input; preserveAspect; startGroup; ] BaseSolutionsBound[ {{x1, 2}, {x2, 1}, {x3, 1}}, {{y1, 2}, {y2, 1}}] :[font = output; output; inactive; preserveAspect; endGroup; ] 6 ;[o] 6 :[font = input; preserveAspect; startGroup; ] LinearCombinationSum[{{x1, 2}, {x2, 1}, {x3, 1}}, 6] :[font = output; output; inactive; preserveAspect; endGroup; ] {{0, 0, 6}, {0, 1, 5}, {0, 2, 4}, {0, 3, 3}, {0, 4, 2}, {0, 5, 1}, {0, 6, 0}, {1, 0, 4}, {1, 1, 3}, {1, 2, 2}, {1, 3, 1}, {1, 4, 0}, {2, 0, 2}, {2, 1, 1}, {2, 2, 0}, {3, 0, 0}} ;[o] {{0, 0, 6}, {0, 1, 5}, {0, 2, 4}, {0, 3, 3}, {0, 4, 2}, {0, 5, 1}, {0, 6, 0}, {1, 0, 4}, {1, 1, 3}, {1, 2, 2}, {1, 3, 1}, {1, 4, 0}, {2, 0, 2}, {2, 1, 1}, {2, 2, 0}, {3, 0, 0}} :[font = input; preserveAspect; startGroup; ] LinearCombinationSum[{{y1, 2}, {y2, 1}}, 6] :[font = output; output; inactive; preserveAspect; endGroup; ] {{0, 6}, {1, 4}, {2, 2}, {3, 0}} ;[o] {{0, 6}, {1, 4}, {2, 2}, {3, 0}} :[font = input; preserveAspect; startGroup; ] DecomposableCombination[{0, 2, 3}, {{1, 0, 0}}] :[font = output; output; inactive; preserveAspect; endGroup; ] False ;[o] False :[font = input; preserveAspect; startGroup; ] DecomposableCombination[{1, 2, 3}, {{1, 0, 0}}] :[font = output; output; inactive; preserveAspect; endGroup; ] True ;[o] True :[font = input; preserveAspect; startGroup; ] BaseSolutions[ {{x1, 2}, {x2, 1}, {x3, 1}}, {{y1, 2}, {y2, 1}}, 6] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; endGroup; ] {{{0, 0, 1}, {0, 1}}, {{0, 0, 2}, {1, 0}}, {{0, 1, 0}, {0, 1}}, {{0, 1, 1}, {1, 0}}, {{0, 2, 0}, {1, 0}}, {{1, 0, 0}, {0, 2}}, {{1, 0, 0}, {1, 0}}} ;[o] {{{0, 0, 1}, {0, 1}}, {{0, 0, 2}, {1, 0}}, {{0, 1, 0}, {0, 1}}, {{0, 1, 1}, {1, 0}}, {{0, 2, 0}, {1, 0}}, {{1, 0, 0}, {0, 2}}, {{1, 0, 0}, {1, 0}}} :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Solutions of a Diophantine Equation :[font = text; inactive; preserveAspect; ] Computed the base solutions, all the other solutions are obtained by combining those. Therefore, we identify any solution with an element of the powerset of the base set. Amon these solutions, the admissible ones will be those who have all positive components. :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] PowerSet :[font = text; inactive; preserveAspect; ] Computes the powerset of the given set. :[font = input; initialization; preserveAspect; endGroup; ] *) PowerSet[{}] = {{}}; PowerSet[set_List] := With[ {powset = PowerSet[Rest[set]]}, Union[powset, Map[Prepend[#, First[set]]& , powset]]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Admissibility Test :[font = text; inactive; preserveAspect; ] Checks if a solution is admissible (i.e. all the components must be positive). :[font = input; initialization; preserveAspect; endGroup; ] *) AdmissibleSolution[sol_, counts_] := MatchQ[ Map[Apply[Plus, #]&, Transpose[sol]], Map[ Map[ If[VariableQ[#[[1]]], _?Positive, 1]&, #]&, counts]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Solution To Terms :[font = text; inactive; preserveAspect; ] Given a solution to the diophantine equation, it constructs the corresponding sets of terms. :[font = input; initialization; preserveAspect; endGroup; ] *) SolutionToTerms[sol_, f_Symbol] := Block[ {i, j, k = Length[sol], vars = Map[GenerateVariable[]&, sol]}, Map[ Map[ (Function[args, If[ Length[args] == 1, First[args], Apply[f, args]]] [Apply[ Join, Table[ Table[vars[[i]], {j, 1, #[[i]]}], {i, 1, k}]]])&, Transpose[#]]&, Transpose[sol]]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = input; preserveAspect; startGroup; ] PowerSet[ { {{0, 0, 1}, {0, 1}}, {{0, 0, 2}, {1, 0}}, {{0, 1, 0}, {0, 1}}, {{0, 1, 1}, {1, 0}}, {{0, 2, 0}, {1, 0}}, {{1, 0, 0}, {0, 2}}, {{1, 0, 0}, {1, 0}} }][[41]] :[font = output; output; inactive; preserveAspect; endGroup; ] {{{0, 0, 1}, {0, 1}}, {{0, 1, 1}, {1, 0}}, {{1, 0, 0}, {1, 0}}} ;[o] {{{0, 0, 1}, {0, 1}}, {{0, 1, 1}, {1, 0}}, {{1, 0, 0}, {1, 0}}} :[font = input; preserveAspect; startGroup; ] AdmissibleSolution[ { {{0, 0, 1}, {0, 1}}, {{0, 1, 1}, {1, 0}}, {{1, 0, 0}, {1, 0}} }, {{{x1, 2}, {x2, 1}, {x3, 1}}, {{y1, 2}, {y2, 1}}}] :[font = output; output; inactive; preserveAspect; endGroup; ] True ;[o] True :[font = input; preserveAspect; startGroup; ] Restart[]; SolutionToTerms[ { {{0, 0, 1}, {0, 1}}, {{0, 1, 1}, {1, 0}}, {{1, 0, 0}, {1, 0}} }, f] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; endGroup; ] {{xnew3, xnew2, f[xnew1, xnew2]}, {f[xnew2, xnew3], xnew1}} ;[o] {{xnew3, xnew2, f[xnew1, xnew2]}, {f[xnew2, xnew3], xnew1}} :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] AC Unification :[font = input; initialization; preserveAspect; endGroup; ] *) ACUnify[list1_List, list2_List, f_Symbol, subst_List:{}] := Block[ {vars = FreeVariables[{list1, list2}], count1 = OccurrencesCount[list1, list2], count2 = OccurrencesCount[list2, list1]}, Map[ Select[#, MemberQ[vars, First[#]]& ]&, Apply[ Union, Map[ Apply[ Function[{newlist1, newlist2}, Unify[ Join[newlist1, newlist2], Map[ First, Join[count1, count2]], subst]], SolutionToTerms[#, f]]&, Select[ PowerSet[ BaseSolutions[ count1, count2, BaseSolutionsBound[ count1, count2]]], AdmissibleSolution[ #, {count1, count2}]& ]]]]] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] List Unification :[font = input; initialization; preserveAspect; endGroup; ] *) Unify[{}, {}, subst_List:{}] = {subst}; Unify[list1_List, {}, subst_List:{}] = {}; Unify[{}, list2_List, subst_List:{}] = {}; Unify[list1_List, list2_List, subst_List:{}] := Block[ {mgus = Unify[First[list1], First[list2]]}, Apply[ Join, Map[ Unify[ Rest[list1] /. #, Rest[list2] /. #, Union[#, subst /. #]]&, mgus]]] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Term Unification :[font = input; initialization; preserveAspect; endGroup; ] *) Unify[x_, x_, subst_List:{}] = {subst}; Unify[x_Symbol?VariableQ, y_Symbol?VariableQ, subst_List:{}] := {Append[subst, x -> y]}; Unify[x_Symbol?VariableQ, y_, subst_List:{}] := If[FreeQ[y, x], {Append[subst, x -> y]}, {}]; Unify[x_, y_Symbol?VariableQ, subst_List:{}] := If[FreeQ[x, y], {Append[subst, y -> x]}, {}]; Unify[x_Symbol, y_, subst_List:{}] = {}; Unify[x_, y_Symbol, subst_List:{}] = {}; Unify[x_, y_, subst_List:{}] := If[ SameQ[Head[x], Head[y]], With[ {head = Head[x]}, If[ ACOperatorQ[head], ACUnify[ Apply[List, x], Apply[List, y], head, subst], Unify[ Apply[List, x], Apply[List, y], subst]]], {}] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = input; preserveAspect; startGroup; ] Unify[p[x, f[a]], p[f[y], f[y]]] :[font = output; output; inactive; preserveAspect; endGroup; ] {{x -> f[a], y -> a}} ;[o] {{x -> f[a], y -> a}} :[font = input; preserveAspect; startGroup; ] Unify[p[b, f[a]], p[b, f[a]]] :[font = output; output; inactive; preserveAspect; endGroup; ] {{}} ;[o] {{}} :[font = input; preserveAspect; startGroup; ] Unify[p[b, f[a]], p[y, f[y]]] :[font = output; output; inactive; preserveAspect; endGroup; ] {} ;[o] {} :[font = input; preserveAspect; startGroup; ] Block[ {oldf, result}, oldf = Attributes[f]; Attributes[f] = {Flat, Orderless, OneIdentity}; Restart[]; result = Unify[g[a, f[x1, a]], g[x2, f[x2, b]]]; Attributes[f] = oldf; result] :[font = output; output; inactive; preserveAspect; endGroup; ] {{x1 -> b, x2 -> a}} ;[o] {{x1 -> b, x2 -> a}} :[font = input; preserveAspect; startGroup; ] Block[ {oldf, result}, oldf = Attributes[f]; Attributes[f] = {Flat, Orderless, OneIdentity}; Restart[]; result = Unify[f[x1, b, a, g[x1]], f[a, g[x2], a, x3]]; Attributes[f] = oldf; result] :[font = output; output; inactive; preserveAspect; endGroup; ] {{x1 -> f[a, xnew20], x2 -> f[a, xnew20], x3 -> f[b, xnew20]}, {x1 -> f[a, g[x2]], x3 -> f[b, g[f[a, g[x2]]]]}, {x1 -> f[a, xnew41, g[x2]], x3 -> f[b, xnew41, g[f[a, xnew41, g[x2]]]]}, {x1 -> a, x2 -> a, x3 -> b}} ;[o] {{x1 -> f[a, xnew20], x2 -> f[a, xnew20], x3 -> f[b, xnew20]}, {x1 -> f[a, g[x2]], x3 -> f[b, g[f[a, g[x2]]]]}, {x1 -> f[a, xnew41, g[x2]], x3 -> f[b, xnew41, g[f[a, xnew41, g[x2]]]]}, {x1 -> a, x2 -> a, x3 -> b}} :[font = input; preserveAspect; startGroup; ] Block[ {oldf, result}, oldf = Attributes[f]; Attributes[f] = {Flat, Orderless, OneIdentity}; Restart[]; result = Unify[ f[f[a, g[x1]], g[a], x2], f[a, x3, f[x4, g[a]]]]; Attributes[f] = oldf; result] :[font = output; output; inactive; preserveAspect; endGroup; ] {{x2 -> x3, x4 -> g[x1]}, {x2 -> x4, x3 -> g[x1]}, {x2 -> f[xnew6, x3], x4 -> f[xnew6, g[x1]]}, {x2 -> f[xnew10, x4], x3 -> f[xnew10, g[x1]]}} ;[o] {{x2 -> x3, x4 -> g[x1]}, {x2 -> x4, x3 -> g[x1]}, {x2 -> f[xnew6, x3], x4 -> f[xnew6, g[x1]]}, {x2 -> f[xnew10, x4], x3 -> f[xnew10, g[x1]]}} :[font = input; preserveAspect; startGroup; ] Block[ {oldf, oldh, result}, oldf = Attributes[f]; Attributes[f] = {Flat, Orderless, OneIdentity}; oldh = Attributes[h]; Attributes[h] = {Flat, Orderless, OneIdentity}; Restart[]; result = Unify[f[b, h[x1, x2]], f[h[x3,a],x3]]; Attributes[f] = oldf; Attributes[h] = oldh; result] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; endGroup; ] {{x1 -> a, x2 -> b, x3 -> b}, {x1 -> b, x2 -> a, x3 -> b}} ;[o] {{x1 -> a, x2 -> b, x3 -> b}, {x1 -> b, x2 -> a, x3 -> b}} :[font = section; inactive; Cclosed; preserveAspect; startGroup; ] Orderings :[font = text; inactive; preserveAspect; ] Knuth-Bendix completion orders equation into rules using a well-founded partial ordering. This guarantees strong termination of the resulting term rewriting system. :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Restricted Quantifiers :[font = text; inactive; preserveAspect; ] The definition of the three term orderings below is significantly simplified if we first introduce functions which compute the truth value of a restricted quantification, i.e. a statement of the form "for all x in L f(x)" or "there exists x in L such that f(x)", where L is a list of terms. :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] ForAll :[font = input; initialization; preserveAspect; endGroup; ] *) ForAll[list_, f_] := Fold[And[#1, f[#2]]& , True, list] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] ForSome :[font = input; initialization; preserveAspect; endGroup; endGroup; ] *) ForSome[list_, f_] := Fold[Or[#1, f[#2]]& , False, list] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Symbols Ordering :[font = text; inactive; preserveAspect; ] All three orderings implemented require that a quasi-order (i.e. a reflexive, transitive relation) greatereq has already been defined over the set of symbols of the language. By default we use a lexicographic ordering on strings, but it is possible, and in some cases advisable, to override this choice. ;[s] 3:0,0;99,1;108,2;304,-1; 3:1,11,8,Times,0,12,0,0,0;1,10,8,Courier,1,12,0,0,0;1,11,8,Times,0,12,0,0,0; :[font = input; initialization; preserveAspect; endGroup; ] *) greatereq[term1_, term2_] := OrderedQ[{term2, term1}] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Weights :[font = text; inactive; preserveAspect; ] The Knuth Bendix ordering also requires a nonnegative weight to be defined for every nonvariable symbol in the language. The weight of a variable is then defined as the minimum of the weights assigned to constant symbols. We assume that the weight of a variable (and therefore the one of at least one constant in the language) is 1. By default, all the other weights are also set to one. :[font = input; initialization; preserveAspect; endGroup; ] *) weight[term_Symbol] = 1; weight[term_] := weight[Head[term]] + Apply[Plus, Map[weight, term]] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Ordering Extensions :[font = text; inactive; preserveAspect; ] In defining term orderings, we will need to compare, given two terms with the same head funtion symbol, the arguments of these funtion. From this the need to extend a given ordering between terms to sequences (or multisets) of terms. :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Multiset :[font = input; initialization; preserveAspect; endGroup; ] *) MultisetGE[{___}, {}, _] = True; MultisetGE[{}, {__}, _] = False; MultisetGE[list1_List, list2_List, greater_] := With[ {term1 = First[list1]}, MultisetGE[ Rest[list1], If[MemberQ[list2, term1], Drop[ list2, First[Position[list2, term1, {1}]]], Select[ list2, Not[greater[term1, #]]& ]], greater]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Lexicographic :[font = input; initialization; preserveAspect; endGroup; ] *) LexicographicGE[{___}, {}, _] = True; LexicographicGE[{}, {__}, _] = False; LexicographicGE[list1_List, list2_List, greater_] := If[ SameQ[First[list1], First[list2]], LexicographicGE[Rest[list1], Rest[list2], greater], greater[First[list1], First[list2]]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = input; preserveAspect; startGroup; ] MultisetGE[{3, 2, 2}, {3, 2, 1, 1, 1, 1}, Greater] :[font = output; output; inactive; preserveAspect; endGroup; ] True ;[o] True :[font = input; preserveAspect; startGroup; ] LexicographicGE[{1, 2, 3}, {1, 2, 2}, Greater] :[font = output; output; inactive; preserveAspect; endGroup; ] True ;[o] True :[font = input; preserveAspect; startGroup; ] LexicographicGE[{1, 2, 3}, {1, 2, 4}, Greater] :[font = output; output; inactive; preserveAspect; endGroup; ] False ;[o] False :[font = input; preserveAspect; startGroup; ] LexicographicGE[{3, 2, 2}, {1, 2, 3, 0}, Greater] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; endGroup; ] True ;[o] True :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Orderings :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Knuth-Bendix :[font = input; initialization; preserveAspect; endGroup; ] *) KnuthBendixGT[term_, term_] = False; KnuthBendixGT[term1_, term2_] := With[ {vars1 = FreeVariables[term1], vars2 = FreeVariables[term2], weight1 = weight[term1], weight2 = weight[term2], head1 = If[MatchQ[term1, _Symbol], term1, Head[term1]], head2 = If[MatchQ[term2, _Symbol], term2, Head[term2]], args1 = If[MatchQ[term1, _Symbol], {}, Apply[List, term1]], args2 = If[MatchQ[term2, _Symbol], {}, Apply[List, term2]]}, And[ MultisetGE[vars1, vars2, (True)& ], weight1 >= weight2, Or[ weight1 > weight2, VariableQ[term2], And[ Not[VariableQ[term1]], greatereq[head1, head2], Not[greatereq[head2, head1]]], And[ Not[VariableQ[term1]], And[ greatereq[head1, head2], greatereq[head2, head1]], If[ Or[ ACOperatorQ[head1], ACOperatorQ[head2]], MultisetGE[ args1, args2, KnuthBendixGT], LexicographicGE[ args1, args2, KnuthBendixGT]]]]]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Recursive Path :[font = input; initialization; preserveAspect; endGroup; ] *) RecursivePathGT[term1_, term1_] = False; RecursivePathGT[term1_Symbol?VariableQ, term2_] = False; RecursivePathGT[term1_, term2_Symbol?VariableQ] := Not[FreeQ[term1, term2]]; RecursivePathGT[term1_Symbol, term2_Symbol] := greatereq[term1, term2]; RecursivePathGT[term1_Symbol, term2_] := And[ greatereq[term1, Head[term2]], ForAll[term2, RecursivePathGT[term1, #]& ]]; RecursivePathGT[term1_, term2_Symbol] := Or[ greatereq[Head[term1], term2], ForSome[term1, RecursivePathGT[#, term2]& ]]; RecursivePathGT[term1_, term2_] := With[ {head1 = Head[term1], head2 = Head[term2], args1 = Apply[List, term1], args2 = Apply[List, term2]}, Or[ And[ greatereq[head1, head2], Not[greatereq[head2, head1]], ForAll[ term2, RecursivePathGT[term1, #]& ]], And[ greatereq[head1, head2], greatereq[head2, head1], MultisetGE[ args1, args2, RecursivePathGT]], ForSome[term1, RecursivePathGT[#, term2]& ]]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Lexicographic Path :[font = input; initialization; preserveAspect; endGroup; ] *) LexicographicPathGT[term1_, term1_] = False; LexicographicPathGT[term1_Symbol?VariableQ, term2_] = False; LexicographicPathGT[term1_, term2_Symbol?VariableQ] := Not[FreeQ[term1, term2]]; LexicographicPathGT[term1_Symbol, term2_Symbol] := greatereq[term1, term2]; LexicographicPathGT[term1_Symbol, term2_] := And[ greatereq[term1, Head[term2]], ForAll[term2, LexicographicPathGT[term1, #]& ]]; LexicographicPathGT[term1_, term2_Symbol] := Or[ greatereq[Head[term1], term2], ForSome[term1, LexicographicPathGT[#, term2]& ]]; LexicographicPathGT[term1_, term2_] := With[ {head1 = Head[term1], head2 = Head[term2], args1 = Apply[List, term1], args2 = Apply[List, term2]}, Or[ And[ greatereq[head1, head2], Not[greatereq[head2, head1]], ForAll[ term2, LexicographicPathGT[term1, #]& ]], And[ greatereq[head1, head2], greatereq[head2, head1], If[ Or[ ACOperatorQ[head1], ACOperatorQ[head2]], MultisetGE[ args1, args2, LexicographicPathGT], LexicographicGE[ args1, args2, LexicographicPathGT]]], ForSome[term1, LexicographicPathGT[#, term2]& ]]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = input; preserveAspect; startGroup; ] RecursivePathGT[g[i[x], y], f[y, x]] :[font = output; output; inactive; preserveAspect; endGroup; ] True ;[o] True :[font = input; preserveAspect; startGroup; ] RecursivePathGT[f[f[x, y], z], f[x, f[y, z]]] :[font = output; output; inactive; preserveAspect; endGroup; ] False ;[o] False :[font = input; preserveAspect; startGroup; ] LexicographicPathGT[f[f[x, y], z], f[x, f[y, z]]] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; endGroup; endGroup; ] True ;[o] True :[font = section; inactive; Cclosed; preserveAspect; startGroup; ] Simplification :[font = text; inactive; preserveAspect; ] The Knuth-Bendix procedure generates which are normal, i.e. whose rules have been simplified as much as possible. During the completion process it will therefore be necessary to simplify all the equations, and to remove the redundant ones. :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Rewrite :[font = input; initialization; preserveAspect; ] *) Rewrite[theory_List, simplifiers_] := Complement[ Map[Rewrite[#, simplifiers]& , theory], {True}] (* :[font = input; initialization; preserveAspect; ] *) Rewrite[rule_Rule, simplifiers_] := Block[ {oldleft = PatternToTerm[rule[[1]]], oldright = rule[[2]], newleft, newright}, newleft = oldleft //. Append[ Complement[simplifiers, {rule}], (h_[x_] :> x /; ACOperatorQ[h])]; newright = oldright //. Append[ simplifiers, (h_[x_] :> x /; ACOperatorQ[h])]; If[newleft =!= oldleft, newleft == newright, TermToPattern[oldleft] -> newright]] (* :[font = input; initialization; preserveAspect; endGroup; ] *) Rewrite[equality_Equal, simplifiers_] := equality //. Append[ simplifiers, (h_[x_] :> x /; ACOperatorQ[h])] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = input; preserveAspect; startGroup; ] Rewrite[ {f[f[x_, e], y_] -> f[x, y]}, {f[f[x_, y_], z_] -> f[x, f[y, z]], f[e, x_] -> x}] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; endGroup; ] {} ;[o] {} :[font = section; inactive; Cclosed; preserveAspect; startGroup; ] Critical Pairs :[font = text; inactive; preserveAspect; ] Critical pairs are by superposition of two rules, i.e. by looking at all the overlaps between the lhs of a rule and nonvariable subterms of the lhs of the other. In the case of a rule involving a AC operator, it will be necessary to consider also all the superpositions with the associative lift of the rule, obtained by adding a new argument to the AC functor to both sides of the rule; for details, see [6]. :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Associative Lift :[font = input; initialization; preserveAspect; ] *) AssociativeLift[rules_List] := Apply[Union, Map[AssociativeLift, rules]] (* :[font = input; initialization; preserveAspect; endGroup; ] *) AssociativeLift[rule_Rule] := With[ {h = Head[rule[[1]]], v = GenerateVariable[]}, If[ACOperatorQ[h], {(f[rule[[1]], Apply[Pattern, {v, Blank[]}]] -> f[rule[[2]], v]), rule}, {rule}]] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Superpose :[font = text; inactive; preserveAspect; ] Compute all superpositions between the two rules. In looking for overlaps, all the nonvariable positions of the lhs of rule2 are considered. However, it is possible to exclude other positions by providing the optional parameter forbidden. ;[s] 5:0,0;119,1;124,2;228,3;237,4;239,-1; 5:1,11,8,Times,0,12,0,0,0;1,10,8,Courier,1,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Courier,1,12,0,0,0;1,11,8,Times,0,12,0,0,0; :[font = input; initialization; preserveAspect; endGroup; ] *) Superpose[rule1_Rule, rule2_Rule, forbidden_List:{}] := With[ {left1 = PatternToTerm[rule1[[1]]], left2 = PatternToTerm[rule2[[1]]], right1 = rule1[[2]], right2 = rule2[[2]]}, Complement[ Apply[ Union, Map[ Function[pos, Apply[ Union, Map[ Function[mgu, If[ pos == {}, {right1 == right2}, {right1 == ReplacePart[ left1, right2, pos]} ] /. mgu], Unify[ left2, Apply[ Part, Prepend[pos, left1]]]]]], Complement[ Position[ left1, _?(Not[VariableQ[#]]&), Heads ->False], forbidden]]], {True}]] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Critical Pairs :[font = input; initialization; preserveAspect; endGroup; ] *) CriticalPairs[rule_Rule, rules_List] := With[ {newrule = AssociativeLift[ Rename[ rule, Length[Union[FreeVariables[rules]]] + 1]], newrules = AssociativeLift[rules]}, Union[ Map[ Rename, Rewrite[ Apply[ Union, Map[ Function[suprule, Union[ Apply[ Union, Map[ Superpose[suprule, #]&, newrules]], Apply[ Union, Map[ Superpose[#, suprule, {{}}]&, newrules]]]], newrule]], rules]]]] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = input; preserveAspect; startGroup; ] Superpose[ f[f[x_, y_], z_] -> f[x, f[y, z]], f[i[u_], u_] -> e] :[font = output; output; inactive; preserveAspect; endGroup; ] {f[i[y], f[y, z]] == f[e, z]} ;[o] {f[i[y], f[y, z]] == f[e, z]} :[font = input; preserveAspect; startGroup; ] CriticalPairs[ f[f[x_, y_], z_] -> f[x, f[y, z]], {f[i[x_], x_] -> e, f[e, x_] -> x}] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; endGroup; ] {f[i[x1], f[x1, x2]] == x2} ;[o] {f[i[x1], f[x1, x2]] == x2} :[font = section; inactive; Cclosed; preserveAspect; startGroup; ] Completion :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Completion Strategies :[font = text; inactive; preserveAspect; ] These strategies are used to select, at each step of the completion process the next rule to consider for superposition. Of these, only the two "F.I.F.O." ones are proved to be fair (for a discussion on fairness of completion strategies, see [1]); however, the others may turn out to be handy in some particular cases. :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Lexicographic F.I.F.O. :[font = text; inactive; preserveAspect; ] Always select the lexicograpically smallest rule. :[font = input; initialization; preserveAspect; endGroup; ] *) LexicographicFIFO[rules_List] := First[Sort[rules]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Lexicographic L.I.F.O. :[font = text; inactive; preserveAspect; ] Always select the lexicograpically largest rule. :[font = input; initialization; preserveAspect; endGroup; ] *) LexicographicLIFO[rules_List] := Last[Sort[rules]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Small Components F.I.F.O. :[font = text; inactive; preserveAspect; ] Always select the rule of minimum size. :[font = input; initialization; preserveAspect; endGroup; ] *) SmallFIFO[rules_List] := First[ Sort[rules, LessEqual[ ByteCount[#1], ByteCount[#2]]& ]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Small Components L.I.F.O. :[font = text; inactive; preserveAspect; ] Always select the rule of maximum size. :[font = input; initialization; preserveAspect; endGroup; endGroup; ] *) SmallLIFO[rules_List] := Last[ Sort[rules, LessEqual[ ByteCount[#1], ByteCount[#2]]& ]] (* :[font = subsection; inactive; preserveAspect; startGroup; ] Completion :[font = input; initialization; preserveAspect; ] *) Complete::trace = ""; (* :[font = input; initialization; preserveAspect; ] *) Options[Complete] = {Ordering -> RecursivePathGT, Strategy -> SmallFIFO, PrintTrace -> True}; (* :[font = input; initialization; preserveAspect; endGroup; endGroup; ] *) Complete[theory_List, options___Rule] := Block[ {choose = Strategy /. {options} /. Options[Complete], orderGT = Ordering /. {options} /. Options[Complete], trace = PrintTrace /. {options} /. Options[Complete], equations, allrules, marked, unmarked, rule}, equations = Map[Rename, theory]; allrules = marked = unmarked = {}; While[Union[equations, unmarked] =!= {}, While[equations =!= {}, Block[ {eq, result}, eq = First[equations]; equations = Rest[equations]; If[eq == True, Continue[]]; Which[ Apply[orderGT, eq], rule = (TermToPattern[eq[[1]]] -> eq[[2]]), Apply[orderGT, Reverse[eq]], rule = (TermToPattern[eq[[2]]] -> eq[[1]]), True, Return[Fail[eq]]]; AppendTo[allrules, rule]; equations = Rewrite[equations, allrules]; result = Rewrite[marked, allrules]; marked = Cases[result, _Rule]; equations = Union[ equations, Cases[result, _Equal]]; result = Rewrite[unmarked, allrules]; unmarked = Cases[result, _Rule]; equations = Union[ equations, Cases[result, _Equal]]; AppendTo[unmarked, rule]; allrules := Union[marked, unmarked]]]; If[trace, Complete::trace = ToString[ TableForm[ Join[marked, unmarked, equations]]]; Message[Complete::trace]]; Restart[]; rule = choose[unmarked]; AppendTo[marked, rule]; equations = CriticalPairs[rule, marked]; unmarked = Complement[unmarked, {rule}]]; Return[marked]] (* :[font = section; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Free abelian groups :[font = text; inactive; preserveAspect; ] The follows is a completion for free abelian groups.. The ordering used is a Lexicographic Path ordering with i > f > e. :[font = input; Cclosed; preserveAspect; startGroup; ] Block[ {oldf, result}, oldf = Attributes[f]; Attributes[f] = {Flat, Orderless, OneIdentity}; result = Complete[ {f[i[x], x] == e, f[e, x] == x}, Ordering -> LexicographicPathGT]; Attributes[f] = oldf; result] :[font = message; inactive; preserveAspect; ] Complete::trace: f[i[x1_], x1_] -> e f[e, x1_] -> x1 :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], x1_] -> e :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], x1_] -> e i[e] -> e i[i[x1_]] -> x1 f[i[f[x1_, x2_]], x1_] -> i[x2] :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], x1_] -> e i[e] -> e f[i[f[x1_, x2_]], x1_] -> i[x2] i[i[x1_]] -> x1 :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], x1_] -> e i[e] -> e i[i[x1_]] -> x1 f[i[f[x1_, x2_]], x1_] -> i[x2] :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], x1_] -> e i[e] -> e i[i[x1_]] -> x1 i[f[x1_, x2_]] -> f[i[x1], i[x2]] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; endGroup; ] {f[e, x1_] -> x1, f[i[x1_], x1_] -> e, i[e] -> e, i[i[x1_]] -> x1, i[f[x1_, x2_]] -> f[i[x1], i[x2]]} ;[o] {f[e, x1_] -> x1, f[i[x1_], x1_] -> e, i[e] -> e, i[i[x1_]] -> x1, i[f[x1_, x2_]] -> f[i[x1], i[x2]]} :[font = section; inactive; Cclosed; preserveAspect; startGroup; ] References :[font = text; inactive; preserveAspect; ] [1]Bachmair, L., Dershowitz, N., "Critical pair criteria for completion", Journal of Symbolic Computation, Vol 6, No. 1, pp. 1-18 :[font = text; inactive; preserveAspect; ] [2]Bachmair, L., Dershowitz, N., Hsiang, J., "Orderings for equational proofs", Proceedings of the 1st Annual IEEE Symposium on Logic in Computer Science, pp. 331-337, Cambridge, MA, 1986, pp. 346-357 :[font = text; inactive; preserveAspect; ] [3] Dershowitz, N., "Orderings for term rewriting systems", Theoretical Computer Science, Vol 17, No. 3, 1982, pp. 279-301 :[font = text; inactive; preserveAspect; ] [4] Huet, G., "A complete proof of correctness of the Knuth-Bendix completion algorithm", Journal of Computer and System Sciences, Vol. 23, 1981, pp. 11-21 :[font = text; inactive; preserveAspect; ] [5] Knuth, D.E., Bendix, P.B., "Simple word problems in universal algebras", Computational Problems in Abstract Algebra, J. Leech, Pergamon Press, Oxford, U.K., 1970, pp. 263-297 :[font = text; inactive; preserveAspect; ] [6] Peterson, G.L., Stickel, M.E., "Complete sets of reductions for some equational theories", Journal of the ACM, Vol. 28, No. 2, pp. 233-264 :[font = text; inactive; preserveAspect; endGroup; ] [7] Stickel, M.E., "A unification algorithm for associative-commutative funtions", Journal of the ACM, Vol. 28, No. 3, pp. 423-434 :[font = subsubtitle; inactive; preserveAspect; endGroup; ] Last updated: 30/5/96 ^*)