12,080
edits
Changes
Directory:Jon Awbrey/Papers/Differential Analytic Turing Automata (view source)
Revision as of 16:24, 28 September 2013
, 16:24, 28 September 2013update
Figure 1.2 expands <math>\mathrm{E}f = \texttt{((} u + \mathrm{d}u \texttt{)(} v + \mathrm{d}v \texttt{))}\!</math> over <math>[u, v]\!</math> to give:
Figure 1.2 expands <math>\mathrm{E}f = \texttt{((} u + \mathrm{d}u \texttt{)(} v + \mathrm{d}v \texttt{))}\!</math> over <math>[u, v]\!</math> to give:
{| align="center" cellpadding="8"
{| align="center" cellpadding="8" style="text-align:center; width:100%"
|
|
<math>\begin{matrix}
<math>\begin{matrix}
Figure 1.3 expands <math>\mathrm{D}f = f + \mathrm{E}f\!</math> over <math>[u, v]\!</math> to produce:
Figure 1.3 expands <math>\mathrm{D}f = f + \mathrm{E}f\!</math> over <math>[u, v]\!</math> to produce:
{| align="center" cellpadding="8"
{| align="center" cellpadding="8" style="text-align:center; width:100%"
|
|
<math>\begin{matrix}
<math>\begin{matrix}
Figure 2.2 expands <math>\mathrm{E}g = \texttt{((} u + \mathrm{d}u \texttt{,~} v + \mathrm{d}v \texttt{))}\!</math> over <math>[u, v]\!</math> to give:
Figure 2.2 expands <math>\mathrm{E}g = \texttt{((} u + \mathrm{d}u \texttt{,~} v + \mathrm{d}v \texttt{))}\!</math> over <math>[u, v]\!</math> to give:
{| align="center" cellpadding="8"
{| align="center" cellpadding="8" style="text-align:center; width:100%"
|
|
<math>\begin{matrix}
<math>\begin{matrix}
Figure 2.3 expands <math>\mathrm{D}g = g + \mathrm{E}g\!</math> over <math>[u, v]\!</math> to yield the form:
Figure 2.3 expands <math>\mathrm{D}g = g + \mathrm{E}g\!</math> over <math>[u, v]\!</math> to yield the form:
{| align="center" cellpadding="8"
{| align="center" cellpadding="8" style="text-align:center; width:100%"
|
|
<math>\begin{matrix}
<math>\begin{matrix}
Justifying a notion of approximation is a little more involved in general, and especially in these discrete logical spaces, than it would be expedient for people in a hurry to tangle with right now. I will just say that there are ''naive'' or ''obvious'' notions and there are ''sophisticated'' or ''subtle'' notions that we might choose among. The later would engage us in trying to construct proper logical analogues of Lie derivatives, and so let's save that for when we have become subtle or sophisticated or both. Against or toward that day, as you wish, let's begin with an option in plain view.
Justifying a notion of approximation is a little more involved in general, and especially in these discrete logical spaces, than it would be expedient for people in a hurry to tangle with right now. I will just say that there are ''naive'' or ''obvious'' notions and there are ''sophisticated'' or ''subtle'' notions that we might choose among. The later would engage us in trying to construct proper logical analogues of Lie derivatives, and so let's save that for when we have become subtle or sophisticated or both. Against or toward that day, as you wish, let's begin with an option in plain view.
Figure 1.4 illustrates one way of ranging over the cells of the underlying universe <math>U^\bullet = [u, v]\!</math> and selecting at each cell the linear proposition in <math>\mathrm{d}U^\bullet = [du, dv]</math> that best approximates the patch of the difference map <math>\mathrm{D}f</math> that is located there, yielding the following formula for the differential <math>\mathrm{d}f.</math>
Figure 1.4 illustrates one way of ranging over the cells of the underlying universe <math>U^\bullet = [u, v]\!</math> and selecting at each cell the linear proposition in <math>\mathrm{d}U^\bullet = [\mathrm{d}u, \mathrm{d}v]\!</math> that best approximates the patch of the difference map <math>{\mathrm{D}f}\!</math> that is located there, yielding the following formula for the differential <math>\mathrm{d}f.\!</math>
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" style="text-align:center; width:100%"
| <math>\mathrm{d}f ~=~ \texttt{uv} \cdot \texttt{0} ~+~ \texttt{u(v)} \cdot \texttt{du} ~+~ \texttt{(u)v} \cdot \texttt{dv} ~+~ \texttt{(u)(v)} \cdot \texttt{(du, dv)}</math>
|
<math>\begin{array}{*{11}{c}}
\mathrm{d}f
& = & \mathrm{d}\texttt{((} u \texttt{)(} v \texttt{))}
& = & uv \cdot 0
& + & u \texttt{(} v \texttt{)} \cdot \mathrm{d}u
& + & \texttt{(} u \texttt{)} v \cdot \mathrm{d}v
& + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot \texttt{(} \mathrm{d}u \texttt{,~} \mathrm{d}v \texttt{)}
\end{array}</math>
|}
|}
|}
|}
Figure 2.4 illustrates one way of ranging over the cells of the underlying universe <math>U^\bullet = [u, v]\!</math> and selecting at each cell the linear proposition in <math>\mathrm{d}U^\bullet = [du, dv]</math> that best approximates the patch of the difference map <math>\mathrm{D}g</math> that is located there, yielding the following formula for the differential <math>\mathrm{d}g.\!</math>
Figure 2.4 illustrates one way of ranging over the cells of the underlying universe <math>U^\bullet = [u, v]\!</math> and selecting at each cell the linear proposition in <math>\mathrm{d}U^\bullet = [du, dv]\!</math> that best approximates the patch of the difference map <math>\mathrm{D}g\!</math> that is located there, yielding the following formula for the differential <math>\mathrm{d}g.\!</math>
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" style="text-align:center; width:100%"
| <math>\mathrm{d}g ~=~ \texttt{uv} \cdot \texttt{(du, dv)} ~+~ \texttt{u(v)} \cdot \texttt{(du, dv)} ~+~ \texttt{(u)v} \cdot \texttt{(du, dv)} ~+~ \texttt{(u)(v)} \cdot \texttt{(du, dv)}</math>
|
<math>\begin{array}{*{11}{c}}
\mathrm{d}g
& = & \mathrm{d}\texttt{((} u \texttt{,} v \texttt{))}
& = & uv \cdot \texttt{(} \mathrm{d}u \texttt{,} \mathrm{d}v \texttt{)}
& + & u \texttt{(} v \texttt{)} \cdot \texttt{(} \mathrm{d}u \texttt{,} \mathrm{d}v \texttt{)}
& + & \texttt{(} u \texttt{)} v \cdot \texttt{(} \mathrm{d}u \texttt{,} \mathrm{d}v \texttt{)}
& + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot \texttt{(} \mathrm{d}u \texttt{,} \mathrm{d}v \texttt{)}
\end{array}</math>
|}
|}
|}
|}
Well, <math>g,\!</math> that was easy, seeing as how <math>\mathrm{D}g</math> is already linear at each locus, <math>\mathrm{d}g = \mathrm{D}g.</math>
Well, <math>g,\!</math> that was easy, seeing as how <math>\mathrm{D}g\!</math> is already linear at each locus, <math>\mathrm{d}g = \mathrm{D}g.\!</math>
==Analytic Series==
==Analytic Series==
We have been conducting the differential analysis of the logical transformation <math>F : [u, v] \mapsto [u, v]</math> defined as <math>F : (u, v) \mapsto ( ~\texttt{((u)(v))}~, ~\texttt{((u, v))}~ ),</math> and this means starting with the extended transformation <math>\mathrm{E}F : [u, v, du, dv] \to [u, v, du, dv]</math> and breaking it into an analytic series, <math>\mathrm{E}F = F + \mathrm{d}F + \mathrm{d}^2 F + \ldots,</math> and
We have been conducting the differential analysis of the logical transformation <math>F : [u, v] \mapsto [u, v]\!</math> defined as <math>F : (u, v) \mapsto ( ~ \texttt{((} u \texttt{)(} v \texttt{))} ~,~ \texttt{((} u \texttt{,~} v \texttt{))} ~ ),\!</math> and this means starting with the extended transformation <math>\mathrm{E}F : [u, v, \mathrm{d}u, \mathrm{d}v] \to [u, v, \mathrm{d}u, \mathrm{d}v]\!</math> and breaking it into an analytic series, <math>\mathrm{E}F = F + \mathrm{d}F + \mathrm{d}^2 F + \ldots,\!</math> and so on until there is nothing left to analyze any further.
so on until there is nothing left to analyze any further.
As a general rule, one proceeds by way of the following stages:
As a general rule, one proceeds by way of the following stages:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
|
|
<math>\begin{array}{lccccc}
<math>\begin{array}{*{6}{l}}
1. & \mathrm{E}F & = & \mathrm{d}^0 F & + & \mathrm{r}^0 F
1. & \mathrm{E}F
& = & \mathrm{d}^0 F
& + & \mathrm{r}^0 F
\\
\\
2. & \mathrm{r}^0 F & = & \mathrm{d}^1 F & + & \mathrm{r}^1 F
2. & \mathrm{r}^0 F
& = & \mathrm{d}^1 F
& + & \mathrm{r}^1 F
\\
\\
3. & \mathrm{r}^1 F & = & \mathrm{d}^2 F & + & \mathrm{r}^2 F
3. & \mathrm{r}^1 F
& = & \mathrm{d}^2 F
& + & \mathrm{r}^2 F
\\
\\
4. & \ldots
4. & \ldots
|}
|}
In our analysis of the transformation <math>F,\!</math> we carried out Step 1 in the more familiar form <math>\mathrm{E}F = F + \mathrm{D}F,</math> and we have just reached Step 2 in the form <math>\mathrm{D}F = \mathrm{d}F + \mathrm{r}F,</math> where <math>\mathrm{r}F</math> is the residual term that remains for us to examine next.
In our analysis of the transformation <math>F,\!</math> we carried out Step 1 in the more familiar form <math>\mathrm{E}F = F + \mathrm{D}F\!</math> and we have just reached Step 2 in the form <math>\mathrm{D}F = \mathrm{d}F + \mathrm{r}F,\!</math> where <math>\mathrm{r}F\!</math> is the residual term that remains for us to examine next.
'''NB.''' I'm am trying to give quick overview here, and this forces me to omit many picky details. The picky reader may wish to consult the more detailed presentation of this material at the following locations:
'''Note.''' I'm am trying to give quick overview here, and this forces me to omit many picky details. The picky reader may wish to consult the more detailed presentation of this material at the following locations:
:* [[Differential Logic and Dynamic Systems 2.0|Differential Logic and Dynamic Systems]]
: [[Differential Logic and Dynamic Systems 2.0#The Secant Operator : E|The Secant Operator]]
::* [[Differential Logic and Dynamic Systems 2.0#The Secant Operator : E|The Secant Operator]]
: [[Differential Logic and Dynamic Systems 2.0#Taking Aim at Higher Dimensional Targets|Higher Dimensional Targets]]
::* [[Differential Logic and Dynamic Systems 2.0#Taking Aim at Higher Dimensional Targets|Higher Dimensional Targets]]
Let's push on with the analysis of the transformation:
Let's push on with the analysis of the transformation:
|
|
<math>\begin{matrix}
<math>\begin{matrix}
F & : & (u, v) & \mapsto & (f(u, v),~g(u, v)) & = & (~\texttt{((u)(v))}~,~\texttt{((u,~v))}~).\end{matrix}</math>
F & : & (u, v) & \mapsto & (f(u, v), g(u, v))
& = & ( ~ \texttt{((} u \texttt{)(} v \texttt{))} ~,~ \texttt{((} u \texttt{,~} v \texttt{))} ~)
\end{matrix}</math>
|}
|}
For ease of comparison and computation, I will collect the Figures that we need for the remainder of the work together on one page.
For ease of comparison and computation, I will collect the Figures that we need for the remainder of the work together on one page.
===Computation Summary : <math>f(u, v) = \texttt{((u)(v))}</math>===
===Computation Summary for Logical Disjunction===
Figure 1.1 shows the expansion of <math>f = \texttt{((u)(v))}</math> over <math>[u, v]\!</math> to produce the expression:
Figure 1.1 shows the expansion of <math>f = \texttt{((} u \texttt{)(} v \texttt{))}\!</math> over <math>[u, v]\!</math> to produce the expression:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
| <math>\texttt{uv} ~+~ \texttt{u(v)} ~+~ \texttt{(u)v}</math>
|
<math>\begin{matrix}
uv & + & u \texttt{(} v \texttt{)} & + & \texttt{(} u \texttt{)} v
\end{matrix}</math>
|}
|}
Figure 1.2 shows the expansion of <math>\mathrm{E}f = \texttt{((u + du)(v + dv))}</math> over <math>[u, v]\!</math> to produce the expression:
Figure 1.2 shows the expansion of <math>\mathrm{E}f = \texttt{((} u + \mathrm{d}u \texttt{)(} v + \mathrm{d}v \texttt{))}\!</math> over <math>[u, v]\!</math> to produce the expression:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
| <math>\texttt{uv} \cdot \texttt{(du~dv)} + \texttt{u(v)} \cdot \texttt{(du (dv))} + \texttt{(u)v} \cdot \texttt{((du) dv)} + \texttt{(u)(v)} \cdot \texttt{((du)(dv))}</math>
|
<math>\begin{matrix}
uv \cdot \texttt{(} \mathrm{d}u ~ \mathrm{d}v \texttt{)} & + &
u \texttt{(} v \texttt{)} \cdot \texttt{(} \mathrm{d}u \texttt{(} \mathrm{d}v \texttt{))} & + &
\texttt{(} u \texttt{)} v \cdot \texttt{((} \mathrm{d}u \texttt{)} \mathrm{d}v \texttt{)} & + &
\texttt{(} u \texttt{)(} v \texttt{)} \cdot \texttt{((} \mathrm{d}u \texttt{)(} \mathrm{d}v \texttt{))}
\end{matrix}</math>
|}
|}
<math>\mathrm{E}f</math> tells you what you would have to do, from where you are in the universe <math>[u, v],\!</math> if you want to end up in a place where <math>f\!</math> is true. In this case, where the prevailing proposition <math>f\!</math> is <math>\texttt{((u)(v))},</math> the indication <math>\texttt{uv} \cdot \texttt{(du~dv)}</math> of <math>\mathrm{E}f</math> tells you this: If <math>u\!</math> and <math>v\!</math> are both true where you are, then just don't change both <math>u\!</math> and <math>v\!</math> at once, and you will end up in a place where <math>\texttt{((u)(v))}</math> is true.
In general, <math>\mathrm{E}f\!</math> tells you what you would have to do, from wherever you are in the universe <math>[u, v],\!</math> if you want to end up in a place where <math>f\!</math> is true. In this case, where the prevailing proposition <math>f\!</math> is <math>\texttt{((} u \texttt{)(} v \texttt{))},\!</math> the indication <math>uv \cdot \texttt{(} \mathrm{d}u ~ \mathrm{d}v \texttt{)}\!</math> of <math>\mathrm{E}f\!</math> tells you this: If <math>u\!</math> and <math>v\!</math> are both true where you are, then just don't change both <math>u\!</math> and <math>v\!</math> at once, and you will end up in a place where <math>\texttt{((} u \texttt{)(} v \texttt{))}\!</math> is true.
Figure 1.3 shows the expansion of <math>\mathrm{D}f</math> over <math>[u, v]\!</math> to produce the expression:
Figure 1.3 shows the expansion of <math>\mathrm{D}f</math> over <math>[u, v]\!</math> to produce the expression:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
| <math>\texttt{uv} \cdot \texttt{du~dv} ~+~ \texttt{u(v)} \cdot \texttt{du(dv)} ~+~ \texttt{(u)v} \cdot \texttt{(du)dv} ~+~ \texttt{(u)(v)} \cdot \texttt{((du)(dv))}</math>
|
<math>\begin{matrix}
uv \cdot \mathrm{d}u ~ \mathrm{d}v & + &
u \texttt{(} v \texttt{)} \cdot \mathrm{d}u \texttt{(} \mathrm{d}v \texttt{)} & + &
\texttt{(} u \texttt{)} v \cdot \texttt{(} \mathrm{d}u \texttt{)} \mathrm{d}v & + &
\texttt{(} u \texttt{)(} v \texttt{)} \cdot \texttt{((} \mathrm{d}u \texttt{)(} \mathrm{d}v \texttt{))}
\end{matrix}</math>
|}
|}
<math>\mathrm{D}f</math> tells you what you would have to do, from where you are in the universe <math>[u, v],\!</math> if you want to bring about a change in the value of <math>f,\!</math> that is, if you want to get to a place where the value of <math>f\!</math> is different from what it is where you are. In the present case, where the reigning proposition <math>f\!</math> is <math>\texttt{((u)(v))},</math> the term <math>\texttt{uv} \cdot \texttt{du~dv}</math> of <math>\mathrm{D}f</math> tells you this: If <math>u\!</math> and <math>v\!</math> are both true where you are, then you would have to change both <math>u\!</math> and <math>v\!</math> in order to reach a place where the value of <math>f\!</math> is different from what it is where you are.
In general, <math>{\mathrm{D}f}\!</math> tells you what you would have to do, from wherever you are in the universe <math>[u, v],\!</math> if you want to bring about a change in the value of <math>f,\!</math> that is, if you want to get to a place where the value of <math>f\!</math> is different from what it is where you are. In the present case, where the reigning proposition <math>f\!</math> is <math>\texttt{((} u \texttt{)(} v \texttt{))},\!</math> the term <math>uv \cdot \mathrm{d}u ~ \mathrm{d}v\!</math> of <math>{\mathrm{D}f}\!</math> tells you this: If <math>u\!</math> and <math>v\!</math> are both true where you are, then you would have to change both <math>u\!</math> and <math>v\!</math> in order to reach a place where the value of <math>f\!</math> is different from what it is where you are.
Figure 1.4 approximates <math>\mathrm{D}f</math> by the linear form <math>\mathrm{d}f</math> that expands over <math>[u, v]\!</math> as follows:
Figure 1.4 approximates <math>{\mathrm{D}f}\!</math> by the linear form <math>\mathrm{d}f\!</math> that expands over <math>[u, v]\!</math> as follows:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
<math>\begin{matrix}
<math>\begin{matrix}
\mathrm{d}f
\mathrm{d}f
& = & \texttt{uv} \cdot \texttt{0} & + & \texttt{u(v)} \cdot \texttt{du} & + & \texttt{(u)v} \cdot \texttt{dv} & + & \texttt{(u)(v)} \cdot \texttt{(du, dv)}
& = & uv \cdot 0
\\ \\
& + & u \texttt{(} v \texttt{)} \cdot \mathrm{d}u
& = & & & \texttt{u(v)} \cdot \texttt{du} & + & \texttt{(u)v} \cdot \texttt{dv} & + & \texttt{(u)(v)} \cdot \texttt{(du, dv)}
& + & \texttt{(} u \texttt{)} v \cdot \mathrm{d}v
& + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot \texttt{(} \mathrm{d}u \texttt{,~} \mathrm{d}v \texttt{)}
\\[8pt]
& = &&& u \texttt{(} v \texttt{)} \cdot \mathrm{d}u
& + & \texttt{(} u \texttt{)} v \cdot \mathrm{d}v
& + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot \texttt{(} \mathrm{d}u \texttt{,~} \mathrm{d}v \texttt{)}
\end{matrix}</math>
\end{matrix}</math>
|}
|}
Figure 1.5 shows what remains of the difference map <math>\mathrm{D}f</math> when the first order linear contribution <math>\mathrm{d}f</math> is removed, namely:
Figure 1.5 shows what remains of the difference map <math>{\mathrm{D}f}\!</math> when the first order linear contribution <math>\mathrm{d}f\!</math> is removed, namely:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
|
|
<math>\begin{matrix}
<math>\begin{array}{*{9}{l}}
\mathrm{r}f
\mathrm{r}f
& = & \texttt{uv} \cdot \texttt{du~dv} & + & \texttt{u(v)} \cdot \texttt{du~dv} & + & \texttt{(u)v} \cdot \texttt{du~dv} & + & \texttt{(u)(v)} \cdot \texttt{du~dv}
& = & uv \cdot \mathrm{d}u ~ \mathrm{d}v
\\ \\
& + & u \texttt{(} v \texttt{)} \cdot \mathrm{d}u ~ \mathrm{d}v
& = & \texttt{du~dv}
& + & \texttt{(} u \texttt{)} v \cdot \mathrm{d}u ~ \mathrm{d}v
\end{matrix}</math>
& + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot \mathrm{d}u ~ \mathrm{d}v
\\[8pt]
& = & \mathrm{d}u ~ \mathrm{d}v
\end{array}</math>
|}
|}
</pre>
</pre>
|}
|}
{| align="center" border="0" cellpadding="10"
{| align="center" border="0" cellpadding="10"
</pre>
</pre>
|}
|}
{| align="center" border="0" cellpadding="10"
{| align="center" border="0" cellpadding="10"
</pre>
</pre>
|}
|}
{| align="center" border="0" cellpadding="10"
{| align="center" border="0" cellpadding="10"
</pre>
</pre>
|}
|}
{| align="center" border="0" cellpadding="10"
{| align="center" border="0" cellpadding="10"
|}
|}
===Computation Summary : <math>g(u, v) = \texttt{((u, v))}</math>===
===Computation Summary for Logical Equality===
Figure 2.1 shows the expansion of <math>g = \texttt{((u, v))}</math> over <math>[u, v]\!</math> to produce the expression:
Figure 2.1 shows the expansion of <math>g = \texttt{((u, v))}</math> over <math>[u, v]\!</math> to produce the expression: