An approach for implementing TUNES

[June Kerby]

This is a vague idea I've had for implementing TUNES. I'm interested to know
what you guys think about it. I'll warn you, I've never taken a class on
logic or lambda-calculus (although I've done quite a bit of studying on
the Internet), so don't be surprised if I say something really dumb or miss
something really elementary. Comments and criticism from everyone is of
course welcome.

Here's the basic idea: we set up a logic system in C, Scheme, or some other
existing language. This system would take in facts, probably in the form
of function application trees, in terms of a few constants (I'm thinking
S, K, forall, and implication) and other terms that need not be "defined"
(their properties are defined inductively in other facts). There would be
a few axioms that say how reasoning can be done (new facts derived from
old); these would probably include Modus Ponens and S and K reduction rules
(which can of course also go the other way) and a few others. New terms
can be "defined" inductively. For instance, the essence of "=" can be described
with the fact "forall \x.x=x" (or without the lambda, "forall (S(S(K(=))I)I)").
Similarly, "not" can be described by saying "forall \x.(not (not x))=x".

Actually, come to think of it, the "constants" will not be any different from
other terms, except that the axioms will involve them. There is no doubt
more than one set of axioms that would work. It doesn't really matter which
ones are chosen as long as they work and are fairly easy to understand.

Using this system, we can describe the behavior of an ibm-pc (or whatever
other machines we target), what it does when it boots up, in terms of 
undefined concepts like time, monitors, speakers, keyboards, etc. All that's
known are the relationships between them and what the machine does when it
boots up.

We would then describe what we would like the machine to do when it boots
up, in terms of those same undefined concepts. It is then up to the logic
system to determine what hard or floppy disk image is needed so that the
machine will behave the way we want it when it boots up. This is the tricky
part. This is different than lambda-calculus or pure combinatory logic, in 
which brute computation can pretty much be used to find the result. At
any time, many useless deductions can be made which will not lead to the
desired conclusion (what hard or floppy disk image to use). What we need
is a logic system that, given a set of possible relevant conclusions, will
find one (or more) efficiently (or as a bonus, prove when they have all be 
found; i.e. find the set of all relevant conclusions that can be found true
with the information it was given).

I have no idea how to do this. Does anyone else? Has anybody else already
attempted something like this, or proven that it was impossible. At the very
least, even if a system like this could not find the hard or floppy images, it
could prove that a hand-coded one is correct.

- Brent Kerby ("Iepos")