image[V,-] rules for group elements

Johan G. F. Belinfante
2009 February 12

SetDirectory["l:"];  << goedel.09feb11b; << tools.m

summary

Knuth and Bendix long ago proposed an algorithm that attempts to transform a given set of equations into a convergent rewrite system.  An application of this algorithm yields a set of ten rewrite rules for group application.

"D. E. Knuth and P. B. Bendix, Simple word problems in universal algebras, in Computational Problems in Abstract Algebra, edited by J. Leech, pp. 263-297, Oxford, Pergamon Press, 1970.";

These ten rules are also discussed on page 19 in the following reference:

"Leo Bachmair, Canonical Equational Proofs, Birkhäuser, Boston, 1991.";

The Knuth-Bendix rewrite rules for group application are approximated by ten rewrite rules in the GOEDEL program.  The fact that these rules are about a group gp[x] is made known to the computer via presence of the gp wrapper , but since the computer still has no way of knowing that the elements to which the group application is being applied are members of range[gp[x]], the rules also contain image[V, ---] expressions for which additional rewrite rules must be supplied. One such rule is derived in this notebook.

the ten Knuth Bendix rules for group application

The associative law for groups is represented by a rewrite rule that puts no conditions on the three variables u, v and w.  No restriction on the variables is needed because APPLY occurs on both sides of the equation  u · (v · w) = (u · v) · w.  If one or more of these is not a member of range[gp[x]], then this equation reduces to V = V.

APPLY[gp[x], PAIR[u, APPLY[gp[x], PAIR[v, w]]]]

The dual pair of rules that express the two axioms about the group identity element e[gp[x]] do introduce an image[V, - ] term, however:

APPLY[gp[x], PAIR[e[gp[x]], u]]

APPLY[gp[x], PAIR[u, e[gp[x]]]]

The same holds for the two rewrite rules that represent the two group axioms about inverses:

APPLY[gp[x], PAIR[APPLY[inv[gp[x]], u], u]]

APPLY[gp[x], PAIR[u, APPLY[inv[gp[x]], u]]]

The theorem that the identity element is its own inverse involves no variables for elements, and is therefore clean:

APPLY[inv[gp[x]], e[gp[x]]]

The theorem about the inverse of a product involves variables for group elements, but it is nonetheless clean because, like the associative law, an APPLY occurs on both sides of the equation.

APPLY[inv[gp[x]], APPLY[gp[x], PAIR[u, v]]]

The theorem about the inverse of an inverse involves one variable for a group element, and needs a corresponding image[V, -] modification.

APPLY[inv[gp[x]], APPLY[inv[gp[x]], u]]

Finally there is a dual pair of rewrite rules that follow from a combination of the laws of inverses and the associative law.  These rules both involve two variables representing group elements, and both need image[V, -] modifications.

APPLY[gp[x], 
      PAIR[APPLY[gp[x], PAIR[u, v]], APPLY[inv[gp[x]], v]]]

APPLY[gp[x], 
      PAIR[APPLY[gp[x], PAIR[u, APPLY[inv[gp[x]], v]]], v]]

image[V, - ] rules

Only the inverse of an element of a group can be an element of the group.

member[APPLY[inv[gp[x]], u], range[gp[x]]]

The corresponding image[V, - ] rule for this fact is already available:

image[V, 
      intersection[range[gp[x]], set[APPLY[inv[gp[x]], u]]]]

A similar result holds for the product of two group elements.

Theorem.  The product  u · v  belongs to range[gp[x]] if and only if both u and v belong to range[gp[x]].

SubstTest[member, APPLY[funpart[t], PAIR[u, v]], range[funpart[t]], 
        t -> gp[x]] // Reverse

member[APPLY[gp[x_], PAIR[u_, v_]], range[gp[x_]]] := 
      and[member[u, range[gp[x]]], member[v, range[gp[x]]]]

Corollary.  The corresponding image[V, - ] rule is needed for rewriting.

image[V, intersection[range[gp[x]], set[APPLY[gp[x], PAIR[u, v]]]]] // 
      Normality

image[V, 
        intersection[range[gp[x_]], set[APPLY[gp[x_], PAIR[u_, v_]]]]] := 
      intersection[image[V, intersection[range[gp[x]], set[u]]], 
        image[V, intersection[range[gp[x]], set[v]]]]