next up previous
Next: Remarks Up: Elephant 2000: A Programming Previous: Algol 50

Elephant Programs as Sentences of Logic

This is the most tentative section of the present article. At present we have two approaches to writing Elephant programs as sentences of logic. The first approach is analogous to Algol 50. It is based on updating a state of the program and a state of the world. Of course, the functions updating the state of the world will be only partially known. Therefore, unknown functions will occur, and the knowledge we have about the world will be expressed by subjecting these functions to axioms. The second approach expresses the program and tentatively what we know about the world in terms of events. The events occur at times determined by axioms. We describe the events that we assert to occur and rely on circumscription to limit the set of occurrences to those that follow from the axioms given. We begin with the Algol 50 approach.

As with Algol 50, in our first approach we use a state vector tex2html_wrap_inline535 for the state of the program during operation. The program is expressed by a formula for tex2html_wrap_inline537 . Since the program interacts with the world, we also have a state vector world(t) of the world external to the computer. Because we can't have complete knowledge of the world, we can't expect to express world(t+1) by a single formula, but proving accomplishment specifications will involve assumptions about the functions that determine how world(t) changes.

We have





Notice that we have written tex2html_wrap_inline477 and world on the right sides of the two equations rather than tex2html_wrap_inline535 and world(t), which might have been expected. This allows us to let tex2html_wrap_inline537 and world(t+1) depend on the whole past rather than just the present. (It would also allow equations expressing dependence on the future, although such equations would be consistent only when subjected to rather strong conditions.)

We have written part of the reservation program in this form, but it isn't yet clear enough to include in the paper.

The second approach uses separate functions and predicates with time as an argument. In this respect it resembles Algol 48.


Note the use of admit with a variable ?seat. We may suppose that admit actually has a large set of arguments with default values. When an tex2html_wrap_inline571 expression is encountered, it is made obvious which arguments are being given values by the expression and which get default values. The signals for this are the name of the variable or an actual named argment as in Common Lisp. In the present case, the compiler will have to come up with a way of assigning a seat from those available.





Asserting that certain outputs occur and that certain propositions hold doesn't establish that others don't occur. Therefore, the program as given is to be supplemented by circumscribing certain predicates, namely tex2html_wrap_inline581 , tex2html_wrap_inline583 and tex2html_wrap_inline585 .

next up previous
Next: Remarks Up: Elephant 2000: A Programming Previous: Algol 50

John McCarthy
Fri Nov 6 21:37:30 PST 1998