Top Preface Data Types
French French German German ItalianItalian SpanishSpanish PortuguesePortuguese JapaneseJapanese KoreanKorean ChineseChinese

Predicates


So far, we have seen formulas used only as queries. But formulas can also be named and stored away for later use. A formula which is named in this way is called a predicate, and predicates are the basic building-blocks of FormulaOne programs. They correspond roughly to the procedures, functions, and subroutines of languages such as Pascal and Basic.

Predicates and Modules

A predicate definition must be stored in a FormulaOne entity called a module. Basically, a module is just a group of predicate definitions and associated information, stored in a file.

A Simple Predicate Definition

Previously we learned how to solve puzzles of the form 
8*s + 6*b = 46
We took the variables to be the numbers of spiders and beetles in a box, but they could just as easily be the numbers of 8-inch and 6-inch pieces that could be cut from 46 inches of dowel. Say that we wanted to solve this kind of problem a lot, but sometimes with numbers other than 46 on the right-hand side. We could do this by defining the following predicate: 
pred Puzzle_soln(x::L, y::L, z::L) iff
    x > 0 & y > 0 & 8*x + 6*y = z
An English translation of this definition is the following:

The predicate Puzzle_soln is true of x, y, and z if and only if x>0, y >0, and 8*x + 6*y = z

Even better, we could say

"x spiders and y beetles' is a solution to the spiders-and-beetles puzzle for z legs if and only if....".


Installation of the FormulaOne compiler also installs the Tutorial project with the module called Tutorial. It contains most of the predicates discussed in this tutorial. You can use this module if you do not plan to type the predicates yourself. The module must be compiled before it can be used the first time. Another possibility is to create your own module, type in the text of the Puzzle_soln predicate so that it appears exactly as above and compile the module afterwards.
Now you can pose the following query. 
all Puzzle_soln(s, b, 46)
No variable declarations are necessary in this case, because FormulaOne can deduce that s and b are numbers from the definition of the predicate Puzzle_soln. Also note, that we are omitting a list of variables after the all, so that all variables will be printed. We should get the same answer as before. FormulaOne has computed this query by replacing it with the predicate body (the part following the iff), after substituting the variables s for x and b for y, and the number 46 for z. It has solved the resulting query, s > 0 & b > 0 & 8*s + 6*b = 46, just like a regular query.
This is how FormulaOne handles all predicate calls (as we call such formulas - logicians would call them predicate applications). It substitutes the predicate call by the predicate body, in the process substituting arguments (the terms given in the call, like s, b, and 46) for the formal parameters (the variables in the predicate declaration, like x, y, and z). If we posed the query Puzzle_soln(s, b, 48), it would substitute 48 for z instead of 46, and we would get the expected response.

Reading Predicate Calls

A predicate is something which expresses some property, quality, or relationship possessed by a term or a group of terms. It's important that we name predicates in such a way that the property they express is clear, even given the terse syntax of logic they are phrased in.
Above, we have defined a predicate which expresses the property that x spiders and y beetles have a total of z legs. We have called it Puzzle_soln so that we can read a call such as Puzzle_soln(a, b, 46) as 'one puzzle solution is a and b when the total is 46 '. Since it's not always clear what the intended reading of the predicate is, it's a good idea to put a comment in the program text immediately after the first line of a predicate declaration, to tell how a call to it is supposed to be read: 
pred Puzzle_soln(x::L, y::L, z::L) iff
    { There are 'x' spiders and 'y' beetles if there are 'z'legs }
    x > 0 & y > 0 & 8*x + 6*y = z
A comment, in general, is any text enclosed by an open brace {, and close brace }. Comments can appear anywhere in program text, and can appear on a single line or be split across any number of lines:

{There are 'x' spiders and 'y' beetles if there are 'z'legs}
Comments can be nested, so that
{Level 1 {Level 2 {} {} }
 Level 1 again}
is a single comment. All the text within a comment is ignored; it is there to help us read and understand program text. This is especially useful for indicating how a predicate is to be read.

Variables

Unlike in the C programming language where a variable can be declared as local or global, in FormulaOne we have only so-called "local" variables. What variables can a predicate "see"?. It can only see
All these variables are local variables. No other predicate can use, alter or refer to a local variable unless it is given access to it by having the variable passed to it as a parameter. This restriction can cause a loss of efficiency on some occasions but to counterbalance that is the great benefit that whole classes of programming errors are eliminated.
For example, we could define a predicate Divis, which expresses the property that one number is divisible by another, by the following: 
pred Divis(x::L, y::L) iff
     {'x' is divisible  by 'y'}
     z::L & z*y = x
An English translation of this definition is the following:
'The number x is divisible by the number y if and only if there is some number z such that z multiplied by y results in x.'
This is exactly how a mathematician would define it. The variable z, which appears only in the body of the predicate, is a local variable, and the predicate is true only if FormulaOne can find some value for z which satisfies z*y = x. For example, the query 
all Divis(6,3)
is successful (z is 2), and so is 
all Divis(69,3)
(z is 23), but 
all Divis(25,6)
fails because there is no z which, when multiplied by 6, will result in 25.
Constants, types and predicates can be designated with the local keyword, but this must not be confused with the concept of 'local' variable.

Calling Predicates in Predicates

Predicate definitions can, of course, refer to other predicates: 
pred Even(x::L) iff
     {'x' is even}
     Divis(x ,2)
"The number x is even if and only if it is divisible by 2." When a call to Even appears in a query, it would be expanded into the Divis call, and then that would be expanded into the body of Divis.
Predicates can even refer to themselves. Such predicates are called recursive, and are used to allow FormulaOne to perform some action repeatedly. The following predicate will find the greatest common divisor of two numbers x and y by an algorithm known since Euclid's time: keep changing the numbers by subtracting the smaller number from the larger, and when the smaller number is zero, the larger number will be the GCD. 
pred GCD(x::L, y::L, n::L) iff
    { The greatest common divisor of 'x' and 'y' is 'n' Uses the Euclidean algorithm }
    y = 0 & n = x
    | x = 0 & n = y
    | y > 0 & x >= y & GCD(x-y, y, n)
    | x > 0 & x < y & GCD(x, y-x, n)
We'll see a more readable version of GCD when we get to if formulas. Let's see how this predicate would work on a query like this: 
all GCD(6, 9, z)
The predicate call would be expanded, replacing 6 for x, 9 for y, and z for n: 
6=0 & z=9
| 9=0 & z=6
| 9>0 & 6>=9 & GCD(6-9, 9, z)
| 6>0 & 6<9  & GCD(6, 9-6, z)
The first three parts of this formula obviously fail, but 6 is indeed greater than 0 and less than 9, so the query is essentially reduced to GCD(6, 3, z). This call expands into 
6=0 & z=3
3=0 & z=6
3>0 & 6>=3 & GCD(6-3,3,z)
6>0 & 6<3 & GCD(6, 3-6, z)
which is reduced to GCD(3, 3, z), and from there, it is reduced to GCD(0, 3, z). This last call will be reduced to z = 3, and we will have the solution. (There will be some backtrack formulas, but all of them will fail; so this will be the only solution.) Here are some more examples of simple recursive arithmetic predicates. Later we will learn how to make these predicates a little more readable with the use of the if formula; but they work perfectly as listed. 
pred Factorial(x::L, f::L) iff
     {'x'-factorial is 'f}
     x<2 & f=l
     | x>=2 & Factorial(x-1, sub) & f=x*sub
     {note that 'sub' will be declared implicitly, as sub::L}

pred Fib(index::L, number::L) iff
     {'number' is the 'index'-th Fibonacci number}
     index<=2 & number=l
     | index>2  &
     Fib(index-l, last) & Fib(index-2, prev) & number = last + prev
This last predicate could be made a lot more efficient. Each call makes two recursive calls, one for the previous number and one for the number before that. So a call like Fib(5, x) will generate one call for the fourth Fibonacci number, two calls for the third, three calls for the second, and so on. A better way to program Fib is for it to pass off most of the work to an auxiliary predicate which is recursive. 
pred Fib1(index::L, number::L) iff
{'number' is the 'index'-th Fibonacci number} Fib_prev(index, prev, number)

pred Fib_prev(index::L, prev::L, number::L) iff
     {'prev' and 'number' are two Fibonacci  numbers
     in sequence, with 'number' being the 'index'-th}
     index<=2 & prev=l & number=l | index>2 &
     Fib_prev(index-1, befprev, prev) & number = befprev + prev

More Formal Definitions

A predicate name is a sequence of letters, numbers, and underscores, beginning with a capital letter. A predicate definition is of the following form:
pred Name(varl::typel,var2::type2,...varn::typen) iff formula

Each of the vari above is a variable identifier, and Name is a predicate name.

Summary


Top Preface Data Types