Top Collecting Solutions with "all" Queries
French French German German ItalianItalian SpanishSpanish PortuguesePortuguese JapaneseJapanese KoreanKorean ChineseChinese

Miscellaneous Advanced Topics


Constant Declarations

You can associate a name with a certain constant value by putting a constant declaration at the start of your program, along with any type declarations you may have. Here are some examples: 
Maxnames :< I = 20 
Pi :< R = 3.14159
Princess :< P_data_t = ('Diana', Female, (1961, 7, 1),(0, 1, 1), 'Spencer')
Declared constants are objects whose value remains static throughout programs, so they are given capitalized name identifiers. The general form of a constant declaration is:

Name :< type = term

This declaration causes Name to act as a constant term whose value is term. The type of the new term is the given type; needless to say, the term must be of that type as well.
Constant declarations are useful for several purposes. If we want to refer to the same value several times in a program, but we think we might want to change it later, we can instead use a constant declaration which gives a name to the value. Then, if we do want to change it, we need only change the constant declaration. Constants are also used for giving a name which is more easily remembered to an important constant, such as Pi above. They also come in handy when giving a brief, concise name to a long tuple constant, as in the case of Princess above. The full syntax of a FormulaOne program (that is, the contents of a program module) is:

tcdecli
.
.
tcdecln
pdecli
.
.
pdeclm

where each tcdecli is a type or constant declaration, and each pdecli is a predicate declaration. FormulaOne permits declaration of constants, types and predicates to be given in any order, with the following restrictions:
In FormulaOne, the declarations of constants, types and predicates are processed before starting the compilation of predicate bodies. This allows for logical grouping of declarations. Declarations of constants and types used globally can be placed at the beginning of a module; constants and types used only in certain predicates can be declared later, before they are used in the predicates. For instance: 
Maxsize :< I = 100
Table = [0..Maxsize-l]->S

proc Tabulate(table :< Table,f:.Ascii) iff
    ...
    Actions = Delete | Add | Modify
    Mylist :< list S = 'Smith','Jones','Meredith',Nil

proc Crosstab(table :< Table, action:< Actions) iff
    Process(Mylist) &
    ...
proc Process(s :< list S) iff
    ...

The Anonymous Variable

The anonymous variable is the term which consists of a single underscore (_). It is like a variable which is new every time it is referred to, so that two occurrences of it do not refer to the same variable. It is used as a placeholder for terms which we want to match and then discard. Consider the procedure from earlier in the book: 
proc All_men(m :> list P_data_t) iff
    {'m' is the list of all men from the P_data file}
    all rec in m
        P_data(rec) & rec = (n, Male, b, d, c)
    end
We really don't care what the values of n, b, d, and c are in this procedure; we just put them there to take the place of the parts of the record. So we could re-code this procedure as: 
proc All_men1(m:>list P_data_t) iff
    {'m' is the list of all men from the P_data file} 
    all rec in m
        P_data(rec) & rec = (_, Male, _, _, _)
    end
The anonymous variables in the equation mean less overhead for the compiler in remembering variable names, and they also indicate clearly that we don't care what the values of those parts of rec are.

Scope of Variables

Variables in FormulaOne are always local variables. Not only may a variable be local to a particular predicate, but it may even be local to a particular part or structure in that predicate. Look at this example: 
pred ListLook(x :< list L]) iff
    x = (h,t) & Print(h)
    | x = Nil & h :> S & h = 'Nil' & Print(h)
This works because of the or ( | ). The compiler knows that the variables h on each side or branch of the or are different local variables. This is an interesting feature of FormulaOne, but it must be used with caution: the variables have meaning or scope only within the branch where they are defined. To attempt to reference h later in ListLook will result in an error because the compiler will not know which h is being referred to. Also, the duplicate definition of h would not be accepted if we had used & instead of |. This is prevented by the laws of logic. If we had used &, we would be saying that h must be defined as a long integer L and as a string S at the same time. Many local variables in FormulaOne have the property of being implicitly existentially quantified. An example which we encountered very early on was the Sum predicate in this line: 
Sum(tail,tailsum)
In plain English we can restate this as "there exists a variable tailsum such that Sum(tail,tailsum) is true". Quantifiers and quantification are topics of mathematical logic beyond the purpose of this text. However it is useful to be able to convert in your own mind from FormulaOne code to the natural language equivalent. When you encounter a variable like tailsum, realize that it has this implicit existential quantification which extends over its scope; that is, over the portion of the program wherever the variable is to be found.
Variables which are defined, explicitly or implicitly, within an all/one/min/max formula are local to that formula. From the point of view of mathematical logic, the arguments of predicates can be considered as universally quantified: 
pred Sum(l::list L,sum::L) iff
    ...
can be read as "for all variables which are lists of long integers and for all variables sum which are long integers, the predicate Sum is true if and only if the following conditions hold...".

The local Keyword

When we specify in FormulaOne that a module uses other modules, we (by default) give that module access to all the constant, type, and predicate declarations in the used modules. But sometimes this is not what we want. Occasionally we will want to hide all but a few declarations from modules that use a given module, so that the interface between modules is as small as possible.
The keyword local gives us the ability to do this hiding. Preceding a constant, type, or predicate declaration by local makes that declaration inaccessible from other modules, even modules which are specified as 'using' the declaration's module. For instance, say we wanted to put our Eratosthenes' Sieve algorithm in a module, say Sieve. We have three procedure declarations, Print_primes, Sift_print_from, and Multiples_marked. The only ones of these that it makes much sense for some other procedure to call is Print_primes. So it would be logical to put the declarations in Sieve this way: 
Number_type = Prime | Composite 
Sieve_type = [0..] -> Number_type

proc Print_primes(max :< I) iff
    ...
local proc Sift_print_from(sieve :. Sieve_type, first :< I, max :< I) iff
    ...
local proc Multiples_marked(sieve :. Sieve_type, prime :< I, multiple :< I ,max :< I) iff
    ...
Now, if any module uses Sieve, the only procedure it will be able to "see" will be Print_primes. If the using module refers to one of the local procedures, it will get an 'identifier undefined' error message. This means less overhead for the system when loading the Sieve module; less chance of error by a predicate mis-using the two auxiliary procedures; and an explicit description of which procedures are intended to be called from other modules. The local keyword also works for constant and type declarations. Some examples: 
local Pi :< R = 3.14159
local Number_type = Prime | Composite
local Date = (year:I, month:[1..12], day:[1..31])

Unnamed tuples

We have seen how tuple types normally have fields which can be accessed by field selection expressions (e.g., parent.b_date.month). But as well as these named tuples, there can also be unnamed tuples, which have no field names in them. These are more compact and convenient when you know you are always going to disassemble terms of that type by matching them with variable terms. 
Complex = (R, R)

proc Complex_product(x:<Complex, y:<Complex, prod:>Complex) iff
    x = (xre, xim) & y = (yre, yim) &
    prod = ( (xre*yre - xim*yim), (xre*yim + yre*xim) )
Unnamed tuples involve a little less overhead for the system. They are no less efficient to use, because the "disassembling" operations x = (xre, xim), for instance, is implemented by associating the variables xre and xim with the appropriate parts of the term x.

Injections, Relations, and Unknown Indices

Injection variables, relation variables, and the unknown index capability are features of FormulaOne which are important for complex constraint-satisfaction applications. They are fairly interdependent, and so will be illustrated together with some simple examples.
The examples are taken from the world of logic puzzles, of the kind found in crossword puzzle magazines. These puzzles are usually simple constraint-satisfaction problems. One such puzzle runs as follows. 
Four friends, including Tim, gathered at Tim's home on a Sunday afternoon to compare the Apple Macintosh and the IBM PC. From the clues that 
follow, determine each person's last name (one is Brown) and occupation (one is a teacher).
1. Two of Tim's guests were Ann and the doctor.
2. Jack, whose last name is not Blue, prefers the IBM PC. 
3. Ann is not the dentist.	
4. Grey, a keen Macintosh user, went home before the benchmarks were finished.
5. Jill and Green were both delighted when the Macintosh finished the last test before the PC.
6. The lawyer was the last person to go home.
7. Blue is not the doctor.
One brute-force solution to this problem would be to just generate all 4!*4!*4!= 13824 combinations of first name, last name, and occupation, and test them to see whether they meet all the conditions. This is what most Prolog implementations would have to do, unless some constraint-satisfaction code were written specifically for the problem. Here is a FormulaOne solution to the puzzle that makes use of injections and relations. 
First_t = Tim | Ann | Jack | Jill
Last_t = Green | Brown | Blue | Grey
Job_t = Doctor | Dentist | Lawyer | Teacher

Name_t = First_t ->> Last_t
Occ_t = Job_t ->> Last_t

pred Hackers(lastname::Name_t, occ::Occ_t) iff
    likesMac::rel Last_t & guest::rel Last_t &
    ~lastname(Tim) in guest &
    {1} lastname(Ann) in guest & occ(Doctor) in guest & lastname(Ann) <> occ(Doctor) &
    {2} lastname(Jack) <> Blue & ~lastname(Jack) in likesMac &
    {3} lastname(Ann) <> occ(Dentist) &
    {4} Grey in likesMac & Grey in guest &
    {5} lastname(Jill) in likesMac & Green in likesMac & 
        lastname(Jill) <> Green & Grey <> lastname(Jill) &
    {6} occ(Lawyer) in guest & occ(Lawyer) <> Grey &
    {7} Blue <> occ(Doctor)
We'll describe the new features used in this example in the sections below.

Injections

The first new feature you will notice is the use of a double arrow (->>) instead of a single arrow (->) in the declaration of Name_t and Occ_t. This double arrow signifies an injection type in the same way as a single arrow signifies an array type.
In mathematics, an injection is a function which never has the same value for two different sets of arguments. In FormulaOne, where arrays are like functions, an injection is an array in which no two elements are the same. Here are some more examples of injection types: 
ID_inj_t = [0..9] ->> I 
Reordering_t = [0..15] ->>[0..15]
An injection works just like an array which has had constraints put on it specifying that no two elements of it are equal to one another. So in the Hackers example predicate,the variable lastname, of type Name_t, is an array of last names, indexed by first names, in which no two of the last names are the same. When the system encounters further constraints on lastname, like 
lastname(Jack) <> Blue & lastname(Ann) <> occ(Doctor)
it puts additional constraints on the variables involved. If there were any equality constraints, like 
lastname(Jack) = Grey
then the fact that the other three elements of lastname could not be Grey would have been propagated through the injection. But even without any equality constraints, eventually there are so many things that a particular element of each injection cannot be that there is only one thing that each element can be.
FormulaOne handles the entire mechanism of propagating the constraints to fill each element of the injection with its appropriate value.

Relations

A predicate expresses the fact that some relation holds between several objects; a relation variable expresses the same kind of thing, and is accessed with a similar notation. The difference is that a predicate is fixed at compile time, whereas a relation variable is built during the execution of the program. In the Hackers example above, the declarations 
likesMac::rel Last_t & guest::rel Last_t
declare likesMac and guest to be relation variable. Once a variable has been declared to be a relation, you can assert that values of the element type of the relation (like Last_t) are either in or not in the relation. A constraint formula on guest, like ~ lastname(Tim) in guest, asserts that the variable lastname(Tim) is not in the relation guest. If later information comes along that, for instance, occ(Doctor) in guest, the system will automatically deduce that lastname(Tim) and occ(Doctor) are not the same; that is, that lastname(Tim) <> occ(Doctor).
The sole purpose of guest in this example is to propagate these inequality constraints through the original constraint ~ lastname(Tim) in guest. The likesMac variable is used in a similar way.
The effect of both of these relation variables could have been achieved with explicit inequality formulas, but the resultant code would not have been as clear. As it is, the relations, together with the injections, make the FormulaOne code an almost exact transcription of the original puzzle into logical notation. A relation variable never has a fixed value; it is represented completely by constraints. However, it may be useful to think of it as a list containing the elements asserted to be in it, and carrying constraints about the elements asserted not to be in it.

Unknown Indices

We'll illustrate the use of unknown indices with another logic puzzle example. It's a puzzle by R. L. Whipkey, taken from the Dell Champion Variety Puzzle magazine, May 1987. 
Islandtown, the main town on Cozy Island, is the crossroads for the island's four roads,
each of which goes in a different direction (north, south, east, west) to one of the four outlying Cozy Island villages.
Given this information and the clues, find each village's direction and distance from Islandtown, and the road that goes to
that village.
1. The village on Ocean Road is 1 mile farther from Islandtown than Summerport is.
2. The closest village is 2 miles from Islandtown; no two villages are the same distance from Islandtown.
3. Winterharbor is a total of 6 miles by road from the village on Island Road.
4. The town on Conch Road is a total of 9 miles by road from Autumnbeach.
5. Springcove is twice as far by road from Islandtown as the village west of the main town.
6. The village on Bay Road, which doesn't go west, is 4 miles from Islandtown.
7. The village south is twice as far from Islandtown as the village north.
The solution of this puzzle in FormulaOne is an elegant example of the use of long integer arithmetic constraints, injections, and the unknown index feature. 
Road    = Ocean_Road | Conch_Road | Bay_Road | Island_Road
Village = Winterharbor | Autumnbeach | Springcove | Summerport
Dir     = North | East | South | West

pred Island(dist :: Road->>L[2..], dir :: Dir->>Road, vill::Village->>Road) iff
    {1} dist(Ocean_Road) = dist(vill(Summerport)) + 1 &
    {3} dist(vill(Winterharbor)) + dist(Island_Road) = 6 &
    {4} dist(Conch_Road) + dist(vill(Autumnbeach)) = 9 &
    {5} dist(vill(Springcove)) = 2 * dist(dir(West)) &
    {6} Bay_Road <> dir(West) & dist(Bay_Road) = 4 &
    {7} dist(dir(South)) = 2 * dist(dir(North))
This may look like a straightforward example of a puzzle with arithmetic constraints and injections, but if you look more closely you'll see an interesting thing. The array element term vill(Summerport), although its value is as yet unknown, is itself being used as an index to the array dist. The same thing happens six more times in the course of the predicate. When you give an array or injection index which is itself a symbolic variable, its value may or may not be known at the time the system processes it. So FormulaOne essentially declares an auxiliary variable of the type of the indexed array term, and sets a constraint on the array that its element at the unknown index is equal to that new variable. For instance, take the formula 
dist(Ocean_Road) = dist(vill(Summerport)) + 1
This formula is equivalent to the formula 
dist(Ocean_Road) = aux + 1 & aux = dist(vill(Summerport))
Later, if it becomes known what dist(Ocean_Road) is, the value of aux will become known. That will have the effect of constraining vill(Summerport) to be, for instance, not equal to Ocean_road(otherwise aux would be equal to aux+1!). Similarly, if the value of vill(Summerport) becomes known, it may cause the value of aux to become known, and thus propagate back to the value of dist(Ocean_road).
In general, the beauty of constraints is that the system determines which way information will flow through the variables, and all you have to do as a programmer is to state the conditions of the problem. The reason this last example is not impressive on first glance is that it is so natural. But no current implementation of Prolog, for example, could solve this problem with anywhere near the readability of FormulaOne, without an exhaustive enumeration of the values of all the variables involved.

Construction and Deconstruction of Arrays, Tuples, Lists and Unions

Data structures such as arrays, n-tuples, lists, or unions are created by the use of constructors. For instance, assume the following type and variable declarations: 
A  = [0. .2]->I
B  = S,L
Bb = s:S,i:L
C  = list Bb
D  = E  | F(I,D,D)
Dd = Ee | Ff(i:I,l:Dd,r:Dd)
... a:>A & b:>Bb & c:>C & d:>D & dd:>Dd ...
The array a can be constructed either by an array constructor 
a = [5,6,7]
or by the duplication predicate: 
Dupl(3,4,a)
or 
a = Dupl(3,4)
The last two formulas are equivalent to: 
a = [4,4,4]
Both n-tuple types B and Bb are the same, the type Bb includes the field names. The pair b is constructed with the help of the pairing operator ',': 
b = 'Smith',56000
Comma is also used to construct lists: 
c  = b,('Jones',20000),Nil
Union values are constructed by using the union tags: 
d  = E
dd = Ff(6,Ee,Ee)
The types D and Dd are not recognized by FormulaOne as the same types. Data structures of FormulaOne can be broken down into their constituents by the use of deconstructors. FormulaOne offers two types of deconstructors: Prolog-like and Pascal-like. Prolog-like deconstructors are similar to the constructors but they use explicitly or implicitly declared output (symbolic) variables: 
a = [al,a2,a3]
The implicitly declared output variables al, a2, and a3 obtain as their values the corresponding elements of the array a. Arrays can be deconstructed also by a Pascal-like indexing. For instance a(0) = a1, a(1) = a2. The tuple b can be deconstructed either in the Prolog style: b = x,y or by the use of Pascal-like field selectors (provided that the tuple type, i.e. Bb in this case, contains named fields). We have b.i = y.
Deconstruction of lists and union values always generates a test to check whether a list is non-empty or whether a union value has the correct tag: 
c  = v,w
d  = F(_,_,_)
dd = Ff(i,p,q)
The list c is non-empty, so, after deconstruction, we have (v = b) 
v = 'Smith',56000
and 
w = ('Jones',20000),Nil
The tag of d is not F so the second deconstructor fails, the third one succeeds setting i = 6 and p = q = Ee. The standard field names h (for the head) and t (for the tail) can be used to deconstruct lists in a Pascal-like fashion. We have the following: 
c.h = v
c.t = w
c.t.h.s = 'Jones'
It is also possible to use the field names of components of lists directly, without the selectors h and t: 
c.i = c.h.i = v.i = 56000.
If the components of a union value are named we can deconstruct the value by selecting the component name in a Pascal-like fashion: 
dd.l = p = Ee.

Tail Recursion Elimination

FormulaOne is a language firmly based on logic. Like other declarative languages, FormulaOne does not contain explicit loop statements. Each loop has to be written as a recursive procedure. It is possible to optimize the recursion by placing the recursive call as the very last action before leaving the body of the procedure. Such recursive calls are called tail recursion. FormulaOne recognizes tail recursion in procedures (proc) and subroutines (subr), and generates a loop instead. This saves both space and time, as there are no stack frames to be allocated, and no arguments passed for the tail-recursive calls.
Consider the Pascal loop computing the factorial of n: 
fact := 1;
while n >= 1 do begin
    fact := n*fact;
    n := n - 1;
end
Note that the variable fact is used as an accumulator to store the partial results of the computation. This loop can be programmed with Pascal's efficiency in FormulaOne by a call to the tail-recursive procedure Fact: 
fact = Fact(n,l)
The tail-recursive procedure Fact is defined as follows: 
proc Fact(n :< L,ace :< L,fact :> I) iff
    if n >= 1 then
        Fact(n - 1, n*acc, fact)
    else
        fact = ace
    end
Note that the recursive call to Fact in its body is the last action performed in the body. Immediately after the return from the recursion the procedure exits.
The 'standard' recursive form of the factorial function as found in the textbooks is not tail-recursive: 
proc Fact(n :< L, fact :> L) iff
    if n >= 1 then
        fact = n*Fact(n-l) {i.e. Fact(n-l,aux) & fact = n*aux }
    else
        fact = 1
    end
This is because after the recursive call returns, the result must yet be computed by a multiplication. There is no tail recursion optimization performed for the predicates (pred). The following example illustrates the reasons for it: 
pred Maxlist(l::list [1..], max::I) iff
    l = Nil & max = 0
    | l = h,t & tmax::I & (tmax >= h & max = tmax | tmax < h & max = h) &
    Maxlist(t,tmax)
The predicate Maxlist finds the maximum of a symbolic list of positive integers. After the seemingly tail-recursive call to find the maximum of t returns, FormulaOne still has to make sure that there exists a value for the variable tmax such that the constraint tmax >= h or tmax < h holds. In logic this situation is called quantifier elimination. There is an implicit existential quantifier binding the variable tmax.
Note that because of constraints, FormulaOne is much more powerful than Prolog. In Prolog it is impossible to assert that tmax > = h when both of the variables are not instantiated. Consequently the implicit quantifiers in Prolog do not have to be eliminated and it is possible to perform tail recursion optimization on arbitrary predicates of Prolog.

Negation

FormulaOne has implemented a logically sound form of negation, called negation by failure. The formula ~A is computed by computing A. If A succeeds then ~A fails and vice-versa.
Negation by failure works as expected from the logical point of view only under certain restrictions on the formula which has been negated. The FormulaOne compiler must process the formula A in the procedure context and no situations which give rise to backtracking may occur within A. So, no true predicates can be called in A and symbolic variables cannot be used unless they are enclosed within an all/one/min/max formula.
Here is a very simple example of what would happen if a backtracking predicate were negated: 
pred OneThree (x :: I) iff
    x = l | x = 3
Logically speaking, these two queries are identical: 
~P(x) & x=2
x=2 & ~P(x)
and must yield the same result - but they don't.
In the first case P(x) succeeds in setting x to 1 and the formula fails because x cannot equal 1 and 2.
In the second case x is given the value 2, and P(2) is of course false so that ~P(x) succeeds and therefore the whole formula succeeds.
In a negated formula you are free to test or refer to input, output or i/o variables which are non-local to (i.e. defined outside of) the formula, but you may not modify them. You may enclose the formula which you are negating with parentheses to make it clear what the scope of the negation is. Within the scope of the negation you may define local variables as you wish. These variables are subject to the scope of variables, and their implicit existential quantification.
Take for instance the procedure Lookup looking up a salary of a specific person in a list of persons: 
Person = name:S, salary:L
    
proc Lookup(persons :< list Person,name :< S,salary :> L) iff
    persons = person,rest &
    if person.name = name then
        salary = person.salary
    else
        Lookup(rest,name,salary)
    end
The call : 
~Lookup(persons,'Smith',_)
which is the same as the call 
~Lookup(persons,'Smith', s)
with a local variable s, succeeds iff (if and only if) it is not the case that there is a salary s such that Lookup(persons,'Smith',s) holds, i.e. iff the name 'Smith' does not occur in the list persons.
In other words, the FormulaOne formula ~A with local variables x,...,z has the logical meaning of ~ exist x,...,z A. A legal FormulaOne formula ~A has the same meaning as the formula ~A of predicate logic only if the formula A does not contain any local variables.
As a result of the restrictions on the formulas within a negation operator, as well as because of the implicit existential quantification of local variables, the formula a <> b is not necessarily equivalent to the formula ~a = b.
For instance, if a were a symbolic variable the first formula is a constraint, whereas the second one is illegal.

More about if-then-else formulas

FormulaOne performs extensive checks in if-then-else constructs. The if-then-else formula if A then B else C end has the same meaning and the same restrictions as the formula 
A & B | ~A & C
The formula A is called the condition of the if formula. Since the conditions of if formulas are negated the same restrictions as with negations apply. Conditions are processed in the procedure context without backtracking. No symbolic variables and no assignments to non-local output and input/output variables are allowed within the conditions. Note that the if-then-else formulas can occur in a predicate, procedure, or subroutine context, and the formulas B and C are evaluated in the same context.
Under the restrictions on conditions, at most one branch of an if formula can hold. Once the condition A has succeeded the else branch cannot be satisfied. Thus the compiler of FormulaOne can generate efficient test and jump code for if-then-else formulas without a double evaluation of conditions and without backtracking. Note that the condition would be evaluated twice if we had used the or (|) form instead of the if-then-else formula. Once the condition A has succeeded there can be no backtrack to the else part. Hence FormulaOne can permit assignments to the non-local output and input/output variables in the formulas B and C. Actually without this it would be impossible to write procedures returning values: 
proc Fact(x :< L,y :> L) iff
    if x > 0 then
        y = 1
    else
        y = x*Fact(x-l)
    end
The output variable y is non-local to the if, yet the procedure cannot possibly backtrack. The following assignment to the variable s is also legal: 
if Lookup(persons,'Smith',s) then
    Print(s)
else
    Print('no such person')
end
The reason for this can be seen from the equivalent formula: 
Lookup(persons,'Smith',s) & Print(s) |
~Lookup(persons,'Smith',s) & Print('no such person')
Note that the assignment to s remains local both to the left argument of the or and to the negation. This kind of assignment is used to advantage in many search situations.
On the other hand, it is impossible to lookup a person in two lists either by the procedure 
proc P4(personsl :< list Person, persons2 :< list Person, s :> L) iff
    Lookup(personsl,'Smith',s) | Lookup(persons2,'Smith',s)
or by the procedure 
proc P4(personsl :< list Person, persons2 :< list Person, s :> L) iff
    if Lookup(personsl,'Smith',s) then
        true
    else
        Lookup(persons2,'Smith',s)
    end
Neither of these procedures is accepted by FormulaOne because of the non-local assignments to the output variable s which occurs within conditions. Such assignments generally call for a backtrack. Consider the logically true predicate call: 
P4((('Smith',45000),Nil),(('Smith',56000),Nil),56000)
The call is compiled as: 
P4((('Smith',45000),Nil),(('Smith',56000),Nil),s) & s = 56000
Backtracking is required in order for the formula to succeed. This is because the call returns s = 45000 which fails the test.
A backtrack is needed to search the second list. The situation can be corrected by turning the first procedure P4 to a backtracking predicate: 
pred P4(personsl :< list Person, persons2 :< list Person, s :> L) iff
    Lookup(personsl,'Smith',s) | Lookup(persons2,'Smith',s)
The second procedure P4 cannot be turned into a predicate because the conditions of the if-then-else formula are processed in the procedural mode without non-local assignments. Note that the seemingly equivalent procedure 
proc P4(personsl :< list Person, persons2 :< list Person, s :> L) iff
    if Lookup(personsl,'Smith',ss) then
        s = ss
    else
        Lookup(persons2,'Smith',s)
    end
is accepted by the compiler of FormulaOne as perfectly legal. This is because the variable ss is local to the first branch of if. Non-local assignments to the variable s occur in situations after the condition has been either positively or negatively evaluated and there is no possibility of backtracking.
However, the meaning of this procedure is not the same as the meaning of the first version of P4. The difference is subtle and lies in the implicit existential quantification of the local variable ss. The body of the last procedure is equivalent to the formula 
Lookup(personsl,'Smith',ss) & s = ss |
~Lookup(personsl,'Smith',ss) & Lookup(persons2,'Smith',s)
The call 
P4((('Smith',45000),Nil),(('Smith',56000),Nil),s) & s = 56000
cannot succeed because the Smith in the first list does not make 56000, and the branch searching the second list cannot succeed because the formula ~Lookup(personsl,'Smith',ss) is false, i.e. there is a Smith in the first list.
The meaning of more complex if-then-else formulas reduces to the above general case. The formula 
if A then B end
has the same meaning as the formula 
if A then B else true end
or as the formula 
A & B | ~A
The formula 
if A then
    B
elsif C then
    D
else
    E
end
has the same meaning as the formula 
if A then
    B
else
    if C then
        D
    else
        E
    end
end
or as the formula 
A & B | ~A & (C & D | ~C & E)

Opening and Closing of Files

Ascii, Bin as well as FormulaOne's database files are opened and closed automatically without any explicit action on the part of the programmer. A file can be opened only in the subroutine context of a query or within a subroutine. This restriction is necessary from the point of view of logic because the mapping of a file name to the physical location of the file requires a hidden environment argument describing the current state of the file system of an OS.
A FormulaOne database file is automatically opened whenever its filename is converted to an input/output file argument. Consider the procedure Printfile which reads and prints a file: 
proc Printfile(f:.Ascii) iff
    if DbAccess(f,s) then
        Print(s,'\n') & DbSkip(f,1) & Printfile(f)
    else
        Print ('---- EOF -----')
    end
Let us assume that the file Myfile is to be of type Ascii. The query Printfile(Myfile) automatically opens the file Myfile before the file is passed to the procedure Printfile for the printing.
The file names of Ascii and Bin files are specified by strings (S). The query 
Printfile('sys\\textfile.doc')
prints the Ascii file textfile.doc in the directory sys. The compiler inserts automatically the conversion from a string constant to the file typed argument. If the file name is given by a variable of type S then an explicit cast to the type Ascii is required: 
subr Printfiles(fs :< list S) iff
    if fs = f,fs2 then
        Print('-------- ',f,' ---------\n') &
        Printfile(f:Ascii) & Printfiles(fs2)
    end
The subroutine Printfiles prints the contents of the Ascii files specified by a list of strings as the argument. The compiler of FormulaOne automatically inserts a call in the body of Printfiles to open and close the Ascii file: 
{open the file f} Printfile(f:Ascii) {close the file f}
Note that the conversion between a file name and a file typed value always means the insertion of the opening and closing code. In the following query the file text.txt is opened twice: 
f = 'text.txt' & Printfile(f:Ascii) & Printfile(f:Ascii)
The query 
Printfile2('text.txt')
calling the subroutine Printfile2 should be used instead: 
subr Printfile2(f:.Ascii) iff
    Printfile(f) & Printfile(f)

Cross Modular Consistency Checks

FormulaOne can automatically detects changes made to the modules and files which could render other modules using the changed modules inexecutable. This automatic cross-modular checking is a sophisticated version of the utility known as MAKE in the C-based environments.
A module is said to export all non-local constants, types, and predicates defined in it. These are collected in the so called export list, sometimes referred to as a symbol table. The information from an export list can be generated into the code of modules using the given module. When the export list of a module is changed the object code of modules using this module might become invalid.
FormulaOne automatically disables the execution of all modules compiled before a used module changes its export list. If the changes to the export list were not extensive it might be enough just to recompile all modules using the changed module. If, for instance, a parameter to a predicate changed its type, all modules using the changed module must be manually modified before they can be recompiled. FormulaOne keeps a time stamp with symbol table. The time stamp records the time of the last change to the export list. The automatic cross-modular consistency checks refer to the time stamps. For this reason it is essential that your computer system clock is always set with the current date and time.

Heap Management

During the execution of programs in symbolic languages like FormulaOne, Prolog, or Lisp, data structures are created dynamically on the heap. It is impossible to predict the pattern of heap allocation during the compile time. Consequently, there should be a mechanism for dynamically removing the unused data structures from the heap, once the heap is exhausted. This is called garbage collection. In logic programming languages such as Prolog and FormulaOne it is relatively easy to manage the heap allocation when a predicate backtracks (there are ors in the program). When a Prolog predicate is deterministic, or when we have a procedure or a subroutine in FormulaOne, there is no backtracking and the heap can quickly overflow.

All implementations of Prolog (except Turbo-Prolog) use the so-called tagged architecture for the data structures. This means that every object manipulated by the interpreter (even a simple integer) must be supplemented by a tag giving the type of object. Tagged architecture slows down the execution of programs because the run-time system must constantly test the tags. On the other hand the tagged architecture makes it easy to implement garbage collectors.

Turbo-Prolog and FormulaOne are typed languages and there are no run-time tags on the data structures. Turbo Prolog has no garbage collector.
FormulaOne has a simple yet surprisingly powerful scheme for the garbage collection of the heap. The heap in FormulaOne is cleared automatically whenever a procedure or subroutine returns without passing (through its arguments) to its caller objects allocated to the heap during the execution of the procedure call. The procedures and predicates called during the processing of this call can allocate objects on the heap, but since the heap-allocated objects cannot be passed up it is possible to cut the heap to the state it was in the moment of the procedure call.
The automatic heap cut occurs when a procedure or a subroutine observes the following restrictions to its arguments:
An argument is of a fixed size whenever it is of

External Modules

Sometimes it is necessary to invoke a subroutine written in a language other than FormulaOne. The FormulaOne compiler creates modules, which are essentially DLLs. It is possible to use DLLs created by other third party tools; we refer to these as external DLLs; or external modules. However, these DLLs do not contain all the information necessary for the FormulaOne compiler to use them correctly. In particular, the number of arguments, their types and the calling convention are necessary to correctly call the external API. This information is provided in FormulaOne source code as part of the external API; declaration:

proc ExtName({ arguments }) iff external [_cdecl |_stdcall] 'dllname':'procname'

subr ExtName({ arguments }) iff external [_cdecl |_stdcall] 'dllname':'procname'

The actual code for the external APIs does not reside in the FormulaOne module itself but in the in the external DLL. All calls to the external module are forwarded to this module. A few notes:

Example:

Create and call an external API returning the current system time.

FormulaOne code:

Time = hour:[0..23],minute:[0..60],second:[0..60],millisecond:[0..1000]

subr PrintTime() iff TimeGetTime(t) & Print('TimeGetTime returned: ',t)

subr TimeGetTime(t:>Time) iff external _cdecl 'extf1.dll':'GetTime'

External module ‘extf1.dll’ code:

#include <windows.h>

typedef struct
    {
    int hour;
    int minute;
    int second;
    int millisecond;
    } TIMEST,*TIMEPT; 

__declspec(dllexport) int __cdecl GetTime(TIMEPT *timept)
    {
    static TIMEST timest;
    SYSTEMTIME SystemTime;

    GetLocalTime(&SystemTime);

    timest.hour = SystemTime.wHour;
    timest.minute = SystemTime.wMinute;
    timest.second = SystemTime.wSecond;
    timest.millisecond = SystemTime.wMilliseconds;

    *timept = &timest;
    return TRUE;
    }


Top Collecting Solutions with "all" Queries