ONT Re: Differential Logic
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
DLOG. Note D9
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Propositions as Types and Higher Order Types
The arrangement of types collected in Table 3 can
serve as a good introduction to several ideas about
"higher order propositional expressions" (HOPE's) and
also about the "propositions as types" (PAT) isomorphism.
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
First, observe that the type of a "Tangent Vector at a Point",
also known as a "directional derivative" at that point, has the
form (K^n -> K) -> K, where K is the chosen ground field, in the
present case either R or B. At a point in a space of type K^n,
a directional derivative operator !q! takes a function on that
space, an f of type (K^n -> K), and maps it to a ground field
value of type K. This value is known as the "derivative" of
f in the direction !q! [Che46, 76-77]. In the boolean case,
!q! : (B^n -> B) -> B has the form of a proposition about
propositions, in other words, a proposition of the next
higher type.
Next, by way of illustrating the propositions as types theme, consider
a proposition of the form X => (Y => Z). One knows from propositional
calculus that this is logically equivalent to a proposition of the form
(X & Y) => Z. But this equivalence should remind us of the functional
isomorphism that exists between a construction of the type X -> (Y -> Z)
and a construction of the type (X x Y) -> Z. The propositions as types
analogy permits us to take a functional type like this and, under the
right conditions, replace the functional arrows "->" and products "x"
with the respective logical arrows "=>" and products "&". Accordingly,
viewing the result as a proposition, we can employ axioms and theorems
of propositional calculus to suggest appropriate isomorphisms among the
categorical and functional constructions.
Finally, examine the middle four rows of Table 3. These display
a series of isomorphic types that stretch from the categories that
are labeled "Vector Field" to those that are labeled "Derivation".
A "vector field", also known as an "infinitesimal transformation",
associates a tangent vector at a point with each point of a space.
In symbols, a vector field is a function !X! : X -> |_| !X!_x that
assigns to each point x of the space X a tangent vector !X!_x to X
at that point [Che46, 82-83]. If X is of type K^n, then !X! is of
type K^n -> ((K^n -> K) -> K). This has the pattern X -> (Y -> Z),
with X = K^n, Y = (K^n -> K), and Z = K.
Applying the propositions as types analogy, one can follow this pattern
through a series of metamorphoses from the type of a vector field to the
type of a derivation, as traced out in Table 4. Observe how the function
f : X -> K, associated with the place of Y in the pattern, moves through
its paces from the second to the first position. In this way, the vector
field !X!, initially viewed as attaching each tangent vector !X!_x to the
site x where it acts in X, now comes to be seen as acting on each scalar
potential f : X -> K like a generalized species of differentiation,
producing another function !X!f : X -> K of the same type.
Table 4. An Equivalence Based on the Propositions as Types Analogy
o-------------------------o------------------------o--------------------------o
| Pattern | Construction | Instance |
o-------------------------o------------------------o--------------------------o
| X -> (Y -> Z) | Vector Field | K^n -> ((K^n -> K) -> K) |
o-------------------------o------------------------o--------------------------o
| (X x Y) -> Z | | (K^n x (K^n -> K)) -> K |
o-------------------------o------------------------o--------------------------o
| (Y x X) -> Z | | ((K^n -> K) x K^n) -> K |
o-------------------------o------------------------o--------------------------o
| Y -> (X -> Z) | Derivation | (K^n -> K) -> (K^n -> K) |
o-------------------------o------------------------o--------------------------o
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o