word monoids

Johan G. F. Belinfante
2009 January 29

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

summary

The binary operation composite[id[P[cart[omega, x]]], JOIN]  of concatenating finite words whose letters come from a class x is a (possibly big) monoid with the empty word 0 as identity.

ids

Lemma.  The empty word is an identity element.

member[0, ids[composite[id[P[cart[omega, x]]], JOIN]]] // 
      AssertTest

(% /. x -> x_) /. Equal -> SetDelayed

Corollary.

Map[not, 
        SubstTest[implies, member[0, t], not[empty[t]], 
          t -> ids[composite[id[P[cart[omega, x]]], JOIN]]]] // 
      Reverse

(% /. x -> x_) /. Equal -> SetDelayed

Theorem.  An implication in one direction.

SubstTest[implies, and[member[t, SEMIGPS], not[empty[ids[t]]]], 
        member[t, MONOIDS], t -> composite[id[P[cart[omega, x]]], JOIN]] // 
      Reverse

(% /. x -> x_) /. Equal -> SetDelayed

Converse.

SubstTest[implies, member[u, v], 
        member[u, V], {u -> composite[id[P[cart[omega, x]]], JOIN], 
          v -> MONOIDS}] // Reverse

(% /. x -> x_) /. Equal -> SetDelayed

Corollary.  Combine the implications in both directions into a rewrite rule.

equiv[member[composite[id[P[cart[omega, x]]], JOIN], MONOIDS], 
      member[x, V]]

member[composite[id[P[cart[omega, x_]]], JOIN], MONOIDS] := 
      member[x, V]

One can generalize this result to the case that x is an arbitrary class, not necessarily a set.  In that case, one obtains what is sometimes called a big monoid, that is, an associative function whose domain is the cartesian square of its range, possessing a single identity element.  A generalization of the uniqueness theorem for identities of binary operations is needed for this task.  The following theorem provides the needed tool to handle this in full generality.

Theorem.  If domain[x] is a cartesian square, then ids[x] is either empty or a singleton.

SubstTest[implies, equal[u, v], 
        equal[image[t, u], image[t, v]], {t -> id[cartsq[ids[x]]], 
          u -> domain[x], v -> cartsq[fix[domain[x]]]}] // 
      Reverse

or[equal[0, ids[x_]], member[ids[x_], range[SINGLETON]], 
        not[equal[cart[fix[domain[x_]], fix[domain[x_]]], domain[x_]]]] := 
      True

Lemma.

Map[implies[and[#, empty[ids[x]]], equal[ids[x], set[e[x]]]] &, 
      SubstTest[equal, t, set[A[t]], t -> ids[x]]]

or[equal[ids[x_], set[e[x_]]], not[equal[0, ids[x_]]]] := 
      True

Lemma.

Map[implies[#, equal[ids[x], set[e[x]]]] &, 
        SubstTest[equal, t, set[A[t]], t -> ids[x]]] // 
      MapNotNot

or[equal[ids[x_], set[e[x_]]], not[member[ids[x_], range[SINGLETON]]]] := 
      True

Corollary.  If domain[x] is a cartesian square, then ids[x] = set[e[x]].

Map[not, 
        SubstTest[and, implies[p1, or[p2, p3]], implies[p2, p4], 
          implies[p3, p4], 
          not[implies[p1, p4]], {p1 -> 
              equal[cart[fix[domain[x]], fix[domain[x]]], domain[x]], 
            p2 -> equal[0, ids[x]], p3 -> member[ids[x], range[SINGLETON]], 
            p4 -> equal[ids[x], set[e[x]]]}]] // Reverse

or[equal[ids[x_], set[e[x_]]], 
        not[equal[cart[fix[domain[x_]], fix[domain[x_]]], domain[x_]]]] := 
      True

Lemma.

SubstTest[implies, 
        equal[cart[fix[domain[t]], fix[domain[t]]], domain[t]], 
        equal[ids[t], set[e[t]]], 
        t -> composite[id[P[cart[omega, x]]], JOIN]] // Reverse

(% /. x -> x_) /. Equal -> SetDelayed

Theorem.

SubstTest[implies, and[member[t, u], equal[u, v]], 
        member[t, v], {t -> 0, 
          u -> ids[composite[id[P[cart[omega, x]]], JOIN]], 
          v -> set[e[composite[id[P[cart[omega, x]]], JOIN]]]}] // 
      Reverse

e[composite[id[P[cart[omega, x_]]], JOIN]] := 0

Lemma.

SubstTest[implies, 
        equal[cart[fix[domain[t]], fix[domain[t]]], domain[t]], 
        equal[ids[t], set[e[t]]], 
        t -> composite[id[P[cart[omega, x]]], JOIN]] // Reverse

(% /. x -> x_) /. Equal -> SetDelayed

Theorem.  The inclusion in the preceding lemma is actually an equation which will be made into a rewrite rule.

equal[ids[composite[id[P[cart[omega, x]]], JOIN]], set[0]]

ids[composite[id[P[cart[omega, x_]]], JOIN]] := set[0]

Theorem.  The only word that has an inverse is the empty word, which is its own inverse.

SubstTest[intersection, image[inverse[t], ids[t]], 
      inverse[image[inverse[t], ids[t]]], 
      t -> composite[id[P[cart[omega, x]]], JOIN]]

inv[composite[id[P[cart[omega, x_]]], JOIN]] := 
      cart[set[0], set[0]]

Observation.  The case x = V reduces to JOIN.

equal[composite[id[P[cart[omega, V]]], JOIN], JOIN]

composite[id[P[cart[omega, V]]], JOIN] := JOIN

Corollary.

SubstTest[inv, composite[id[P[cart[omega, x]]], JOIN], x -> V] // 
      Reverse

inv[JOIN] := cart[set[0], set[0]]