ONT Re: Differential Logic -- Series A
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
DLOG. Note A5
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
The enlargement operator E, also known as the "shift operator",
has many interesting and very useful properties in its own right,
so let us not fail to observe a few of the more salient features
that play out on the surface of our simple example, f(x, y) = xy.
Introduce a suitably generic definition of the extended universe of discourse:
Let U = X_1 x ... x X_k and EU = U x dU = X_1 x ... x X_k x dX_1 x ... x dX_k.
For a proposition f : X_1 x ... x X_k -> B,
the (first order) "enlargement" of f is the
proposition Ef : EU -> B that is defined by:
Ef(x_1, ..., x_k, dx_1, ..., dx_k) = f(x_1 + dx_1, ..., x_k + dx_k).
It should be noted that the so-called "differential variables" dx_j
are really just the same kind of boolean variables as the other x_j.
It is conventional to give the additional variables these brands of
inflected names, but whatever extra connotations we might choose to
attach to these syntactic conveniences are wholly external to their
purely algebraic meanings.
For the example f(x, y) = xy, we obtain:
Ef(x, y, dx, dy) = (x + dx)(y + dy).
Given that this expression uses nothing more than the "boolean ring"
operations of addition (+) and multiplication (.), it is permissible
to "multiply things out" in the usual manner to arrive at the result:
Ef(x, y, dx, dy) = x y + x dy + y dx + dx dy
To understand what this means in logical terms, for instance, as expressed
in a boolean expansion or a "disjunctive normal form" (DNF), it is perhaps
a little better to go back and analyze the expression the same way that we
did for Df. Thus, let us compute the value of the enlarged proposition Ef
at each of the points in the universe of discourse U = X x Y.
o-------------------------------------------------o
| |
| x dx y dy |
| o---o o---o |
| \ | | / |
| \ | | / |
| \| |/ |
| @=@ |
| |
o-------------------------------------------------o
| Ef = (x, dx) (y, dy) |
o-------------------------------------------------o
o-------------------------------------------------o
| |
| dx dy |
| o---o o---o |
| \ | | / |
| \ | | / |
| \| |/ |
| @=@ |
| |
o-------------------------------------------------o
| Ef|xy = (dx) (dy) |
o-------------------------------------------------o
o-------------------------------------------------o
| |
| o |
| dx | dy |
| o---o o---o |
| \ | | / |
| \ | | / |
| \| |/ |
| @=@ |
| |
o-------------------------------------------------o
| Ef|x(y) = (dx) dy |
o-------------------------------------------------o
o-------------------------------------------------o
| |
| o |
| | dx dy |
| o---o o---o |
| \ | | / |
| \ | | / |
| \| |/ |
| @=@ |
| |
o-------------------------------------------------o
| Ef|(x)y = dx (dy) |
o-------------------------------------------------o
o-------------------------------------------------o
| |
| o o |
| | dx | dy |
| o---o o---o |
| \ | | / |
| \ | | / |
| \| |/ |
| @=@ |
| |
o-------------------------------------------------o
| Ef|(x)(y) = dx dy |
o-------------------------------------------------o
Given the sort of data that arises from this form of analysis,
we can now fold the disjoined ingredients back into a boolean
expansion or a DNF that is equivalent to the proposition Ef.
Ef = xy Ef_xy + x(y) Ef_x(y) + (x)y Ef_(x)y + (x)(y) Ef_(x)(y)
Here is a summary of the result, illustrated by means of a digraph picture,
where the "no change" element (dx)(dy) is drawn as a loop at the point x y.
o-------------------------------------------------o
| f = x y |
o-------------------------------------------------o
| |
| Ef = x y (dx)(dy) |
| |
| + x (y) (dx) dy |
| |
| + (x) y dx (dy) |
| |
| + (x)(y) dx dy |
| |
o-------------------------------------------------o
| |
| (dx) (dy) |
| .--->---. |
| \ / |
| \x y/ |
| \ / |
| x (y) o-------------->o<--------------o (x) y |
| (dx) dy ^ dx (dy) |
| | |
| | |
| dx | dy |
| | |
| | |
| | |
| o |
| (x) (y) |
| |
o-------------------------------------------------o
We may understand the enlarged proposition Ef
as telling us all the different ways to reach
a model of f from any point of the universe U.
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
http://www.cs.bsu.edu/homepages/mighty/history.html
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o