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:
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 ...
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) endWe 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, _, _, _) endThe 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.
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.
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...".
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])
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.
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.
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) = Greythen 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.
likesMac::rel Last_t & guest::rel Last_tdeclare 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).
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)) + 1This 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).
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',56000Comma is also used to construct lists:
c = b,('Jones',20000),NilUnion 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.
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',56000and
w = ('Jones',20000),NilThe 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.
fact := 1; while n >= 1 do begin fact := n*fact; n := n - 1; endNote 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 endNote 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.
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 endThis 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.
pred OneThree (x :: I) iff x = l | x = 3Logically speaking, these two queries are identical:
~P(x) & x=2 x=2 & ~P(x)and must yield the same result - but they don't.
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) endThe 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.
A & B | ~A & CThe 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.
proc Fact(x :< L,y :> L) iff if x > 0 then y = 1 else y = x*Fact(x-l) endThe 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') endThe 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.
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) endNeither 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 = 56000Backtracking is required in order for the formula to succeed. This is because the call returns s = 45000 which fails the test.
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) endis 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.
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 = 56000cannot 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.
if A then B endhas the same meaning as the formula
if A then B else true endor as the formula
A & B | ~AThe formula
if A then B elsif C then D else E endhas the same meaning as the formula
if A then B else if C then D else E end endor as the formula
A & B | ~A & (C & D | ~C & E)
proc Printfile(f:.Ascii) iff if DbAccess(f,s) then Print(s,'\n') & DbSkip(f,1) & Printfile(f) else Print ('---- EOF -----') endLet 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.
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) endThe 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)
Most implementations of 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.
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.
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 = ×t; return TRUE; }