Top
Control Structures
Building Types
French
German
Italian
Spanish
Portuguese
Japanese
Korean
Chinese
These predicates are called procedures because they are so much like the procedures of Pascal and C programming languages. Certain kinds of procedures can also be called functions. FormulaOne also facilitates subroutines, procedures that can access system information and variables.
| Class | Backtracking | I/O variables | External Data | Call pred | Call proc | Call subr |
| pred | yes | no | no | yes | yes | no |
| proc | no | yes | no | yes(*) | yes | no |
| subr | yes | yes | yes(*) | yes | yes | yes |
In addition, subroutines can access data external to the FormulaOne system such as user input and system date and time information. Any class of predicate can call a procedure but only a subroutine can call other subroutine (because external data are being passed implicitly from one subroutine to another). Also the procedures and subroutines cannot call predicates except in context of all/one/min/max formulas, though any predicate can call another predicate.
With that knowledge, FormulaOne can compile it into an efficient form that never keeps or refers to this backtrack data. You declare a procedure exactly the way you declare a true predicate, except that you use the keyword proc where you would normally use pred.
proc Sum3(l:<list I, sum:>I) iff
{the sum of the members of 'l' is 's'}
case l of
Nil => sum = 0;
(head, tail) => Sum3(tail, tailsum) & sum = head + tailsum;
end
proc Powers(first :< I, last :< I) iff
{ prints square and cube of integers from 'first' to 'last' }
square = first*first &
Print(first,' ', square,' ', first*square, '\n') &
if first < last then
Powers(first+1, last)
end
So a procedure is like a predicate which is entered, does its job, and exits, after which it can be completely forgotten about.
Although a procedure can't call a predicate directly, a predicate can call a procedure, because it's effectively just a special kind of predicate.
A procedure can fail, just like a regular predicate. A procedure like the following could be expected to fail if the first argument were not an even number.
proc Half(x :< I, y :> I) iff
{'y' is half of 'x'}
x mod 2 = 0 & y = x / 2
Procedure can use if and case formulas. In fact, these two types of formulas were defined partly with procedures
in mind. Since the possible outcomes in if's and case's do not overlap, no backtrack is ever needed for them, even in true
predicates. Also, because they cannot backtrack, procedure calls with output variables can be themselves used in the conditions of if formulas:
... &
Sum3(ilistl, s1) &
if Sum3(ilist2) = s1 then
Print('Sums the same\n')
end &
....
The if condition can be written even in the following form:
. &
Sum3(ilistl, si) &
if Sum3(ilist2,s1) then
Print('Sums the same\n')
end &
....
where Sum3(ilist2,s1) is actually test of the outcome of procedure Sum3 with input parameter ilistl, and previously obtained value s1.
In FormulaOne it is possible to use or-s, ("|") in the subroutine context of a query or in the bodies of procedures and subroutines. Or-s behave similarly as the boolean or in Pascal or C. For instance:
proc Test(x :< I) iff
x = 1 | x = 5
The procedure call Test(x) tests whether the argument x is 1 or 5.
The or-s within procedures and subroutines are efficiently compiled by the tests and jumps just as in Pascal or C. This is possible because there is no backtracking in the procedure/subroutine context. In contrast to this, or-s within predicates permit backtracking, and require a more complicated implementation mechanism called choice points.
FormulaOne performs an extensive data analysis to make sure that procedures do not backtrack. If a non-local output or input/output variable is to be modified within an or in a procedure context, the logic of FormulaOne calls for the use of backtracking. Consequently the compiler of FormulaOne prohibits non-local assignments within or-s. For instance the following procedure is not accepted:proc Gen(x :> I) iff
x = 1 | x = 2
This is because the procedure Gen generates a value for its output argument x from within the or. The query Gen(2)
should logically succeed but since it is compiled as Gen(z) & z = 2, and the value returned from the call is z = 1, the
test z = 2 fails. It is impossible to generate the correct value 2 without backtracking. Similarly, input/output variables
non-local to an or can only be referred to (i.e. can be tested). Assignments to such variables are not permitted.proc P1(x :< I) iff
y:=1 & (y := y + l & x = 2 | y = 1) & T(y,x)
In the call P1(1) the first branch of or fails the test x = 2 and the second one should succeed.
If your problem calls for non-local assignments to the output or input/output variables you will have to use predicates.
Assignments to local output and input/output variables within the procedures are permitted. For instance the procedure:
proc P2(x :< I) iff
y = 1 & T(x,y) | z := 5 & Q(x,z)
is a legal one because the effect of the assignment of 1 to the output variable y is localized to the left argument of the or.
Similarly, the input/output variable z can be modified within the scope of the right argument of the or. See the section Scope of Variables.
For instance, imagine a subroutine Dates(date string) defined with the following declaration:
subr Dates(date_string :> S) iff ...A query to this subroutine would look like this:
Dates(date)(Note the absence of the all keyword in this query, which we'll explain later.) The result of the query would be date = '06/11/2001', or whatever the current date was.
The restrictions on the bodies of subroutines are exactly the same as those on the bodies of procedures. But there is an important restriction on the use of subroutines: they can be called only from other subroutines, or from queries.
This restriction has to do with how we explain logically what is going on in subroutines. Subroutines have to access data which come from outside the parameters they have been given. This means that two calls of a subroutine, with exactly the same parameters, could give two different results at different times.FormulaOne explains this logical anomaly by considering there to be an "imaginary first parameter" to every subroutine. The imaginary parameter contains all the external data that will ever be requested by the subroutine, including user input. (This is just an abstract concept, and has nothing to do with how subroutines are actually computed. Clearly the value of the imaginary parameter is impossible to predict at the time the subroutine is called.)
The value of the parameter is "known" to the top-level query processor and is "passed down" from subroutine to subroutine as an input/output variable, being modified as various subroutines take what they need from it. So the distinction between procedure and subroutine is necessary in order to explain logically such things as user input. But it's also very useful to programmers, because it makes a clear distinction between predicates whose behavior cannot be predicted due to different user inputs, and those whose behavior is predictable only from their parameters.
proc Sum4(l :< list I, s :> I) iff
iosum :. I &
iosum := 0 &
Sum_io(l, iosum) &
s = iosum
proc Sum_io(l :< list I, sofar :. I) iff
case l of
Nil => true;
(head, tail) => sofar := sofar + head & Sum_io(tail, sofar);
end
Notice the new symbol in these procedures, ":= ". This can be read as "is assigned"; for instance, "sofar is assigned the
value of the expression sofar + head". It means that whatever value the variable to the left of the := was, it now will
take on the value of the expression to the right of it.
We can think of the sofar parameter in the above program as being like a pair of parameters, one input and one output, with an intermediate variable local to the procedure to hold the new value. Similarly, we can think of the iosum local variable as being an initial variable and another variable to hold its final value. If we rewrite the program in this way, it would look like this:
proc Sum5(l :< list I, s :> I) iff
iosum_first :> I &
iosum_last :> I &
iosum_first = 0 &
Sum_io1(l, iosum_first, iosum_last) &
s = iosum_last
proc Sum_io1(l :< list I, sofar_first :< I, sofar_last :> I) iff
case l of
Nil => sofar_last = sofar_first;
(head, tail) => sofar_med :> I &
sofarjmed = sofar_first + head & Sum_io1(tail, sofarjmed, sofar_last);
end
Of course, the reason we wrote it with input/output, i/o variables in the first place was that all these different
variables were collapsed into one. No new storage is ever allocated for the new versions of iosum or sofar; they all
use the same area of memory for their value.
Old values of i/o variables are overwritten with new ones, so no backtracking can be done on them because their old value has been lost. In procedures and subroutines, no backtracking is ever done, so there is no problem. In FormulaOne, it is possible to use input/output variables in the predicates. For instance:
pred P3(x :. I) iff
x := x + 1 | x := x + 2
The query
all x := 2 & P3(x)will give two answers x = 3 and x = 4. Note that the assignment x := x + 1 is automatically undone when backtracking occurs, and the original value x = 2 is restored. The i/o variables are used with great advantage in many situations within a predicate context. See the modules maze and containers for the examples of i/o arrays to record the state of traversal through a graph. The module schuses i/o variables in a predicate context in order to satisfy a constraint which is not expressible by the standard constraints.
When backtracking occurs the previous values of i/o variables are automatically restored. This is done by remembering (trailing) the value of an i/o variable just before an assignment changes its value.
Procedures cannot backtrack and they are compiled without saving the previous values of i/o variables. This increases the efficiency of generated code. For this reason the procedures with i/o arguments cannot be called from within the predicate (backtracking) context.
proc Incr(x:.I) iff
x := x + 1
the query
all x := 6 & (Incr(x) & x = 7 | x = 6)is not permitted because the procedure Incr destroys the old value of the variable x. In this particular case, it would be quite simple to remember the value of x just before the procedure Incr was called. In general, saving the current value could be expensive if, for instance the i/o variable passed to a procedure were an array. The procedure could change only one element of the array but the compiler cannot know this and would have to generate the code saving the whole array.
For the same reason it is impossible to use i/o files in the predicate context. File operations make changes to the files which cannot be undone upon backtracking.
Local i/o variables must be initialized on their first use, just like local output variables. This is because FormulaOne would rather enforce such a standard than to be unable to know whether an i/o variable had a true value or just the random value found in the memory allocated for it.I/O variables are especially useful as error condition and return code parameters, which are usually set to something other than a standard value only in special circumstances:
{ loop on the subroutine Get_process_command, until a fatal error
occurs or user requests termination}
subr Main_command_loop() iff
e:.I & e := 0 &
Get_process_command(e) &
if e > 1 then {error condition; fail}
Print('Fatal error\n') & false
elsif e = 1 then {normal termination}
Print('End of command loop\n')
else
Main_command_loop()
end
subr Get_process_command(e :. I) iff
Print('Enter q to quit, a to abort ') &
Print('or anything else to continue') &
TTYKeyGet(x) &
if x = "q" then
e := 1
elsif x = "a" then
e := 2
else
Print('...processing')
end &
Print('\n')
I/O variables provide for the in-place modification of values. Each i/o variable is from a logical point of view a pair of variables: one
input variable holding the old value and the output variable holding the new modified value. The implementation, of course, is st as in Pascal or C.
Since FormulaOne is a programming language firmly based on logic, there are certain restrictions on the use of the i/o variables which make the variables different from the Pascal or C variables. Consider, for instance, the following predicate declarations:
proc P7(x:.[0..3]->[0..3]->I) iff .... proc P8(x:.[0..3]->I) iff .....The procedure P7 takes an i/o matrix of integers and the procedure P8 takes an i/o vector of integers. The predicates are used in the following contexts:
proc P9(x:.[0..3]->[0..3]->I) iff x = [_,r2,_] & P7(x) & P8(r2) proc P10(x:.[0..3]->[0..3]->I) iff P7(x) & P8(x(l))The predicate P9 deconstructs the array x in a Prolog-like fashion, whereas the predicate uses Pascal-like indexing. The compiler of FormulaOne must assume that the procedure P7 will modify the array x. In order to preserve the logical reading of P9, the compiler must deconstruct the array x in its body by copying the second row of x to the implicitly declared i/o variable r2. This is necessary to preserve the value unchanged across the call to P7. Consequently, any changes in P8 to the row r2 cannot affect the value of the matrix x. On the other hand, by passing to the predicate P8 in the body of P10, the second row of x selected by the indexing x(l), we achieve the same effect as in Pascal. Only a pointer is passed; the changes to the row are done directly in the matrix x.
When you want to use (and modify) a component of an i/o structure, you should use Pascal-like deconstructors of indexing or field selection. In this way, you make sure that pointers to components of data structures are passed. Because of the considerations dictated by logic, the Prolog-like deconstruction of i/o variables always results in the copying of components.
If the Pascal-like selection from fixed-size i/o variables is used, the compiler of FormulaOne can generate efficient code. Fixed-size data structures are, for instance, fixed-size arrays of integers (or of other fixed-size arrays). See Heap Management for the definition of the term fixed-size.A word of caution is needed here. FormulaOne is a logic programming with an integrated procedural part which is reminiscent of Pascal. It would be easy to implement input/output variables in the same manner as Pascal or C. Unfortunately, this is unacceptable because things could happen to variables in the course of program execution which then violate the basic concepts of logic. These same side-effects or unintended effects are also the ones that give rise to bugs and plague programs. Certainly it is possible to have bugs in a FormulaOne program, but in general if your program will compile at all then you have few bugs left to find and they are much easier to ferret out than in older languages.
By sticking to logic we get better programs. There may be some loss of efficiency but usually FormulaOne makes up for that elsewhere. Also, any program that works is better than one that doesn't.The all keyword makes the formula into a simplified form of the all formula and thus makes it able to contain backtracking formulas. So the exact guidelines for deciding whether to put an all in front of your queries are:
A function is declared as a procedure. But for a given procedure to be a function, the last parameter must be of output mode, and all the others must be of input mode. So, for instance, the SumS procedure is a function, and so is the following version of the Fib predicate:
proc Fib5(index :< I, number :> I) iff
{The 'index'-th Fibonacci number is 'number'}
Fib_prev3(index, prev, number)
proc Fib_prev3(index :< I, prev :> I, fib :>I) iff
{'fib' is the 'index'-th Fibonacci number, and prev is the one before it}
if index <= 2 then
fib = 1 & prev = 1
else
Fib_prev3(index-1, befprev, prev) & fib = prev + befprev
end
Note that the Fib_prev3 predicate is not a function because it has two output arguments.
So if functions are just procedures, why do we care about them? Because we can refer to them in a much more compact and easy-to-read format. We can define the following predicate:
pred Largesum(ilist :< list I) iff
{the sum of 'ilist' is greater than 10}
Sum5(ilist) > 10
The expression Sum5(l) is here used as a term. This is functional notation: we are calling Sum5 with all its parameters except
the last one, and the value of the term is what the value of the last parameter would have been if it had been included. So the above
predicate definition is completely equivalent to the following:
pred Largesum1(ilist :< list I) iff
{the sum of 'ilist' is greater than 10}
Sum5(ilist, sum) & sum > 10
Functional notation is useful because we can make our programs more readable and compact with it (this is something that we consider
natural in languages like Pascal and C, but it's disallowed in Prologs). For instance, the final version of the procedure Sum can be
naturally coded as follows:
proc Sum6(l :< list I, sum :> I) iff
{the sum of the members of 'l' is 's'}
case l of
Nil => sum = 0;
(head, tail) => sum = head + Sum6(tail);
end
We usually write functions with the idea of using them as functions, and name them so that function calls read nicely. In the above
example, we can read the first definition of Largesum as "a list has a large sum if the sum of the list is greater than 10."
The second definition's reading is more complex, and slightly obscures its real meaning.
A function call can appear anywhere any other term can, including inside other function calls. The type of the function call term is the type of the last parameter which it stands for. So with Fib5 declared as a procedure, we can issue the following query:
x = Fib5(Fib5(Sum6((2,4,Nil))))The sum of the list is 6, the sixth Fibonacci number is 8, and the eighth Fibonacci number is 21; so we would expect the query to give us the answer x = 21.
Top
Control Structures
Building Types