Procedures in CLIP (was: Joy, Lambdas, ...)

[iepos@tunes.org]

> > But, what action does "Square a number" express? 
> > What would the system do if you told it, "Square a number".
> 
> Square a number, hopefully.  Possibly by multiplying it by itself, although
> I didn't specify that.  What would you expect it to do?
> 
> Hmm, if you really wish to be literal, I would expect it to take a
> representation of a number as input, and produce a representation of the
> square of that number as output.
> 
> I'm not sure what blocks you from understanding the need for that, but
> perhaps it'll help if I use a more complicated example: "Compute the DES
> encryption of a 8-byte quantity."  The two procedures express the same basic
> idea.

Ahh... This example did help. Thanks. Such a program could be
represented in my system... Reverting back to the simpler example of
squaring, a program to compute the square of 129 could be written as
something like:

  put (stringify (square 129))

This seems to me like a natural way to express the procedure,
since what you really want the system to do is print onto the
screen a string representing (in some normal form that the user
can understand) the square of 129. If you told the system just,

  square 129

it would respond with an error, complaining that this was not a
procedure and that it could not execute it.

Anyway, once you told the system to "put (stringify (square 129))",
the thing it would set work to do is to get "stringify (square 129)"
into a form that it can understand well enough to actually output
the string. It would probably then discover that this could
be achieved if it could get "square 129" into a normal enough form.

Actually, "stringify" is sort of an odd primitive that I have not
really thought much about... As I've used it in my example,
one might hope that when applied to the square of 129, it
would yield the 5-character string "16641". Surely such a
"stringify" cannot be too fundamental though, if it has such a special
connection with base-10 number representations.

Probably, in a real system, I would not use a "stringify" quite
like this. An alternative would be to use a procedure instead,
a procedure that takes a thing as a parameter and results in
a string representation of that thing; the system would probably
pick a representation that it thought the user would like...
I'm not really sure how this might work...

> > A function, as I use the word, is just an abstract mapping from
> > keys to values... not a step of a process...
> 
> "Mapping" is a form of a verb, "to map".  In other words, a mapping may be
> used as part of a procedure to map one thing to another.  A mapping is a
> noun; a procedure is (essentially) a verb.

Hmm... certainly functions could be used to construct procedures...
Actually, every function has an associated procedure, a procedure
which takes a single parameter, has no effect, but then results
in the function of that parameter (procedures like these, that have no
effect, in general I will call "pure procedures"). There is
a precise connection between functions and their associated
procedures; however, functions would be distinct from their associated
procedures in my system ...

There is probably a little bit of confusion now associated with the
word "procedure", since I have used it in several distinct ways...
I originally used "procedure" to refer only to specific
things-to-do. A specific thing-to-do I will now call a "command"
(this use of "command" is similar to what I called "procedure completions")
while a "procedure" I will use to refer to things that are
like commands, except that they take parameters and yield results.

> > > Let me try to write a brief program:
> 
> > > &
> > >   !  @exec @Output @stringify @@+ 4 5
> > >      stop
> 
> > This is not correct. "&", "!", and "exec" are all strange things that
> > you do not need. Also, "stop" is not needed in this example. If I
> > understand what you want the program to do, it should be written:
> 
> >   @Output @stringify @@+ 4 5
> 
> > This is a procedure that outputs the string "9". There is no need
> > to wrap it with "exec" or "&". When you type in an expression
> > representing a procedure, the interpreter will probably respond
> > by executing the procedure, and then giving you another prompt.
> 
> In other words, the interpreter implicitly prepends the "&" operator when
> appropriate.  There will be times when you will need to prepend it yourself.
> (I don't care what the operator looks like, I'm just using a handy key.)

Well, I guess you could think of it that way if you want, although
my current implementation does not prepend anything like an "&" operator
to expressions.

> This is different from what would happen if the user typed "@@+ 4 5"; in
> that case, I would expect the interpreter to cleverly realize that the user
> probably wanted the system to perform the map thus indicated (even though
> it's not a procedure and thus has no meaning in terms of being performed).

If a user typed in "@@+ 4 5", the system would give an error
because it does not denote a procedure... one might suggest extending
the system a sort of sugar so that the system would just write
the normal form of the user's input if it was not a procedure;
but, I would not like the system this way, as it would probably
make programming more error-prone; I would not mind leaving
explicit the instruction to output.

> The problem is that I'm trying to think of your system as being
> consistent and simple, when it's actually not.  It's got a very complex
> interpreter, which tries its best to "do what you mean".  The thing is, this
> actually makes sense for your language, since your language isn't about
> _doing_ things; it's natural that your interpreter has to be smart in order
> to _do_ things using it.

This is exactly correct.

> Okay.  Sorry for the visible thinking process.  I think I understand the
> reason for this; I'm missing one little thing, though, so I'm going to try
> repeating what you said.
> 
> "@Input someFunction" means to get some input, apply someFunction to it
> (resulting in a procedure completion), and then execute the resulting
> procedure completion, right?  

Yeah... that's right. The expression "@Input someFunction" denotes
the command ("procedure completion") of getting an input and then going
on to do the command "someFunction foo", where "foo" is the input that
was gotten.

> So in a sense @Input is a REALLY special
> function, more like a combinator, right?

Yeah... "Input" is a fairly special function. I wouldn't consider
it nearly as SPECIAL as some combinators like I, B, C, S, and K though :-)

> Okay, so at this point it's pretty clear that "someFunction" has to be
> _executed_ at runtime; unlike the other functions we've been using, it's
> _forced_ to act like a procedure.  

And who is the one to apply the FORCE? I do not see the problem
that apparently you see. Note that it is not "someFunction" itself
that is executed (it would not make sense to execute a function).
Rather it is the application of "someFunction" to the "foo" input;
this application is supposed to be a command ("procedure completion");
if "someFunction" turns out not to be a function from strings
to commands, then the system would never have began executing
"@Input someFunction" in the first place, and would have complained
that it was jibberish (actually, this is not true of my current system,
which would not complain until after it had read the input and tried
to execute "someFunction foo", but some future revision of my system
should work this way).

> I don't like this: I think that your
> model of input and output needs to be refined.  It just doesn't seem to work
> with the rest of your ideas.  Perhaps one of the other applicative languages
> might provide a useful theory?

8-(

Really I see no problem with this model of Output and Input...
Actually, I have not even implemented Output and Input in my system.
All I have is a raw "putc" and "keyhook". But from these I was
planning on implementing an Output and Input at some point.

> Oh, and one more question.  Suppose I wanted to input a number and print the
> number which is five more than it.  Let @Input handle numbers only (so that
> we don't have to worry about errors).
> 
> @Input @Output @+ 5
> 
> Is that right? 

No, unfortunately, this would be jibberish to my system.
Perhaps it would help clarify things if I state the "types"
of some my primitives:

5     : Number
+     : Number -> (Number -> Number)
Output: String -> (Command -> Command)
Input : (String -> Command) -> Command

For example, the function "+" takes a Number and yields another
function, an adding function, which is a function from a Number
to a Number. You could of course also think of it as a function
that takes two Numbers through currying and yields a Number.

Now, for the Output... This function is only meaningful
when applied to a string. Your expression includes "@Output @+ 5",
an application of Output to a function; this is not meaningful.
Also, it seems that you are trying to apply "add-5" to a string;
the Output and Input procedures as I originally thought of them
were simply procedures that outputted and inputted strings...
If you were going to take a result of Input and add a number
to it, you would first have to decode the inputted string using
a primitive which I'll call "meaningof" (which is sort of the inverse
of "stringify"); then once you had your result as a number,
you would have to "stringify" it before outputting it...

However, for the purpose of this example, we can modify
Input and Output so that they input and output things in general,
rather than strings (they have "meaningof" and "stringify" built
into them, so to speak). Their new types would be

Output: Thing -> (Command -> Command)
Input : (Thing -> Command) -> Command

Now, using this Input and Output, the program you wanted could
be constructed as:

  Input (C (Output . +5) stop)

Recall an example from an earlier post, which just inputted
something and outputted it back:

  Input (C Output stop)

The new program which adds 5 first is the same as this, except that
"Output" is composed with "+5" (the add-5 function). In that "@"
syntax that program could be written:

  @Input @@C @@B Output @+ 5 stop

Once an input "foo" is gotten, the system goes on to execute

  C (Output . +5) stop foo

which reduces to

  (Output . +5) foo stop

and thus

  Output (+5 foo) stop

> If Joy were subject to the same restrictions, the program would look like
> this:
> 
> [5 + Output] Input.
> 
> Do I get it?

Yes, I think this is right, although this would be a weird thing to
do in Joy, of course... One would probably really use

  Input 5 + Output

> Another possible example would be
> 
> [5 swap / Output] Input.

I'm not sure what is meant by "/" here...

> >   @Input @@C Output z
> 
> Hmm.  Yes, I think I see this.  And then if we write the result of Input as
> "Input", we get:
> 
> @Output "Input" z
> 
> Thanks to the 'swap' action of @@C.  Right?

Correct.

> > I'm guessing this may still seem a bit foggy, as it is not
> > entirely familiar even to me, who has made up this system.
> 
> Good call.  
> 
> > Now for another example... Now suppose we have more general
> > primitives "Rinse", "Scrub", and "Dry", which are functions
> > (taking a piece of dishware or something) that yield procedures;
> > these procedures would be kind of like the "Output" mentioned
> > earlier, which is also a function that yields a procedure.
> > Now, with these three primitives, we want to form a function
> > that takes a piece of dishware and yields a procedure that does
> > all three things to it; using a lambda, we could express this
> > procedure as
> 
> Note that lambda actually does a poor job of modelling this action; the
> problem is that lambda notation implies that the object being named remains
> constant within a given lexical scope, and an object which is at one moment
> 'wet' and at the next 'dry' is not constant.

Uh oh... I can see that using a physical example was a bad idea.
I had thought of Rinse, Scrub, and Dry as simple procedures with
no results. I had thought of the "piece of dishware" as the
abstract "identity" of the dish, not the state or the physical
structure of the dish, which changes over time. Another example
may help clarify this; consider this command here written in English:

  Send Bill the letter.
  Then, wait until Bill sends back a response.
  Then, throw the response in the trash.

Does it seem unnatural that the command makes several references
to "Bill"; would it have been clearer if the author had written
"the new Bill" in the second occurence to make clear that
Bill may no longer be the same? It seems to me that it would
not make it clearer; the two references to "Bill" refer to
the same person... My multiple references to a piece of dishware
are similar to the multiple references to Bill in this silly command.

> Hmm.  I can't figure out how to have a function take a parameter which is
> returned by another function, and then return something which is used by yet
> another function.

It sounds like you have three functions, and want to yield their
composite. If your three functions are called "f", "g", and "h",
then the composite could be called either "B f (B g h)" or 
"B (B f g) h", since "B" is associative; or you could just
write it as "f . g . h", using sugar...

> Okay, after a weekend of relaxation it makes a little more sense.  It's
> merely a matter of convention -- we have to choose which order the
> parameters will go in.  I choose to put the parameter list before the return
> function.
> 
> @@Rinse dish Dry

Okay... it took me a bit to figure out that you were redefining
"Rinse", "Scrub", and "Dry" for the purpose of another example...
I see now...

If I understand, you want your "Rinse" procedure to take a dish,
and then result in the new dish (the new "rinsed" dish, as if
it were distinct from the original; I guess we are now talking
about the states of the dishes, so to speak, rather than the
"abstract identity" of the dishes). The "Rinse" primitive itself
would then be a function of the type

  Dish -> (Dish -> Command) -> Command

Essentially, "Rinse" takes a Dish and a continuation that uses the
new Dish.

> Hmm, it seems to me that multiple returns would be easy to perform (or at
> least would be no harder than single returns).  Your opinion?

I'm not sure I quite understand this. By "multiple returns", are you
talking about returns of multiple parameters? 

> Finally, it's clear to me that you'd need a combinator to handle anything
> more than two levels of that.  What combinator would that be?  How would you
> Wash, Dry, then Rinse a dish using this design?

Well... if you really want to rinse the dish after you've dried it,
then you could do it this way (where "foo" is the original state of
the dish):

  Wash foo (x\ Dry x (y\ Rinse y (z\ stop)))

This program, after it has washed, dried, and rinsed the dish,
goes on just to stop, disregarding the final state of the dish.
A variation of it could be written that passed on the final state
to some other function. Now, that last program could be written
without lambdas as:

  Wash foo (x\ Dry x (y\ Rinse y (K stop)))
  Wash foo (x\ Dry x (C Rinse (K stop)))
  Wash foo (C Dry (C Rinse (K stop)))

If you wanted to abstract out the dish "foo" to be washed, you'd get:

  C Wash (C Dry (C Rinse (K stop)))

Finally, if you want to abstract out the thing to do after the
job is finished (instead of necessarily "stop"), you'd get:

  C Wash . C Dry . C Rinse . K

> > For curiosity, a program analagous to "Rinse + Scrub + Dry"
> > I think would be written in Joy as
> 
> >   dup dup Rinse Scrub Dry
> 
> Ideally, it would be written (using my design) as
> 
> Rinse Scrub Dry.

Ahh... this would be a variation that kept the final state of the dish
on the stack. A similar variation could be made of mine:

  C Wash . C Dry . C Rinse

Right now it is standing out that with my style of procedures, it is
harder to express this example. I think I may have pinpointed why
this is so; it is because my approach is fundamentally Backwards
and needs to be fixed (I'll clarify on this in a minute).

> However, using your design, your writing works; I would more commonly write
> it as
> 
> dup Rinse dup Scrub Dry;
> 
> since we only duplicate before the use.  Makes sense to me.

Yeah... it's fine with me that way too.

> Note that in my design, 'Dry' returns the dried plate, so the whole function
> returns a clean and dry plate.  Your function doesn't return anything.  My
> function can be modified to act like yours by rewriting it, intuitively
> enough, as follows:
> 
> Rinse Scrub Dry drop.

Yes... I see that, if "drop" is a synonym for "pop" (is it?).

> > Anyway, do you understand now the way of doing procedures that
> > I've described? (If you do, you might try to give me another
> > example program)...
> 
> How did I do?

You did well... it looks like we're communicating now.

> > It seems to be quite a nice, pure approach
> > that, as far as I know, has never been attempted (of course, it
> > may have been attempted and I not know).
> 
> I don't really like it very much, honestly.  

8-(

> It may be pure, but I fail to
> see any benefits this purity brings.  Joy is equally pure, but is _much_
> easier to work with procedurally, 

I suspect that my kind of system may lend itself better to textual
reasoning, the primary fault of Joy being the "opaqueness" of
the quotation construct; but, as you've said, this problem of Joy
could be remedied... But, I think I may be close to understanding the
exact relationship between my kind of system and Joy's... If the
exact relationship can be discovered, it will be easy to judge which
is superior, or if they are really just simple sugared variants of
each other.

> mainly because Joy is theoretically based
> on composition, and procedure execution has the same behavior as function
> composition.

My approach is also theoretically based on composition (although
composition does not play quite so fundamental a role as it
does in Joy).

> Whoops!  I was just checking my Python URLs for the week, and I read the
> explanation of Continuations at
> http://www.ps.uni-sb.de/~duchier/python/continuations.html; guess what?  It
> turns out that your procedures match the formal version of the theory of
> continuations.  Cool.  I've used continuations before, but I haven't seen
> them explained that way.  Take a look.

This pointer was very very helpful. I also took a look at several
other pages on continuations. I had heard the term "continuation"
before somewhere but did not realize that it was identical to
the technique which I used. It is a bit of a surprise that this
technique is used in common optimizing compilers (on the other
hand, it sort of is not surprising that continuation passing is
used in optimizing compilers, considering what an amazingly Good
technique it is).

Now I'll share with you my some new (untested) enlightenment...
All this time with primitives like "Output" and "Putc" I have
been having them take the continuation as their final parameter
(after the string in the case of Output, or after the coordinates
and the character, in the case of Putc). I now realize that the
correct way is for the continuation to come First in the parameter
list (I know this sounds like a terrible, doctrinaire statement,
but bear with this and you will see that it really is Better this way).

I will now redefine what I mean by "procedure" (this is not consistent
with my prior usage, but who cares):

  a "procedure" is a function that takes a continuation parameter
  and possibly several other parameters afterwards, and yields a command
  that that does something and then goes on to do either the
  continuation, or else an application of the continuation to
  something else, or else an application of such an application
  to something else, or else ... (what we're trying to say here
  is that the continuation may be applied through currying to
  as many things as the procedure wants to apply it to, although
  the number of such things must be the same each time).

The most immediate advantage of having the continuation parameter
come first is that we can now identify the Regular Combinators
as a kind of procedure (albeit a "pure procedure", which has
no effect except to filter the parameters). I have for a while
suspected that the combinators "C", "W", and "K" were analagous
to the "swap", "dup", and "pop" of Joy respectively; I think
now I can see why this is so:

  C f x y == f y x
  W f x   == f x x
  K f x   == f

You can see that the rewrite rules for these combinators are
quite similar to the rules that Joy uses for "swap", "dup", and "pop",
except that these seem to have an extra parameter "f" at the
front that was not present in the Joy analogues; this parameter
is essentially the continuation parameter...

The "C" combinator, for instance, can be thought of as a procedure
which takes a continuation parameter "f" and then two other
parameters "x" and "y"; it goes on to do just "f y x". Essentially,
the "C" combinator, if you think of it as a procedure, takes
two parameters and has two results, the two results being the
exact same as the two parameters except that they are swapped.

There is also the "B" combinator...

  B f x y == f (x y)

As a procedure, it takes two parameters and has one result,
the application of the first parameter to the second. Although
"B" is used in many cases in my system where "dip" is used in Joy,
I do not think they are as closely related as C, W, and K are
to "swap", "dup", and "pop". Also, there is one very fascinating thing
which I just realized about the "M" combinator (which takes
a function and applies it to itself, and is constructable
as "WI" or "SII"),

  M f == f f

This combinator can be interpreted as a procedure that takes
no parameters, but which results in the "current continuation".
This could be very useful for the purposes of iteration;
I'm not really quite sure now what the exact relationship is between
this "M" though and "Y", which can also be used for iteration.
I'll have to think on this some more...

Another combinator which will play quite a special role in
my system, I suspect, is the so called "T" combinator
(constructable as "CI"):

  T x f == f x

Note that "T" is not a regular combinator, since its first parameter
is not used as a continuation... However, "T" can be used to
form procedures; specifically, "T" can be used to form a
procedure that takes no parameters and has no effect, but
which has a single result. 

For instance, "T foo" is a procedure that immediately results
in "foo"; when "T foo" is applied to a continuation "f" it
results in simply "f foo" (by T's rewrite rule). Thus,
"T" can be used to form procedures that "push a value onto the stack",
so to speak (although in a way there really is not an explicit stack).

Now, here is a simple program that we could write using this
new convention of the continuation coming first:

  T "hello" . Output

If you are used to Joy, you would probably think of this program as
a program that pushes "hello" onto the stack, and then runs Output.
But, you could also think of it more literally as a function
that takes a continuation "f" and yields

  (T "hello" . Output) f
  T "hello" (Output f)    [B]
  Output f "hello"        [T]

The thing we have then is a command that outputs "hello" and then
does the continuation "f". The original program might also have
been written as

  C Output "hello"

It is fairly well known that in "Tx . f" is the same as "C f x" in
all cases. Now, for another example, using "putc":

  T 'x . T 5 . T 4 . putc

This is a program that pushes "x", "5", and "4" onto the stack and
then runs "putc". You could more literally think of it as a function that
takes a continuation "f" and yields

  T 'x (T 5 (T 4 (putc f)))  [B]
  T 'x (T 5 (putc f 4))      [T]
  T 'x (putc f 4 5)          [T]
  putc f 4 5 'x              [T]

Note that the order of the parameters has been reversed; the
"T" combinator naturally has a reversing effect... Note that
this program written as "T 'x . T 5 . T 4 . putc" is quite
analagous to how one would write it in Joy, as:

  'x 5 4 putc

Now for another example... The program which takes an Input
and immediately outputs the result back out:

  Input . Output

Again, this is quite analagous to how one might do it in Joy...
This is a function that takes a continuation "f" and yields

  (Input . Output) f
  Input (Output f)     [B]

This is a command that gets an input, and then goes on to do
"Output f foo", where "foo" is the input that was got.
In contrast to my other example program that did the same thing,
it is now not necessary to use "C" (it was only necessary before
because the "Output" was Backwards).

Now for lists... lists are very interesting things, which might
be interesting to discuss, since they play such a fundamental
role in Joy, and since I'm trying to find the connection between
my system and Joy...

Although it would be possible to take lists as primitive in
my system, and have special constructs for "cons", "car", "cdr",
and such, there is an interesting way in which lists can
be emulated with something else. In particular, a list can
be emulated using a procedure that has no effect but which
pushes some items onto the stack (again, take my references to
the "stack" loosely). For instance, the list of the numbers
"3", "4", and "5" (in that order) could be represented as
the pure procedure

  f\ f 3 4 5

This function takes a continuation "f" and yields the application
of that continuation to "3", "4", and "5". There are ways to write
this function without using a lambda; one way is

  C (C (C I 3) 4) 5

Another way is

  T 5 . T 4 . T 3

In fact, "T" can be used to form a unit list, and composition
can be used to concatenate lists (albeit in a backwards way;
the first list comes last, and the last comes first). So,
in writing the list this way, we have wrapped each element
of the list with "T" to form unit lists and then concatenated
them all together to make the big list. You can see that this
list when given a continuation "f" gives

  (T 5 . T 4 . T 3) f
  T 5 (T 4 (T 3 f))     [B]
  T 5 (T 4 (f 3))       [T]
  T 5 (f 3 4)           [T]
  f 3 4 5               [T]

I think I can almost see a direct way now that Joy procedures can
be translated into procedures of my system. I think I'll give
it a try...

First I'll start with a simple example: the Joy program "3 2 + put",
which outputs "5". That program would be written in my system as:

  T 3 . T 2 . T + . B . B . put

You can see that this program when applied to a continuation "f" will
give:

  (T 3 . T 2 . T + . B . B . put) f
  T 3 (T 2 (T + (B (B (put f)))))     [B]
  T 3 (T 2 (B (B (put f)) +))         [T]
  T 3 (B (B (put f)) + 2)             [T]
  B (B (put f)) + 2 3                 [T]
  B (put f) (+ 2) 3                   [B]
  put f (+ 2 3)                       [B]

This is the program that puts "5" and then goes on to do "f"...
If one were really going to write this kind of program in my
system, one would probably use something like

  T (+ 2 3) . put

In the first version, the "+" operator of Joy was translated into
the "T + . B . B" of my system, since the "+" of Joy sort of has two
applications built into it. 

Here are a few words of Joy and their translations to my system:

  swap: C
  dup:  W
  pop:  K
  put:  put
  get:  get
  3:    T 3
  +:    T + . B . B

Now for the matter of quoted programs... A quoted program in Joy
is a simple program that does nothing except push a single
result onto the stack. The way I'll translate quoted programs in
my system will reflect this... A quoted program like "[3 2 + put]"
will be translated as just "T (T 3 . T 2 . T + . B . B . put)";
basically it is translated the same way as the program within
the []s, but with "T" applied to the whole thing.

Now, here are some more Joy words and their translations:

  i:      T
  dip:    CB
  concat: TB . B . B
  cons:   C . B . B

For curiousity, the Joy program "dig3" or in other words

  [[swap] dip swap] dip swap

is straightforwardly translated into my system as

  T(TC . CB . C) . CB . C

Do you see how "[swap]" has been changed to "TC", and "dip" to "CB",
etc.? You can see that it works in analogy with "dig3" by seeing
that when it is applied to a continuation "f" and four other
things, you get

  (T(TC . CB . C) . CB . C) f x y z u
  T(TC . CB . C) (CB (Cf)) x y z u      [B]
  CB (Cf) (TC . CB . C) x y z u         [T]
  B (TC . CB . C) (Cf) x y z u          [C]
  (TC . CB . C) (Cfx) y z u             [B]
  TC (CB (C (Cfx))) y z u               [B]
  CB (C (Cfx)) C y z u                  [T]
  B C (C (Cfx)) y z u                   [C]
  C (C (Cfx) y) z u                     [B]
  C (Cfx) y u z                         [C]
  Cfx u y z                             [C]
  f u x y z                             [C]

As you can see, it is a procedure that that takes four parameters
and results in those same four parameters, but with the "u"
(which was buried three deep) dug up to the top.

Isn't this weird... ?

By the way, that last "dig3" in my system I would not normally
write that way. Normally it would be written:

  C . BC . B(BC)

Also, I think I might have some trouble constructing certain
operators on lists... for instance, the "length" operator which,
given a lists, gives its size... I'm not sure how I would construct it...
It would be possible, though, if I had a "reification" primitive or such...
But, the solution I usually use is to make the first element of
a list contain its length in some cases... I'm not sure if
this is good or not, though... Another option would be to construct
lists as chains of pairs, with a terminator; this is the approach
that is usually used, I guess, but it would make the other list
operators (for instance, concatenation) much more complex.

> Start is a non-function.  That is, its only purpose is to do something, not
> to 'return' something.
>
> Right?

This is true, in that "start", as I've defined it, is a procedure
that does not give a result. But, in a literal sense, "start" is a
function, a function that takes a continuation and a task to start,
and yields a command (a continuation).

> > of itself, for instance. Also, the system might do common-sense
> > consistency checks before accepting new information at all, to make
> > sure it is not absurd; but, a full consistency check (meaning a
> > proof that the added information will not cause everything to
> > be provable) in general would not be possible, I think, according to
> > "Godel's theorem", unless the system is already blown
> > (in which case everything would be provable, including
> > that the system is consistent).
> 
> Well, you _can_ check that the new theorem doesn't contradict the axioms,
> can't you?

Well, I'm hardly a specialist on this, but if I understand correctly, 
you cannot. You could, of course, check that the new theorem isn't a
direct negation of any axiom... But, checking all the _consequences_
of the axioms, to see that none of them is an absurdity, is generally
not possible. A brute force approach will not work, because there
are an infinite number of consequences of the axioms, and you
cannot check them all. But, there are some cases where the consistency
of a system can be shown, but it is usually quite a difficult task,
and there is not a general algorithm for doing it. 

However, I think Godel's theorem only applies to a certain class of
systems (albeit quite a broad class). You could maybe get around it
if, for instance, you arbitrarily restricted your proof system
so that only formulae that could be proven within 20 steps
using the axioms were accepted as theorems. Then, a brute-force
check for consistency would in principle be possible (although
probably not practical).

Anyway, I wouldn't let this theoretical limit stop you... A partial
consistency check (that only looked ahead some certain number
of steps to see that an absurdity could not be derived) would
in most cases be acceptable, I would guess. Some inconsistencies
could slip through, but only those of quite a subtle kind...

There would probably from time to time be cases where the system
found an inconsistency... I'm not sure what would be a good thing
for it to do at that point... One possibility would be for it
to eradicate the absurd result from its memory; then, the
least trusted of the premises from which it was derived would
also be eradicated; then, if this one was derived from somewhere,
its least trusted premise would also be eradicated. This would
continue until an axiom was reached, one of the least trusted of the
axioms upon which the original absurd result was based; this
axiom would be eliminated. 

Anyway, I'm still open for ideas on how do a logic system...
I suppose there are real automated logic systems out there
(for instance, Coq or HOL) which I could learn from...

> > - "iepos" (Brent Kerby)
> 
> -Billy

- "iepos" (Brent Kerby)