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 for the state of the program during operation. The program is expressed by a formula for . 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.
Notice that we have written and world on the right sides of the two equations rather than and world(t), which might have been expected. This allows us to let 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 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 , and .