monotonicity rules for map and MAP

Johan G. F. Belinfante
2003 May 7

<< goedel52.r63; << tools.m

summary

A monotonicity rule for map[x,y], and a corresponding property for the function MAP are derived in this notebook.  The class of mappings from  x  to  y  is defined by:

class[w, 
      and[FUNCTION[w], equal[domain[w], x], 
        subclass[range[w], y]]]

The binary function  MAP  is defined by:

lambda[pair[x, y], map[x, y]]

The derivation is mainly of interest as an illustration of how one goes about about eliminating set-variables  from statements.

monotonicity of map[x,y]

The constructor  map[x,y]  is monotone with respect to its second argument.

implies[subclass[y, z], subclass[map[x, y], map[x, z]]] // 
      AssertTest

or[not[subclass[y_, z_]], subclass[map[x_, y_], map[x_, z_]]] := 
      True

monotonicity in terms of MAP

The derivation of a variable-free  version of this law is a bit tricky.  One way to do it is to make use of the function LEFT[x].

class[pair[u, pair[v, w]], and[equal[v, x], equal[u, w]]]

The derivation begins with an application of the tool VSRerenormality. This tool builds in two assert's.

intersection[S, 
        composite[inverse[LEFT[x]], inverse[MAP], complement[S], MAP, 
          LEFT[x]]] // VSRerenormality

intersection[S, 
        composite[inverse[LEFT[x_]], inverse[MAP], complement[S], MAP, 
          LEFT[x_]]] := 0

From this one derives a conditional inclusion:

SubstTest[equal, 0, 
        dif[u, v], {u -> S, 
          v -> complement[
              composite[inverse[LEFT[x]], inverse[MAP], complement[S], MAP, 
                LEFT[x]]]}] // Reverse

or[not[member[x_, V]], 
        subclass[S, 
          composite[inverse[LEFT[x_]], inverse[MAP], S, MAP, LEFT[x_]]]] := 
      True

The condition that  x  be a set is necessary as well as sufficient:

SubstTest[implies, subclass[u, v], 
      subclass[image[inverse[u], singleton[0]], 
        image[inverse[v], singleton[0]]], {u -> S, 
        v -> composite[inverse[LEFT[x]], inverse[MAP], S, MAP, 
            LEFT[x]]}]

or[member[x_, V], 
        not[subclass[S, 
            composite[inverse[LEFT[x_]], inverse[MAP], S, MAP, LEFT[x_]]]]] := 
      True

Thus one can introduce a rewrite rule:

equiv[
      subclass[S, 
        composite[inverse[LEFT[x]], inverse[MAP], S, MAP, LEFT[x]]], 
      member[x, V]]

subclass[S, 
        composite[inverse[LEFT[x_]], inverse[MAP], S, MAP, LEFT[x_]]] := 
      member[x, V]

Eliminating the inverse's is easy:

\(SubstTest[implies, subclass[u, v], 
      subclass[composite[w, u], composite[w, v]], 
	{u -> S, 
        v -> composite[inverse[LEFT[x]], inverse[MAP], S, MAP, 
            LEFT[x]], 
		w -> composite[MAP, LEFT[x]]}]\)

or[not[member[x_, V]], 
        subclass[composite[MAP, LEFT[x_], S], composite[S, MAP, LEFT[x_]]]] := 
      True

This conditional inclusion also holds without the membership condition:

\(SubstTest[implies, equal[0, u], 
      subclass[u, v], 
	{u -> composite[MAP, LEFT[x], S], 
        v -> composite[S, MAP, LEFT[x]]}]\)

or[member[x_, V], 
        subclass[composite[MAP, LEFT[x_], S], composite[S, MAP, LEFT[x_]]]] := 
      True

Thus one can simplify the statement:

\(SubstTest[and, implies[p1, p2], 
        implies[not[p1], p2], 
	{p1 -> member[x, V], 
          p2 -> subclass[composite[MAP, LEFT[x], S], 
              composite[S, MAP, LEFT[x]]]}] // Reverse\)

subclass[composite[MAP, LEFT[x_], S], composite[S, MAP, LEFT[x_]]] := 
      True

This can be viewed as a statement of subcommutativity.

subcommute[composite[MAP, LEFT[x]], S]

The variable  x  that appears in this statement can be eliminated as follows:

Map[equal[V, #] &, 
        SubstTest[class, x, subcommute[composite[z, LEFT[x]], S], z -> MAP]] // 
      Reverse

subclass[
        composite[FIRST, 
          intersection[composite[inverse[MAP], FIRST], 
            composite[inverse[SECOND], S, SECOND]]], 
        rotate[composite[S, MAP, SWAP]]] := True

This variable-free  statement can be simplified by applying  flip and  rotate :

\(SubstTest[implies, subclass[u, v], 
      subclass[flip[u], 
        flip[v]], 
	{u -> 
          composite[FIRST, 
            intersection[composite[inverse[MAP], FIRST], 
              composite[inverse[SECOND], S, SECOND]]], 
        v -> rotate[composite[S, MAP, SWAP]]}]\)

subclass[
        composite[FIRST, 
          intersection[composite[inverse[MAP], SECOND], 
            composite[inverse[SECOND], S, FIRST]]], 
        composite[rotate[composite[S, MAP, SWAP]], SWAP]] := True

\(SubstTest[subclass, rotate[u], 
      rotate[v], 
	{u -> 
          composite[FIRST, 
            intersection[composite[inverse[MAP], SECOND], 
              composite[inverse[SECOND], S, FIRST]]], 
        v -> composite[rotate[composite[S, MAP, SWAP]], SWAP]}]\)

This is the final version of the variable-free  formulation of the monotonicity rule:

subclass[composite[MAP, cross[Id, S]], composite[S, MAP]] := 
      True