13.1 Introduction
In the preceding unit (Chapters 710), we saw how to write rules to define view relations in terms of base relations. Once defined, we can use those views in queries and in the definitions of other views.
In this unit (Chapters 1114), we look at how to write rules that define operations in terms of changes to base relations. Once defined, we can use those operations in updates and in the definitions of other operations.
As we have seen, the rules used in writing view definitions generalize the rules used in writing queries; and, as we shall see, the rules used in writing operation definitions generalize the rules used in writing updates. That said, it is important to keep in mind the differences between views and operations  views are used in talking about facts that are true in states whereas operations are used in talking about changes to states.
In this chapter, we define the syntax and semantics of operation definitions. In the next chapter, we see how operation definitions can be used to specify the handling of events in dynamic systems (where the system's behavior changes in response to external stimuli). In Chapter 13, we look at how to use operation definitions in database management. And, in Chapter 14, we look at how to use operation definitions in building interactive worksheets.
13.2 Syntax
The syntax of operation definitions builds upon the syntax of updates described in Chapter 4. The various types of constants are the same, and the notions of term and atom and literal are also the same. However, to these, we add a few new items.
To denote operations, we designate some constants as operation constants. As with constructors and relation constants, each operation constant has a fixed arity  unary, binary, and so forth.
An action is an application of an operation to specific objects. In what follows, we denote actions using a syntax similar to that of atomic sentences, viz. an nary operation constant followed by n terms enclosed in parentheses and separated by commas. For example, if f is a binary operation constant and a and b are symbols, then f(a,b) denotes the action of applying the operation f to a and b.
An operation definition rule (or, more simply, an operation rule) is an expression of the form shown below. Each rule consists of (1) an action expression, (2) a double colon, (3) a literal or a conjunction of literals, (4) a double shafted forward arrow, and (5) a literal or an action expression or a conjunction of literals and action expressions. The action expression to the left of the double colon is called the head; the literals to the left of the arrow are called conditions; and the literals to its right are called effects.
γ :: [~]φ_{1} & ... & [~]φ_{m} ==> [~]ψ_{1} & ... & [~]ψ_{n} & γ_{1} & ... & γ_{k} 
Intuitively, the meaning of an operation rule is simple. If the conditions of a rule are true in any state, then executing the action in the head requites that we execute the effects of the rule.
For example, the following rule states that in any state in which p(a,b) is true and q(a) is false, the executing click(a) requires that we remove p(a,b) from our dataset, add q(b), perform action click(b).
click(a) :: p(a,b) & ~q(a) ==> ~p(a,b) & q(a) & click(b) 
As with rules defining views, operation rules may contain variables to express information in a compact form. For example, we can write the following rule to generalize the preceding rule to all objects.
click(X) :: p(X,Y) & ~q(X) ==> ~p(X,Y) & q(X) & click(Y) 
As with view rules, safety is a consideration. Safety in this case means that every variable among the effects of a rule or in negative conditions also appears in the head of the rule or in the positive conditions.
The operation rules shown above are both safe. However, the rules shown below are not. The second effect of the first rule contains a variable that does not appear in the head or in any positive condition. In the second rule, there is a variable that appears in a negative condition that does not appear in the head or in any positive condition.
click(X) :: p(X,Y) & ~q(X) ==> ~p(X,Y) & q(Z) & click(Y) 
click(X) :: p(X,Y) & ~q(Z) ==> ~p(X,Y) & q(X) & click(Y) 
In some operation rules there is no condition, i.e. the effects of the transition rule take place on all datasets. We can, of course, write such rules by using the condition true, as in the following example.
click(X) :: true ==> ~p(X) & q(X) 
For the sake of simplicity in writing our examples, we sometimes abbreviate such rules by dropping the conditions and the transition operator and instead write just the effects of the transition as the body of the operation rule. For example, we can abbreviate the rule above as shown below.
An operation definition is a collection of operation rules in which the same operation appears in the head of every rule. As with view definitions, we are interested primarily in rulesets that are finite. However, in analyzing operation definitions, we occasionally talk about the set of all ground instances of the rules, and in some cases these sets are infinite.
13.3 Semantics
The semantics of operation definitions is more complicated than the semantics of updates due to the possible occurrence of views in the conditions of the rule and the possible occurrence of operations in its effects. In what follows, we first define the expansion of an action in the context of a given dataset, and we then define the result of performing that action on that dataset.
Suppose we are given a set Ω of rules, a set Γ of actions (factoids, negated factoids, and actions), and a dataset Δ. We say that an instance of a rule in Ω is active with respect to Γ and Δ if and only if the head of the rule is in Γ and the conditions of the rule are all true in Δ.
Given this notion, we define the expansion of action γ with respect to rule set Ω and dataset Δ as follows. Let Γ_{0} be {γ} and let Γ_{i+1} be the set of all effects in any instance of any rule in Ω with respect to Γ_{i} and Δ. We define our expansion U(γ,Ω,Δ) as the fixpoint of this series. Equivalently, it is the union of the sets Γ_{i}, for all nonnegative integers i.
Next, we define the positive updates A(γ,Ω,Δ) to be the positive base factoids in U(γ,Ω,Δ). We define the negative updates D(γ,Ω,Δ) to be the set of all negative factoids in U(γ,Ω,Δ).
Finally, we define the result of applying an action γ to a dataset Δ as the result of removing the negative updates from Δ and adding the positive updates, i.e. the result is (Δ  D(γ,Ω,Δ)) ∪ A(γ,Ω,Δ).
To illustrate these definitions, consider an application with a dataset representing a directed acyclic graph. In the sentences below, we use symbols to designate the nodes of the graph, and we use the edge relation to designate the arcs of the graph.
edge(a,b) 
edge(b,d) 
edge(b,e) 
The following operation definition defines a ternary operation copy that copies the outgoing arcs in the graph from its first argument to its second argument.
copy(X,Y) :: edge(X,Z) ==> edge(Y,Z) 
Given this operation definition and the dataset shown above, the expansion of copy(b,c) consists of the changes shown below. In this case, the factoids representing the two arcs emanating from b are all copied to c.
After executing this event, we end up with the following dataset.
edge(a,b) 
edge(b,d) 
edge(b,e) 
edge(c,d) 
edge(c,e) 
The following rule defines a unary operation invert that reverses the incoming arcs of the node specified as it argument.
invert(Y) :: edge(X,Y) ==> ~edge(X,Y) & edge(Y,X) 
The expansion of invert(c) is shown below. In this case, the arguments in the factoid with c as second argument have all been reversed.
~edge(c,d) 
~edge(c,e) 
edge(d,c) 
edge(e,c) 
After executing this event, we end up with the following dataset.
edge(a,b) 
edge(b,d) 
edge(b,e) 
edge(d,c) 
edge(e,c) 
Finally, the following operation rules define a binary operation that inserts a new node into the graph (the first argument) with an arc to the second argument and arcs to all of the nodes that are reachable from the second argument.
insert(X,Y) :: edge(X,Y) 
insert(X,Y) :: edge(Y,Z) ==> insert(X,Z) 
The expansion of insert(w,b) is shown below. The first rule adds edge(w,b) to the expansion. The second rule adds insert(w,d) and insert(w,e). Given these events, on the next round of expansion, the first rule adds edge(w,d) and edge(w,e) and the second rules adds insert(w,c). On the third round of expansion, we get edge(w,c). At this point, neither rule adds any additional items to our expansion, and the process terminates.
insert(w,b) 
edge(w,b) 
insert(w,d) 
insert(w,e) 
edge(w,d) 
edge(w,e) 
insert(w,c) 
edge(w,c) 
Applying this event to the preceding dataset produces the result shown below.
edge(a,b) 
edge(b,d) 
edge(b,e) 
edge(d,c) 
edge(e,c) 
edge(w,b) 
edge(w,d) 
edge(w,e) 
edge(w,c) 
Note that it is possible to define insert in other ways. We could, for example, define a view of edge that relates each node to every node that can be reached from the node; and we could then use this view in a nonrecursive definition of insert. However, this would require us to introduce a new view into our vocabulary; and, for many people, this is less clear than the definition shown above.
Exercises
Exercise 13.1: For each of the following strings, say whether it is a syntactically legal operation definition.

(a) 
a(X) :: p(X,Y) ==> q(Y,X) 

(b) 
a(X) :: p(X,Y) & a(Y) ==> q(Y,X) 

(c) 
a(X) :: p(X,Y) ==> q(Y,X) & a(Y) 

(d) 
a(X) :: p(X,Y) ==> q(Y,X) & ~a(Y) 

(e) 
a(X) :: p(Y,Y) ==> q(X,Y) 
Exercise 13.2: Say whether each of the following rules is safe.

(a) 
a(X) :: p(X,Y) & p(Y,Z) ==> p(X,Z) 

(b) 
a(X) :: p(X,Y) & ~p(Y,Z) ==> p(X,Z) 

(c) 
a(X) :: p(Y,Z) ==> p(X,Z) 

(d) 
a(X) :: p(Y,Z) ==> ~p(X,Z) 

(e) 
a(X) :: p(Y,Z) ==> p(Z,Y) 
Exercise 13.3: Given the definition fix(X) :: p(X,Y) & p(Y,Z) ==> p(X,Z), what is the result of executing the action fix(a) on the dataset shown below.
p(a,b) 
p(b,c) 
p(c,d) 
p(d,e) 
Exercise 13.4: Given the definition fix(X) :: p(X,Y) & p(Y,Z) ==> p(X,Z) & fix(Y), what is the result of executing the action fix(a) on the dataset shown below.
p(a,b) 
p(b,c) 
p(c,d) 
p(d,e) 
Exercise 13.5: Consider a type hierarchy like the one shown below.
subtype(giraffe,mammal) 
subtype(rabbit,mammal) 
subtype(mammal,vertebrate) 
subtype(earthworm,vertebrate) 
subtype(vertebrate,animal) 
subtype(invertebrate,animal) 
Define an operation classify that takes an object and a type as arguments and adds factoids stating that the object has that type and all supertypes of that type. For example, executing the action classify(george,giraffe) should result in the following factoids being added to the dataset.
type(george,giraffe) 
type(george,mammal) 
type(george,vertebrate) 
type(george,animal) 
