12,080
edits
Changes
MyWikiBiz, Author Your Legacy — Saturday December 28, 2024
Jump to navigationJump to searchDirectory:Jon Awbrey/Papers/Differential Analytic Turing Automata (view source)
Revision as of 03:30, 27 September 2013
, 03:30, 27 September 2013update
The task ahead is to chart a course from general ideas about ''transformational equivalence classes of graphs'' to a notion of ''differential analytic turing automata'' (DATA). It may be a while before we get within sight of that goal, but it will provide a better measure of motivation to name the thread after the envisioned end rather than the more homely starting place.
The task ahead is to chart a course from general ideas about ''transformational equivalence classes of graphs'' to a notion of ''differential analytic turing automata'' (DATA). It may be a while before we get within sight of that goal, but it will provide a better measure of motivation to name the thread after the envisioned end rather than the more homely starting place.
The basic idea is as follows. One has a set <math>\mathcal{G}</math> of graphs and a set <math>\mathcal{T}</math> of transformation rules, and each rule <math>\operatorname{t} \in \mathcal{T}</math> has the effect of transforming graphs into graphs, <math>\operatorname{t} : \mathcal{G} \to \mathcal{G}.</math> In the cases that we shall be studying, this set of transformation rules partitions the set of graphs into ''transformational equivalence classes'' (TECs).
The basic idea is as follows. One has a set <math>\mathcal{G}</math> of graphs and a set <math>\mathcal{T}</math> of transformation rules, and each rule <math>\mathrm{t} \in \mathcal{T}</math> has the effect of transforming graphs into graphs, <math>\mathrm{t} : \mathcal{G} \to \mathcal{G}.</math> In the cases that we shall be studying, this set of transformation rules partitions the set of graphs into ''transformational equivalence classes'' (TECs).
There are many interesting excursions to be had here, but I will focus mainly on logical applications, and and so the TECs I talk about will almost always have the character of ''logical equivalence classes'' (LECs).
There are many interesting excursions to be had here, but I will focus mainly on logical applications, and and so the TECs I talk about will almost always have the character of ''logical equivalence classes'' (LECs).
|}
|}
Given any transformation of this type, <math>G : U^\bullet \to X^\bullet,\!</math> the (first order) differential analysis of <math>G\!</math> is based on the definition of a couple of further transformations, derived by way of operators on <math>G,\!</math> that ply between the (first order) extended universes, <math>\mathrm{E}U^\bullet = [u, v, du, dv]\!</math> and <math>\operatorname{E}X^\bullet = [x, y, dx, dy],\!</math> of <math>G\text{'s}\!</math> own source and target universes.
Given any transformation of this type, <math>G : U^\bullet \to X^\bullet,\!</math> the (first order) differential analysis of <math>G\!</math> is based on the definition of a couple of further transformations, derived by way of operators on <math>G,\!</math> that ply between the (first order) extended universes, <math>\mathrm{E}U^\bullet = [u, v, du, dv]\!</math> and <math>\mathrm{E}X^\bullet = [x, y, dx, dy],\!</math> of <math>G\text{'s}\!</math> own source and target universes.
First, the ''enlargement map'' (or the ''secant transformation'') <math>\mathrm{E}G = (\mathrm{E}G_1, \mathrm{E}G_2) : \mathrm{E}U^\bullet \to \mathrm{E}X^\bullet\!</math> is defined by the following pair of component equations:
First, the ''enlargement map'' (or the ''secant transformation'') <math>\mathrm{E}G = (\mathrm{E}G_1, \mathrm{E}G_2) : \mathrm{E}U^\bullet \to \mathrm{E}X^\bullet\!</math> is defined by the following pair of component equations:
|
|
<math>\begin{array}{ll}
<math>\begin{array}{ll}
1.1. & f : \mathbb{B} \to \mathbb{B} ~\text{such that}~ f : \texttt{x} \mapsto \texttt{(x)}
1.1. & f : \mathbb{B} \to \mathbb{B} ~\text{such that}~ f : x \mapsto \texttt{(} x \texttt{)}
\\
\\
1.2. & \texttt{x}' ~=~ \texttt{(x)}
1.2. & x' ~=~ \texttt{(} x \texttt{)}
\\
\\
1.3. & \texttt{x} ~:=~ \texttt{(x)}
1.3. & x ~:=~ \texttt{(} x \texttt{)}
\\
\\
1.4. & \texttt{dx} ~=~ \texttt{1}
1.4. & \mathrm{d}x ~=~ 1
\end{array}</math>
\end{array}</math>
|}
|}
|
|
<math>\begin{array}{ll}
<math>\begin{array}{ll}
2.1. & F : \mathbb{B}^2 \to \mathbb{B}^2 ~\text{such that}~ F : (\texttt{u}, \texttt{v}) \mapsto ( ~\texttt{((u)(v))}~ , ~\texttt{((u,~v))}~ )
2.1. & F : \mathbb{B}^2 \to \mathbb{B}^2 ~\text{such that}~ F : (u, v) \mapsto ( ~ \texttt{((} u \texttt{)(} v \texttt{))} ~,~ \texttt{((} u \texttt{,~} v \texttt{))} ~ )
\\
\\
2.2. & \texttt{u}' ~=~ \texttt{((u)(v))}~, \quad \texttt{v}' ~=~ \texttt{((u,~v))}
2.2. & u' ~=~ \texttt{((} u \texttt{)(} v \texttt{))} \quad ~,~ \quad v' ~=~ \texttt{((} u \texttt{,~} v \texttt{))}
\\
\\
2.3. & \texttt{u} ~:=~ \texttt{((u)(v))}~, \quad \texttt{v} ~:=~ \texttt{((u,~v))}
2.3. & u ~:=~ \texttt{((} u \texttt{)(} v \texttt{))} \quad ~,~ \quad v ~:=~ \texttt{((} u \texttt{,~} v \texttt{))}
\\
\\
2.4. & ???
2.4. & ?
\end{array}</math>
\end{array}</math>
|}
|}
Well, the last one is not such a fall off the log, but that is exactly the purpose for which we have been developing all of the foregoing machinations.
Well, the last one is not such a fall off a log, but that is exactly the purpose for which we have been developing all of the foregoing machinations.
Here is what I got when I just went ahead and calculated the finite differences willy-nilly:
Here is what I got when I just went ahead and calculated the finite differences willy-nilly:
{| align="center" cellpadding="8" style="text-align:center"
{| align="center" cellpadding="8" style="text-align:center"
|-
|-
| <math>\text{Orbit 1. Intitial Point :}~ (u, v) = (1, 1)</math>
| <math>\text{Orbit 1. Intitial Point :}~ (u, v) = (1, 1)\!</math>
|-
|-
|
|
<math>\begin{array}{c|cc|cc|cc|cc|cc|c}
<math>\begin{array}{c|cc|cc|cc|cc|cc|c}
t & u & v & du & dv & d^2 u & d^2 v & d^3 u & d^3 v & d^4 u & d^4 v & \ldots \\
t & u & v & \mathrm{d}u & \mathrm{d}v & \mathrm{d}^2 u & \mathrm{d}^2 v & \mathrm{d}^3 u & \mathrm{d}^3 v & \mathrm{d}^4 u & \mathrm{d}^4 v & \ldots \\[8pt]
0 & 1 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\
0 & 1 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\
1 & 1 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\
1 & 1 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\
2 & {}^\shortparallel & {}^\shortparallel & {}^\shortparallel & {}^\shortparallel & {}^\shortparallel & {}^\shortparallel & {}^\shortparallel & {}^\shortparallel & {}^\shortparallel & {}^\shortparallel & \ldots
\end{array}</math>
\end{array}</math>
|-
|-
| <math>\text{Orbit 2. Intitial Point :}~ (u, v) = (0, 0)</math>
| <math>\text{Orbit 2. Intitial Point :}~ (u, v) = (0, 0)\!</math>
|-
|-
|
|
<math>\begin{array}{c|cc|cc|cc|cc|cc|c}
<math>\begin{array}{c|cc|cc|cc|cc|cc|c}
t & u & v & du & dv & d^2 u & d^2 v & d^3 u & d^3 v & d^4 u & d^4 v & \ldots \\
t & u & v & \mathrm{d}u & \mathrm{d}v & \mathrm{d}^2 u & \mathrm{d}^2 v & \mathrm{d}^3 u & \mathrm{d}^3 v & \mathrm{d}^4 u & \mathrm{d}^4 v & \ldots \\[8pt]
0 & 0 & 0 & 0 & 1 & 1 & 0 & 0 & 1 & 1 & 0 & \ldots \\
0 & 0 & 0 & 0 & 1 & 1 & 0 & 0 & 1 & 1 & 0 & \ldots \\
1 & 0 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & \ldots \\
1 & 0 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & \ldots \\
2 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\
2 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\
3 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\
3 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\
4 & {}^\shortparallel & {}^\shortparallel & {}^\shortparallel & {}^\shortparallel & {}^\shortparallel & {}^\shortparallel & {}^\shortparallel & {}^\shortparallel & {}^\shortparallel & {}^\shortparallel & \ldots
4 & '' & '' & '' & '' & '' & '' & '' & '' & '' & '' & \ldots \\
\end{array}</math>
\end{array}</math>
|}
|}
What we are looking for is — one rule to rule them all, a rule that applies to every state and works every time.
What we are looking for is — one rule to rule them all, a rule that applies to every state and works every time.
What we see at first sight in the tables above are patterns of differential features that attach to the states in each orbit of the dynamics. Looked at locally to these orbits, the isolated fixed point at <math>(1, 1)\!</math> is no problem, as the rule <math>\texttt{du~=~dv~=~0}</math> describes it pithily enough. When it comes to the other orbit, the first thing that comes to mind is to write out the law <math>\texttt{du~=~v}, ~\texttt{dv~=~(u)}.</math>
What we see at first sight in the tables above are patterns of differential features that attach to the states in each orbit of the dynamics. Looked at locally to these orbits, the isolated fixed point at <math>(1, 1)\!</math> is no problem, as the rule <math>\mathrm{d}u = \mathrm{d}v = 0\!</math> describes it pithily enough. When it comes to the other orbit, the first thing that comes to mind is to write out the law <math>\mathrm{d}u = v ~,~ \mathrm{d}v = \texttt{(} u \texttt{)}.\!</math>
==Symbolic Method==
==Symbolic Method==
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
|
|
<math>\begin{array}{lllll}
<math>\begin{matrix}
F & = & (f, g) & = & ( ~\texttt{((u)(v))}~ , ~\texttt{((u,~v))}~ ).
F & = & (f, g) & = & ( ~ \texttt{((} u \texttt{)(} v \texttt{))} ~,~ \texttt{((} u \texttt{,~} v \texttt{))} ~ ).
\end{array}</math>
\end{matrix}</math>
|}
|}
In their application to this logical transformation the operators <math>\operatorname{E}</math> and <math>\operatorname{D}</math> respectively produce the ''enlarged map'' <math>\operatorname{E}F = (\operatorname{E}f, \operatorname{E}g)</math> and the ''difference map'' <math>\operatorname{D}F = (\operatorname{D}f, \operatorname{D}g),</math> whose components can be given as follows, if the reader, in the absence of a special format for logical parentheses, can forgive syntactically bilingual phrases:
In their application to this logical transformation the operators <math>\mathrm{E}\!</math> and <math>\mathrm{D}\!</math> respectively produce the ''enlarged map'' <math>\mathrm{E}F = (\mathrm{E}f, \mathrm{E}g)\!</math> and the ''difference map'' <math>\mathrm{D}F = (\mathrm{D}f, \mathrm{D}g),\!</math> whose components can be given as follows.
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
|
|
<math>\begin{array}{lll}
<math>\begin{array}{lll}
\operatorname{E}f & = & \texttt{(( u + du )( v + dv ))}
\mathrm{E}f & = & \texttt{((} u + \mathrm{d}u \texttt{)(} v + \mathrm{d}v \texttt{))}
\\ \\
\\[8pt]
\operatorname{E}g & = & \texttt{(( u + du ,~ v + dv ))}
\mathrm{E}g & = & \texttt{((} u + \mathrm{d}u \texttt{,~} v + \mathrm{d}v \texttt{))}
\\ \\
\\[8pt]
\operatorname{D}f & = & \texttt{((u)(v)) ~+~ (( u + du )( v + dv ))}
\mathrm{D}f & = & \texttt{((} u \texttt{)(} v \texttt{))} ~+~ \texttt{((} u + \mathrm{d}u \texttt{)(} v + \mathrm{d}v \texttt{))}
\\ \\
\\[8pt]
\operatorname{D}g & = & \texttt{((u,~v)) ~+~ (( u + du ,~ v + dv ))}
\mathrm{D}g & = & \texttt{((} u \texttt{,~} v \texttt{))} ~+~ \texttt{((} u + \mathrm{d}u \texttt{,~} v + \mathrm{d}v \texttt{))}
\end{array}\!</math>
\end{array}</math>
|}
|}
But these initial formulas are purely definitional, and help us little to understand either the purpose of the operators or the significance of the results. Working symbolically, let's apply a more systematic method to the separate components of the mapping <math>F.\!</math>
But these initial formulas are purely definitional, and help us little to understand either the purpose of the operators or the significance of the results. Working symbolically, let's apply a more systematic method to the separate components of the mapping <math>F.\!</math>
A sketch of this work is presented in the following series of Figures, where each logical proposition is expanded over the basic cells <math>\texttt{uv}, \texttt{u(v)}, \texttt{(u)v}, \texttt{(u)(v)}</math> of the 2-dimensional universe of discourse <math>U^\bullet = [u, v].\!</math>
A sketch of this work is presented in the following series of Figures, where each logical proposition is expanded over the basic cells <math>uv, u \texttt{(} v \texttt{)}, \texttt{(} u \texttt{)} v, \texttt{(} u \texttt{)(} v \texttt{)}\!</math> of the 2-dimensional universe of discourse <math>U^\bullet = [u, v].\!</math>
===Computation Summary : <math>f(u, v) = \texttt{((u)(v))}</math>===
===Computation Summary : <math>f(u, v) = \texttt{((u)(v))}</math>===
|}
|}
Figure 1.2 expands <math>\operatorname{E}f = \texttt{((u + du)(v + dv))}</math> over <math>[u, v]\!</math> to give:
Figure 1.2 expands <math>\mathrm{E}f = \texttt{((u + du)(v + dv))}</math> over <math>[u, v]\!</math> to give:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
|}
|}
Figure 1.3 expands <math>\operatorname{D}f = f + \operatorname{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" width="90%"
{| align="center" cellpadding="8" width="90%"
|}
|}
Figure 2.2 expands <math>\operatorname{E}g = \texttt{((u + du,~v + dv))}</math> over <math>[u, v]\!</math> to give:
Figure 2.2 expands <math>\mathrm{E}g = \texttt{((u + du,~v + dv))}</math> over <math>[u, v]\!</math> to give:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
|}
|}
Figure 2.3 expands <math>\operatorname{D}g = g + \operatorname{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" width="90%"
{| align="center" cellpadding="8" width="90%"
|}
|}
To speed things along, I will skip a mass of motivating discussion and just exhibit the simplest form of a differential <math>\operatorname{d}F\!</math> for the current example of a logical transformation <math>F,\!</math> after which the majority of the easiest questions will have been answered in visually intuitive terms.
To speed things along, I will skip a mass of motivating discussion and just exhibit the simplest form of a differential <math>\mathrm{d}F\!</math> for the current example of a logical transformation <math>F,\!</math> after which the majority of the easiest questions will have been answered in visually intuitive terms.
For <math>F = (f, g)\!</math> we have <math>\operatorname{d}F = (\operatorname{d}f, \operatorname{d}g),</math> and so we can proceed componentwise, patching the pieces back together at the end.
For <math>F = (f, g)\!</math> we have <math>\mathrm{d}F = (\mathrm{d}f, \mathrm{d}g),</math> and so we can proceed componentwise, patching the pieces back together at the end.
We have prepared the ground already by computing these terms:
We have prepared the ground already by computing these terms:
|
|
<math>\begin{array}{lll}
<math>\begin{array}{lll}
\operatorname{E}f & = & \texttt{(( u + du )( v + dv ))}
\mathrm{E}f & = & \texttt{(( u + du )( v + dv ))}
\\ \\
\\ \\
\operatorname{E}g & = & \texttt{(( u + du ,~ v + dv ))}
\mathrm{E}g & = & \texttt{(( u + du ,~ v + dv ))}
\\ \\
\\ \\
\operatorname{D}f & = & \texttt{((u)(v)) ~+~ (( u + du )( v + dv ))}
\mathrm{D}f & = & \texttt{((u)(v)) ~+~ (( u + du )( v + dv ))}
\\ \\
\\ \\
\operatorname{D}g & = & \texttt{((u,~v)) ~+~ (( u + du ,~ v + dv ))}
\mathrm{D}g & = & \texttt{((u,~v)) ~+~ (( u + du ,~ v + dv ))}
\end{array}\!</math>
\end{array}\!</math>
|}
|}
As a matter of fact, computing the symmetric differences <math>\operatorname{D}f = f + \operatorname{E}f</math> and <math>\operatorname{D}g = g + \operatorname{E}g</math> has already taken care of the ''localizing'' part of the task by subtracting out the forms of <math>f\!</math> and <math>g\!</math> from the forms of <math>\operatorname{E}f</math> and <math>\operatorname{E}g,</math> respectively. Thus all we have left to do is to decide what linear propositions best approximate the difference maps <math>\operatorname{D}f</math> and <math>\operatorname{D}g,</math> respectively.
As a matter of fact, computing the symmetric differences <math>\mathrm{D}f = f + \mathrm{E}f</math> and <math>\mathrm{D}g = g + \mathrm{E}g</math> has already taken care of the ''localizing'' part of the task by subtracting out the forms of <math>f\!</math> and <math>g\!</math> from the forms of <math>\mathrm{E}f</math> and <math>\mathrm{E}g,</math> respectively. Thus all we have left to do is to decide what linear propositions best approximate the difference maps <math>\mathrm{D}f</math> and <math>\mathrm{D}g,</math> respectively.
This raises the question: What is a linear proposition?
This raises the question: What is a linear proposition?
In particular, the linear functions that we want will be linear functions in the differential variables <math>du\!</math> and <math>dv.\!</math>
In particular, the linear functions that we want will be linear functions in the differential variables <math>du\!</math> and <math>dv.\!</math>
As it turns out, there are just four linear propositions in the associated ''differential universe'' <math>\operatorname{d}U^\bullet = [du, dv],</math> and these are the propositions that are commonly denoted: <math>\texttt{0}, \texttt{du}, \texttt{dv}, \texttt{du + dv},</math> in other words, <math>\texttt{()}, \texttt{du}, \texttt{dv}, \texttt{(du, dv)}.</math>
As it turns out, there are just four linear propositions in the associated ''differential universe'' <math>\mathrm{d}U^\bullet = [du, dv],</math> and these are the propositions that are commonly denoted: <math>\texttt{0}, \texttt{du}, \texttt{dv}, \texttt{du + dv},</math> in other words, <math>\texttt{()}, \texttt{du}, \texttt{dv}, \texttt{(du, dv)}.</math>
==Notions of Approximation==
==Notions of Approximation==
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>\operatorname{d}U^\bullet = [du, dv]</math> that best approximates the patch of the difference map <math>\operatorname{D}f</math> that is located there, yielding the following formula for the differential <math>\operatorname{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 = [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>
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
| <math>\operatorname{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>\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>
|}
|}
|}
|}
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>\operatorname{d}U^\bullet = [du, dv]</math> that best approximates the patch of the difference map <math>\operatorname{D}g</math> that is located there, yielding the following formula for the differential <math>\operatorname{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" width="90%"
| <math>\operatorname{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>\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>
|}
|}
|}
|}
Well, <math>g,\!</math> that was easy, seeing as how <math>\operatorname{D}g</math> is already linear at each locus, <math>\operatorname{d}g = \operatorname{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>\operatorname{E}F : [u, v, du, dv] \to [u, v, du, dv]</math> and breaking it into an analytic series, <math>\operatorname{E}F = F + \operatorname{d}F + \operatorname{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)(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
so on until there is nothing left to analyze any further.
so on until there is nothing left to analyze any further.
|
|
<math>\begin{array}{lccccc}
<math>\begin{array}{lccccc}
1. & \operatorname{E}F & = & \operatorname{d}^0 F & + & \operatorname{r}^0 F
1. & \mathrm{E}F & = & \mathrm{d}^0 F & + & \mathrm{r}^0 F
\\
\\
2. & \operatorname{r}^0 F & = & \operatorname{d}^1 F & + & \operatorname{r}^1 F
2. & \mathrm{r}^0 F & = & \mathrm{d}^1 F & + & \mathrm{r}^1 F
\\
\\
3. & \operatorname{r}^1 F & = & \operatorname{d}^2 F & + & \operatorname{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>\operatorname{E}F = F + \operatorname{D}F,</math> and we have just reached Step 2 in the form <math>\operatorname{D}F = \operatorname{d}F + \operatorname{r}F,</math> where <math>\operatorname{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:
'''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:
|}
|}
Figure 1.2 shows the expansion of <math>\operatorname{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 + du)(v + dv))}</math> over <math>[u, v]\!</math> to produce the expression:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
|}
|}
<math>\operatorname{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>\operatorname{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.
<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.
Figure 1.3 shows the expansion of <math>\operatorname{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>\operatorname{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>\operatorname{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.
<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.
Figure 1.4 approximates <math>\operatorname{D}f</math> by the linear form <math>\operatorname{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}
\operatorname{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)}
& = & \texttt{uv} \cdot \texttt{0} & + & \texttt{u(v)} \cdot \texttt{du} & + & \texttt{(u)v} \cdot \texttt{dv} & + & \texttt{(u)(v)} \cdot \texttt{(du, dv)}
\\ \\
\\ \\
|}
|}
Figure 1.5 shows what remains of the difference map <math>\operatorname{D}f</math> when the first order linear contribution <math>\operatorname{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{matrix}
\operatorname{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}
& = & \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}
\\ \\
\\ \\
|}
|}
Figure 2.2 shows the expansion of <math>\operatorname{E}g = \texttt{((u + du, v + dv))}</math> over <math>[u, v]\!</math> to produce the expression:
Figure 2.2 shows the expansion of <math>\mathrm{E}g = \texttt{((u + du, v + dv))}</math> over <math>[u, v]\!</math> to produce the expression:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
|}
|}
<math>\operatorname{E}g</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>g\!</math> is true. In this case, where the prevailing proposition <math>g\!</math> is <math>\texttt{((u, v))},</math> the component <math>\texttt{uv} \cdot \texttt{((du, dv))}</math> of <math>\operatorname{E}g</math> tells you this: If <math>u\!</math> and <math>v\!</math> are both true where you are, then change either both or neither of <math>u\!</math> and <math>v\!</math> at the same time, and you will attain a place where <math>\texttt{((du, dv))}</math> is true.
<math>\mathrm{E}g</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>g\!</math> is true. In this case, where the prevailing proposition <math>g\!</math> is <math>\texttt{((u, v))},</math> the component <math>\texttt{uv} \cdot \texttt{((du, dv))}</math> of <math>\mathrm{E}g</math> tells you this: If <math>u\!</math> and <math>v\!</math> are both true where you are, then change either both or neither of <math>u\!</math> and <math>v\!</math> at the same time, and you will attain a place where <math>\texttt{((du, dv))}</math> is true.
Figure 2.3 shows the expansion of <math>\operatorname{D}g</math> over <math>[u, v]\!</math> to produce the expression:
Figure 2.3 shows the expansion of <math>\mathrm{D}g</math> over <math>[u, v]\!</math> to produce the expression:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
|}
|}
<math>\operatorname{D}g</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>g,\!</math> that is, if you want to get to a place where the value of <math>g\!</math> is different from what it is where you are. In the present case, where the ruling proposition <math>g\!</math> is <math>\texttt{((u, v))},</math> the term <math>\texttt{uv} \cdot \texttt{(du, dv)}</math> of <math>\operatorname{D}g</math> tells you this: If <math>u\!</math> and <math>v\!</math> are both true where you are, then you would have to change one or the other but not both <math>u\!</math> and <math>v\!</math> in order to reach a place where the value of <math>g\!</math> is different from what it is where you are.
<math>\mathrm{D}g</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>g,\!</math> that is, if you want to get to a place where the value of <math>g\!</math> is different from what it is where you are. In the present case, where the ruling proposition <math>g\!</math> is <math>\texttt{((u, v))},</math> the term <math>\texttt{uv} \cdot \texttt{(du, dv)}</math> of <math>\mathrm{D}g</math> tells you this: If <math>u\!</math> and <math>v\!</math> are both true where you are, then you would have to change one or the other but not both <math>u\!</math> and <math>v\!</math> in order to reach a place where the value of <math>g\!</math> is different from what it is where you are.
Figure 2.4 approximates <math>\operatorname{D}g</math> by the linear form <math>\operatorname{d}g</math> that expands over <math>[u, v]\!</math> as follows:
Figure 2.4 approximates <math>\mathrm{D}g</math> by the linear form <math>\mathrm{d}g</math> that expands over <math>[u, v]\!</math> as follows:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
|
|
<math>\begin{array}{lll}
<math>\begin{array}{lll}
\operatorname{d}g
\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)}
& = & \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)}
\\ \\
\\ \\
|}
|}
Figure 2.5 shows what remains of the difference map <math>\operatorname{D}g</math> when the first order linear contribution <math>\operatorname{d}g</math> is removed, namely:
Figure 2.5 shows what remains of the difference map <math>\mathrm{D}g</math> when the first order linear contribution <math>\mathrm{d}g</math> is removed, namely:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
|
|
<math>\begin{matrix}
<math>\begin{matrix}
\operatorname{r}g
\mathrm{r}g
& = & \texttt{uv} \cdot \texttt{0} & + & \texttt{u(v)} \cdot \texttt{0} & + & \texttt{(u)v} \cdot \texttt{0} & + & \texttt{(u)(v)} \cdot \texttt{0}
& = & \texttt{uv} \cdot \texttt{0} & + & \texttt{u(v)} \cdot \texttt{0} & + & \texttt{(u)v} \cdot \texttt{0} & + & \texttt{(u)(v)} \cdot \texttt{0}
\\ \\
\\ \\
By way of providing a simple illustration of Cook's Theorem, namely, that “Propositional Satisfiability is NP-Complete”, I will describe one way to translate finite approximations of turing machines into propositional expressions, using the cactus language syntax for propositional calculus that I will describe in more detail as we proceed.
By way of providing a simple illustration of Cook's Theorem, namely, that “Propositional Satisfiability is NP-Complete”, I will describe one way to translate finite approximations of turing machines into propositional expressions, using the cactus language syntax for propositional calculus that I will describe in more detail as we proceed.
:; <math>\operatorname{Stilt}(k) =\!</math>
:; <math>\mathrm{Stilt}(k) =\!</math>
:: '''Space and time limited turing machine''',
:: '''Space and time limited turing machine''',
:: with <math>k\!</math> units of space and <math>k\!</math> units of time.
:: with <math>k\!</math> units of space and <math>k\!</math> units of time.
:; <math>\operatorname{Stunt}(k) =\!</math>
:; <math>\mathrm{Stunt}(k) =\!</math>
:: '''Space and time limited turing machine''',
:: '''Space and time limited turing machine''',
:: for computing the parity of a bit string, with number of tape cells of input equal to <math>k.\!</math>
:: for computing the parity of a bit string, with number of tape cells of input equal to <math>k.\!</math>
<br>
<br>
The TM has a ''finite automaton'' (FA) as one component. Let us refer to this particular FA by the name of <math>\operatorname{M}.</math>
The TM has a ''finite automaton'' (FA) as one component. Let us refer to this particular FA by the name of <math>\mathrm{M}.</math>
The ''tape head'' (that is, the ''read unit'') will be called <math>\operatorname{H}.</math> The ''registers'' are also called ''tape cells'' or ''tape squares''.
The ''tape head'' (that is, the ''read unit'') will be called <math>\mathrm{H}.</math> The ''registers'' are also called ''tape cells'' or ''tape squares''.
===Finite Approximations===
===Finite Approximations===
To see how each finite approximation to a given turing machine can be given a purely propositional description, one fixes the parameter <math>k\!</math> and limits the rest of the discussion to describing <math>\operatorname{Stilt}(k),\!</math> which is not really a full-fledged TM anymore but just a finite automaton in disguise.
To see how each finite approximation to a given turing machine can be given a purely propositional description, one fixes the parameter <math>k\!</math> and limits the rest of the discussion to describing <math>\mathrm{Stilt}(k),\!</math> which is not really a full-fledged TM anymore but just a finite automaton in disguise.
In this example, for the sake of a minimal illustration, we choose <math>k = 2,\!</math> and discuss <math>\operatorname{Stunt}(2).</math> Since the zeroth tape cell and the last tape cell are both occupied by the character <math>^{\backprime\backprime}\texttt{\#}^{\prime\prime}</math> that is used for both the ''beginning of file'' <math>(\operatorname{bof})</math> and the ''end of file'' <math>(\operatorname{eof})</math> markers, this allows for only one digit of significant computation.
In this example, for the sake of a minimal illustration, we choose <math>k = 2,\!</math> and discuss <math>\mathrm{Stunt}(2).</math> Since the zeroth tape cell and the last tape cell are both occupied by the character <math>^{\backprime\backprime}\texttt{\#}^{\prime\prime}</math> that is used for both the ''beginning of file'' <math>(\mathrm{bof})</math> and the ''end of file'' <math>(\mathrm{eof})</math> markers, this allows for only one digit of significant computation.
To translate <math>\operatorname{Stunt}(2)</math> into propositional form we use the following collection of basic propositions, boolean variables, or logical features, depending on what one prefers to call them:
To translate <math>\mathrm{Stunt}(2)</math> into propositional form we use the following collection of basic propositions, boolean variables, or logical features, depending on what one prefers to call them:
The basic propositions for describing the ''present state function'' <math>\operatorname{QF} : P \to Q</math> are these:
The basic propositions for describing the ''present state function'' <math>\mathrm{QF} : P \to Q</math> are these:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
| At the point-in-time <math>p_i,\!</math> the finite state machine <math>\operatorname{M}</math> is in the state <math>q_j.\!</math>
| At the point-in-time <math>p_i,\!</math> the finite state machine <math>\mathrm{M}</math> is in the state <math>q_j.\!</math>
|}
|}
The basic propositions for describing the ''present register function'' <math>\operatorname{RF} : P \to R</math> are these:
The basic propositions for describing the ''present register function'' <math>\mathrm{RF} : P \to R</math> are these:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
| At the point-in-time <math>p_i,\!</math> the tape head <math>\operatorname{H}</math> is on the tape cell <math>r_j.\!</math>
| At the point-in-time <math>p_i,\!</math> the tape head <math>\mathrm{H}</math> is on the tape cell <math>r_j.\!</math>
|}
|}
The basic propositions for describing the ''present symbol function'' <math>\operatorname{SF} : P \to (R \to S)</math> are these:
The basic propositions for describing the ''present symbol function'' <math>\mathrm{SF} : P \to (R \to S)</math> are these:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
===Initial Conditions===
===Initial Conditions===
Given but a single free square on the tape, there are just two different sets of initial conditions for <math>\operatorname{Stunt}(2),</math> the finite approximation to the parity turing machine that we are presently considering.
Given but a single free square on the tape, there are just two different sets of initial conditions for <math>\mathrm{Stunt}(2),</math> the finite approximation to the parity turing machine that we are presently considering.
====Initial Conditions for Tape Input "0"====
====Initial Conditions for Tape Input "0"====
The following conjunction of 5 basic propositions describes the initial conditions when <math>\operatorname{Stunt}(2)</math> is started with an input of "0" in its free square:
The following conjunction of 5 basic propositions describes the initial conditions when <math>\mathrm{Stunt}(2)</math> is started with an input of "0" in its free square:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding=8" width="90%"
{| align="center" cellpadding=8" width="90%"
|
|
<p>At time <math>p_0,\!</math> machine <math>\operatorname{M}</math> is in the state <math>q_0,\!</math></p>
<p>At time <math>p_0,\!</math> machine <math>\mathrm{M}</math> is in the state <math>q_0,\!</math></p>
<p>At time <math>p_0,\!</math> scanner <math>\operatorname{H}</math> is reading cell <math>r_1,\!</math></p>
<p>At time <math>p_0,\!</math> scanner <math>\mathrm{H}</math> is reading cell <math>r_1,\!</math></p>
<p>At time <math>p_0,\!</math> cell <math>r_0\!</math> contains the symbol <math>\texttt{\#},</math></p>
<p>At time <math>p_0,\!</math> cell <math>r_0\!</math> contains the symbol <math>\texttt{\#},</math></p>
<p>At time <math>p_0,\!</math> cell <math>r_1\!</math> contains the symbol <math>\texttt{0},</math></p>
<p>At time <math>p_0,\!</math> cell <math>r_1\!</math> contains the symbol <math>\texttt{0},</math></p>
====Initial Conditions for Tape Input "1"====
====Initial Conditions for Tape Input "1"====
The following conjunction of 5 basic propositions describes the initial conditions when <math>\operatorname{Stunt}(2)</math> is started with an input of "1" in its free square:
The following conjunction of 5 basic propositions describes the initial conditions when <math>\mathrm{Stunt}(2)</math> is started with an input of "1" in its free square:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding=8" width="90%"
{| align="center" cellpadding=8" width="90%"
|
|
<p>At time <math>p_0,\!</math> machine <math>\operatorname{M}</math> is in the state <math>q_0,\!</math></p>
<p>At time <math>p_0,\!</math> machine <math>\mathrm{M}</math> is in the state <math>q_0,\!</math></p>
<p>At time <math>p_0,\!</math> scanner <math>\operatorname{H}</math> is reading cell <math>r_1,\!</math></p>
<p>At time <math>p_0,\!</math> scanner <math>\mathrm{H}</math> is reading cell <math>r_1,\!</math></p>
<p>At time <math>p_0,\!</math> cell <math>r_0\!</math> contains the symbol <math>\texttt{\#},</math></p>
<p>At time <math>p_0,\!</math> cell <math>r_0\!</math> contains the symbol <math>\texttt{\#},</math></p>
<p>At time <math>p_0,\!</math> cell <math>r_1\!</math> contains the symbol <math>\texttt{1},</math></p>
<p>At time <math>p_0,\!</math> cell <math>r_1\!</math> contains the symbol <math>\texttt{1},</math></p>
===Propositional Program===
===Propositional Program===
A complete description of <math>\operatorname{Stunt}(2)</math> in propositional form is obtained by conjoining one of the above choices for initial conditions with all of the following sets of propositions, that serve in effect as a simple type of ''declarative program'', telling us all that we need to know about the anatomy and behavior of the truncated TM in question.
A complete description of <math>\mathrm{Stunt}(2)</math> in propositional form is obtained by conjoining one of the above choices for initial conditions with all of the following sets of propositions, that serve in effect as a simple type of ''declarative program'', telling us all that we need to know about the anatomy and behavior of the truncated TM in question.
====Mediate Conditions====
====Mediate Conditions====
===Interpretation of the Propositional Program===
===Interpretation of the Propositional Program===
Let us now run through the propositional specification of <math>\operatorname{Stunt}(2),</math> our truncated TM, and paraphrase what it says in ordinary language.
Let us now run through the propositional specification of <math>\mathrm{Stunt}(2),</math> our truncated TM, and paraphrase what it says in ordinary language.
====Mediate Conditions====
====Mediate Conditions====
|
|
<math>\begin{array}{l}
<math>\begin{array}{l}
\operatorname{not}~ p ~\operatorname{without}~ q
\mathrm{not}~ p ~\mathrm{without}~ q
\\[4pt]
\\[4pt]
p ~\operatorname{implies}~ q
p ~\mathrm{implies}~ q
\\[4pt]
\\[4pt]
\operatorname{if}~ p ~\operatorname{then}~ q
\mathrm{if}~ p ~\mathrm{then}~ q
\\[4pt]
\\[4pt]
p \Rightarrow q
p \Rightarrow q
{| align="center" cellpadding=8" width="90%"
{| align="center" cellpadding=8" width="90%"
|
|
<p>If <math>\operatorname{M}</math> at <math>p_0\!</math> is in state <math>q_\#,\!</math> then <math>\operatorname{M}</math> at <math>p_1\!</math> is in state <math>q_\#,\!</math> and</p>
<p>If <math>\mathrm{M}</math> at <math>p_0\!</math> is in state <math>q_\#,\!</math> then <math>\mathrm{M}</math> at <math>p_1\!</math> is in state <math>q_\#,\!</math> and</p>
<p>If <math>\operatorname{M}</math> at <math>p_0\!</math> is in state <math>q_*,\!</math> then <math>\operatorname{M}</math> at <math>p_1\!</math> is in state <math>q_*,\!</math> and</p>
<p>If <math>\mathrm{M}</math> at <math>p_0\!</math> is in state <math>q_*,\!</math> then <math>\mathrm{M}</math> at <math>p_1\!</math> is in state <math>q_*,\!</math> and</p>
<p>If <math>\operatorname{M}</math> at <math>p_1\!</math> is in state <math>q_\#,\!</math> then <math>\operatorname{M}</math> at <math>p_2\!</math> is in state <math>q_\#,\!</math> and</p>
<p>If <math>\mathrm{M}</math> at <math>p_1\!</math> is in state <math>q_\#,\!</math> then <math>\mathrm{M}</math> at <math>p_2\!</math> is in state <math>q_\#,\!</math> and</p>
<p>If <math>\operatorname{M}</math> at <math>p_1\!</math> is in state <math>q_*,\!</math> then <math>\operatorname{M}</math> at <math>p_2\!</math> is in state <math>q_*.\!</math></p>
<p>If <math>\mathrm{M}</math> at <math>p_1\!</math> is in state <math>q_*,\!</math> then <math>\mathrm{M}</math> at <math>p_2\!</math> is in state <math>q_*.\!</math></p>
|}
|}
|}
|}
In cactus syntax, an expression of the form <math>\texttt{((p)(q))}</math> expresses the disjunction <math>p ~\operatorname{or}~ q.</math> The corresponding cactus graph, here just a tree, has the following shape:
In cactus syntax, an expression of the form <math>\texttt{((p)(q))}</math> expresses the disjunction <math>p ~\mathrm{or}~ q.</math> The corresponding cactus graph, here just a tree, has the following shape:
<br>
<br>
{| align="center" cellpadding=8" width="90%"
{| align="center" cellpadding=8" width="90%"
|
|
<p>At time <math>p_2\!</math> machine <math>\operatorname{M}</math> is in state <math>q_\#,\!</math> or</p>
<p>At time <math>p_2\!</math> machine <math>\mathrm{M}</math> is in state <math>q_\#,\!</math> or</p>
<p>At time <math>p_2\!</math> machine <math>\operatorname{M}</math> is in state <math>q_*.\!</math></p>
<p>At time <math>p_2\!</math> machine <math>\mathrm{M}</math> is in state <math>q_*.\!</math></p>
|}
|}
<br>
<br>
The State Partition segment of the propositional program consists of three universal partition expressions, taken in conjunction expressing the condition that <math>\operatorname{M}</math> has to be in one and only one of its states at each point in time under consideration. In short, we have the constraint:
The State Partition segment of the propositional program consists of three universal partition expressions, taken in conjunction expressing the condition that <math>\mathrm{M}</math> has to be in one and only one of its states at each point in time under consideration. In short, we have the constraint:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
<p>At each of the points in time <math>p_i,\!</math> for <math>i\!</math> in the set <math>\{ 0, 1, 2 \},\!</math></p>
<p>At each of the points in time <math>p_i,\!</math> for <math>i\!</math> in the set <math>\{ 0, 1, 2 \},\!</math></p>
<p><math>\operatorname{M}</math> can be in exactly one state <math>q_j,\!</math> for <math>j\!</math> in the set <math>\{ 0, 1, \#, * \}.\!</math></p>
<p><math>\mathrm{M}</math> can be in exactly one state <math>q_j,\!</math> for <math>j\!</math> in the set <math>\{ 0, 1, \#, * \}.\!</math></p>
|}
|}
|}
|}
The Register Partition segment of the propositional program consists of three universal partition expressions, taken in conjunction saying that the read head <math>\operatorname{H}</math> must be reading one and only one of the registers or tape cells available to it at each of the points in time under consideration. In sum:
The Register Partition segment of the propositional program consists of three universal partition expressions, taken in conjunction saying that the read head <math>\mathrm{H}</math> must be reading one and only one of the registers or tape cells available to it at each of the points in time under consideration. In sum:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
<p>At each of the points in time <math>p_i,\!</math> for <math>i = 0, 1, 2,\!</math></p>
<p>At each of the points in time <math>p_i,\!</math> for <math>i = 0, 1, 2,\!</math></p>
<p><math>\operatorname{H}</math> is reading exactly one cell <math>r_j,\!</math> for <math>j = 0, 1, 2.\!</math>
<p><math>\mathrm{H}</math> is reading exactly one cell <math>r_j,\!</math> for <math>j = 0, 1, 2.\!</math>
|}
|}
|}
|}
The Symbol Partition segment of the propositional program for <math>\operatorname{Stunt}(2)</math> consists of nine universal partition expressions, taken in conjunction stipulating that there has to be one and only one symbol in each of the registers at each point in time under consideration. In short, we have:
The Symbol Partition segment of the propositional program for <math>\mathrm{Stunt}(2)</math> consists of nine universal partition expressions, taken in conjunction stipulating that there has to be one and only one symbol in each of the registers at each point in time under consideration. In short, we have:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
|<math>\operatorname{If}</math>
|<math>\mathrm{If}</math>
|-
|-
| At the time <math>p_i,\!</math> the tape cell <math>r_j\!</math> bears the mark <math>s_k,\!</math>
| At the time <math>p_i,\!</math> the tape cell <math>r_j\!</math> bears the mark <math>s_k,\!</math>
|-
|-
| <math>\operatorname{But}</math> it is not the case that:
| <math>\mathrm{But}</math> it is not the case that:
|-
|-
| At the time <math>p_i,\!</math> the tape head is on the tape cell <math>r_j,\!</math>
| At the time <math>p_i,\!</math> the tape head is on the tape cell <math>r_j,\!</math>
|-
|-
| <math>\operatorname{Then}</math>
| <math>\mathrm{Then}</math>
|-
|-
| At the time <math>p_{i+1},\!</math> the tape cell <math>r_j\!</math> bears the mark <math>s_k.\!</math>
| At the time <math>p_{i+1},\!</math> the tape cell <math>r_j\!</math> bears the mark <math>s_k.\!</math>
|}
|}
The Transition Relation segment of the propositional program for <math>\operatorname{Stunt}(2)</math> consists of sixteen implication statements with complex antecedents and consequents. Taken together, these give propositional expression to the TM Figure and Table that were given at the outset.
The Transition Relation segment of the propositional program for <math>\mathrm{Stunt}(2)</math> consists of sixteen implication statements with complex antecedents and consequents. Taken together, these give propositional expression to the TM Figure and Table that were given at the outset.
Just by way of a single example, consider the clause:
Just by way of a single example, consider the clause:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
|<math>\operatorname{If}</math>
|<math>\mathrm{If}</math>
|-
|-
| At the time <math>p_0,\!</math> the machine <math>\operatorname{M}</math> is in the state <math>q_0,\!</math> and
| At the time <math>p_0,\!</math> the machine <math>\mathrm{M}</math> is in the state <math>q_0,\!</math> and
|-
|-
| At the time <math>p_0,\!</math> the scanner <math>\operatorname{H}</math> is reading cell <math>r_1,\!</math> and
| At the time <math>p_0,\!</math> the scanner <math>\mathrm{H}</math> is reading cell <math>r_1,\!</math> and
|-
|-
| At the time <math>p_0,\!</math> the tape cell <math>r_1\!</math> contains a <math>\texttt{1},</math>
| At the time <math>p_0,\!</math> the tape cell <math>r_1\!</math> contains a <math>\texttt{1},</math>
|-
|-
| <math>\operatorname{Then}</math>
| <math>\mathrm{Then}</math>
|-
|-
| At the time <math>p_1,\!</math> the machine <math>\operatorname{M}</math> is in the state <math>q_1,\!</math> and
| At the time <math>p_1,\!</math> the machine <math>\mathrm{M}</math> is in the state <math>q_1,\!</math> and
|-
|-
| At the time <math>p_1,\!</math> the scanner <math>\operatorname{H}</math> is reading cell <math>r_2,\!</math> and
| At the time <math>p_1,\!</math> the scanner <math>\mathrm{H}</math> is reading cell <math>r_2,\!</math> and
|-
|-
| At the time <math>p_1,\!</math> the tape cell <math>r_1\!</math> contains a <math>\texttt{1}.</math>
| At the time <math>p_1,\!</math> the tape cell <math>r_1\!</math> contains a <math>\texttt{1}.</math>
===Computation===
===Computation===
The propositional program for <math>\operatorname{Stunt}(2)</math> uses the following set
The propositional program for <math>\mathrm{Stunt}(2)</math> uses the following set
of <math>9 + 12 + 36 = 57\!</math> basic propositions or boolean variables:
of <math>9 + 12 + 36 = 57\!</math> basic propositions or boolean variables:
===Output===
===Output===
One component of the <math>\begin{smallmatrix}\operatorname{Theme~One}\end{smallmatrix}</math> program that I wrote some years ago finds all the satisfying interpretations of propositions expressed in cactus syntax. It's not a polynomial time algorithm, as you may guess, but it was just barely efficient enough to do this example in the 500 K of spare memory that I had on an old 286 PC in about 1989, so I will give you the actual outputs from those trials.
One component of the <math>\begin{smallmatrix}\mathrm{Theme~One}\end{smallmatrix}</math> program that I wrote some years ago finds all the satisfying interpretations of propositions expressed in cactus syntax. It's not a polynomial time algorithm, as you may guess, but it was just barely efficient enough to do this example in the 500 K of spare memory that I had on an old 286 PC in about 1989, so I will give you the actual outputs from those trials.
====Output Conditions for Tape Input "0"====
====Output Conditions for Tape Input "0"====
Let <math>p_0\!</math> be the proposition that we get by conjoining the proposition that describes the initial conditions for tape input "0" with the proposition that describes the truncated turing machine <math>\operatorname{Stunt}(2).</math> As it turns out, <math>p_0\!</math> has a single satisfying interpretation. This interpretation is expressible in the form of a singular proposition, which can in turn be indicated by its positive logical features, as shown in the following display:
Let <math>p_0\!</math> be the proposition that we get by conjoining the proposition that describes the initial conditions for tape input "0" with the proposition that describes the truncated turing machine <math>\mathrm{Stunt}(2).</math> As it turns out, <math>p_0\!</math> has a single satisfying interpretation. This interpretation is expressible in the form of a singular proposition, which can in turn be indicated by its positive logical features, as shown in the following display:
<br>
<br>
{| align="center" cellpadding=8" width="90%"
{| align="center" cellpadding=8" width="90%"
|
|
<p>At the time <math>p_0,\!</math> machine <math>\operatorname{M}</math> is in the state <math>q_0,\!</math> and</p>
<p>At the time <math>p_0,\!</math> machine <math>\mathrm{M}</math> is in the state <math>q_0,\!</math> and</p>
<p>At the time <math>p_0,\!</math> scanner <math>\operatorname{H}</math> is reading cell <math>r_1,\!</math> and</p>
<p>At the time <math>p_0,\!</math> scanner <math>\mathrm{H}</math> is reading cell <math>r_1,\!</math> and</p>
<p>At the time <math>p_0,\!</math> cell <math>r_0\!</math> contains the symbol <math>\texttt{\#},</math> and</p>
<p>At the time <math>p_0,\!</math> cell <math>r_0\!</math> contains the symbol <math>\texttt{\#},</math> and</p>
<p>At the time <math>p_0,\!</math> cell <math>r_1\!</math> contains the symbol <math>\texttt{0},</math> and</p>
<p>At the time <math>p_0,\!</math> cell <math>r_1\!</math> contains the symbol <math>\texttt{0},</math> and</p>
|-
|-
|
|
<p>At the time <math>p_1,\!</math> machine <math>\operatorname{M}</math> is in the state <math>q_0,\!</math> and</p>
<p>At the time <math>p_1,\!</math> machine <math>\mathrm{M}</math> is in the state <math>q_0,\!</math> and</p>
<p>At the time <math>p_1,\!</math> scanner <math>\operatorname{H}</math> is reading cell <math>r_2,\!</math> and</p>
<p>At the time <math>p_1,\!</math> scanner <math>\mathrm{H}</math> is reading cell <math>r_2,\!</math> and</p>
<p>At the time <math>p_1,\!</math> cell <math>r_0\!</math> contains the symbol <math>\texttt{\#},</math> and</p>
<p>At the time <math>p_1,\!</math> cell <math>r_0\!</math> contains the symbol <math>\texttt{\#},</math> and</p>
<p>At the time <math>p_1,\!</math> cell <math>r_1\!</math> contains the symbol <math>\texttt{0},</math> and</p>
<p>At the time <math>p_1,\!</math> cell <math>r_1\!</math> contains the symbol <math>\texttt{0},</math> and</p>
|-
|-
|
|
<p>At the time <math>p_2,\!</math> machine <math>\operatorname{M}</math> is in the state <math>q_\#,\!</math> and</p>
<p>At the time <math>p_2,\!</math> machine <math>\mathrm{M}</math> is in the state <math>q_\#,\!</math> and</p>
<p>At the time <math>p_2,\!</math> scanner <math>\operatorname{H}</math> is reading cell <math>r_1,\!</math> and</p>
<p>At the time <math>p_2,\!</math> scanner <math>\mathrm{H}</math> is reading cell <math>r_1,\!</math> and</p>
<p>At the time <math>p_2,\!</math> cell <math>r_0\!</math> contains the symbol <math>\texttt{\#},</math> and</p>
<p>At the time <math>p_2,\!</math> cell <math>r_0\!</math> contains the symbol <math>\texttt{\#},</math> and</p>
<p>At the time <math>p_2,\!</math> cell <math>r_1\!</math> contains the symbol <math>\texttt{0},</math> and</p>
<p>At the time <math>p_2,\!</math> cell <math>r_1\!</math> contains the symbol <math>\texttt{0},</math> and</p>
|}
|}
The output of <math>\operatorname{Stunt}(2)</math> being the symbol that rests under the tape head <math>\operatorname{H}</math> if and when the machine <math>\operatorname{M}</math> reaches one of its resting states, we get the result that <math>\operatorname{Parity}(0) = 0.</math>
The output of <math>\mathrm{Stunt}(2)</math> being the symbol that rests under the tape head <math>\mathrm{H}</math> if and when the machine <math>\mathrm{M}</math> reaches one of its resting states, we get the result that <math>\mathrm{Parity}(0) = 0.</math>
====Output Conditions for Tape Input "1"====
====Output Conditions for Tape Input "1"====
Let <math>p_1\!</math> be the proposition that we get by conjoining the proposition that describes the initial conditions for tape input "1" with the proposition that describes the truncated turing machine <math>\operatorname{Stunt}(2).</math> As it turns out, <math>p_1\!</math> has a single satisfying interpretation. This interpretation is expressible in the form of a singular proposition, which can in turn be indicated by its positive logical features, as shown in the following display:
Let <math>p_1\!</math> be the proposition that we get by conjoining the proposition that describes the initial conditions for tape input "1" with the proposition that describes the truncated turing machine <math>\mathrm{Stunt}(2).</math> As it turns out, <math>p_1\!</math> has a single satisfying interpretation. This interpretation is expressible in the form of a singular proposition, which can in turn be indicated by its positive logical features, as shown in the following display:
<br>
<br>
{| align="center" cellpadding=8" width="90%"
{| align="center" cellpadding=8" width="90%"
|
|
<p>At the time <math>p_0,\!</math> machine <math>\operatorname{M}</math> is in the state <math>q_0,\!</math> and</p>
<p>At the time <math>p_0,\!</math> machine <math>\mathrm{M}</math> is in the state <math>q_0,\!</math> and</p>
<p>At the time <math>p_0,\!</math> scanner <math>\operatorname{H}</math> is reading cell <math>r_1,\!</math> and</p>
<p>At the time <math>p_0,\!</math> scanner <math>\mathrm{H}</math> is reading cell <math>r_1,\!</math> and</p>
<p>At the time <math>p_0,\!</math> cell <math>r_0\!</math> contains the symbol <math>\texttt{\#},</math> and</p>
<p>At the time <math>p_0,\!</math> cell <math>r_0\!</math> contains the symbol <math>\texttt{\#},</math> and</p>
<p>At the time <math>p_0,\!</math> cell <math>r_1\!</math> contains the symbol <math>\texttt{1},</math> and</p>
<p>At the time <math>p_0,\!</math> cell <math>r_1\!</math> contains the symbol <math>\texttt{1},</math> and</p>
|-
|-
|
|
<p>At the time <math>p_1,\!</math> machine <math>\operatorname{M}</math> is in the state <math>q_1,\!</math> and</p>
<p>At the time <math>p_1,\!</math> machine <math>\mathrm{M}</math> is in the state <math>q_1,\!</math> and</p>
<p>At the time <math>p_1,\!</math> scanner <math>\operatorname{H}</math> is reading cell <math>r_2,\!</math> and</p>
<p>At the time <math>p_1,\!</math> scanner <math>\mathrm{H}</math> is reading cell <math>r_2,\!</math> and</p>
<p>At the time <math>p_1,\!</math> cell <math>r_0\!</math> contains the symbol <math>\texttt{\#},</math> and</p>
<p>At the time <math>p_1,\!</math> cell <math>r_0\!</math> contains the symbol <math>\texttt{\#},</math> and</p>
<p>At the time <math>p_1,\!</math> cell <math>r_1\!</math> contains the symbol <math>\texttt{1},</math> and</p>
<p>At the time <math>p_1,\!</math> cell <math>r_1\!</math> contains the symbol <math>\texttt{1},</math> and</p>
|-
|-
|
|
<p>At the time <math>p_2,\!</math> machine <math>\operatorname{M}</math> is in the state <math>q_*,\!</math> and</p>
<p>At the time <math>p_2,\!</math> machine <math>\mathrm{M}</math> is in the state <math>q_*,\!</math> and</p>
<p>At the time <math>p_2,\!</math> scanner <math>\operatorname{H}</math> is reading cell <math>r_1,\!</math> and</p>
<p>At the time <math>p_2,\!</math> scanner <math>\mathrm{H}</math> is reading cell <math>r_1,\!</math> and</p>
<p>At the time <math>p_2,\!</math> cell <math>r_0\!</math> contains the symbol <math>\texttt{\#},</math> and</p>
<p>At the time <math>p_2,\!</math> cell <math>r_0\!</math> contains the symbol <math>\texttt{\#},</math> and</p>
<p>At the time <math>p_2,\!</math> cell <math>r_1\!</math> contains the symbol <math>\texttt{1},</math> and</p>
<p>At the time <math>p_2,\!</math> cell <math>r_1\!</math> contains the symbol <math>\texttt{1},</math> and</p>
|}
|}
The output of <math>\operatorname{Stunt}(2)</math> being the symbol that rests under the tape head <math>\operatorname{H}</math> when and if the machine <math>\operatorname{M}</math> reaches one of its resting states, we get the result that <math>\operatorname{Parity}(1) = 1.</math>
The output of <math>\mathrm{Stunt}(2)</math> being the symbol that rests under the tape head <math>\mathrm{H}</math> when and if the machine <math>\mathrm{M}</math> reaches one of its resting states, we get the result that <math>\mathrm{Parity}(1) = 1.</math>
==Work Area==
==Work Area==
