VocabularyNext Things Next

The “Vocabulary” box is where we tell the solver what we want it to find. In the fairytale example, maybe the aim is to find the lucky winner among Esmerelda’s suitors – the one chosen by Her Royal Highness – so we might see in the “Vocabulary” box something like:

name TrueLove: suitor {}

Then we can use the word “TrueLove” as the name of a suitor in writing constraints, just as we used “x” in the trivial numerical example on the Introduction page, to state the conditions that have to be satisfied by the chosen suitor. If we wished, we could simply use it in constraints as we did with x, without declaring it, but if it is an important part of the language we may prefer to make it explicit and state its type.

The sort name after the colon tells us what sort of thing is allowed to be the value of the name. In this case, TrueLove has to be one of the suitors; any attempt to use the name where a thing of a different sort is expected will result in an error message saying that the types of the expressions do not match. Logic for Fun is very strict about types – a fact which may initially seem annoying but which actually helps make the job easier.

“TrueLove” is just a name, or constant. Vocabulary can be more complicated, however. Suppose a relevant consideration is how much gold each dwarf has. Then we might see a declaration like:

function n_coins(dwarf): natnum {}

We then require the solver to determine how many coins each dwarf has. The expression “natnum”, usually abbreviated to “nat”, means that the valuie in question is a natural number (0, 1, 2, …). We can use “n_coins” to write conditions in the “Constraints” box like:

n_coins(Doc) > n_coins(Grumpy).

to say that Doc is richer than Grumpy. The function has an argument place which may be occupied by a dwarf, and it delivers a value which is an non-negative whole number representing how many coins that dwarf has. That is the meaning of the function declaration: the function goes from each dwarf to an number. In jargon, we say it maps the seven dwarves to natural numbers.

In the “Vocabulary” declaration, the expression in the parentheses is the name of a sort. In a constraint, the expression in that position will refer to a thing of that sort.

A function symbol like “n_coins” is used to make expressions that refer to objects (integers in this case) rather as names do. To make sentences out of those, we use predicate symbols. For instance, maybe the problem requires us to talk about whether a dwarf has an odd or even number of coins. For this, we could use a predicate “is_even”, for instance, so “is_even(4)” is true, while “is_even(3)” is false. We declare:

predicate is_even(nat) {}

A statement like

is_even(n_coins(Grumpy))

will then say that Grumpy has an even-sized hoard.

Predicates and functions with arguments, unlike names, must be declared in the “Vocabulary” box before they can be used to say anything.

Functions (and predicates) can have more than one argument place. Suppose the suitors have to joust against each other one-to-one. For each such contest there is a victor:

function victor(suitor, suitor): suitor {}

Then victor(x,y) is whichever of the two (x or y) wins the joust between x and y. Notice that there are two argument places in this case, so we say that the “victor” function is dyadic. Of course, victor(x,y) must be the same suitor as victor(y,x), though that’s a special feature of “victor”: it is not true of functions in general that you can reverse their argument places and still get the same value.

Vocabulary:

name TrueLove: suitor. {}

function {

n_coins(dwarf) : nat {}

victor(suitor,suitor) : suitor {}

}

predicate is_even(nat) {}

Declarations of the constant “TrueLove”, monadic function “n_coins”, dyadic function “victor” and predicate “is_even”.

In any model found by the solver, TrueLove must be one of the suitors, each dwarf must have a specific number of coins (an integer), and the outcome of each joust between two of the suitors must be determined.