Home   Downloads   Sample Code   Screenshots   Getting Started   FAQ   Support   RSS feed

French French German German ItalianItalian SpanishSpanish PortuguesePortuguese JapaneseJapanese KoreanKorean ChineseChinese

FormulaOne Programmer's Manual

This file documents the use of the Formula One compiler.
Copyright © 2003, 2004, 2005, 2006, 2007, 2008, 2009 K2 Software Corp.

About This Document
What Is Formula One
FormulaOne and Other Languages

Formulas and Queries

Data Types


Control Structures

Procedures, Subroutines and Functions

Building Types

Database Files

Collecting Solutions with "all"

Miscellaneous Advanced Topics


FormulaOne Language Definition

BNF Syntax of FormulaOne

Type Conversion

Mode Coercion

Runtime Library

About This Document

This file documents the use of the FormulaOne compiler. The screenshots in this document are based on the FormulaOne Release 40 IDE (Integrated Development Environment). Other releases may have different look and feel and a different method of invoking queries. This should be rather irrelevent, as this document focuses on the programming language itself. Installation of the FormulaOne Compiler Release 40 also installs the Tutorial project with the module called Tutorial. It contains most of the predicates discussed in this manual. 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. Once the module is compiled it can be used by various queries without a recompilation, unless, of course, it has been modified.


FormulaOne a language which integrates procedural, declarative and database programming into one highly efficient language.
Since the early 1980's micro-computers have won an important place in science, education, entertainment and industry. Procedural programming, which details how computing is performed, has lighten the drudgery of repetitive calculation for many people. However, procedural programming shows weakness when faced with problems concerning logic, reasoning or the evaluation of complex data relations. One answer to this impasse is declarative programming, which lies at the very heart of AI (artificial intelligence). Using this approach, the relation between information and objects is the matter of scrutiny and many of the programming details can be left to the compiler. With declarative programming, the inference engine organizes information and then finds a way to logically interpret or process that information, when queried with respect to a given problem. Expert systems place exceptional demands on such information processing, and great programming effort must be expended to meet the challenge when using procedural languages such as C, Fortran or Pascal. On the other hand, declarative languages such as Prolog and FormulaOne (which are very high-level languages) have the needed tools built into their inferences engines. At the start of the 1990's it is apparent that new development in computer languages has lagged behind hardware development.
The transition to declarative programming may still be lengthy for the software industry. Certainly for the individual, time is required to switch over to new languages and to learn the new styles, philosophies and techniques they require. Complex and flexible applications will require both declarative and procedural programming. Prolog is the widest known of declarative languages but it suffers from the flaw of lacking procedural and program control features and must simulate them. FormulaOne has overcome this stumbling block and has elegantly integrated both programming philosophies into one unit.

FormulaOne can be learned by a beginner but will be most appreciated by experienced programmers. If you are a problem solver, FormulaOne's truly unique implementation of constraints will be invaluable. Constraints enable numeric problems to be solved more rapidly, by orders of magnitude - in real time. And they work readily with FormulaOne's highly structured and modular nature to produce better code. "Better" code means more readable, more error-free and easier to maintain and change. This is another reason why FormulaOne is superior to any other declarative programming language.

What Is FormulaOne?

FormulaOne is a computer programming language, but it's also a complete programming environment that gives programmers the ability to efficiently develop, test and run their programs. At the heart of FormulaOne is the language itself, which can be viewed as a successor to the procedural language of the third generation Pascal, extended to cover the paradigms of database languages (fourth generation) and logic languages (fifth generation).
FormulaOne has the readability and efficiency of third-generation languages like BASIC, C, and Pascal, and the database update and query capabilities of fourth-generation systems. These features are all brought together by the powers of symbolic computing and logic programming with backtracking search - the same power as in fifth-generation languages like Prolog. Along with the FormulaOne language comes a complete visually oriented IDE environment. In the FormulaOne system, users can edit, compile, and run programs; build, query, and update database files; and create interlocking structures of program modules and databases of any desired complexity.

FormulaOne and Other Languages

FormulaOne is a new programming language, so it's useful to compare and contrast it to other popular programming languages. The foundations of FormulaOne are most like those of Prolog. Both languages:
Both FormulaOne and Pascal:
But the type structure of FormulaOne is more like that of C than the loose structure of most prologs or the rigid one of Pascal. In FormulaOne, you can build arrays, structures, lists, and unions which are implemented as efficiently as they are in C. And as in C, terms of one type can be recast into terms of another type, when possible. FormulaOne also has many advanced features which are not found in either Prolog, Pascal or C. These include:
In addition to all this, FormulaOne is firmly grounded in its underlying logic. Instead of the non-declarative, extra logical features of Prolog, like "cut", there are features like "if" which are more powerful, readable, and logically valid. There is not a single extra logical feature in FormulaOne.

Formulas and Queries

FormulaOne is different from other programming languages, and systems, in many ways. In well-known languages like Basic and Pascal, we order the computer to perform some task for us, and watch the results. In FormulaOne, we ask the computer questions and get responses.
The basic unit of programming in FormulaOne is the formula. A formula is a statement about the world, phrased in a language similar to mathematical logic. When we enter a formula into the query window of the FormulaOne system, it is interpreted as a query; the system will respond by stating whether the query is true, or by stating the conditions under which it's true.

Simple Arithmetic Queries

The simplest example of a query formula is an arithmetic statement. When we say 2 + 2 = 4 or x = 3, we are making a statement about the numbers and variables involved. In general, a formula is a statement, which says something about objects (like numbers), variables, and the relationships they hold to one another.
When we type in an arithmetic formula as a query to FormulaOne, we are asking it to tell us whether the formula is true or false, according to what it knows about arithmetic. For instance, you can ask FormulaOne whether 2 + 2 = 4 by the following steps:
Note: Newer compilers can determine an expression to be true or false at compile time and subsequently issue a corresponding warning. Additionally, newer compilers can also treat warnings as errors. If this happens, go to "Project->Settings" and uncheck "Treat warnings as errors".

The result will be displayed in the window:

that is, FormulaOne believes it to be true, which is of course correct. Now try to run 2 + 2 = 5 query instead, it will give us Failure result instead of Success. After the Success, or Failure comes some statistics on how long the query took to run.
FormulaOne can tell you whether an arithmetic formula is true or not. But more importantly, if you pose a query containing variables, FormulaOne will try to find values for those variables which will make the query true, and will report to you what those values are. Consider the following example:

The phrase all res indicates to the system that we want to see all the solutions for the unknown variable we are calling. res::L is a variable declaration; we can consider it to mean res is a number. The & symbol means and. So the full meaning of this query is "show all values for res such that res is a number equal to (3 + 33) multiplied by (4 + 44)".
Instead of indicating Success or Failure for this query, FormulaOne will give you a solution that looks like following:

FormulaOne has found one solution to the query, one value for res which will make the query formula true. That value is 1728, (3 + 33) * (4 + 44).
Actually, you would get the same result even if you omitted everything in the query up to and including the &. The complete set of circumstances in which you can do this will be explained later. For now, we will precede all our queries containing unknown variables with an all phrase and a variable declaration.
Now let's consider a slightly more complex example.

This query has a new symbol, |, which means or. Translation into English of this query is "show all values for x and y meeting the condition that x and y are numbers, x is equal to either 4 or 5, and y is equal to 64 + x". You can see for yourself that this query has more than one solution, and that the solutions will involve both variables. FormulaOne has found two combinations of values for the variables, and each combination satisfies the formula. If we had said all x instead of all x,y, we would have gotten only the solutions for x, and similarly for y. If we had said simply all, omitting the list of variables entirely, it would have defaulted to all variables; that is, the same thing as all x,y.
It's worth noting here that the same solutions would have been found to the above query if we had said (x > 3 & x < 6) instead of (x = 4 | x = 5). FormulaOne has considerably more knowledge of arithmetic, than every other widely-used programming language, including all current Prolog implementations. It can use this knowledge to figure out that the first formula has the same effect as the second.

Here are some more examples of arithmetic queries that you can try out:
6*9 = 42
all sec sec::L & sec = 60 * 60 * 24
all f f::L & f-32 = (20 * 9)/5

We can put FormulaOne's knowledge of arithmetic to good use in solving problems of arithmetic which humans can't solve easily. Consider the following puzzle.

Some spiders and some beetles are in a box. The box contains forty-six legs. How many spiders and how many beetles are in the box?

Since we know that spiders have eight legs and beetles have six legs, we can make a first stab at the puzzle by posing the query:

all s, b s::L & b::L & 8*s + 6*b = 46
We are using s and b to stand for the number of spiders and the number of beetles, respectively, so 8*s + 6*b must be equal to 46. It seems that it should work; but when we issue this as a query, the system pops up the following error message:

This corresponds to a very large number of solutions (more than 1G).

There are an infinite number of values for s and b because the way we declared them, they can have either positive or negative numbers as their values. So because there can't be a negative number of either spiders or beetles, and the problem indicates that there is at least one of each in the box, we can add a restriction:
all s::L & b::L & s > 0 &  b > 0 & 8*s + 6*b = 46
And now we get the results we wanted, as shown

A brief check will show that these are all the combinations of spiders and beetles that will give forty-six legs in the box. Note the section of the results screen which states Number of backtracks: 0. This phrase means that FormulaOne has found these solutions not by trying all possible alternatives, as all current Prolog implementations would have done, but by applying a decision procedure for solving arithmetic queries. This decision procedure avoids having to test the many possible solutions which fail to satisfy the formula.

Some Formal Definitions

Let's look a little more formally at the syntax of simple arithmetic formulas and queries in FormulaOne. This is just a small subset of the whole FormulaOne language. The rest of this tutorial will be concerned largely with what the "other things", terms, formulas, and queries can be. A complete and comprehensive description of the language can be found in the Programmer's Manual section.

"How It Does It"

We can trust FormulaOne to solve arithmetic queries correctly without needing to know how it manages to solve them. But when we write programs, we will have to know more about this, in order to predict the course of events in our programs. The way it actually solves a query is very complex, but this section will give a simplified version of the process that will be all that's needed to understand it.
We'll describe the process using a fairly simple example:
all x  x::L & (x<4 | x>6) & x = 10 
We'll explain how other kinds of formulas are handled as we get to them.
We can think of FormulaOne as having a query pointer which points to the current position in the query that it is considering. The query pointer will be denoted below by the symbol (DownArr). The system will advance the query pointer through the formula, building up an environment which contains the information it has so far about the values of variables. Occasionally, it will set up backtrack points (o) which it will return to if it encounters inconsistencies. Each backtrack point will be associated with a skip point later in the query. When the system gets to the end of the query without getting any inconsistent information about the values of variables, it will try to print a solution.
  1. The first thing the system will do is to store the fact that the user is requesting values of x with the expression all x. Then it will start the processing of the main part of the query, with an empty environment, the query pointer at the start of the query formula, and no backtrack or skip points set up.
    x::L & (x<4 | x>6) & x = 10 & (Env: empty)
  2. The query pointer will be advanced through the first formula, with the information that x is a number being stored in the environment. The next formula the system encounters will be an or (|) formula; it will set up a backtrack point at the or, and a skip point after the second part of the formula. It will then advance the pointer to the first part of the formula.
    x::L & ( x<4 | x>6 ) & x = 10 & (Env: x::L)
  3. The pointer will be advanced through x<4, with that information going to the environment. When the pointer reaches the backtrack point, it will skip over to the skip point. The system is following the rationale that if 'A or B' is true, we can first assume A, and then come back to B later.
    x::L & ( x<4 | x>6 ) & x = 10 & (Env: x<4)
  4. Now the system encounters an inconsistency. It knows from the environment that it has assumed x<4, but now it faces the information that x = 10 as well. This is an inconsistency; a failure occurs, causing a backtrack operation. The system moves the pointer to the last backtrack point set up. As it does this, it removes the backtrack point, its associated skip point, and all information that it put into the environment since the backtrack point was set up. The system is essentially saying 'Assuming x<4 didn't work after all, so let's try assuming x>6.
    x::L & ( x<4 | x>6 ) & x =10 & (Env: x<4)
  5. Now, the system can advance the pointer through the rest of the query to the end, without setting up backtrack points or encountering inconsistencies. When it reaches the end, it will print out the value of x taken from its environment (as requested by the all clause at the start of the query).
    x::L & ( x<4 | x>6 ) & x = 10 & (Env: x=10)
There are no backtrack points set up at the time the pointer reaches the end of the query, so processing ends there. However, if some backtrack point had remained, the system would have made a backtrack after printing the solution, to see if there were more possible solution. It would have kept on doing backtracks after finding solutions until no backtrack points remained. Figure 2.5 shows the result of this query. Note the Number of fails statistic, which lists the number of times the system had to make a backtrack due to a failure (in this case, one, the failure noted in point 4 above). This statistic is a good measure of how complex the query was to solve. All of our previous examples have had 0 fails, so they have not been very complicated by FormulaOne standards.

Queries with explicit or-s in them will always cause backtrack points to be set up. But implicit backtracks can also occur; for instance, in the query
all x  x::L & x > 10 & x < 20
the variable x does not have a single value by the end of the query, so the system enumerates all the possible values between the bounds that it knows. It should give each integer between 11 and 19 inclusive as possible solutions.

Another example of implicit backtracking is the 'spiders and beetles' query from earlier mentioned earlier. There, the decision procedure for integers caused a single backtrack to occur which caught the other solution to the puzzle. That particular example is too complex to go into, but you should be able to trace through all the other examples without too much trouble.

The Print Formula

The Print formula is a useful tool for tracing the execution of queries, and doing simple output to the screen. A formula of the form Print('xxxx'), where xxxx is any text, can be used anywhere any other formula can. (In fact, Print is just a predefined predicate in FormulaOne) When the FormulaOne query pointer is advanced to such a formula, it has the effect of just printing out the text within the two single quotation marks. For instance, the query
will just cause FormulaOne to print the line ABC in the results window, followed by Success. The query
Print('A') & Print('BC')
would have exactly the same effect, since the Print formula does not put any space between successive printed text. Other things besides quoted strings can appear as arguments to Print (the things inside the parentheses). Any term can be an argument, causing its value to be printed; and if the special term '\n' is printed, it causes a carriage return.

So the query
Print('ABC\n') & Print((3 + 33) * (4 + 44))
would cause the output

Print arguments can also be strung together within the parentheses, if they are separated by commas. So the query
Print('ABC','\n',(3 + 33) * (4 + 44))
would have exactly the same effect as the query above.

Print can be used effectively in helping us follow the course of computation of a formula. Any backtrack that causes a Print to be re-evaluated will cause the text in it to be printed again. We can insert a Print formula into our extended example above:
all x  x::L & (x < 4 | x > 6) & Print('Here\n') & x = 10
Then the output of the query will look like

As an exercise, you might want to trace through the execution of this query just to see that the result above makes sense.


Locations of visitors to this page

Valid HTML 4.01! Valid CSS!

Last updated: October 4, 2009