ONT Re: Differential Logic
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
DLOG. Note D7
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
The Analogy Between Real and Boolean Types
| Measurement consists in correlating our subject matter with the series of
| real numbers; and such correlations are desirable because, once they are
| set up, all the well-worked theory of numerical mathematics lies ready at
| hand as a tool for our further reasoning.
|
| W.V. Quine, 'Mathematical Logic', [Qui, 7]
There are two further reasons why I am spending so much time on a careful
treatment of types, and they both have to do with our being able to take
full computational advantage of certain dimensions of flexibility in the
types that apply to terms. First, the domains of differential geometry
and logic programming are connected by analogies between real and boolean
types of the same pattern. Second, the types involved in these patterns
have important isomorphisms connecting them that apply on both the real
and the boolean sides of the picture.
Amazingly enough, these isomorphisms are themselves schematized by the
axioms and theorems of propositional logic. This fact is known as the
"propositions as types" (PAT) analogy [How]. In another formulation
it says that terms are to types as proofs are to propositions. This
principle seems to have more implications for our subject than I can
fully comprehend at present, though I sense that they must be crucial.
(Cf. [LaS, 42-46] and [SeH] for discussion and further references.)
To anticipate the bearing of these issues on our immediate topic,
Table 3 sketches a partial overview of the PAT analogy that may
serve to illustrate the paradigm that I have in mind.
Table 3. Analogy of Real and Boolean Types
o-------------------------o-------------------------o-------------------------o
| Real Domain R | <-> | Boolean Domain B |
o-------------------------o-------------------------o-------------------------o
| R^n | Basic Space | B^n |
o-------------------------o-------------------------o-------------------------o
| R^n -> R | Function Space | B^n -> B |
o-------------------------o-------------------------o-------------------------o
| (R^n -> R) -> R | Tangent Vector | (B^n -> B) -> B |
o-------------------------o-------------------------o-------------------------o
| R^n -> ((R^n -> R) -> R)| Vector Field | B^n -> ((B^n -> B) -> B)|
o-------------------------o-------------------------o-------------------------o
| (R^n x (R^n -> R)) -> R | ditto | (B^n x (B^n -> B)) -> B |
o-------------------------o-------------------------o-------------------------o
| ((R^n -> R) x R^n) -> R | ditto | ((B^n -> B) x B^n) -> B |
o-------------------------o-------------------------o-------------------------o
| (R^n -> R) -> (R^n -> R)| Derivation | (B^n -> B) -> (B^n -> B)|
o-------------------------o-------------------------o-------------------------o
| R^n -> R^m | Basic Transformation | B^n -> B^m |
o-------------------------o-------------------------o-------------------------o
| (R^n -> R) -> (R^m -> R)| Function Transformation | (B^n -> B) -> (B^m -> B)|
o-------------------------o-------------------------o-------------------------o
| ... | ... | ... |
o-------------------------o-------------------------o-------------------------o
The Table exhibits a sample of likely parallels between the real and boolean domains.
The central column gives a selection of terminology that I borrow from typical usage
in differential geometry and extend in its meaning to the logical side of the Table.
These are the varieties of spaces that come up when we turn to analyzing the dynamics
of processes that followe their courses through the states of an arbitrary space X.
Moreover, when it becomes necessary to approach situations of overwhelming dynamic
complexity in a succession of qualitative reaches, then the methods of logic that
are afforded by the boolean domains, with their declarative means of synthesis
and deductive modes of analysis, supply a natural battery of tools for the task.
It is usually expedient to take these spaces two at a time, in dual pairs of the
form X and (X -> K). In general, one creates pairs of type schemas by replacing
any space X with its dual (X -> K), for example, pairing the type X -> Y with the
type (X -> K) -> (Y -> K), and X x Y with (X -> K) x (Y -> K). Here, I am using
the word "dual" in its latger sense to mean all of the functionals, not just the
linear ones. Given any function f : X -> K, the "converse" or inverse relation
corresponding to f is denoted as f^(-1), and the subsets of X that are defined
by f^(-1)(k), taken over k in K, are called the "fibers" or the "level sets"
of the function f.
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o