Lunar Lockout

Lunar Lockout is a simple logic game, which was shown to me by a primary school teacher who bought it for the kids in her class. A few pieces are placed on a 5x5 board. The goal is to place a particular piece at the center, while being allowed to move any piece only if it can be blocked by another piece. It's a classic example of a game that can be solved by brute-force search.

I programmed a simple solver in Python. The method by which I programed this solver could be used to solve many other logic games. In fact, you could easily abstract the pieces away. You need:

1. a representation for a state of game (here, I use a list of cartesian coordinates, one per piece, the first element being for the piece that has to be moved to the center),
2. a function to generate all legal moves for a given state game,
3. a function that applies a move to a given game state, returning a new game state (it's easier than mutating the given game state for searching many alternatives at once).
4. a predicate to test whether a game state is a solution (here, I simply check whether the first coordinate is the center of the board).

With this pieces, it's easy to do a brute-force search (here, I use a breath-first search which skips already seen game states).

The Curry-Howard Isomorphism, a Tiny Appetizer

Enjoy these two facts.

Amazing fact 1: Any combinator (i.e. lambda-definable term) can be written using only the two combinators S (lambda (x) (lambda (y) (lambda (z) ((x z) (y z))) and K (lambda (x) (lambda (y) x). For a cute exploitation of this fact, see Iota and Jot: the simplest languages?.

Amazing fact 2 (The Curry-Howard Isomorphism): The types of combinators correspond to tautologies of propositional logic. For example, the type of K is A -> (B -> A). Read A, B as variables and -> as implication. Try S: (A -> (B -> C)) -> ((A -> B) -> (A -> C)). Even more, any tautology can be derived from S and K using modus ponens. Why? The rules (for abstraction and application) in typed lambda-calculus correspond to the rules (for introduction and elimination of implication) in a natural deduction system. For a whirlwind tour of lambda-calculus which mentions the Curry-Howard isomorphism, see the paper Church's Thesis and Functional Programming (PDF). For an exposition of a natural deduction system, see the book Building Problem Solver, section 4.4 Natural Deduction.