Arrow query...

[RE01 Rice Brian T. EM2]

i am sending the following to the Tunes group as well, since it may clear up
some present ambiguities:

[ongoing discussion with Alexis concerning Maude's rewrite logic reflective
capabilities and the Arrow idea.]

> True, what you have said in in the paper is valid but without proof it
> stands merely as an ideal.
> 
but if you say that your mathematical background is lacking as you say, then
i would consider you a poor judge of proof in any case, so that if i offered
you a weak proof you would mistake it for a strong one unless i noted its
weakness.

i'm thinking of using a "divide and conquer" strategy to solve this by
dividing up the paper into modular parts, addressing the ontology idea, the
arrow modelling construct, the review of homo-iconic system paradigms, and
the analysis of reflective capabilities of an arrow system all in separate
arguments.

my most major concern is that the arrow idea doesn't seem to fit into any
first-order model.  i've been trying for months to formulate the idea in a
standard formal system, with no satisfaction, although i have certainly had
success in describing every other formal system as an arrow construction.
basically, any symbolic system seems to be unfit, since there is quite a lot
of reflection going on, so that the problem isn't a "tower of
meta-regression", but instead an infinite number of directions in which a
machine could regress.  i'm trying to explore the possibilities in my Squeak
code.

> >the paper should already have explained this to you, but i see that you
> >haven't read that much into it, and that I must include more
> illustrations
> >of the strangeness of graphs in order to explain it better.
> 
> More graphs would be nice, more definitions and smaller words would be
> more
> so. The paper has already explained that you are trying to extend category
> theory, but without proofs I am talking about what is concrete, ie.
> essentially creating a computer simulation of category theory in a worst
> case scenario. Making claims for a system is fine but don't rely on them.
> 
i am sick of this category theory subject, since my arrow theory should
trivially address it.  please don't mention it again, because my system is
not about computability itself, which is what the lambda-calculus and
category theory address.  i know that currently no full implementation
exists for either categories or arrows, but could you leave that issue out
of the discussion?  it is ancillary to my primary concerns of reflective
modelling capabilities, not encapsulating lambda-theoretic formalisms.  i
don't want to have to re-emphasize that category theory is not under
discussion, and i am not interested in it since it's formal capabilities are
undisputed.

perhaps i should make clear again that the arrow system should be able to
model things in ways that are not computable, since computability as the
representation of a domain as a finite algorithm is an arbitrary modelling
process.  in my goal system, i should be able to model a computation as
incomputable or undecidable in the target domain, as well as providing the
inverse capability, that of modelling an undecidable thing as something
readily achieved by an algorithm for a more appropriate machine.  the point
is to model things that humans are capable of, for instance, but withstand
full accomplishment by machines with algorithmic hardware, and to gather
information for reasoning from such a model and its characteristics.  the
point is that although a machine may not be able to do a thing, it certainly
can provide utility by processing the intensional properties of that
procedure.  and intensional properties for a procedure which the target
machine may only model with an infinitary number of constructs requires a
formalism that can treat that infinitary construction as a first-order thing
without deadlocking, since intensionality implies a "direct link" between
source and target, which in this case is not computable.  perhaps that makes
my interest a little more clear.

> >since the arrow theory is more general than category theory, then i'd
> have
> >to say that indeed the arrow system must definitely offer semantics more
> >powerful than maude can.
> 
> Proofs excepted of course.
> 
well, if i can manage to fully explain this idea of mine, and what kind of
reflection i propose, then proofs may be trivial to derive.  i consider
explanation to be my primary task, since no mathematical proofs have ever
been given for a subject which has no expression in a standard first-order
model.  i'd like to see, for instance, a mathematical proof about the human
mind or even language, since proofs for my arrow system would be just a
little simpler.

> >what i'm trying to express is the ability to
> >manage multiple models of the sam esystem, whether it be hardware,
> software,
> >user-views of the system, or representations of those systems within the
> >spaces of new theories.  these models should be consistent within the
> limits
> >of computability.
> 
> Then you have the same goal as the maude group. I still need to look
> deeper
> at what they are doing as slightly more practically speaking, I don't know
> how GC, security, modularity etc. issues are handled, if at all. TUNES is
> more than just the fundamentals (though still reliant on).
> 
no, the maude group seems to prefer a selected set of models rather than
arbitrary representations of domains.  i am considering a system that can
interpret any system according to arbitrary ontologies, which includes
multiple interpretation methods, etc.  these methods should not have to be
declared, either.  perhaps a reflection mechanism may even be lazily
implemented or existentially (or modally) quantified.  i am looking into
these ideas right now, and results should follow soon.

> >my current direction for the prototype is to bootstrap an environment
> that
> >begins to duplicate the functions of the VM up to a minimal core set of
> >arrow-manipulation handles.  this should enhance portability and test my
> >theories of reflection.  perhaps then, the environment can be ported to a
> >very small VM, and then the real reflection may take place.
> 
> As far as I can see, you have written a paper as a specification for your
> language, and now need to program a VM (for want of a better word) to
> experiment in to find the proofs to get this thing off the ground. I'm not
> sure I can help there as mathematically speaking I'm a minnow in a big
> sea,
> be watching your code though...
> 
well, i don't consider it a formal specification, and this is my greatest
hurdle right now: it seems virtually impossible to achieve this goal.  if
you can think of a language which allows the expression of incomputability
in a first-order way (code-level constructs) and at every possible
invocation point, then please forward the information, because such a
radical design would be an immense help.  it seems however that this is far
from being the case for the next decade or so.