[Inquiry] Re: Dynamics And Logic

[Jon Awbrey]

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

DAL.  Note 26

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

If we follow the classical line that singles out linear functions
as ideals of simplicity, then we may complete the analytic series
of the proposition f = pq : X -> B in the following way.

Figure 26-1 shows the differential proposition df = d[pq] : EX -> B
that we get by extracting the cell-wise linear approximation to the
difference map Df = D[pq] : EX -> B.  This is the logical analogue
of what would ordinarily be called 'the' differential of pq, but
since I've been attaching the adjective "differential" to just
about everything in sight, the distinction tends to be lost.
For the time being, I'll resort to using the alternative
name "tangent map" for df.

o---------------------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` X ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `o-------------------o` `o-------------------o` ` ` ` ` ` |
| ` ` ` ` ` / ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` \ ` ` ` ` ` |
| ` ` ` ` `/` P ` ` ` ` ` ` ` ` ` `o` ` ` ` ` ` ` ` ` ` Q `\` ` ` ` ` |
| ` ` ` ` / ` ` ` ` ` ` ` ` ` ` ` /`\ ` ` ` ` ` ` ` ` ` ` ` \ ` ` ` ` |
| ` ` ` `/` ` ` ` ` ` ` ` ` ` ` `/```\` ` ` ` ` ` ` ` ` ` ` `\` ` ` ` |
| ` ` ` / ` ` ` ` ` ` ` ` ` ` ` /`````\ ` ` ` ` ` ` ` ` ` ` ` \ ` ` ` |
| ` ` `/` ` ` ` ` ` ` ` ` ` ` `/```o```\` ` ` ` ` ` `` ` ` ` ` \` ` ` |
| ` ` / ` ` ` ` ` ` ` ` ` ` ` /```^`^```\ ` ` ` ` ` ` ` ` ` ` ` \ ` ` |
| ` `o` ` ` ` ` ` ` ` ` ` ` `o```/```\```o` ` ` ` ` ` ` ` ` ` ` `o` ` |
| ` `|` ` ` ` ` ` ` ` ` ` ` `|``/`````\``|` ` ` ` ` ` ` ` ` ` ` `|` ` |
| ` `|` ` ` ` ` ` ` ` ` ` ` `|`/```````\`|` ` ` ` ` ` ` ` ` ` ` `|` ` |
| ` `|` ` ` ` ` ` ` ` ` ` ` `|/`````````\|` ` ` ` ` ` ` ` ` ` ` `|` ` |
| ` `|` ` ` ` ` ` ` ` ` `(dp)/`dq`````dp`\(dq)` ` ` ` ` ` ` ` ` `|` ` |
| ` `|` ` ` ` ` ` ` ` ` ` ` /|```````````|\ ` ` ` ` ` ` ` ` ` ` `|` ` |
| ` `|` ` ` ` ` ` ` ` ` ` `/`|```````````|`\` ` ` ` ` ` ` ` ` ` `|` ` |
| ` `|` ` ` ` ` ` ` ` ` ` / `|```````````|` \ ` ` ` ` ` ` ` ` ` `|` ` |
| ` `o` ` ` ` ` ` ` ` ` `/` `o```````````o` `\` ` ` ` ` ` ` ` ` `o` ` |
| ` ` \ ` ` ` ` ` ` ` ` v ` ` \``dp dq``/ ` ` v ` ` ` ` ` ` ` ` / ` ` |
| ` ` `\` ` ` ` ` ` ` `o<--------------------->o` ` ` ` ` ` ` `/` ` ` |
| ` ` ` \ ` ` ` ` ` ` ` ` ` ` ` \`````/ ` ` ` ` ` ` ` ` ` ` ` / ` ` ` |
| ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `\```/` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` |
| ` ` ` ` \ ` ` ` ` ` ` ` ` ` ` ` \`/ ` ` ` ` ` ` ` ` ` ` ` / ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `o` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` |
| ` ` ` ` ` \ ` ` ` ` ` ` ` ` ` ` / \ ` ` ` ` ` ` ` ` ` ` / ` ` ` ` ` |
| ` ` ` ` ` `o-------------------o` `o-------------------o` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o---------------------------------------------------------------------o
Figure 26-1.  Differential or Tangent d[pq] : EX -> B

Just to be clear about what's being indicated here,
it's a visual way of specifying the following data:

   d[pq]

   =

   p q . (dp, dq)

   +

   p (q) . dq

   +

   (p) q . dp

   +

   (p)(q) . 0

To understand the extended interpretations, that is,
the conjunctions of basic and differential features
that are being indicated here, it may help to note
the following equivalences:

   (dp, dq)  =   dp + dq   =   dp(dq) + (dp)dq

      dp     =   dp dq  +  dp(dq)

      dq     =   dp dq  +  (dp)dq

Capping the series that analyzes the proposition pq
in terms of succeeding orders of linear propositions,
Figure 26-2 shows the remainder map r[pq] : EX -> B,
that happens to be linear in pairs of variables.

o---------------------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` X ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `o-------------------o` `o-------------------o` ` ` ` ` ` |
| ` ` ` ` ` / ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` \ ` ` ` ` ` |
| ` ` ` ` `/` P ` ` ` ` ` ` ` ` ` `o` ` ` ` ` ` ` ` ` ` Q `\` ` ` ` ` |
| ` ` ` ` / ` ` ` ` ` ` ` ` ` ` ` /`\ ` ` ` ` ` ` ` ` ` ` ` \ ` ` ` ` |
| ` ` ` `/` ` ` ` ` ` ` ` ` ` ` `/```\` ` ` ` ` ` ` ` ` ` ` `\` ` ` ` |
| ` ` ` / ` ` ` ` ` ` ` ` ` ` ` /`````\ ` ` ` ` ` ` ` ` ` ` ` \ ` ` ` |
| ` ` `/` ` ` ` ` ` ` ` ` ` ` `/```````\` ` ` ` ` ` `` ` ` ` ` \` ` ` |
| ` ` / ` ` ` ` ` ` ` ` ` ` ` /`````````\ ` ` ` ` ` ` ` ` ` ` ` \ ` ` |
| ` `o` ` ` ` ` ` ` ` ` ` ` `o```````````o` ` ` ` ` ` ` ` ` ` ` `o` ` |
| ` `|` ` ` ` ` ` ` ` ` ` ` `|```````````|` ` ` ` ` ` ` ` ` ` ` `|` ` |
| ` `|` ` ` ` ` ` ` ` ` ` ` `|```````````|` ` ` ` ` ` ` ` ` ` ` `|` ` |
| ` `|` ` ` ` ` ` ` ` ` ` ` `|```dp dq```|` ` ` ` ` ` ` ` ` ` ` `|` ` |
| ` `|` ` ` ` ` ` o<------------------------------->o ` ` ` ` ` `|` ` |
| ` `|` ` ` ` ` ` ` ` ` ` ` `|```````````|` ` ` ` ` ` ` ` ` ` ` `|` ` |
| ` `|` ` ` ` ` ` ` ` ` ` ` `|```````````|` ` ` ` ` ` ` ` ` ` ` `|` ` |
| ` `|` ` ` ` ` ` ` ` ` ` ` `|`````o`````|` ` ` ` ` ` ` ` ` ` ` `|` ` |
| ` `o` ` ` ` ` ` ` ` ` ` ` `o`````^`````o` ` ` ` ` ` ` ` ` ` ` `o` ` |
| ` ` \ ` ` ` ` ` ` ` ` ` ` ` \````|````/ ` ` ` ` ` ` ` ` ` ` ` / ` ` |
| ` ` `\` ` ` ` ` ` ` ` ` ` ` `\```|```/` ` ` ` ` ` ` ` ` ` ` `/` ` ` |
| ` ` ` \ ` ` ` ` ` ` ` ` ` ` ` \``|``/ ` ` ` ` ` ` ` ` ` ` ` / ` ` ` |
| ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `\`|`/` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` |
| ` ` ` ` \ ` ` ` ` ` ` ` ` ` ` ` \|/ ` ` ` ` ` ` ` ` ` ` ` / ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` dp | dq ` ` ` ` ` ` ` ` ` `/` ` ` ` ` |
| ` ` ` ` ` \ ` ` ` ` ` ` ` ` ` ` /|\ ` ` ` ` ` ` ` ` ` ` / ` ` ` ` ` |
| ` ` ` ` ` `o-------------------o | o-------------------o` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `v` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `o` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o---------------------------------------------------------------------o
Figure 26-2.  Remainder r[pq] : EX -> B

Reading the arrows off the map produces the following data:

    r[pq]

    =

    p q . dp dq

    +

    p (q) . dp dq

    +

    (p) q . dp dq

    +

    (p)(q) . dp dq

In short, r[pq] is a constant field,
having the value dp dq at each cell.

A more detailed presentation of Differential Logic can be found here:

DLOG D.  http://stderr.org/pipermail/inquiry/2003-May/thread.html#478
DLOG D.  http://stderr.org/pipermail/inquiry/2003-June/thread.html#553
DLOG D.  http://stderr.org/pipermail/inquiry/2003-June/thread.html#571

Jon Awbrey

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
inquiry e-lab: http://stderr.org/pipermail/inquiry/
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o