12,080
edits
Changes
MyWikiBiz, Author Your Legacy — Tuesday November 19, 2024
Jump to navigationJump to searchDirectory:Jon Awbrey/Papers/Differential Analytic Turing Automata (view source)
Revision as of 14:14, 25 September 2013
, 14:14, 25 September 2013update
{{DISPLAYTITLE:Differential Analytic Turing Automata}}
{{DISPLAYTITLE:Differential Analytic Turing Automata}}
'''Author: [[User:Jon Awbrey|Jon Awbrey]]'''
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.
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).
An example that will figure heavily in the sequel is given by rooted trees as the species of graphs and a pair of equational transformation rules that derive from the graphical calculi of [[C.S. Peirce]], as revived and extended by George Spencer Brown.
An example that will figure heavily in the sequel is given by rooted trees as the species of graphs and a pair of equational transformation rules that derive from the graphical calculi of C.S. Peirce, as revived and extended by George Spencer Brown.
Here are the fundamental transformation rules, also referred to as the ''arithmetic axioms'', more precisely, the ''arithmetic initials''.
Here are the fundamental transformation rules, also referred to as the ''arithmetic axioms'', more precisely, the ''arithmetic initials''.
I will be making use of the ''cactus language'' extension of Peirce's Alpha Graphs, so called because it uses a species of graphs that are usually called "cacti" in graph theory. The last exposition of the cactus syntax that I've written can be found here:
I will be making use of the ''cactus language'' extension of Peirce's Alpha Graphs, so called because it uses a species of graphs that are usually called "cacti" in graph theory. The last exposition of the cactus syntax that I've written can be found here:
:* [http://mywikibiz.com/Directory:Jon_Awbrey/Papers/Propositional_Equation_Reasoning_Systems Propositional Equation Reasoning Systems (PERS)]
:* [[Propositional Equation Reasoning Systems|Propositional Equation Reasoning Systems (PERS)]]
The representational and computational efficiency of the cactus language for the tasks that are usually associated with boolean algebra and propositional calculus makes it possible to entertain a further extension, to what we may call ''differential logic'', because it develops this basic level of logic in the same way that differential calculus augments analytic geometry to handle change and diversity. There are several different introductions to differential logic that I have written and distributed across the Internet. You might start with the following couple of treatments:
The representational and computational efficiency of the cactus language for the tasks that are usually associated with boolean algebra and propositional calculus makes it possible to entertain a further extension, to what we may call ''differential logic'', because it develops this basic level of logic in the same way that differential calculus augments analytic geometry to handle change and diversity. There are several different introductions to differential logic that I have written and distributed across the Internet. You might start with the following couple of treatments:
|}
|}
"Aha!" we say, and think we see the way of things, writing down the rule <math>\texttt{x}^\prime = \texttt{(x)}</math> where <math>\texttt{x}^\prime</math> is the next state after <math>\texttt{x},</math> and <math>\texttt{(x)}</math> is the negation of <math>\texttt{x}</math> in boolean logic.
"Aha!" we say, and think we see the way of things, writing down the rule <math>\texttt{x}^\prime = \texttt{(x)}</math> where <math>\texttt{x}^\prime</math> is the next state after <math>\texttt{x},</math> and <math>\texttt{(x)}</math> is the negation of <math>\texttt{x}\!</math> in boolean logic.
Another way to detect patterns is to write out a table of finite differences. For this example, we would get:
Another way to detect patterns is to write out a table of finite differences. For this example, we would get:
There is a more detailed account of differential logic in the following paper:
There is a more detailed account of differential logic in the following paper:
:* [[Directory:Jon_Awbrey/Papers/Differential_Logic_and_Dynamic_Systems_2.0|Differential Logic and Dynamic Systems]]
:* [[Differential Logic and Dynamic Systems 2.0|Differential Logic and Dynamic Systems]]
For future reference, here are a couple of handy rosetta stones for translating back and forth between different notations for the boolean functions <math>f : \mathbb{B}^k \to \mathbb{B},</math> where <math>k = 1, 2.\!</math>
For future reference, here are a couple of handy rosetta stones for translating back and forth between different notations for the boolean functions <math>f : \mathbb{B}^k \to \mathbb{B},</math> where <math>k = 1, 2.\!</math>
:* [[Directory:Jon_Awbrey/Papers/Differential_Logic_and_Dynamic_Systems_2.0#Tables_of_Propositional_Forms|Tables of Propositional Forms]]
:* [[Differential Logic and Dynamic Systems 2.0#Tables of Propositional Forms|Tables of Propositional Forms]]
==Example 2==
==Example 2==
|}
|}
Note that the state <math>\begin{matrix}\texttt{x (dx)(d}^\texttt{2}\texttt{x)},\end{matrix}</math> that is, <math>\begin{matrix}(\texttt{x}, \texttt{dx}, \texttt{d}^\texttt{2}\texttt{x}) ~=~ (1, 0, 0),\end{matrix}</math> is a stable attractor for both orbits.
Note that the state <math>\begin{matrix}\texttt{x (dx)(d}^\texttt{2}\texttt{x)},\end{matrix}\!</math> that is, <math>\begin{matrix}(\texttt{x}, \texttt{dx}, \texttt{d}^\texttt{2}\texttt{x}) ~=~ (1, 0, 0),\end{matrix}</math> is a stable attractor for both orbits.
Further discussion of this example, complete with charts and graphs, can be found at this location:
Further discussion of this example, complete with charts and graphs, can be found at this location:
:* [[Directory:Jon_Awbrey/Papers/Differential_Logic_and_Dynamic_Systems_2.0#Example_1._A_Square_Rigging|Example 1. A Square Rigging]]
:* [[Differential Logic and Dynamic Systems 2.0#Example 1. A Square Rigging|Example 1. A Square Rigging]]
==Example 3==
==Example 3==
But first, let me introduce a few more elements of general notation that I'll be using to describe finite dimensional universes of discourse and the qualitative dynamics that we envision occurring in them.
But first, let me introduce a few more elements of general notation that I'll be using to describe finite dimensional universes of discourse and the qualitative dynamics that we envision occurring in them.
Let <math>\mathcal{X} = \{ x_1, \ldots, x_n \}</math> be the ''alphabet'' of logical ''features'' or ''variables'' that we use to describe the n-dimensional universe of discourse <math>X^\circ = [\mathcal{X}] = [ x_1, \ldots, x_n ].</math> Picturesquely viewed, one may think of a venn diagram with n overlapping "circles" that are labeled with the feature names in the set <math>\mathcal{X}.</math> Staying with this picture, one visualizes the universe of discourse <math>X^\circ = [\mathcal{X}]</math> as having two layers: (1) the set <math>X = \langle \mathcal{X} \rangle = \langle x_1, \dots, x_n \rangle</math> of ''points'' or ''cells'' — in another sense of the word than when we speak of ''cellular automata'' — (2) the set <math>X^\uparrow = (X \to \mathbb{B})</math> of ''propositions'', boolean-valued functions, or maps from <math>X\!</math> to <math>\mathbb{B}.</math>
Let <math>\mathcal{X} = \{ x_1, \ldots, x_n \}</math> be the ''alphabet'' of logical ''features'' or ''variables'' that we use to describe the n-dimensional universe of discourse <math>X^\Box = [\mathcal{X}] = [ x_1, \ldots, x_n ].</math> Picturesquely viewed, one may think of a venn diagram with n overlapping "circles" that are labeled with the feature names in the set <math>\mathcal{X}.</math> Staying with this picture, one visualizes the universe of discourse <math>X^\Box = [\mathcal{X}]\!</math> as having two layers: (1) the set <math>X = \langle \mathcal{X} \rangle = \langle x_1, \dots, x_n \rangle</math> of ''points'' or ''cells'' — in another sense of the word than when we speak of ''cellular automata'' — (2) the set <math>X^\uparrow = (X \to \mathbb{B})</math> of ''propositions'', boolean-valued functions, or maps from <math>X\!</math> to <math>\mathbb{B}.</math>
Thus, we may speak of the universe of discourse <math>X^\circ</math> as being an ordered pair <math>(X, X^\uparrow),</math> with <math>2^n\!</math> points in the underlying space <math>X\!</math> and <math>2^{2^n}</math> propositions in the function space <math>X^\uparrow.</math>
Thus, we may speak of the universe of discourse <math>X^\Box</math> as being an ordered pair <math>(X, X^\uparrow),</math> with <math>2^n\!</math> points in the underlying space <math>X\!</math> and <math>2^{2^n}</math> propositions in the function space <math>X^\uparrow.</math>
A more complete discussion of these notations can be found here:
A more complete discussion of these notations can be found here:
:* [[Directory:Jon_Awbrey/Papers/Differential_Logic_and_Dynamic_Systems_2.0#A_Functional_Conception_of_Propositional_Calculus|A Functional Conception of Propositional Calculus]]
:* [Differential Logic and Dynamic Systems 2.0#A Functional Conception of Propositional Calculus|A Functional Conception of Propositional Calculus]]
Now, to the Example.
Now, to the Example.
Since <math>d^4 x\!</math> and all higher order <math>d^j x\!</math> are fixed, the entire dynamics can be plotted in the extended space <math>\operatorname{E}^3 X = \langle x, dx, d^2 x, d^3 x \rangle.</math> Thus, there is just enough room in a planar venn diagram to plot both orbits and to show how they partition the points of <math>\operatorname{E}^3 X.</math> As it turns out, there are exactly two possible orbits, of eight points each, as illustrated in Figures 16-a and 16-b. See here:
Since <math>d^4 x\!</math> and all higher order <math>d^j x\!</math> are fixed, the entire dynamics can be plotted in the extended space <math>\operatorname{E}^3 X = \langle x, dx, d^2 x, d^3 x \rangle.</math> Thus, there is just enough room in a planar venn diagram to plot both orbits and to show how they partition the points of <math>\operatorname{E}^3 X.</math> As it turns out, there are exactly two possible orbits, of eight points each, as illustrated in Figures 16-a and 16-b. See here:
:* [[Directory:Jon_Awbrey/Papers/Differential_Logic_and_Dynamic_Systems_2.0#Example_2._Drives_and_Their_Vicissitudes|Example 2. Drives and Their Vicissitudes]]
:* [[Differential Logic and Dynamic Systems 2.0#Example 2. Drives and Their Vicissitudes|Example 2. Drives and Their Vicissitudes]]
Here are the <math>4^\text{th}\!</math> gear curves over the 1-feature universe <math>X = \langle x \rangle</math> arranged in the form of tabular arrays, listing the extended state vectors <math>(x, dx, d^2 x, d^3 x, d^4 x)\!</math> as they occur in one cyclic period of each orbit.
Here are the <math>4^\text{th}\!</math> gear curves over the 1-feature universe <math>X = \langle x \rangle</math> arranged in the form of tabular arrays, listing the extended state vectors <math>(x, dx, d^2 x, d^3 x, d^4 x)\!</math> as they occur in one cyclic period of each orbit.
|}
|}
In this arrangement, the temporal ordering of states can be reckoned by a kind of ''parallel round-up rule''. Specifically, if <math>(a_k, a_{k+1})\!</math> is any pair of adjacent digits in a state vector <math>(a_0, a_1, \ldots, a_n),\!</math> then the value of <math>a_k\!</math> in the next state is <math>a_k^\prime = a_k + a_{k+1},\!</math> the addition being taken mod 2, of course.
In this arrangement, the temporal ordering of states can be reckoned by a kind of ''parallel round-up rule''. Specifically, if <math>(a_k, a_{k+1})\!</math> is any pair of adjacent digits in a state vector <math>{(a_0, a_1, \ldots, a_n)},\!</math> then the value of <math>a_k\!</math> in the next state is <math>a_k^\prime = a_k + a_{k+1},\!</math> the addition being taken mod 2, of course.
A more complete discussion of this arrangement is given here:
A more complete discussion of this arrangement is given here:
:* [[Directory:Jon_Awbrey/Papers/Differential_Logic_and_Dynamic_Systems_2.0#Example_2._Drives_and_Their_Vicissitudes|Example 2. Drives and Their Vicissitudes]]
:* [[Differential Logic and Dynamic Systems 2.0#Example 2. Drives and Their Vicissitudes|Example 2. Drives and Their Vicissitudes]]
==Example 4==
==Example 4==
Onward and upward to Flatland, the differential analysis of transformations between 2-dimensional universes of discourse.
Onward and upward to Flatland, the differential analysis of transformations between 2-dimensional universes of discourse.
Consider the transformation from the universe <math>U^\circ = [u, v]</math> to the universe <math>X^\circ = [x, y]</math> that is defined by this system of equations:
Consider the transformation from the universe <math>U^\Box = [u, v]</math> to the universe <math>X^\Box = [x, y]</math> that is defined by this system of equations:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
|+ <math>\text{Table 1. Syntax and Semantics of a Calculus for Propositional Logic}\!</math>
|+ <math>\text{Table 1. Syntax and Semantics of a Calculus for Propositional Logic}\!</math>
|- style="background:whitesmoke"
|- style="background:whitesmoke"
| <math>\text{Expression}\!</math>
| <math>\text{Expression}~\!</math>
| <math>\text{Interpretation}\!</math>
| <math>\text{Interpretation}\!</math>
| <math>\text{Other Notations}\!</math>
| <math>\text{Other Notations}\!</math>
| <math>0\!</math>
| <math>0\!</math>
|-
|-
| <math>\texttt{x}</math>
| <math>\texttt{x}\!</math>
| <math>x\!</math>
| <math>x\!</math>
| <math>x\!</math>
| <math>x\!</math>
<br>
<br>
The component notation <math>F = (F_1, F_2) = (f, g) : U^\circ \to X^\circ</math> allows us to give a name and a type to this transformation, and permits us to define it by means of the compact description that follows:
The component notation <math>F = (F_1, F_2) = (f, g) : U^\Box \to X^\Box</math> allows us to give a name and a type to this transformation, and permits us to define it by means of the compact description that follows:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
A more complete framework of discussion and a fuller development of this example can be found in the neighborhood of the following site:
A more complete framework of discussion and a fuller development of this example can be found in the neighborhood of the following site:
:* [[Directory:Jon_Awbrey/Papers/Differential_Logic_and_Dynamic_Systems_2.0#Transformations_of_Type_B2_.E2.86.92_B2|Transformations of Type '''B'''<sup>2</sup> → '''B'''<sup>2</sup>]]
:* [[Differential Logic and Dynamic Systems 2.0#Transformations of Type B2 .E2.86.92 B2|Transformations of Type '''B'''<sup>2</sup> → '''B'''<sup>2</sup>]]
Consider the "transformation of textual elements" (TOTE) in progress:
Consider the "transformation of textual elements" (TOTE) in progress:
|}
|}
Taken as a transformation from the universe <math>U^\circ = [u, v]</math> to the universe <math>X^\circ = [x, y],</math> this is a particular type of formal object, and it can be studied at that level of abstraction until the chickens come home to roost, as they say, but when the time comes to count those chickens, if you will, the terms of artifice that we use to talk about abstract objects, almost as if we actually knew what we were talking about, need to be fully fledged or fleshed out with extra "bits of interpretive data" (BOIDs).
Taken as a transformation from the universe <math>U^\Box = [u, v]</math> to the universe <math>X^\Box = [x, y],</math> this is a particular type of formal object, and it can be studied at that level of abstraction until the chickens come home to roost, as they say, but when the time comes to count those chickens, if you will, the terms of artifice that we use to talk about abstract objects, almost as if we actually knew what we were talking about, need to be fully fledged or fleshed out with extra "bits of interpretive data" (BOIDs).
And so, to decompress the story, the TOTE that we use to convey the FOMA has to be interpreted before it can be applied to anything that actually puts supper on the table, so to speak.
And so, to decompress the story, the TOTE that we use to convey the FOMA has to be interpreted before it can be applied to anything that actually puts supper on the table, so to speak.
When we consider a transformation in the alias interpretation, we are merely changing the terms that we use to describe what may very well be, to some approximation, the very same things.
When we consider a transformation in the alias interpretation, we are merely changing the terms that we use to describe what may very well be, to some approximation, the very same things.
For example, in some applications the discursive universes <math>U^\circ = [u, v]</math> and <math>X^\circ = [x, y]</math> are best understood as diverse frames, instruments, reticules, scopes, or templates, that we adopt for the sake of viewing from variant perspectives what we conceive to be roughly the same underlying objects.
For example, in some applications the discursive universes <math>U^\Box = [u, v]</math> and <math>X^\Box = [x, y]</math> are best understood as diverse frames, instruments, reticules, scopes, or templates, that we adopt for the sake of viewing from variant perspectives what we conceive to be roughly the same underlying objects.
When we consider a transformation in the alibi interpretation, we are thinking of the objective things as objectively moving around in space or changing their qualitative characteristics. There are times when we think of this alibi transformation as taking place in a dimension of time, and then there are times when time is not an object.
When we consider a transformation in the alibi interpretation, we are thinking of the objective things as objectively moving around in space or changing their qualitative characteristics. There are times when we think of this alibi transformation as taking place in a dimension of time, and then there are times when time is not an object.
For example, in some applications the discursive universes <math>U^\circ = [u, v]</math> and <math>X^\circ = [x, y]</math> are actually the same universe, and what we have is a frame where <math>x\!</math> is the next state of <math>u\!</math> and <math>y\!</math> is the next state of <math>v,\!</math> notated as <math>x = u'\!</math> and <math>y = v'.\!</math> This permits us to rewrite the transformation <math>F\!</math> as follows:
For example, in some applications the discursive universes <math>U^\Box = [u, v]</math> and <math>X^\Box = [x, y]</math> are actually the same universe, and what we have is a frame where <math>x\!</math> is the next state of <math>u\!</math> and <math>y\!</math> is the next state of <math>v,\!</math> notated as <math>x = u'\!</math> and <math>y = v'.\!</math> This permits us to rewrite the transformation <math>F\!</math> as follows:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
<math>F\!</math> is just one example among — well, now that I think of it — how many other logical transformations from the same source to the same target universe? In the light of that question, maybe it would be advisable to contemplate the character of <math>F\!</math> within the fold of its most closely akin transformations.
<math>F\!</math> is just one example among — well, now that I think of it — how many other logical transformations from the same source to the same target universe? In the light of that question, maybe it would be advisable to contemplate the character of <math>F\!</math> within the fold of its most closely akin transformations.
Given the alphabets <math>\mathcal{U} = \{ u, v \}</math> and <math>\mathcal{X} = \{ x, y \},</math> along with the corresponding universes of discourse <math>U^\circ</math> and <math>X^\circ = [\mathbb{B}^2],</math> how many logical transformations of the general form <math>G = (G_1, G_2) : U^\circ \to X^\circ</math> are there?
Given the alphabets <math>\mathcal{U} = \{ u, v \}</math> and <math>\mathcal{X} = \{ x, y \},</math> along with the corresponding universes of discourse <math>U^\Box</math> and <math>X^\Box = [\mathbb{B}^2],</math> how many logical transformations of the general form <math>G = (G_1, G_2) : U^\Box \to X^\Box</math> are there?
Since <math>G_1\!</math> and <math>G_2\!</math> can be any propositions of the type <math>\mathbb{B}^2 \to \mathbb{B},</math> there are <math>2^4 = 16\!</math> choices for each of the maps <math>G_1\!</math> and <math>G_2,\!</math> and thus there are <math>2^4 \cdot 2^4 = 2^8 = 256\!</math> different mappings altogether of the form <math>G : U^\circ \to X^\circ.</math>
Since <math>G_1\!</math> and <math>G_2\!</math> can be any propositions of the type <math>\mathbb{B}^2 \to \mathbb{B},</math> there are <math>2^4 = 16\!</math> choices for each of the maps <math>G_1\!</math> and <math>G_2,\!</math> and thus there are <math>2^4 \cdot 2^4 = 2^8 = 256\!</math> different mappings altogether of the form <math>G : U^\Box \to X^\Box.</math>
The set of all functions of a given type is customarily denoted by placing its type indicator in parentheses, in the present instance writing <math>(U^\circ \to X^\circ) = \{ G : U^\circ \to X^\circ \},</math> and so the cardinality of this ''function space'' can most conveniently be summed up by writing:
The set of all functions of a given type is customarily denoted by placing its type indicator in parentheses, in the present instance writing <math>(U^\Box \to X^\Box) = \{ G : U^\Box \to X^\Box \},</math> and so the cardinality of this ''function space'' can most conveniently be summed up by writing:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
| <math>|(U^\circ \to X^\circ)| ~=~ |(\mathbb{B}^2 \to \mathbb{B}^2)| ~=~ 4^4 ~=~ 256.</math>
| <math>|(U^\Box \to X^\Box)| ~=~ |(\mathbb{B}^2 \to \mathbb{B}^2)| ~=~ 4^4 ~=~ 256.</math>
|}
|}
Given any transformation of this type, <math>G : U^\circ \to X^\circ,</math> the (first order)
Given any transformation of this type, <math>G : U^\Box \to X^\Box,</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>\operatorname{E}U^\circ = [u, v, du, dv]</math> and <math>\operatorname{E}X^\circ = [x, y, dx, dy],</math> of <math>G \operatorname{'s}\!</math> own source and target universes.
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>\operatorname{E}U^\Box = [u, v, du, dv]</math> and <math>\operatorname{E}X^\Box = [x, y, dx, dy],</math> of <math>G \operatorname{'s}\!</math> own source and target universes.
First, the ''enlargement map'' (or the ''secant transformation'') <math>\operatorname{E}G = (\operatorname{E}G_1, \operatorname{E}G_2) : \operatorname{E}U^\circ \to \operatorname{E}X^\circ</math> is defined by the following pair of component equations:
First, the ''enlargement map'' (or the ''secant transformation'') <math>\operatorname{E}G = (\operatorname{E}G_1, \operatorname{E}G_2) : \operatorname{E}U^\Box \to \operatorname{E}X^\Box</math> is defined by the following pair of component equations:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
|}
|}
Second, the ''difference map'' (or the ''chordal transformation'') <math>\operatorname{D}G = (\operatorname{D}G_1, \operatorname{D}G_2) : \operatorname{E}U^\circ \to \operatorname{E}X^\circ</math> is defined in a component-wise fashion as the boolean sum of the initial proposition <math>G_j\!</math> and the ''enlarged'' or ''shifted'' proposition <math>\operatorname{E}G_j,</math> for <math>j = 1, 2,\!</math> in accord with following pair of equations:
Second, the ''difference map'' (or the ''chordal transformation'') <math>\operatorname{D}G = (\operatorname{D}G_1, \operatorname{D}G_2) : \operatorname{E}U^\Box \to \operatorname{E}X^\Box</math> is defined in a component-wise fashion as the boolean sum of the initial proposition <math>G_j\!</math> and the ''enlarged'' or ''shifted'' proposition <math>\operatorname{E}G_j,</math> for <math>j = 1, 2,\!</math> in accord with following pair of equations:
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
Given these general considerations about the operators <math>\operatorname{E}</math> and <math>\operatorname{D},</math> let's return to particular cases, and carry out the first order analysis of the transformation <math>F(u, v) ~=~ ( ~\texttt{((u)(v))}~ , ~\texttt{((u,~v))}~ ).</math>
Given these general considerations about the operators <math>\operatorname{E}</math> and <math>\operatorname{D},</math> let's return to particular cases, and carry out the first order analysis of the transformation <math>F(u, v) ~=~ ( ~\texttt{((u)(v))}~ , ~\texttt{((u,~v))}~ ).</math>
By way of getting our feet back on solid ground, let's crank up our current case of a transformation of discourse, <math>F : U^\circ \to X^\circ,</math> with concrete type <math>[u, v] \to [x, y]</math> or abstract type <math>\mathbb{B}^2 \to \mathbb{B}^2,</math> and let it spin through a sufficient number of turns to see how it goes, as viewed under the scope of what is probably its most straightforward view, as an elsewhen map <math>F : [u, v] \to [u', v'].</math>
By way of getting our feet back on solid ground, let's crank up our current case of a transformation of discourse, <math>F : U^\Box \to X^\Box,</math> with concrete type <math>[u, v] \to [x, y]</math> or abstract type <math>\mathbb{B}^2 \to \mathbb{B}^2,</math> and let it spin through a sufficient number of turns to see how it goes, as viewed under the scope of what is probably its most straightforward view, as an elsewhen map <math>F : [u, v] \to [u', v'].</math>
{| align="center" cellpadding="8" style="text-align:center"
{| align="center" cellpadding="8" style="text-align:center"
\\ \\
\\ \\
\operatorname{D}g & = & \texttt{((u,~v)) ~+~ (( u + du ,~ v + dv ))}
\operatorname{D}g & = & \texttt{((u,~v)) ~+~ (( u + du ,~ v + dv ))}
\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^\circ = [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>\texttt{uv}, \texttt{u(v)}, \texttt{(u)v}, \texttt{(u)(v)}</math> of the 2-dimensional universe of discourse <math>U^\Box = [u, v].\!</math>
===Computation Summary : <math>f(u, v) = \texttt{((u)(v))}</math>===
===Computation Summary : <math>f(u, v) = \texttt{((u)(v))}</math>===
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
| <math>\texttt{uv~(du,~dv) ~+~ u(v)~(du,~dv) ~+~ (u)v~(du,~dv) ~+~ (u)(v)~(du,~dv)}</math>
| <math>\texttt{uv~(du,~dv) ~+~ u(v)~(du,~dv) ~+~ (u)v~(du,~dv) ~+~ (u)(v)~(du,~dv)}\!</math>
|}
|}
\\ \\
\\ \\
\operatorname{D}g & = & \texttt{((u,~v)) ~+~ (( u + du ,~ v + dv ))}
\operatorname{D}g & = & \texttt{((u,~v)) ~+~ (( u + du ,~ v + dv ))}
\end{array}</math>
\end{array}\!</math>
|}
|}
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^\circ = [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>\operatorname{d}U^\Box = [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^\circ = [u, v]\!</math> and selecting at each cell the linear proposition in <math>\operatorname{d}U^\circ = [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^\Box = [u, v]\!</math> and selecting at each cell the linear proposition in <math>\operatorname{d}U^\Box = [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>
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
</pre>
</pre>
Figure 2.4 illustrates one way of ranging over the cells of the underlying universe <math>U^\circ = [u, v]\!</math> and selecting at each cell the linear proposition in <math>\operatorname{d}U^\circ = [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^\Box = [u, v]\!</math> and selecting at each cell the linear proposition in <math>\operatorname{d}U^\Box = [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>
{| align="center" cellpadding="8" width="90%"
{| align="center" cellpadding="8" width="90%"
'''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:
; Jon Awbrey, "[[Directory:Jon_Awbrey/Papers/Differential_Logic_and_Dynamic_Systems_2.0|Differential Logic and Dynamic Systems]]"
; [[Differential Logic and Dynamic Systems 2.0|Differential Logic and Dynamic Systems]]
: [[Directory:Jon_Awbrey/Papers/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]]
: [[Directory:Jon_Awbrey/Papers/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:
==Visualization==
==Visualization==
In my work on "[[Directory:Jon_Awbrey/Papers/Differential_Logic_and_Dynamic_Systems_2.0|Differential Logic and Dynamic Systems]]", I found it useful to develop several different ways of visualizing logical transformations, indeed, I devised four distinct styles of picture for the job. Thus far in our work on the mapping <math>F : [u, v] \to [u, v],\!</math> we've been making use of what I call the ''areal view'' of the extended universe of discourse, <math>[u, v, du, dv],\!</math> but as the number of dimensions climbs beyond four, it's time to bid this genre adieu, and look for a style that can scale a little better. At any rate, before we proceed any further, let's first assemble the information that we have gathered about <math>F\!</math> from several different angles, and see if it can be fitted into a coherent picture of the transformation <math>F : (u, v) \mapsto ( ~\texttt{((u)(v))}~, ~\texttt{((u, v))}~ ).</math>
In my work on [[Differential Logic and Dynamic Systems 2.0|Differential Logic and Dynamic Systems]], I found it useful to develop several different ways of visualizing logical transformations, indeed, I devised four distinct styles of picture for the job. Thus far in our work on the mapping <math>F : [u, v] \to [u, v],\!</math> we've been making use of what I call the ''areal view'' of the extended universe of discourse, <math>[u, v, du, dv],\!</math> but as the number of dimensions climbs beyond four, it's time to bid this genre adieu, and look for a style that can scale a little better. At any rate, before we proceed any further, let's first assemble the information that we have gathered about <math>F\!</math> from several different angles, and see if it can be fitted into a coherent picture of the transformation <math>F : (u, v) \mapsto ( ~\texttt{((u)(v))}~, ~\texttt{((u, v))}~ ).</math>
In our first crack at the transformation <math>F,\!</math> we simply plotted the state transitions and applied the utterly stock technique of calculating the finite differences.
In our first crack at the transformation <math>F,\!</math> we simply plotted the state transitions and applied the utterly stock technique of calculating the finite differences.
==Turing Machine Example==
==Turing Machine Example==
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>\operatorname{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>\operatorname{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>
===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>\operatorname{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>\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 cactus syntax, an expression of the form <math>\texttt{((} e_1 \texttt{),(} e_2 \texttt{),(} \ldots \texttt{),(} e_k \texttt{))}</math> expresses a statement to the effect that ''exactly one of the expressions <math>e_j\!</math> is true, for <math>j = 1 ~\mathit{to}~ k.</math>'' Expressions of this form are called ''universal partition'' expressions, and the corresponding ''painted and rooted cactus'' (PARC) has the following shape:
In cactus syntax, an expression of the form <math>\texttt{((} e_1 \texttt{),(} e_2 \texttt{),(} \ldots \texttt{),(} e_k \texttt{))}\!</math> expresses a statement to the effect that ''exactly one of the expressions <math>e_j\!</math> is true, for <math>j = 1 ~\mathit{to}~ k.</math>'' Expressions of this form are called ''universal partition'' expressions, and the corresponding ''painted and rooted cactus'' (PARC) has the following shape:
<br>
<br>
<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>\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>
|}
|}
This means that the propositional program itself is nothing but a single proposition or boolean function of the form <math>p : \mathbb{B}^{57} \to \mathbb{B}.</math>
This means that the propositional program itself is nothing but a single proposition or boolean function of the form <math>p : \mathbb{B}^{57} \to \mathbb{B}.</math>
An assignment of boolean values to the above set of boolean variables is called an ''interpretation'' of the proposition <math>p,\!</math> and any interpretation of <math>p\!</math> that makes the proposition <math>p : \mathbb{B}^{57} \to \mathbb{B}</math> evaluate to <math>1\!</math> is referred to as a ''satisfying interpretation'' of the proposition <math>p.\!</math> Another way to specify interpretations, instead of giving them as bit vectors in <math>\mathbb{B}^{57}</math> and trying to remember some arbitrary ordering of variables, is to give them in the form of ''singular propositions'', that is, a conjunction of the form <math>e_1 \cdot \ldots \cdot e_{57}</math> where each <math>e_j\!</math> is either <math>v_j\!</math> or <math>\texttt{(} v_j \texttt{)},</math> that is, either the assertion or the negation of the boolean variable <math>v_j,\!</math> as <math>j\!</math> runs from 1 to 57. Even more briefly, the same information can be communicated simply by giving the conjunction of the asserted variables, with the understanding that each of the others is negated.
An assignment of boolean values to the above set of boolean variables is called an ''interpretation'' of the proposition <math>p,\!</math> and any interpretation of <math>p\!</math> that makes the proposition <math>p : \mathbb{B}^{57} \to \mathbb{B}</math> evaluate to <math>1\!</math> is referred to as a ''satisfying interpretation'' of the proposition <math>p.\!</math> Another way to specify interpretations, instead of giving them as bit vectors in <math>\mathbb{B}^{57}</math> and trying to remember some arbitrary ordering of variables, is to give them in the form of ''singular propositions'', that is, a conjunction of the form <math>e_1 \cdot \ldots \cdot e_{57}</math> where each <math>e_j\!</math> is either <math>v_j\!</math> or <math>\texttt{(} v_j \texttt{)},</math> that is, either the assertion or the negation of the boolean variable <math>{v_j},\!</math> as <math>j\!</math> runs from 1 to 57. Even more briefly, the same information can be communicated simply by giving the conjunction of the asserted variables, with the understanding that each of the others is negated.
A satisfying interpretation of the proposition <math>p\!</math> supplies us with all the information of a complete execution history for the corresponding program, and so all we have to do in order to get the output of the program <math>p\!</math> is to read off the proper part of the data from the expression of this interpretation.
A satisfying interpretation of the proposition <math>p\!</math> supplies us with all the information of a complete execution history for the corresponding program, and so all we have to do in order to get the output of the program <math>p\!</math> is to read off the proper part of the data from the expression of this interpretation.
