Harvey Mudd College
Computer Science 60
Assignment 10, Due Thursday, April 6, by midnight

Prolog Puzzles plus Program Proving

You will need to submit either two files or one file and a hand-written part for this assignment. Problems 1-3 are prolog "programs" (really predicates). They should be submitted all together in a file named puzzles.pl . There is a (small) file named /cs/cs60/as/a10/puzzles.pl with a few predicates to start you out. The second part (Problem 4) can be typed and submitted as an ascii file named proof.txt or handwritten and submitted under the door of Olin 1245 by 6:00 pm Sat., Apr. 8.


Problem 1

Write a prolog clause (or a number of clauses) that implement remove, where remove(E, LBefore, LAfter) indicates that LAfter is the same as list LBefore, except that the first occurrence (if there is one) of element E is removed from LAfter. If E is not in LBefore, then LAfter is identical to LBefore.

For example, possible uses of remove might include

?- remove(1, [2, 1, 3, 1], [2, 3, 1]).

yes


?- remove(X, [2, 1, 3, 1], [2, 1, 1]).

X = 3 ;
no


?- remove(1, [1, 2, 3, 1, 2], X).

X = [2,3,1,2] ;
no


?- remove(1, X, [2, 3, 4]).

X = [1,2,3,4] ;
X = [2,1,3,4] ;
X = [2,3,1,4] ;
X = [2,3,4] ;
X = [2,3,4,1] ;
no

You may want to use the member predicate we discussed in class as an example.

Problem 2

Pattern matching is an important task in many applications such as cryptography and DNA sequencing. This problem asks you to find a sublist wherever it might appear within a larger list. Write the predicate find(Pattern, Target, Index) that takes two lists Pattern and Target and a non-negative integer Index as input. This predicate is true if and only if Pattern occurs inside list Target beginning at position Index.

For example, here is a Prolog query and response:

      | ?- find([1, 2], [1, 2, 1, 2, 1], 0).
      yes
    
Notice that pattern [1, 2] occurs in target [1, 2, 1, 2, 1] beginning at position 0 of the target (that is, the very beginning of the target list).
    [1, 2, 1, 2, 1]
     ^
     |
     The pattern [1, 2] appears beginning right here at location 0.
     I'm looking for a 1 followed immediately by a 2 and I find it
     beginning here!
    
It also occurs again at position 2 of the target.
    [1, 2, 1, 2, 1]
           ^
           |
           The pattern [1, 2] appears beginning right here at location 2.
    
Thus, here's another Prolog query and response:
      | ?- find([1, 2], [1, 2, 1, 2, 1], 2).        
      yes
    
In fact, these are the only two occurences as indicated by the following Prolog query and response:
      | ?- find([1, 2], [1, 2, 1, 2, 1], X).   

      X = 0 ;
      X = 2 ;
      no
    
Write the rules for the predicate find. You may want to write some helper predicates to make find easier, though it can be written without such helper predicates.

Problem 3

In this problem you will be solving (or writing prolog predicates to solve) the general Missionaries and Cannibals problem. You may want to use the example puzzles -- particularly the towers of Hanoi problem -- done in class as a guide.

In this problem, there are some number of missionaries and cannibals on the banks of a river and only one boat available. The goal is to achieve some desired configuration of missionaries and cannibals on the two sides of the river, but you are subject to two constraints. First, the number of cannibals can never be greater than the number of missionaries on either side of the river. If, however, there are no missionaries at all on one riverbank, then there may be any number of cannibals there. The second constraint is that there is only one boat available. Thus, it has to go back and forth across the river. The boat must have at least one person to navigate it (either a missionary or a cannibal) and can fit at most two people (any combination of missionaries and cannibals).

The problem is to write a prolog predicate solveMC that will enable queries to solve arbitrary missionaries and cannibals problems. One way to write solveMC is the following:

solveMC( MoveList, StateList, StartState, EndState ) :- ...
where the predicate solveMC takes four arguments: the first is the list of legal moves that will get the missionaries and cannibals from their initial configuration (StartState) to their final configuration (EndState). The second argument StateList is a list of all of the configurations that have been seen "so far." The states in this list must be avoided (to avoid loops).

You will want to use the member predicate (gone over in class and in /cs/cs60/as/a10/puzzles.pl). You will also want to write your own "helper" predicates -- for example, a predicate named valid that checks that a particular State is valid under the problem's constraints. Another helpful predicate might be move that describes each of the legal moves. There are 10 legal moves, listed below. Please use these names (to make checking your work easier):

mToL      - one missionary from right to left
cToL      - one cannibal from right to left
mmToL     - two missionaries from right to left
ccToL     - two cannibals from right to left
cmToL     - one missionaries and one cannibal from right to left

mToR      - one missionary from left to right
cToR      - one cannibal from left to right
mmToR     - two missionaries from left to right
ccToR     - two cannibals from left to right
cmToR     - one missionaries and one cannibal from left to right

Some example runs of the solveMC predicate include

/* The original problem */

?- solveMC( MoveList, [], [ left, 3, 3, 0, 0 ], [ right, 0, 0, 3, 3 ] ).

MoveList = [ccToR,cToL,ccToR,cToL,mmToR,cmToL,mmToR,cToL,ccToR,mToL,cmToR]; 
<plus others, you may have a different initial solution>


/* Just getting one missionary and one cannibal across */

?- solveMC( MoveList, [], [ left, 1, 1, 0, 0 ], [ right, 0, 0, 1, 1 ] ).

MoveList = [cmToR] ;
<plus repeats, though there are no other solutions>
<that do not repeat states.>



/* There is no solution that gets 4 missionaries and 4 cannibals across. */

?- solveMC( MoveList, [], [ left, 4, 4, 0, 0 ], [ right, 0, 0, 4, 4 ] ).

no



You can also use setof to get all distinct solutions.

/* There are four distinct solutions to the original */

a(S) :- setof(Moves, solveMC(Moves, [], [ left, 3, 3, 0, 0 ], [ right, 0, 0, 3, 3 ] ), S).  

?- a(S).

S = [[ccToR,cToL,ccToR,cToL,mmToR,cmToL,mmToR,cToL,ccToR,cToL,ccToR],
     [ccToR,cToL,ccToR,cToL,mmToR,cmToL,mmToR,cToL,ccToR,mToL,cmToR],
     [cmToR,mToL,ccToR,cToL,mmToR,cmToL,mmToR,cToL,ccToR,cToL,ccToR],
     [cmToR,mToL,ccToR,cToL,mmToR,cmToL,mmToR,cToL,ccToR,mToL,cmToR]] ;
     
no


/* There is only one solution to the single missionary, single cannibal problem */

b(S) :- setof(Moves, solveMC(Moves, [], [ left, 1, 1, 0, 0 ], [ right, 0, 0, 1, 1 ] ), S).  
?- b(S).

S = [[cmToR]] ;

no

Note that all of theses solutions do not allow repeated states (otherwise whenever there was one solution, there would be infinitely many, because a cannibal could cross the river any number of times after the initial solution was found).



4. Transition Induction

(10 points)

The solution to this problem should be typed into a plain text file and submitted as proof.txt. Alternatively, the solution can be written out and handed in at Olin 1245 by 6:00 pm Sat.

Given the following program, create appropriate loop invariants (statements that are true each time the program reaches the point labeled /* HERE */ in the code). You should have 4 invariabts -- one for each of x, y, z, and i.

Once you have your four loop invariants, prove them true by induction. Then, use the loop invariants to show that that the following function returns the cube of its argument, assuming that the input argument is non-negative.

Thus, you will need to prove two things: (1) that each loop invariant you've created holds true before every loop test and (2) that for the precondition N >= 0, the postcondition x = N*N*N holds (as long as N hasn't changed).

static long cube(long N)
  {
  long i, x, y, z;
  x = 0;
  y = 1;
  z = 6;

  for( i = 0; /* HERE */ i < N; i++ )
    {
    x = x + y;
    y = y + z;
    z = z + 6;
    }
  return x;
}

Testing

Prolog doesn't offer the kinds of redirection that rex does, so there are no test files to use this week. However, I would suggest testing your prolog predicates with the examples given in the problem descriptions.

Reading

Prolog, Predicate logic, and proving programs correct are all covered in Chapter 10 of the book.

Submission

You should submit (or hand in) a proof.txt file that answers Problem 4. The puzzles.pl file with your prolog solutions should be submitted in the usual way, i.e., with

% cs60submit puzzles.pl
In each case you will be asked to input the assignment number (10).

Extra Credit

For optional bonus credit (up to 20%), write a prolog predicate (you will need helper predicates to do this) that solves the four fours problem. This is a very open-ended extra credit -- all solutions are necessarily partial solutions. You should consider solving the problem from 0 to 100 an absolute success. Martin Gardener (a long-time columnist for Scientific American) claimed that solving it for the integer 113 was impossible, though it's not proven one way or the other! If you do try it, submit your prolog code in a separate file named fours.pl.

The four fours problem is the following challenge: for each nonnegative integer, write that integer as an arithmetic combination of exactly four fours. Some of the many possible examples for the first few (nonnegative) integers are these:

0 =  4 + 4 - 4 -4

1 =  44 / 44

2 =  (4/4) + (4/4)
  
3 =  4 - (4/4) - sqrt(4)
  
4 =  .4 * (4 + 4 + sqrt(4))

etcetera.

The permitted operations are

As odd as it may seem, this problem has received a lot of attention in the formal (and not so formal) mathematical literature. Feel free to develop your own representations for sequences of operators and for the predicates you use. (Additional information on prolog is available from this site.)