arrow-structure syntax and semantics
RE01 Rice Brian T. EM2
BRice@vinson.navy.mil
Mon, 7 Dec 1998 11:57:24 +0800
> Just some corrections to my original post (which I hardly proof-read) as
> well as some more thoughts on the subject:
>
The number of elements in the linked-list proposed would be (n-1) for n
elements, not (n+1).
> Speaking of which, some ideas about operator add-ons are:
> modus ponens (inference)
> lambda (function-abstraction)
> mu (i'm still trying to find a good short description)
> pi (path)
>
I'm also thinking about a 'shallow copy' idea where a new arrow is created
with all links to the original arrow duplicated for the second arrow. This
doesn't seem very useful, though. If anyone can make anything out of it,
I'd be glad to hear the idea.
If anyone was curious, the 'multi-dimensional arrow theory' amounts to an
arrow theory where arrows are lists with n slots (vice two slots 'tail' and
'head'). There's not much work done on it yet, but it doesn't seem to have
added anything useful that couldn't be quickly gained by reflection. It
also results in some rather non-intuitive properties and complicated
operator structures that don't seem worth the hassle, although they are
interesting mathematically.
> There is also a question I stumbled on while looking at a simulation I was
> doing in my head. It seems that the possibility of an arrow pointing to a
> group of arrows is a bit confusing to the system itself unless we add
> something. The idea that I had about using LISP style linked lists (made
> of arrows, that is) to form a structure denoting a group results in some
> confusion about how that group is denoted. Maybe this will clarify:
<rambling edited for content>
> However, all of these methods seem only to be quick fixes which
> themselves will be replaced once infinitary structures come into place.
>
It just occurred to me to point to a node from which arrows point to all the
objects in the group. However, this idea also seems to suggest leaving such
a construct at the meta-level, as the linked-list idea could be. But this
idea also seems to work with the idea of using a linked-list to a
linked-list in order to encode a linked-list arrow target explicitly, so
that we now would have a node with arrows to nodes with more arrows?? (ok,
that doesn't sound like it makes sense to me either, so i'll keep working on
it) However, this idea _does_ seem to scale well to the infinitary level,
since all one would have to do is to simply state 'for every member of this
set (those arrows satisfying these conditions), such-and-such arrow points
to it (or their is an arrow from such-and-such node to that arrow)'.
Here's a declarational paradigm for arrows: to make statements, we can use
the axiomatic paradigm to explicitly encode context, and some sort of
relational structure can describe to the system that the context applies in
such-and-such structure. However, to construct contexts 'from the ground
up' seems to need some fleshing out in our minds (or at least in my mind).
We're going to take the traditional language paradigm and 'factor out'
syntax and such. Proofs, for instance, should simply consist of inference
diagrams, instead of statement sequences with annotations showing the 'line
numbers' and names of principles (theorems and axioms) used to generate the
statement in that line. Instead, a directed (I remembered to say it this
time) arrow graph could use arrows as dependency relations and nodes as
statement containers. The nodes would in turn have arrows pointing to
structures of the statements, not with symbols, but direct links to the
actual somethings (can someone find a better word?). The idea here is a
dataflow graph in a quite abstract form. Obviously, there are four distinct
arrow-structure worlds(?) here: the dependency graph, the mapping from the
nodes in that graph to the syntax(?) structures, the syntax structures
themselves, and the data-flow graph.
A useful addition to this is the explication of the operator idea using
state transition diagrams. What I mean is that the changes in the state of
the system should be describable by declarations using arrows themselves,
like stating that the inversion operator creates a new arrow with ...
(another metaphor is that all arrows created by combinations of operators
'already exist' and merely generate references at the appropriate time).
This idea itself should be reflective, so the knowledge of the system's
state should be encodable as well. All of this screams complexity, but the
coincidence of reflection should negate the resulting interface problems.