arrow-structure syntax
RE01 Rice Brian T. EM2
BRice@vinson.navy.mil
Sat, 5 Dec 1998 17:48:59 +0800
> when you know so many arrows, I expect that you know category theory,
> which is the theory of arrows par excellence.
> I was originally invented for algebraic/geometric used,
> but it has been since used to independently reconstruct type theory
> as known in typed lambda-calculi...
>
> I don't know category theory *that* well, but enough of it to know that
> * it's very powerful
> * it's mostly the same as lambda-calculus,
> only with a graphical rather than syntactical formalism.
>
> What I mean is: there are lots of things that we don't have to reinvent,
> and that we shouldn't reinvent, because it's already there.
> I certainly do not mean to lessen any one's talent.
> But I'd rather learn known things from a book, and discover new things,
> than discover known things the hard way, and have no time for new things.
>
Yes, category theory is indeed very rich, and serves quite well for a
homo-iconic system of knowledge over an almost arbitrarily large system of
domains. I also have two books on the subject (one for laymen, another for
formalists) due to the course of my research, but i found limitations in the
work of previous researchers due to sticking with implicit formalisms such
as naming conventions, finite domain sets, and (as far as i can tell) a
complete lack of the ability to reflect at knowledge level. The
arrow-structures that I am working on is my best bet on exceeding those
limitations, with the critical decision being the choice of starting point
for the system development.
Just to let you know, I have already presented to you arrow theory which is
an _extension_ of the arrow theory which has been developed over the past
decade or so, so that what I present to you is not proven, and I am aping no
one's conjectures concerning the theories with which I am dealing.
I also plan on using both the pedagogy of the laymen's book which uses
categories to rationalize all sorts of problem-solving analysis methods, as
well as the formal proofs in the other book to aid the Tunes reasoning
system development. And, yes, the obvious benefit of the graphical metaphor
has not escaped me in the least for category theory, arrow theory, dynamic
logics, and the topological issues associated with graphs.