(*^ ::[paletteColors = 128; 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 Knuth-Bendix 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 Knuth-Bendix completion, as described in [5]; the algorithm used is basicly the one presented in [4]. Three term orderings are provided with this implementation: Knuth-Bendix, 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; endGroup; ] f[x4, x3, x3] ;[o] f[x4, x3, x3] :[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; ] List Unification :[font = input; initialization; preserveAspect; endGroup; ] *) Unify[{}, {}, subst_List:{}] = subst; Unify[list1_List, {}, subst_List:{}] = False; Unify[{}, list2_List, subst_List:{}] = False; Unify[list1_List, list2_List, subst_List:{}] := Block[ {mgu = Unify[First[list1], First[list2]]}, If[mgu =!= False, Unify[ Rest[list1] /. mgu, Rest[list2] /. mgu, Union[mgu, subst /. mgu]], False]] (* :[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], False]; Unify[x_, y_Symbol?VariableQ, subst_List:{}] := If[FreeQ[x, y], Append[subst, y -> x], False]; Unify[x_Symbol, y_, subst_List:{}] = False; Unify[x_, y_Symbol, subst_List:{}] = False; Unify[x_, y_, subst_List:{}] := If[ SameQ[Head[x], Head[y]], Unify[Apply[List, x], Apply[List, y], subst], False] (* :[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; endGroup; endGroup; ] False ;[o] False :[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 = text; inactive; preserveAspect; ] Knuth-Bendix ordering, originally presented in [5]. :[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]], LexicographicGE[ args1, args2, KnuthBendixGT]]]]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Recursive Path :[font = text; inactive; preserveAspect; ] Recursive Path Ordering; for details, see [3]. :[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 = text; inactive; preserveAspect; ] Lexicographic Recursive Path Ordering; for details, see [3]. :[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], 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 //. Complement[simplifiers, {rule}]; newright = oldright //. simplifiers; If[newleft =!= oldleft, newleft == newright, TermToPattern[oldleft] -> newright]] (* :[font = input; initialization; preserveAspect; endGroup; ] *) Rewrite[equality_Equal, simplifiers_] := equality //. simplifiers (* :[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. :[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[ Map[ Function[pos, With[ {mgu = Unify[ left2, Apply[ Part, Prepend[pos, left1]]]}, If[mgu =!= False, If[pos == {}, right1 == right2, right1 == ReplacePart[ left1, right2, pos]] /. mgu, True]]], 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 = Rename[ rule, Length[Union[FreeVariables[rules]]] + 1]}, Union[ Map[ Rename, Rewrite[ Union[ Apply[ Union, Map[ Superpose[newrule, #]&, rules]], Apply[ Union, Map[ Superpose[#, newrule, {{}}]&, rules]]], 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; Cclosed; 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]]; rule = choose[unmarked]; equations = CriticalPairs[rule, allrules]; AppendTo[marked, rule]; unmarked = Complement[unmarked, {rule}]]; Return[marked]] (* :[font = section; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Free groups :[font = text; inactive; preserveAspect; ] The follows is a completion for free groups.. The ordering used is a Lexicographic Path ordering with i > f > e. :[font = input; Cclosed; preserveAspect; startGroup; ] Complete[ {f[f[x, y], z] == f[x, f[y, z]], f[i[x], x] == e, f[e, x] == x}, Ordering -> LexicographicPathGT] :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] f[i[x1_], x1_] -> e :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] f[i[x1_], x1_] -> e :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], x1_] -> e f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] f[i[x1_], f[x1_, x2_]] -> x2 :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], f[x1_, x2_]] -> x2 f[i[x1_], x1_] -> e f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] f[i[e], x1_] -> x1 f[i[f[x1_, x2_]], f[x1_, f[x2_, x3_]]] -> x3 f[i[i[x1_]], x2_] -> f[x1, x2] f[x1_, e] -> x1 :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], f[x1_, x2_]] -> x2 f[i[x1_], x1_] -> e f[x1_, e] -> x1 f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] f[i[f[x1_, x2_]], f[x1_, f[x2_, x3_]]] -> x3 i[e] -> e i[i[x1_]] -> x1 :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], f[x1_, x2_]] -> x2 f[i[x1_], x1_] -> e f[x1_, e] -> x1 i[e] -> e f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] f[i[f[x1_, x2_]], f[x1_, f[x2_, x3_]]] -> x3 i[i[x1_]] -> x1 :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], f[x1_, x2_]] -> x2 f[i[x1_], x1_] -> e f[x1_, e] -> x1 i[e] -> e i[i[x1_]] -> x1 f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] f[i[f[x1_, x2_]], f[x1_, f[x2_, x3_]]] -> x3 f[x1_, i[x1_]] -> e f[x2_, f[i[x2_], x1_]] -> x1 :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], f[x1_, x2_]] -> x2 f[i[x1_], x1_] -> e f[x1_, e] -> x1 f[x1_, i[x1_]] -> e i[e] -> e i[i[x1_]] -> x1 f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] f[i[f[x1_, x2_]], f[x1_, f[x2_, x3_]]] -> x3 f[x1_, f[x2_, i[f[x1_, x2_]]]] -> e f[x2_, f[i[x2_], x1_]] -> x1 f[i[f[x1_, x2_]], x1_] -> i[x2] :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], f[x1_, x2_]] -> x2 f[i[x1_], x1_] -> e f[x1_, e] -> x1 f[x1_, i[x1_]] -> e f[x2_, f[i[x2_], x1_]] -> x1 i[e] -> e i[i[x1_]] -> x1 f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] f[i[f[x1_, x2_]], f[x1_, x3_]] -> f[i[x2], x3] f[i[f[x1_, x2_]], x1_] -> i[x2] f[x1_, f[x2_, f[i[f[x1_, x2_]], x3_]]] -> x3 f[x1_, f[x2_, i[f[x1_, x2_]]]] -> e i[f[i[x1_], x2_]] -> f[i[x2], x1] :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], f[x1_, x2_]] -> x2 f[i[x1_], x1_] -> e f[x1_, e] -> x1 f[x1_, i[x1_]] -> e f[x2_, f[i[x2_], x1_]] -> x1 i[e] -> e i[i[x1_]] -> x1 f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] i[f[x1_, x2_]] -> f[i[x2], i[x1]] :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], f[x1_, x2_]] -> x2 f[i[x1_], x1_] -> e f[x1_, e] -> x1 f[x1_, i[x1_]] -> e f[x2_, f[i[x2_], x1_]] -> x1 i[e] -> e i[i[x1_]] -> x1 i[f[x1_, x2_]] -> f[i[x2], i[x1]] f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] :[font = output; output; inactive; preserveAspect; endGroup; ] {f[e, x1_] -> x1, f[i[x1_], f[x1_, x2_]] -> x2, f[i[x1_], x1_] -> e, f[x1_, e] -> x1, f[x1_, i[x1_]] -> e, f[x2_, f[i[x2_], x1_]] -> x1, i[e] -> e, i[i[x1_]] -> x1, i[f[x1_, x2_]] -> f[i[x2], i[x1]], f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]]} ;[o] {f[e, x1_] -> x1, f[i[x1_], f[x1_, x2_]] -> x2, f[i[x1_], x1_] -> e, f[x1_, e] -> x1, f[x1_, i[x1_]] -> e, f[x2_, f[i[x2_], x1_]] -> x1, i[e] -> e, i[i[x1_]] -> x1, i[f[x1_, x2_]] -> f[i[x2], i[x1]], f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]]} :[font = text; inactive; preserveAspect; ] Another way to obtain the same canonical term rewriting system is to use the Knuth-Bendix ordering, with i > f > e, weight[e] = weight[f] = 1, and weight[i] = 0. See [5]. :[font = input; Cclosed; preserveAspect; startGroup; ] weight[i] = 0; Complete[ {f[f[x, y], z] == f[x, f[y, z]], f[i[x], x] == e, f[e, x] == x}, Ordering -> KnuthBendixGT] :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] f[i[x1_], x1_] -> e :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] f[i[x1_], x1_] -> e :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], x1_] -> e f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] f[i[x1_], f[x1_, x2_]] -> x2 :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], f[x1_, x2_]] -> x2 f[i[x1_], x1_] -> e f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] f[i[e], x1_] -> x1 f[i[f[x1_, x2_]], f[x1_, f[x2_, x3_]]] -> x3 f[i[i[x1_]], x2_] -> f[x1, x2] f[x1_, e] -> x1 :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], f[x1_, x2_]] -> x2 f[i[x1_], x1_] -> e f[x1_, e] -> x1 f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] f[i[f[x1_, x2_]], f[x1_, f[x2_, x3_]]] -> x3 i[e] -> e i[i[x1_]] -> x1 :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], f[x1_, x2_]] -> x2 f[i[x1_], x1_] -> e f[x1_, e] -> x1 i[e] -> e f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] f[i[f[x1_, x2_]], f[x1_, f[x2_, x3_]]] -> x3 i[i[x1_]] -> x1 :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], f[x1_, x2_]] -> x2 f[i[x1_], x1_] -> e f[x1_, e] -> x1 i[e] -> e i[i[x1_]] -> x1 f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] f[i[f[x1_, x2_]], f[x1_, f[x2_, x3_]]] -> x3 f[x1_, i[x1_]] -> e f[x2_, f[i[x2_], x1_]] -> x1 :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], f[x1_, x2_]] -> x2 f[i[x1_], x1_] -> e f[x1_, e] -> x1 f[x1_, i[x1_]] -> e i[e] -> e i[i[x1_]] -> x1 f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] f[i[f[x1_, x2_]], f[x1_, f[x2_, x3_]]] -> x3 f[x1_, f[x2_, i[f[x1_, x2_]]]] -> e f[x2_, f[i[x2_], x1_]] -> x1 f[i[f[x1_, x2_]], x1_] -> i[x2] :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], f[x1_, x2_]] -> x2 f[i[x1_], x1_] -> e f[x1_, e] -> x1 f[x1_, i[x1_]] -> e f[x2_, f[i[x2_], x1_]] -> x1 i[e] -> e i[i[x1_]] -> x1 f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] f[i[f[x1_, x2_]], f[x1_, x3_]] -> f[i[x2], x3] f[i[f[x1_, x2_]], x1_] -> i[x2] f[x1_, f[x2_, f[i[f[x1_, x2_]], x3_]]] -> x3 f[x1_, f[x2_, i[f[x1_, x2_]]]] -> e i[f[i[x1_], x2_]] -> f[i[x2], x1] :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], f[x1_, x2_]] -> x2 f[i[x1_], x1_] -> e f[x1_, e] -> x1 f[x1_, i[x1_]] -> e f[x2_, f[i[x2_], x1_]] -> x1 i[e] -> e i[i[x1_]] -> x1 f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] i[f[x1_, x2_]] -> f[i[x2], i[x1]] :[font = message; inactive; preserveAspect; ] Complete::trace: f[e, x1_] -> x1 f[i[x1_], f[x1_, x2_]] -> x2 f[i[x1_], x1_] -> e f[x1_, e] -> x1 f[x1_, i[x1_]] -> e f[x2_, f[i[x2_], x1_]] -> x1 i[e] -> e i[i[x1_]] -> x1 i[f[x1_, x2_]] -> f[i[x2], i[x1]] f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; endGroup; ] {f[e, x1_] -> x1, f[i[x1_], f[x1_, x2_]] -> x2, f[i[x1_], x1_] -> e, f[x1_, e] -> x1, f[x1_, i[x1_]] -> e, f[x2_, f[i[x2_], x1_]] -> x1, i[e] -> e, i[i[x1_]] -> x1, i[f[x1_, x2_]] -> f[i[x2], i[x1]], f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]]} ;[o] {f[e, x1_] -> x1, f[i[x1_], f[x1_, x2_]] -> x2, f[i[x1_], x1_] -> e, f[x1_, e] -> x1, f[x1_, i[x1_]] -> e, f[x2_, f[i[x2_], x1_]] -> x1, i[e] -> e, i[i[x1_]] -> x1, i[f[x1_, x2_]] -> f[i[x2], i[x1]], f[f[x1_, x2_], x3_] -> f[x1, f[x2, x3]]} :[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, No. 1, 1981, pp. 11-21 :[font = text; inactive; preserveAspect; endGroup; ] [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 = subsubtitle; inactive; preserveAspect; endGroup; ] Last updated: 30/5/96 ^*)