the clock unary operation

Lee Martie and Johan Belinfante
2006 July 13

SetDirectory["l:"]; << goedel83.11b; << tools.m

summary

Birkhoff and Bartee illustrate the concept of unary operation with an example that they call the clock algebra.

"Garrett Birkhoff and Thomas C. Bartee, Modern Applied Algebra, \
McGraw-Hill Book Company, 1970. See page 49.";

In this notebook, two constructions of the clock algebra are related, and some of its basic properties are derived.

definition

One way to construct the clock algebra is to combine the successor function with reduction modulo x.

member[x_, clock[y_]] := 
      and[equal[natmod[succ[first[x]], y], second[x]], 
        member[first[x], y]]

Lemma.

Map[equal[0, #] &, dif[clock[x], cart[V, V]] // Normality]

subclass[clock[x_], cart[V, V]] := True

Corollary.

equal[composite[Id, clock[x]], clock[x]]

composite[Id, clock[x_]] := clock[x]

Lemma.

symdif[clock[x], composite[modulo[x], SUCC, id[x]]] // 
      RelnNormality

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

A formula for the clock algebra results:

SubstTest[equal, 0, 
      composite[Id, symdif[u, v]], {u -> composite[modulo[x], SUCC, id[x]], 
        v -> clock[x]}]

composite[modulo[x_], SUCC, id[x_]] := clock[x]

From this formula, one can derive various properties:

IminComp[composite[modulo[x], SUCC], id[x], V]

domain[clock[x_]] := nat[x]

SubstTest[FUNCTION, composite[modulo[x], funpart[y], id[x]], 
      y -> SUCC]

FUNCTION[clock[x_]] := True

Corollary.  The clock is a set.

SubstTest[member, domain[funpart[w]], V, w -> clock[x]] // 
      Reverse

member[clock[x_], V] := True

clock[x] is a unary operation

Lemma.

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
      subclass[u, 
        w], 
{u -> image[modulo[x], image[SUCC, x]], 
        v -> range[modulo[x]], w -> nat[x]}]

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

The same conclusion holds when x s zero, so one can get rid of the literal equal[0,x].

SubstTest[and, implies[p1, p2], 
        or[p1, p2], {p1 -> equal[0, x], 
          p2 -> subclass[image[modulo[x], image[SUCC, x]], nat[x]]}] // 
      Reverse

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

This clock is a unary operation:

Map[subclass[#, nat[x]] &, 
      ImageComp[composite[modulo[x], SUCC], id[x], V]]

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

Corollary.

member[clock[x], map[nat[x], nat[x]]] // AssertTest

member[clock[x_], map[nat[x_], nat[x_]]] := True

Corollary.

SubstTest[member, y, map[domain[y], domain[y]], y -> clock[x]] // 
      Reverse

member[clock[x_], UNOPS] := True

clock[x] is one-to-one

It is a bit tricky to show that clock[x] is one-to-one.  The basic idea is to use the pigeon-hole principle, showing that its domain and range are equal. The finiteness is easy:

SubstTest[member, domain[funpart[y]], FINITE, y -> clock[x]] // 
      Reverse

member[clock[x_], FINITE] := True

The range of clock[x] gets rewritten when one adds a nat wrapper.  So, if one wants to proceed with such wrappers, one needs this corollary of an inclusion derived in the preceding section.

SubstTest[subclass, image[modulo[w], image[SUCC, w]], nat[w], 
      w -> nat[x]]

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

The reverse inclusion must also be shown.  One can start with these observations:

SubstTest[image, modulo[nat[x]], 
      union[u, v], {u -> nat[x], v -> set[nat[x]]}]

image[modulo[nat[x_]], succ[nat[x_]]] := 
      union[nat[x], set[0]]

SubstTest[image, modulo[nat[x]], 
        union[u, v], {u -> dif[succ[nat[x]], set[0]], 
          v -> set[0]}] // Reverse

union[
        image[modulo[nat[x_]], 
          intersection[complement[set[0]], succ[nat[x_]]]], set[0]] := 
      union[nat[x], set[0]]

Map[union[set[0], #] &, 
      ImageComp[composite[modulo[nat[x]], SUCC], id[nat[x]], V]]

union[range[clock[nat[x_]]], set[0]] := 
      union[nat[x], set[0]]

Lemma.  If nat[x] is not 0, then 0 belongs to range[clock[nat[x]]].

SubstTest[implies, subclass[u, v], 
      subclass[image[w, u], 
        image[w, v]], 
{u -> set[nat[x]], 
        v -> intersection[complement[set[0]], succ[nat[x]]], 
        w -> modulo[nat[x]]}]

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

Restatement:

Map[or[equal[0, nat[x]], member[0, #]] &, 
      ImageComp[composite[modulo[nat[x]], SUCC], id[nat[x]], V]]

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

Corollary.

SubstTest[implies, and[subclass[u, union[v, set[0]]], member[0, v]], 
      subclass[u, v], {u -> nat[x], 
        v -> range[clock[nat[x]]]}]

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

This suffices to establish the this inclusion:

Map[not, 
      SubstTest[and, implies[p1, p2], implies[p2, p3], 
        not[implies[p1, p3]], {p1 -> not[empty[nat[x]]], 
          p2 -> member[0, range[clock[nat[x]]]], 
          p3 -> subclass[nat[x], range[clock[nat[x]]]]}]]

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

The reverse inclusion also holds:

SubstTest[subclass, range[clock[w]], nat[w], 
      w -> nat[x]]

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

The two inclusions can be combined into an equation:

SubstTest[and, subclass[u, v], 
        subclass[v, u], {u -> range[clock[nat[x]]], v -> nat[x]}] // 
      Reverse

range[clock[nat[x_]]] := nat[x]

The next step is to remove the nat wrapper.

SubstTest[implies, equal[x, nat[y]], equal[range[clock[x]], nat[x]], 
      y -> x]

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

The same conclusion can be derived when x is not a number:

ImageComp[composite[modulo[x], SUCC], id[x], V] // Reverse

image[modulo[x_], image[SUCC, x_]] := range[clock[x]]

SubstTest[implies, and[equal[0, z], not[member[x, omega]]], 
      equal[image[z, image[SUCC, x]], nat[x]], 
      z -> modulo[x]]

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

Combining the cases of numbers and non-numbers yields:

SubstTest[and, implies[p1, p2], 
      or[p1, p2], {p1 -> member[x, omega], 
        p2 -> equal[range[clock[x]], nat[x]]}]

range[clock[x_]] := nat[x]

Applying the pigeonhole principle, one finds that clock[x] is also one-to-one.

SubstTest[implies, 
      and[FUNCTION[w], member[w, FINITE], equal[domain[w], range[w]]], 
      FUNCTION[inverse[w]], 
w -> clock[x]]

FUNCTION[inverse[clock[x_]]] := True

another construction of the clock algebra

One can construct a clock algebra as the function union[cart[set[nat[x]], set[0]], composite[SUCC, id[nat[x]]]] which takes each number less than nat[x] to its successor, and nat[x] itself to 0.  Lee Martie made the following key observation about this construction:

SubstTest[dif, 
      union[cart[set[nat[x]], set[0]], composite[SUCC, id[nat[x]]]], 
      composite[modulo[succ[nat[x]]], SUCC, id[y]], 
      y -> succ[nat[x]]]

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

Lemma.

SubstTest[equal, 0, 
        dif[u, v], {u -> 
            union[cart[set[nat[x]], set[0]], composite[SUCC, id[nat[x]]]], 
          v -> clock[succ[nat[x]]]}] // Reverse

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

The equality of the two clocks follows:

SubstTest[implies, and[subclass[u, v], FUNCTION[v]], 
      equal[u, composite[v, id[domain[u]]]], {u -> 
          union[cart[set[nat[x]], set[0]], composite[SUCC, id[nat[x]]]], 
        v -> clock[succ[nat[x]]]}]

union[cart[set[nat[x_]], set[0]], composite[SUCC, id[nat[x_]]]] := 
      clock[succ[nat[x]]]

This is a unary operation, with domain and range equal to succ[nat[x]].

SubstTest[member, clock[w], map[nat[w], nat[w]], 
      w -> succ[nat[x]]]

member[clock[succ[nat[x_]]], map[succ[nat[x_]], succ[nat[x_]]]] := 
      True

reify rule

SubstTest[reify, x, composite[modulo[f[x]], z, id[f[x]]], 
      z -> SUCC]

reify[x_, clock[y_]] := 
      composite[SWAP, RIF, id[cart[V, SUCC]], 
        intersection[composite[inverse[SECOND], inverse[FIRST], reify[x, y]], 
          composite[inverse[FIRST], SWAP, inverse[rotate[NATMOD]], 
            VERTSECT[reify[x, y]]]]]