Hypothetical Reasoning

• backtrack() -> void
• backtrack(n:integer) -> void
• choice() -> void
• commit() -> void
• commit(n:integer) -> void
• contradiction!() -> void
• prealloc_list(t:type, n:integer) -> list [XL]
• prealloc_set(t:type, n:integer) -> set [XL]
• put_store(self:property, x:object, y:any, b:boolean) -> void
• store(rels:listargs) -> void
• store(v:global_variable) -> void
• store(a:array, n:integer, v:any, b:boolean) -> void
• store(l:list, n:integer, v:any, b:boolean) -> void
• world?() -> integer

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.

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

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.

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)] : (1 .. 8) := unknown  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 initialization 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^thelement 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. It is worth noticing that hypothetical reasoning.

backtrack() -> void

backtrack() pops the current world and returns to the previous one.

backtrack(n:integer) -> void

backtrack(n) returns to the world numbered with n, and pops all the intermediary worlds.

choice() -> void

choice() creates a new world and steps into it.

commit() -> void

The method commit() returns to the previous world but carries the updates that were made within the current world; these updates now belong to the previous world and another call to backtrack() would undo them.

commit(n:integer) -> void

commit(n) returns to the world numbered with n through successive applications of commit().

contradiction!() -> void

contradiction!() throws a contradiction. contradiction!() uses a unique instance of the contradiction exception class such to save a little memory.

prealloc_list(t:type, n:integer) -> list

XL CLAIRE provides a convenient way to (pre)allocate defeasible lists in a class prototypes. Starting with CLAIRE 3, the content of a defeasible list have to be allocated prior to perform updates on it. prealloc_list(t,n) allocates an empty list for a class prototype that will automatically initialize a slot with a preallocated list of n elements and initially empty :

lesson <: ephemeral_object(              students:list[student] = prealloc_list(student, 100))  (store(students))  lesson!() : lesson -> lesson()

notice that the list owned by the class prototype is actually empty and that it becomes allocated only once it is copied (as done by instantiation process).

prealloc_set(t:type, n:integer) -> set

preallocate a set in a similar way to prealloc_list.

put_store(self:property, x:object, y:any, b:boolean) -> void

put_store(r,x,v,b) is equivalent to put(r,x,v) but also stores this update in the current world if b is true. The difference with the use of the statement store(p) is that put_store allows the user to control precisely which update should be backtracked.

store(rels:listargs) -> void

store(r1, r2, ...) declares the relations (properties or arrays) as defeasible (using the world mechanism)

store(v:global_variable) -> void

store(v) declares the global variable v as defeasible (using the world mechanism).

store(a:array, n:integer, v:any, b:boolean) -> void

store(a, n, v, b) is equivalent to a[n] := v but also stores this update in the current world if b is true. As a syntactical convenience, the argument b may be omitted if it is true. Note that there is a similar method for properties called put_store.

store(l:list, n:integer, v:any, b:boolean) -> void

store(l, n, v, b) is equivalent to l[n] := v but also stores this update in the current world if b is true. As a syntactical convenience, the argument b may be omitted if it is true. Note that there is a similar method for properties called put_store.

world?() -> integer

world?() returns the index of the current world.