# Problem Set 4: Creating Life

### Due Thursday, March 27, 2008, 11:59 pm.

For this problem set, you are to turn in an overview document covering Part 2. The overview document should be composed as described in Overview Requirements. As with the previous problem set it is your job to convince us that your code works, by describing your implementation and by presenting a testing strategy, test cases, and results.

You may work on this problem set with a partner. We strongly recommend discussing, critiquing, and agreeing on specifications before doing any implementation. You can also bring specs to office hours to get feedback. When critiquing a spec, think about the spec both from the standpoint of the client who is going to use the spec, and the developer who must implement it. It is also a good idea to discuss and agree on abstraction functions and rep invariants for your data structures. You will also need to think about how to divide your program into modules.

We will be holding 20-minute design review meetings during March 10–13. Your group is expected to meet with one of the TAs or the instructor during their office hours, or with consultants during consulting hours. A signup schedule is available on CMS. You should be able to explain your design in about 15 minutes, leaving 5 minutes for questions. However, the course staff may interrupt and ask questions! In your design review, plan to talk about at least:

• How you will divide the program into modules, and why.
• Specifications for any modules you define.
• What representations (and invariants over them) you will use.
• Any other interesting issues you foresee.

## Part 1: Written Problems

1. Explain briefly how equipping a collection abstraction (such as lists, set, or maps) with a `fold` operation or operations (e.g., `foldl`, `foldr`) promotes loose coupling. Compare to the alternatives.

2. Propositional Logic

Prove the following statements using only the inference rules provided in Lecture 11: Natural Deduction.

1. P ∧ Q ⇒ P ∨ Q
2. ¬¬P ⇒ P
3. Predicate Logic

Prove the following statements using the inference rules for propositional logic in Lecture 11: Natural Deduction and the rules for quantifiers in Lecture 12.

1. ¬(∃x. ⊥)
2. (∀ x. Q ⇒ P) ⇒ ((∀ x. Q) ⇒ (∀ x. P))
4. Program verification

Suppose we have a function `max` with the following spec:

```(* Requires: ⊤
* Returns: r = max(x,y) where (r=x∨r=y) ∧ r≥x ∧ r≥y *)
```

Now we implement a function that takes the maximum of three numbers as follows:

```(* Requires: ⊤
* Returns: r = max3(x,y,z) where (r=x∨r=y∨r=z) ∧ r≥x ∧ r≥y ∧ r≥z *)
fun max3(x,y,z) =
if x <= y then max(y,z) else max(x,z)
```
1. Derive the verification condition for the function `max3` meeting its spec.
2. Prove the verification condition correct using the rules for predicate logic and the following axioms for inequality on integers:
• ⊢ ∀x.x≤x
• ⊢ ∀x.∀y.x≤y ⇔ y≥x
• ⊢ ∀x.∀y.∀z. x≤y ∧ y≤z ⇒ x≤z

## Part 2: Conway's Game of Life

1. If a cell is dead and it has exactly 3 live neighbors, it becomes live.
2. If a cell is dead and has any other number of live neighbors, it stays dead.
3. If a cell is alive and has either 2 or 3 live neighbors, it stays alive.
4. If a cell is alive and has any other number of live neighbors, it dies.

It might help to play around with the system in any one of many available implementations online to obtain a better grasp of the consequences of these rules.

All state transitions occur across the entire board at the same time. That is, if we consider the current state of the game to be represented as the state of each cell on the board, then the next state of the game is one in which the above transition function is applied once to each cell simultaneously. We call this board transition a tick. One can imagine a slight variation on this game in which live cells also contain an RGB color represented as a 3-tuple of integers, each between 0 and 255. For this variation, the transition rules given above need to be slightly modified. When a dead cell is brought to life by its three neighbors, it gets the average color of those neighbors. When a live cell is kept alive by its 2 or 3 neighbors, its color remains unchanged.

Your main task is to implement `structure GameOfLife`, for which we've provided a skeleton in gameOfLife.sml. The `structure GameOfLife` instantiates ```signature GAMEOFLIFE``` which we also provide in gameOfLife.sig. As will be discussed in greater detail below, we've given you an interface to a GUI that will allow you to display the state of your game graphically. The way you use your functions to update the GUI is intrinsically tied to your design, and you should consider this carefully when defining `type state`. The `GAMEOFLIFE` is defined as follows:

```signature GAMEOFLIFE = sig
(* Your representation of the current state of Conway's Game of Life *)
type state

(* A single 24-bit color.  Each channel may range from 0 to 255, with
0 being lowest intensity and 255 being the highest.  In order, the
color channels are Red, Green, and Blue. *)
type color = int * int * int

(* A cell (x,y,c) is alive at position (x,y) on the board, with
color c *)
type cell = int * int * color

(* an instance of board = n represents a board with
range [0,2^n - 1] in both the x and y dimensions *)
type board_size = int

(* The initial state of the game: a board, and a list of live cells *)
type config = board_size * cell list

(* Initialize the game state, from a provided configuration *)
val startConfig: config -> state

(* Advances the game of life by one tick, and updates the GUI with any
visible changes to the state of the board. *)
val tick: state -> state

(* zoom i sets the current zoom to level i - initial value is 0 When
i<0, each pixel drawn is equivalent to a 2^(~i) square cell block
When i=0, each pixel corresponds exactly to a single cell When
i>0, each cell is drawn as a 2^i pixel square block in the GUI *)
val zoom: (state * int) -> state

(* pan x y centers the view at (x+0.5,y+0.5) - initial value is set
to be x=y=2^(n-1)-1 - that is, located at the center of the 2^n
x 2^n board.  For higher levels of magnification, this offset
should be displayed exactly, but for zoomed-out views it is
acceptable to adjust the center by sub-pixel increments if the
implementation is simpler or faster *)
val pan: (state * int * int) -> state

(* autozoom b sets the Auto-Zoom state to enabled or disabled.  When
it is enabled, at every tick the pan and zoom values are adjusted
internally to ensure that all live cells are in view for the GUI,
and the level of zoom is as close as is reasonably possible. *)
val autozoom: (state * bool) -> state
end
```

The `GAMEOFLIFE` specification has some subtleties. The game's universe is square, with a power-of-2 number of cells in each dimension. Cells themselves occur at integer locations in our space. The upper left cell is (0,0) and the bottom right is (2n - 1, 2^n - 1) for board size n. However, the GUI is always centered between cells, and thus ` pan x y ` centers the view at (x+0.5,y+0.5). The following picture demonstrates this:

Note that because the viewing window is always centered between cells, we cannot zoom indefinitely. The viewing window is limited to 512 x 512 pixels, so zooming in further than `zoom 8` does not make much sense. When the level of zoom is such that each viewing window pixel represents several cells in the game of life, the color of the cell in the GUI should be displayed as the average color of all cells that fall within that window pixel, including dead cells, which are black (0,0,0).

### Getting Started

It is of the utmost importance that you come up with a good representation for the game state. Your representation should allow for efficient zooming at powers of two as described above and accommodate very large boards as long as they are sparsely populated; your implementation should handle sparse populations on board sizes as large as 224×224 efficiently. To assure this, run time must not grow linearly with the size of the board. Be sure that you have a good understanding of what is required for all parts of the assignment before you design the state representation.

### Using CM

You will compile multiple structures at once using the Compilation Manager (CM). We are providing a file sources.cm that contains a list of all files that need to be compiled. Use the compilation manager by typing CM.make("sources.cm"); at the SML command prompt. This command will automatically compile all of the files that have changed since the last time CM was invoked. Add your own files to the sources.cm file to have them compiled automatically.

### Using the GUI

Linux Executable (with source - requires SDL and SDL_net libraries)
Windows Executable (with source and required dlls)

When run, the GUI should open a 512×512 display window, as well as a console for displaying status messages.

### Connecting to the GUI with SML

To connect to an already-running instance of the GUI, invoke NetGraphics.setup with a list of pairs (host, port) as arguments. For example, `NetGraphics.setup [("localhost", 3124)]` will connect to the GUI running on port 3124 (the GUI's default) on the local machine. Once the connection has been established, you program will interact with the GUI using one command: ```NetGraphics.report( msg )``` where `msg` is a string containing a drawing command or commands, each of which is followed by a newline. The commands understood by the GUI are as follows:

• "Clear" will clear the entire GUI display to (0,0,0) (Black).
• "Pixel <X> <Y> <R> <G> <B>", where (<X>,<Y>) are the coordinates of the pixel to draw to, each from 0-255, and (<R>,<G>,<B>) is the 24-bit color value to color it, with values 0-255 for each channel.
• "Rectangle <X1> <Y1> <X2> <Y2> <R> <G> <B>", where (<X1>,<Y1>) and (<X2>,<Y2>) are opposite corners of the axis-aligned rectangle to draw, and (<R>,<G>,<B>) is the color to fill it with.
• "Flip" will swap the display buffers, rendering everything drawn visible to the user. It is not advisable to flip buffers after every drawing command - wait until you've drawn the entire results of a game step, as it will prevent flicker and run much faster.

Since the GUI only relies upon the first letter of the command to identify its type, it is perfectly acceptable and encouraged to shorten the command words to "C", "P", "R" and "F", respectively. To experiment with the effects of the different commands, you can also connect to the GUI outside of SML with `telnet localhost 3124`. Any commands you type in will executed by the GUI exactly as if they had been reported by your SML code -- remember to hit "F" and press enter to update the display!

### The Debug Loop

We've provided you with a tool, called the debug loop, to manipulate the Game of Life from the command line. After compiling the code (`CM.make("sources.cm")`), you can enter the debugging mode using the command Debug.debug s; where s is a valid state in your game. You will see a prompt (>). From here you have access to the follow commands:

• tick/t : Advance the state of the board by a single tick, updating GUI.
• tick/t i : Advance the state of the board by i ticks, updating GUI.
• zoom/z i : Set the zoom level to i, signifying that every cell occupies 2^i pixels in each dimension. For example, a zoom of 0 means that each cell is a single pixel, a zoom of 2 means that each cell is drawn as a 4×4 block, and a zoom of ~1 means that each pixel on the GUI represents a 2×2 square of cells.
• pan/p x y : Set the current center of the display window to cell (x+0.5,y+0.5) on the board. (The exact center of the display window should always be at the intersection of 4 pixels on the display, and 4 cells on the board.)
• autozoom/a b : Enable (b=true) or disable (b=false) automatic zooming and panning of the display. When enabled, the values for zooming and panning should be automatically adjusted at each time step to ensure that all live cells are visible on the display, without zooming out excessively.
• quit/q : Exit the debug loop.
• help/h : Show Help.

So long as you have correctly implemented all of the functionality in gameOfLife.sml, the debug loop should run smoothly and require no changes on your part.