new operators... finally

[RE01 Rice Brian T. EM2]

ok.  i've tried to restore at least my body chemistry and flush my system by
drinking lots of water, so maybe i'll be up to giving you some good thoughts
now.

i've been studying the idea of arrow logics and multi-modal logics recently.
what i've been getting out of it is some formalization of procedure logic,
due to the multi-modal paradigm, and formalization of the logic of
transitions, due to arrow logic.  the former looks at conditionalization
(conversion of data into control-flow).  the latter, at generalized
information updates.  for the most part, we shouldn't have to look at our
system in either of those two ways to get benefits out of the system.  we've
so far figured out how to use our system to represent logical diagrams of
state-machines, inference diagrams (the union of all proofs), control and
data-flow diagrams, and data-structures themselves.  i want to get to some
examples where we build numbers and encapsulate them using the machine
model, but that is for later.  the point is that there is an aspect to
arrow-structures involving accumulating an internal state for our machine to
reason about the information a human would find intuitive about the diagrams
that the user is building.  what arrow logic does is to build a reasoning
system using atomic predicates over the objects we call arrows, and to
introduce new operators to the standard logic for arrow-composition,
reversal, and identity.  the new operators are designed to capture the idea
of graph-traversal in axiomatic form.  there are also the ideas of pairs of
conjugate operators, which amount to stating that some pair of formula-sets
corresponding to arrows with a common start/ end-point are related by the
information transition arrow which is the argument.

ok, so that didn't explain it too well.  here's a better way:

if any of you have looked at the problem-solving metaphor in category theory
of the retraction / selection maps, then you will see something quite
similar.  the point of that argument is to classify all questions into
structures of 'how do i construct a mapping which composes with my given
mapping into the total mapping that i want?', where the mapping is either
the first or second of the series.

the two cases are:
	1. i know that i want to define the relationship between two sets (A
and C), and i know that the first set (A) maps to some other set (B).  how
do i get from (B) to (C) in a way that composes correctly?  this is like
knowing how to classify some things according to one statement, then
starting from that classification, further classifying it into smaller
parts.

	2. i know how to define the relationship from two sets (A and B) to
a third set (C).  i want to find a relationship between the first two (A and
B) that composes.

these explanations are terrible, i know, so someone with some experience
with category theory please clarify this for me.

by the way, here's a couple of relations to throw into the arrow world for
speaking about arrow diagrams.  they are the incidence relations, and they
only work on directed (multi-) graphs.  yes, these are obvious:  four
relations for two arrows (2^n relations for n arrows) stating whether or not
those arrows meet at a single node in a certain configuration.  the base of
the relations are whether the 'head' or 'tail' points to the arrow,
permutated over the number of arrows at the node.  so, if three arrows touch
a single node, the first two pointing at the node and the third leading
away, then the strongest statement (3-ary) about this situation would say
'R<1,1,0> (x,y,z)'.  the aspect language for this operator would naturally
include statements for inferring (n-1)-ary statements from n-ary statements,
as well as iteration generalization to allow the construction of
higher-arity relations.  naturally, the unary relation would be so weak that
it would only say that there is a node (arrow) which the argument arrow
leads to or away from, which of course is true for any arrow in both cases
of direction.  wait!  doesn't that make it an implicit assumption?  so, part
of this aspect language is part of our universal context!  i didn't notice
that before.  what about the 0-ary relation?  i guess that it would only say
that a node (arrow) exists, obviously the weakest thing we could say, but
still also part of the universal context.  wow.  this looks like a good
start.

(it also looks as if this 0-ary relation which postulates a node / arrow
could be similar to the desired \-/ operator equivalent for us.  i'll have
to reason this out.)

let's re-define our operators in light of this class of relations R:
	combinator C:  x C y = z  IFF  R<1,1>(y,z) /\ R<0,0>(x,z) /\
R<0,1>(y,x)
	(with some implicit add-ones like:   /\ R<1,0>(x,y) /\ (unary
statements too weak to include)).
	inverse I:  I x = y  IFF  ~R<0,0>(x,y) /\ R<0,1>(x,y) /\ R<1,0>(x,y)
/\ ~R<1,1>(x,y)
	identity Id:  Id x = y  IFF  R<0,0>(x,y) /\ ~R<0,1>(x,y) /\
~R<1,0>(x,y) /\ R<1,1>(x,y)

well, those aren't very clean statements, but we should be able to make them
with the arrow system pretty easily.

so now we have an unexpected addition to our formalization of arrow context.
we should probably guide this reasoning toward iteration and the means of
building up information structures in arrows (and counting numbers) by a
machine.  we also have to remember the idea of constructing sub-contexts for
later on.