Top Data Types Control Structures
French French German German ItalianItalian SpanishSpanish PortuguesePortuguese JapaneseJapanese KoreanKorean ChineseChinese

Modes


One power of the variables we have worked with so far has been that they can be used and referred to without our knowing what their values are, or indeed whether they have values at all. But that power is sometimes not necessary, and in fact sometimes it gets in the way of writing efficient, readable programs.

You can specify, if you want, that a parameter or a local variable definitely has a value, or that it definitely does not have a value, when the predicate is entered. This is called the mode of the variable. The first kind of mode is called input mode, and is denoted by using the symbols " :< " instead of " :: " in the variable declaration; the second kind is called output mode, and is denoted by " :> ". The mode we have been using so far, denoted by " :: ", is called symbolic mode. Variables of this mode are often called logical variables in the terminology of Prolog.

Choosing variable mode specifications wisely can make your programs more readable. The compiler can also use this information to make compiled programs have the great efficiency of compiled Pascal or C programs, and to check for erroneous predicate calls which you have put into your program code by mistake.

Symbolic Mode

The variables we have been working with so far are in symbolic mode. (The symbols " :: " between the variable name and the type are what indicate that.) With symbolic mode, the FormulaOne compiler can't tell, at the time the program is being compiled, whether the variable has a value or not. That fact is, however, known at run time. In the representation of the variable in memory, along with the space for its value is space for constraints that have been put on the variable. By the nature of these constraints, the running program can tell whether the variable has a full value.

If the constraints so far have determined a unique value for the variable, it acts just like a variable in other programming languages like Pascal or BASIC.

Formulas which compare the variable to other terms by relational operators (" = ", " < ", etc.) act just like tests. But if a unique value is not known, such formulas put new constraints on the variable, which may result in finding a unique value, or (if the new constraint is incompatible) causing a failure and a backtrack. FormulaOne has to check which of these conditions holds every time it encounters any relational operator formula.

Input Mode

Consider the Sum predicate. Its first parameter is a list of I values, and the second is the sum of that list. Now, a query such as 
l::list I & Sum(l,3)

would be ridiculous, since there are an infinite number of lists of integers whose elements sum to 3. It may well be, in fact, that for any purpose you are going to use Sum for, neither the first variable nor any part of it will ever be unknown. That is, you may want to use Sum exclusively to find the sum of a known list, or to confirm that some number is the sum of a known list.

If this is the case, you could specify that the first parameter always has a value by declaring it to be an input mode parameter. 
pred Sum1(l :< list I, s :: I) iff
{The sum of the integers in 'l' is 's'}
     l = Nil & s = 0  |
     l = (head, tail) & Sum1(tail, tailsurn) &
     s = head + tailsum
The only thing that has changed here is that the first parameter is declared with the symbols :< separating the variable name from the type. The only effect this has is that the new Sum1 predicate can take only full-value terms in its first parameter; that is, terms built up from constant terms or variables which have values at the time of the predicate call.

But this is a decrease in power from what we had with the old Sum predicate. Why should we ever want to do such a thing? There are three main reasons.

The first is that input variables are more efficient than symbolic variables (those declared with ::). Since FormulaOne knows that an input variable must have a fixed value, it doesn't need to store information about its value, such as constraints. It need only allocate enough memory for the value itself. And of course it doesn't need to take the time to check whether the variable has a value when it performs a comparison.

The second reason is that it makes it clearer what the predicate is intended to do. If you explicitly state that, for instance, the first Sum1 parameter always has a value, it makes it clear that it is to be used to find the sum of a given list. This makes your programs more readable.
The third reason to use input mode declarations is that such declarations help the FormulaOne compiler help you to debug your programs. A query such as 

all z::list I & Sum(z, 3)
would soon cause a "Too many backtracks" error with the old version of Sum, after having returned one solution. But in a larger program, a variable with no value which should have a value can often work its way through many predicate calls before it causes a problem. Most programmers would prefer to be able to detect such mistakes at chosen points, than to have them come up in difficult-to-detect ways later in a running program.

An input variable has the significant property that it cannot be reassigned, i.e. given a new value. It can be referred to, deconstructed if it is a list or some other composite term, used as a parameter, anything as long as it is not reassigned.

Thus the following is a test, not a reassignment of: 
pred Test_x (x :< I) iff
    x = 3
The query Text_x(3) will succeed. Test_x(4) will fail but it will not modify x in the process. This property makes for a sort of safety valve. In the case where you have nested predicates (that is, one predicate calls another which may call more in turn) you can pass a value on to greater "depths" of nesting and know that the value cannot be accidently corrupted. This value prevents many hard-to-find program bugs.

Output Mode

Here's something that happens quite often in all computer programs: a routine is called, and the value of one of its parameters is fully computed and then passed back to the calling routine. If we have parameters which are handled like this in FormulaOne programs, we would like to be able to tell the compiler to use the efficient, constraint-free representation for the parameter. But we can't declare it to be an input parameter then, because we specifically don't know the parameter's value until it is computed.

Just as there is a way of telling the compiler that a parameter has a value, there is a way of telling it that a parameter does not have a value, but will receive one by the end of the predicate call processing. This kind of parameter is called an output mode parameter, and is denoted by the symbols ":> ", output between the variable name and the type.

The second parameter in our Sum1 predicate is a good candidate. We can declare it to be an output-mode variable by using the following as the first line in the predicate declaration: 
pred Sum1(l :< list I, s :> I)
This declaration tells the FormulaOne compiler to make sure that the parameter s receives a value in any call to Sum1. That information helps FormulaOne to compile calls to Sum1 more efficiently.
The only space allocated for an output variable in memory is, as for an input variable, enough space for its value. Constraints are not used for output variables either, because FormulaOne makes sure that the output variable is not used before its value is known. This means, for instance, that in Sum1, implicitly declared local variable tailsum is known to have a value after the recursive call to Sum1, so the addition operation immediately after is compiled as a simple addition, with no checks or constraints. The speed-up in this new version of Sum1 is very noticeable (just look at the time FormulaOne reports that it took to compute the sum of a list under the old and the new versions of the predicate).

FormulaOne imposes two restrictions on output variables. The first use of an output variable must assign a full value to that variable; and the variable must be used at some time in any call to that predicate, no matter which set of conditions has caused the predicate body to be true.

For instance, if we omitted the last line from the definition of Sum1, the new definition would not even be accepted by the compiler: 
pred Sum1(l :< list I, s :> I) iff
    l = Nil & s = 0 | l = (head, tail) &
    Sum1(tail, tailsum)
If s had been declared as symbolic mode, there would have been no problem with this definition. But as it stands, if l is not Nil, s is never assigned a value. FormulaOne cannot guarantee that s has a value at the end of the processing of any call to Sum1, so it refuses to accept the definition.

Here's another example of how input and output variables interact. It's just the Fibonacci number predicates from earlier in the book, modified by using integers and input and output annotations. Try to follow how data flows through the predicates as computation goes on. 

pred Fib2(index :< I, number :> I) iff
    {The 'index'-th Fibonacci number is 'number'}
    Fib prevl(index, prev, number)

pred Fib_prevl(index :< I, prev :> I, fib :> I) iff
    {'prev' and 'fib' are two Fibonacci numbers in sequence, where 'fib' is the 'index'-th}
    index <= 2 & prev = 1 & fib = 1 | index > 2 &
    Fib_prevl(index-1, befprev, prev) &
    fib = befprev + prev

Mode Clash

We have seen some examples of what happens when a term of one type is used as an argument corresponding to a parameter of another type. What happens when an argument does not match its parameter because of incompatibility in modes?

With output parameters, the answer is simple enough. While the usual thing to use as an argument to an output-mode parameter is another output variable, FormulaOne will accept symbolic or input variables, constants, or complex terms made up of a mixture of variables and constants. The way it handles the situation is to implicitly declare an invisible local output variable, use that in place of the original term, and then compare the result that comes back with the original term. For example, the query 

all Sum1((3, 2, 1, Nil), 6)
would be handled in the same way as would 
all Sum1((3, 2, 1, Nil), aux) & aux = 6
With input parameters, the situation is more complex. Normally FormulaOne allows only terms made up of constants, input variables, and output variables which have been assigned values to be used as input arguments. But it does not forbid the use of symbolic variables in input arguments, because sometimes, in the course of a program, symbolic variables do have definite values.

This means that symbolic variables are allowed, but a check is put into the compiled code to make sure that the variable has a value. If it does not, one of two things can happen. If the variable can take on a finite number of values, such as a variable of a subrange type, then the call is preceded by a formula enumerating all those possible values.

For instance, the query 
all i::[0..3] & Fib2(i, x)
would be handled in exactly the same way as the following query. 
all i::[0..3] & (i=0 | i=l | i=2 | i=3) & Fib2(i, x)
This clearly causes the query to backtrack to get all solutions, even though no explicit or-s, (|) were in it.

The other possibility is that the symbolic variable can take on an infinite or very large number of values, due to being of a type such as I or list S. In this case, FormulaOne sees that trying to "backtrack out" a value for the variable would cause it to keep backtracking indefinitely. This is the source of the familiar "Too many backtracks" help message on such errors. FormulaOne would like to be able to generate all the values for the variable, but cannot because the number of values is infinite.

There is one more mode of a variable, input/output (":."), which is explained separately since it can appear only in procedures and subroutines, special cases of predicates.

Summary


Top Data Types Control Structures