ExistenceMore Advanced Topics

One of the more tricky built in predicates is “EST”, which (not surprisingly) is used to say that things exist. Where e is any expression, “EST (e)” has the same semantics as “SOME x (x=e)”, but it is to be preferred, not only because it is shorter but also because it is more efficient as the solver has built-in ways of reasoning with it.

Let’s go back to the seven dwarves. Recall that they are given as an enumerated list in a sort declaration, as shown to the right of this page.

Now let’s look at the function that increments each dwarf by two. In the “Vocabulary” box, you will see the “next” and “next but one” functions. The “partial” means that they are not always guaranteed to have a value.

In the “Constraints” box we stipulate constraints defining the new functions, as expected.

If you hit SOLVE you will see that, for instance, NextButOne(Happy) is Dopey. The last two dwarves, however, have no “next but one” because, if you like, the function has fallen off the end of the list of dwarves.

Now one might think that the condition

ALL d (Next(d) < NextButOne(d)).

is automatically true, but if you try adding this as an extra constraint you will discover that there is no model of it consistent with the earlier definitions. That is because Next(Doc) does not exist, and so does not come earlier in the order than NextButOne(Doc). In order to make the ordering condition true, we need an existence restriction:

ALL d (EST(NextButOne(d) ) IMP Next(d) < NextButOne(d)).

That is, “If there exists such a thing as NextButOne(d), then it comes after Next(d).” This is the commonest kind of use for the “EST” predicate, to clear away nonsense cases so that the rest of a constraint says what it is supposed to say in the presence of partial functions.

Why don’t we need to stipulate that there is such a thing as Next(d)? Well, the order of the natural numbers 1 and 2 is built into the language, so if adding two to a dwarf stays within the domain, then adding one surely does.

What the solver actually does with terms which fail to refer is to set them to an invisible “undefined” value of the appropriate sort. This is a “junk” value which is of the right sort (so that you don’t get type errors when reference fails) but it is not one of the things in the universe and cannot be the value of a variable.

Applying a function symbol f to a term t gives a longer term f(t). In general, if t has no reference (i.e. it is assigned the non-object as its value) then the same is true of f(t), except of course that the sort of t and the sort of f(t) need not be the same. However, the built in (pre-defined) predicates do have values in cases of non-existence. This is most obvious in the case of the predicate EST: if “t” has no value then “EST (t)” is false, not valueless. Similarly, identity statements always have a value. If a exists but b does not, then “a = b” has the truth value FALSE. On the other hand, if neither a not b has a value, then they are both assigned the non-object, so in that case “a = b” holds and has the truth value TRUE. Since the non-object is not in the universe, it is not ordered with respect to anything that exists, so the relations ‘<’ and ‘>’ always return FALSE unless both of the terms they apply to succeed in referring.

Note that “a <= b” for instance is a disjunction. It means the same as “a < b OR a = b”. This is not quite the same as “a !> b” becausse in the case where “a” has a value, but “b” does not, “a <= b” is false but “a !> b” is true. Similarly, in the same case, “a <> b” is false because there is no ordering in either direction between something that exists and something that doesn’t, but “a != b” is obviously true. Hence there is a subtle difference between the two ways of expressing non-identity, so care must be taken in the use of these relations where partial functions are present.

Confused? Take a look at the example on the next page…