MyWikiBiz, Author Your Legacy — Sunday May 05, 2024
Jump to navigationJump to search
28 bytes added
, 04:20, 12 July 2009
Line 513: |
Line 513: |
| The types collected in Table 3 (repeated below) serve to illustrate the themes of ''higher order propositional expressions'' and the ''propositions as types'' (PAT) analogy. | | The types collected in Table 3 (repeated below) serve to illustrate 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%" | + | <br> |
− | |+ '''Table 3. Analogy Between Real and Boolean Types''' | + | |
− | |- style="background:ghostwhite" | + | {| align="center" border="1" cellpadding="8" cellspacing="0" style="background:#f8f8ff; text-align:center; width:90%" |
− | ! <math>\mbox{Real Domain}\ \mathbb{R}</math>
| + | |+ <math>\text{Table 3.}~~\text{Analogy Between Real and Boolean Types}</math> |
− | ! <math>\longleftrightarrow</math>
| + | |- style="background:#f0f0ff" |
− | ! <math>\mbox{Boolean Domain}\ \mathbb{B}</math>
| + | | <math>\text{Real Domain}~ \mathbb{R}</math> |
| + | | <math>\longleftrightarrow</math> |
| + | | <math>\text{Boolean Domain}~ \mathbb{B}</math> |
| |- | | |- |
| | <math>\mathbb{R}^n</math> | | | <math>\mathbb{R}^n</math> |
Line 559: |
Line 561: |
| <p><math>\mbox{Transformation}\!</math></p> | | <p><math>\mbox{Transformation}\!</math></p> |
| | <math>(\mathbb{B}^n \to \mathbb{B}) \to (\mathbb{B}^m \to \mathbb{B})</math> | | | <math>(\mathbb{B}^n \to \mathbb{B}) \to (\mathbb{B}^m \to \mathbb{B})</math> |
− | |}<br> | + | |} |
| + | |
| + | <br> |
| | | |
| First, observe that the type of a ''tangent vector at a point'', also known as a ''directional derivative'' at that point, has the form <math>(\mathbb{K}^n \to \mathbb{K}) \to \mathbb{K},</math> where <math>\mathbb{K}</math> is the chosen ground field, in the present case either <math>\mathbb{R}</math> or <math>\mathbb{B}.</math> At a point in a space of type <math>\mathbb{K}^n,</math> a directional derivative operator <math>\vartheta\!</math> takes a function on that space, an <math>f\!</math> of type <math>(\mathbb{K}^n \to \mathbb{K}),</math> and maps it to a ground field value of type <math>\mathbb{K}.</math> This value is known as the ''derivative'' of <math>f\!</math> in the direction <math>\vartheta\!</math> [Che46, 76–77]. In the boolean case <math>\vartheta : (\mathbb{B}^n \to \mathbb{B}) \to \mathbb{B}</math> has the form of a proposition about propositions, in other words, a proposition of the next higher type. | | First, observe that the type of a ''tangent vector at a point'', also known as a ''directional derivative'' at that point, has the form <math>(\mathbb{K}^n \to \mathbb{K}) \to \mathbb{K},</math> where <math>\mathbb{K}</math> is the chosen ground field, in the present case either <math>\mathbb{R}</math> or <math>\mathbb{B}.</math> At a point in a space of type <math>\mathbb{K}^n,</math> a directional derivative operator <math>\vartheta\!</math> takes a function on that space, an <math>f\!</math> of type <math>(\mathbb{K}^n \to \mathbb{K}),</math> and maps it to a ground field value of type <math>\mathbb{K}.</math> This value is known as the ''derivative'' of <math>f\!</math> in the direction <math>\vartheta\!</math> [Che46, 76–77]. In the boolean case <math>\vartheta : (\mathbb{B}^n \to \mathbb{B}) \to \mathbb{B}</math> has the form of a proposition about propositions, in other words, a proposition of the next higher type. |