(music and vocals) In this lecture we'll look at the sum operator that we need to specify processes for data. Let's look again at this example of a buffer. Where you read a number, and you deliver a number, so up til now we specified it like this, by an equation, where we can read for instance, number zero and deliver zero, or read one and deliver one. And do this for finite number of values. But let's assume that we would like to read an arbitrary number so, something like this reads, a natural number and delivering number and then we have an infinite number of choices. And we could try to specify it like this with dots. But of course this is not a specification. Actually we don't like infinite objects. We want to specify our behavior. By finite equations. And then in order to do this, we need a new operator and that is the sum operator. Specification of the buffer then looks like this. What write down is this and we only write down the right hand side of the equation. We take, we choose a number and from the domain of natural numbers. We read that number, deliver that number, and then we have the behavior of the buffer again. And we used the sigma operator because this is, in some sense the generalized sum operator If you would like to use this to generate state space, then you can imagine that this will not be possible because the number of transitions is infinite. So this is actually the transition system. So if we want to restrict the number, the transition into something finite, then the sum operator can still be useful. So suppose that you would like to read the numbers zero up to thousand, and including thousand. Then we can ask the extra condition n should be smaller or equal than to thousands. To our equation, and it looks like this. So, we get, at the right hand side, that we reach that number, and we will do the inaction when n is smaller or equal than 1000, and then deliver it. And the interesting question is, how does states base looks like of this process? And that is something we can see on the next slide, and I think it will be obvious that such states bases are not very insightful although they look nice. You can see the initial state in the middle. And for each number, there's a state with a transition to that state, after which it goes back to the initial state. The sum operator is a relatively difficult operator, and it has a number of axioms that characterize its behavior. In strong bisimulation. And they are hard to interpret because we use variables that range over processes, and variables that range over functions from data to processes. So look at the first axiom, this axiom, SUM1 says that if I have a choice over behavior X and in X, the variable D does not occur. Then, we actually have equal choices for any failure of D. And that means, that sum over D of Type D of X is equal to X. The second axiom says that if I have the choice over lots of processes X(d) for concrete D's then we can actually make that, take one of these values out of the choice generalized sum operator, and put it separately, so in this case we can have the concrete value E of type D, and we can say that the sum of D, of type D, of X, D is equal to the same expression, or I do X(E) explicitly. This axiom is probably the most difficult axiom that we have up til now. And quite a lot of people, when they see this axiom for the first time, believe that it cannot be true. But this is really an axiom belonging to the sum operator. And we have two axioms that probably look more difficult, but actually are quite straightforward. Namely, the sum operator distributes of the plus operator, and that is what SUM4 says, so we can have expressions X and Y and this D can occur, and then you can simply push the sum operator over the choice. SUM5 says the same, but now you push the sum operator over the sequential composition operator. And here it is important that the variable D does not occur in the process y. So you can only distribute to some operator, over sequential operator if it will not bind variables in Y, so D may not occur in Y, and, therefore, Y is put there as a small variable not depending on D. Okay, if you have axioms, we can prove simple identities. So question is, can we prove this? Suppose we have the process Xn over all natural numbers. So essentially Xn equals X0, X1, X2, X3 or X4, etc. Can we take X0 and X1 out of this sum, explicitly. And the expression is, yes of course we can. And the proof is straightforward. Namely if we have the left-hand side, then using the axiom SUM3, we can first move a zero out of there. And then, by applying SUM3 again, we can move X one out of this expression and we obtain on the right hand side. Let's look at two examples. The first example, is this one. How can we prove the identity that you see here? Here we have a second exercise. Slightly more complex expression. If we work in setting of strong bisimulation, can we prove this identity and if so which axiom do we need for that? We saw the introduction of the generalized sum operator with which we can denote choices of infinite choices of data. We introduced four axioms that actually characterised the sum operator. And I think this is quite a memorable moment because, list operators to specify processes we can now specify any behavior. We will not introduce any fundamental new operators anymore. We will introduce a few operators that are helpful such as the parallel operator, but they do not essentially extend the expressability of the language. In the next lecture we will look again at the alarm clock. And it will specify it using these process operators that we have introduced. [MUSIC]