the Arrow language
RE01 Rice Brian T. EM2
Mon, 14 Dec 1998 20:41:10 +0600
naturally, those of you familiar with category theory will expect a similar
development of a systematized set of constructions for standard mathematical
the path that i will follow will be quite more general for the simple reason
that my intention is to avoid some pitfalls of standard ontologies. this
should become clear later.
we've got to develop some theory in arrows which subsumes standard theory of
mappings, functions, sets, attributes, methods, and information states.
for now, i'm going to link the idea of using aspect languages to encode
information with our new interface example of 'panes' (or planes) in which
arrow structures are embedded. basically, i'm looking at including axiom
systems and their relations to each other and their properties, instead of
just dealing with, say, proof structure itself.
axiom systems as i'm familiar with them usually consist of lists of
statements containing a fixed set of relational symbols as well as variables
whose existence is postulated. another way of looking at it is that we want
constraints placed on tuples of objects in our aspect languages in a way
that we can study the interaction between them via inference structures
generated and the structures' properties. this suggests that we should
develop an aspect language solely for 'classifying' inference structures and
what they tell us about the axioms we've chosen. i digress. the axiom
systems that we want will of course reference their relational/ operational
symbols (which might be infinite in number) using arrow structures, which
doesn't seem to be a problem, offhand. the statements about tuples under
those symbols' scopes could be made, as discussed before, with syntax
diagrams, in most cases quite simple. (a question seems obvious to me,
given the standard prepositional logic that we are accustomed to.) how do
we encode the idea of picking 'n' arbitrary atoms in the language, only
assuming implicit meaning? the simplest solution seems to me to
re-interpret the sentence "there exists a1 such that a1Rx and ..." into
"a1Rx implies ...". in other words, although i used a syntactical symbol
which will be quite useless in my system, the idea that i want is that the
postulation of the symbol is 'noise' in Fare's terms. it introduces new
information which induces bookkeeping overhead for the viewer (machine or
human) of the system without transmitting new information about the system.
this is one place where my 'intension vs extension' argument applies. so,
instead of postulating a symbol, we instead create a new node (implicitly, i
guess, and perhaps also virtually) and reference it with statements within
the aspect language's axiom area that constrain it in the way that we want.
these syntactic structures encoding the axiom statements could be then
mapped to the inference structure we discussed earlier.
now, theory should become practical usefulness. more later...