French German Italian Spanish Portuguese Japanese Korean Chinese

- Predicates and Modules
- A Simple Predicate Definition
- Reading Predicate Calls
- Variables
- Calling Predicates in Predicates
- More Formal Definitions
- Summary

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.

8*s + 6*b = 46We 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 = zAn 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*

"*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

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

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

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 = zA 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.

- the variables which are in its parameter list, or
- variables which are defined in the body of the predicate itself, or
- variables which are implicitly defined in a predicate call made by this predicate. An example is the Sum predicate.

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

pred Divis(x::L, y::L) iff {'x' is divisible by 'y'} z::L & z*y = xAn 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

all Divis(6,3)is successful (

all Divis(69,3)(

all Divis(25,6)fails because there is no

Constants, types and predicates can be designated with the

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

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

all GCD(6, 9, z)The predicate call would be expanded, replacing 6 for

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

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

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 + prevThis 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

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

pred Name(var_{l}::type_{l},var_{2}::type_{2},...var_{n}::type_{n}) iff
formula

Each of the

- Predicate definitions allow us to compute the same formula many times with different parameters .
- Predicate definitions must appear in program modules, and the modules must be compiled before FormulaOne is able to use those definitions in queries.
- FormulaOne expands a defined predicate call into the body of its definition, substituting arguments for parameters.
- Predicate definitions should include comments to help readers understand what they signify.
- Predicates can refer to local variables not appearing in their list of parameters.
- Predicates can call other predicates, including themselves. Predicates which call themselves are called recursive.

Top Preface Data Types