next up previous contents
Next: Next Steps Up: PARTIAL FORMALIZATIONS AND THE Previous: Tree Search

Some Formulas for a Simple Lemmings Game

Game0 is a simplification of the first game of Lemmings Jr. There is only one lemming.

We give a sequence of formulas narrating the journey of a lemming tex2html_wrap658 from the lemming source to the lemming sink. It applies to the journey of the lemming chosen to dig even when other lemmings are present. For each formula we say where we expect it to come from.


 equation232
As is conventional in situation calculus formalizations, tex2html_wrap653 is the initial situation. The formula states that the lemming source will open. This is inferred from a general fact about the start of lemming games. Some lemming games have more than one source. However, we may take it as an observation of the screen that there is one lemming source in this game.

Let tex2html_wrap788. We now have


displaymath850
This follows from (8). It is a general fact about Lemmings that a lemming will fall out if not all have fallen out. Calling one of them tex2html_wrap658 is allowable, but we'll do this more precisely in a later version of these formulas.

Let


 equation237
This is the next situation in which tex2html_wrap658 is falling.


displaymath851
A simple chamber will be rectangular on the screen with walls at both ends. We make tex2html_wrap652 a simple chamber in tex2html_wrap653 and can rely on persistence to keep it a simple chamber in tex2html_wrap654 and beyond. This would be used in planning to solve Game0. Alternatively, if we are actually playing Game0, we can observe that tex2html_wrap652 is a simple chamber in tex2html_wrap654. This requires a mechanism for associating names with features of the picture and with situations depicted on the screen.

Next we want

Let tex2html_wrap796.

This is the point on tex2html_wrap652 immediately below the source. I suppose we should assert (and later infer) it exists before we name it.


displaymath852


displaymath853
Now we can have


displaymath854

We are now ready for


displaymath855
and consequently


displaymath856
with


displaymath857

Now that tex2html_wrap658 is down on the floor of tex2html_wrap652, it will walk around until the player turns it into a digger. The details of that, while part of the ``biography'' of l0, do not come into postulating


displaymath858
because this refers to an action of the player in designating tex2html_wrap658 to be a digger. From it we get


displaymath859

The fact that tex2html_wrap658 is still in tex2html_wrap652 does come into inferring from


displaymath860
that


displaymath861

Now we need more geography, including the lower chamber tex2html_wrap662. We need to say that tex2html_wrap662 is a simple chamber modified by putting the lemming sink at its right end. We also must say that every point of the floor of tex2html_wrap652 is above the ceiling of tex2html_wrap662.

I am not satisfied with the suggestions given above for describing chamber types as modifications of basic types, so we will omit this for now. On the other hand, it is straightforward to say that the floor of tex2html_wrap807 is above the ceiling of tex2html_wrap652. We have


displaymath862
and from it we get


displaymath863
and


displaymath864

We have used tex2html_wrap809.

Similarly we want to infer that tex2html_wrap658 will fall to a point tex2html_wrap811 on tex2html_wrap812, giving


displaymath865


displaymath866

Now we have two cases according to whether tex2html_wrap813 or tex2html_wrap814. In either case we can show


displaymath867
.

I used tex2html_wrap678 instead of just tex2html_wrap816, because we might want to quantify over tex2html_wrap679. However, we haven't used this in the formulas given so far.

There are many more non-trivial matters that require careful consideration.




next up previous contents
Next: Next Steps Up: PARTIAL FORMALIZATIONS AND THE Previous: Tree Search

John McCarthy
Mon Mar 2 16:21:50 PDT 1998