Changes

===Propositions as Types and Higher Order Types===

===Propositions as Types and Higher Order Types===

The arrangement of types collected in Table 3 (repeated below) 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.

The arrangement of types collected in Table 3 (repeated below) serve to introduce the themes of ''higher order propositional expressions'' and the ''propositions as types'' (PAT) analogy.

{| align="center" border="1" cellpadding="8" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"

{| align="center" border="1" cellpadding="8" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"

Next, by way of illustrating the propositions as types idea, consider a proposition of the form <math>X \Rightarrow (Y \Rightarrow Z).</math>  One knows from propositional calculus that this is logically equivalent to a proposition of the form <math>(X \land Y) \Rightarrow Z.</math>  But this equivalence should remind us of the functional isomorphism that exists between a construction of the type <math>X \to (Y \to Z)</math> and a construction of the type <math>(X \times Y) \to Z.</math>  The propositions as types analogy permits us to take a functional type like this and, under the right conditions, replace the functional arrows "<math>\to\!</math>" and products "<math>\times\!</math>" with the respective logical arrows "<math>\Rightarrow\!</math>" and products "<math>\land\!</math>".  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.

Next, by way of illustrating the propositions as types idea, consider a proposition of the form <math>X \Rightarrow (Y \Rightarrow Z).</math>  One knows from propositional calculus that this is logically equivalent to a proposition of the form <math>(X \land Y) \Rightarrow Z.</math>  But this equivalence should remind us of the functional isomorphism that exists between a construction of the type <math>X \to (Y \to Z)</math> and a construction of the type <math>(X \times Y) \to Z.</math>  The propositions as types analogy permits us to take a functional type like this and, under the right conditions, replace the functional arrows "<math>\to\!</math>" and products "<math>\times\!</math>" with the respective logical arrows "<math>\Rightarrow\!</math>" and products "<math>\land\!</math>".  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&nbsp;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 of the form <math>\chi\!</math>&nbsp;:&nbsp;''X''&nbsp;&rarr;&nbsp;<math>\bigcup_x \ \chi_x\!</math> that assigns to each point ''x'' of the space ''X'' a tangent vector to ''X'' at that point, namely, the tangent vector <math>\chi_x\!</math> [Che46, 82&ndash;83].  If ''X'' is of type '''K'''^''n'', then <math>\chi\!</math> is of type '''K'''^''n''&nbsp;&rarr;&nbsp;(('''K'''^''n''&nbsp;&rarr;&nbsp;'''K''')&nbsp;&rarr;&nbsp;'''K''').  This has the pattern ''X''&nbsp;&rarr;&nbsp;(''Y''&nbsp;&rarr;&nbsp;''Z''), with ''X''&nbsp;=&nbsp;'''K'''^''n'', ''Y''&nbsp;=&nbsp;('''K'''^''n''&nbsp;&rarr;&nbsp;'''K'''), and ''Z''&nbsp;=&nbsp;'''K'''.

Finally, examine the middle four rows of Table&nbsp;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 of the form <math>\chi : X \to \bigcup_{x \in X} \chi_x</math> that assigns to each point <math>x\!</math> of the space <math>X\!</math> a tangent vector to <math>X\!</math> at that point, namely, the tangent vector <math>\chi_x\!</math> [Che46, 82&ndash;83].  If <math>X\!</math> is of type <math>\mathbb{K}^n,</math> then <math>\chi\!</math> is of type <math>\mathbb{K}^n \to ((\mathbb{K}^n \to \mathbb{K}) \to \mathbb{K}).</math> This has the pattern <math>X \to (Y \to Z),</math> with <math>X = \mathbb{K}^n,</math> <math>Y = (\mathbb{K}^n \to \mathbb{K}),</math> and <math>Z = \mathbb{K}.</math>

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''&nbsp;:&nbsp;''X''&nbsp;&rarr;&nbsp;'''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 <math>\chi\!</math>, initially viewed as attaching each tangent vector <math>\chi_x\!</math> to the site ''x'' where it acts in ''X'', now comes to be seen as acting on each scalar potential ''f''&nbsp;:&nbsp;''X''&nbsp;&rarr;&nbsp;'''K''' like a generalized species of differentiation, producing another function <math>\chi\!</math>''f''&nbsp;:&nbsp;''X''&nbsp;&rarr;&nbsp;'''K''' of the same type.

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&nbsp;4.  Observe how the function ''f''&nbsp;:&nbsp;''X''&nbsp;&rarr;&nbsp;'''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 <math>\chi\!</math>, initially viewed as attaching each tangent vector <math>\chi_x\!</math> to the site ''x'' where it acts in ''X'', now comes to be seen as acting on each scalar potential ''f''&nbsp;:&nbsp;''X''&nbsp;&rarr;&nbsp;'''K''' like a generalized species of differentiation, producing another function <math>\chi\!</math>''f''&nbsp;:&nbsp;''X''&nbsp;&rarr;&nbsp;'''K''' of the same type.

<font face="courier new">

<font face="courier new">