Line 569: |
Line 569: |
| 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 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>\xi : X \to \bigcup_{x \in X} \xi_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>\xi_x\!</math> [Che46, 82–83]. If <math>X\!</math> is of the type <math>\mathbb{K}^n,</math> then <math>\xi\!</math> is of the 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> | + | 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 of the form <math>\xi : X \to \textstyle\bigcup_{x \in X} \xi_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>\xi_x\!</math> [Che46, 82–83]. If <math>X\!</math> is of the type <math>\mathbb{K}^n,</math> then <math>\xi\!</math> is of the 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 <math>f : X \to \mathbb{K},</math> associated with the place of <math>Y\!</math> in the pattern, moves through its paces from the second to the first position. In this way, the vector field <math>\xi,\!</math> initially viewed as attaching each tangent vector <math>\xi_x\!</math> to the site <math>x\!</math> where it acts in <math>X,\!</math> now comes to be seen as acting on each scalar potential <math>f : X \to \mathbb{K}</math> like a generalized species of differentiation, producing another function <math>\xi f : X \to \mathbb{K}</math> 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 4. Observe how the function <math>f : X \to \mathbb{K},</math> associated with the place of <math>Y\!</math> in the pattern, moves through its paces from the second to the first position. In this way, the vector field <math>\xi,\!</math> initially viewed as attaching each tangent vector <math>\xi_x\!</math> to the site <math>x\!</math> where it acts in <math>X,\!</math> now comes to be seen as acting on each scalar potential <math>f : X \to \mathbb{K}</math> like a generalized species of differentiation, producing another function <math>\xi f : X \to \mathbb{K}</math> of the same type. |
| | | |
− | {| align="center" border="1" cellpadding="8" cellspacing="0" style="text-align:center; width:96%" | + | <br> |
− | |+ '''Table 4. An Equivalence Based on the Propositions as Types Analogy | + | |
− | '''
| + | {| align="center" border="1" cellpadding="8" cellspacing="0" style="background:#f8f8ff; text-align:center; width:90%" |
− | |- style="background:ghostwhite" | + | |+ <math>\text{Table 4.}~~\text{An Equivalence Based on the Propositions as Types Analogy}</math> |
− | ! <math>\mbox{Pattern}\!</math>
| + | |- style="background:#f0f0ff" |
− | ! <math>\mbox{Construct}\!</math>
| + | | <math>\text{Pattern}\!</math> |
− | ! <math>\mbox{Instance}\!</math>
| + | | <math>\text{Construct}\!</math> |
| + | | <math>\text{Instance}\!</math> |
| |- | | |- |
| | <math>X \to (Y \to Z)</math> | | | <math>X \to (Y \to Z)</math> |
Line 596: |
Line 597: |
| | <math>\mbox{Derivation}\!</math> | | | <math>\mbox{Derivation}\!</math> |
| | <math>(\mathbb{K}^n \to \mathbb{K}) \to (\mathbb{K}^n \to \mathbb{K})</math> | | | <math>(\mathbb{K}^n \to \mathbb{K}) \to (\mathbb{K}^n \to \mathbb{K})</math> |
− | |}<br> | + | |} |
| + | |
| + | <br> |
| | | |
| ===Reality at the Threshold of Logic=== | | ===Reality at the Threshold of Logic=== |