Tables and Rules

5.1 Tables

Named arrays, called tables, can be defined in claire with the following syntax:

<name>[var:(<integer> .. <integer>)] : <type> := <expression(var)>

The <type> is the range of the table and <expression> is an expression that is used to fill the table. This expression may either be a constant or a function of the variables of the table (i.e., an expression in which the variables appear). If the expression is a constant, it is implicitly considered as a default value, the domain of the table may thus be infinite. If the default expression is a function, then the table is filled when it is created, so the domain needs to be finite. When one wants to represent incomplete information, one should fill this spot with the value unknown. For instance, we can define

square[x:(0 .. 20)] : integer := (x * x)

Notice that the compounded expression x * x is put inside parenthesis because grammar requires a « closed » expression, as for a method (cf. Appendix A). Tables can be accessed through square brackets and can be modified with assignment expressions like for local variables.

square[1], square[2] := 4, square[4] :+ 5,

Tables have been extended in claire by allowing the use of any type instead of an integer interval for their domain. They are thus useful to model relations, when the domain of a relation is more complex than a class (in which case a slot should rather be used to model the relation). The syntax for defining such a table (i.e., an associative array) is, therefore,

<table> º <name>[var:<type>] : <type> := <expression(var)>

This is a way to represent many sorts of complex relations and use them as we would with arrays. Here are some examples.

creator[x:class] : string := "who created that class"

maximum[x:set[0 .. 10]] : integer := (if x min(x,> @ integer) else 0)

color[x:{car,house,table}] : colors := unknown

We can also define two-dimensional arrays such as

distance[x:tuple(city,city)] : integer := 0

cost[x:tuple(1 .. 10, 1 .. 10)] : integer := 0

The proper way to use such a table is distance[list(denver,miami)] but claire also supports distance[denver,miami]. claire also supports a more straightforward declaration such as :

cost[x:(1 .. 10), y:(1 .. 10)] : integer := 0

As for properties, tables can have an explicit inverse, which is either a property or a table. Notice that this implies that the inverse of a property can be set to a table. However, inverses should only be used for one-dimension array. Thus the inverse management is not carried if the special two-dimension update forms such as « cost[x,y] := 0 » are used.

5.2 Rules

A rule in claire is made by associating an event condition to an expression. The rule is attached to a set of free variables of given types: each time that an event that matches the condition becomes occurs for a given binding of the variables (i.e., association of one value to each variable), the expression will be evaluated with this binding. The interest of rules is to attach an expression not to a functional call (as with methods) but to an event, with a binding that is more flexible (many rules can be combined for one event) and more incremental.

Definition: A rule is an object that binds a condition to an action, called its conclusion. Each time the condition becomes true for a set of objects because of a new event, the conclusion is executed. The condition is expressed as a logic formula on one or more free variables that represent objects to which the rule applies. The conclusion is a CLAIRE expression that uses the same free variables. An event is an update on these objects, either the change of a slot or a table value, or the instantiation of a class. A rulecondition is checked if and only if an event has occurred.

A novelty in CLAIRE 3.0 is the introduction of event logic. There are two events that can be matched precisely: the update of a slot or a table, and the instantiation of a class. CLAIRE 3.2 use expressions called event pattern to specify which kind of events the rule is associated with. For instance, the expression x.r := y is an event expression that says both that x.r = y and that the last event is actually the update of x.r from a previous value. More precisely, here are the events that are supported:

· x.r := y, where r is a slot of x.

· a[x] := y, where a is a table.

· x.r :add y, where r is a multi-valued slot of x (with range bag).

· a[x] :add y, where a is a multi-valued table.

Note that an update of the type x.r :delete y (resp. a[x] :delete y), where r is a slot of x (resp. a is a table), will never be considered as an event if r is multi-valued. However, one can always replace this declaration by x.r := delete(x.r, y) which is an event, but which costs a memory allocation for the creation of the new x.r.

In addition, a new event pattern was introduced in CLAIRE 3.0 to capture the transition from an old to a new value. This is achieved with the expression x.r := (z -> y) which says that the last event is the update of x.r from z to y. For instance, here is the event expression that states that x.salary crossed the 100000 limit:

x.salary := (y -> z) & y < 100000 & z >= 100000

In CLAIRE 3.2 we introduced the notion of a “pure” event. If a property p has no restrictions, then p(x,y) represents a virtual call to p with parameters x and y. This event may be used in a rule in a way similar to x.p := y, with the difference that it does not correspond to an update. We saw an example in the Sudoku example of our Section 1 tutorial. Virtual events are very generic since one of the parameter may be arbitrarily complex (a list, a set, a tuple …). The event filter associated to a virtual event is simply the expression “p(x,y)”. To create such an event, one simply calls p(x,y), once a rule using such an event has been defined. As a matter of fact, the definition of a rule using p(x,y) as an event pattern will provoke the creation of a generic method p that creates the event.

Virtual event may be used for many purposes. The creation of a virtual event requires neither time nor memory; thus, it is a convenient technique to capture state transition in your object system. For instance, we can create an event signaling the instantiation of a class as follows:

instantiation :: property(domain = myClass, range = string)

[close(x:MyClass) : MyClass -> instantiation(x,date!(1)), x ]

controlRule() :: rule( instantiation(x,s)

=> printf(“--- create ~S at ~A \n”,x,s))

To define a rule, we must indeed define:

- a condition, which is the combination of an event pattern and a CLAIRE Boolean expression using the same variables

- a conclusion that is preceded by =>.

Here is a classical transitive closure example:

r1() :: rule(

x.friends :add y

=> for z in y.friend x.friends :add z )

Rules are named (for easier debugging) and can use any claire expression as a conclusion, using the event parameters as variables. Rule triggering can be traced using trace(if_write), as shown in Appendix C. Notice that a rule definition in CLAIRE 3.2 has no parameters; rules with parameters require the presence of the ClaireRules library, which is no longer available.

For instance, let us define the following rule to fill the table fib with the Fibonacci sequence.

r3() :: rule(

y := fib[x] & x % (0 .. 100)

=> when z := get(fib,x – 1) in fib[x + 1] := y + z)

(fib[0] := 1, fib[1] := 1)

Warning: CLAIRE 2’s logical rules are no longer supported. If you define a rule with arguments “r1(x:<type>,y:<type>) :: rule( …), you will get an error message.


5.3 Hypothetical Reasoning

In addition to rules, claire also provides the ability to do some hypothetical reasoning. It is indeed possible to make hypotheses on part of the knowledge (the database of relations) of claire, and to change them whenever we come to a dead-end. This possibility to store successive versions of the database and to come back to a previous one is called the world mechanism (each version is called a world). The slots or tables x on which hypothetical reasoning will be done need to be specified with the declaration store(x). For instance,

store(age,friends,fib) <=> store(age), store(friends), store(fib)

Each time we ask claire to create a new world, claire saves the status of tables and slots declared with the store command. Worlds are represented with numbers, and creating a new world is done with choice(). Returning to the previous world is done with backtrack(). Returning to a previous world n is done with backtrack(n). Worlds are organized into a stack (sorry, you cannot explore two worlds at the same time) so that save/restore operations are very fast. The current world that is being used can be found with world?(), which returns an integer.

Definition: A world is a virtual copy of the defeasible part of the object database. The object database (set of slots, tables and global variables) is divided into the defeasible part and the stable part using the store declaration. Defeasible means that updates performed to a defeasible relation or variable can be undone later; r is defeasible if store(r) has been declared. Creating a world (choice) means storing the current status of the defeasible database (a delta-storage using the previous world as a reference). Returning to the previous world (backtrack) is just restoring the defeasible database to its previously stored state.

In addition, you may accept the hypothetical changes that you made within a world while removing the world and keeping the changes. This is done with the commit and commit= methods. commit() decreases the world counter by one, while keeping the updates that were made in the current world. It can be seen as a collapse of the current world and the previous world. commit=(n) repeats commit() until the current world is n. Notice that this “collapse” will simply make the updates that were made in the current world (n) look like they were made in the previous world (n – 1); thus, these updates are still defeasible. A stronger version, commit0, is available that consider the updates made in the current world as non-defeasible (as if they belonged to the world with index 0). Thus, unless commit is used to return to the initial world (with index 0) – in which case commit and commit0 are equivalent - commit grows the size of the current world since it does not free the stack memory that is used to trail updates.

Last, we have seen in the Sudoku example from the Tutorial and in Section 3.6 the existence of the branch(X) control structure which creates “a branch of a search tree” through the use of worlds.

To summarize:

  • choice() creates a “branching point” (a copy of the stored slots and tables that can be backtracked to).

  • backtrack() returns to the previously saved world, that is, the value of each slot and stable which has been declared as “defeasible” through the store(…) declaration is returned to what it was when choice() was invoked.

  • World?() returns an integer, the number of branches that have been made using choice().

  • commit() makes all changes made in the current world (n) part of the previous world (n – 1), which becomes the current world.

  • branch(<exp>) creates a new world, evaluate <exp>, if the result is true returns the true Boolean value in the new world, otherwise backtrack to the initial state and returns false. A seen in section 3.6, branch creates a handler that catches the raise of a contradiction, which is interpreted as a failure (hence causes a backtrack and returns false).

The amount of memory that is assigned to the management of the world stack is a parameter to CLAIRE, as explained in Appendix C. Defeasible updates are fairly optimized in claire, with an emphasis on minimal book-keeping to ensure better performance. Roughly speaking, CLAIRE stores a pair of pointers for each defeasible update in the world stack. There are (rare) cases where it may be interesting to record more information to avoid overloading the trailing stack. For instance, trailing information is added to the stack for each update even if the current world has not changed. This strategy is actually faster than using a more sophisticated book-keeping but may yield a world stack overflow. The example of Store, given in Section 2.6, may be used as a template to remedy this problem.

For instance, here is a simple program that solves the n queens problem (the problem is the following: how many queens can one place on a chessboard so that none are in situation of chess, given that a queen can move vertically, horizontally and diagonally in both ways ?)

column[n:(1 .. 8)] : (0 .. 8) := 0 // 0 for no values yet

possible[x:(1 .. 8), y:(1 .. 8)] : boolean := true

store(column, possible)

r1() :: rule(

column[x] := z => for y in ((1 .. 8) but x) possible[y,z] := false)

r2() :: rule(

column[x] := z => let d := x + z in

for y in (max(1,d - 8) .. min(d - 1, 8))

possible[y,d - y] := false )

r3() :: rule(

column[x] := z => let d := z – x in

for y in (max(1,1 - d) .. min(8,8 - d))

possible[y,y + d] := false)

queens(n:(0 .. 8)) : boolean

-> ( if (n = 0) true

else exists(p in (1 .. 8) |

(possible[n,p] &

branch( (column[n] := p, queens(n - 1)) ))))

queens(8)

In this program queens(n) returns true if it is possible to place n queens. Obviously there can be at most one queen per line, so the purpose is to find a column for each queen in each line : this is represented by the column table. So, we have eight levels of decision in this problem (finding a line for each of the eight queens). The search tree (these imbricated choices) is represented by the stack of the recursive calls to the method queens. At each level of the tree, each time a decision is made (an affectation to the table column), a new world is created, so that we can backtrack (go back to previous decision level) if this hypothesis (this branch of the tree) leads to a failure.

Note that the table possible, which tells us whether the n-th queen can be set on the p-th line, is filled by means of rules triggered by column (declared event) and that both possible and column are declared store so that the decisions taken in worlds that have been left are undone (this avoids to keep track of decisions taken under hypotheses that have been dismissed since).

Updates on lists can also be “stored” on worlds so that they become defeasible. Instead of using the nth= method, one can use the method store(l,x,v,b) that places the value v in l[x] and stores the update if b is true. In this case, a return to a previous world will restore the previous value of l[x]. If the boolean value is always true, the shorter form store(l,x,y) may be used. Here is a typical use of store:

store(l,n,y,l[n] != y)

This is often necessary for tables with range list or set. For instance, consider the following :

A[i:(1 .. 10)] : tuple(integer,integer,integer) := list<integer>(0,0,0)

(let l := A[x] in

(l[1] := 3, l[3] := 3))

even if store(A) is declared, the manipulation on l will not be recorded by the world mechanism. You would need to write :

A[x] := list(3,A[x][2],3)

Using store, you can use the original (and more space-efficient) pattern and write:

(let l := A[x] in

(store(l,1,3), store(l,3,3)))

There is another problem with the previous definition. The expression given as a default in a table definition is evaluated only once and the value is stored. Thus the same list<integer>(0,0,0) will be used for all A[x]. In this case, which is a default value that will support side-effects, it is better to introduce an explicit initialisation of the table:

(for i in (1 .. 10) A[i] := list<integer>(0,0,0))

There are two operations that are supported in a defeasible manner: direct replacement of the i-th element of l with y (using store(l,i,y)) and adding a new element at the end of the list (using store(l,y)). All other operations, such as nth+ or nth- are not defeasible. The addition of a new element is interesting because it either returns a new list or perform a defeasible side-effect. Therefore, one must also make sure that the assignment of the value of store(l,x) is also made in a defeasible manner (e.g., placing the value in a defeasible global variable). To perform an operation like nth+ or delete on a list in a defeasible manner, one usually needs to use an explicit copy (to protect the original list) and store the result using a defeasible update (cf. the second update in the next example)

It is also important to notice that the management of defeasible updates is done at the relation level and not the object level. Suppose that we have the following:

C1 < : object(a:list<any>, b:integer)

C2 < : thing(c:C1)

store(c,a)

P :: C1()

P.c := C2(a = list<any>(1,2,3) , b = 0) // defeasible but the C2 object remains

P.c.a := delete(copy(P.c.a), 2) // this is defeasible

P.c.b := 2 // not defeasible

The first two updates are defeasible but the third is not, because store(b) has not been declared. It is also possible to make a defeasible update on a regular property using put_store.