We have developed a new programming language for implementing distributed algorithms encoded by means of local computations [17]. This language, called Lidia, is based on a two-level transition system model: the first level is used to specify the behavior of each single component, whereas the second level captures their interactions. Transitions are basically expressed in a precondition-effect style. Lidia depends on a logic \lambda _\infty ^* that is used to express the preconditions of each transition. The main topic of this paper is to present the \lambda _\infty ^* language and to bring out some of its basic properties. Moreover, we will take advantage of these properties to define a class of distributed algorithms encoded by means of local computations, that can be implemented in our programming language. The completeness of Lidia, related to the use of users defined functions, will represent the main result of this paper.