Logical Methods in Computer Science
Vol. 11(4:21)2015, pp. 1–53
www.lmcs-online.org

Submitted
Published

Dec. 15, 2014
Dec. 31, 2015

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS ∗
FERRUCCIO DAMIANI a AND MIRKO VIROLI b
a

University of Torino, Italy
e-mail address: ferruccio.damiani@unito.it

b

University of Bologna, Italy
e-mail address: mirko.viroli@unibo.it
A BSTRACT. Emerging network scenarios require the development of solid large-scale situated systems. Unfortunately, the diffusion/aggregation computational processes therein often introduce a
source of complexity that hampers predictability of the overall system behaviour. Computational fields
have been introduced to help engineering such systems: they are spatially distributed data structures
designed to adapt their shape to the topology of the underlying (mobile) network and to the events
occurring in it, with notable applications to pervasive computing, sensor networks, and mobile robots.
To assure behavioural correctness, namely, correspondence of micro-level specification (single device
behaviour) with macro-level behaviour (resulting global spatial pattern), we investigate the issue of
self-stabilisation for computational fields. We present a tiny, expressive, and type-sound calculus of
computational fields, and define sufficient conditions for self-stabilisation, defined as the ability to
react to changes in the environment finding a new stable state in finite time. A type-based approach is
used to provide a correct checking procedure for self-stabilisation.

1. I NTRODUCTION
Computational fields [34, 42] (sometimes simply fields in the following) are an abstraction traditionally used to enact self-organisation mechanisms in contexts including swarm robotics [3], sensor
2012 ACM CCS: [Theory of computation]: Models of computation—Concurrency—Distributed computing models;
Logic—Type theory; Design and analysis of algorithms—Distributed algorithms—Self-organization; Semantics and
reasoning—Program constructs—Control primitives; Semantics and reasoning—Program semantics; Semantics and
reasoning—Program reasoning—Program analysis; [Software and its engineering]: Software notations and tools —
General programming languages—Language types— Distributed programming languages / Functional languages; Software
notations and tools—Context specific languages; [Computing methodologies]: Artificial intelligence—Distributed
artificial intelligence—Cooperation and coordination.
Key words and phrases: Computational field, Core calculus, Operational semantics, Spatial computing, Type-based
analysis, Type soundness, Type system, Refinement type.
∗ A preliminary version of some of the material presented in this paper has appeared in COORDINATION 2015.
a Ferruccio Damiani has been partially supported by project HyVar (www.hyvar-project.eu) which has received funding
from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 644298, by ICT
COST Action IC1402 ARVI (www.cost-arvi.eu), by ICT COST Action IC1201 BETTY (www.behavioural-types.eu), by
the Italian PRIN 2010/2011 project CINA (sysma.imtlucca.it/cina), and by Ateneo/CSP project SALT (salt.di.unito.it).
b Mirko Viroli has been partially supported by the EU FP7 project “SAPERE - Self-aware Pervasive Service Ecosystems”
under contract No. 256873 and by the Italian PRIN 2010/2011 project CINA (sysma.imtlucca.it/cina).

l

LOGICAL METHODS
IN COMPUTER SCIENCE

c
DOI:10.2168/LMCS-11(4:21)2015

CC

F. Damiani and M. Viroli
Creative Commons

2

F. DAMIANI AND M. VIROLI

networks [5], pervasive computing [35], task assignment [49], and traffic control [13]. They are
distributed data structures originated from pointwise events raised in some specific device (i.e., a sensor), and propagating in a whole network region until forming a spatio-temporal data structure upon
which distributed and coordinated computation can take place. Middleware/platforms supporting this
notion include TOTA [35], Proto [36], and SAPERE [51, 44]. The most paradigmatic example of
computational field is the so-called gradient [6, 35, 38], mapping each node of the network to the
minimum distance from the source node where the gradient has been injected. Gradients are key to
get awareness of physical/logical distances, to project a single-device event into a whole network
region, and to find the direction towards certain locations of a network, e.g., for routing purposes.
Several pieces of work have been developed that investigate coordination models supporting fields
[35, 47], introduce advanced gradient-based spatial patterns [37], study universality and expressiveness [10], and develop catalogues of self-organisation mechanisms where gradients play a crucial
role [25].
As with most self-organisation approaches, a key issue is to try to fill the gap between the
system micro-level (the single-node computation and interaction behaviour) and the system macrolevel (the shape of the globally established spatio-temporal structure), namely, ensuring that the
programmed code results in the expected global-level behaviour. However, the issue of formally
tackling the problem is basically yet unexplored in the context of spatial computing, coordination,
and process calculi—some exceptions are [6, 27], which however apply in rather ad-hoc cases. We
note instead that studying this issue will likely shed light on which language constructs are best
suited for developing well-engineered self-organisation mechanisms based on computational fields,
and to consolidate existing patterns or develop new ones.
In this paper we follow this direction and devise an expressive calculus to specify the propagation
process of those computational fields for which we can identify a precise mapping between system
micro- and macro-level. The key constructs of the calculus are three: sensor fields (considered as
an environmental input), pointwise functional composition of fields, and a form of spreading that
tightly couples information diffusion and re-aggregation. The spreading construct is constrained
so as to enforce a special “stabilising-diffusion condition” that we identified, by which we derive
self-stabilisation [22], that is, the ability of the system running computational fields to reach a stable
distributed state in spite of perturbations (changes of network topology and of local sensed data)
from which it recovers in finite time. A consequence of our results is that the ultimate (and stable)
state of an even complex computational field can be fully-predicted once the environment state is
known (network topology and sensors state). Still, checking that a field specification satisfies such
stabilising-diffusion condition is subtle, since it involves the ability of reasoning about the relation
holding between inputs and outputs of functions used to propagate information across nodes. Hence,
as an additional contribution, we introduce a type-based approach that provides a correct checking
procedure for the stabilising-diffusion condition.
The remainder of this paper is organised as follows: Section 2 illustrates the proposed linguistic
constructs by means of examples; Section 3 presents the calculus and formalises the self-stabilisation
property; Section 4 introduces the stabilising-diffusion condition to constrain spreading in order to
ensure self-stabilisation; Section 5 proves that the stabilising-diffusion condition guarantees selfstabilisation; Section 6 extends the calculus with the pair data structure and provides further examples;
Sections 7, 8 and 9 incrementally present a type-based approach for checking the stabilising-diffusion
condition and prove that the approach is sound; Section 10 discusses related work; and finally
Section 11 concludes and discusses directions for future work. The appendices contain the proof
of the main results. A preliminary version of some of the material presented in this paper appeared
in [45].

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

e
f
D

::= x s g e0 ?e1 :e2 f(e1 , ..., en )
::= d b
::= def T d(T1 x1 , ..., Tn xn ) is e

{e : f(@, e1 , ..., en )}

3

expression
function name
function definition

Figure 1: Syntax of expressions and function definitions
2. C OMPUTATIONAL F IELDS
From an abstract viewpoint, a computational field is simply a map from nodes of a network to
some kind of value. They are used as a valuable abstraction to engineer self-organisation into
networks of situated devices. Namely, out of local interactions (devices communicating with a small
neighbourhood), global and coherent patterns (the computational fields themselves) establish that
are robust to changes of environmental conditions. Such an adaptive behaviour is key in developing
system coordination in dynamic and unpredictable environments [40].
Self-organisation and computational fields are known to build on top of three basic mechanisms
[25]: diffusion (devices broadcast information to their neighbours), aggregation (multiple information
can be reduced back into a single sum-up value), and evaporation/decay (a cleanup mechanism is
used to reactively adapt to changes). These mechansisms have been used to synthetise a rather vast
set of distributed algorithms [21, 52, 25, 7].
For instance, these mechanisms are precisely those used to create adaptive and stable gradients,
which are building blocks of more advanced patterns [25, 37]. A gradient is used to reify in any
node some information about the path towards the nearest gradient source. It can be computed by
the following process: value 0 is held in the gradient source; each node executes asynchronous
computation rounds in which (i) messages from neighbours are gathered and aggregated in a
minimum value, (ii) this is increased by one and is diffused to all neighbours, and (iii) the same
value is stored locally, to replace the old one which decays. This continuous “spreading process”
stabilises to a so called hop-count gradient, storing distance to the nearest source in any node, and
automatically repairing in finite time to changes in the environment (changes of topology, position
and number of sources).
2.1. Basic Ingredients. Based on these ideas, and framing them so as to isolate those cases where
the spreading process actually stabilises, we propose a core calculus to express computational fields.
Its syntax is reported in Figure 1. Our language is typed and (following the general approach used in
other languages for spatial computing [46, 36], which the one we propose here can be considered as
a core fragment) functional.
Types T are monomorphic. For simplicity, only ground types G (like real and bool) are
modeled—in Section 6 we will point out that the properties of the calculus are indeed parametric in
the set of modeled types (in particular, we will consider and extension of the calculus that models
pairs). We write [[T]] to denote the set of the values of type T. We assume that each type T is equipped
with a total order ≤T over [[T]] that is noetherian [31], i.e., there are no infinite ascending chains of
values v0 <T v1 <T v2 <T · · · . This implies that [[T]] has a maximum element, that we denote by >T .
Each ground type usually comes with a natural ordering (for bool we consider FALSE ≤bool TRUE)
which is total and noetherian—though in principle ad-hoc ordering relations could be used in a
deployed specification language.
An expression can be a variable x, a sensor s, a ground-value g, a conditional e0 ?e1 :e2 , a
function application f(e1 , . . . , en ) or a spreading {e : f(@, e1 , ..., en )}. Variables are the formal
parameters of a function.

4

F. DAMIANI AND M. VIROLI

Sensors are sources of input produced by the environment, available in each device (in examples,
we shall use for them literals starting with symbol “#”). For instance, in a urban scenario we may
want to use a crowd sensor #crowd yielding non-negative real numbers, to represent the perception
of crowd level available in each deployed sensor over time [38].
Values v coincide with ground values g (i.e., values of ground type), like reals (e.g., 1, 5.7,...
and POSINF and NEGINF meaning the maximum and the minimum real, respectively) and booleans
(TRUE and FALSE).
A function can be either a built-in function b or a user-defined function d. Built-in functions
include usual mathematical/logical ones, used either in prefix or infix notation, e.g., to form expressions like 2*#crowd and or(TRUE,FALSE). User-defined functions are declared by a function
definition def T d(T1 x1 , ..., Tn xn ) is e—cyclic definitions are prohibited, and the 0-ary function
main is the program entry point. As a first example of user-defined function consider the following
function restrict:
def real restrict(real i, bool c) is c ?

i :

POSINF.

It takes two arguments i and c, and yields the former if c is true, or POSINF otherwise—as we shall
see, because of our semantics POSINF plays a role similar to an undefined value.
A pure function f is either a built-in function b, or a user-defined function d whose call graph
(including d itself) does not contain functions with spreading expressions or sensors in their body.
We write [[f]] to denote the (trivial) semantics of a pure-function f, which is a computable functions
that maps a tuple of elements from [[T1 ]],..., [[Tn ]] to [[T]], where T1 , ..., Tn and T are the types of the
arguments and the type of the result of f, respectively.
As in [46, 36], expressions in our language have a twofold interpretation. When focussing on the
local device behaviour, they represent values computed in a node at a given time. When reasoning
about the global outcome of a specification instead, they represent whole computational fields: 1 is
the immutable field holding 1 in each device, #crowd is the (evolving) crowd field, and so on.
The key construct of the proposed language is spreading, denoted by syntax {e : f(@, e1 , ..., en )},
where e is called source expression, and f(@, e1 , ..., en ) is called diffusion expression. In a diffusion
expression the function f, which we call diffusion, must be a pure function whose return type and first
argument type are the same. The symbol @ plays the role of a formal argument, hence the diffusion
expression can be seen as the body of an anonymous, unary function. Viewed locally to a node,
expression e = {e0 : f(@, e1 , ..., en )} is evaluated at a given time to value v as follows:
(1) expressions e0 , e1 , ..., en are evaluated to values v0 , v1 , ..., vn ;
(2) the current values w1 , ..., wm of e in neighbours are gathered;
(3) for each w j in them, the diffusion function is applied as f(w j , v1 , ..., vn ), giving value w0j ;
(4) the final result v is the minimum value among {v0 , w01 , ..., w0m }: this value is made available to
other nodes.
Note that v ≤T v0 , and if the device is isolated then v = v0 . Viewed globally, {e0 : f(@, e1 , ..., en )}
represents a field initially equal to e0 ; as time passes some field values can decrease due to smaller
values being received from neighbours (after applying the diffusion function).
The hop-count gradient created out of a #src sensor is hence simply defined as
{ #src :

@ + 1 }

assuming #src holds what we call a zero-field, namely, it is 0 on source nodes and POSINF everywhere else. In this case #src is the source expression, and f is unary successor function.

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

def real grad(real i) is { i :

5

@ + #dist }

def real restrict(real i, bool c) is c ?

i :

POSINF

def real restrictSum(real x, real y, bool c) is restrict(x + y, c)
def real gradobs(real i, bool c) is { i :

restrictSum(@,#dist, c) }

def float gradbound(real i, real z) is gradobs(i, grad(i) < z))

Figure 2: Definitions of examples

Figure 3: Pictorial representation of hop-count gradient field (left), a gradient circumventing “crowd”
obstacles field (center), and a gradient with bounded distance (right)
2.2. Examples. As a reference scenario to ground the discussion, we can consider crowd steering
in pervasive environments [38]: computational fields run on top of a myriad of small devices spread
in the environment (including smartphones), and are used to guide people in complex environments
(buildings, cities) towards points of interest (POIs) across appropriate paths. There, a smartphone
can perceive neighbour values of a gradient spread from a POI, and give directions towards smallest
values so as to steer its owner and make him/her quickly descend the gradient [35]. Starting from the
hop-count gradient, various kinds of behaviour useful in crowd steering can be programmed, based
on the definitions reported in Figure 2.
The first function in Figure 2 defines a more powerful gradient construct, called grad, which
can be used to generalise over the hop-by-hop notion of distance: sensor #dist is assumed to exist
that reifies an application-specific notion of distance as a positive number. It can be 1 everywhere to
model hop-count gradient, or can vary from device to device to take into consideration contextual
information. For instance, it can be the output of a crowd sensor, leading to greater distances
when/where crowded areas are perceived, so as to dynamically compute routes penalising crowded
areas as in [38]. In this case, note that diffusion function f maps (v1 , v2 ) to v1 + v2 . Figure 3
(left) shows a pictorial representation, assuming devices are uniformly spread in a 2D environment:
considering that an agent or data items move in the direction descending the values of a field, a
gradient looks like a sort of uniform attractor towards the source, i.e., to the nearest source node.
It should be noted that when deployed in articulated environments, the gradient would stretch and
dilate to accommodate the static/dynamic shape of environment, computing optimal routes.
By suitably changing the diffusion function, it is also possible to block the diffusion process
of gradients, as shown in function gradobs: there, by restriction we turn the gradient value to
POSINF in nodes where the “obstacle” boolean field c holds FALSE. This can be used to completely
circumvent obstacle areas, as shown in Figure 3 (center). Note that we here refer to a “blocking”
behaviour, since sending a POSINF value has no effect on the target because of the semantics of
spreading; hence, an optimised implementation could simply avoid sending a POSINF at all, so as

6

F. DAMIANI AND M. VIROLI

T `e:T

Expression type checking:
[T-VAR]

[T-SNS]

[T-GVAL]

T ,x : T ` x : T

T ` s : type(s)

T ` g : type(g)

[T-COND]

[T-FUN]

T ` e0 : bool T ` e1 : T
T ` e0 ?e1 :e2 : T

T(T) = t-sig(f) T ` e : T
T ` f(e) : T

User-defined function type checking:
[T-DEF]
x:T`e:T
` def T d(T x) = e : T(T)

[T-SPR]

T ` e2 : T

diffusion(f) T ` f(e, e) : T
T ` {e : f(@, e)} : T
` D : T(T)

Figure 4: Type-checking rules for expressions and function definitions
not to flood the entire network. This pattern is useful whenever steering people in environments with
prohibited areas—e.g. road construction in a urban scenario.
Finally, by a different blocking mechanism we can limit the propagation distance of a gradient,
as shown by function gradbound and Figure 3 (right): the second argument z imposes a numerical
bound to the distance, which is applied by exploiting the functions gradobs and grad.
In section 6 we will exploit the pair data structure to program more advanced examples of
behaviour useful in crowd steering.
3. T HE C ALCULUS OF S ELF -S TABILISING C OMPUTATIONAL F IELDS
After informally introducing the proposed calculus in previous section, we now provide a formal
account of it and precisely state the self-stabilisation property. Namely, we formalise and illustrate
by means of examples the type system (in Section 3.1), the operational semantics (in Section 3.2),
and the self-stabilisation property (in Section 3.3).
3.1. Type checking. The syntax of the calculus is reported in Figure 1. As a standard syntactic
notation in calculi for object-oriented and functional languages [32], we use the overbar notation to
denote metavariables over lists, e.g., we let e range over lists of expressions, written e1 e2 ... en , and
similarly for x, T and so on. We write t-sig(f) to denote the type-signature T(T) of f (which specifies
the type T of the result and the types T = T1 , ..., Tn of the n ≥ 0 arguments of f). We assume that the
mapping t-sig(·) associates a type-signature to each built-in function and, for user-defined functions,
returns the type-signature specified in the function definition.
A program P in our language is a mapping from function names to function definitions, enjoying
the following sanity conditions: (i) P(d) = def d · · · (· · · ) is · · · for every d ∈ dom(P); (ii) for every
function name d appearing anywhere in P, we have d ∈ dom(P); (iii) there are no cycles in the
function call graph (i.e., there are no recursive functions in the program); and (iv) main ∈ dom(P)
and it has zero arguments. A program that does not contain the main function is called a library.
The type system we provide aims to guarantee that no run-time error may arise during evaluation:
its typing rules are given in Figure 4. Type environments, ranged over by T and written x : T, contain
type assumptions for program variables. The type-checking judgement for expressions is of the form

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

7

Ground types:
G = bool real
Sensor types:
type(#src) = real
type(#dist) = real
Built-in function type-signatures:
t-sig(not) = bool(bool)
t-sig(or) = bool(bool, bool)
t-sig(−)
= real(real)
t-sig(+)
= real(real, real)
t-sig(=)
= bool(real, real)
t-sig(<)
= bool(real, real)
Figure 5: Ground types, types for sensors, and type-signatures for built-in functions used in the
examples
T ` e : T, to be read: e has type T under the type assumptions T for the program variables occurring
in e. As a standard syntax in type systems [32], given x = x1 , ..., xn , T = T1 , ..., Tn and e = e1 , ..., en
(n ≥ 0), we write x : T as short for x1 : T1 , ..., xn : Tn , and T ` e : T as short for T ` e1 : T1 · · ·
T ` en : Tn .
Type checking of variables, sensors, ground values, conditionals, and function applications
are almost standard. In particular, values and sensors and built-in functions are given a type by
construction: the mapping type(·) associates a sort to each ground value and to each sensor, while
rule [T-FUN] exploits the mapping t-sig(·).
Example 3.1. Figure 5 illustrates the ground types, sensors, and built-in functions used in the
examples introduced throughout the paper.
The only ad-hoc type checking is provided for spreading expressions {e : f(@, e)}: they are
given the type of f(e, e), though the function f must be a diffusion, according to the following
definition.
Definition 3.2 (Diffusion). A type signature T(T) with T = T1 , ..., Tn (n ≥ 1) is a diffusion type
signature (notation diffusion(T(T))) if T = T1 . A pure function f is a diffusion (notation diffusion(f))
if its type signature t-sig(f) is a diffusion type signature.
Example 3.3. Consider the functions defined in Figure 2. The following two predicates hold:
• diffusion(+), and
• diffusion(restrictSum)
Function type checking, represented by judgement T ` D : T(T), is standard. In the following
we always consider a well-typed program (or library) P, to mean that all the function declarations in
P type check. Note that no choice may be done when building a derivation for a given type-checking
judgment, so the type-checking rules straightforwardly describe a type-checking algorithm.
Example 3.4. The library in Figure 2 type checks by using the ground types, sensors, and typesignatures for built-in functions in Figure 5.

8

F. DAMIANI AND M. VIROLI

3.2. Operational Semantics. In this section we fomalise the operational semantics of the calculus.
As for the field calculus [46] and the Proto language [36], devices undergo computation in rounds.
In each round, a device sleeps for some time, wakes up, gathers information about messages
received from neighbours while sleeping, evaluates the program, and finally broadcasts a message to
neighbours with information about the outcome of evaluation and goes back to sleep. The scheduling
of such rounds across the network is fair and non-synchronous. The structure of the network may
change over time: when a device is sleeping its neighborhood may change and the device itself
may disappear (switch-off) and subsequently appear (switch-on). We first focus on single-device
computations (in Section 3.2.1) and then on whole network evolution (in Section 3.2.2).
3.2.1. Device Computation. In the following, we let meta-variable ι range over the denumerable
set I of device identifiers, meta-variable I over finite sets of suchVdevices, meta-variables u, v and w
over values. GivenVa finite nonempty set V ⊆ [[T]] we denote by V its minimum element, and write
v ∧ v0 as short for {v, v0 }.
In order to simplify the notation, we shall assume a fixed program P and write emain to denote the
body of the main function. We say that “device ι fires”, to mean that expression emain is evaluated on
device ι. The result of the evaluation is a value-tree, which is an ordered tree of values, tracking the
value of any evaluated subexpression. Intuitively, such an evaluation is performed against the most
recently received value-trees of current neighbours and the current value of sensors, and produces as
result a new value-tree that is broadcasted to current neighbours for their firing. Note that considering
simply a value (instead of a value-tree) as the outcome of the evaluation emain on a device ι would
not be enough, since the evaluation of each spreading expression e occurring in emain requires the
values (at the root of their sub-value-trees) produced by the most recent evaluation of e on neighbours
of ι (c.f. Sect. 2).1
The syntax of value-trees is given in Figure 6, together with the definition of the auxiliary
functions ρ(·) and πi (·) for extracting the root value and the i-th subtree of a value-tree, respectively—
also the extension of these functions to sequences of value-environments θ is defined. We sometimes
abuse the notation writing a value-tree with just the root as v instead of v(). The state of sensors σ is
a map from sensor names to values, modelling the inputs received from the external world. This is
written s  v as an abuse of notation to mean s1  v1 , ..., sn  vn . We shall assume that it is complete
(it has a mapping for any sensor used in the program), and correct (each sensor s has a type written
type(s), and is mapped to a value of that type). For this map, and for the others to come, we shall
use the following notations: σ (s) is used to extract the value that s is mapped to, σ [σ 0 ] is the map
obtained by updating σ with all the associations s  v of σ 0 which do not escape the domain of σ
(namely, only those such that σ is defined for s).
The computation that takes place on a single device is formalised by the big-step operational
semantics rules given in Figure 6. The derived judgements are of the form σ ; θ ` e ⇓ θ , to be read
“expression e evaluates to value-tree θ on sensor state σ and w.r.t. the value-trees θ ”, where:
• σ is the current sensor-value map, modelling the inputs received from the external world;
• θ is the list of the value-trees produced by the most recent evaluation of e on the current device’s
neighbours;
• e is the closed expression to be evaluated;
• the value-tree θ represents the values computed for all the expressions encountered during the
evaluation of e— in particular ρ(θ ) is the local value of field expression e.
1Any implementation might massively compress the value-tree, storing only enough information for tracking the values
of spreading expressions.

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

Value-trees and sensor-value maps:
θ , η ::= v(θ )
σ ::= s  v
Auxiliary functions:
ρ(v(θ )) = v
ρ(θ1 , ..., θn ) = ρ(θ1 ), ..., ρ(θn )

value-tree
sensor-value map

πi (v(θ1 , ..., θn )) = θi
πi (θ1 , ..., θn ) = πi (θ1 ), ..., πi (θn )
σ;θ ` e ⇓ θ

Rules for expression evaluation:
[E-SNS]

[E-VAL]

σ ; θ ` s ⇓ σ (s)

σ;θ ` v ⇓ v

[E-COND]

9



σ ; π1 (θ ) ` e1 ⇓ η1

···

ρ(η2 ) if ρ(η1 ) = TRUE
ρ(η3 ) if ρ(η1 ) = FALSE
σ ; θ ` e1 ?e2 :e3 ⇓ v(η1 , η2 , η3 )

σ ; π3 (θ ) ` e3 ⇓ η3

v=

[E-BLT]

σ ; π1 (θ ) ` e1 ⇓ η1

· · · σ ; πn (θ ) ` en ⇓ ηn
v = [[b]](ρ(η1 ), ..., ρ(ηn ))
σ ; θ ` b(e1 , ..., en ) ⇓ v(η1 , ..., ηn )

[E-DEF]

def T d(T1 x1 , ..., Tn xn ) = e
σ ; π1 (θ ) ` e1 ⇓ θ10 · · · σ ; πn (θ ) ` en ⇓ θn0
σ ; πn+1 (θ ) ` e[x1 := ρ(θ10 ), ..., xn := ρ(θn0 )] ⇓ v(η)
σ ; θ ` d(e1 , ..., en ) ⇓ v(θ10 , ..., θn0 , v(η))
[E-SPR]

σ ; π0 (θ ) ` e0 ⇓ η0 · · · σ ; πn (θ ) ` en ⇓ ηn
ρ(η0 , ..., ηn ) = v0 ...vn
ρ(θ ) = w1 ...wm
σ ; 0/ ` f(w1 , v1 , ..., vn ) ⇓ u1 (· · · ) · · · σ ; 0/ ` f(wm , v1 , ..., vn ) ⇓ um (· · · )
V
σ ; θ ` {e0 : f(@, e1 , ..., en )} ⇓ {v0 , u1 , ..., um }(η0 , η1 , ..., ηn )
Figure 6: Big-step operational semantics for expression evaluation
The rules of the operational semantics are syntax directed, namely, the rule used for deriving
a judgement σ ; θ ` e ⇓ θ is univocally determined by e (cf. Figure 6). Therefore, the shape of the
value-tree θ is univocally determined by e, and the whole value-tree is univocally determined by σ ,
θ , and e.
The rules of the operational semantics are almost standard, with the exception that rules [E-COND],
[E-BLT], [E-DEF] and [E-SPR] use the auxiliary function πi (·) to ensure that, in the judgements in the
premise of the rule, the value-tree environment is aligned with the expression to be evaluated. Note
that the semantics of conditional expressions prescribes that both the branches of the conditional are
evaluated.2
The most important rule is [E-SPR] which handles spreading expressions formalising the description provided in Section 2.1. It first recursively evaluates expressions ei to value-trees ηi (after
proper alignment of value-tree environment by operator πi (.)) with top-level values vi . Then it gets
from neighbours their values w j for the spreading expression, and for each of them f is evaluated
giving top-level result u j . The resulting value is then obtained by the minimum among v0 and the
2Our calculus does not model the domain restriction construct in [46, 36].

10

F. DAMIANI AND M. VIROLI

values u j (which equates to v0 if there are currently no neighbours). Note that, since in a spreading
expression {e0 : f(@, e1 , ..., en )} the function f must be a diffusion and diffusions are pure functions
(cf. Section 3.1), only the root of the value-tree produced by the evaluation of the application of f to
the values of e1 , . . ., en must be stored (c.f. the conclusion of rule [E-SPR]). We will in the following
provide a network semantics taking care of associating to each device the set of neighbour trees
against which it performs a computation round, namely, connecting this operational semantics to the
actual network topology.
Example 3.5 (About device semantics). Consider the program P:
def real main() is { #src :

@ + #dist },

where #src and #dist are sensors of type real, and + is the built-in sum operator which has
type-signature real(real,real).
The evaluation of emain = { #src : @ + #dist } on a device ι1 when
• the current sensor-value map for ι1 is σ1 such that σ1 (#src) = 0 and σ1 (#dist) = 1, and
• ι1 has currently no neighbours,
(expressed by the judgement σ1 ; 0/ ` emain ⇓ θ1 ) yields the value-tree θ1 = 0(0, 1) by rule [E-SPR], since:
n = 1; the evaluation of e0 = #src yields η0V= 0() (by rule [E-SNS]); the evaluation of e1 = #dist
yields η1 = 1() (by rule [E-SNS]); m = 0; and {0} = 0.
Similarly, the evaluation of emain on a device ι2 when
• the current sensor-value map for ι2 is σ2 such that σ2 (#src) = 8 and σ2 (#dist) = 1, and
• ι2 has currently no neighbours,
(expressed by the judgement σ2 ; 0/ ` emain ⇓ θ2 ) yields the value-tree θ2 = 8(8, 1) by rule [E-SPR], since:
n = 1; the evaluation of e0 = #src yields η0V= 8() (by rule [E-SNS]); the evaluation of e1 = #dist
yields η1 = 1() (by rule [E-SNS]); m = 0; and {8} = 8.
Then, the evaluation of emain on a device ι3 when
• the current sensor-value map for ι3 is σ3 such that σ3 (#src) = 4 and σ3 (#dist) = 1, and
• ι3 has neighbours ι1 and ι2 ,
(expressed by the judgement σ3 ; θ1 θ2 ` emain ⇓ θ3 ) yields the value-tree θ3 = 1(4, 1) by rule [E-SPR],
since: n = 1; the evaluation of e0 = #src yields η0 = 4() (by rule [E-SNS]); the evaluation of
e1 = #dist yields η1 = 1() (by rule [E-SNS]); m = 2; the evaluation of 0 +V1 yields 1(0(), 1()) (by
rule [E-BLT]); the evaluation of 8 + 1 yields 9(0(), 8()) (by rule [E-BLT]); and {4, 1, 9} = 1.
3.2.2. Network Evolution. We now provide an operational semantics for the evolution of whole
networks, namely, for modelling the distributed evolution of computational fields over time. Figure
7 (top) defines key syntactic elements to this end. F models the overall computational field (state),
as a map from device identifiers to value-trees. τ models network topology, namely, a directed
neighbouring graph, as a map from device identifiers to set of identifiers. Σ models sensor (distributed)
state, as a map from device identifiers to (local) sensors (i.e., sensor name/value maps). Then, E
(a couple of topology and sensor state) models the system’s environment. So, a whole network
configuration N is a couple of a field and environment.
`
We define network operational semantics in terms of small-steps transitions of the kind N →
− N 0,
where ` is either a device identifier in case it represents its firing, or label ε to model any environment
change. This is formalised by the two rules in Figure 7 (bottom). Rule [N-FIR] models a network
evolution due to a computation round (firing) at device ι: it reconstructs the proper local environment,

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

System configurations and action labels:
F ::= ι  θ
τ ::= ι  I
Σ ::= ι  σ
E ::= τ, Σ
N ::= hE; Fi
` ::= ι ε

11

computational field
topology
sensors-map
environment
network configuration
action label

Environment well-formedness:
WFE(τ, Σ) holds if τ, Σ have same domain, and τ’s values do not escape it.
Transition rules for network evolution:
[N-FIR]

[N-ENV]

`

N→
− N

E = τ, Σ
τ(ι) = ι
Σ(ι); F(ι) ` emain ⇓ θ
ι
hE; Fi →
− hE; F[ι  θ ]i

WFE(E 0 )
E 0 = τ, ι1  σ1 , ..., ιn  σn
σ1 ; 0/ ` emain ⇓ θ1 · · · σn ; 0/ ` emain ⇓ θn
F0 = ι1  θ1 , ..., ιn  θn
ε
0
hE; Fi →
− hE ; F0 [F]i
Figure 7: Small-step operational semantics for network evolution
taking local sensors (Σ(ι)) and accessing the value-trees of ι’s neighbours;3 then by the single device
semantics we obtain the device’s value-tree θ , which is used to update system configuration. Rule
[N-ENV] models a network evolution due to change of the environment E to an arbitrarily new wellformed environment E 0 —note that this encompasses both neighborhood change and addition/removal
of devices. Let ι1 , ..., ιn be the domain of E 0 . We first construct a field F0 associating to all the
devices of E 0 the default value-trees θ1 , ..., θn obtained by making devices perform an evaluation with
no neighbours and sensors as of E 0 . Then, we adapt the existing field F to the new set of devices:
F0 [F] automatically handles removal of devices, map of new devices to their default value-tree, and
retention of existing value-trees in the other devices.
Example 3.6 (About network evolution). Consider a network of devices running the program P
of Example 3.5. The initial situation, when (the functionality associated to) the program P is
switched-off on all the devices, is modelled by the empty network configuration h0/  0,
/ 0/  0;
/ 0/  0i.
/
The network evolution representing the fact that the environment evolves because device ι3
switches-on when its sensor #src perceives value 0 and its sensor #dist perceives value 1 (and
gets initialised to the value-tree obtained by firing with respect to the empty set of neighbourhs), is
ε
modelled (according to rule [N-ENV]) by the reduction step h0/  0,
/ 0/  0;
/ 0/  0i
/ →
− hι3  0,
/ ι3  σ1 ; ι3 
θ1 i, where the sensor-value mapping σ1 and the value-tree θ1 are those introduced in Example 3.5.
Then, the network evolution representing the fact that the environment evolves is as follows:
• the device ι1 switches-on when its sensor #src perceives value 0 and its sensor #dist perceives
value 1, and has only ι3 as neighbour;
3The operational semantics abstracts from the details of message broadcast from/to neighbours: the most recent
value-trees received by a device ι from its neighbours while it was sleeping are identified with the value-trees associated to
the neighbours of the device ι when it fires.

12

F. DAMIANI AND M. VIROLI

• the device ι2 switches-on when its sensor #src perceives value 4 and its sensor #dist perceives
value 1, and has no neighbours, and
• on device ι3 sensor #src perceives value 8, sensor #dist perceives value 1, and ι3 has ι1 and ι2
as neighbours,
is modelled (according to rule
where

[N-ENV])

τ = ι1  {ι3 }, ι2  0,
/ ι3  {ι1 , ι2 },

ε

by the reduction step hι3  0,
/ ι3  σ1 ; ι3  θ1 i →
− hτ, Σ; Fi,

Σ = ι1  σ1 , ι2  σ2 , ι3  σ3 ,

F = ι1  θ1 , ι2  θ2 , ι3  θ1

and the sensor-value mapping σ2 , σ3 and the value-tree θ2 are those introduced in Example 3.5.
Finally, the network evolution representing the fact that device ι3 fires is modelled (according to
ι3
rule [N-FIR]) by the reduction step hτ, Σ; Fi −
→
hτ, Σ; ι1  θ1 , ι2  θ2 , ι3  θ3 i, where the value-tree θ2
is that introduced in Example 3.5.
3.3. The Self-stabilisation Property. Upon this semantics, we introduce the following definitions
and notations ending with the self-stabilisation property.
Initiality: The empty network configuration h0/  0,
/ 0/  0;
/ 0/  0i
/ is said initial.
`

`

`

`

n
1
2
Reachability: Write N =⇒ N 0 as short for N →
N1 →
··· →
N 0 . A configuration N is said reachable

`

if N0 =⇒ N where N0 is initial. Reachable configurations are the well-formed ones, and in the
following we shall implicitly consider only reachable configurations.
ι
Firing: A firing evolution from N to N 0 , written N =⇒ N 0 , is one such that N =⇒ N 0 for some ι,
namely, where only firings occur.
ι
Stability: A network configuration N is said stable if N →
− N 0 implies N = N 0 , namely, the computation of fields reached a fixpoint in the current environment. Note that if N is stable, then it also
holds that N =⇒ N 0 implies N = N 0 .
Fairness: We say that a sequence of device fires is k-fair (k ≥ 0) to mean that, for every h (1 ≤ h ≤ k),
the h-th fire of any device is followed by at least k − h fires of all the other devices. Accordingly,
ι
ι
a firing evolution N =⇒ N 0 is said k-fair, written N =⇒k N 0 , to mean that ι is k-fair. We also
ι
write N =⇒k N 0 if N =⇒k N 0 for some ι. This notion of fairness will be used to characterise
finite firing evolutions in which all devices are given equal chance to fire when all others had.
Strong self-stabilisation: A network configuration hE; Fi is said to (strongly) self-stabilise (simply,
self-stabilise, in the following) to hE; F 0 i if there is a k > 0 and a field F 0 such that hE; Fi =⇒k
hE; F 0 i implies hE; F 0 i is stable, and F 0 is univocally determined by E. Self-stability basically
amounts to the inevitable reachability of a stable state depending only on environment conditions,
through a sufficiently long fair evolution. Hence, the terminology is abused equivalently saying
that a program P or (equivalently) a field expression emain is self-stabilising if for any environment
state E there exists a unique stable field F 0 such that any hE; Fi self-stabilises to hE; F 0 i.
Self-stability: A network configuration hE; Fi is said self-stable to mean that it is stable and F is
univocally determined by E.
Note that our definition of self-stabilisation is actually a stronger version of the standard definition of
self-stabilisation as given e.g. in [22]—see more details in Section 10. Instead of simply requiring
that we enter a “self-stable set” of states and never escape from it, we require that (i) such a set has
a single element, and (ii) such an element is globally unique, i.e., it does not depend on the initial
state. Viewed in the context of an open system, it means that we seek for programs self-stabilising in
any environment independently of any intermediate computation state. This is a requirement of key

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

13

importance, since it entails that any subexpression of the program can be associated to a final and
stable field, reached in finite time by fair evolutions and adapting to the shape of the environment.
This acts as the sought bridge between the micro-level (field expression in program code), and the
macro-level (expected global outcome).
Example 3.7 (A self-stabilising program). Consider a network of devices running the program P of
Examples 3.5 and 3.6
def real main() is { #src :

@ + #dist },

and assume that the sensor #dist is guaranteed to always return a positive value (recall that
the sensors #src and #dist have type real and the built-in operator + has type-signature
real(real,real)). Then, the operator + is guaranteed to be used with type real(real, pr),
where pr is the type of positive reals (i.e., the refinement type [26] that refines type real by keeping
only the positive values), so that the following conditions are satisfied:
(1) + is monotonic nondecreasing in its first argument, i.e., for any v, v0 and v2 of type pr:
v ≤real v0 implies v + v2 ≤real v0 + v2 ;
(2) + is progressive in its first argument, i.e., for any v and v2 of type pr:
POSINF = POSINF + v2 , and v 6= POSINF implies v <real v + v2 .
Starting from an initial empty configuration, we move by rule [N-ENV] to a new environment with
the following features:
• the domain is formed by 2n (n ≥ 1) devices ι1 , ..., ιn , ιn+1 , ..., ι2n ;
• the topology is such that any device ιi is connected to ιi+1 and ιi−1 (if they exist);
• sensor #dist gives 1 everywhere;
• sensor #src gives 0 on the devices ιi (1 ≤ i ≤ n, briefly referred to as left devices) and a value u
(u > n + 1) on the devices ι j (n + 1 ≤ j ≤ 2n, briefly referred to as right devices).
Accordingly, the left devices are all assigned to value-tree 0(0, 1), while the right ones to u(u, 1):
hence, the resulting field maps left devices to 0 and right devices to 1—remember such evaluations
are done assuming nodes are isolated, hence the result is exactly the value of the source expression.
With this environment, the firing of a device can only replace the root of a value-tree, making it the
minimum of the source expression’s value and the successor of neighbour’s values. Hence, any firing
of a device that is not ιn+1 does not change its value-tree. When ιn+1 fires instead by rule [N-FIR], its
value-tree becomes 1(u, 1), and it remains so if more firings occur next.
Now, only a firing at ιn+2 causes a change: its value-tree becomes 2(u, 1). Going on this way,
it is easy to see that after any n-fair firing sequence the network self-stabilises to the field state
where left devices still have value-tree 0(u, 1), while right devices ιn+1 , ιn+2 , ιn+3 , ... have value-trees
1(u, 1), 2(u, 1), 3(u, 1), ..., respectively. That is, the root of such trees form a hop-count gradient,
measuring minimum distance to the source nodes, namely, the left devices.
It can also be shown that any environment change, followed by a sufficiently long firing sequence,
makes the system self-stabilise again, possibly to a different field state. For instance, if the two
connections of ι2n−1 to/from ι2n−2 break (assuming n > 2), the part of the network excluding ι2n−1
and ι2n keeps stable in the same state. The values at ι2n−1 and ι2n start raising instead, increasing of
2 alternatively until both reach the initial value-trees u(u, 1)—and this happens in finite time by a fair
evolution thanks to the local noetherianity property of stabilising diffusions. Note that the final state
is still the hop-count gradient, though adapted to the new environment topology.
Example 3.8 (A non self-stabilising program). An example of program that is not self-stabilising is
def real main() is { #src :

id(@) }

14

F. DAMIANI AND M. VIROLI

(written def real main() is { #src : @ } for short). There, the diffusion is the identity
function: real id(real x) is x, which (under the assumption, done in Example 3.7, that the
sensor #scr is guaranteed to return positive values) is guaranteed to be used with signature (pr)pr
and is not progressive in its first argument (c.f. condition (1) in Example 3.7).4
Assuming a connected network, and #src holding value vs in one node and POSINF in all others,
then any configuration where all nodes hold the same value v less than or equal to vs is trivially stable.
This would model a source gossiping a fixed value vs everywhere: if the source suddenly gossips a
value v0s smaller than v, then the network would self-organise and all nodes would eventually hold v0s .
However, if the source then gossips a value v00s greater than v0s , the network would not self-organise
and all nodes would remain stuck to value v0s .
4. S ORTS , S TABILISING D IFFUSIONS AND THE S TABILISING -D IFFUSION C ONDITION
In this section we state a sufficient condition for self-stabilisation. This condition is about the
behaviour of a diffusion (cf. Definition 3.2) on a subsets of its arguments (cf. Example 3.7). We first
introduce refinement types (or sorts) as a convenient way to denote these subsets (in Section 4.1)
and then use them to formulate the notion of stabilising diffusion (in Section 4.2) and the sufficient
condition for self-stabilisation (in Section 4.3).
4.1. Refinement Types (or Sorts). Refinement types [26] provide a mean to conservatively extend
the static type system of a language by providing the ability of specify refinements of each type. All
the programs accepted by the original type system are accepted by the refinement-type system and
vice-versa, but refinement-types provide additional information that support stating and checking
properties of programs. Following [17], we refer to refinement types as sorts and use terms like
subsorting and sort checking.
For instance, for the ground type real of reals we consider the six ground sorts nr (negative
reals), zr (the sort for 0), pr (positive reals), znr (zero or negative reals), zpr (zero or positive
reals), and real (each type trivially refines itself); while for the type bool we consider the thee sorts
false (the sort for FALSE), true (the sort for TRUE) and bool. Each sort-signature has the same
structure of the type-signature it refines. For instance, we can build 9(= 32 ) sort-signatures for the
type-signature bool(bool):
false(false), false(true), false(bool),
true(false), true(true), true(bool),
bool(false), bool(true), bool(bool).
We assume a mapping sorts(·) that associates to each type the (set of) sorts that refine it, and a
mapping sort-signatures(·) that associates to each type-signature the (set of) sort-signatures that
refine it (note that the latter mapping is determined by the the former, i.e., by the value of sorts(·)
on ground types). A type T trivially refines itself, i.e., for every type T it holds that T ∈ sorts(T).
Similarly, for every type-signature T(T) it holds that T(T) ∈ sort-signatures(T(T)). We write [[S]] to
denote the set of values of sort S. Note that, by construction:
for all S ∈ sorts(T) it holds that [[S]] ⊆ [[T]].
Sorts and sort-signatures express properties of expressions and functions, respectively. We say that:
4The function id is progressive whenever its is used with a signature of the form (real n)real n, where real n is
the refinement type that refines real n by keeping only the value n—in the example, this corresponds to the case when
the sensor #scr is guaranteed to always return the constant value n on all the devices.

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

15

Ground sorts:
sorts(bool) = false, true, bool
sorts(real) = nr, zr, pr, znr, zpr, real
Subsorting for ground sorts:

zpr

znr

bool
false

real

true

nr

zr

pr

Figure 8: Sorts and subsorting for the ground types used in the examples
• a value v has (or satisfies) sort S to mean that v ∈ [[S]] holds—we write sorts(v) to denote the set
of all the sorts satisfied by v, and
• a pure function f has (or satisfies) sort-signature S(S) to mean that for all v ∈ [[S]] it holds that
[[f]](v) ∈ [[S]]—we write sort-signatures(f) to denote the set of all the sort-signatures satisfied by
f.
For every sort S in sorts(T) we write ≤S to denote the restriction to [[S]] of the total order ≤T (cf.
Section 2.1) and write >S to denote the maximum element of [[S]] with respect to ≤S .
Subsorting is a partial order relation over sorts of each type that models the inclusion relationship
between them. For instance, each positive number is a zero or positive number, so will write nr ≤ znr
to indicate that nr is a subsort of znr. We require that the subsorting relation satisfies the following
(fairly standard) conditions:
(1) The type T is the maximum element with respect to subsorting relation on sorts(T).
(2) For every S1 , S2 ∈ sorts(T) there exists a least upper bound in sorts(T)—that we denote by
sup≤ (S1 , S2 ).
(3) For each value v the set of sorts sorts(type(v)) has a minimum element w.r.t. ≤.
(4) The subsorting relation is sound and complete according to the semantics of sorts, i.e.,
S ≤ S0 if and only if [[S]] ⊆ [[S0 ]].
Example 4.1. Figure 8 illustrates the sorts and the subsorting for the ground types used in the
examples introduced throughout the paper.
Subsigning is the partial order obtained by lifting subsorting to sort-signatures by the following
subsigning rule (which, as usual, is covariant in the result sort and contravariant in the argument
sorts):
0
[I-SIG]
S ≤ S0 S ≤ S
S(S) ≤ S0 (S0 )
According to the above explanations, for every type T and type-signature T(T) we have that both
(sorts(T), ≤) and (sort-signatures(T(T)), ≤) are partial orders.
4.2. Stabilising Diffusions. Recall the notion of diffusion (Definition 3.2). In this section we exploit
sorts to formulate the notion of stabilising diffusion: a predicate on the behaviour of a diffusion
that will be used to express the sufficient condition for self-stabilisation. The stabilising diffusion
predicate specifies constraints on the behaviour of a diffusion f of type T1 (T1 , ..., Tn ) by exploiting a
sort-signature S(S1 , ..., Sn ) ∈ sort-signatures(f).

16

F. DAMIANI AND M. VIROLI

Definition 4.2 (Stabilising diffusion). A diffusion f is stabilising with respect to the sort-signature
S(S1 S) ∈ sort-signatures(f) such that S ≤ S1 (notation stabilising(f, S(S1 S))) if the following
conditions hold:
(1) f is monotonic nondecreasing in its first argument, i.e., for all v ∈ [[S1 ]], v0 ∈ [[S1 ]] and v ∈ [[S]]:
v ≤S1 v0 implies [[f]](v, v) ≤S1 [[f]](v0 , v));
(2) f is progressive in its first argument, i.e., for all v ∈ [[S]]: [[f]](>S1 , v) =S1 >S1 and, for all
v ∈ [[S1 ]] − {>S1 }, v <S1 [[f]](v, v).
We say that the sort-signature S(S) is stabilising for f to mean that stabilising(f, S(S)) holds, and
write stabilising-sort-signatures(f) to denote set of the stabilising sort-signatures for f.
Example 4.3. Consider the library in Figure 2. The following predicates hold:
• stabilising(+, zr(zr, zr)),
• stabilising(+, pr(zpr, pr)),
• stabilising(+, real(real, pr)), and
• stabilising(restrictSum, real(real, pr, bool)).
Note that Condition (2) in Definition 4.2 introduces a further constraint between the sort of
the first argument S1 and the sort of the result S in the sort-signature S(S1 , ..., Sn ) used for f. For
instance, given the diffusion
def real f(real x, real y) is -(x+y)
the sort signature nr(pr, pr) ∈ sort-signatures(f) ⊂ sort-signatures(real(real, real)) is not
compatible with Condition (2), since v1 , v2 ∈ [[pr, pr]] and v = [[f]](v1 , v2 ) ∈ nr imply v1 6≤ v.
Namely, the sort of the result S and the sort of the first argument S1 must be such that [[S]] ⊆progressive
[[S1 ]], where the relation ⊆progressive between two subsets S and S1 of [[T]] (i.e., between elements of
the powerset P([[T]])), that we call progressive inclusion, is defined as follows:
S ⊆progressive S1

if and only if

S ⊆ S1

>S = >S1 .

and

≤progressive

We write
to denote the progressive subsorting relation, which is the restriction of subsorting relation defined as follows:
S ≤progressive S0 if and only if [[S]] ⊆progressive [[S0 ]].
To summarise: if a sort signature S(S) is stabilising for some diffusion, then S(S) must be progressive,
according to the following definition.
Definition 4.4 (Progressive sort-signature). A sort-signature S(S) with S = S1 , ..., Sn (n ≥ 1) is a
progressive sort-signature (notation progressive(S(S))) if S ≤progressive S1 .
Given
a
diffusion
type-signature
T(T)
(cf.
Definition
3.2)
we
write
progressive-sort-signatures(T(T)) to denote the (set of) progressive sort-signatures that
refine it.
Example 4.5. Figure 9 illustrates the progressive subsorting for the ground sorts used in the examples
introduced throughout the paper.
The following partial order between progressive sort-signatures, that we call stabilising subsigning:

0

S ≤progressive S0 S01 ≤progressive S1 S ≤ S
0
S(S1 S) ≤stabilising S0 (S01 S )
captures the natural implication relation between stabilisation properties, as stated by the following
proposition.
[I-S-SIG]

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

17

real

false

zpr

znr

bool
true

nr

zr

pr

Figure 9: Progressive subsorting for the ground sorts used in the examples (cf. Figure 8)
Proposition 4.6 (Soudness of stabilising subsigning). If stabilising(f, S(S)) and S(S) ≤stabilising
0
S0 (S ), then stabilising(f, S0 (S0 )).
Proof. Straightforward from Definition 4.2 and the definition of progressive subsigning (Rule [I-S-SIG]
above).
4.3. The Stabilising-Diffusion Condition. We have now all the ingredients to formulate a sufficient
condition for self-stabilisation of a well-typed program P, that we call the stabilising-diffusion
condition: any diffusion f used in a spreading expression e of the program (or library) P must be
a stabilising diffusion with respect a sort-signature for f that correctly describes the sorts of the
arguments of f in e. More formally, a well-typed program (or library) P satisfies the stabilisingdiffusion condition if and only if it admits valid sort-signature and stabilising assumptions for
diffusions. I.e., for each diffusion-expression {e1 : f(@, e2 , ..., en )} occurring in P, there exists a
sort-signature S(S1 , . . . , Sn ) such that the following two conditions are satisfied.
(1) Validity of the sort-signature assumption: the diffusion f has sort-signature S(S1 , . . . , Sn ) and,
in any reachable network configuration, the evaluation of the subexpression ei yields a value
vi ∈ [[Si ]] (1 ≤ i ≤ n).
(2) Validity of the stabilising assumption: the sort-signature S(S1 , . . . , Sn ) is stabilising for the
diffusion f.
Example 4.7. In the body of the function main in Example 3.7, which defines a self-stabilising field:
(1) the diffusion function + is applied according to the sort-signature real(real, pr) since its
second argument is the sensor #dist of type real that is guaranteed to always return a value of
sort pr; and
(2) stabilising(+, real(real, pr)) holds (cf. Example 4.3).
Therefore, the stabilising diffusion condition is satisfied. Also the library in Figure 2 satisfies the
stabilising diffusion condition.
Instead, for the diffusion function id of type-signature real(real) used in the non-selfstabilising spreading expression considered in Example 3.8, S(S1 ) = zr(zr) is the only sort-signature
such that stabilising(id, S(S1 )) holds.5 Therefore, since the sensor #src returns a value of sort pr,
the stabilising diffusion condition cannot be satisfied.
Remark 4.8 (On choosing the refinements of type real). The choice of the refinements for type
real that we considered in the examples is somehow arbitrary. We have chosen a set of refinements
that is expressive enough in order the show that all the self-stabilising examples considered in the
paper satisfy the stabilising-diffusion condition. For instance, dropping the refinements nr and
5Considering the sorts given in Figure 8—c.f. the footnote in Example 3.8.

18

F. DAMIANI AND M. VIROLI

pr would make it impossible to show that the program considered in Example 3.7 satisfies the
stabilising-diffusion condition.
Considering a richer set of refinement would allow to prove more properties of programs (and
would make the check more complex). For instance, adding the refinement npr (negative or positive
number) such that:
nr ≤ npr
pr ≤ npr
npr ≤ real
would allow to assign (according to the sort-checking rules presented in Section 8) sort npr to the
expressions (x ? -1 : 1), to assume sort-signature false(zr, npr) for the built-in equality
operator on reals =, and therefore to check that the user-defined function
def <bool> f(<bool> x) is 0 = (x ?

-1 :

1)

has sort-signature false(bool). Although, this would allow to show that more program satisfies
the stabilising-diffusion, the refinement npr is not needed in order to show that the self-stabilising
examples considered in the paper satisfy the stabilising-diffusion condition. Therefore we have not
considered it in the examples.

5. P ROGRAMS THAT S ATISFY THE S TABILISING -D IFFUSION C ONDITION S ELF - STABILISE
In this section we prove the main properties of the proposed calculus, namely: type soundness and
termination of device computation (in Section 5.1), and self-stabilisation of network evolution for
programs that satisfy the stabilising-diffusion condition (in Section 5.2).
As already mentioned, our notion of self-stabilisation is key as it allows one to conceptually
map any (self-stabilising) field expression to its final and stable field state, reached in finite time by
fair evolutions and adapting to the shape of the environment. This acts as the sought bridge between
the micro-level (field expression in program code), and the macro-level (expected global outcome).
In order facilitate the exploitation of this bridge it would be useful to have an effective means for
checking the stabilising-diffusion condition. A technique providing such an effective means (for the
extension of the calculus with pairs introduced in Section 6) is illustrated in Sections 7, 8 and 9.
5.1. Type Soundness and Termination of Device Computation. In order to state the properties
of device computation we introduce the notion of set of well-typed values trees for an expression.
Given an expression e such that x : T ` e : T, the set WTVT(x : T, e, T) of the well-typed valuetrees for e, is inductively defined as follows: θ ∈ WTVT(x : T, e, T) if there exist
• a sensor mapping σ ;
• well-formed tree environments θ ∈ WTVT(x : T, e, T); and
• values v such that length(v) = length(x) and 0/ ` v : T;
such that σ ; θ ` e[x := v] ⇓ θ holds—note that this definition is inductive, since the sequence of
evaluation trees θ may be empty.
As this notion is defined we can state the following two theorems, guaranteeing that from a
properly typed environment, evaluation of a well-typed expression yields a properly typed result and
always terminates, respectively.
Theorem 5.1 (Device computation type preservation). If x : T ` e : T, σ is a sensor mapping,
θ ∈ WTVT(x : T, e, T), length(v) = length(x), 0/ ` v : T and σ ; θ ` e[x := v] ⇓ θ , then 0/ ` ρ(θ ) : T.
Proof. See Appendix A.

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

19

Theorem 5.2 (Device computation termination). If x : T ` e : T, σ is a sensor mapping, θ ∈ WTVT(x :
T, e, T), length(v) = length(x) and 0/ ` v : T, then σ ; θ ` e[x := v] ⇓ θ for some value-tree θ .
Proof. See Appendix A.
The two theorems above guarantee type-soundness and termination of device computations, that
is: the evaluation of a well-typed program on any device completes without type errors assuming that
the values received from the sensors and the values in the value trees received from the neighbours
are well-typed.
5.2. Self-stabilisation of Network Evolution for Programs that Satisfy the StabilisingDiffusion Condition. On top of the type soundness and termination result for device computation
we can prove the main technical result of the paper: self-stabilisation of any program that satisfies
the stabilising-diffusion condition.
Theorem 5.3 (Network self-stabilisation for programs that satisfy the stabilising-diffusion condition).
Given a program with valid sort and stabilising diffusion assumptions, every reachable network
configuration N self-stabilises, i.e., there exists k ≥ 0 such that N =⇒k N 0 implies that N 0 is self-stable.
Proof. See Appendix B.
We conclude this section by giving an outline of the proof of Theorem 5.3. To this aim we first
introduce some auxiliary definitions.
Auxiliary Definitions. In the following we omit the subscript S in <S and ≤S when it is clear from
the context (i.e., we just write < and ≤).
Given a network N with main expression e, we write θι(in N) to denote the value-tree of e
on device ι in the network configuration N, and write vι(in N) to denote the value ρ(θι(in N) ) of e
on device ι in the network configuration N. Moreover, when e = {e0 : f(@, e1 , . . . , en )} we write
θ j,ι(in N) and write v j,ι(in N) to denote the value-tree and the value of e j (0 ≤ j ≤ n), respectively. In
the following we omit to specify the network configuration N when is is clear from the context, i.e.,
we simply write θι , vι , θ j,ι and v j,ι .
We say that a device ι is stable in N to mean that N =⇒ N 0 implies θι(in N) = θι(in N 0 ) . Note that
the following three statements are equivalent:
• N is stable.
• All the devices of N are stable.
• N =⇒ N 0 implies N = N 0 .
We write environment(N) to denote the environment E of a network configuration N = hE; Fi. We
say that a device ι is self-stable in a network N to mean that it is stable and its value is univocally
determined by environment(N). Note that a network is self-stable if and only if all its devices are
self-stable.
We say that a network N with main expression e = {e0 : f(@, e1 , . . . , en )} is pre-stable to mean
that for every device ι in N:
(1) the subexpressions ei (0 ≤ i ≤ n) are stable, and
(2) vι ≤ v0,ι .

20

F. DAMIANI AND M. VIROLI

We say that the network N is pre-self-stable to mean that it is pre-stable and the value trees of the
subexpressions ei (0 ≤ i ≤ n) are self-stable (i.e, they are univocally determined by environment(N)).
Note that pre-stability is preserved by firing evolution (i.e., if N is pre-stable and N =⇒ N 0 , then N 0
is pre-stable).
An Outline of the Proof of Theorem 5.3. The proof is by induction on the syntax of closed expressions
e and on the number of function calls that may be encountered during the evaluation of e. Let e be the
main expression of N and E = environment(N). The only interesting case is when e is a spreading
expression {e0 : f(@, e1 , . . . , en )}. By induction there exists h ≥ 0 such that if N =⇒h N1 then on
every device ι, the evaluation of e0 , e1 , . . . , en produce stable value-trees θ0,ι , θ1,ι , . . . , θn,ι , which
are univocally determined by E. Note that, if N =⇒h+1 N2 then N2 is pre-self-stable. Therefore we
focus on the case when N is pre-self-stable. The proof of this case is based on the following auxiliary
results (which corresponds to Lemmas B.1-B.6 of Appendix B).
B.1 (Minimum value): Any 1-fair evolution N =⇒1 N 0 increases the value of any not self-stable
device ι in N such that vι(in N) is minimum (among the values of the devices in N). The new value
vι(in N 0 ) is such that there exists a value v0 such that vι(in N) < v0 ≤ vι(in N 0 ) and in any subsequent
firing evolution N 0 =⇒ N 00 the value of the device ι will be always greater or equal to v0 (i.e.,
v0 ≤ vι(in N 00 ) ).
B.2 (Self-stabilisation of the minimum value): Let S1 be the subset of the devices in N such that
v0,ι is minimum (among the values of e0 in the devices in N). There exists k ≥ 0 such that any
k-fair evolution N =⇒k N 0 is such that
(1) each device ι in S1 is self-stable in N 0 .
(2) in N 0 each device not in S1 has a value greater or equal then the values of the devices in S1
and, during any firing evolution, it will always assume values greater than the values of the
devices in S1 .
B.3 (Frontier): Let D be a set of devices. Given a set of stable devices S ⊆ D we wrote frontierS (D)
to denote the subset of the devices ι ∈ D − S such that there exists a device ι 0 ∈ S such that ι 0 is a
neighbour of ι. If D are devices of the network and S satisfies the following conditions
(i) the condition obtained form condition (1) above by replacing S1 with S,
(ii) the condition obtained form condition (2) above by replacing S1 with S, and
(iii) frontierS (D) 6= 0,
/
then any 1-fair evolution makes the devices in frontierS (D) self-stable.
B.4 (Minimum value not in S): If D are devices of the network and S satisfies conditions (i)-(iii)
above, satisfies the following condition
(iv) each device in frontierS (D) is self-stable in N, and
M ⊆ D − S is the set of devices ι such that vι(in N) is minimum (among the values of the devices
in D − S), and M ∩ frontierS (D) = 0,
/ then any 1-fair evolution N =⇒1 N 0 increases the value of
any not self-stable device ι in M. The new value vι(in N 0 ) is such that there exists a value v0 such
that vι(in N) < v0 ≤ vι(in N 0 ) and in any subsequent firing evolution N 0 =⇒ N 00 the value of the
device ι will be always greater or equal to v0 (i.e., v0 ≤ vι(in N 00 ) ).
B.5 (Self-stabilisation of the minimum value not in S): If D are devices of the network and S
satisfies conditions (i)-(iv) above, and M ⊆ D − S is the set of devices ι such that vι(in N) is
minimum (among the values of the devices in D − S), then there exists k ≥ 0 such that any k-fair
evolution N =⇒k N 0 is such that there exists a device ι1 in D − S such that S1 = S ∪ {ι1 } satisfies
the conditions (1) and (2) above.

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

T ::= G <T, T>
e ::= · · · <e, e>

21

type

fst e

snd e

expression

Figure 10: Extensions to the syntax of types and expressions (in Fig. 1) to model pairs
B.6 (Pre-self-stable network self-stabilization): For every reachable pre-self-stable network configuration N there exists k ≥ 0 such that N =⇒k N 0 implies that N 0 is self-stable. This sixth
auxiliary result, which concludes our proof outline, follows from the previous five auxiliary
results. The idea is to consider the auxiliary results B.2, B.3 and B.5 as reasoning steps that may
be iterated. We start by applying the auxiliary result B.2 to produce a non-empty set of devices
S1 that satisfies conditions (1) and (2) above. Then, we rename S1 to S and iterate the following
two reasoning steps until the set of devices S is such that frontierS (D) = 0:
/
• apply the auxiliary results B.3 and B.5 to produce a non-empty set of devices S1 that satisfies
conditions (1) and (2) above; and
• rename S1 to S.
Clearly the number of iterations is finite (note that S = D implies frontierS (D) = 0).
/ If S = D we
have done. Otherwise note that, since frontierS (D) = 0,
/ the evolution of the devices in D − S is
independent from the devices in S. Therefore we we can iterate the whole reasoning (i.e., starting
from the auxiliary result B.2) on the the portion of the network with devices in D − S.
6. E XTENDING THE C ALCULUS WITH PAIRS
The calculus presented in Sections 2 and 3 does not model data structures. In this section we
point out that the definitions and results presented in Sections 4 and 5 are parametric in the set
of modeled types by considering an extension of the calculus that models the pair data structure.
Recent works, such as [8], show that the ability of modelling pairs of values is key in realising
context-dependent propagation of information, where along with distance one let the computational
field carry additional information as gathered during propagation. In fact, pairs are needed for
programming further interesting examples (illustrated in Section 6.2), and their introduction here is
useful to better grasp the subtleties of our checking algorithm for self-stabilisation, as described in
next sections.
6.1. Syntax. The extensions to the syntax of the calculus for modeling pairs are reported in Figure 10.
Now types include pair types (like <real,bool>, <real,<bool,real>>,... and so on), expressions
include pair construction (<e, e>) and pair deconstruction (fst e or snd e), and values includes pair
values (<1,TRUE>, <2,3.5>, <<1,FALSE>,3>,... and so on).
The ordering for ground types has to be somehow lifted to non-ground types. A naural choice
for pairs is the lexicographic preorder, i.e, to define <v1 , v2 > ≤<T1 ,T2 > <v01 , v02 > if either v1 <T1 v01
holds or both v1 = v01 and v2 ≤T2 v02 hold.
6.2. Examples. In this section we build on the examples introduced in Section 2.2 and show how
pairs can be used to program further kinds of behaviour useful in self-organisation mechanisms in
general, and also in the specific case of crowd steering, as reported in Figure 11.
The fourth function in Figure 11, called sector, can be used to keep track of specific situations
during the propagation process. It takes a zero-field source i (a field holding value 0 in a “source”,
as usual) and a boolean field c denoting an area of interest: it creates a gradient of pairs, orderly

22

F. DAMIANI AND M. VIROLI

def <real,bool> sum or(<real,bool> x, <real,bool> y) is <fst x + fst y, snd x or snd y>
def <real,bool> pt POSINF TRUE(<real, bool> x) is ((fst x)=POSINF) ? <POSINF,TRUE> :

x

def <real,bool> sd sum or(<real,bool> x, <real,bool> y) is pt POSINF TRUE(sum or(x,y))
def bool sector(real i, bool c) is snd { <i, c> :

sum or(@,<#dist,c>) }

def <real,real> add to 1st(<real,real> x, real y) is <fst x + y, snd x>
def <real,real> pt POSINF POSINF(<real, real> x) is ((fst x)=POSINF) ? <POSINF,POSINF> :

x

def <real,real> sd add to 1st(<real,real> x, real y) is pt POSINF POSINF(add to 1st(x,y))
def <real,real> gradcast(real i, real j) is { <i, j> :

add to 1st(@, #dist) }

def real dist(real i, real j) is gradcast(restrict(j,j==0),grad(i))
def bool path(real i, real j, real w) is (grad(i)+grad(j))+(-w) < dist(i, j)
def real channel(real i, real j, real w) is gradobs(grad(j),not path(i, j, w))

Figure 11: Definitions of examples using pairs (see Fig. 2 for the definitions of functions restrict,
grad and gradobs)

Figure 12: Pictorial representation of sector field (left), partition (center) and channel field (right)
holding distance from source and a boolean value representing whether the route towards the source
crossed area c. As one such gradient is produced, it is wholly applied to operator snd, extracting a
sector-like boolean field as shown in Figure 3 (left). To do so, we use a special diffusion function
sum or working on real,bool pairs, which sums the first components, and apply disjunction to the
second. In crowd steering, this pattern is useful to make people be aware of certain areas that the
proposed path would cross, so as to support proper choices among alternatives [37]. Figure 12 (left)
shows a pictorial representation.
However, our self-stabilisation result reveals a subtlety. Function sum or has to be tuned by
composing it with pt POSINF TRUE (which propagates the top value from the first to the second
component of the pair), leading to function sd sum or (which is a stabilising diffusion). This is
needed to make sure that the top value <POSINF,TRUE> of pairs of type <real,bool> is used when
distance reaches POSINF: this is required to achieve progressiveness, and hence self-stabilisation.
Without it, in the whole area where distance is POSINF we would have a behaviour similar to that
of Example 3.8: in particular, if c is true and i is POSINF everywhere, both states where all nodes
have second component equal to true (state s1 ) and where all nodes have second component equal
or false (state s2 ) would be stable, and an even temporaneous flip of c to false in some node
would make the system inevitable move to s2 —a clear indication of non self-stabilisation.
Note that sector function can be easily changed to propagate values of any sort by changing
the type of the second component of pairs, and generalising over the or function. E.g., one could
easily define a spreading of “set of values” representing the obstacles encountered during the spread.

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

T ` e1 : T1 T ` e2 : T2
T ` <e1 , e2 > : <T1 , T2 >

[T-PAIR]

T ` e : <T1 , T2 >
T ` fst e : T1

[T-FST]

23

T ` e : <T1 , T2 >
T ` snd e : T2

[T-SND]

Figure 13: Type-checking rules for pair construction and deconstruction expressions (cf. Fig. 4)
Another interesting function working on pairs is gradcast, that is useful to let a gradient carry
some information existing in the source. Expression gradcast(i,j), where i is a 0-field as usual,
results in a field of pairs in which the first component is the minimum distance from a source and the
second component is the value of j at that source. Assuming j is a field of unique values in each
node, e.g. a unique identifier ID, gradcast performs a partitioning behaviour (namely, a so-called
Voronoi partition): its second component forms a partition of the network into regions based on
“closeness” to sources, and each region of the partition holds the value of j in that source; first
component still forms a gradient towards such sources. See Figure 12 (center). Again, function
add to 1st has to be changed to sd add to 1st to preserve self-stabilisation.
The remaining functions dist, path and channel are used to obtain a spatial pattern more
heavily relying on multi-level composition, known as channel [46, 36]. Assume i and j are 0fields, and suppose to be willing to steer people in complex and large environments from area i to
destination j, i.e., from a node where i holds 0 to a node where j holds 0. Typically, it is important
to activate the steering service (spreading information, providing signs, and detecting contextual
information such as congestion) only along the shortest path, possibly properly extended of a distance
width w to tolerate some randomness of people movement—see Figure 12 (right). Function dist
uses gradcast to broadcasts the distance d between i and j—i.e., the minimum distance between a
node where i holds 0 and a node where j holds 0. This is done by sending a gradcast from the source
of j holding the value of grad(i) there, which is exactly the distance d. Function path simply
marks as positive those nodes whose distance from the shortest path between i and j is smaller than
w. Finally, function channel generates from j a gradient confined inside path(i,j,w), which can
be used to steer people towards the POI at j without escaping the path area.
6.3. Type checking. The typing rules for pair construction and deconstruction expressions are given
in Figure 13. Note that adding these rules to the rules in Fig. 4 preserves the property that no choice
may be done when building a derivation for a given type-checking judgment, so the type-checking
rules straightforwardly describe a type-checking algorithm (cf. end of Section 3.1).
Example 6.1. Consider the library in Figure 11. The following predicates hold:
• diffusion(sum or),
• diffusion(sd sum or),
• diffusion(add to 1st), and
• diffusion(sd add to 1st)
Example 6.2. The library in Figure 11 type checks by using the ground types, sensors, and typesignatures for built-in functions in Figure 5.
6.4. Device Computation. The big-step operational semantics rules for pair construction and
deconstruction expressions are given in Figure 14. Note that they are syntax directed (in particular,
the first premise of rule [E-PAIR] ensures that there is no conflict with rule [E-VAL] of Fig. 6).

24

F. DAMIANI AND M. VIROLI

v ::= g

<v, v>

value

[E-PAIR]

<e1 , e2 > not a value σ ; π1 (θ ) ` e1 ⇓ η1 σ ; π2 (θ ) ` e2 ⇓ η2 v1 = ρ(η1 ) v2 = ρ(η2 )
σ ; θ ` <e1 , e2 > ⇓ <v1 , v2 >(η1 , η2 )
[E-FST]

[E-SND]

σ ; π1 (θ ) ` e ⇓ η <v1 , v2 > = ρ(η)
σ ; θ ` fst e ⇓ v1 (η)

σ ; π1 (θ ) ` e ⇓ η <v1 , v2 > = ρ(η)
σ ; θ ` snd e ⇓ v2 (η)

Figure 14: Big-step operational semantics for pair construction and deconstruction expressions (cf.
Fig. 6)
6.5. Sorts. Each sort has the same structure of the type it refines. For instance, considering the sorts
for ground types given in Figure 8, we can build 36(= 62 ) pair sorts for the pair type <real, real>:
<nr, nr>,
..
.
<real, nr>,

<nr, znr>,
..
.
<real, znr>,

<nr, zr>,
..
.
<real, zr>,

<nr, zpr>,
..
.

<nr, pr>,
..
.

<nr, real>
..
.
<real, zpr>, <real, pr>, <real, real>

and 108(36 ∗ 3) sorts for the type <<real, real>, bool>:
<<nr, nr>, false>,

<<nr, znr>, false>,

...,

<<real, real>, bool>.

Subsorting between ground sorts can be lifted to the sorts for non-ground types by suitable
subsorting rules. The following subsorting rule:
S1 ≤ S01 S2 ≤ S02
<S1 , S2 > ≤ <S01 , S02 >

[I-PAIR]

lifts subsorting between ground sorts to pair sorts by modelling pointwise ordering on pairs. Note that
the subsorting relation is determined by the subsorting for ground sorts. Using the inclusions nr ≤ znr
and true ≤ bool, and the above rule it is possible to derive, e.g., the inclusion <<nr, nr>, true> ≤
<<nr, znr>, bool>. Note that no choice may be done when building a derivation for a given
subsorting judgment S1 ≤ S2 , so the subsorting rules (i.e, the rule [I-PAIR] and the subsorting for
ground sorts) describe a deterministic algorithm.
Similarly, progressive subsorting between ground sorts is lifted to pair-sorts by the following
progressive subsorting rule:
[P-I-PAIR]

S1 ≤progressive S01 S1 ≤progressive S01
<S1 , S2 > ≤progressive <S01 , S02 >

which (together with the progressive subsorting for ground sorts) describes a deterministic algorithm.
6.6. Stabilising Diffusion predicate and Properties. The stabilising diffusion predicate (Definition 4.2) and the stabilising diffusion condition (Section 4.3) are parametric in the set of types
modeled by the calculus.
Example 6.3. The library in Figure 11 satisfies the stabilising diffusion condition. In particular, the
following predicates hold:
• stabilising(sd sum or, <real, bool>(<real, bool>, <pr, bool>)), and
• stabilising(sd add to 1st, <real, real>(<real, real>, pr)).

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

25

The statements of device computation type preservation (Theorem 5.1), device computation
termination (Theorem 5.2), and network self-stabilisation for programs with valid sort and stabilising
assumptions (Theorem 5.3) are parametric in the set of types modeled by the calculus. The proofs
(see Appendix A and Appendix B) are indeed given for the calculus with pairs—the cases for pair
construction and deconstruction are straightforward by induction. The rest of the paper considers
the calculus with pairs—in particular, the rules for checking sort and stabilising assumptions for
diffusions are able to check the examples presented in Section 6.2.
7. O N C HECKING THE S TABILISING -D IFFUSION C ONDITION
The rest of the paper is devoted to illustrate a type-based analysis for checking the stabilising-diffusion
condition (cf. Section 4.3) for the extension of the calculus with pairs introduced in Section 6.
7.1. A Type-based approach for checking the Stabilising-Diffusion Condition. Recall that the
stabilising-diffusion condition consists of two parts:
• validity of the sort-signature assumptions (Condition (1) of Section 4.3; and
• validity of the stabilising assumptions (Condition (2) of Section 4.3).
In order to check the stabilising-diffusion condition we assume that each program P comes with:
• a non-empty set of sort-signature assumptions s-sigs(f) for each function f; and
• a possibly empty set of stabilising sort-signature assumptions stb-s-sigs(f) for each diffusion f.
The assumptions s-sigs(b) and stb-s-sigs(b) for the built-in functions b are considered valid—they
should come with the definition of the language. Instead, the validity of the assumptions s-sigs(d)
and stb-s-sigs(d) for the user-defined functions d must be checked—these assumptions could be
either (possibly partially) provided by the user or automatically inferred.6
7.1.1. On checking Condition (1) of Section 4.3. Section 8 introduces a sort-checking system that
checks Condition (1) of Section 4.3. Namely, given a program (or library) P, it checks that: (i) each
user-defined function d in P has all the sort signatures in s-sigs(d) and, if d is a diffusion, it has
also the sort signatures in stb-s-sigs(d); and (ii) every diffusion-expressions {e1 : f(@, e2 , ..., en )}
occurring in P is sort-checked by considering for f only the sort-signatures in stb-s-sigs(f). The
soundness of the sort-checking system (shown in Section 8.6) guarantees that, if the check is passed,
then for every diffusion-expressions {e1 : f(@, e2 , ..., en )} occurring in the P there is a sort-signature
S(S1 , . . . , Sn ) ∈ stb-s-sigs(f) such that the evaluation of the subexpression ei yields a value vi ∈ [[Si ]]
(1 ≤ i ≤ n). I.e., Condition (1) of Section 4.3 holds.
6The naive inference approach, that is: inferring s-sigs(d) by checking all the possible refinements of the type-signature
of d is linear in the number of elements of sort-signatures(t-sig(d)). Some optimizations are possible. We do not address
this issue in the paper.

26

F. DAMIANI AND M. VIROLI

7.1.2. On checking Condition (2) of Section 4.3. Note that, if Condition (1) of Section 4.3 has
been checked by the sort-checking system of Section 8, then in order to check Condition (2) of
Section 4.3 holds it is enough to check that for each user-defined diffusion d, each sort-signature
S(S1 , . . . , Sn ) ∈ stb-s-sigs(d) is stabilising for d.
In order to check that for each user-defined diffusion d of signature T1 (T1 , . . . , Tn ) each sortsignature S(S1 , . . . , Sn ) ∈ stb-s-sigs(d) is stabilising for d, we introduce additional requirements.
Namely, we require that for every user-defined diffusion d such that stb-s-sigs(d) 6= 0:
/
0
(1) there exists a sort-signature S(· · · ) ∈ stb-s-sigs(d) such that S (· · · ) ∈ stb-s-sigs(d) implies
S ≤progressive S0 ; and
(2) if T1 is not ground (i.e., if it is a pair type), then the user-defined diffusion d is of the form
def T1 d(T1 x1 , . . . , Tn xn ) is pt[>S ](f(x1 , . . . , xn ))

(7.1)

where
• pt[>S ] (defined in Section 7.2) is a pure function of sort-signature S(S),
• f is a diffusion, and
• if f is user-defined then stb-s-sigs(f) = 0.
/
Note that the above additional requirements can be checked automatically.
In the rest of this section we first (in Section 7.2) introduce some auxiliary definitions (including,
for each sort S, the definition of the pure function pt[>S ]); then (in Section 7.3) we introduce the
notion of !-prestabilising diffusion with respect to a progressive sort-signature S(S1 , . . . , Sn ) and
show that
• S ground implies that: if S(S1 , . . . , Sn ) is !-prestabilising for the user-defined diffusion d then
S(S1 , . . . , Sn ) is stabilising for d;
• if S(S1 , . . . , Sn ) is !-prestabilising for the diffusion f then S(S1 , . . . , Sn ) is stabilising for the userdefined diffusion d displayed in Equation 7.1; and
finally (in Section 7.4) we introduce annotated sort-signatures and annotated sorts as convenient
notations to be used in writing type-based rules for checking !-prestabilisation.
Section 9 introduces an annotated sort checking system that checks that for each user-defined
diffusion d of signature T1 (T1 , . . . , Tn ) and for each sort-signature S(S1 , . . . , Sn ) ∈ stb-s-sigs(d):
• S ground implies that S(S1 , . . . , Sn ) is !-prestabilising for d; and
• S not ground implies that S(S1 , . . . , Sn ) is !-prestabilising for the diffusion f occurring in Equation 7.1.
The soundness of the annotated sort checking system (shown in Section 9.5) guarantees that, if the
check is passed, then Condition (2) of Section 4.3 holds.
7.2. Auxiliary definitions. For any type T the leftmost-as-key preorder ≤1T is the preorder that
weakens the order ≤T by considering each pair as a record where the leftmost ground element is the
key. It is defined by:
• v ≤1T v0 if v ≤T v0 , where T is a ground type; and
• <v1 , v2 > ≤1<T1 ,T2 > <v01 , v02 > if v1 ≤1T1 v01 .
Note that that the leftmost-as-key preorder is total, i.e., for every v, v0 ∈ [[T]] we have that either
v ≤1T v0 or v0 ≤1T v holds. We write v =1T v0 to mean that both v ≤1T v0 and v0 ≤1T v hold. Of course
v =1T v0 does not imply v =T v0 . Note also that v <1T v0 implies v <T v0 .
For every sort S of T, we wrote ≤1S to denote the restriction of ≤1T to [[S]]. According to the
previous definition, we define the key of a sort S as the the leftmost ground sort occurring in S,

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

27

and the key of a value v as the the leftmost ground value occurring in v. The key mappings can be
inductively defined as follows:
• key(S) = S, if S is a ground sort
• key(S) = key(S1 ), if S = <S1 , · · · >
and
• key(v) = v, if v is a ground value
• key(v) = key(v1 ), if v = <v1 , · · · >.
Note that, for every v and v0 of sort S it holds that:
v ≤1S v0

if and only if

key(v) ≤key(S) key(v0 ).

(7.2)

For every sort S of type T we write pt[>S ] to denote the pure function (which satisfies the
sort-signature S(S)), that maps the elements v such that v =1S >S to >S (i.e., that propagates the
top value from the key of a pair value to all the other components of the value), and is the identity
otherwise. Note that the function pt[>S ] can be inductively defined as: def T pt[>S ](T x) is e,
where

x
if S is ground
e=
0
0
pt[>S ](fst x) = >S ) ? >S : x if >S = <>S0 , · · · >
For every diffusion f with signatureT1 (T1 , . . . , Tn ) and sort signature S(S1 , . . . , Sn ) (n ≥ 1) we
write sd[f, >S ] to denote the composition of f and pt[>S ], which is the diffusion (which satisfies the
sort-signature S(S1 , . . . , Sn )) defined as follows:
def T1 sd[f, >S ](T1 x1 , . . . , Tn xn ) is pt[>S ](f(x1 , . . . , xn ))
7.3. !-Prestabilising Diffusions and ?-Prestabilising Diffusions. A π-prestabilising diffusion is
a diffusion whose progressiveness behaviour is expressed by the annotation π that ranges over ! (for
certainly prestabilising) and ? (for possibly prestabilising), as illustrated by the following definition.
Definition 7.1 (π-prestabilising diffusion). A diffusion f is π-prestabilising with respect to the
progressive sort signature S(S1 S) ∈ sort-signatures(f) (notation π-prestabilising(f, S(S1 S))) if for
any v ∈ [[S]]:
(1) if π = ! then
• v <1S1 v0 and [[f]](v, v) = v00 6=1S1 >S1 imply v00 <1S1 [[f]](v0 , v);
• for all v ∈ [[S1 ]] − {>S1 }, v <1S1 [[f]](v, v);
(2) if π ∈ {!, ?} then
• v ≤1S1 v0 implies [[f]](v, v) ≤1S1 [[f]](v0 , v);
• for all v ∈ [[S1 ]], v ≤1S1 [[f]](v, v).
We say that the sort-signature S(S) is π-prestabilising for f to mean that π-prestabilising(f, S(S))
holds, and write π-prestabilising-sort-signatures(f) to denote set of the π-prestabilising sortsignatures for f.
Recall the definition of sd[f, >S ] given at the end of Section 7.2. The following proposition
guarantees that if S(S) is !-prestabilising for the diffusion f then:
• S ground implies that S(S) is stabilising for f; and
• S(S) is stabilising for the user-defined diffusion d displayed in Equation 7.1 of Section 7.2.
Proposition 7.2. (1) if S is ground then: !-stabilising(f, S(S)) implies stabilising(f, S(S)), i.e,
!-prestabilising-sort-signatures(f) ⊆ stabilising-sort-signatures(f).

28

F. DAMIANI AND M. VIROLI

(2) !-stabilising(f, S(S)) implies stabilising(sd[f, >S ], S(S)), i.e,
!-prestabilising-sort-signatures(f) ⊆ stabilising-sort-signatures(sd[f, S]).
Proof. Straightforward from Definition 7.1, Definition 4.2, and the definition of sd[f, S].
Example 7.3. Consider the libraries in Figure 2 and 11. The following predicates hold (cf. Examples 4.3 and 6.3):
• !-stabilising(+, real(real, pr)) and ?-stabilising(+, real(pr, zpr))
• !-stabilising(max, pr(znr, pr)) and ?-stabilising(max, real(real, real)), where max is the the
binary maximum function:
def max(real x, real y) is x < y ? y : x
• ?-stabilising(id, real(real))
• ?-stabilising(restrict, real(real, bool))
• !-stabilising(restrictSum, real(real, pr, bool))
• !-stabilising(sum or, <real, bool>(<real, bool>, <pr, bool>))
• !-stabilising(add to 1st, <real, real>(<real, real>, pr))
7.4. Annotated Sort-Signatures and Annotated Sorts. In order to be able to write type-based
rules for checking π-stabilisation we introduce, as convenient notations, annotated sort-signatures
and annotated sorts.
An annotated sort-signature S(S)[π] is a progressive sort-signature (cf. Definition 4.4)
with a π annotation. It provides a convenient notation to express the fact that the predicate
π-prestabilising(f, S(S)) holds. Namely, we say that a diffusion f has (or satisfies) the annotated sort-signature S(S)[π] to mean that the predicate π-prestabilising(f, S(S)) holds. We write
π-annotated-sort-signatures(f) to denote the set of the annotated sort-signatures with annotation π that are satisfied by the diffusion f, and we write annotated-sort-signatures(f) to denote
!-annotated-sort-signatures(f) ∪ ?-annotated-sort-signatures(f).
The support of an annotated sort signature S(S)[π] is the progressive sort signature S(S).
Given an annotated sort-signature S(S)[π] we write |S(S)[π]| to denote its support. Note that,
according to the above definitions, the mapping π-annotated-sort-signatures(·) provides the same
information of the mapping π-prestabilising-sort-signatures(·) introduced in Section 7.3, i.e.,
π-prestabilising-sort-signatures(f) = |π-annotated-sort-signatures(f)|.
Given a diffusion type-signature T(TT) (cf. Definition 3.2) we write
annotated-sort-signatures(T(TT)) to denote the (set of) annotated sort-signatures that refine it, i.e.,
the set
{S(S0 S)[π] | S(S0 S) ∈ progressive-sort-signatures(T(TT)) and π ∈ {!, ?}}.
Recall the stabilising subsigning partial order between progressive signatures introduced at
the end of Section 4.2. The following order between progressiveness annotations, that we call
subannotating relation and denote by ≤,
?
!

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

29

induces the following partial order between annotated sort-signatures, that we call annotated subsigning:
0
[I-A-SIG]
S(S1 S) ≤stabilising S0 (S01 S ) π ≤ π 0
0
S(S1 S)[π] ≤ S0 (S01 S )[π 0 ]
The following proposition shows that annotated subsigning captures the natural implication relation
between π-prestabilisation properties.
Proposition 7.4 (Sounness of annotated subsigning). If the diffusion f satisfies the the annotated
0
sort-signature S(S)[π] and S(S)[π] ≤ S0 (S )[π 0 ], then f satisfies S0 (S0 )[π 0 ].
Proof. Straightforward from Definition 7.1 and the definition of annotated subsigning (Rule [I-A-SIG]
above).
We say that an value v has (or satisfies) annotated sort S01 [π] to mean that v has sort S01 , and
• the application of any diffusion with annotated sort signature S(S1 , ..., Sn )[π] such that both
key(S01 ) ≤progressive key(S1 ) and S01 ≤ S1 hold
• to v and to values v2 , . . . , vn of sorts S02 , ..., S0n (respectively) such that S02 ≤ S2 , ..., S0n ≤ Sn ,
produces a result of annotated sort S[π 00 ], where π 00 = π(π 0 ). According to this definition, the
following property holds.
Proposition 7.5 (Annotated sorts for ground values). For every sort S ∈ sorts(T) the maximum
element v of [[S]] w.r.t. ≤S has both sort S[!] and sort S[?].
Proof. Straightforward from Definition 7.1.
The following partial order between annotated sorts, that we call annotated subsorting, models the
natural implication between the properties they represent:
[I-A-SORT]

key(S) ≤progressive key(S0 ) S ≤ S0
S[π] ≤ S0 [π 0 ]

π ≤ π0

The support of an annotated sort S[π] is the sort S. Given an annotated sort A we write |A| to denote
its support.
8. C HECKING S ORT-S IGNATURE A SSUMPTIONS FOR U SER -D EFINED F UNCTIONS
In this section we present a decidable sort-checking system that guarantees that if a program (or
library) P is well-sorted (i.e., it can be successfully checked by the rules of the system) then Condition
(1) of Section 4.3 holds. 7
We first introduce some auxiliary definitions (in Section 8.1); then we consider the issue of
associating sorts to values and sensors (in Section 8.2), sort-signatures to functions (in Section 8.3)
and stabilising sort-signatures to diffusions (in Section 8.4); and finally we present a decidable sort
system for checking the correctness of sort-signature declarations for user-defined functions (in
Section 8.5) and show that it is sound (in Section 8.6).
7Note that, in this section, we do not use the additional requirements (1) and (2) introduced at the beginning of
Section 7.1.2. This generality might become useful since Condition (2) of Section 4.3 might be checked by using a
technique different from the one presented in Section 7.

30

F. DAMIANI AND M. VIROLI

8.1. Auxiliary Definitions. The auxiliary definitions presented in this section will be used (in
Section 8.5) to formulate the sort-checking rules for function applications and spreading expressions.
Recall that for every type T and type-signature T(T) both (sorts(T), ≤) and
(sort-signatures(T(T)), ≤) are partial orders (cf. Section 4.1). Sort checking an expression
e of type T amounts to compute an abstract interpretation [15] over these partial orders.
Given a partial order (P, ≤) and a subset Q of P we say that:
• an element q0 ∈ Q is minimal in Q to mean that: if q ∈ Q and q ≤ q0 then q = q0 —the set of the
minimal elements of Q is denoted by minimals(Q);
• Q is minimised to mean that every q ∈ Q is minimal in Q, i.e., that Q = minimals(Q).
0
Given a set of sort-signatures Q ⊆ sort-signatures(T(T)) and some sorts S ∈
sort-signatures(T), consider the (possibly empty) subset of Q defined as follows:
0

0

Q(S ) = {S(S) ∈ Q | S ≤ S}.
0

We say that Q is deterministic, notation deterministic(Q), to mean that for all sorts S there exists a
0
0
sort-signature S(S) ∈ Q(S ), called the most specific sort-signature for S in Q, such that:
00
0
for all S00 (S ) ∈ Q(S ) it holds that S ≤ S00 .
0
The mapping ms(Q, S ), given a deterministic set of sort-signatures Q ⊆ sort-signatures(T(T)) and
0
0
0
some sorts S ∈ sort-signatures(T), returns the most specific sort-signature for S in Q if Q(S ) is
not empty, and is undefined otherwise.
8.2. Sorts for Values and Sensors. We assume a mapping sort(·) that associates:
• to each ground value g the minimum (w.r.t. ≤) sort sort(g) in sorts(g), and
• to each sensor s the minimum (w.r.t. ≤) sort sort(s) in sorts(type(s)) such that g ∈ [[sort(s)]] for
every ground value g that may be returned by s.
Example 8.1. Figure 15 illustrates the sorts for the ground values and sensors used in the examples
introduced throughout the paper.
8.3. Sort-signatures for Functions. We assume a mapping s-sigs(·) that associates to each built-in
function b a set of sort-signatures s-sigs(b) ⊆ sort-signatures(b) such that the following conditions
are satisfied:
• s-sigs(b) is non-empty, minimised and deterministic, and
0
• s-sigs(b) represents all the sort-signatures satisfied by f, i.e., for each S0 (S ) ∈ sort-signatures(b)
0
there exists S(S) ∈ s-sigs(b) such that S(S) ≤ S0 (S ) holds.
Note that the first of the above two conditions on the mapping s-sigs(b) can be checked automatically.
Example 8.2. Figure 16 illustrates the sort-signatures for built-in functions used in the examples
introduced throughout the paper.
We also assume that the mapping s-sigs(·) associates to each user-defined function d a set of
sort-signatures s-sigs(d) ⊆ sort-signatures(t-sig(d)) such that the following conditions are satisfied:
• s-sigs(d) is non-empty, minimised and deterministic, and
• s-sigs(d) contains at least a sort-signature which is smaller than the type-signature t-sig(d), i.e.,
there exists S(S) ∈ s-sigs(d) such that S(S) ≤ t-sig(d) holds.
Note that the above two conditions on the mapping s-sigs(d) can be checked automatically.

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

31

Ground values sort:
sort(FALSE) = false
sort(TRUE) = true
sort(g)
= nr, if type(g) = real and g < 0
sort(g)
= zr, if g = 0
sort(g)
= pr, if type(g) = real and g > 0
Sensors sort:
sort(#src) = zpr
sort(#dist) = pr
Figure 15: Sorts for ground values and sensors used in the examples (cf. Figure 5)
8.4. Stabilising Sort-signatures for Diffusions. We assume a mapping stb-s-sigs(·) that associates
to each built-in diffusion b a (possibly empty) set of sort-signatures stb-s-sigs(b) such that the
following conditions are satisfied:
• stb-s-sigs(b) is minimised and deterministic;
• stb-s-sigs(b) ⊆ stabilising-sort-signatures(b); and
0
• stb-s-sigs(b) represents all the stabilising sort-signatures satisfied by b, i.e., for each S0 (S ) ∈
0
stabilising-sort-signatures(b) there exists S(S) ∈ stb-s-sigs(b) such that S(S) ≤ S0 (S ) holds.
Note that the first of the above three conditions on the mapping stb-s-sigs(b) can be checked
automatically.
Example 8.3. Figure 17 gives the stabilising sort-signatures for the built-in diffusions b used in
the examples introduced throughout the paper—the built-in diffusions without stabilising sortsignatures are omitted. Note that stb-s-sigs(+) 6⊆ s-sigs(+), since the stabilising sort-signature
real(real, pr) ∈ stb-s-sigs(+) is not minimal in s-sigs(+) ∪ {real(real, pr)} and therefore it
cannot be included in s-sigs(+)—it would break both the requirement that s-sigs(+) must be
minimised and deterministic (condition (1) at the beginning of Section 7.1.2).
We also assume that the mapping stb-s-sigs(·) associates to each user-defined diffusion d a
(possibly empty) set of stabilising sort-signatures stb-s-sigs(d) ⊆ stabilising-sort-signatures(d)
such that the following conditions are satisfied:
• stb-s-sigs(d) is minimised and deterministic, and
0
• stb-s-sigs(d) is implied by s-sigs(d), i.e., for each S0 (S ) ∈ stb-s-sigs(d) there exists S(S) ∈
0
s-sigs(d) such that S(S) ≤ S0 (S ).
Note that the above two conditions on the mapping stb-s-sigs(d) can be checked automatically.
Example 8.4. We assume that for the user-defined functions d used in the examples introduced
throughout the paper
s-sigs(d) = minimals({t-sig(d)} ∪ stb-s-sigs(d)).
Figure 18 gives minimised deterministic sets of stabilising sort-signatures that allow to successfully
check the user-defined diffusions d used in the examples introduced in the paper—note that both the
additional requirements (1) and (2) given at the beginning of Section 7 are satisfied.

32

F. DAMIANI AND M. VIROLI

s-sigs(not) = true(false),
false(true),
bool(bool)
s-sigs(or) = false(false, false),
true(true, bool),
true(bool, true),
bool(bool, bool)
s-sigs(−)
= nr(pr),
znr(zpr),
zr(zr),
zpr(znr),
pr(nr),
real(real)
s-sigs(+)
= nr(nr, znr),
nr(znr, nr),
znr(znr, znr),
zr(zr, zr),
zpr(zpr, zpr),
pr(zpr, pr),
pr(pr, zpr),
real(real, real)
s-sigs(=)
= false(znr, pr),
false(nr, zpr),
false(zpr, nr),
false(pr, znr),
true(zr, zr),
bool(real, real)
s-sigs(<)
= false(zpr, nr),
false(pr, znr),
false(zr, zr),
true(nr, zpr),
true(znr, pr),
bool(real, real)
Figure 16: Sort-signatures for built-in functions used in the examples (cf. Figure 5)
stb-s-sigs(or) = false(false, false),
true(true, bool),
true(bool, true)
stb-s-sigs(+) = zr(zr, zr),
pr(zpr, pr),
real(real, pr)
(6∈ s-sigs(+))
Figure 17: Stabilising sort-signatures for built-in functions used in the examples (cf. Figure 16)

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

33

stb-s-sigs(restrictSum)
= real(real, pr, bool),
stb-s-sigs(sd sum or)
= <real, bool>(<real, bool>, <pr, bool>)
stb-s-sigs(sd add to 1st) = <real, real>(<real, real>, pr)
Figure 18: Stabilising sort-signatures for the user-defined functions used in the examples
S `e:S

Expression sort checking:
[S-VAR]

[S-SNS]

[S-GVAL]

S ,x : S ` x : S

S ` s : sort(s)

S ` g : sort(g)

S ` e1 : S1 S ` e2 : S2
S ` <e1 , e2 > : <S1 , S2 >

[S-PAIR]

[S-COND]

S ` e0 : bool S ` e1 : S1 S ` e2 : S2
S ` e0 ?e1 :e2 : S
[S-COND-TRUE]

[S-COND-FALSE]

[S-FUN]

[S-SPR]

S ` e : <S1 , S2 >
S ` fst e : S1

[S-FST]

S ` e0 : true S ` e1 : S1
S ` e0 ?e1 :e2 : S1
S ` e0 : false S ` e1 : S1
S ` e0 ?e1 :e2 : S2

S ` e : <S1 , S2 >
S ` snd e : S2

[S-SND]

S = sup≤ (S1 , S2 )
S ` e2 : S2
S ` e2 : S2

S ` e : S S(· · · ) = ms(s-sigs(f), S)
S ` f(e) : S

diffusion(f) S ` e0 e : S0 S S0 (· · · ) = ms(stb-s-sigs(f), S0 S) S = sup≤ (S0 , S0 )
S ` {e0 : f(@, e)} : S

User-defined function sort checking:
[S-DEF]
for all S(S) ∈ s-sigs(d), x : S ` e : S0
` def T d(T x) is e : s-sigs(d)

` D : S(S)
S0

≤S

Figure 19: Sort-checking rules for expressions and function definitions
8.5. Sort Checking. In this section we present a decidable sort checking system for user-defined
functions to check whether the sort-signature declarations provided by the mapping s-sigs(·) are
correct. The sort-checking rules are given in Figure 19. Sort environments, ranged over by S
and written x : S, contain sort assumptions for program variables. The sort-checking judgement
for expressions is of the form S ` e : S, to be read: e has sort S under the sort assumptions S
for the program variables occurring in e. Sort checking of variables, sensors, ground values, pair
constructions and deconstructions, and conditionals is similar to type checking. In particular, ground
values and sensors are given a sort by construction by exploiting the mapping sort(·) introduced in
Section 8.2, and the sort assigned to a conditional-expression is:
• the least upper bound sup≤ (S1 , S2 ) of the sorts assigned to the branches (cf. Section 4.1) when the
condition has sort bool;
• the sort assigned to the left branch when the condition has sort true; and
• the sort assigned to the right branch when the condition has sort false.

34

F. DAMIANI AND M. VIROLI

The sort-checking rule [S-FUN] for function application exploits the mapping s-sigs(·) introduced in
Section 8.3 and the auxiliary mapping ms(·, ·) introduced in Section 8.1. It first infers the sorts S for
the arguments e of f, then uses the most specific sort-signature for S in s-sigs(f) for assigning to
the application f(e) the minimum sort S that can be assigned to f(e) by using for f any of the sort
signatures in s-sigs(f).
In a similar way, the sort-checking rule [S-SPR] for spreading expressions first infers the sorts S0 S
for e0 e, then retrieves the most specific sort-signature for S0 S in stb-s-sigs(f), S(· · · ), and finally
assigns to the spreading expression the the least upper bound of S0 and S.
The sort-checking rule for function definitions (which derives judgements of the form S `
(1)
(n)
D : S(S), where S(S) = S(1) (S ), ..., S(n) (S ) and n ≥ 1) requires to check the definition D of a
user-defined function d with respect to all the sort-signatures in s-sigs(d).
We say that a program (or library) P is well sorted to mean that all the user-defined function
definitions in P sort check by using the rules in Figure 19.
Since no choice may be done when building a derivation for a given sort-checking judgment, the
sort-checking rules straightforwardly describe a sort-checking algorithm.
Example 8.5. All user-defined functions provided in the examples in Sections 2.2 and 6.2 sort check
by assuming the ground sorts and the subsorting given in Figure 8, the sorts for the ground values
and sensors given in Figure 15, the sort-signatures for built-in functions given in Figure 16, the
stabilising sort-signatures for built-in functions given in Figures 17 and the stabilising sort-signatures
for user-defined diffusions given in 18.
8.6. Sort Soundness of Device Computation. In order to state the correctness of the sort-checking
system presented in Section 8.5 we introduce the notion of set of well-sorted values trees for an
expression, which generalizes to sorts the notion of set of well-typed values trees for an expression
introduced in Section 5.1.
Given an expression e such that x : S ` e : S, the set WSVT(x : S, e, S) of the well-sorted
value-trees for e, is inductively defined as follows: θ ∈ WSVT(x : S, e, S) if there exist
• a sensor mapping σ ;
• well-formed tree environments θ ∈ WSVT(x : S, e, S); and
0
0
• values v such that length(v) = length(x), 0/ ` v : S and S ≤ S;
such that σ ; θ ` e[x := v] ⇓ θ holds—note that this definition is inductive, since the sequence of
evaluation trees θ may be empty.
The following theorem guarantees that from a properly sorted environment, evaluation of a
well-sorted expression yields a properly sorted result.
Theorem 8.6 (Device computation sort preservation). If x : S ` e : S, σ is a sensor mapping,
0
0
θ ∈ WSVT(x : S, e, S), length(v) = length(x), 0/ ` v : S , S ≤ S, and σ ; θ ` e[x := v] ⇓ θ , then
0
0
0
0/ ` ρ(θ ) : S for some S such that S ≤ S.
Proof. See Appendix C.
Remark 8.7 (On the relation between type checking and sort checking). A sort system should be such
that all the programs (or libraries) accepted by the sort system are accepted by the original type system
and vice-versa (cf. the discussion at the beginning of Section 4.1). However, the sort system considered in this paper has a peculiarity: it checks that every diffusion-expressions {e1 : f(@, e2 , ..., en )}
occurring in P is sort-checked by considering for f only the sort-signatures in stb-s-sigs(f)—which

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

35

is assumed to be such that for all S(S) ∈ stb-s-sigs(f) the predicate stabilising(f, S(S)) holds. Therefore, some well-typed programs (or libraries)—including all the non-self-stabilising programs (like
the one considered in Example 3.8)—do not sort check.
The standard relation between the sort system and the type system that it refines holds for
programs (or libraries) that do not contain spreading expressions. I.e., all the programs (or libraries)
that do not contain spreading expressions that accepted by the original type system are accepted by
the sort system and vice-versa. In particular, whenever all the sorts are trivial (i.e., sorts(T) = {T},
for every type T) we have that, on programs (or libraries) that do not contain spreading expressions,
the sort checking rules (in Figure 19) behave exactly as the type-checking rules (in Figure 4).

9. C HECKING S TABILISING A SSUPTIONS FOR U SER -D EFINED D IFFUSIONS
In this section we present a decidable annotated sort checking system that guarantees that if a
program P is well-sorted (i.e., it can be successfully checked by the rules of the system given in
Section 8 and, therefore, satisfies Condition (1) of Section 4.3) guarantees that, under the additional
requirements (1) and (2) introduced at the beginning of Section 7.1.2, if P is well-annotated (i.e., it
can be successfully checked by the rules of the system) then Condition (2) of Section 4.3 holds, and
hence self-stabilisation follows.
To this aim, under the additional requirements (1) and (2) introduced at the beginning of
Section 7, we assume that each program P comes with a mapping a-s-sigs(·) that associates to
each diffusion f a (possibly empty) set of annotated sort-signatures a-s-sigs(f) (we write π-s-sigs(·)
to denote the mapping such that π-s-sigs(f) = {S(S)[π] | S(S)[π] ∈ a-s-sigs(f)}) such that the
following conditions are satisfied:
• for every diffusion f of type T(· · · ), if T is ground, then stb-s-sigs(f) = |!-s-sigs(f)|;
• for every user-defined diffusion d of the form displayed in Equation 7.1 of Section 7.2, consider
the function f occurring in the body of d:
– if f is built-in function, then stb-s-sigs(d) ⊆ |!-s-sigs(f)|, and
– if f is user-defined, then stb-s-sigs(d) = |!-s-sigs(f)|.
Note that the above conditions (which can be checked automatically) imply that, for every user
defined function d, the value of stb-s-sigs(d) is completely defined by the mapping a-s-sigs(·)—
therefore, there is no need to explicitly define the value of stb-s-sigs(·) for user-defined diffusions.
The assumptions a-s-sigs(b) for the built-in functions b are considered valid—they should come with
the definition of the language. Instead, the validity of the assumptions a-s-sigs(d) for the user-defined
functions d must be checked—these assumptions could be either (possibly partially) provided by the
user or automatically inferred.8 Therefore, in order to check that Condition (2) of Section 4.3 holds,
it is enough to check that each the user-defined diffusions d of P has all the annotated sort signatures
a-s-sigs(d).
We first introduce some auxiliary definitions (in Section 9.1), then we consider the issue of associating annotated sort-signatures to diffusions (in Section 9.2) and the issue of associating annotated
sorts to values (in Section 9.3), and finally we present a decidable annotated sort checking system
for checking the correctness of annotated sort-signature declarations for user-defined diffusions (in
Section 9.4) and show its soundness (in Section 9.5).
8The naive inference approach, that is: inferring a-s-sigs(d) by checking all the sort-signature of d is linear in the
number of elements of s-sigs(d). Some optimizations are possible. We do not address this issue in the paper.

36

F. DAMIANI AND M. VIROLI

9.1. Auxiliary definitions. In this section we adapt the notions of minimal set of sort-signatures,
deterministic set of sort signatures and most specific sort-signature (cf. Section 8.1) to annotated
sort-signatures. These notions will be used (in Section 9.4) to formulate the annotated sort-checking
rules for function applications.
Given a diffusion signature T(TT) and a set of annotated sort-signatures Q ⊆
annotated-sort-signatures(T(TT)), an annotated sort S01 [π 0 ] such that S01 ∈ sort-signatures(T1 )
0
and some sorts S ∈ sort-signatures(T), consider the (possibly empty) subset of Q defined as follows:
0

0

Q(S01 [π 0 ]S ) = {S(S1 S)[π 00 ] ∈ Q | key(S01 ) ≤progressive key(S1 ), S01 ≤ S1 and S ≤ S}.
0

We say that Q is deterministic, notation deterministic(Q), to mean that for all S01 [π 0 ]S there exists an
0
annotated sort-signature S(S1 S)[π] ∈ Q(S01 [π 0 ]S ), called the most specific annotated sort-signature
0
for S in Q, such that:
00
0
for all S00 (S )[π 00 ] ∈ Q(S01 [π 0 ]S ) it holds that S[π(π 0 )] ≤ S00 [π 00 (π 0 )].
0

The mapping ms(Q, S01 [π 0 ]S ), given a deterministic set of sort-signatures Q ⊆
annotated-sort-signatures(T(TT)), an annotated sort S01 [π 0 ] such that S01 ∈ sort-signatures(T1 )
0
and some sorts S ∈ sort-signatures(T), returns the most specific annotated sort-signature for
0
0
S01 [π 0 ]S in Q if Q(S01 [π 0 ]S ) is not empty, and is undefined otherwise.
9.2. Annotated Sort-Signatures for Diffusions. The mapping a-s-sigs(·) and the conditions that
provides its link with the mapping stb-s-sigs() have been illustrated at the beginning of Section 9.
Here, we illustrate some additional condition that is needed to simplify the formulation of the
annotated sort checking rules and to guarantee their soundness.
We assume that for each built-in diffusion b the (possibly empty) set of annotated sort-signatures
a-s-sigs(b) is such that the following conditions are satisfied:
• a-s-sigs(b) is minimized and deterministic;
• a-s-sigs(b) ⊆ annotated-sort-signatures(b); and
0
• a-s-sigs(b) represents all the annotated sort-signatures satisfied by b, i.e., for each S0 (S )[π 0 ] ∈
annotated-sort-signatures(b) there exists S(S)[π] ∈ a-s-sigs(b) such that S(S)[π] ≤
0
S0 (S )[π 0 ] holds.
Note that the first of the above three conditions on the mapping a-s-sigs(b) can be checked automatically.
Example 9.1. Figure 20 illustrates the annotated sort-signatures for the built-in diffusions used in
the examples introduced thought the paper.
We also assume that for each user-defined diffusion d the (possibly empty) set of annotated
sort-signatures a-s-sigs(d) is minimized and deterministic (note that this condition can be checked
automatically).
Example 9.2. Figure 21 gives minimal deterministic sets of annotated sort signatures for the userdefined π-prestabilising diffusions that allow to successfully check the user-defined diffusions used
in the examples introduced thought the paper.

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

37

a-s-sigs(or) = false(false, false)[!],
true(true, bool)[!],
true(bool, true)[!]
a-s-sigs(+)

= nr(nr, zr)[?],
znr(znr, zr)[?],
zr(zr, zr)[!],
zpr(zpr, zpr)[?],
pr(zpr, pr)[!],
pr(pr, zpr)[?],
real(real, zpr)[?],
real(real, pr)[!]

Figure 20: Annotated sort signatures for built-in π-prestabilising diffusions used in the examples (cf.
Figure 16)
a-s-sigs(restrict)
a-s-sigs(restrictSum)
a-s-sigs(sum or)
a-s-sigs(add to 1st)

=
=
=
=

real(real, bool)[?]
real(real, pr, bool)[!]
<real, bool>(<real, bool>, <pr, bool>)[!]
<real, real>(<real, real>, pr)[!]

Figure 21: Annotated sort signatures for the user-defined π-prestabilising diffusions used in the
examples (cf. Figure 18)
a-sort(FALSE)
a-sort(TRUE)
a-sort(0)
a-sort(POSINF)

=
=
=
=

false[!]
true[!]
zr[!]
pr[!]

Figure 22: Annotated sorts for the ground values used in the examples
9.3. Annotated Sorts for Values. We assume a partial mapping a-sort(·) that for each ground value
g:
• returns the annotated sort sort(g)[!], if g is the maximum element of [[sort(g)]] w.r.t. ≤type(g) , and
• is undefined, otherwise.
Note that Proposition 7.5 guarantees the soundness of the mapping a-sort(·).
Example 9.3. Figure 22 illustrates the !-annotated sorts for the ground values used in the examples
introduced thought the paper.
9.4. Annotated Sort Checking for User-Defined Diffusions. In this section we present a decidable
annotated sort checking system to check whether the π-annotated sort-signature assumptions for
the user-defined diffusions d provided by the mapping a-s-sigs(·) are correct. The annotated sortchecking rules are given in Figure 23.

38

F. DAMIANI AND M. VIROLI

A `e:A

Pure expression annotated sort checking:
A , x : S[?] ` x : S[?]
[A-PAIR]

>key(S) = g
A , x : S[?] ` g : a-sort(g)
[A-GVAL]

[A-VAR]

A ` e1 : S1 [π] |A | ` e2 : S2
A ` <e1 , e2 > : <S1 , S2 >[π]

A ` e : <S1 , S2 >[π]
A ` fst e : S1 [π]

[A-FST]

|A | ` e0 : bool A ` e1 : A1 A ` e2 : A2
A ` e0 ?e1 :e2 : A

[A-COND]

[A-COND-TRUE]

[A-COND-FALSE]

A = sup≤ (A1 , A2 )

|A | ` e0 : true A ` e1 : A |A | ` e2 : S
A ` e0 ?e1 :e2 : A
|A | ` e0 : false |A | ` e1 : S A ` e2 : A
A ` e0 ?e1 :e2 : A

[A-FUN]

A ` e1 : S1 [π 00 ]

|A | ` e : S

S(· · · )[π 0 ] ∈ ms(a-s-sigs(f), S1 S)
A ` f(e1 , e) : S[π]

User-defined diffusion annotated sort checking:

π = π 0 (π 00 )
` D : S(S)[π]

[A-DEF]

for all S(S1 S)[π] ∈ a-s-sigs(d),
x : S1 [?] S ` e : S0 [π 0 ]
S0 [π 0 ] ≤ S[π]
` def T d(T x) is e : a-s-sigs(d)
Figure 23: Annotated sort checking rules for expressions and diffusion definitions
The check a user defined diffusion d has the annotated sort signature (S1 , ..., Sn )S[π] can be
done by assuming annotated sort S1 [?] for the first formal parameter of d, assuming sorts S2 , ..., Sn
for the other formal parameters of d, and trying to assign to the body of d an annotated sort S0 [π 0 ]
such that S0 [π 0 ] ≤ S[π]. According to this observation we introduce the notion of annotated
sort environments, ranged over by A and written x : S[?], x : S, that contain one ?-annotated sort
assumption and some (possibly none) sort assumptions for program variables. The annotated sort
checking rule for user-defined diffusions [A-DEF] (which derives judgements of the form ` D : S(S)[π])
uses this strategy to check that the definition of a user-defined diffusion d with respect to all the
annotated sort signatures in a-s-sigs(d).
The annotated sort-checking judgement for expressions is of the form A ` e : A, to be read:
pure-expression e has annotated sort A under the assumptions A for the program variables occurring
in e. The support of an annotated sort environment A , denoted by |A |, is the sort environment
obtained from A by removing the input annotation, i.e.,
|x : S[?], x : S| = x : S, x : S
(cf. Section 7.4). Some of the annotated sort-checking rules rely on the judgements of the sort
checking system introduced in Section 9.2 to sort check some subexpressions. Namely: the right
element of the pair in rule [A-PAIR]; the condition of the conditional-expression in rules [A-COND], [ACOND-TRUE] and [A-COND-FALSE]; the right branch of the conditional-expression in rule [A-COND-TRUE];

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

39

the left branch of the conditional-expression in rule [A-COND-FALSE]; and the arguments (excluding the
first one) of the pure function f (that must be an π-diffusion) in rule [A-FUN].
Annotated sort checking of variables and ground values is similar to sort checking. In particular,
ground values may be given an annotated sort by construction by exploiting the mapping a-sort(·)—
the premise >key(S) = g ensures that the value g is relevant to the overall goal of the annotated sort
checking derivation process, that is: deriving an annotated sort S0 [π 0 ] such that S0 [π 0 ] ≤ S[π] for
the body e of a user-defined diffusion d in order to check that d has the annotated sort-signature
S(S1 , ..., Sn )[π].
Note that there is no annotated sort checking rule for expressions of the form snd e—because of
the leftmost-as-key preorder such an expression is not relevant to the overall goal of the annotated
sort checking derivation process.
The sort-checking rule [A-FUN] for diffusion application exploits the mapping a-s-sigs(·) and
the auxiliary mapping ms(·, ·) introduced in Section 9.1. It first infers the sort S1 [π 00 ] for the first
argument e1 of f and the sorts S for remaining the arguments e of f, then uses the most specific
annotated sort signature for S in a-s-sigs(f) for assigning to the application f(e) the minimum
annotated sort S[π 0 ] that can be assigned to f(e) by using for f any of the annotated sort signatures
in s-sigs(f).
We say that a program (or library) P is well annotated to mean that: all the user-defined function
definitions in P check by using the sort-checking rules in Figure 19, and all the user-defined diffusion
definitions sort checking rules in Figure 23.
Example 9.4. All user-defined functions provided in the examples in Sections 2.2 and 6.2 sort-check
and (when they are diffusions) annotate sort check by assuming the ground sorts and the subsorting
given in Figure 8, the sorts for the ground values and sensors given in Figure 15, the sort-signatures
for built-in functions given in Figure 16, the annotated sorts for ground values given in Figure 22, the
annotated sort-signatures for built-in functions given in Figures 20 and the annotated sort-signatures
for user-defined diffusions given in 21.
Since no choice may be done when building a derivation for a given annotated sort-checking
judgment, the annotated sort-checking rules straightforwardly describe an annotated sort-checking
algorithm.
9.5. Annotation Soundness. The following theorem states the correctness of the annotationchecking system presented in Section 9.4
Theorem 9.5 (Annotation soundness). If ` D : S(S)[π] holds, then π-prestabilising(f, S(S)) holds
for all S(S)[π] ∈ S(S)[π].
Proof. See Appendix D.

10. R ELATED W ORK AND D ISCUSSION
We here discuss the main related pieces of work, rooted in previous research on finding core models
for spatial computing and self-organisation, formal approaches for large-scale systems, and finally
on self-stabilisation in distributed systems.

40

F. DAMIANI AND M. VIROLI

10.1. Spatial computing and self-organisation. A first step in studying general behavioural properties of self-organising systems is the identification of a reference model, making it possible to reuse
results across many different models, languages and platforms. The review in [7] surveys a good deal
of the approaches considering some notion of space-time computations, which are the basis for any
self-organising system. Examples of such models include the Hood sensor network abstraction [50],
the σ τ-Linda model [47], the SAPERE computing model [48], and TOTA middleware [35], which
all implement computational fields using similar notions of spreading. More generally, Proto [36, 5]
and its core formalisation as the “field calculus” [16], provides a functional model that appear general
enough to serve as a starting point for investigating behavioural aspects of spatial computation and
self-organisation [9]. In fact, in [10] it is proved that the field calculus is universal, in the sense that it
can be used to describe any causal and discretely-approximable computation in space-time.
Hence, we started from the field calculus, in which computation is expressed by the functional
combination of input fields (as provided by sensors), combined with mechanisms of space-based
(neighbour) data aggregation, restriction (distributed branch) and state persistence. The calculus
presented here is a fragment of the field calculus, focussing on only two basic computational elements:
(i) functional composition of fields, and (ii) a spreading expression. In particular, the latter is a
suitable combination of basic mechanisms of the field calculus, for which we were able to prove
convergence to a single final state. Namely, a spreading expression {e0 : g(@,e1 ,..,en )} in our
calculus is equivalent to the following field calculus expression:
(rep x (inf) (min e0 (g (min-hood+ (nbr x)) e1 .. en )))
In particular, it was key to our end to neglect recursive function calls (in order to ensure termination
of device fires, since the calculus does not model the domain restriction construct [46, 36] and both
the branches of a conditional expression are evaluated), stateful operations (in our model, the state of
a device is always cleaned up before computing the new one), and to restrict aggregation to minimum
function and progression to what we called “stabilising diffusion” functions.
Other than applying to fragments of the field calculus, the result provided here can be applied
to rule-based systems like those of the SAPERE approach [48] and of rewrite-based coordination
models [47], along the lines depicted in [43]. Note that our condition for self-stabilisation is only a
sufficient one. A primary example of the fact that it is not necessary is Laplacian consensus [24],
expressed as follows in the field calculus:
(rep x ei (+ x (* eε (sum-hood (- (nbr x) x))))))
It cannot be expressed in the calculus we propose here, but still stabilises to a plateau field, computed
as a consensus among the values of input field ei (with eε ) driving the dynamics of the output field.
Other cases include so-called convergence cast [8].
10.2. Formal approaches. In this paper we are interested in formally predicting the behaviour of a
complex system, in which the local interactions among a possibly miriad of devices make a global
and robust pattern of behaviour emerge. In the general case, one such kind of prediction can hardly
be obtained.
The quintessential formal approach, model-checking [14], cannot typically scale with the number
of involved components: suitable abstractions are needed to model arbitrary-size systems (as in [18]),
which however only work in very constrained situations. Approximate model-checking [29, 12],
basically consisting in a high number of simulation bursts, is viable in principle, but it still falls
under the umbrella of semi-empirical evaluations, for only statistical results are provided. Recently,
fluid flow approximation has been proposed to turn large-scale computational systems into systems

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

41

of differential equations that one could solve analytically or use to derive an evaluation of system
behaviour [11]. Unfortunately, this approach seems developed yet only to abstract from the number
of (equivalent and non-situated) agents performing a repetitive task, instead of abstracting from the
discreteness of a large-scale situated computational network.
Recent works finally aim at proving properties of large-scale systems by hand-written proofs,
which are the works most related to the result of present paper. The only work aiming at a mathematical proof of stabilisation for the specific case of computational fields is [6]. There, a self-healing
gradient algorithm called CRF (constraints and restoring forces) is introduced to estimate physical
distance in a spatial computer, where the neighbouring relation is fixed to unit-disc radio, and node
firing is strictly connected to physical time. Compared to our approach, the work in [6] tackles a
more specific problem, and is highly dependent on the underlying spatial computer assumptions.
Another work presenting a proof methodology that could be helpful in future stages of our research
is the universality study in [10].
From the viewpoint of rewrite semantics [31], which is the meta-model closest to our formalisation attempt, our proof is most closely related to the confluence property, that is, don’t care
non-determinism. Our result entails confluence, but it is actually a much strongest property of global
uniqueness of a normal form, independently of initial state.
10.3. Self-stabilisation. Our work concerns the problem of identifying complex network computations whose outcome is predictable. The notion we focus on requires a unique global state being
reached in finite time independently of the initial state, that is, depending only on the state of the
environment (topology and sensors). It is named (strong) self-stabilisation since it is related with a
usual notion of self-stabilisation to correct states for distributed systems [22], defined in terms of a
set C of correct states in which the system eventually enters in finite time, and then never escapes
from – in our case, C is made by the single state corresponding to the sougth result of computation.
Actually many different versions of the notion of self-stabilisation have been adopted in past,
surveyed in [41], from works of Dijkstra’s [20, 19] to more recent and abstract ones [1], typically
depending on the reference model for the system to study—protocols, state machines. In our case,
self-stabilisation is studied for a distributed data structure (the computational field). Previous work on
this context like [30] however only considers the case of heap-like data structures in a non-distributed
settings: this generally makes it difficult to draw a bridge with existing research.
Several variations of the definition also deal with different levels of quality (fairness, performance). For instance, the notion of superstabilisation [23] adds to the standard self-stabilisation
definition a requirement on a “passage predicate” that should hold while a system recovers from a
specific topological change. Our work does not address this very issue, since we currently completely
equate the treatment of topological changes and changes to the inputs (i.e., sensors), and do not
address specific performance requirements. However, future works addressing performance issues
will likely require some of the techniques studied in [23]. Performance is also affected by the fairness
assumption adopted: we relied on a notion abstracting from more concrete ones typically used [33],
which we could use as well though losing a bit of the generality of our result.
Concerning the specific technical result achieved here, the closest one appears to be the creation
of a hop-count gradient, which is known to self-stabilise: this is used in [22] as a preliminary step in
the creation of the spanning tree of a graph. The main novelty in this context is that self-stabilisation
is not proved here for a specific algorithm/system: it is proved for all fields inductively obtained
by functional composition of fixed fields (sensors, values) and by a gradient-inspired spreading
process. Other works attempt to devise general methodologies for building self-stabilising systems
like we do. The work in [2] depicts a compiler turning any protocol into a self-stabilising one.

42

F. DAMIANI AND M. VIROLI

Though this is technically unrelated to our solution, it shares the philosophy of hiding the details
of how self-stabilisation is achieved under the hood of the execution platform: in our case in fact,
the designer wants to focus on the macro-level specification, trusting that components behave and
interact so as to achieve the global outcome in a self-stabilising way. The work in [28] suggests that
hierarchical composition of self-stabilising programs is self-stabilising: an idea that is key to the
construction of a functional language of self-stabilising “programs”.
In spite of the connection with some of these previous works, to the best of our knowledge ours is
novel under different dimensions. First, it is the first attempt of providing a notion of self-stabilisation
directly connected to the problem of engineering self-organisation. Secondly, the idea of appliying it
to a whole specification language is also new, along with the fact that we apply a type-based approach,
providing a correct checking procedure that paves the way towards compiler support. As we use now
a type-based approach, other static analysis techniques may be worth studying in future attempts
(see, e.g., [39]).
11. C ONCLUSIONS AND F UTURE W ORK
Emerging application scenarios like pervasive computing, robotic systems, and wireless sensor
networks call for developing robust and predictable large-scale situated systems. However, the
diffusion/aggregation processes that are typically to be implemented therein are source of complex
phenomena, and are notoriously very hard to be formally treated. The goal of this work is to
bootstrap a research thread in which mechanisms of self-organisation are captured by linguistic
constructs, so that static analysis in the programming language style can be used to isolate fragments
with provable predictable behaviour. In the medium term, we believe this is key to provide a toolchain (programming language, libraries, simulation and execution platforms) which enables the
development of complex software systems whose behaviour has still some predictability obtained
“by construction”.
Along this line, this paper studies a notion of strong self-stabilisation, identifying a sufficient
condition expressed on the diffusion/aggregation mechanisms occurring in the system. This targets
the remarkable situation in which the final shape of the distributed data structure created (i.e., the
computational field) is deterministically established, does not depend on transient events (such as
temporaneous failures), and is only determined by the stabilised network topology. Namely, this is
the case in which we can associate to a complex computation a deterministic and easily computable
result.
It would be interesting to relax some of the conditions and assumptions we relied upon in this
paper, so as to provide a more general self-stabilisation result. First of all, the current definition of
self-stabilisation requires values to have upper-bounds, to prevent network subparts that become
isolated from “sources” (e.g., of a gradient) to be associated with values that grow to infinity without
reaching a fixpoint: a more involved definition of self-stabilisation could be given that declares such
a divergence as admitted, allowing us to relax “noetherianity” of values. We also plan to extend
the result to encompass the domain restriction construct [46, 36] (i.e., to add to the calculus a form
of conditional expression where only one of the branches is evaluated). In this way also recursive
function definitions could be added (then, in order to guarantee termination of computation rounds,
standard analysis techniques for checking termination of recursive function definitions might be used).
We currently focus only on spreading-like self-stabilisation, whether recent works [8] suggest that
“aggregation” patterns can be similarly addressed as well, though they might require a completely
different language and proof methodology.

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

43

Of course, other behavioural properties are of interest which we plan to study in future work as
an extension to the results discussed here. First, it is key to study notions of self-stabilisation for
computational fields which are designed so as to be dynamically evolving, like e.g. the anticipative
gradient [37]. Second, it would be interesting to extend our notion of self-stabilisation so as to
take into account those cases in which only approximate reachability of the sought state is required,
since it can lead to computations with better average performance, as proposed in [4]. Other
aspects of interest that can be formally handled include performance characterisation, code mobility,
expressiveness of mechanisms, and independence of network density, which will likely be subject of
next investigations as well.
ACKNOWLEDGEMENT
We thank the anonymous COORDINATION 2014 referees for useful comments on an earlier version
of this paper, and the anonymous LMCS referees for insightful comments and suggestions for
improving the presentation.
R EFERENCES
[1] A. Arora and M. Gouda. Closure and convergence: a foundation of fault-tolerant computing. IEEE Transactions on
Software Engineering, 19:1015–1027, 1993.
[2] B. Awerbuch and G. Varghese. Distributed program checking: a paradigm for building self-stabilizing distributed
protocols. In FOCS91 Proceedings of the 31st Annual IEEE Symposium on Foundations of Computer Science, pages
258–267, 1991.
[3] J. Bachrach, J. Beal, and J. McLurkin. Composable continuous space programs for robotic swarms. Neural Computing
and Applications, 19(6):825–847, 2010.
[4] J. Beal. Flexible self-healing gradients. In S. Y. Shin and S. Ossowski, editors, Proceedings of the 2009 ACM
Symposium on Applied Computing (SAC), Honolulu, Hawaii, USA, March 9-12, 2009, pages 1197–1201. ACM,
2009.
[5] J. Beal and J. Bachrach. Infrastructure for engineered emergence in sensor/actuator networks. IEEE Intelligent
Systems, 21:10–19, March/April 2006.
[6] J. Beal, J. Bachrach, D. Vickery, and M. Tobenkin. Fast self-healing gradients. In Proceedings of ACM SAC 2008,
pages 1969–1975. ACM, 2008.
[7] J. Beal, S. Dulman, K. Usbeck, M. Viroli, and N. Correll. Organizing the aggregate: Languages for spatial computing.
In M. Mernik, editor, Formal and Practical Aspects of Domain-Specific Languages: Recent Developments, chapter 16,
pages 436–501. IGI Global, 2013. A longer version available at: http://arxiv.org/abs/1202.5509.
[8] J. Beal and M. Viroli. Building blocks for aggregate programming of self-organising applications. In 2nd FoCAS
Workshop on Fundamentals of Collective Systems, pages 1–6. IEEE CS, to appear, 2014.
[9] J. Beal and M. Viroli. Space–time programming. Philosophical Transactions of the Royal Society of London A:
Mathematical, Physical and Engineering Sciences, 373(2046), 2015.
[10] J. Beal, M. Viroli, and F. Damiani. Towards a unified model of spatial computing. In 7th Spatial Computing Workshop
(SCW 2014), AAMAS 2014, Paris, France, May 2014.
[11] L. Bortolussi, D. Latella, and M. Massink. Stochastic process algebra and stability analysis of collective systems. In
R. D. Nicola and C. Julien, editors, Coordination Models and Languages, 15th International Conference, COORDINATION 2013, Held as Part of the 8th International Federated Conference on Distributed Computing Techniques,
DisCoTec 2013, Florence, Italy, June 3-5, 2013. Proceedings, volume 7890 of Lecture Notes in Computer Science,
pages 1–15. Springer, 2013.
[12] M. Casadei and M. Viroli. Toward approximate stochastic model checking of computational fields for pervasive
computing systems. In J. Pitt, editor, Self-Adaptive and Self-Organizing Systems Workshops (SASOW), pages 199–204.
IEEE CS, Apr. 2012. 2012 IEEE Sixth International Conference (SASOW 2012), Lyon, France, 10-14 Sept. 2012.
Proceedings.
[13] R. Claes, T. Holvoet, and D. Weyns. A decentralized approach for anticipatory vehicle routing using delegate
multiagent systems. IEEE Transactions on Intelligent Transportation Systems, 12(2):364–373, 2011.

44

F. DAMIANI AND M. VIROLI

[14] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, January 2000.
[15] P. Cousot. Abstract interpretation. ACM Comput. Surv., 28(2):324–328, June 1996.
[16] F. Damiani, M. Viroli, D. Pianini, and J. Beal. Code mobility meets self-organisation: A higher-order calculus of
computational fields. In S. Graf and M. Viswanathan, editors, Formal Techniques for Distributed Objects, Components,
and Systems, volume 9039 of Lecture Notes in Computer Science, pages 113–128. Springer International Publishing,
2015.
[17] R. Davies. Practical Refinement-Type Checking. PhD thesis, CMU, Pittsburgh, PA, USA, 2005.
[18] G. Delzanno. An overview of msr(c): A clp-based framework for the symbolic verification of parameterized
concurrent systems. Electronic Notes in Theoretical Computer Science, 76, 2002.
[19] E. Dijkstra. Self stabilizing systems in spite of distributed control. Communications of the Association of the
Computing Machinery, 17(11):643–644, 1974.
[20] E. Dijkstra. Ewd391 self-stabilization in spite of distributed control. In Selected Writings on Computing: A Personal
Perspective, pages 41–46. Springer-Verlag, 1982. EWD391’s original date is 1973.
[21] S. Dobson, S. Denazis, A. Fernández, D. Gaı̈ti, E. Gelenbe, F. Massacci, P. Nixon, F. Saffre, N. Schmidt, and
F. Zambonelli. A survey of autonomic communications. TAAS, 1(2):223–259, 2006.
[22] S. Dolev. Self-Stabilization. MIT Press, 2000.
[23] S. Dolev and T. Herman. Superstabilizing protocols for dynamic distributed systems. Chicago Journal of Theoretical
Computer Science, 1997.
[24] N. Elhage and J. Beal. Laplacian-based consensus on spatial computers. In W. van der Hoek, G. A. Kaminka,
Y. Lespérance, M. Luck, and S. Sen, editors, 9th International Conference on Autonomous Agents and Multiagent
Systems (AAMAS 2010), Toronto, Canada, May 10-14, 2010, Volume 1-3, pages 907–914, 2010.
[25] J. L. Fernandez-Marquez, G. D. M. Serugendo, S. Montagna, M. Viroli, and J. L. Arcos. Description and composition
of bio-inspired design patterns: a complete overview. Natural Computing, 12(1):43–67, 2013.
[26] T. Freeman and F. Pfenning. Refinement types for ml. In Proceedings of the ACM SIGPLAN 1991 Conference on
Programming Language Design and Implementation, PLDI ’91, pages 268–277, New York, NY, USA, 1991. ACM.
[27] J.-L. Giavitto, O. Michel, and A. Spicher. Spatial organization of the chemical paradigm and the specification of
autonomic systems. volume 5380 of Lecture Notes in Computer Science, pages 235–254. Springer, 2008.
[28] M. Gouda and T. Herman. Adaptive programming. IEEE Transactions on Software Engineering, 17:911–921, 1991.
[29] T. Hérault, R. Lassaigne, F. Magniette, and S. Peyronnet. Approximate probabilistic model checking. In Proc. 5th
International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI’04), volume 2937 of
LNCS. Springer, 2004.
[30] T. Herman and I. Pirwani. A composite stabilizing data structure. In WSS01 Proceedings of the Fifth International
Workshop on Self-Stabilizing Systems, Springer LNCS:2194, pages 167–182, 2001.
[31] G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems: Abstract properties
and applications to term rewriting systems. J. ACM, 27(4):797–821, Oct. 1980.
[32] A. Igarashi, B. C. Pierce, and P. Wadler. Featherweight Java: A minimal core calculus for Java and GJ. ACM
Transactions on Programming Languages and Systems, 23(3), 2001.
[33] M. Karaata and P. Chaudhuri. A self-stabilizing algorithm for strong fairness. Computing, 60:217–228, 1998.
[34] B. MacLennan. Field computation: A theoretical framework for massively parallel analog computation, parts i-iv.
Technical Report Department of Computer Science Technical Report CS-90-100, University of Tennessee, Knoxville,
February 1990.
[35] M. Mamei and F. Zambonelli. Programming pervasive and mobile computing applications: The tota approach. ACM
Trans. on Software Engineering Methodologies, 18(4):1–56, 2009.
[36] MIT Proto. software available at http://proto.bbn.com/, Retrieved January 1st, 2012.
[37] S. Montagna, D. Pianini, and M. Viroli. Gradient-based self-organisation patterns of anticipative adaptation. In
Proceedings of SASO 2012, pages 169–174. IEEE, September 2012.
[38] S. Montagna, M. Viroli, J. L. Fernandez-Marquez, G. Di Marzo Serugendo, and F. Zambonelli. Injecting selforganisation into pervasive service ecosystems. Mobile Networks and Applications, pages 1–15, September 2012.
Online first.
[39] F. Nielson, H. R. Nielson, and C. Hankin. Principles of program analysis. Springer, 1999.
[40] A. Omicini and M. Viroli. Coordination models and languages: From parallel computing to self-organisation. The
Knowledge Engineering Review, 26(1):53–59, Mar. 2011.
[41] M. Schneider. Self-stabilization. ACM Computing Surveys, 25:45–67, 1993.

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

45

[42] M. Tokoro. Computational field model: toward a new computing model/methodology for open distributed environment. In Distributed Computing Systems, 1990. Proceedings., Second IEEE Workshop on Future Trends of, pages
501–506, 1990.
[43] M. Viroli. Engineering confluent computational fields: from functions to rewrite rules. In Spatial Computing Workshop
(SCW 2013), AAMAS 2013, May 2013.
[44] M. Viroli, M. Casadei, and A. Omicini. A framework for modelling and implementing self-organising coordination.
In Proceedings of ACM SAC 2009, volume III, pages 1353–1360. ACM, 8–12 Mar. 2009.
[45] M. Viroli and F. Damiani. A calculus of self-stabilising computational fields. In E. Kühn and R. Pugliese, editors, Coordination Models and Languages, Lecture Notes in Computer Science, pages 163–178. Springer Berlin Heidelberg,
2014.
[46] M. Viroli, F. Damiani, and J. Beal. A calculus of computational fields. In C. Canal and M. Villari, editors, Advances
in Service-Oriented and Cloud Computing, volume 393 of Communications in Computer and Information Science,
pages 114–128. Springer Berlin Heidelberg, 2013.
[47] M. Viroli, D. Pianini, and J. Beal. Linda in space-time: an adaptive coordination model for mobile ad-hoc environments. In Proceedings of Coordination 2012, volume 7274 of Lecture Notes in Computer Science, pages 212–229.
Springer, 2012.
[48] M. Viroli, D. Pianini, S. Montagna, G. Stevenson, and F. Zambonelli. A coordination model of pervasive service
ecosystems. Science of Computer Programming, 110:3 – 22, 2015.
[49] D. Weyns, N. Boucké, and T. Holvoet. A field-based versus a protocol-based approach for adaptive task assignment.
Autonomous Agents and Multi-Agent Systems, 17(2):288–319, 2008.
[50] K. Whitehouse, C. Sharp, E. Brewer, and D. Culler. Hood: a neighborhood abstraction for sensor networks. In
Proceedings of the 2nd international conference on Mobile systems, applications, and services. ACM Press, 2004.
[51] F. Zambonelli, G. Castelli, L. Ferrari, M. Mamei, A. Rosi, G. D. M. Serugendo, M. Risoldi, A.-E. Tchao, S. Dobson,
G. Stevenson, J. Ye, E. Nardini, A. Omicini, S. Montagna, M. Viroli, A. Ferscha, S. Maschek, and B. Wally.
Self-aware pervasive service ecosystems. Procedia CS, 7:197–199, 2011.
[52] F. Zambonelli and M. Viroli. A survey on nature-inspired metaphors for pervasive service ecosystems. International
Journal of Pervasive Computing and Communications, 2011.

A PPENDIX A. P ROOF OF T HEOREM 5.1 AND T HEOREM 5.2
The proof are given for the calculus with pairs (cf. Section 6).
Lemma A.1 (Substitution lemma for typing). If x : T ` e : T, length(v) = length(x) and 0/ ` v : T,
then 0/ ` e[x := v] : T.
Proof. Straightforward by induction on the application of the typing rules for expressions in Fig. 4
and Fig. 13.
Lemma A.2 (Device computation type preservation). If θ ∈ WTVT(x : T, e, T), then 0/ ` ρ(θ ) : T.
Proof. Recall that the typing rules (in Fig. 4 and Fig. 13) and the evaluation rules (in Fig. 6 and
Fig. 14) are syntax directed. The proof is by induction on the definition of WTVT(x : T, e, T) (given
in Section 5.1), on the number of user-defined function calls that may be encountered during
the evaluation of e[x := v] (cf. sanity condition (iii) in Section 3.1), and on the syntax of closed
expressions.
From the hypothesis θ ∈ WTVT(x : T, e, T) we have x : T ` e : T, σ ; θ ` e[x := v] ⇓ θ for
some sensor mapping σ , evaluation trees θ ∈ WTVT(x : T, e, T), and values v such that length(v) =
length(x) and 0/ ` v : T. Moreover, by Lemma A.1 we have that 0/ ` e[x := v] : T holds. The case θ
empty represents the base of the induction on the definition of WTVT(x : T, e, T). Therefore the rest
of this proof can be understood as a proof of the base step by assuming θ = 0/ and a proof of the
inductive step by assuming θ 6= 0.
/
The case when e does non contain user-defined function calls represents the base on the
induction on the number of user-defined function calls that may be encountered during the evaluation

46

F. DAMIANI AND M. VIROLI

of e[x := v]. Therefore the rest of this proof can be understood as a proof of the base step by ignoring
the cases e[x := v] = f(e1 , ..., en ) and e[x := v] = {e0 : f(@, e1 , ..., en )} when f is a used-defined
function d. The base of the induction on e[x := v] consist of two cases.
Case s: From the hypothesis we have 0/ ` s : T where T = type(s) (by rule [T-SNS]) and σ ; θ ` s ⇓ θ
where θ = v() and v = σ (s) (by rule [E-SNS]). Since the sensor s returns values of type type(s),
we have that type(v) = type(s) = T. So the result follows by a straightforward induction of the
syntax of values using rules [T-VAL] and [T-PAIR].
Case v: From the hypothesis we have 0/ ` v : T and (by rule [E-VAL]) σ ; θ ` v ⇓ θ where θ = v(). So
the result follows by a straightforward induction of the syntax of values using rules [T-VAL] and
[T-PAIR].
For the inductive step on e[x := v], we show only the two most interesting cases (all the other cases
are straightforward by induction).
Case d(e1 , ..., en ): From the hypothesis we have 0/ ` f(e1 , ..., en ) : T (by rule T-FUN]) and σ ; θ `
d(e1 , ..., en ) ⇓ v(θ10 , ..., θn0 , v(η)) (by rule E-DEF]). Therefore we have T(T1 , ..., Tn ) = t-sig(d),
0/ ` e1 : T1 , ..., 0/ ` en : Tn (the premises of rule T-FUN]) and def T d(T1 x1 , ..., Tn xn ) = e00 ,
σ ; π1 (θ ) ` e1 ⇓ θ10 , ..., σ ; πn (θ ) ` en ⇓ θn0 and
σ ; πn+1 (θ ) ` e0 ⇓ v(η) where e0 = e00 [x1 := ρ(θ10 ), ..., xn := ρ(θn0 )]

(A.1)

(the premises of rule E-DEF]).
Since πi (θ ) ∈ WTVT(0,
/ ei , Ti ) (1 ≤ i ≤ n) then θi0 ∈ WTVT(0,
/ ei , Ti ); therefore, by induction
0
we have 0/ ` ρ(θ1 ) : T1 , ..., 0/ ` ρ(θn0 ) : Tn .
Since the program is well typed (cf. Section 3.1) we have x1 : T1 , ..., xn : Tn ` e00 : T (by rule
T-DEF]).
Since πn+1 (θ ) ∈ WTVT(x1 : T1 , ..., xn : Tn , e00 , T), then (by (A.1)) we have v(η) ∈ WTVT(x1 :
T1 , ..., xn : Tn , e00 , T); therefore, by induction we have that 0/ ` v : T.
Case {e0 : f(@, e1 , ..., en )}: From the hypothesis we have 0/ ` {e0 : f(@, e1 , ..., en )} : T (by rule T-SPR])
V
and σ ; θ ` {e0 : f(@, e1 , ..., en )} ⇓ {v0 , u1 , ..., um }(η0 , η1 , ..., ηn ) (by rule E-SPR]). Therefore we
have diffusion(f), T(T, T1 , ..., Tn ) = t-sig(d), 0/ ` e0 : T, 0/ ` e1 : T1 , ..., 0/ ` en : Tn (the premises
of rules T-SPR] and T-FUN]) and σ ; π1 (θ ) ` e1 ⇓ θ10 , ..., σ ; πn (θ ) ` en ⇓ θn0 , ρ(η0 , ..., ηn ) = v0 ...vn ,
ρ(θ ) = w1 ...wm ,
σ ; 0/ ` f(w1 , v1 , ..., vn ) ⇓ u1 (· · · ), ..., σ ; 0/ ` f(wm , v1 , ..., vn ) ⇓ um (· · · )

(A.2)

(the premises rule E-SPR]). By induction we have 0/ ` v0 ...vn : TT1 ...Tn and 0/ ` w1 : T, ..., 0/ ` wm : T.
We have two subcases:
• If f is a user-defined function, then from (A.2) we get (by reasoning as in the proof of case
d(e1 , ..., en )) 0/ ` u1 : T, ..., 0/ ` um : T.
• If f is a built-in function, then from (A.2) we get (by the semantics of built-in functions)
0/ ` u1 : T, ..., 0/ V
` um : T.
In both cases v = {v0 , u1 , ..., um } has type T, i.e., 0/ ` v : T holds.
Restatement of Theorem 5.1 (Device computation type preservation). If x : T ` e : T, σ is a
sensor mapping, θ ∈ WTVT(x : T, e, T), length(v) = length(x), 0/ ` v : T and σ ; θ ` e[x := v] ⇓ θ ,
then 0/ ` ρ(θ ) : T.
Proof. Straightforward by Lemma A.2, since θ ∈ WTVT(x : T, e, T).

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

47

Restatement of Theorem 5.2 (Device computation termination). If x : T ` e : T, σ is a sensor
mapping, θ ∈ WTVT(x : T, e, T), length(v) = length(x) and 0/ ` v : T, then σ ; θ ` e[x := v] ⇓ θ for
some value-tree θ .
Proof. By induction on the number of function calls that may be encountered during the evaluation
of e[x := v] (cf. sanity condition (iii) in Section 3.1) and on the syntax of closed expressions, using
Lemma A.2.

A PPENDIX B. P ROOF OF T HEOREM 5.3
Recall the auxiliary definitions and the outline of the proof of Theorem 5.3 given in Section 5.2. The
following six lemmas corresponds to the auxiliary results B.1-B.6 introduced in Section 5.2.
Lemma B.1 (Minimum value). Given a program e = {e0 : f(@, e1 , . . . , en )} with valid sort and
stabilising diffusion assumptions, for every reachable pre-self-stable network configuration N, for
any device ι in N such that vι(in N) is minimum (among the values of the devices in N):
ι

(1) if N =⇒ N 0 and ι 6∈ ι, then vι(in N 0 ) = vι(in N) is minimum (among the values of the devices in
N 0 ); and
(2) either vι(in N) = v0,ι (i.e., ι is self-stable in N) or if N =⇒1 N 0 then there exists v0 such that:
(a) vι(in N) < v0 ≤ vι(in N 0 ) ; and
(b) if N 0 =⇒ N 00 , then v0 ≤ vι(in N 00 ) .
Proof. Point (1). Consider a device ι 0 6= ι. Then vι(in N) ≤ vι 0 (in N) ≤ v0,ι 0 and its m ≥ 0 neighbours
have values w j such that vι(in N) ≤ w j (1 ≤ j ≤ m). Since the stabilising diffusion assumptions
V
hold, w j < [[f]](w j , v1,ι 0 , . . . , vn,ι 0 ) = u j . Therefore, vι(in N) ≤ {v0,ι 0 , u1 , ..., um } = vι 0 (in N 0 ) . So
vι(in N 0 ) = vι(in N) is minimum (among the values of the devices in N 0 ).
Point (2). Assume that vι(in N) < v0,ι . The m ≥ 0 neighbours of ι have values w j such that vι(in N) ≤ w j
(1 ≤ j ≤ m). Since the stabilising diffusion assumptions hold, vι(in N) < [[f]](vι(in N) , v1,ι , . . . , vn,ι ) =
u0 and u0 ≤ [[f]](w j , v1,ι , . . . ,Vvn,ι ) = u j . Therefore, the value v0 = v0,ι ∧ u0 is such that when ι
fires its new value vι(in N 0 ) = {v0,ι , u1 , ..., um } is such that vι(in N) < v0 ≤ vι(in N 0 ) . Moreover, since
vι(in N) < vι(in N 0 ) we have that in a firing evolution none of devices ι 0 6= ι will reach a value less than
vι(in N) and therefore the device ι will never reach a value less than v0 .
Lemma B.2 (Self-stabilisation of the minimum value). Given a program e = {e0 : f(@, e1 , . . . , en )}
with valid sort and stabilising diffusion assumptions, for every reachable pre-self-stable network
configuration N, if S1 is the subset of the devices in N such that v0,ι is minimum (among the values
of e0 in the devices in N), then there exists k ≥ 0 such that N =⇒k N 0 implies that S1 satisfies the
following conditions:
(1) each device ι in S1 is self-stable in N 0 and has value vι(in N 0 ) = v0,ι ;
(2) in N 0 each device not in S1 has a value greater or equal to the values of the devices in S1 and,
during any firing evolution, it will always assume values greater than the values of the devices in
S1 .
Proof. The number of devices in the network configuration is finite, the environment does not change,
the network is pre-self-stable, and the stabilising diffusion assumptions holds. The results follows by
Lemma B.1. Namely, if there is a device ι whose value vι is minimum and such that vι < v0,ι , then
after a 1-fair network evolution ι reaches a value which is greater or equal to some v0 such that
• v < v0 ≤ v0,ι ; and

48

F. DAMIANI AND M. VIROLI

• in any subsequent firing evolution the value of ι will be always greater or equal to v0 .
Therefore, after a finite number k of 1-fair evolutions (i.e., after any k-fair evolution) conditions (1)
and (2) in the statement of the lemma are satisfied.
Lemma B.3 (Frontier). Given a program e = {e0 : f(@, e1 , . . . , en )} with valid sort and stabilising
diffusion assumptions, for every reachable pre-stable network configuration N with devices D and a
non-empty subset of devices S ⊂ D such that
(i) each device in S is self-stable in N;
(ii) each device in D − S has a value greater or equal to the values of the devices in S and, during
any firing evolution, will always assume values greater or equal to the values of the devices in
S; and
(iii) frontierS (D) 6= 0;
/
0
if N =⇒1 N then each device in frontierS (D) is self-stable in N 0 .
Proof. When a device ι in frontierS (D) fires it gets the value
v0,ι ∧ [[f]](vι 0 , v1,ι , . . . , vn,ι )
ι0

where ∈ S is the neighbour of ι that has minimum value (among the neighbours of ι). This value is
univocally determined by environment(N) and is stable, since the values vι 0 and v j,ι (0 ≤ j ≤ n) are
stable and in any firing evolution each neighbour of ι assumes only values greater or equal to vι 0 .
Note that conditions (i)-(iii) of the following lemma are exactly the same as in Lemma B.3.
Lemma B.4 (Minimum value not in S). Given a program e = {e0 : f(@, e1 , . . . , en )} with valid sort
and stabilising diffusion assumptions, for every reachable pre-self-stable network configuration N
with devices D and a non-empty subset of devices S ⊂ D such that
(i) each device in S is self-stable in N;
(ii) each device in D − S has a value greater or equal to the values of the devices in S and, during
any firing evolution, will always assume values greater or equal to the values of the devices in
S;
(iii) frontierS (D) 6= 0;
/ and
(iv) each device in frontierS (D) is self-stable in N;
if M ⊆ D − S is the set of devices ι such that vι(in N) is minimum (among the values of the devices in
D − S), then
ι

(1) if ι ∈ M, N =⇒ N 0 and ι 6∈ ι, then vι(in N) = vι(in N 0 ) is minimum (among the values of the devices
in D − S in N 0 );
(2) if M ∩ frontierS (D) = 0,
/ then there is a device ι ∈ M such that either vι(in N) = v0,ι (i.e., ι is
self-stable in N) or if N =⇒1 N 0 then there exists v0 such that:
(a) vι(in N) < v0 ≤ vι(in N 0 ) ; and
(b) if N 0 =⇒ N 00 , then v0 ≤ vι(in N 00 ) .
Proof. Since the self-stable values in frontierS (D) ensure that in any firing evolution the values of
the devices in D − (S ∪ frontierS (D)) are computed without using the values of the devices in S, the
proof is similar to the proof of Lemma B.1.
Point (1). Consider a device ι 0 6∈ S ∪ M. Then vι(in N) ≤ vι 0 (in N) ≤ v0,ι 0 and its m ≥ 0 neighbours
have values w j such that vι(in N) ≤ w j (1 ≤ j ≤ m). Since the stabilising diffusion assumptions
V
hold, w j < [[f]](w j , v1,ι 0 , . . . , vn,ι 0 ) = u j . Therefore, vι(in N) ≤ {v0,ι 0 , u1 , ..., um } = vι 0 (in N 0 ) . So
vι(in N 0 ) = vι(in N) is minimum (among the values of the devices of D − S in N 0 ).

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

49

Point (2). Assume that vι(in N) < v0,ι . The m ≥ 0 neighbours of ι have values w j such that vι(in N) ≤ w j
(1 ≤ j ≤ m). Since the stabilising diffusion assumptions hold, vι(in N) < [[f]](vι(in N) , v1,ι , . . . , vn,ι ) =
u0 and u0 ≤ [[f]](w j , v1,ι , . . . ,Vvn,ι ) = u j . Therefore, the value v0 = v0,ι ∧ u0 is such that when ι
fires its new value vι(in N 0 ) = {v0,ι , u1 , ..., um } is such that vι(in N) < v0 ≤ vι(in N 0 ) . Moreover, since
vι(in N) < vι(in N 0 ) we have that in a firing evolution none of the devices ι 0 ∈ D − (S ∪ {ι}) will reach
a value less than vι(in N) and therefore the device ι will never reach a value less than v0 .
Note that conditions (i)-(iv) of the following lemma are exactly the same as in Lemma B.4.
Lemma B.5 (Self-stabilisation of the minimum value not in S). Given a program e = {e0 :
f(@, e1 , . . . , en )} with valid sort and stabilising diffusion assumptions, for every reachable preself-stable network configuration N with devices D and a non-empty subset of devices S ⊂ D such
that
(i) each device in S is self-stable in N;
(ii) each device in D − S has a value greater or equal to the values of the devices in S and, during
any firing evolution, will always assume values greater or equal to the values of the devices in
S;
(iii) frontierS (D) 6= 0;
/ and
(iv) each device in frontierS (D) is self-stable in N;
there exists k ≥ 0 such that N =⇒k N 0 implies that there exists a device ι1 in D − S such that
S1 = S ∪ {ι1 } satisfies the following conditions:
(1) each device ι in S1 is self-stable in N 0 ; and
(2) in N 0 any device in D − S1 has a value greater or equal to the values of the devices in S1 and,
during any firing evolution, will always assume values greater than the values of the devices in
S1 .
Proof. Let M ⊆ D − S be the set of devices ι such that vι(in N) is minimum (among the values of the
devices in D − S). We consider two cases.
M ∩ frontierS (D) 6= 0:
/ Any of the devices ι1 ∈ M ∩ frontierS (D) is such that conditions (1) and (2)
in the statement of the lemma are satisfied.
M ∩ frontierS (D) = 0:
/ The number of devices in the network configuration is finite, the environment
does not change, the network is pre-self-stable, and the stabilising diffusion condition holds. The
results follows by Lemma B.4.9 Namely, if there is a device ι ∈ M such that vι < v0,ι , then after
a 1-fair network evolution ι reaches a value which is greater or equal to some v0 such that
• v < v0 ≤ v0,ι ; and
• in any subsequent firing evolution the value of ι will be always greater or equal to v0 .
Therefore, after a finite number k of 1-fair evolutions (i.e., after any h-fair evolution with h ≥ k)
conditions (1) and (2) in the statement of the lemma are satisfied.
Lemma B.6 (Pre-self-stable network self-stabilization). Given a program e = {e0 : f(@, e1 , . . . , en )}
with valid sort and stabilising diffusion assumptions, for every reachable pre-self-stable network
configuration N there exists k ≥ 0 such that N =⇒k N 0 implies that N 0 is self-stable.
Proof. Let D be a set of devices of N. The proof is by induction on the number of devices in D.
Case D = 0:
/ Immediate.
9In particular, since the self-stable values in frontier (D) ensure that in any firing evolution the values of the devices in
S
D − (S ∪ frontierS (D)) are computed without using the values of the devices in S, the proof of this case is similar to the
proof of Lemma B.2 (by using Lemma B.4 instead of Lemma B.1).

50

F. DAMIANI AND M. VIROLI

Case D 6= 0:
/ By Lemma B.2 there exists k0 ≥ 0 such that after any k0 -fair evolution there is a
non-empty set of devices S1 that satisfies conditions (1) and (2) in the statement of Lemma B.2
(and, therefore, also conditions (1) and (2) in the statement of Lemma B.5).
Now rename S1 to S, consider a counter c intially equal to 1, and iterate the following two
reasoning steps while the set of devices S is such that frontierS (D) 6= 0:
/
• By lemma B.3 and lemma B.5 there exists kc ≥ 0 such that after any kc -fair evolution there is a
non-empty set of devices S1 that satisfies conditions (1) and (2) in the statement of Lemma B.5.
• Rename S1 to S and increment the value of c.
Since at each iteration the number devices in S is increased by one, the number of iterations is
finite (note that S = D implies frontierS (D) = 0).
/ After the last iteration, we have proved that
0 -fair evolution there is a non-empty set of devices
there exists k0 = Σc−1
k
such
that
after
any
k
j=0 j
S that satisfies conditions (1) and (2) in the statement of Lemma B.5. Since frontierS (D) = 0,
/
then the evolution of the devices in D − S is independent from the devices in S. By induction
there exists k00 ≥ 0 such that after any k00 -fair evolution the portion of the network with devices in
D − S is self-stable. Therefore, we have proved the lemma with k = k0 + k00 .
Restatement of Theorem 5.3 (Network self-stabilisation for programs that satisfy the stabilisingdiffusion condition). Given a program with valid sort and stabilising diffusion assumptions, every
reachable network configuration N self-stabilises, i.e., there exists k ≥ 0 such that N =⇒k N 0 implies
that N 0 is self-stable.
Proof. By induction on the syntax of closed expressions e and on the number of function calls that
may be encountered during the evaluation of e. Let E = environment(N).
Case v: Any device fire produces the value-tree v() (independently from E).
Case s: Each fire of device ι produces the value-tree v(), where v = σι (s) is univocally determined
by E.
Case b(e): Straightforward by induction.
Case f(e): Straightforward by induction.
Case {e0 : f(@, e1 , . . . , en )}: By induction there exists h ≥ 0 such that if N =⇒h N1 then on every
device ι, the evaluation of e0 , e1 , . . . , en produce stable value-trees θ0,ι , θ1,ι , . . . , θn,ι , which are
univocally determined by E. Note that, if N =⇒h+1 N2 then N2 is pre-self-stable. Therefore the
result follows straightforwardly by Lemma B.6.

A PPENDIX C. P ROOF OF T HEOREM 8.6
The proof of Theorem 8.6 is similar to the proof of Theorem 5.1 (cf. Appendix A)—see Remark 8.7.
0

Lemma C.1 (Substitution lemma for sorting). If x : S ` e : S, length(v) = length(x), 0/ ` v : S , and
0
S ≤ S, then 0/ ` e[x := v] : S0 for some S0 such that S0 ≤ S.
Proof. Straightforward by induction on the application of the sort-checking rules for expressions in
Fig. 19.

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

51

Lemma C.2 (Device computation sort preservation). If θ ∈ WSVT(x : S, e, S), then 0/ ` ρ(θ ) : S0 for
some S0 such that S0 ≤ S.
Proof. Recall that the sorting rules (in Fig. 19) and the evaluation rules (in Fig. 6 and Fig. 14) are
syntax directed. The proof is by induction on the definition of WSVT(x : S, e, S) (given in Section 8.6),
on the number of user-defined function calls that may be encountered during the evaluation of
e[x := v] (cf. sanity condition (iii) in Section 3.1), and on the syntax of closed expressions.
From the hypothesis θ ∈ WSVT(x : S, e, S) we have x : S ` e : S, σ ; θ ` e ⇓ θ for some sensor
mapping σ , evaluation trees θ ∈ WSVT(x : S, e, S), and values v such that length(v) = length(x),
0
0
0/ ` v : S , and S ≤ S. The case θ empty represents the base of the induction on the definition of
WSVT(x : S, e, S). Therefore the rest of this proof can be understood as a proof of the base step by
assuming θ = 0/ and a proof of the inductive step by assuming θ 6= 0.
/ Moreover, by Lemma C.1 we
0
0
0
have that 0/ ` e[x := v] : S for some S such that S ≤ S.
The case when e does non contain user-defined function calls represents the base on the
induction on the number of user-defined function calls that may be encountered during the evaluation
of e[x := v]. Therefore the rest of this proof can be understood as a proof of the base step by ignoring
the cases e[x := v] = f(e1 , ..., en ) and e[x := v] = {e0 : f(@, e1 , ..., en )} when f is a used-defined
function d. The base of the induction on e[x := v] consist of two cases.
Case s: From the hypothesis we have 0/ ` s : S where S = sort(s) (by rule [T-SNS]) and σ ; θ ` s ⇓ θ
where θ = v() and v = σ (s) (by rule [E-SNS]). Since the sensor s returns values of sort sort(s),
we have that sort(v) ≤ sort(s) = S. So the result follows by a straightforward induction of the
syntax of values using rules [S-VAL] and [S-PAIR].
Case v: From the hypothesis we have 0/ ` v : S and (by rule [E-VAL]) σ ; θ ` v ⇓ θ where θ = v(). So
the result follows by a straightforward induction of the syntax of values using rules [S-VAL] and
[S-PAIR].
For the inductive step on e[x := v], we show only the two most interesting cases (all the other cases
are straightforward by induction).
Case d(e1 , ..., en ): From the hypothesis we have 0/ ` f(e1 , ..., en ) : S (by rule S-FUN]) and
σ ; θ ` d(e1 , ..., en ) ⇓ v(θ10 , ..., θn0 , v(η)) (by rule E-DEF]). Therefore we have S(S1 , ..., Sn ) =
ms(s-sigs(f), S01 , . . . , S0n ), 0/ ` e1 : S01 , ..., 0/ ` en : S0n and S01 ≤ S1 , ..., S0n ≤ Sn (by the premises of
rule S-FUN]) and def T d(T1 x1 , ..., Tn xn ) = e00 , σ ; π1 (θ ) ` e1 ⇓ θ10 , ..., σ ; πn (θ ) ` en ⇓ θn0 and
σ ; πn+1 (θ ) ` e0 ⇓ v(η) where e0 = e00 [x1 := ρ(θ10 ), ..., xn := ρ(θn0 )]

(C.1)

(the premises of rule E-DEF]).
Since πi (θ ) ∈ WSVT(0,
/ ei , S0i ) (1 ≤ i ≤ n), then θi0 ∈ WSVT(0,
/ ei , S0i ); therefore, by induction
we have 0/ ` ρ(θ10 ) : S001 , ..., 0/ ` ρ(θn00 ) : S00n and S001 ≤ S01 ≤ S1 , ..., S00n ≤ S0n ≤ Sn .
Since the program is well sorted (cf. Section 8.5) we have x1 : S1 , ..., xn : Sn ` e00 : S0 and S0 ≤ S
(by rule T-DEF]).
Since πn+1 (θ ) ∈ WTVT(x1 : S1 , ..., xn : Sn , e00 , S0 ), then (by (C.1)) we have v(η) ∈ WTVT(x1 :
S1 , ..., xn : Sn , e00 , S0 ); therefore, by induction we have that 0/ ` v : S00 with S00 ≤ S0 ≤ S.
Case {e0 : f(@, e1 , ..., en )}: From the hypothesis we have 0/ ` {e0 : f(@, e1 , ..., en )} : S0 (by rule
V
S-SPR]) and σ ; θ ` {e0 : f(@, e)} ⇓ {v0 , u1 , ..., um }(η0 , η1 , ..., ηn ) (by rule E-SPR]). Therefore
0
0
we have diffusion(f), S ` e0 e : S00 S , S0 (S0 S) = ms(stb-s-sigs(f), S00 S ), S = sup≤ (S00 , S0 ) and
0
S00 S ≤ S0 S (by the premises of rule S-SPR]) and σ ; π1 (θ ) ` e1 ⇓ θ10 , ..., σ ; πn (θ ) ` en ⇓ θn0 ,
ρ(η0 , ..., ηn ) = v0 ...vn , ρ(θ ) = w1 ...wm ,
σ ; 0/ ` f(w1 , v1 , ..., vn ) ⇓ u1 (· · · ), ..., σ ; 0/ ` f(wm , v1 , ..., vn ) ⇓ um (· · · )

(C.2)

52

F. DAMIANI AND M. VIROLI

(the premises rule E-SPR]). By induction we have 0/ ` v0 ...vn : S000 S001 ...S00n with S000 S001 ...S00n ≤ S00 S01 ...S0n
000
and 0/ ` w1 : S000
/ ` wm : S000
m with Sl ≤ S ≤ S0 (1 ≤ l ≤ m). We have two subcases.
1 , ..., 0
• If f is a user-defined function, then from (C.2) we get (by reasoning as in the proof of case
0000
0000
0
d(e1 , ..., en )) 0/ ` u1 : S0000
/ ` um : S0000
m for some Sl such that Sl ≤ S (1 ≤ l ≤ m).
1 , ..., 0
• If f is a built-in function, then from (C.2) we get (by the semantics of built-in functions)
0000
0000
0
0/ ` u1 : S0000
/ ` um : S0000
m for some Sl such that Sl ≤ S (1 ≤ l ≤ m).
1 , ...,V0
00
000
In both cases v = {v0 , u1 , ..., um } has a sort S with S ≤ S, i.e., 0/ ` v : S000 with S000 ≤ S holds.
Restatement of Theorem 8.6 (Device computation sort preservation). If x : S ` e : S, σ is a sensor
0 0
mapping, θ ∈ WSVT(x : S, e, S), length(v) = length(x), 0/ ` v : S , S ≤ S, and σ ; θ ` e[x := v] ⇓ θ ,
then 0/ ` ρ(θ ) : S0 for some S0 such that S0 ≤ S.
Proof. Straightforward by Lemma C.2, since θ ∈ WSVT(x : S, e, S).
A PPENDIX D. P ROOF OF T HEOREM 9.5
Lemma D.1 (Annotated sort of an expression). If x1 : S1 [?], x : S ` e : S[π], then x : S1 , x : S ` e : S
and >key(S1 ) = >key(S) .
Proof. Straightforward by induction on the application of the annotated sort checking rules for
expressions in Fig. 23.
A pure expression e with free variables x of sorts S represents the pure function that for every
v ∈ [[S]] returns the value [[e[x := v]]]. In the following we will write fun(e) to denote such a function.
Lemma D.2 (Annotation soundness for expressions). If , x1 : S1 [?], x : S ` e : S[π] and v ∈ [[S]],
then
(1) if π = ! then
• v <1S1 v0 and [[fun(e)]](v, v) = v00 6=1S >S imply implies v00 <1S [[fun(e)]](v0 , v);
• for all v ∈ [[S1 ]] − {>S1 }, key(v) <key(S1 ) key([[fun(e)]](v, v));
(2) if π ∈ {!, ?} then
• v ≤1S1 v0 implies [[fun(e)]](v, v) ≤1S [[fun(e)]](v0 , v);
• for all v ∈ [[S1 ]], key(v) ≤key(S1 ) key([[fun(e)]](v, v)).
Proof. By Lemma D.1 [[e]] has sort S(S1 S) and either key(S1 ) ≤progressive key(S) or key(S) ≤progressive
key(S1 ). Recall that the annotated sort checking rules (in Fig. 23) and the evaluation rules (in Fig. 6
and Fig. 14) are syntax directed. By induction on the syntax of pure expressions e. The base of the
induction on e consist of two cases.
Case x: Immediate by rule [A-VAR].
Case v: Straightforward by rule [A-GVAL] and Proposition 7.5.
For the inductive step on e, we show only the case for function application (all the other cases are
straightforward by induction).
Case f(e1 , e): Then the premises of rule [A-FUN]:
• A ` e1 : S01 [π 00 ]
0
• |A | ` e : S
00
• S(S001 S )[π 0 ] ∈ ms(a-s-sigs(f), S01 S0 )
00
hold and π = π 0 (π 00 ). By the last premise, we have that π 0 -prestabilising(f, S(S001 S )) holds.
Then, the result follows straightforward by induction (using Definition 7.1).

TYPE-BASED SELF-STABILISATION FOR COMPUTATIONAL FIELDS

Restatement of Theorem 9.5 (Annotation soundness).
π-prestabilising(f, S(S)) holds for all S(S)[π] ∈ S(S)[π].

53

If ` D : S(S)[π] holds, then

Proof. Straighforward from rule [A-DEF] in Fig. 19 using Lemma D.2 and Proposition 7.4.

This work is licensed under the Creative Commons Attribution-NoDerivs License. To view
a copy of this license, visit http://creativecommons.org/licenses/by-nd/2.0/ or send a
letter to Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or
Eisenacher Strasse 2, 10777 Berlin, Germany

