arrow-structure syntax and semantics

[RE01 Rice Brian T. EM2]

> > Just some corrections to my original post (which I hardly proof-read) as
> > well as some more thoughts on the subject:
> 
Okay, I know that I'm running ahead of everybody here at this point by not
waiting for responses, but I'm getting all sorts of ideas consecutively.  I
promise to answer questions as soon as you bring them up, though.

> 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.
> 
First, corrections:
	-'dependency graph' was supposed to be 'inference graph' (proof
structure)
	-'syntax structures' for now are 'syntax trees' (binary, we'll
suppose).
	-the mapping is generic, and so I don't think a new name will help
it.
	-'data-flow graph' could be better explained as 'symbol flow graph'
(or structure flow graph).  the point is that the arrow-structure in
question migrates to the location where it is used, instead of having a
representation.  maybe this concept won't work.

Now, more thoughts:
	This 'arrow worlds' idea brings up something that I'd been thinking
about earlier.  There are obviously arrows that belong to a sort of
component language, arrows that speak of the relationship between lots of
objects according to one relation (the kind from formal logic).  In the
above example, the dependency graph is an obvious abstraction of a proof
structure with the objects (nodes) being statements in the language, and
relations (arrows) being the direct dependency relation which together form
a mini-language, along with, say, logical operators like "and", "or",
"implies", and "not" or "false".  Then, you obviously have the separate
structures attached to the nodes, which linguistically have no common
relations, describing the syntax of the statement, not the statement itself.
So, that mini-language's relation is some sort of operator-application
relation, and the nodes of that graph point to the symbols used.  I could
continue with the other parts, but they seem un-interesting to the argument.
The point is that we have here arrow structures which, without annotation
from the rest of the system, have no intrinsic meaning, so that identical
graphs from both mini-languages are essentially the same structures.  What
is needed is a way of annotating these groups of arrows with information
about their semantic content.  (ASIDE.  Before you continue with this
thought process, I'm going to draw a potentially useful metaphor to unify
terminology here.  These "mini-languages", as I've been calling them, are
nothing more then abstract versions of the "aspect languages" that I was
ranting about last month.  ("Ah-Ha!!" says the croud, "He closes a loop!")
So, now I'll just call them "aspect languages".)

I'll leave you with that to chew on.

more later...