new operators... finally

[RE01 Rice Brian T. EM2]

well, i still haven't received the responses that i've been waiting for, so
i'm just going to post the ideas that i've been working on lately for the
Arrow language.

basically, i'm going to wait until a good example crops up for the
infinitary example implementation before i continue with that line of
thought.

	there are several different ways that we can use the paradigm of
arrows.  keep in mind, however, the over-riding metaphor that an arrow
expresses the applicability of the local relation to a pair of objects in
the aspect language.

	one way is to specify the domain of 'nodes' for a graph, and assume
that all arrows are available as first-order entities.  this is called the
'square' logic, for the reason that the cartesian product of pairs of nodes
forms an N by N grid of objects representing the arrows.  other ways
basically look at restricted subsets of these arrows, with the constraints
specified axiomatically for instance.  an example of the latter is an RST
(equivalence) relation over some arbitrary group of objects.  logics with
less than all of the square of relational objects amount to a mapping from
the square to {0,1}.  this is also equivalent to relational algebra (with
possible axiomatized restrictions as the case is necessary).

	the axiomatizations for many of these ideas i'm considering are
finite and regular (this is of course a good thing).  an interesting problem
is that the strong form of the associativity axiom of the combinator
operator, which results in the familiar 'vector addition' visual metaphor,
causes the logic to be undecideable.  this is the case in basic boolean
algebra and its derivatives including the relational algebra that i
mentioned.  it basically amounts to treating spaces where the combinator is
associative as special cases in order to isolate the decidable areas of the
system.

	speaking of boolean logic, i've been trying to work out the right
equivalent idea in my system of the quantifiers, i.e. 'for all' and 'there
exists'.  of course, each one is interpretable due to the other's existence,
but that's not what i'm thinking about.  what i'm trying to figure out is
that since we will be 'pushing' arrows (we'll just think of them as nodes
for now, i suppose) into the heap for the use of formulas for specifying
relationships or constraints, we need to work out where the ideas of 'free'
and 'bound' variables fit in the new paradigm.  there are no symbol
references, so the parsing isn't an issue.  we would merely have some
'arena' with symbols on one side and a syntax tree on the other, using a
directed graph to place the symbols into their containers on the other side.
but an object's 'free'ness is pretty relative, when you consider that
context includes implicit axioms, i.e. statements or restrictions that do
not have to be stated at each instantiation of usage, but are still included
in the associated reasoning system.  our system, though, will jump in and
out of contexts quite readily and transparently to the user, so that some
way to encode context would have to be integral to the reasoning system.
this is the essence of the ideas behind dynamic logic: that the binding and
freeing of atoms (including propositions) within language statements can be
done in a formalized way.

	here's an interpretation for (for all) '\-/x.P(x, ...)':  every time
we postulate a new variable in standard logic, 'for all' relates that
variable's emergence to the node flowing to the first argument of the
application of P.  '\-/x.' can be made, basically, into the statement 'x is
an object only restricted by this language implies ...' which _isn't_ a_
first_ order_ statement_.  you can't ordinarily refer to the language
_within_ that language.  so we have a meta, or somehow an aspect, statement
describing the application of the predicate to the tuple of objects.  now we
have not only predicates and objects of a language, but also applications
between them.  we would probably call the graph of applications a 'document'
or 'program' in that language.  i just want to cleanly separate this idea
from the rest of the mess.

	 i could take a cue at this point from the modula-3 language
compiler i was studying the other day, which used separate modules at the
front end to handle various semantical elements of the language.  we could,
say, use the 'kleene star' operator to encode the idea of indeterminate
loop-iteration and have it available in a variety of contexts in a similar
way.

bleh.  i recognize that i'm getting mired down in theory.  (actually, i just
feel sick due to the food that i've just eaten.)  :(

i'm just trying to factor out a lot of parts of logic and program
composition in order to simplify the development of our prototype.

let's relate this to arrows again: we want to have something do the same
thing for our arrow system as languages do for people and programmers.  we
could have a 'language language' (just joking, a meta-language, really)
where some objects are languages and others are plain nodes, with statements
like 'N is a node in language L iff ... '.

i'm sorry about the poor quality of this blather.  when i'm feeling a little
better i'll put some good stuff out, hopefully in a few hours.