[Inquiry] Re: Differential Logic

[Jon Awbrey]

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