ONT Re: Differential Logic
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
DLOG. Note D79
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Transformations of Type B^2 -> B^2 (cont.)
In their application to the present example, namely, the
logical transformation F = <f, g> = <((u)(v)), ((u, v))>,
the operators E and D respectively produce the enlarged
map EF = <Ef, Eg> and the difference map DF = <Df, Dg>,
whose components can be given as follows, if the reader,
in lieu of a special font for the logical parentheses,
can forgive a syntactically bilingual formulation:
o-------------------------------------------------o
| |
| Ef = ((u + du)(v + dv)) |
| |
| Eg = ((u + du, v + dv)) |
| |
o-------------------------------------------------o
o-------------------------------------------------o
| |
| Df = ((u)(v)) + ((u + du)(v + dv)) |
| |
| Dg = ((u, v)) + ((u + du, v + dv)) |
| |
o-------------------------------------------------o
But these initial formulas are purely definitional, and help us little
in understanding either the purpose of the operators or the meaning of
their results. Working symbolically, let us apply the same method to
the separate components f and g that we earlier used on J. This work
is recorded in Appendix 1 and a summary of the results is presented
in Tables 66-i and 66-ii.
Table 66-i. Computation Summary for f<u, v> = ((u)(v))
o--------------------------------------------------------------------------------o
| |
| !e!f = uv. 1 + u(v). 1 + (u)v. 1 + (u)(v). 0 |
| |
| Ef = uv. (du dv) + u(v). (du (dv)) + (u)v.((du) dv) + (u)(v).((du)(dv)) |
| |
| Df = uv. du dv + u(v). du (dv) + (u)v. (du) dv + (u)(v).((du)(dv)) |
| |
| df = uv. 0 + u(v). du + (u)v. dv + (u)(v). (du, dv) |
| |
| rf = uv. du dv + u(v). du dv + (u)v. du dv + (u)(v). du dv |
| |
o--------------------------------------------------------------------------------o
Table 66-ii. Computation Summary for g<u, v> = ((u, v))
o--------------------------------------------------------------------------------o
| |
| !e!g = uv. 1 + u(v). 0 + (u)v. 0 + (u)(v). 1 |
| |
| Eg = uv.((du, dv)) + u(v). (du, dv) + (u)v. (du, dv) + (u)(v).((du, dv)) |
| |
| Dg = uv. (du, dv) + u(v). (du, dv) + (u)v. (du, dv) + (u)(v). (du, dv) |
| |
| dg = uv. (du, dv) + u(v). (du, dv) + (u)v. (du, dv) + (u)(v). (du, dv) |
| |
| rg = uv. 0 + u(v). 0 + (u)v. 0 + (u)(v). 0 |
| |
o--------------------------------------------------------------------------------o
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o