The state of the art for Arrow specs

[iepos@tunes.org]

Greetings, Brian (and other TUNES-sters)...

First, I apologize for not having been able to get your Squeak
Arrow environment to work (I've never used Squeak before; when
I try to load your file as the image (in Windoze by dragging it to the
icon for the interpreter) it gives an error like "Could not open image
file '|'")...

Anyhow, I have a few questions and comments...

> Well, I've been working through all sort of ideas for implementing basic
> Arrow functionality, and have worked out a lot of the ideas, though some
> areas remain open.  What remains is not impossible to implement, but I am
> insisting on a clean design so that the system's model of itself will be
> simple.

Sounds like a good plan...

> So, here are some of the "primitive" arrow objects:
> (1,2) "car" and "cdr" (or "head" and "tail" or whatever): these are two
> graphs which contain all off the reified references that all arrows in the
> system contain.  Note that this is a recursive definition, since arrows in
> "car" and "cdr" can have their references reified as well.  This allows
> arbitrary reification of references.

Hmm... I'm wondering how your system is overall going to work... If
I understand correctly, the system is going to use arrow structures
internally to represent information that the system "knows". Will the
network of arrows then evolve as the user feeds information to the system?
Will it expand as the system makes deductions, or contract when
the system finds information that is unsound or unimportant?

Back to "car" and "cdr"... By "graph" I suppose you mean a set of arrows;
yet from what you say it seems like each is a specific arrow itself. So,
are you modeling a set of arrows somehow using a cohesive arrow structure;
(i.e., a sort of linked list of arrows)? If so, then since "car" is a
function mapping arrows to their "tails" (i.e., the arrow their tails refer
to), I suppose each member of the "car" list (each arrow pointed to somehow
by the linked list) would be a arrow from a particular arrow to its "tail"?

If this is correct, then I see what you mean by "recursive"... since "car"
is an arrow itself, there would need to be a member of the "car" list which
mapped the "car" arrow to its tail (possibly the the first mapping in
the function (if you're using a linked list) or maybe a reference to the
next link). There would then need to be items in the "car" list for all the
other arrows involved in the list. This would only create more arrows
which would also need to be mentioned in the "car" list; so, it seems
that extending the "car" list can never make it complete in a finite
system (but I don't suppose you were really planning on having a system
finite in this way anyway, although this feature would seem to me to
be a Good Thing if it could be preserved)...

>  The axiom amounts to:
>    for each arrow X, there is an arrow in "car" whose car is X and whose cdr
>    is the arrow referred to by X's car slot, and there is an arrow in "cdr"
>    with the corresponding definition.

Okay, so you definitely are planning on using arrows as the mappings of the
functions (I'm still curious whether you're going to use a linked list for
the whole thing...). Anyhow, if this axiom holds for your system, then your
system is definitely not going to have a finite number of arrows...
correct?

> 	Note: Reifying a reference has nothing to do with obtaining the arrow
> referred to.  More on that below.
> 
> (3) Treating a graph as a function and applying it to an arrow.  This
> amounts to an "apply" graph which contains the arrow referred to by all
> arrows' cdrs.  (Visualizing this is left as an exercise for the masochist.)

Hmm... I don't quite understand that sentence. You're not really talking
about a big list of "cdrs", are you? If this is graph is like application,
I suppose it would map pairs of function and parameter to values (where
the "functions" I suppose are linked lists of mappings themselves), or
maybe to a set (linked list) of values if you mean non-deterministic functions
("relations").

>  Inverting a graph's arrows allows one to invert the function obtained.  As
> far as seems obvious, this service would be invoked by drawing arrows
> between the argument and the function, but the complete system's picture
> will probably be much more interesting.

Hmm... I'm not sure what you mean by that paragraph... 

> The axiom amounts to:
>   for each arrow X and graph G, return all arrows Y for which there is an
>   arrow in G whose car is X and whose cdr is Y.

Well... literally this seems like a command ("return all arrows Y ...")
rather than a statement (what we'd expect an axiom to be). I suppose
when you say "return all arrows Y ..." you mean "the set of all arrows 
[that meet these such-and-such conditions] is the cdr of some member of
the 'apply' graph [a member whose car is the pair of function G and
parameter X]" ... 

> 
> 	Note: In combination with the car and cdr graphs, this can be used to
> obtain the arrows referred to by a given arrow indirectly, which is what
> programming is all about.

Heh heh... won't you get bored after a while of using indirect methods to
find out what arrows point to? Seriously, I'm not sure what you mean.
I thought procedures, iteration, logic, and such were what made
programming fun... By the way, are you planning on using arrows to
represent procedures, and will the system carry out actions when told
to (i.e., informed that the some action is "expedient" or "should be done"
or something); surely the system is going to play with procedures,
isn't it?

>   Note2: If the graph as a function is multiply-defined, this could be used
> as a concurrency mechanism or as quantification over a set of values, like
> a type.  This could be highly-useful in any case.

Functions that are multiply-defined are rather silly functions (not
really functions at all in the ordinary sense). Fare seems to like them
too; I don't know what's wrong (:-)). Anyway, I don't see how quantification
is going to pop out of multiply-defined functions (relations); it seems
like you're going to need some quantifying primitive or something. 
On second thought, I suppose if you took a multiply-defined function "f" that
yields statements and said "fx" you could wind up stating something about
all of "f"s many values for "x" (this would be kind of silly
though; I'm not sure if this is what you had in mind).

> Now, obviously these tools allow us to obtain the arrows that argument
> arrows actually refer to.  However, this says nothing overtly about how to
> obtain arrows that refer to the target arrow, which means that
> meta-information is so far inaccessible.

Hmm... I'm not sure what you mean by "obtain"... It seems like you mean
indirectly-reference-using-an-application-construct. Were you planning
on having a sort of reduction rule that resolves application constructs?
Actually, it doesn't seem like you've really mentioned an application
"construct"; how do you actually apply the "apply" graph to a function
and parameter? i.e., if F is a graph and X is some arrow, is there really
a way to draw an arrow Z (referencing F and X and possibly other
special arrows) that the system will interpret as being the same as F's
value (or the set of F's values) at X?... 

... The obvious option, simply drawing an arrow from F to X, is not 
available, since the meaning of such an arrow is reserved for other things. 
In particular, in a function definition, an arrow signifies a mapping from
parameter to value; it would be nice to be able to use an application
construct inside a function definition to indirectly refer to the pair of
parameter and value, but this doesn't seem possible (unless you add another
construct besides arrows for application, which doesn't seem acceptable),
since any arrow would in fact be construed as a mapping from parameter to
value. The only other option that stands out to me (and it seems to be a
pretty good one) is to revise the model of pairing so that arrows inside
function definitions (or elsewhere) are not interpreted as pairs; actually,
every arrow could be interpreted as a function application; then, when one
really wanted to represent a pair (or linked lists, which would likely be
built from pairs) one would use a special pairing function (which could be
taken as primitive, although there are other options). Anyhow, maybe you
didn't really want an application construct anyway... (?)

> (...) Now, what remains is the system for specifying graphs, which seems to
> me to naturally be a system for taking certain graph constructs and
> modifying them incrementally using cleanly-defined arrow functions to
> produce graphs of all sorts.

Hmm... I'm curious... are you interested in graphs that are not cohesive
(i.e., ones that not entirely connected and may have "islands" of sorts)?

> 
> Also, the appropriate analogue of quantification is still missing, although
> a simple solution seems to be to predicate a graph that specifies a type,
> and infering from an arrow's membership in the graph that other statements
> apply to it, a la formal logic.  The problem there is that one runs into

Hmm. I'm not entirely sure what you mean. Anyhow, just having the ability
to say that things are of such-and-such types is hardly quantification,
although it almost is, if you have the ability to say that is a type
is universal (i.e., everything is a member), but I guess you'll also
need a construct for forming types like "the type of all 'x' that such
[some criteria]", which could probably be taken care of if you had a lambda
construct.

Anyhow, this is a question of expressiveness... I'm somewhat confused,
because it seemed like you once mentioned that Arrow was not a language;
I suppose Arrow will use a sort of language (with arrows as the syntax)
but will be more than a language itself (also a reasoning system and such).
Anyhow, it will use sort of an odd language, since it seems that there
are some common things (such as "car" or "cdr") that cannot be referred to
with a finite arrow structure (but yet they'll certainly need to be
referred to). Are you going to provide idioms for things like "car" or
"cdr"? (Some sort of closed self-referential arrow structure might do, 
I guess).

> the problems of set theory, which might be very complex for Arrow.

Heh heh... do you mean the Russell set, or sentences that reduce to their
own negation? Anyhow, such problems I think will crop up anyway even if
you don't have a set-membership construct or quantification. As long as you
have a negation and a lambda (or complete combinator base) with an appropriate
beta-reduction rule, you'll have something like "(\x.~(x x)) (\x.~(x x))"
which reduces to its own negation. Of course, this isn't really a problem ;)

> Alternatively, our "function" above could be applied to the meta-graph of
> the set, returning all the elements (in an abstract sense) and performing
> evaluations based on the properties of those arrows.

Hmm... how about returning all the elements (in a really silly sense)?
Do you mean that if you have something like the set of natural numbers
you'll have a construct that takes the set and yields "all the natural
numbers"? If this means that it yields something that is equal to all
natural numbers, then that's a bad thing, because that would mean
(by transitivity of equality) that all the natural numbers are equal
to each other also, something that hopefully wouldn't be derivable in
a system. Anyhow, that's probably not really what you meant (and I
realize this is just one of your "alternative" suggestions, not something
I'm guessing you'd defend with zeal). Still, I might be able to deal with
such a fuzzy notion of quantification, except that there are much better
approaches (for instance, as I mentioned before, a universal quantification
function "A" such that "Af" means that "f" is a universal set (everything
a member), or in other words, that "fx" holds for all "x")

> 
> I will post updates to this spec incrementally.
> 
> Comments are, of course, highly welcome.

Anyway, I'm interested in what you're working on... Hopefully none of
this has come out as criticism (in a bad sense)...

And by the way, if you have some time, you may be interested in reading my
stuff on the web at http://www.tunes.org/~iepos, particularly the section
on combinators... I haven't had any contact with anyone else interested
in approaches based on combinators, but it seems good to me; if you've
already considered these kinds of approaches, I'd be curious to know
why you don't like them as much as Arrow (although a combinator-based
approach is probably compatible with Arrow).

> 	-Brian
> 

- Brent Kerby ("Iepos")