images and inverse images of eval[x]

Johan G. F. Belinfante
2006 November 3

SetDirectory["l:"];  << goedel87.01a; << tools.m

summary

Rewrite rules for the classes image[eval[x], y] and image[inverse[eval[x]], y] are derived in this notebook, and some examples in arithmetic in arithmetic are provided to illustrate them.

image[eval[x], y] formula

The basic result is this:

ImageComp[inverse[LEFT[x]], composite[inverse[E], FUNPART], 
      y]

image[eval[x_], y_] := image[U[image[FUNPART, y]], set[x]]

This formula requires one to simplify the expression image[FUNPART, x].  One can automate this to a large extent, as will be seen below.

a rewrite rule for image[FUNPART, x]

Lemma

ImageComp[FUNPART, id[FUNS], x] // Reverse

image[FUNPART, intersection[FUNS, x_]] := 
      intersection[FUNS, x]

Theorem.

SubstTest[implies, equal[x, y], 
        equal[image[w, x], image[w, y]], {y -> intersection[x, FUNS], 
          w -> FUNPART}] // Reverse

or[equal[x_, image[FUNPART, x_]], not[subclass[x_, FUNS]]] := 
      True

This is best made into a conditional rewrite rule:

image[FUNPART, x_] := x  /;  subclass[x, FUNS]

some examples

The rewrite rules derived above suffice for numerous special cases.  For example:

image[eval[x], map[y, z]]

In particular, the following statement says that if x belongs to a set y, then every member of z is the value at x of some mapping from y to z.  This is hardly surprising, because there is a constant function which does the job.  A technical note: Although x and y must be sets, the class z need not be a set.

implies[and[member[x, y], member[y, V]], 
      equal[z, image[eval[x], map[y, z]]]]

To obtain more interesting examples, one can consider classes of mappings that satisfy some extra conditions.  An example of interest in the arithmetic of natural numbers is the set binhom[NATADD,NATADD] of all endomorphisms of natural number addition.  This subset of map[omega, omega] is the set of all functions of the form times[x] for some natural number x.  In other words, this is the set of all linear functions, functions whose graphs in the plane cart[omega, omega] are straight lines through the origin with slopes 0, 1, 2, ... .  The only constant function in this collection is times[0].   In this case the values of these functions at x are all multiples of x.

image[eval[x], binhom[NATADD, NATADD]]

More generally, the set of values at x of the class of binary homomorphisms from y to z is the vertical section of the union of this collection of functions.

image[eval[x], binhom[y, z]]

a rewrite rule for core

In the next section the class image[INVERSE, range[PLUS]] of non-positive integers is considered.  The union of this class of functions leads to an expression involving core.  More generally, one may encounter expressions of this form:

U[image[INVERSE, x]]

To automate the simplification of such expressions, a rewrite rule is desirable.  A basic result is this:

SubstTest[implies, equal[x, z], equal[U[x], U[z]], 
        z -> intersection[x, P[y]]] // Reverse

or[equal[core[x_, y_], U[x_]], not[subclass[U[x_], y_]]] := 
      True

The following conditional rule suffices for many applications, and in particular for the example encountered in the next section.

core[x_, y_]  :=  U[x]  /;  subclass[U[x], y]

adding and subtracting

The following says that for any natural number nat[x], one can obtain any natural number greater than or equal to nat[x] by adding some natural number to it.

image[eval[nat[x]], range[PLUS]]

There is a corresponding result for subtraction, but for that case a new rewrite rule is needed:

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
        subclass[u, w], 
{u -> image[INVERSE, range[PLUS]], 
          v -> Z, w -> FUNS}] // Reverse

subclass[image[INVERSE, range[PLUS]], FUNS] := True

The following result is now obtained, which says that one can obtain any natural number less than or equal to nat[x] by subtracting some natural number from nat[x].

image[eval[nat[x]], image[INVERSE, range[PLUS]]]

The following formula says that one can obtain any natural number from nat[x] by either adding or subtracting some natural number.

image[eval[nat[x]], Z]

Corollary.  The set omega of all natural numbers is the union of the set of natural numbers greater than or equal to nat[x] and the set of natural numbers less than or equal to nat[x].  These two sets are not disjoint because the number nat[x] itself belongs to both of them.

SubstTest[image, eval[nat[x]], 
      union[u, v], {u -> range[PLUS], 
        v -> image[INVERSE, range[PLUS]]}]

union[intersection[omega, complement[nat[x_]]], succ[nat[x_]]] := 
      omega

a rule for inverse images

For inverse images, one has the following membership rule:

equiv[member[x, image[inverse[eval[y]], z]], 
        and[member[x, V], member[y, image[inverse[funpart[x]], z]]]] // 
      assert

member[x_, image[inverse[eval[y_]], z_]] := 
      and[member[x, V], member[y, image[inverse[funpart[x]], z]]]

This rule generalizes one for the the special case z = V:

member[x, domain[eval[y]]]