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

Procedures, Subroutines and Functions

Usually there is a trade off between logic programming languages and other programming languages. If you use logic programming, you get the power of built-in backtracking search and symbolic variables, but the programs you write are not very efficient. If you use conventional languages such as Pascal or Basic, the programs are very efficient, but you have very limited search and symbolic capabilities.
One very important aspects of FormulaOne is that it gives you the power of logic programming yet allows you to write predicates and programs which are compiled with the efficiency of conventional programs.

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.

Predicate Classes

A predicate can be declared with either the proc or subr keyword in the place of pred keyword. Each of these keywords asserts that the predicate is in a different class of predicate, the three classes being pred (true predicate), proc (procedure) and subr (subroutine).

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 

Only true predicates can do backtracking through symbolic variables and or-s but only procedures and subroutines can have input/output (I/O) variables.

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.


The major source of power in logic programs is the backtracking mechanism. But sometimes this can also be a source of inefficiency. To control backtrack, a logic program has to keep a lot of data around concerning where the next backtrack location is, what the old values of variables were, and so on. When you declare a predicate to be an FormulaOne procedure, you are asserting that it is never going to backtrack. (This is what's called a "deterministic predicate" in Prolog terminology.)

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;

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)
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.

The following procedure would not compile, because the input/output variable has had its value modified to 2 in the left argument of the or:
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.


A subroutine is a special kind of procedure which can access data external to the FormulaOne environment, such as input from the user or the computer's date and time. In fact, the only reason we would declare something to be a subroutine rather than a procedure is to access this kind of data through the existing system-defined subroutines.

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:
(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.

Input/Output Mode

Now that we have covered procedures and subroutines, we can discuss the fourth and last variable mode. This is input/output mode. An input/output (i/o) mode variable is like a simple input or output variable in that no constraints are ever recorded for it, just its value. But unlike input and output variables, i/o variables can have their values reassigned. Consider the following version of our Sum procedure.
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);
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);
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.

For instance, given the procedure Incr
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') 

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
    end &
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.

Queries Revisited

Up to now, we have been using the all keyword at the beginnings of queries, followed by an optional list of variables. In fact, the all clause is sometimes not necessary, and sometimes unusable. A query is executed as if it were a formula which is the body of a predicate. By default, the predicate whose body it is, is of class subr, and so cannot do any of the things listed in section 7.2; however, it can call subroutines and use i/o variables.

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:


In mathematics, a function is an object which maps a set of parameters onto a single, uniquely-determined value. In FormulaOne, a function is much the same thing: a procedure which determines one parameter from several others, without backtracking.

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
        Fib_prev3(index-1, befprev, prev) & fib = prev + befprev
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);
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