An approach for implementing TUNES

[Brent Kerby]

> >>>>> "June" == June Kerby <magister@ns4.tecinfo.net> writes:

Oops, oh yeah, i forgot this is my mom's account, but this is from Brent
Kerby.

> I do not really understand what the system would be like. Can you give
> us an example of how you'd do "hello world", ` 2 + 2 ', or something
> simple  ?
> 
> Laurent

Well ... remember that this is only an approach at implementing TUNES. The
pure "logic" system I was talking about is not intended to be TUNES (what
I'd like TUNES to actually be might be the subject of another message). It
is only intended to be a tool for implementing TUNES. Using this tool, it
would not be able to express concepts such as numbers or greetings. It
would only be possible to state relationships about concepts, and have the
system make deductions about those relationships. For instance, if the
system knew that "forall \x.forall \y.forall \z.(x=y & y=z) -> x=z" (the
transitive property) and "A=B" and "B=C", it would be able to deduce that
"A=C", even without knowing what A, B, C, and "=" are. Another example, if
the system knew that "not true = false" and "not false = true", it could
deduce that "not (not true) = true", even without knowing what "not",
"true", and "false" really mean.  Of course, there still need to be a few
basic intuitive rules for deduction (as I mentioned before, S and K
reduction rules, along with Modus Ponens and a rule for deducing a specific
instance from a forall (is there a widely accepted name for this?) might do
.. There is probably a simpler set that I have not thought of).

Anyway, another example... if the system knew that "forall \x.forall
\y.forall \z.(x+y)+z = x+(y+z)", and that "0+1=1" and that "1+1 = 2" and
that "2+1 = 3" and that "3+1 = 4" then it could deduce that "2+2 = 4", even
without knowing what 0, 1, 2, 3, and 4 really mean. 

Similarly, this tool would be used to specify the behavior of an ibm-pc (or
any other system we will target for TUNES), in terms of low-level things
like RAM, ROM, memory, registers, i/o ports, scan codes, bits, bytes, disk
drivers cylinders, tracks, sectors, interrupts, etc., linking them with
high-level terms like storage, monitors, pixels, keyboards, bootup, and
shutdown. (again, the tool does not need to know what these things mean; it
only needs to reason with certain properties of them). 
Then, we'd specify the desired behavior of our TUNES system in terms of
those high-level things. The logic system then finds a disk image that,
when booted by the machine, gives the desired behavior. Then, we just "dd"
or "rawrite" the thing to a disk, reboot, and voila. That's the idea, at
least.

I think that both definitions (the behavior of an ibm-pc and a TUNES
system) would be quite feasible to write. However, I have almost no idea
how to implement the logic tool. Once again, I ask, does anyone else know
how? 

Anyway, I hope that cleared things up a little.

- Brent Kerby ("Iepos")