There is an interesting problem of self identification. It can be illustrated on the example of the following simple version of Dijkstra's dining philosophers protocol (which may deadlock). There are n philosophers, marked with numbers modulo n, each equipped with a fork. A philosopher i may think (which requires no forks) or eat using his/her fork and the fork of philosopher i+1. A fork cannot be used by two philosophers at the same time.
Using functions Fork(i), where Fork(i) = up if the fork of philosopher i is used and Fork(i) = down otherwise, we can write a separate program for each philosopher i . Intuitively, however, all philosophers use the same program in the protocol.
To solve such problems, we suppose that each agent a is represented by an element of the common carrier. For simplicity, we will not distinguish between an agent and the element that represents the agent. Further, we use a special nullary function Self, interpreted differently by different agents. An agent a interprets Self as a . Thus function Self allows an agent to identify itself among other agents. Self is a logic name and cannot be the subject of an update instruction. To make rules sound a little better for humans, we use some capitalized pronouns, e.g. Me, as aliases for Self. Viewing agents as elements of the carrier is useful for other purposes as well. For example, it allows us to model the creation of new agents.
We return to the dining philosophers protocol. Here is a possible program (courtesy of Jim Huggins):
if Mode(Me)=think and Fork(Me)=Fork(Me+1)=down then
Fork(Me) := up, Fork(Me+1) := up, Mode(Me) := eat
elseif Mode(Me)=eat then
Fork(Me) := down, Fork(Me+1) := down, Mode(Me) := think
endif
It may be convenient to suppress the argument Self. For example, terms Mode(Me), Fork(Me) and Fork(Me+1) may be treated as nullary functions and abbreviated, e.g., as mode, lfork and rfork, so that the rfork function of philosopher i is the lfork function of philosopher i+1 and mode is a private function.