tunes-0.0.1.c

[RE01 Rice Brian T. EM2]

well, let's continue with the development of the arrow-structure system.

in order to denote an arbitrarily large population of arrows and to
distinguish them formally, the notation of using mapped integer
addressing is obviously insufficient.

there seem to be two possible routes to solving the problem.  one could
involve a 'hack' type system where the low-level representation for
arrows could be 'sugared' with special 'infinitary' copying
designations, with the problem of selecting arrows among such structures
with more mapped indices (i.e. for countable-structures, a single
integer will do, but for higher-order infinities more would be
required).  such a system seems rather limited, in that only certain
types of infinities would be denotable, and problems with denotation of
arrows might arise (although this is only my intuition as of yet).

the other route would entirely abstract the layer of 'mapped-addressing'
schemes and present a direct 'intensional' type denotation method (i.e.
like selecting the arrow desired by pointing and clicking in a graphical
system).  it is possible that within such a system, the 'sugarings'
could be interface notations only, with the program providing the
desired arrow-creation support at some lower layer.  such a system might
be made free of the natural-number limit based model and so allow more
flexibility.

naturally, the examples that i am _really_ working with are quite more
specific, but my intent here is not to give you an exact idea, but to
stimulate thought in a direction so that you could share with me your
own ideas in that direction.

i'll keep working on the logic of such a system, including using ideas
like modal logics to help with the reflection upon this property of the
system in a decidable/provable sort of way...

more later...