infinitary structures

RE01 Rice Brian T. EM2 BRice@vinson.navy.mil
Fri, 18 Dec 1998 13:49:22 +0500


first, to explain the sudden paucity of my output, i should tell you that
our ship is approaching the persian gulf, so that security is being fairly
rigorously enforced on outgoing e-mail due to the political situation.

> the only results that i have so far for expressing an infinite number of
> things is rather weak: axiomatic specification.  with axiomatic
> specification, the _number_ of things referred to is irrelevant,
> theoretically.  in actuality, it of course matters a great deal if the
> axiomatization gives:
> 	0,
> 	1,
> 	a finite linearly-calculable number,
> 	an NP-hard (or NP-complete) calculable number,
> 	a countable number (as many as the natural numbers),
> 	or any of the uncountable quantities of numbers of solutions.
> 
> even this description fails to account for undecidable or undefinable
> numbers of 'solutions' to our 'equational axioms', to take an analogy.
> 
looking back at the posts which followed this one, i see now that both
stances are correct, although i would rather express it this way:  axiomatic
specification is not weak _within the arrow language_, as it is within
first-order predicate logic or other standard non-reflective logics.  my
revelation is that no types of statements should be unavailable within the
aspect-oriented reflective paradigm that i am suggesting.  this allows us to
axiomatically specify how a given set of objects should behave with each
other, while separately developing a set of logic (formerly only
meta-theory) which applies to the closure created by such a system of
statements and deals with the logic of 'computational complexity shape'.

speaking of computational shape, this sounds like a good word to use to
describe the arrow language (or any similar system that we use for tunes).
for instance, we could describe the whole arrow system as a language of
shapes (shapes of arrows, that is).  statements are made about shapes by
shapes themselves (witness the proof (inference) structures and symbol-flow
graphs). meta/ aspect information, axioms, control-flow graphs, data-flow
graphs, and symbolic logic and mathematics are all now available to us in
first-order form in the arrow language.  constructions are no longer
implicit, but explicit.  the ability to encapsulate infinitary ideas via
indirect (meta/ aspect) specification should allow the software system to
reason about the user's capabilities to draw inferences and metaphors where
the software system cannot.  the drawbacks, though, include first the
complicated interfaces which would need to be built to express the kinds of
complex relationships between the shapes in our world in a way that the user
can manipulate.  another drawback is the lack of clear boundaries on the
'definition' of an object in our system: many definitions will no doubt be
'circular' and far-reaching in their implications on the rest of the system.
perhaps the inference structures will be the main reference point for the
system's ontologies.

well, i want to construct a finite state-machine which digests the
information in arrow structures and can perform transformations on them as
specified by other arrow structures, producing new arrow-structure states.
this machine's existence will necessitate structures to be built encoding
cause-and-effect relationships and garbage collection based on some sort of
specification for 'necessary information' which describes all the data that
the system would wish to keep, and what arrows carry that information
redundantly within the system.  this garbage collector would obviously be
making trade-offs between keeping the old and recording the procedure to
make the new, and keeping the new and the same procedure for back-tracking
purposes.

also, some implicit information to encode in the c-program's implementation
of the machine model should probably record information provided by searches
through the arrow system to provide an 'arrow cache' which can be quickly
scanned for frequently-used arrows.  this could be done on a per-pane basis,
to resolve the basic difficulty in keeping track of all references to arrows
within a pane by the system.  this introduces the notion of taking arrow
'instructions' and virtualizing them, so that efficiency issues for the
computer are eased.  also, i'm looking at ways to store arrow 'panes' in
more memory-efficient ways, mostly involving incidence arrays with pointers
attached for external references or something.

also, if i use the idea of meta/ aspect specification of infinitary
structures, then the 'infinite store of arrows' idea should be pretty easy
to implement based on indirectly being able to tell the system to 'fake' the
existence of a postulated set of arrows.  i know that there's a good
metaphor for this in current programming systems, i just can't recall where
it is that i've seen it.