ConstraintsNext Things Next

So we know what sorts of things there are in the universe of our problem, and we know what functions of those sorts the solver is to work out. Now to state what the problem actually is, we need to put conditions on what counts as a solution. For this we use the “Constraints” box.

Each constraint is simply a statement which is required to be true before anything counts as a solution. The simplest kind of constraint is an equation or inequation such as the ones with which this guide began. Every constraint must be terminated with a full stop (period). White space (spaces, tabs and line feeds) between words is irrelevant except to separate them, so it’s OK to break long constraints across two or more lines, indent them and so forth, to make them easier to read.

We have seen what the solver’s output looks like where there is just a constant (name) to find. We have also seen monadic functions, in the Queens and Muddle Management problems. Here’s another example:

Sorts:

thing enum: this, that.

Vocabulary:

function opposite(thing): thing {}

Constraints:

ALL x NOT (opposite (x) = x).

Here we take the world to consist of two things called “this” and “that”, and we want to find the function “opposite” which takes each of these things to the other one. The vocabulary declaration says that the opposite of a thing is a thing.

Let’s concentrate on the constraint, which says that opposite(x) is not equal to x. There are two features particularly worth noting. Firstly, this condition is stated to hold not just of some specific thing but generally of all things of the appropriate sort. In other words, it does not matter what we substitute for the “x”, the result has to be true. The special keyword ALL lets us say this straightforwardly. Secondly, note the keyword NOT, which of course negates the equation, so that we can say the two things are not the same. This is obviously very useful.

Sorts:

thing enum: this, that, home.

Vocabulary:

function i(thing): thing {}

function *(thing, thing): thing {}

Constraints:

ALL x ( x * home  =  x ).

ALL x ( x * i(x)  =  home ).

ALL x ALL y ALL z ( x * (y * z)  =  (x * y) * z ).

Now to illustrate what happens in the case of binary (or dyadic) functions, and to show you the neat trick of writing binary symbols in infix (between their arguments) rather than prefix (before them), here’s a definition of a group of three “things”.

The third thing, “home”, is the identity for the group. There are two functions, i (inverse) and the group operation symbolised by a star. Don’t worry if you don’t know what a “group” is: these pages are all about logical puzzle solving, not mathematics, so this is as far into group theory as we are going to venture!

The point worth noting this time, apart from what the solver says when you pose it this problem, is that a term like “y * z” built up with a function symbols can itself be used in the argument place of another function.