How to build CSP denotational semantics for a small example?

Question

Haskell

Here I have a simple recursive formula that describes a certain system of processes:

X(i) = if (i == 0) then [left -> X(0) | right -> X(1)] else [left -> X(i-1) | right -> X(i+1)]

Let me explain what operators above processes mean (I'm talking to TC experts, but they may not know anything about CSP).
The operator a -> Pmeans: after the event occurs, acontinue as a process P. That is, it constructs a new process from some event and process.
The operator a -> P | b -> Qmeans: if happens a, then it will be further P, if b, then Q.
In general (it seems to be important), these are two special cases of the choice operator a:A -> P(a), which means: after one of the events of the set occurs A, the process will continue, as determined by the function P.
a -> Pwrite when too lazy to specify a set of one element, anda -> P | b -> Q they write when they are too lazy to write if.
For processes, you can define traces, that is, sequences of events that lead to the continuation of the process. For example, for a special process, the STOPset of traces contains only the empty {""}. And the process a -> STOP | b -> c -> STOPwill have a set of traces {"a", "bc", ""}.
Yes, in a sense, traces are similar to the languages ​​defined by COP grammars (the difference is that processes have a much richer algebra than the one I use here).
Further, in the mathematical interpretation, the processes are identified with their sets of traces. On the set of such processes, it is possible to introduce a partial order - the order by including one set of traces into another. This is great, because, as a result, we get a domain in which we can solve various recursive equations. Wherein,a:A -> P(a)will be a continuous function.
Now, actually, to a question. Here (again) I have a formula:

X(i) = if (i == 0) then [left -> X(0) | right -> X(1)] else [left -> X(i-1) | right -> X(i+1)]

Hoare himself (the author of CSP) in this formula proposes to see the following meaning (this is a simplified version of Hoare's example, in which the robot moves along the plane into a cell): if we are standing in the zero cell, then we are standing in it, when trying to move to the left; in any other cell we move in the specified direction.
This recursive equation has a continuous function on the right. And we can therefore use the fixed point operator. The initial value should be a function, bottom: λi. STOP. And, it seems, everything is fine. And the limit even converges. But it does not converge at all to what we would like it to converge.
The result is a function that describes a system of processes such that in the zero cell, when you try to go left (handling the left event) or right (handling the right), everything freezes (ends with the STOP process), from other cells you can only go left, when you try to go to the right, everything freezes.
Is it possible to somehow hang more and more intuitive semantics on this? I’m reading about the theory of domains and categories, and there is such a thing as a domain of subdomains (powerdomain), and it seems like, within this structure, limits are considered that allow you to work with infinite structures and gradually unfold the semantic construction. But, unfortunately, everything is written there at a high abstract level, and I absolutely do not understand how this can be applied in practice. At least for such a simple example.
If anyone can help, or at least point to a book with relevant examples, I will be very grateful.

Answer 1

Of course, I looked at this CSP quite a bit, but it seems to me that with such a definition, traces for all processes will be {left, right}*. Maybe there in the definition at least for i = 0 with left everything stops? Or I just don't understand something.