Approach for implementing TUNES
RE01 Rice Brian T. EM2
Sat, 1 May 1999 22:58:24 -0700
> And ... by the way, Brian, I've almost finished reading your arrow draft.
> I still don't understand exactly how you are going to use arrows to
> represent information, but I'm trying. Also, aren't you going to need an
> inference system (that draws arrows that are "logical consequences" of
> existing ones, in an attempt to find useful conclusions that the system
> can act on) to make the whole thing work?
representing information: arrows basically form shapes of information. it
says in the paper that they represent ordered pairs of references that are
available for reference. that makes them similar to Lisp's list construct.
the presence of an arrow represents either the choice of an ordered pair of
references or a derived truth value over an ordered pair of atoms, relative
to a given context.
arrows aren't just truth values. however, they can be used to _model_ a
logic system, and the virtual machine that processes them, programmed by
various protocols, can be modeled and implemented. i'm not sure what you're
trying to infer (perhaps that i must implement the arrow system on top of
yours or not at all... :), but i've already outlined a notion of the lambda
calculus and a conceptual framework for the system both in the paper and the
discussion thread. btw, the Curry-Howard-deBruyn Isomorphism relates
functions and types to proof structures relatively easily, and i am already
too familiar with this issue.