has to occur

Computation Against a Neighbour

G. Audrito]Giorgio Audrito
Università degli Studi di Torino, Corso Svizzera 185

R. Casadei]Roberto Casadei
Alma Mater Studiorum–Università di Bologna, Via Cesare Pavese, 50

F. Damiani]Ferruccio Damiani
Università degli Studi di Torino, Corso Svizzera 185

M. Viroli]Mirko Viroli
Alma Mater Studiorum–Università di Bologna, Via Cesare Pavese, 50

Recent works in contexts like the Internet of Things (IoT) and large-scale Cyber-Physical Systems (CPS) propose the idea of programming distributed systems by focussing on their global behaviour across space and time.

In this view, a potentially vast and heterogeneous set of devices is considered as an “aggregate”
to be programmed as a whole, while abstracting away the details of individual behaviour and exchange of messages, which are expressed declaratively.

One such a paradigm, known as aggregate programming,
builds on computational models
inspired by field-based coordination.

Existing models such as the field calculus capture interaction with neighbours by a so-called “neighbouring field” (a map from neighbours to values). This requires ad-hoc mechanisms to smoothly compose with standard values, thus complicating programming and introducing clutter in aggregate programs, libraries and domain-specific languages (DSLs).

To address this key issue we introduce the novel notion of “computation against a neighbour”,
whereby the evaluation of certain subexpressions of the aggregate program are affected by recent corresponding evaluations in neighbours.

We capture this notion in the  (), a new field calculus variant
which is shown to smoothly support declarative specification of interaction with neighbours, and correspondingly facilitate the embedding of field computations as internal DSLs in common general-purpose programming languages—as exemplified by a Scala implementation, called .

This paper formalises ,
thoroughly compares it with respect to the classic field calculus,
and shows its expressiveness by means of a case study in edge computing, developed in .

§ INTRODUCTION

Pervasive computing, Internet of Things (IoT), Cyber-Physical Systems (CPS), Smart Cities and related initiatives,
all point out a trend in informatics envisioning a future where computation is fully pervasive and ubiquitous,
and is carried on by a potentially huge and dynamic set of heterogeneous devices deployed in physical space.

To address the intrinsic complexity of these settings, a new viewpoint is increasingly emerging:
a large-scale network of devices, situated in some environment (e.g., the urban area of a smart city),
can be seen as a computational overlay of the physical world, to be programmed as a single “distributed machine”.

These kinds of systems are sometimes referred to as Collective Adaptive Systems (CAS) [3],
to emphasise that computational activities are collective (i.e., they involve multiple coordinated individuals),
and that a main expected advantage is inherent adaptivity of behaviours to unforeseen changes—whether they are changes/faults
in the computational environment or pertain unexpected interaction with humans or other systems.

Aggregate Computing [14] is an approach to CAS engineering
that takes a global perspective to design and programming.

Its key idea is to declaratively program a large system as a whole, that is, to directly consider an ensemble of devices as the target machine to be programmed, providing an abstraction over individual behaviour and exchange of messages.

Then, it provides under-the-hood, automatic, global-to-local mapping:
once the desired system-level behaviour is expressed by a global program, then individual computational entities of an aggregate are bound to play a derived, contextualised local behaviour of that program.

This approach is especially suitable to problems and application domains such as crowd engineering, complex situated coordination, robot/UAV swarms, smart ecosystems and the
like [57].

One fundamental enabling abstraction for specifying the dynamics of situated collectives
is that of a computational field (or simply, field) [9, 10, 43]: a distributed data structure that
maps devices to computational objects across time.

Accordingly, Aggregate Programming is about describing field computations, namely, how input fields (data coming from sensors) turn into output fields
(actions feeding actuators)—computations that can be conveniently expressed using the functional paradigm.

From an operational perspective, the approach works by deploying the same piece of program (also called aggregate program) to the devices making up the aggregate system,
and having any device asynchronously and repeatedly run such program against its local context (built from sensor readings and messages from neighbour devices),
according to a local semantics enacted by a locally installed “aggregate virtual machine”.

The state-of-the-art aggregate programming constructs, formalised by the field calculus [57, 9] and implemented by  Domain Specific Languages (DSLs) such as Proto (a Scheme external DSL) [10], Protelis (a Java external DSL) [50],
FCPP (a C++ internal DSL) [8], rely on
the notion of “neighbouring value” (a map from neighbours to data values) to model device interaction.

It is used to locally express the outcome of message reception from neighbours, and to manipulate such information to collect resulting values.

As a consequence, these languages need two classes of operators and types:
one for dealing with local values,
and one for dealing with collection-like, neighbouring values.

Managing and reconciling these two kinds of operations may tend to complicate aggregate programming, design of libraries, and language implementation.

Existing DSLs deal with this issue in a variety of ways: relying on dynamic typing (as in Proto), using macros and meta-programming techniques to alleviate such issues to the user (as in FCPP), or requiring duplication of operation across local and neighbouring values (as in Protelis)—none of which is completely satisfactory.

In order to resolve the duality of local/neighbouring values, with the goal of conceptual economy and to promote smooth embedding of field computations in mainstream languages and programming practice, in this paper we introduce a novel notion of “computation against a neighbour”, used to express interaction in field-based coordination by entirely replacing the notion of neighbouring value.

The key idea is to allow the evaluation of a certain sub-expression of the aggregate program to depend on a recent outcome of the evaluation of the same subexpression in a neighbour.

Such a dependency is hence expressed fully declaratively, without escaping the functional paradigm of field-based computing, and is then internally implemented by asynchronous message exchange across neighbours.

To present this mechanism and study its implications, in this paper we:

* define syntax, typing, operational semantics of a foundation calculus, called  ();

* investigate the properties of the  and its relationship with the field calculus;

* show the advantages that  brings in term of smooth embedding into mainstream programming.

In particular, the last contribution is based on the implementation of the  computational model in [<https://github.com/scafi/scafi>] (Scala Fields).

is a Scala [52] aggregate programming toolkit comprising an internal DSL for aggregate programming, which has been used in a variety of
applications [29, 25, 27, 18].

Hence, in addition to formalising the “computation against a neighbour” mechanism,  also serves as formalisation of the core of .

The remainder of this paper is structured as follows.

<Ref> provides background information about Aggregate Computing and field computations.

<Ref> describes syntax, typing, and operational semantics  of .

<Ref> provides a detailed account on the properties of , by comparison with the field calculus.

<Ref> presents the  Scala-based  implementation, and the key advantage of the approach over other implementations approaches for field calculi.

<Ref> describes an edge computing case study built on /.

Finally, <Ref> summarises related works, and

<Ref> ends up the paper with a wrap-up and discussion of future works.

§ BACKGROUND

In this section, we recap Aggregate Computing (<Ref>) and its formal embodiment into a computational model based on a field abstraction (<Ref>), as a response to the need of engineering the collective adaptive behaviour of large-scale distributed and physically situated systems.

§.§ Aggregate Computing

Aggregate Computing is an approach to CAS development
that abstracts from the traditional, device-centric viewpoint (where the programs describe what a device should do)
in favour of a “holistic stance” where the target of design/development is the whole collection of situated and interacting devices that compose the system, seen as a single programmable, distributed, computational body [14].

The core idea is to provide a specification of how the system globally behaves without even mentioning the existence of individuals, and hence independently of the shape and size of the set of devices: it is “under-the-hood” that the local behaviours to be executed by the individual devices are derived.

This approach may be labelled as a macro-to-micro one, to differentiate it from the more classical (micro-to-macro) approach where the components are individually implemented in order to produce the intended system-level behaviour by more or less “controlled” emergence.

Hence, from the programming perspective, the key advantage is the ability of declaratively expressing the logic of an ensemble, avoiding to directly solve the generally intractable local-to-global mapping problem and clearly separating the concerns of overall aggregate behaviour from the device-specific ones.

The general idea of programming at the macro level dates back to works such as [46, 13] in the context of wireless sensor networks, but it has recently received considerable renewed interest (see, e.g., the
survey [12] and the many related approaches mentioned in <Ref>) with the emergence of the IoT.
In this research context, the key contribution of Aggregate Computing lies in supporting abstract and resilient composition of collective adaptive behaviours.

Since an aggregate program is expressed in a way that is independent of the actual number and dislocation of devices – and the resulting computation is a repetitive, gossip-like process of data distribution and computation – adaptation to changes and faults is inherent, and can be controlled by relying on specific programming patterns [58], often biologically inspired.

Then, at this level, compositionality refers to the capability of combining behaviours in such a way that the result of the combination,
and its properties, are in several cases fully predictable
[16, 56, 60].

In particular, self-stabilisation is retained by a large class of aggregate programs: it makes an aggregate system able to tolerate circumscribed failures and react to disruptive changes in the environment in order to re-establish, after some transient adjusting phase, the proper operation.

§.§ Computing with Fields

Dynamic view of a computational field: a field maps devices to values over time; devices can enter and exit a given space-time domain freely (openness); devices fire asynchronously (possibly at varying rates), execute a computational round upon fires producing the local value of the field, and  then “sleep” in between fires. At a given time, a snapshot of the most-recent value at each device gives a field value (this view of an external, global observer is conceptually useful but global fields are not to be computationally manipulated in a direct fashion).
A device can only directly communicate with a subset of other devices which is known as its neighbourhood (e.g., for $\delta_2$, represented by the green area), which usually (but not necessarily) reflects spatial proximity in situated systems.

The computational framework incarnating the ideas and goals of Aggregate Computing
is based on the notion of computational field (or simply field) [57].

Intuitively, as shown in <Ref>, a computational field is an abstraction that represents a distributed data structure mapping points in space-time (the field domain) to values produced (by some device) as computation result at those points.

Programming field computations hence encourages to reason in terms of evolving global structures that continuously express both the result of computation and the relationships between individuals.

Field computations generally comprise mechanisms for:
(i) lifting standard values and computations, which are “local”, to work as whole fields by flatly applying them to each space-time point of the domain;
(ii) expressing the dynamics of fields, namely, how fields evolve over time;
(iii) exchanging values across neighbours, such that information can flow beyond localities and interaction can unfold to realise complex patterns such as, e.g., outward propagation of local events; and
(iv) branching fields into spatio-temporally-isolated sub-fields, in order to organise a computation into multiple parts co-existing in different space-time regions.

Inspired by
minimal core
calculi such as $\lambda$-calculus [20]
and FJ [38], the above mechanisms
have been formalised by the field calculus  [9].
The field calculus relies on the basic functional programming model abstractions (i.e., first-class functions and functional composition) to support composability of distributed behaviour.

In a nutshell,
expressions denote whole fields; a specific construct, called , deals with field dynamics;
another construct, called , declaratively expresses interaction with neighbours; finally, higher-order function call captures behaviour activation as well as branching (as a “field of functions” can be invoked through the call operator, space-time regions are naturally defined by where/when the same function is actually called).

As suggested in <Ref>, field computations assume a set of networked devices that
run at asynchronous or partially synchronous rounds of execution.
It is such an iterative execution that, combined with repetitive local sensing
and device-to-device interaction,
enables intrinsic adaptation to environmental perturbations
and progressive steering of the system towards the desired states—much like in swarm and computational collective intelligence [11, 54].
In each computation round, a device: (i) determines its local context,
by retrieving any previous state and collecting sensor values as well as messages potentially received from its neighbours;
(ii) locally executes a field computation expression, in a contextual fashion and
according to the local semantics, producing an output and
an export value which provides information for collective coordination;
(iii) shares the export with its neighbours, through a conceptual broadcast;
and finally (iv) feeds actuators, with the produced output.
In other words, this execution model implements a sort of distributed, continuous closed loop
between field computation and the environment, where each device computes values
that are contextually related with those computed by neighbours.

§ THE

This section presents  the (), a minimal core calculus that models aggregate computing via computations against a neighbour, instead of the neighbouring values used in the higher-order field calculus () [9]—a thoughtful comparison between  and  is presented in Section <ref>.

Devices undergo computation in rounds. When a round starts, the device gathers information about messages received from neighbours (only the last message from
each neighbour is actually considered), performs an evaluation of the program, and finally emits a message to all neighbours with information about the outcome of
computation. The scheduling policy of such rounds is abstracted in this formalisation, though it is typically considered fair and non-synchronous.

<Ref> presents the syntax of ;
<Ref> presents its type system;
<Ref> presents an operational semantics for the computation that takes place on individual devices;
and  <Ref> presents an operational semantics for the evolution of whole networks.

§.§ Syntax

The syntax of  is given in Figure <ref>.
Following [38], the overbar notation denotes metavariables over sequences and the empty sequence is denoted  by $\emptyseq$;
e.g., for expressions, we let $\overline\e$ range over sequences of expressions, written $\e_1,\,\e_2,\,\ldots\,\e_n$ $(n\ge 0)$.
focusses on aggregate programming constructs: hence,

it is  parametric in the set of built-in data constructors and functions. In the examples, we consider the set of built-in data constructors and functions listed (with their types) in Section <ref>.

\begin{array}{l@{\hspace{1mm}}c@{\hspace{1mm}}l@{\hspace{20mm}}r}
\PROGRAM & \BNFcce & \overline{\FUNCTION}  \; \e
&   {\footnotesize \mbox{program}}                                                                                \\[3pt]
\FUNCTION & \BNFcce &  \defK \; \fname (\overline{\xname}) \; \eqSymK{\e}                                                                                &   {\footnotesize \mbox{function declaration}}
\\[3pt]
\e & \BNFcce & \xname \, \BNFmid \, \anyvalue \, \BNFmid \, (\overline{\xname}) \; \toSymK{\e} \, \BNFmid \, \e(\overline{\e}) \, \BNFmid \,
%\repK(\e)\{ \e \}
\repK(\e)\{ \e \}
\, \BNFmid \, \nbrK\{\e\}
&   {\footnotesize \mbox{expression}} \\[1pt]
& \BNFmid & \foldK(\e, \e, \e)
\\[3pt]
\anyvalue & \BNFcce &  {\dc(\overline{\anyvalue})} \; \BNFmid \; \funvalue                                                                                &   {\footnotesize\mbox{value}}
\\[3pt]
\funvalue & \BNFcce & \bname \; \BNFmid \; \fname \; \BNFmid \; (\overline{\xname}) \; \toSymK{\e}                                                                                &   {\footnotesize\mbox{function value}} \\
\end{array}

Syntax of .

A program  $\PROGRAM$ consists of a sequence $\overline{\FUNCTION}$ of function declarations and a main expression $\e$.
A function declaration  $\FUNCTION$ defines a (possibly recursive) function; it consists of a name $\fname$, $n\ge 0$ variable names $\overline{\xname}$ representing the formal parameters, and an expression $\e$ representing the body of the function.

Expressions $\e$ are the main entities of the calculus, modelling a whole field computation. An expression can be:
a variable $\xname$, used as function formal parameter;
a value $\anyvalue$;
an anonymous function $(\overline{\xname}) \; \toSymK{\e}$ (where $\overline{\xname}$ are the formal parameters and $\e$ is the body),

a function call $\e(\overline{\e})$;
a $\repK$-expression $\repK(\e)\{\e\}$, modelling time evolution;
an $\nbrK$-expression $\nbrK\{\e\}$, modelling  neighbourhood interaction;
or a $\foldK$-expression $\foldK(\e,\e,\e)$ which combines values obtained from neighbours.

The set of the free variables of an expression $\e$, denoted by $\FV{\e}$, is defined as usual (the only binding construct is
$(\overline{\xname}) \; \toSymK{\e}$). An expression $\e$ is closed  if $\FV{\e}=\emptyseq$. The main expression of a program must be closed.

A value can be either a data value $\dc(\overline{\anyvalue})$ or a functional value $\funvalue$.
A data value consists of a data constructor $\dc$ of some arity $m\ge 0$ applied to a sequence of $m$ data values
$\overline{\anyvalue}=\anyvalue_1,...,\anyvalue_m$. For readability, the parenthesis may be omitted for arity $m=0$, writing $\dc()$ as $\dc$.
According to the data constructors listed in Figure <ref>, examples of data values are:
the Booleans $\truevalue$ and $\falsevalue$, numbers, pairs (like $\PairK(\truevalue,\PairK(5,7))$) and lists (like $\ConsK(3,\ConsK(4,\NullK))$).

Functional values $\funvalue$ comprise:

* declared function names $\fname$;

* closed anonymous function expressions $(\overline{\xname}) \; \toSymK{\e}$ (i.e., such that $\FV{\e} \subseteq \{\overline\xname\}$);

* built-in functions $\bname$, which can in turn be:

* pure operators $\oname$, such as functions for building and decomposing pairs (, , )
and lists (, , ),

the equality function ($=$), mathematical and logical functions (, , ...), and so on;

* sensors $\svalue$, which depend on the current environmental conditions of the computing device $\deviceId$, such as a  sensor;

* relational sensors $\snvalue$,
which in addition depend also on a specific neighbour device $\deviceId'$ (e.g., $\texttt{nbrRange}$, which measures the distance with a neighbour device).

In case $\e$ is a binary built-in function $\bname$, we  write
$\e_1 ~\bname~ \e_2$ for the function call $\bname(\e_1,\e_2)$ whenever convenient for readability of the whole expression in which it is contained.

The key constructs of the calculus are:

* Function  call: $\e(\e_1,\ldots,\e_n)$ is the main construct of the language.
The function call evaluates to the result of applying the function value $\funvalue$ produced by the evaluation of $\e$  to the value of the parameters $\e_1, \ldots, \e_n$
relatively to the aligned neighbours, that is, relatively to the neighbours that  in their last execution round
have evaluated $\e$ to a function value
with the same name of  $\funvalue$. Hence, calling a declared or anonymous function acts as a branch, with each function in the range applied only on the subspace of devices holding a (syntactically) identical function.

* Time evolution: $\repK (\e_1)\{\e_2\}$ is a
construct for dynamically changing fields through the “eated” application of the functional expression $\e_2$.

At the first computation round
(or, more precisely, when no previous state is available—e.g., initially or at re-entrance after state was cleared out due to branching), $\e_2$ is applied to $\e_1$, then at each other step it is applied to the value obtained at the previous step.
For instance, $\repK(0)\{(\xname)\; \toSymK{\xname + 1}\}$ counts how many rounds each device has computed (from the beginning, or more generally, since that piece of state was missing).

* Neighbourhood interaction: $\foldK(\e_1, \e_2, \e_3)$ and $\nbrK \{\e\}$ model device-to-device interaction, and are at the core of the “computation against a neighbour” mechanism.
The $\foldK$ construct evaluates expression $\e_3$ against every aligned neighbour (excluding the device itself),
then aggregates the values collected through binary operator $\e_2$ together with the initial value $\e_1$.
Used inside $\e_3$, the $\nbrK$ construct tags a sub-expression $\e$ signalling that, when evaluated against a neighbour $\deviceId$, it should not be actually evaluated as usual, but should give as result the one obtained by evaluating $\e$ in $\deviceId$. Put in other words, when evaluated against $\deviceId$, $\nbrK \{\e\}$ means “observing” the recent resulting value of $\e$ in $\deviceId$—and also let later $\deviceId$ observe the local valued of $\e$, conversely.
Such behaviour is implemented via a conceptual broadcast of the values evaluated for $\e$. Subexpressions of $\e_3$ not containing $\nbrK$ are evaluated as usual instead, i.e., with no gathering of information from neighbours.

As an example, consider the expression
\[\foldK(2, \texttt{+}, \texttt{min}(\nbrK\{\texttt{temperature}()\}, \texttt{temperature}()) )\]

evaluated in device $\deviceId_1$ (in which $\texttt{temperature}() = 10$) with neighbours $\deviceId_2$ and $\deviceId_3$
(in which $\texttt{temperature}()$ gave $15$ and $5$ in their last evaluation round, orderly).
The result of the expression is then computed adding $2$, $\texttt{min}(15,10)$ and $\texttt{min}(5,10)$ for a final value of $17$.

§.§.§ Additional syntactic sugar
To facilitate specification of examples, we  write $\ifK (\e_1) \{ \e_2 \} \{ \e_3 \}$ as a shorthand for $\muxK(\e_1, () ~\toSymK{\e_2}, () ~\toSymK{\e_3})()$, where the multiplexer function $\muxK$ selects between its second and third argument based on the value of the first, in formulas: $\muxK(b, \anyvalue_\top, \anyvalue_\bot) = \anyvalue_b$.

Additionally, in order to improve readability, we  also sometimes write $\letK \; \xname = \e_1 \; \inK \; \e_2$  as syntactic sugar for $((\xname) \toSymK{\e_2}) \, (\e_1)$.

§.§ Typing

We now present a type system for . Since the type system is a customisation of the Hindley-Milner type system [33],
there is an algorithm (not presented here) that, given an expression $\e$ and type assumptions for its free variables,
either fails (if the expression cannot be typed under the given type assumptions) or returns its principal type, i.e.,
a type such that all the types that can be assigned to $\e$ by the type inference rules can be obtained from the principal type by substituting
type variables with types. The syntax of type and type schemes is presented in Figure <ref> (top),
where $\builtintype$ ranges over the built-in types provided by the language (such as $\ntype$, $\btype$, $\pairltypeOf{\type_1}{\type_2}$, $\listltypeOf{\type}$).
The set of type variables occurring in a type $\type$ is denoted by $\FTV{\type}$.

[1]
%%%  TYPES
\textbf{Types:}\\
<EMAIL_ADDRESS>\type & \BNFcce &  \tvar  \; \BNFmid \;  \builtintype \; \BNFmid \;  (\overline\type) \rightarrow \type        &   {\footnotesize \mbox{type}} \\
\typescheme & \BNFcce &  \forall\overline{\tvar}.\type      &   {\footnotesize \mbox{type scheme}} \\
%\localenv & \BNFcce & \envS{\senstate}{\overline\vtree} &   {\footnotesize \mbox{local environment}} \\
\end{array}\\
\hline\\[-8pt]
%%%  TYPE RULES
\textbf{Expression typing:}
\hfill
\boxed{\expTypJud{\TStypEnv}{\TtypEnv}{\e}{\type}}
\vspace{0.1cm}
\\
\begin{array}{c}
\nullsurfaceTyping{T-VAR}{
\expTypJud{\TStypEnv}{\TtypEnv,\xname:\type}{\xname}{\type}
\qquad
\surfaceTyping{T-DAT}{ \quad
\applySubstitution{\type'}{\substitution{\overline\tvar}{\overline\type''}} = (\overline{\type})\rightarrow\type
\qquad
\expTypJud{\TStypEnv}{\TtypEnv}{\overline{\anyvalue}}{\overline{\type}}
\expTypJud{\TStypEnv,\dc: \forall \overline{\tvar}. \type'}{\TtypEnv}{\dc(\overline{\anyvalue})}{\type} }
\skiptransition
\surfaceTyping{T-A-FUN}{ \quad
\expTypJud{\TStypEnv}{\;\TtypEnv,\,\overline{\xname}:\overline{\type}}{\e}{\type}
}{ \expTypJud{\TStypEnv}{\TtypEnv}{ (\overline{\xname}) \toSymKtag{\name}{\e}}{(\overline{\type})\rightarrow\type} }
\qquad
\surfaceTyping{T-N-FUN}{ \quad
\mbox{$\funvalue$ is a (built-in or declared) function}}{
\expTypJud{\TStypEnv,\funvalue: \forall \overline{\tvar}. \type}{\TtypEnv}{\funvalue}{\applySubstitution{\type}{\substitution{\overline\tvar}{\overline\type}}} }
\skiptransition
\surfaceTyping{T-APP}{ \quad
\expTypJud{\TStypEnv}{\TtypEnv}{\e}{(\overline{\type})\rightarrow\type} \qquad
\expTypJud{\TStypEnv}{\TtypEnv}{\overline{\e}}{\overline{\type}} }{
\expTypJud{\TStypEnv}{\TtypEnv}{\e(\overline{\e})}{\type} }
\skiptransition
%\surfaceTyping{T-BRANCH}{ \qquad
%\quad \expTypJud{\TStypEnv}{\TtypEnv}{\e_2}{\type}
%\quad \expTypJud{\TStypEnv}{\TtypEnv}{\e_3}{\type} }{
%\expTypJud{\TStypEnv}{\TtypEnv}{\ifK(\e_1) \{\e_2\} \{\e_3\} }{\type} }
\surfaceTyping{T-REP}{ \qquad
\expTypJud{\TStypEnv}{\TtypEnv}{\e_1}{\type}
\qquad \expTypJud{\TStypEnv}{\TtypEnv}{\e_2}{(\type)\to \type} }{
\expTypJud{\TStypEnv}{\TtypEnv}{\repK(\e_1)\{\e_2\}}{\type} }
\qquad\qquad
\surfaceTyping{T-NBR}{ \qquad
\expTypJud{\TStypEnv}{\TtypEnv}{\e}{\type}
}{ \expTypJud{\TStypEnv}{\TtypEnv}{\nbrK\{\e\}}{\type} }
\skiptransition
\surfaceTyping{T-FOLD}{ \qquad
\expTypJud{\TStypEnv}{\TtypEnv}{\e_1}{\type}
\quad \expTypJud{\TStypEnv}{\TtypEnv}{\e_2}{(\type, \type) \to \type}
\quad \expTypJud{\TStypEnv}{\TtypEnv}{\e_3}{\type} }{
\expTypJud{\TStypEnv}{\TtypEnv}{\foldK(\e_1, \e_2, \e_3) }{\type} }
\skiptransition
\end{array}
\\
\textbf{Function typing:}
\hfill
\boxed{\funTypJud{\TStypEnv}{\FUNCTION}{\typescheme}}
\\
\begin{array}{c}
\surfaceTyping{T-FUNCTION}{
\qquad
\expTypJud{\TStypEnv,\,\fname:\forall\emptyseq.(\overline{\type})\rightarrow\type}{\overline{\xname}:\overline{\type}}{\e}{\type}
\qquad
\overline{\tvar}=\FTV{(\overline{\type})\rightarrow\type}
}{ \funTypJud{\TStypEnv}{\defK \; \fname (\overline{\xname}) \; \eqSymK{\e}}{\forall\overline{\tvar}.(\overline{\type})\rightarrow\type}}
\skiptransition
\end{array}
\\
\textbf{Program typing:}
\hfill
\boxed{\proTypJud{\PROGRAM}{\type}}
\\
\begin{array}{c}
\surfaceTyping{T-PROGRAM}{
\\
\TStypEnv_0=\OStypEnv
\\
\FUNCTION_i = \defK \; \fname_i (\_) \; \eqSymK{\_}
\qquad
\funTypJud{\TStypEnv_{i-1}}{\FUNCTION_i}{\typescheme_i}
\qquad
\TStypEnv_i=\TStypEnv_{i-1},\, \fname_i:\typescheme_i
\qquad
(i \in 1..n)
\\
\expTypJud{\TStypEnv_n}{\emptyset}{\e}{\type}
}{ \proTypJud{\FUNCTION_1\cdots\FUNCTION_n  \;
\e}{\type}}
\end{array}
\end{array}$
Type rules for expressions, function declarations, and programs.

Type environments, ranged over by $\TtypEnv$ and written $\overline{\xname}:\overline{\type}$,
are used to collect type assumptions for program variables (i.e., formal parameters of functions).
Type-scheme environments, ranged over by $\TStypEnv$ and written $\overline{\anyvalue}:\overline{\typescheme}$, are used to collect the type schemes for built-in constructors and built-in operators together with the type schemes inferred for user-defined functions. In particular,
the distinguished  built-in type-scheme environment  $\OStypEnv$ associates a type scheme
to each  built-in constructor $\dc$ and
to each built-in function $\bname$—Figure <ref> shows the type schemes for the built-in constructors and built-in functions
used throughout this paper.

[] $\begin{array}{l}
\textbf{Built-in data constructors}\\
<EMAIL_ADDRESS>\typeof{\truevalue} & = & \btype
\\
\typeof{\falsevalue} & = & \btype
\\
\typeof{n} & = & \ntype, \quad \text{where } n \text{ is a number or } \texttt{PositiveInfinity}
\\
\typeof{\PairK} & = & \forall\tvar_1\tvar_2.(\tvar_1,\tvar_2)\rightarrow \pairltypeOf{\tvar_1}{\tvar_2}
\\
\typeof{\NullK} & = & \forall\tvar. \listltypeOf{\tvar}
\\
\typeof{\ConsK} & = & \forall\tvar. (\tvar,\listltypeOf{\tvar})\to \listltypeOf{\tvar}
\\
\end{array}
\\
\textbf{Built-in functions: pure operators}\\
<EMAIL_ADDRESS>\typeof{\pairK} & = & \forall\tvar_1\tvar_2. \tvar_1 \to \tvar_2 \to \pairltypeOf{\tvar_1}{\tvar_2}
\\
\typeof{\fstK} & = & \forall\tvar_1\tvar_2.(\pairltypeOf{\tvar_1}{\tvar_2}) \to \tvar_1
\\
\typeof{\sndK} & = & \forall\tvar_1\tvar_2.(\pairltypeOf{\tvar_1}{\tvar_2}) \to \tvar_2
\\
\typeof{\consK} & = & \forall\tvar. \tvar\to \listltypeOf{\tvar} \to \listltypeOf{\tvar}
\\
\typeof{\headK} & = & \forall\tvar.(\listltypeOf{\tvar}) \rightarrow \tvar
\\
\typeof{\tailK} & = & \forall\tvar.(\listltypeOf{\tvar}) \rightarrow \listltypeOf{\tvar}
\\
\typeof{\texttt{=}} & = & \forall\tvar.(\tvar,\tvar) \to \btype
\\
\typeof{\texttt{mux}} & = & \forall\tvar.(\btype,\tvar,\tvar)\to\tvar
\\
\typeof{\texttt{+}} & = & (\ntype,\ntype)\to\ntype
\\
\typeof{\texttt{and}} & = & (\btype,\btype)\to\btype
\\
\typeof{\texttt{min}} & = & (\ntype, \ntype) \to \ntype
\\
\typeof{\texttt{<}} & = & (\ntype,\ntype)\to \btype
\\
\end{array}
\\
\textbf{Built-in functions: sensors}\\
<EMAIL_ADDRESS>\typeof{\texttt{temperature}} & = & () \to \ntype
\\
\end{array}
\\
\textbf{Built-in functions: relational sensors}\\
<EMAIL_ADDRESS>\typeof{\texttt{nbrRange}} & = & () \to \ntype
\\
\end{array}
\end{array}
Type schemes for the built-in value constructors and functions used in the examples.

The typing judgement for expressions is of the form “$\expTypJud{\TStypEnv}{\TtypEnv}{\e}{\type}$”, to be read:
“$\e$ has type $\type$ under the type-scheme assumptions $\TStypEnv$ (for built-in constructors and for  built-in and user-defined functions)
and the type assumptions $\TtypEnv$ (for the program variables occurring in $\e$), respectively”.

As a standard syntax in type systems [38], given
$\overline{\type}=\type_1,\ldots,\type_n$ and
$\overline{\e}=\e_1,\ldots,\e_n$ ($n\ge 0$), we write
as short for $\expTypJud{\TStypEnv}{\TtypEnv}{\e_1}{\type_1}$
$\cdots$ $\expTypJud{\TStypEnv}{\TtypEnv}{\e_n}{\type_n}$.

The typing rules for expressions are presented in Figure <ref> (bottom).
The rules for variables ([T-VAR]), data values ([T-DAT]), anonymous function expressions ([T-A-FUN]),
built-in or defined function names ([T-N-FUN]), and function application ([T-APP]),  are almost standard.
Rule [T-REP] (for $\repK$-expressions) ensures that both the initial value $\e_1$  and the domain and range of function $\e_2$
have the same type, and then assigns it to $\repK(\e_1)\{\e_2\}$;
rule [T-NBR] (for $\nbrK$-expressions) assigns to $\nbrK\{\e\}$ the same type as $\e$; and rule
[T-FOLD] (for $\foldK$-expressions) ensures that
$\e_1$ and  $\e_3$ have the same type $\type$ and that $\e_2$ has type $(T, T) \to T$, and then assigns
type $\type$ to $\foldK(\e_1,\e_2,\e_3)$.
The typing rules for declared functions ([T-FUNCTION])
and programs ([T-PROGRAM]) are almost standard.

Consider the following simple implementation of a self-healing gradient [4] (i.e., the field of minimum distances from source devices) that also circumvents obstacles.

Its semantics will be presented later (see <Ref>); now, we merely consider its typing.

def gradient(source, metric)  // : (bool, ()->num) -> num
rep(PositiveInfinity) (distance) =>
mux(source, 0.0,
foldhood(PositiveInfinity, min, nbrdistance + metric())

if (isObstacle)  PositiveInfinity   gradient(isSource)   // : num

The types of the gradient function and of the main expression inferred by the type system are inserted above as comments. By rule [T-APP] and assumptions on built-in , the type system infers that the third argument of the  expression must be $\ntype$, since the second argument is also $\ntype$. It follows that  must be of type $\ntype$ (rule [T-NBR]) as well and  must be of type $() \to \ntype$ (rule [T-APP]), from which function  can be inferred to have type $(\btype, () \to \ntype) \to \ntype$ (rule [T-FUNCTION]). The overall program has then type $\ntype$ (rule [T-PROGRAM]).

§.§ Operational Semantics: Device Semantics

This section presents a formal semantics of device computation as happens in .

Starting from  syntax as previously described, we  assume a fixed program $\PROGRAM$. We say that “device $\deviceId$ fires”, to mean that the main expression of $\PROGRAM$ is evaluated on $\deviceId$.

As  allows recursive functions, termination of a device firing is not decidable. In the rest of the paper we assume

that only terminating programs are considered.

§.§.§ Device semantics: overall picture and preliminary definitions

We model device computation by a big-step operational semantics
where the result of evaluation is a value-tree $\vtree$  (see <Ref>, first frame),
which is an ordered tree of values, tracking the result of any evaluated subexpression. Intuitively, the evaluation of an expression at a given time in a device $\deviceId$ is performed against the recently-received value-trees of neighbours, namely, its outcome depends on those value-trees.

The result is a new value-tree that is conversely made available to $\deviceId$'s neighbours (through a broadcast) for their firing; this includes $\deviceId$ itself, so as to support a form of state across computation rounds (note that an implementation may massively compress the value-trees, storing only enough information for expressions to be aligned).

A value-tree environment $\Trees$ is a map from device identifiers to value-trees, collecting the outcome of the last evaluation on neighbours.
This is written $\envmap{\overline\deviceId}{\overline\vtree}$ as short for $\envmap{\deviceId_1}{\vtree_1},\ldots,\envmap{\deviceId_n}{\vtree_n}$.
The syntax of value-trees and value-tree environments is given in Figure <ref> (first frame).

The graphical representation of the value-trees

\[
\mbox{$\vtree_1=\mkvt{\truevalue}{\mkvt{<}{},\mkvt{-2}{},\mkvt{5}{},\mkvt{\truevalue}{}}$ $\qquad$
and $\qquad$ $\vtree_2=\mkvt{4}{\mkvt{f}{},\mkvt{3}{},\mkvt{4}{\mkvt{+}{},\mkvt{3}{},\mkvt{1}{},\mkvt{4}{}}}$}
\]

is as follows:

[-,node distance=1.5cm and 1.5cm, node/.style=rectangle,draw, node2/.style=draw]

[node] (a1) [] ;
[node] (a2) [below left=0.5cm and 1.5cm of a1] ;
[node] (a3) [below left=0.5cm and 0cm of a1] ;
[node] (a4) [below right=0.5cm and 0cm of a1] ;
[node] (a5) [below right=0.5cm and 1.5cm of a1] ;

[node] (b1) [right=6cm of a1] ;
[node] (b2) [below left=0.5cm and 1.5cm of b1] ;
[node] (b3) [below=0.5cm of b1] ;
[node] (b4) [below right=0.5cm and 1.5cm of b1] ;
[node] (b41) [below left=0.5cm and 1.5cm of b4] ;
[node] (b42) [below left=0.5cm and 0cm of b4] ;
[node] (b43) [below right=0.5cm and 0cm of b4] ;
[node] (b44) [below right=0.5cm and 1.5cm of b4] ;

(a1) edge [] node []  (a2)
(a1) edge [] node []  (a3)
(a1) edge [] node []  (a4)
(a1) edge [] node []  (a5)

(b1) edge [] node []  (b2)
(b1) edge [] node []  (b3)
(b1) edge [] node []  (b4)
(b4) edge [] node []  (b41)
(b4) edge [] node []  (b42)
(b4) edge [] node []  (b43)
(b4) edge [] node []  (b44)

In the following, for sake of readability, we sometimes write the value $\anyvalue$ as shorthand for the value-tree $\mkvt{\anyvalue}{}$. Following this convention, the value-tree $\vtree_1$ is shortened to $\mkvt{\truevalue}{<,-2,5,\truevalue}$,  and the value-tree $\vtree_2$ is shortened to $\mkvt{4}{\texttt{f},3,\mkvt{4}{+,3,1,4}}$.

In order to define the semantics of function calls (which requires checking functions for equality in a decidable way), we assume that prior to execution each anonymous function sub-expression $(\overline\xname) \toSymK{\e}$ of a program $\emain$ is automatically annotated as $(\overline\xname) \toSymKtag{\name}{\e}$ with a tag $\name$ which uniquely identifies the expression.[For example, the tag could be generated as $\name = (\emain, n)$ where $n$ is the index of the occurrence of the $\toSym{}$ keyword in $\emain$.] The tag serves as a name for anonymous functions, and function values are considered equal if they share the same name.

Figure <ref> (second frame) defines: the auxiliary functions $\rho$ and $\pi$ for extracting the root value and a subtree of a value-tree, respectively (further explanations about function $\pi$ will be given later); the extension of functions $\rho$ and $\pi$ to value-tree environments; and the auxiliary functions $\nameOf$, $\argsNAME$ and $\bodyNAME$ for extracting the name, formal parameters and body of a (user-defined or anonymous) function, respectively.

The computation that takes place on a single device is formalised  by the big-step operational semantics rules given in Figure <ref> (fourth frame).
The derived judgements are of the form

\[
\bsopsem{\deviceId,\deviceId'}{\Trees}{\senstate}{\e}{\vtree}
\]

to be read “expression $\e$ evaluates to  value-tree $\vtree$ on device $\deviceId$ with respect to the neighbour $\deviceId'$, value-tree environment $\Trees$ and sensor state $\senstate$”, where:
(i) $\deviceId$ is the identifier of the current device and $\deviceId'$ is either equal to $\deviceId$ or is one of its neighbours;
(ii) $\Trees$ is the field of the value-trees produced by the most recent evaluation of (an expression corresponding to) $\e$ on $\deviceId$ and its neighbours;
(iii) $\e$ is an expression;
(iv) the value-tree $\vtree$  represents the values computed for all the expressions encountered during the evaluation of $\e$—in particular $\vrootOf{\vtree}$ is the result value of $\e$.

The operational semantics  rules  are based on rather standard rules for functional languages,
extended so as to be able to evaluate a subexpression $\e'$ of $\e$ with respect to the value-tree environment $\Trees'$ obtained from $\Trees$
by extracting the corresponding subtree (when present) in the value-trees in the range of $\Trees$. This process, called alignment,
is modelled by the auxiliary function $\pi$, defined in Figure <ref> (second frame).
Function $\pi$ has two different behaviours (specified by its subscript or superscript): $\piIof{i}{\vtree}$ extracts the $i$-th subtree of $\vtree$, if it is present;
and $\piBof{\funvalue}{\vtree}$ extracts the last subtree of $\vtree$, if it is present and the root of first subtree of $\vtree$ is equal to $\funvalue$.

When a device $\deviceId$ fires, its main expression $\e$ is evaluated with respect to $\deviceId$ itself. That is, by means of a judgement where

\[
\bsopsem{\deviceId,\deviceId}{\Trees}{\senstate}{\e}{\vtree}.
\]

A key aspect of the semantics is that, if $\e$ is a $\foldK$-expression $\foldK(\e_1,\e_2,\e_3)$ then its body $\e_3$ is evaluated with respect to each of the devices $\deviceId'$  (if any)  in $\domof{\Trees}\setminus\{\deviceId\}$.
Because of alignment (see above), it might happen that a sub-expression $\e'$ of $\e_3$ is evaluated by a judgement

\[
\bsopsem{\deviceId,\deviceId'}{\Trees}{\senstate}{\e'}{\vtree}  \quad \mbox{ where $\deviceId\neq\deviceId'\not\in\domof{\Trees}$ }
\]

and, if the evaluation of $\e'$ exploits the device $\deviceId'$, then the evaluation of $\e_3$ with respect to $\deviceId'$ fails and
the evaluation of the $\foldK$-expression $\foldK(\e_1,\e_2,\e_3)$ does not consider the neighbour $\deviceId'$. The
evaluation rule for $\foldK$-expressions, [E-FOLD],  formalises failure of evaluation with respect to a neighbour $\deviceId'$
by means of the auxiliary predicate

\[
\bsopsemFAIL{\deviceId,\deviceId'}{\Trees}{\senstate}{\e}
\]

to be read “expression $\e$ fails to evaluate on device $\deviceId$  against neighbour $\deviceId'$ with respect to value-tree environment $\Trees$ and
sensor state $\senstate$”, which is formalised by the big-step operational semantics rules given in Figure <ref>.

[1]
\textbf{Value-trees
and value-tree environments:}\\
<EMAIL_ADDRESS>\vtree & \BNFcce &  \mkvtree{E-Rule}{\anyvalue}{\overline{\vtree}}
&   {\footnotesize \mbox{value-tree}} \\
\Trees & \BNFcce & \envmap{\overline{\deviceId}}{\overline{\vtree}}
&   {\footnotesize \mbox{value-tree environment}} \\
\end{array}\\
\hline\\[-8pt]
\textbf{Auxiliary functions:}\\
\begin{array}{l}
\begin{array}{l@{\hspace{8pt}}l@{\hspace{8pt}}l}
\nameOf((\overline{\xname}) \; \toSymKtag{\name}{\e}) = \name
\args{ (\overline{\xname}) \; \toSymKtag{\name}{\e}} = \overline{\xname}
\body{(\overline{\xname}) \; \toSymKtag{\name}{\e}} = \e
\\
\nameOf(\fname) = \fname
\args{\fname} = \overline{\xname}
\body{\fname} = \e  \; (\text{if } \, \defK \; \fname (\overline{\xname}) \; \eqSymK{\e})
\\
\nameOf(\bname) = \bname
\vrootOf{\mkvtree{}{\anyvalue}{\overline{\vtree}}}  =   \anyvalue
\\
\piIof{i}{\mkvtree{E-Rule}{\anyvalue}{\vtree_1,\ldots,\vtree_n}}  =  \vtree_i
\text{if~} 1\le i \le n
\text{~else~} \emptyseq
\\
\piBof{\funvalue}{\mkvtree{E-Rule}{\anyvalue}{\vtree_1,\ldots,\vtree_{n+2}}}  =   \vtree_{n+2}
\text{if~} \nameOf(\vrootOf{\vtree_{1}}) = \nameOf(\funvalue)
\text{~else~} \emptyseq
\end{array} \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!
\\[30pt]
\mbox{For } \auxNAME\in\rho,\piI{i},\piB{\funvalue}:
\quad
\left\{{\begin{array}{lcll}
\aux{\emptyseq}  & =  & \emptyseq
\\
\aux{\envmap{\deviceId}{\vtree}, \Trees}  & =   & \aux{\Trees}  & \quad \mbox{if} \; \aux{\vtree}=\emptyseq
\\
\aux{\envmap{\deviceId}{\vtree}, \Trees}  & =  & \envmap{\deviceId}{\aux{\vtree}}, \aux{\Trees} & \quad \mbox{if} \; \aux{\vtree} \not=\emptyseq
\end{array}}\right.   \!\!\!\!\!\!
\end{array}\\
\hline\\[-10pt]
\textbf{Syntactic shorthands:}\\
\!\!\begin{array}{l@{\hspace{4pt}}l@{\hspace{4pt}}l}
\bsopsem{\deviceId,\deviceId'}{\piIofOv{\Trees}}{\senstate}{\overline{\e}}{\overline{\vtree}}
\textrm{where~~} |\overline{\e}|=n
\textrm{for~~}
\bsopsem{\deviceId,\deviceId'}{\piIof{1}{\Trees}}{\senstate}{\e_1}{\vtree_1}
\ldots
\bsopsem{\deviceId,\deviceId'}{\piIof{n}{\Trees}}{\senstate}{\e_n}{\vtree_n} \!\!\!\!\!\!\!\!\!\!\!\! \\
\vrootOf{\overline{\vtree}}
\textrm{where~~} |\overline{\vtree}|=n
& \textrm{for~~}
\vrootOf{\vtree_1} ~ \ldots ~ \vrootOf{\vtree_n}\\
\substitution{\overline{\xname}}{\vrootOf{\overline{\vtree}}}
&   \textrm{where~~} |\overline{\xname}|=n
\textrm{for~~}
\substitution{\xname_1}{\vrootOf{\vtree_1}}~\ldots~\substitution{\xname_n}{\vrootOf{\vtree_n}}
\end{array}\\
\hline\\[-10pt]
\textbf{Rules for expression evaluation:} \hspace{55mm}
\boxed{\bsopsem{\deviceId,\deviceId'}{\Trees}{\senstate}{\e}{\vtree}}
\skiptransitionR
\!\!\!\!\!\begin{array}{c}
\nullsurfaceTyping{E-VAL}{
\bsopsem{\deviceId,\deviceId'}{\Trees}{\senstate}{\anyvalue}{\mkvtree{}{\anyvalue}{}}
\skiptransitionN\\
\surfaceTyping{E-B-APP}{
\begin{array}{ll}
\bsopsem{\deviceId,\deviceId}{\piIof{1}{\Trees}}{\senstate}{\e}{\vtree}
\bsopsem{\deviceId,\deviceId'}{\piIof{i+1}{\Trees}}{\senstate}{\e_i}{\vtree_i}  \quad \text{for all}\; i \in 1, \ldots, n
\\
\anyvalue=\builtinop{\bname}{\deviceId,\deviceId'}{\piBof{\bname}{\Trees},\senstate}(\vrootOf{\overline{\vtree}})
(\bname = \vrootOf{\vtree} \text{ is not relational }) \vee (\deviceId' \in \domof{\piBof{\bname}{\Trees}} \cup \{\deviceId\})
\end{array} \!\!\!\!
\bsopsem{\deviceId,\deviceId'}{\Trees}{\senstate}{\e(\overline{\e})}{\mkvtree{}{\anyvalue}{\vtree,\overline{\vtree},\anyvalue}}
\skiptransitionN\\
\surfaceTyping{E-D-APP}{
\begin{array}{ll}
\bsopsem{\deviceId,\deviceId}{\piIof{1}{\Trees}}{\senstate}{\e}{\vtree}
\bsopsem{\deviceId,\deviceId'}{\piIof{i+1}{\Trees}}{\senstate}{\e_i}{\vtree_i} \quad \text{for all}\; i \in 1, \ldots, n

\\
\funvalue = \vrootOf{\vtree} \mbox{ is not a built-in}
\bsopsem{\deviceId,\deviceId'}{\piBof{\funvalue}{\Trees}}{\senstate}{\applySubstitution{\body{\funvalue}}{\substitution{\args{\funvalue}}{\vrootOf{\overline{\vtree}}}}}{\vtree'}
\end{array} \!\!\!\!
\bsopsem{\deviceId,\deviceId'}{\Trees}{\senstate}{\e(\overline{\e})}{\mkvtree{}{\vrootOf{\vtree'}}{\vtree,\overline{\vtree},\vtree'}}
\skiptransitionN\\
\surfaceTyping{E-REP}{
\begin{array}{ll}
\bsopsem{\deviceId,\deviceId}{\piIof{1}{\Trees}}{\senstate}{\e_1}{\vtree_1} & \anyvalue_1=\vrootOf{\vtree_{1}}\\
\bsopsem{\deviceId,\deviceId}{\piIof{2}{\Trees}}{\senstate}{\e_2(\anyvalue_0)}{\vtree_2}~~& \anyvalue_2=\vrootOf{\vtree_{2}}
\end{array}
\quad
\anyvalue_0 = \left\{\begin{array}{ll}
\vrootOf{\piIof{2}{\Trees}}(\deviceId) & \mbox{if} \;  \deviceId \in \domof{\Trees} \\
\anyvalue_1 & \mbox{otherwise}
\end{array}\right.
\bsopsem{\deviceId,\deviceId'}{\Trees}{\senstate}{\repK(\e_1)\{\e_2\}}{\mkvtree{}{\anyvalue_2}{\vtree_1,\vtree_2}}
\skiptransitionN\\
\surfaceTyping{E-NBR}{
\quad
\deviceId \neq \deviceId' \in \domof{\Trees}
\qquad
\vtree = \Trees(\deviceId')
\bsopsem{\deviceId,\deviceId'}{\Trees}{\senstate}{\nbrK\{\e\}}{\vtree}
\qquad
\surfaceTyping{E-NBR-LOC}{
\quad
\bsopsem{\deviceId,\deviceId}{\piIof{1}{\Trees}}{\senstate}{\e}{\vtree}
\bsopsem{\deviceId,\deviceId}{\Trees}{\senstate}{\nbrK\{\e\}}{\mkvtree{}{\vrootOf{\vtree}}{\vtree}}
\skiptransitionN\\
\surfaceTyping{E-FOLD}{
\begin{array}{ll}
\bsopsem{\deviceId,\deviceId}{\piIof{1}{\Trees}}{\senstate}{\e_1}{\vtree^1}
\quad
\bsopsem{\deviceId,\deviceId}{\piIof{2}{\Trees}}{\senstate}{\e_2}{\vtree_f}
\qquad
\funvalue = \vrootOf{\vtree_f}
\\
\deviceId_1, \ldots, \deviceId_n = \domof{\Trees} \setminus \{\deviceId\}
\quad
n\ge m\ge 0, \deviceId_1, \ldots, \deviceId_m \text{ increasing}, \deviceId_0 = \deviceId
\\
\bsopsem{\deviceId,\deviceId_i}{\piIof{3}{\Trees}}{\senstate}{\e_3}{\vtree_i}
\quad
\text{for all } i \in 0,...,m
\\
\bsopsemFAIL{\deviceId,\deviceId_j}{\piIof{3}{\Trees}}{\senstate}{\e_3}{}
\quad
\text{for all } j \in m+1,...,n
\\
\bsopsem{\deviceId,\deviceId}{\emptyset}{\senstate}{\funvalue(\vrootOf{\vtree^i}, \vrootOf{\vtree_i})}{\vtree^{i+1}}
\quad
\text{for all } i \in 1,...,m
\end{array}
\bsopsem{\deviceId,\deviceId'}{\Trees}{\senstate}{\foldK(\e_1,\e_2,\e_3)}{\mkvtree{}{\vrootOf{\vtree^{m+1}}}{\vtree^1, \vtree_f, \vtree_0}}
\end{array}\!\!\!\!\!
\end{array}$

Big-step operational semantics for expression evaluation (see also <Ref>).

[1]
~\textbf{Auxiliary rules for expression evaluation failure:} \hspace{23mm}
\boxed{\bsopsemFAIL{\deviceId,\deviceId'}{\Trees}{\senstate}{\e}}
\skiptransition
\begin{array}{c}
\surfaceTyping{E-NBR-FAIL}{
~~ \quad
\deviceId \neq \deviceId' \not\in \domof{\Trees}
\bsopsemFAIL{\deviceId,\deviceId'}{\Trees}{\senstate}{\nbrK\{\e\}}
\skiptransitionN
\\
\surfaceTyping{E-R-APP-FAIL}{
\begin{array}{ll}
\bsopsem{\deviceId,\deviceId}{\piIof{1}{\Trees}}{\senstate}{\e}{\vtree}
\bsopsem{\deviceId,\deviceId'}{\piIof{i+1}{\Trees}}{\senstate}{\e_i}{\vtree_i} ~~ \text{for all}\; i \in 1, \ldots, n
\\
\snvalue = \vrootOf{\vtree} \mbox{ is relational-built-in}
\deviceId \neq \deviceId' \not\in \domof{\piBof{\snvalue}{\Trees}}
\end{array}\!\!\!\!
\bsopsemFAIL{\deviceId,\deviceId'}{\Trees}{\senstate}{\e(\overline\e)}
\skiptransitionN
\\
%	~~ \quad
%	\bsopsemFAIL{\deviceId,\deviceId}{\piIof{n+1}{\Trees}}{\senstate}{\e}
% }{
%	\bsopsemFAIL{\deviceId,\deviceId'}{\Trees}{\senstate}{\e(\overline\e)}
\surfaceTyping{E-APP-ARG-FAIL}{
\begin{array}{ll}
\bsopsem{\deviceId,\deviceId}{\piIof{1}{\Trees}}{\senstate}{\e}{\vtree}
\quad
\overline{\e} = \e_1,...,\e_n
\qquad
n\ge 0
\\
\bsopsem{\deviceId,\deviceId'}{\piIof{i+1}{\Trees}}{\senstate}{\e_i}{\vtree_i}
\quad
\text{for all } i \in 1,...,m < n
\\
\bsopsemFAIL{\deviceId,\deviceId'}{\piIof{m+2}{\Trees}}{\senstate}{\e_{m+1}}
\end{array}
\bsopsemFAIL{\deviceId,\deviceId'}{\Trees}{\senstate}{\e(\overline{\e})}
\skiptransitionN
\\
\surfaceTyping{E-D-APP-FAIL}{
\begin{array}{ll}
\bsopsem{\deviceId,\deviceId}{\piIof{1}{\Trees}}{\senstate}{\e}{\vtree}
\quad
\bsopsem{\deviceId,\deviceId'}{\piIof{i+1}{\Trees}}{\senstate}{\e_i}{\vtree_i} ~~ \text{for all}\; i \in 1, \ldots, n
\\
\funvalue = \vrootOf{\vtree} \mbox{ is not a built-in}
\quad
\bsopsemFAIL{\deviceId,\deviceId'}{\piBof{\funvalue}{\Trees}}{\senstate}{\applySubstitution{\body{\funvalue}}{\substitution{\args{\funvalue}}{\vrootOf{\overline{\vtree}}}}} %\!\!\!\!\!\!\!\!\!
\end{array}\!\!\!\!
\bsopsemFAIL{\deviceId,\deviceId'}{\Trees}{\senstate}{\e(\overline{\e})}
\end{array}
\end{array}$

Big-step operational semantics for expression evaluation (auxiliary rules for expression evaluation failure).

§.§.§ Device semantics: rules for expression evaluation

We start by explaining the rules in <Ref> (fourth frame), then we will
explain the rules in <Ref>.

Rule [E-VAL] implements the evaluation of an expression that is already a value.
For instance, evaluating the expression $\mathtt{1}$ produces (by Rule  [E-VAL]) the value-tree $\mkvtree{}{1}{}$,
while evaluating the expression $\mathtt{+}$ produces the value-tree $\mkvtree{}{+}{}$.

Rules [E-B-APP] and [E-D-APP] model function application $\e(\e_1 \cdots \e_n)$.
In case $\e$ evaluates to a built-in function $\bname$, rule [E-B-APP] is used, whose behaviour is driven by the special auxiliary
function $\builtinop{\bname}{\deviceId,\deviceId'}{\Trees, \senstate}$ (operational interpretation of $\bname$), whose actual definition is abstracted away.

[Built-in function application]
Evaluating the expression $\mathtt{<(-2, 5)}$ produces the value-tree $\vtree_1=\mkvt{\truevalue}{<,-2,5,\truevalue}$ introduced in Example <ref>.

The operational interpretation $\builtinop{<}{\deviceId,\deviceId'}{\Trees, \senstate}$ of $<$ is the following (notice that this interpretation does not depend on $\Trees, \senstate, \deviceId, \deviceId'$, since $<$ is a pure mathematical operator):

\[
\builtinop{<}{\deviceId,\deviceId'}{\Trees, \senstate} = \denotf{x}{} \denotf{y}{} \begin{cases}
\truevalue & x < y \\
\falsevalue & \text{otherwise}
\end{cases}
\]

The value of the whole expression, $\truevalue$ (the root of the last subtree of the value-tree), has been computed by using rule [E-B-APP] to evaluate the application $\builtinop{<}{\deviceId,\deviceId'}{\Trees, \senstate}(-2,5)$ of the less-then operator $<$ (the root of the first subtree of the value-tree) to the values $-2$  (the root of the second subtree of the value-tree) and $5$ (the root of the third subtree of the value-tree).

In case $\e$ evaluates to a user-defined or anonymous function $\funvalue$, rule [E-D-APP] is used:
it performs
domain restriction $\piBof{\funvalue}{\Trees}$ (thus discarding devices that did not apply the same function $\funvalue$, for which no consistent information on the application of $\funvalue$ is present),
then continues the evaluation by substituting the arguments into the body of $\funvalue$.

We remark that we do not assume that $\Trees$ is empty whenever it does not contain $\deviceId$.
In fact, in any round where $\e$ evaluates to a function $\funvalue$ for the first time on a device, $\funvalue(\overline\e)$
will be evaluated with respect to an environment not containing $\deviceId$ but possibly containing other devices (whose $\e$ evaluated to
$\funvalue$ in their previous round of computation).

[Defined or anonymous function application]
Evaluating the expression $\funvalue(3)$, where $\funvalue$ is the name of the declared function $\defK \; \funvalue(\xname) \; \eqSymK{\xname + 1}$, produces the value-tree $\vtree_2=\mkvt{4}{\texttt{f},3,\mkvt{4}{+,3,1,4}}$ introduced in Example <ref>.
The value of the whole expression, $4$ (the root of  $\vtree_2$), which has been computed by using rule [E-D-APP], is the root of the last subtree of $\vtree_2$, which is produced by the evaluation of the expression $3+1$ (obtained from the body of $\funvalue$ by replacing $\xname$ with $3$).

Evaluating the similar expression $\funvalue(3)$ where $\funvalue$ is the anonymous function $((\xname)\; \toSymKtag{\name}{\xname + 1})$, produces the same value-tree $\vtree_2$ by the same rule [E-D-APP].

Rule [E-REP] implements internal state evolution through computational rounds: on the first firing of a device, $\repK(\e_1)\{\e_2\}$ evaluates to $\e_2(\e_1)$, then it evaluates to $\e_2(\anyvalue)$ where $\anyvalue$ is the value calculated in the previous round.

[Time evolution]
To illustrate rule [E-REP], as well as computational rounds, we consider the program $\repK(3)\{\funvalue\}$
where $\funvalue$ is the anonymous function $(\xname)\; \toSymKtag{\name}{\xname + 1}$ introduced in Example <ref>.
The first firing of a device $\deviceId$  is performed against the empty tree environment. Therefore, according to rule  [E-REP],
evaluating  $\repK(3)\{\funvalue\}$ produces the value-tree $\vtree=\mkvt{4}{3, \vtree_2}$ where $\vtree_2=\mkvt{4}{\texttt{f},3,\mkvt{4}{+,3,1,4}}$
is the value-tree (introduced in Example <ref>) produced by evaluating the expression $\funvalue(3)$
as described in Example <ref>. The overall result of the firing is the root $4$ of $\vtree$.
Any subsequent firing of the device $\deviceId$ is performed with respect to a value-tree environment $\Trees$ that associates to $\deviceId$
the outcome $\vtree$ of the most recent firing of $\deviceId$.
Therefore, evaluating    $\repK(3)\{\funvalue\}$ at the second firing produces the value-tree $\vtree'=\mkvt{5}{4, \vtree'_2}$ where
is the value-tree  produced by evaluating the expression $\funvalue(4)$, where $4$ is the root of $\vtree$.
Hence, the results of the firings are $4$, $5$, $6$, and so on.

Rules [E-NBR] and [E-NBR-LOC] model device interaction (together with [E-FOLD] which we shall consider later).  When an $\nbrK$-expression is not evaluated against a neighbour (that is, $\deviceId' = \deviceId$), by Rule [E-NBR-LOC] the $\nbrK$ operator is discarded and the evaluation continues. Whenever instead an $\nbrK$-expression is evaluated against a neighbour (that is, $\deviceId' \neq \deviceId$), by Rule [E-NBR] the expression directly evaluates to $\Trees(\deviceId')$ (which is the value-tree calculated by device $\deviceId'$ in its last computational round). Notice that it could be possible that $\deviceId'$ is not in the domain of $\Trees$ due to alignment operations performed in subexpressions of the enclosing instance of $\foldK$. In this case, no rule is applicable and the $\nbrK$-expression fails, causing $\deviceId'$ to be ignored by the enclosing $\foldK$ operator (see Rule [E-FOLD]).

Rule [E-FOLD] implements collection and aggregation of results from neighbours, proceeding in the following steps:

* Evaluate the initial value $\e_1$ with respect to the current device obtaining the value-tree $\vtree^1$.

* Evaluate the aggregator $\e_2$ with respect to  the current device obtaining $\vtree_f$ with root $\funvalue$.

* Evaluate the body $\e_3$ with respect to the current device $\deviceId_0 = \deviceId$, obtaining $\vtree_0$ which constitutes the third branch of the overall resulting value-tree, then with respect to every neighbour $\deviceId' \in \domof{\piIof{3}{\Trees}}\setminus\{\deviceId\}$ and consider only the $m \ge 0$ neighbours  $\deviceId_1,...,\deviceId_m$ for which the evaluation does not fail, obtaining the value-trees $\vtree_1,...,\vtree_m$, respectively.[If the aggregator $\funvalue$ is associative and commutative, then the result of the aggregation does not depend on the order in which the neighbours $\deviceId' \in \domof{\piIof{3}{\Trees}}\setminus\{\deviceId\}$ are considered. To ensure determinism even in the case when the aggregator $\funvalue$ is not associative and commutative, we assume that the neighbours are considered according to a given total order on device identifiers.]

* Aggregate the values $\vrootOf{\vtree_i}$ ($1\le i\le m$) computed above together with the initial value $\vrootOf{\vtree^1}$ via function $\funvalue$, obtaining the final outcome $\vrootOf{\vtree^{m+1}}$. Notice that when $m=0$, the final outcome is the result $\vrootOf{\vtree^1}$ of $\e_1$. The aggregation is performed with respect to the current device and the empty environment, since the value-trees of the aggregation process cannot be meaningfully related with one another (and thus are not stored in the final outcome of the computation). In other words, the aggregator $\funvalue$ is forced to be a “pure” function independent of the current device and environment (even though the expression $\e_2$  as a whole might depend on the environment).

The values aggregated by $\foldK$ exclude the value of $\e_3$ in the current device $\deviceId$. However, an inclusive folding operation $\mathtt{foldhoodPlusSelf}$ can  be encoded as

[language=hfc]|def foldhoodPlusSelf(f, v)  foldhood(v, f, v) |.

We also remark that a sequence of nested $\foldK$-operators (not interleaved by $\nbrK$-operators) can lead to an evaluation time which is exponential in the evaluation tree depth.[In actual implementations, the outcome of $\foldK$ and $\repK$ subexpressions can be “memoised” in order to prevent subsequent re-evaluation (since such expressions are independent of the neighbour against which are evaluated). This addresses the performance issues of nested $\foldK$-operators.]

Failure of evaluation against a neighbour is formalised by means of the auxiliary judgement $\bsopsemFAIL{\deviceId,\deviceId'}{\Trees}{\senstate}{\e}$ defined by the rules in  Figure <ref>. Rules [E-NBR-FAIL] and [E-R-APP-FAIL] model the failure sources, while the other rules model failure propagation.

[Neighbourhood interaction]
To illustrate rules [E-FOLD], [E-NBR] and [E-NBR-LOC],  we consider program

\[
\foldK(2,\texttt{+}, \texttt{min}(\nbrK\{\texttt{temperature}()\}, \texttt{temperature}()) )
\]

evaluated in device $\deviceId_0$ (in which $\texttt{temperature}() = 10$) with neighbours $\deviceId_1$ (in which $\texttt{temperature}() = 15$)
and $\deviceId_2$ (in which $\texttt{temperature}() = 5$). By Rule [E-FOLD], the three subexpressions of the $\foldK$-expression
are evaluated with respect to $\deviceId_0$ into the value-trees $\vtree^1, \vtree_f, \vtree_0$ which will constitute the branches of the final tree. The first two of them are
$\vtree^1 = \mkvt{2}{}$ and $\vtree_f = \mkvt{\texttt{+}}{}$, each obtained by Rule [E-VAL].
Then, the third subexpression is evaluated against $\deviceId_0$, $\deviceId_1$  and $\deviceId_2$, obtaining:

\begin{align*}
\vtree_0 &= \mkvt{10}{\texttt{min}, \mkvt{10}{\mkvt{10}{\mathtt{temperature},10}}, \mkvt{10}{\mathtt{temperature},10}, 10}, \\
\vtree_1 &= \mkvt{10}{\texttt{min}, \mkvt{15}{\mkvt{15}{\mathtt{temperature},15}}, \mkvt{10}{\mathtt{temperature},10}, 10},  \\
\vtree_2 &= \mkvt{5}{\texttt{min}, \mkvt{5}{\mkvt{5}{\mathtt{temperature},5}}, \mkvt{10}{\mathtt{temperature},10}, 5}
\end{align*}

the first one ($\vtree_0$) obtained through three applications of Rule [E-B-APP] and one of Rule [E-NBR-LOC], and the other two ($\vtree_1 $ and $\vtree_2$) obtained through three applications of Rule [E-B-APP] and one of Rule [E-NBR].
The roots of value-trees $\vtree_1$ and $\vtree_2$ are then combined through operator $\texttt{+}$, together with the initial value $2$, for a total result of $2 + 10+ 5 = 17$  which is the root of the final value-tree $\mkvt{17}{2, \texttt{+}, \vtree_0}$.

Rules [E-VAL], [E-REP], [E-FOLD] are independent of the neighbour $\deviceId'$
against which the expression is computed (since $\deviceId'$ does not occur in the premises of those rules). Rules [E-B-APP]
and [E-D-APP] simply pass $\deviceId'$ through, allowing subexpressions to make use of it
(including evaluation of built-in relational sensors $\snvalue$). The neighbour device $\deviceId'$ is then non-trivially
exploited only in rules [E-NBR], [E-NBR-LOC], [E-NBR-FAIL] and [E-R-APP-FAIL].

We say that a neighbour is considered by the evaluation of a  $\foldK$-expression to mean that it contributes to the result of the expression. Because of the interplay between neighbourhood interaction and  branching (i.e., function call)  only a subset of the neighbourhood of a device might be considered by a $\foldK$-expression.

[Combining time evolution with neighbourhood interaction: the gradient]

Consider the gradient function from Example <ref>.
def gradient(source, metric)  // : (bool, ()->num) -> num
rep(PositiveInfinity) (distance) =>
mux(source, 0.0,
foldhood(PositiveInfinity, min, nbrdistance + metric())

The  function computes the field of minimum distances (according to ) from devices where  is $\truevalue$.
It uses $\repK$ to keep track of the local gradient value, which is computed by looking at the corresponding value in the neighbourhood.
If  is locally $\truevalue$, then the value is merely , since it means that the device is a source;
otherwise, the gradient value is obtained by folding over neighbours (via ) to collect the minimum value of .
The repeated application of such a function, together with actual communication (formally covered in <Ref>) consisting of the  evaluations of neighbours, makes the output field eventually converge to the correct value (minimum distances from sources).

The gradient is a fundamental building block
for collective adaptive behaviour.
It is amenable to various implementations [4]
and plays a crucial role in higher-level patterns [24], as also shown in the case study of <Ref>.

[Neighbourhood interaction and branching]
In order to illustrate the alignment process, guiding neighbour interaction through branching statements, consider the expression for a gradient avoiding obstacles, introduced in Example <ref>.
if (isObstacle)  PositiveInfinity   gradient(isSource)   // : num

Expanding the syntactic sugar, the $\ifK$ statement corresponds to the execution of a different anonymous function depending on the value of :
mux( isObstacle, () => PositiveInfinity, () => gradient(isSource) )()

Assume that device $\deviceId_0$ evaluates this program with respect to $\Trees = \{\envmap{\deviceId_0}{\vtree_0}, \envmap{\deviceId_1}{\vtree_1}, \envmap{\deviceId_2}{\vtree_2}\}$, where  is true in $\deviceId_2$ and false on the other devices.
Thus, the execution of the $\texttt{mux}$ statement produces $\funvalue_\bot = ()\, \toSymKtag{}{\texttt{gradient}(\texttt{isSource})}$ on $\deviceId_0$ and $\deviceId_1$, while it produces
$\funvalue_\top= ()\, \toSymKtag{}{\texttt{PositiveInfinity}}$ on $\deviceId_2$.

The evaluation of the main expression is performed through rule [E-D-APP]. First, the function to be applied is computed as the result of the  expression. Then, the body $\texttt{gradient}(\texttt{isSource})$ is computed with respect to the environment $\piBof{\funvalue_\bot}{\Trees} = \{\envmap{\deviceId_0}{\piIof{2}{\vtree_0}}, \envmap{\deviceId_1}{\piIof{2}{\vtree_1}}\}$: the value-tree of device $\deviceId_2$ is removed since it corresponded to the evaluation of $\funvalue_\top$. The evaluation of $\texttt{gradient}(\texttt{isSource})$ will then require the evaluation of the  expression, in which only devices $\deviceId_0$ and $\deviceId_1$ will be considered (since $\deviceId_2$ has already been discarded).

§.§ Operational Semantics: Network Semantics

[1]
%%%  SYNTAX
\textbf{System configurations and action labels:}\\[5pt]
\begin{array}{lcl@{\hspace{44mm}}r}
\Field & \BNFcce &  \envmap{\overline\deviceId}{\overline\Trees}    &   {\footnotesize \mbox{value-tree field}} \\
\Activation & \BNFcce &  \envmap{\overline\deviceId}{\overline a} \text{ with } a \in \{\actOFF,\actON\}   &   \footnotesize \mbox{activation predicate} \\
\Stat & \BNFcce &  \EnviS{\Field}{\Activation}    &   \footnotesize \mbox{status} \\
\Topo & \BNFcce &  \ap{\overline\deviceId, \overline\deviceId'}    &   {\footnotesize \mbox{topology}} \\
\Sens & \BNFcce &  \envmap{\overline\deviceId}{\overline\senstate}    &   {\footnotesize \mbox{sensor state}} \\
\Envi & \BNFcce &  \EnviS{\Topo}{\Sens}    &   {\footnotesize \mbox{environment}} \\
\Cfg & \BNFcce &  \SystS{\Envi}{\Stat}    &   {\footnotesize \mbox{network configuration}} \\
\act & \BNFcce &  \deviceId+ \;\BNFmid\; \deviceId- \;\BNFmid\; \envact    &   {\footnotesize \mbox{action label}} \\
\end{array}\\
\hline\\[-8pt]
\textbf{Environment well-formedness:}\\[5pt]
\begin{array}{l}
\wfn{\EnviS{\Topo}{\Sens}} \textrm{~~holds iff~~} \bp{\ap{\deviceId,\deviceId} \mid \deviceId \in \deviceIdSet} \subseteq \, \Topo \, \subseteq \deviceIdSet \times \deviceIdSet \text{~~where~~} \deviceIdSet = \domof{\Sens}
\end{array}\\
\hline\\[-8pt]
%%%  REDUCTION RULES
\textbf{Transition rules for network evolution:} \hspace{5.5cm}
\boxed{\nettran{\Cfg}{\act}{\Cfg}}
\\[5pt]
\begin{array}{c}
\netopsemRule{N-COMP}{
\;\; \Activation(\deviceId)\!=\!\actOFF
\quad \Trees' = \filter_\deviceId(\Field(\deviceId))
\quad \bsopsem{\deviceId,\deviceId}{\Trees'}{\Sens(\deviceId)}{\emain}{\vtree}
\quad \Trees\!=\!\mapupdate{\Trees'}{\envmap{\deviceId}{\vtree}}
\nettran{\SystS{\EnviS{\Topo}{\Sens}}{\EnviS{\Field}{\Activation}}}{\deviceId+}{\SystS{\EnviS{\Topo}{\Sens}}{\EnviS{\mapupdate{\Field}{\envmap{\deviceId}{\Trees}}}{\mapupdate{\Activation}{\envmap{\deviceId}{\actON}}}}}
\\[15pt]
\netopsemRule{N-SEND}{
\quad \Activation(\deviceId)\!=\!\actON
\quad \overline\deviceId  = \bp{\deviceId' ~\mid~ \deviceId \Topo \deviceId'}
\quad \vtree = \Field(\deviceId)(\deviceId)
\quad \Trees = \envmap{\deviceId}{\vtree}
\nettran{\SystS{\EnviS{\Topo}{\Sens}}{\EnviS{\Field}{\Activation}}}{\deviceId-}{\SystS{\EnviS{\Topo}{\Sens}}{\EnviS{\globalupdate{\Field}{\envmap{\overline\deviceId}{\Trees}}}{\mapupdate{\Activation}{\envmap{\deviceId}{\actOFF}}}}}
\\[15pt]
\netopsemRule{N-ENV}{
\quad \wfn{\Envi'}
\quad
\Envi'=\EnviS{\Topo}{\envmap{\overline\deviceId}{\overline\senstate}}
\quad
\Field_0=\envmap{\overline\deviceId}{\emptyset}
\quad
\Activation_0=\envmap{\overline\deviceId}{\actOFF}
\nettran{\SystS{\Envi}{\Field,\Activation}}{\envact}{\SystS{\Envi'}{\mapupdate{\Field_0}{\Field}, \mapupdate{\Activation_0}{\Activation}}}
\end{array}\\
\end{array}$
Small-step operational semantics for 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. The semantics is given as a nondeterministic, small-step transition system on network configurations $\Cfg$. This semantics has already been given for  in [1], with the only difference of referring to the  device semantics instead of the  device semantics. Figure <ref> (top) defines key syntactic elements to this end:

* $\Field$ is a computational field (called value-tree field) that models the overall state of the computation as a map from device identifiers to the value-tree environments that are locally stored in the corresponding devices.

* $\Activation$ is an activation predicate specifying whether each device is currently activated (i.e., is performing a computation round).

* $\Stat$ (a pair of value-tree field and activation predicate) models the overall computation status.

* $\Topo$ models network topology as a directed neighbouring graph, i.e. a reflexive neighbouring relation $\Topo \subseteq \deviceIdSet \times \deviceIdSet$ so that $\deviceId \Topo \deviceId$ for each $\deviceId \in \deviceIdSet$.

* $\Sens$ models (distributed) sensor state, as a map from device identifiers to (local) sensors representations (i.e., sensor name/value maps denoted as $\senstate$).

* $\Envi$ (a pair of topology and sensor state) models the network environment.

* $\Cfg$ (a pair of status and environment) models a whole network configuration.

We use the following notation for maps. Let $\envmap{\overline x}{y}$ denote a map sending each element in the sequence $\overline x$ to the same element $y$. Let $\mapupdate{m_0}{m_1}$ denote the map with domain $\domof{m_0} \cup \domof{m_1}$ coinciding with $m_1$ in the domain of $m_1$ and with $m_0$ otherwise. Let $\globalupdate{m_0}{m_1}$ (where $m_i$ are maps to maps) denote the map with the same domain as $m_0$ made of $\envmap{x}{\mapupdate{m_0(x)}{m_1(x)}}$ for all $x$ in the domain of $m_1$, $\envmap{x}{m_0(x)}$ otherwise.

The notation $\filter_\deviceId(\cdot)$ used in rule [N-FIR], Figure <ref> (bottom), models a filtering operation that clears out old stored value-trees from $\Field(\deviceId)$, implicitly based on space/time tags.[For example, the filter may remove value-trees that were stored before $t - \Delta t$, where $t$ is the time of the current firing and $\Delta t$ is a decay parameter of the filter.] Notice that this mechanism allows messages to persist across rounds.

We define network operational semantics in terms of small-steps transitions  $\nettran{\Cfg}{\act}{\Cfg'}$ of three kinds: firing starts on a given device (for which $\act$ is $\deviceId+$ where $\deviceId$ is the corresponding device identifier), firing ends and messages are sent on a given device (for which $\act$ is $\deviceId-$), and environment changes, where $\act$ is the special label $\envact$. This is formalised in Figure <ref> (bottom).

Rule [N-COMP] (available for sleeping devices, i.e., with $\Activation(\deviceId) = \actOFF$, and setting them to executing, i.e., $\Activation(\deviceId) = \actON$) models a computation round at device $\deviceId$: it takes the local value-tree environment filtered out of old values $\Trees' = \filter_\deviceId(\Field(\deviceId))$; then by the single device semantics it obtains the device's value-tree $\vtree$, which is used to update the system configuration of  $\deviceId$ to $\Trees = \mapupdate{\Trees'}{\envmap{\deviceId}{\vtree}}$.
Notice that expression $\emain$ is always evaluated against the device $\deviceId$ itself (that is, against no neighbour), and that local sensors $\Sens(\deviceId)$ are used by the auxiliary function $\builtinop{\bname}{\deviceId,\deviceId'}{\Trees,\Sens(\deviceId)}$ that gives the semantics to the built-in functions.
Furthermore, although this rule updates a device's system configuration instantaneously, it models computations taking an arbitrarily long time, since the update is not visible until the following rule [N-SEND]. Notice also that all values used to compute $\vtree$ are locally available (at the beginning of the computation), thus allowing for a fully-distributed implementation without global knowledge.

Rule [N-SEND] (available for running devices with $\Activation(\deviceId) = \actON$, and setting them to non-running) models the message sending happening at the end of a computation round at a device $\deviceId$. It takes the local value-tree $\vtree = \Field(\deviceId)(\deviceId)$ computed by last rule [N-COMP], and uses it to update neighbours' $\overline\deviceId$ values of $\Field(\overline\deviceId)$. Notice that the usage of $\Activation$ ensures that occurrences of rules [N-COMP] and [N-SEND] for a device are alternated.

Rule [N-ENV] takes into account the change of the environment to a new well-formed environment $\Envi'$—environment well-formedness is specified by the predicate $\wfn{\Envi}$ in Figure <ref> (middle)—thus modelling node mobility as well as changes in environmental parameters. Let $\overline\deviceId$ be the domain of $\Envi'$. We first construct a value-tree field $\Field_0$ and an activation predicate $\Activation_0$ associating to all the devices of $\Envi'$ the empty context $\emptyset$ and the $\actOFF$ activation. Then, we adapt the existing value-tree field $\Field$ and activation predicate $\Activation$ to the new set of devices: $\mapupdate{\Field_0}{\Field}$, $\mapupdate{\Activation_0}{\Activation}$ automatically handles removal of devices, mapping of new devices to the empty context and $\actOFF$ activation, and retention of existing contexts and activation in the other devices. We remark that this rule is also used to model communication failure as topology changes.

[Network evolution]
Consider the program in Example <ref>:

\[
\foldK(2,\texttt{+}, \texttt{min}(\nbrK\{\texttt{temperature}()\}, \texttt{temperature}()) )
\]

and let $\vtree^n = \mkvt{n}{\texttt{min}, \mkvt{n}{\mkvt{n}{\mathtt{temperature},n}}, \mkvt{n}{\mathtt{temperature},n}, n}$ be the result of evaluation of $\texttt{min}(\nbrK\{\texttt{temperature}()\}, \texttt{temperature}())$ in a device where $\texttt{temperature}() = n$ (with respect to the device itself as neighbour).

We start from a configuration $\Cfg_0 = \SystS{\EnviS{\Topo}{\Sens}}{\EnviS{\Field_0}{\Activation_0}}$ with three devices $\overline\deviceId$, so that $\Topo = \bp{(\deviceId_i, \deviceId_j) ~ \mid ~ i,j \le 3}$ (all devices are connected), $\Field_0 = \envmap{\overline\deviceId}{\emptyset}$ (devices do not hold any information), $\Activation_0 = \envmap{\overline\deviceId}{\actOFF}$ (devices are not computing) and

\[
\Sens = \envmap{\deviceId_1}{\{t=10\}}, \envmap{\deviceId_2}{\{t=15\}}, \envmap{\deviceId_3}{\{t=5\}}
\]

(temperatures are as in Example <ref>).

After transitions $\nettran{\Cfg_0}{\deviceId_2^+}{\Cfg} \nettran{}{\deviceId_2^-}{\Cfg_1}$, the computational field $\Field_0$ is updated by sending the result $\vtree_0 = \mkvt{2}{2, \texttt{+}, \vtree^{15}}$ of the computation of $\deviceId_2$ (with respect to its empty environment) to every device, obtaining $\Field_1 = \envmap{\overline\deviceId}{\{\envmap{\deviceId_2}{\vtree_0}\}}$.

Then, other transitions take place: $\nettran{\Cfg_1}{\deviceId_3^+}{\Cfg} \nettran{}{\deviceId_3^-}{\Cfg_2}$, where $\Field_1$ is further updated with the result $\vtree_1 = \mkvt{7}{2, \texttt{+}, \vtree^{5}}$ of the computation of $\deviceId_3$ (with respect to the information received from $\deviceId_2$), obtaining $\Field_2 = \envmap{\overline\deviceId}{\{\envmap{\deviceId_2}{\vtree_0}, \envmap{\deviceId_3}{\vtree_1}\}}$.

Finally, transitions $\nettran{\Cfg_2}{\deviceId_1^+}{\Cfg} \nettran{}{\deviceId_1^-}{\Cfg_3}$ happen as described in Example <ref>, producing $\Field_3 = \envmap{\overline\deviceId}{\{\envmap{\deviceId_1}{\vtree_2}, \envmap{\deviceId_2}{\vtree_0}, \envmap{\deviceId_3}{\vtree_1}\}}$ where $\vtree_2 = \mkvt{17}{2, \texttt{+}, \vtree^{10}}$.

Lastly, a transition $\nettran{\Cfg_3}{\envact}{\Cfg_4}$ may happen, lowering temperatures, deleting device $\deviceId_2$, inserting device $\deviceId_4$, and disconnecting device $\deviceId_1$ from device $\deviceId_3$. The result is configuration $\Cfg_4 = \SystS{\EnviS{\Topo'}{\Sens'}}{\EnviS{\Field_4}{\Activation_4}}$ where:

\begin{align*}
\Topo' = ~& \ap{\deviceId_1, \deviceId_4}, \ap{\deviceId_3, \deviceId_4}, \ap{\deviceId_4, \deviceId_1}, \ap{\deviceId_4, \deviceId_3} \\
\Sens' = ~&\envmap{\deviceId_1}{\{t=9\}}, \envmap{\deviceId_1}{\{t=4\}}, \envmap{\deviceId_4}{\{t=1\}} \\
\Field_4 = ~&\envmap{\deviceId_1}{\{\envmap{\deviceId_1}{\vtree_2}, \envmap{\deviceId_2}{\vtree_0}, \envmap{\deviceId_3}{\vtree_1}\}}, \envmap{\deviceId_3}{\{\envmap{\deviceId_1}{\vtree_2}, \envmap{\deviceId_2}{\vtree_0}, \envmap{\deviceId_3}{\vtree_1}\}}, \envmap{\deviceId_4}{\emptyset}, \\
\Activation_4 = ~&\envmap{\deviceId_1}{\actOFF}, \envmap{\deviceId_3}{\actOFF}, \envmap{\deviceId_4}{\actOFF}.
\end{align*}

Notice that devices $\deviceId_1$, $\deviceId_3$ are not aware yet of the disappearance of $\deviceId_2$, nor of their disconnection. When one of them will fire, the filter $\filter(\cdot)$ may be able to remove the obsolete values from the corresponding value-tree environments.

§.§ Type Preservation in

In this section we show that the evaluation rules for  are deterministic and preserve types, provided that the value-tree environment used for the evaluation is coherent with the expression being evaluated according to the following definition.

[Well Formed Value Tree]
Given a closed expression $\e$, a local-type-scheme environment $\LTStypEnv$, a type environment $\TtypEnv=\overline{\xname}:\overline{\type}$, and a type $\type$ such that $\expTypJud{\LTStypEnv}{\TtypEnv}{\e}{\type}$ holds, the set $\coherent{\e}{\type}{\LTStypEnv;\TtypEnv}$ of the well-formed value-trees for $\e$ is inductively defined as follows. $\vtree \in \coherent{\e}{\type}{\LTStypEnv;\TtypEnv}$ if and only if $\anyvalue = \vrootOf{\vtree}$ has type $T$ (i.e. $\expTypJud{\LTStypEnv}{\emptyset}{\anyvalue}{\type}$) and

* if $\e$ is a value, $\vtree$ is of the form $\mkvtree{}{\anyvalue}{}$;

* if $\e = \nbrK\{\e_1\}$, $\vtree$ is of the form $\mkvtree{}{\anyvalue}{\vtree_1}$ where $\vtree_1 \in \coherent{\e_1}{\type}{\LTStypEnv;\TtypEnv}$;

* if $\e = \repK(\e_1)\{\e_2\}$, $\vtree$ is of the form $\mkvtree{}{\anyvalue}{\vtree_1,\vtree_2}$ where $\vtree_1 \in \coherent{\e_1}{\type}{\LTStypEnv;\TtypEnv}$ and $\vtree_2 \in \coherent{\e_2(\xname)}{\type}{\LTStypEnv;\TtypEnv, \xname:\type}$;

* If $\e = \foldK(\e_1, \e_2, \e_3)$, $\vtree$ is of the form $\mkvtree{}{\anyvalue}{\vtree_1,\vtree_2,\vtree_3}$ where $\overline\vtree \in \coherent{\overline\e}{\type, (\type,\type) \to \type, \type}{\LTStypEnv;\TtypEnv}$;

* if $\e = \e'(\overline\e)$ and $\expTypJud{\LTStypEnv}{\TtypEnv}{\e'}{\type'}$, $\expTypJud{\LTStypEnv}{\TtypEnv}{\overline\e}{\overline\type}$, then $\vtree$ is of the form $\mkvtree{}{\anyvalue}{\vtree',\overline\vtree,\vtree''}$ where $\vtree' \in \coherent{\e'}{\type'}{\LTStypEnv;\TtypEnv}$, $\overline\vtree \in \coherent{\overline\e}{\overline\type}{\LTStypEnv;\TtypEnv}$, and either:

* $\funvalue = \vrootOf{\vtree'}$ is a built-in function and $\vtree'' = \mkvtree{}{\anyvalue}{}$,

* $\funvalue$ is not a built-in function and $\vtree'' \in \coherent{\body{\funvalue}}{\type}{\LTStypEnv;\TtypEnv, \args{\funvalue} : \overline\type}$.

Similarly, the set of well-formed value-tree environments $\coherentEnv{\e}{\type}{\LTStypEnv;\TtypEnv}$ is the set of $\Trees = \envmap{\overline\deviceId}{\overline\vtree}$ such that $\overline\vtree \in \coherent{\e}{\type}{\LTStypEnv;\TtypEnv}$.

In other words, the above definition demands value-trees to be plausible outcomes of the evaluation of $\e$.

Let $\e$ be a well-typed closed expression and $\Trees \in \coherentEnv{\e}{\type}{\LTStypEnv;\TtypEnv}$. Then for all device identifiers $\deviceId$, $\deviceId'$ and sensor state $\senstate$:

* $\bsopsemFAIL{\deviceId,\deviceId}{\Trees}{\senstate}{\e}$ cannot hold.

* There is at most one derivation of the kind $\bsopsem{\deviceId,\deviceId'}{\Trees}{\senstate}{\e}{\vtree}$ or $\bsopsemFAIL{\deviceId,\deviceId'}{\Trees}{\senstate}{\e}$.

Notice that a failure can occur only if in a certain subexpression (which is a relational sensor application or $\nbrK$-expression) the neighbour $\deviceId'$ is not in $\domof{\Trees} \cup \{\deviceId\}$, thus in particular $\deviceId' \neq \deviceId$. Any construct other than a $\foldK$ either propagates the neighbour $\deviceId'$ as is or resets it to $\deviceId$, so for a failure to occur in a sub-evaluation of $\bsopsemFAIL{\deviceId,\deviceId}{\Trees}{\senstate}{\e}$ the involved subexpression must be inside a $\foldK$-expression. However, $\foldK$-expressions never fail, as they “absorb” failures by skipping failing neighbours, concluding the proof.

* We assume that $\e$ has at least one possible derivation of the big-step operational semantics, and prove by induction on its length that this derivation is unique.

If $\e$ is a value, a $\repK$- or $\foldK$-expression, then it cannot fail since the conclusions of every rule in Figure <ref> is either a function application or a $\nbrK$-expression. Furthermore, its evaluation produces a value by rules [E-VAL], [E-REP] or [E-FOLD] (respectively), using fact (<ref>) and observing that the only sub-evaluation which may fail occur in the third argument of a $\foldK$, and does not influence the evaluation of the $\foldK$ itself. Such value must be unique, since by inductive hypothesis so are the results of its subexpressions and rules are deterministic.

If $\e$ is an $\nbrK$-expression, then exactly one of the rules [E-NBR], [E-NBR-LOC] or [E-NBR-FAIL] must be applicable, depending on whether resp. $\deviceId' = \deviceId$, $\deviceId' \in \domof{\Trees} \setminus \deviceId$, or neither holds. In the first two cases, the result is then unique by inductive hypothesis and rule determinism.

Finally, if $\e = \e'(\overline\e)$ is a function application, then the evaluation of $\e'$ does not fail by fact (<ref>), and thus produces a uniquely determined function $\funvalue$ (with a possibly infinite derivation) by inductive hypothesis. If the evaluation of some of the arguments fails, then rule [E-APP-ARG-FAIL] applies and $\e$ fails, and none of the other function application rules ([E-B-APP], [E-D-APP], [E-R-APP-FAIL], [E-D-APP-FAIL]) applies since they all require all arguments to evaluate to a value.

Otherwise, $\overline\e$ evaluates (uniquely) to $\overline\anyvalue$. If $\funvalue = \snvalue$ is a relational sensor and $\deviceId'$ is not in $\domof{\piBof{\snvalue}{\Trees}} \cup \{\deviceId\}$, then $\e$ fails by Rule [E-R-APP-FAIL] and does not produce a value since $\builtinop{\snvalue}{\deviceId,\deviceId'}{\piBof{\snvalue}{\Trees},\senstate}$ is undefined making rule [E-B-APP] inapplicable. If instead $\funvalue$ is a built-in function which is not a relational sensor or $\deviceId'$ is in $\domof{\piBof{\funvalue}{\Trees}} \cup \{\deviceId\}$, then $\builtinop{\funvalue}{\deviceId,\deviceId'}{\piBof{\funvalue}{\Trees},\senstate}$ is defined and rule [E-B-APP] is applicable while rule [E-R-APP-FAIL] is not. The result is then unique by inductive hypothesis and rule determinism.

The only remaining case is when $\funvalue$ is a user-defined or anonymous function. By inductive hypothesis, $\applySubstitution{\body{\funvalue}}{\substitution{\args{\funvalue}}{\vrootOf{\overline{\vtree}}}}$ either fails or it produces a unique value. In the first case, rule [E-D-APP] applies (producing an unique value) while rule [E-D-APP-FAIL] does not; in the second case the converse happens, concluding that derivations are unique (when present).

By this lemma, evaluation does not result on  when it is performed relative to the current device (as it is the case for main expressions), and rules are deterministic. Furthermore, the evaluation rules respect the types given in <Ref>, provided that the built-in interpretations respect the given types. Formally, given $\bname$ such that $\expTypJud{\OStypEnv}{\emptyset}{\bname}{\overline\type \to \type}$ and any $\expTypJud{\OStypEnv}{\emptyset}{\overline\anyvalue}{\overline\type}$, $\Trees = \envmap{\overline\deviceId}{\mkvtree{}{\overline\anyvalue'}{}}$ with $\expTypJud{\OStypEnv}{\emptyset}{\overline\anyvalue'}{\type}$, $\deviceId' \in \{\deviceId,\overline\deviceId\}$, then we require $\builtinop{\bname}{\Trees,\senstate}{\deviceId,\deviceId'}$ to be a value of type $\type$.

Assume that the interpretation of built-in operators respects the given types.
Let $\TtypEnv=\overline{\xname}:\overline{\type}$ and $\expTypJud{\LTStypEnv}{\emptyset}{\overline{\anyvalue}}{\overline{\type}}$, so that $\lengthOf{\overline{\anyvalue}}=\lengthOf{\overline{\xname}}$.
If $\expTypJud{\LTStypEnv}{\TtypEnv}{\e}{\type}$, $\Trees\in \coherentEnv{\e}{\type}{\LTStypEnv;\TtypEnv}$ and $\bsopsem{\deviceId,\deviceId'}{\Trees}{\senstate}{\applySubstitution{\e}{\substitution{\overline{\xname}}{\overline{\anyvalue}}}}{\vtree}$, then $\vtree \in \coherent{\e}{\type}{\LTStypEnv;\TtypEnv}$.

Notice that, since the evaluation of $\e$ produces a value-tree which is coherent with $\e$, the value-tree environment $\Trees$ can be proved to be coherent with the main expression by induction on the network evolution.

Furthermore, observe that the typing rules (in Figure <ref>) and the evaluation rules (in Figure <ref> and <ref>) are syntax directed. Then the proof can be carried out by induction on the derivation length for $\bsopsem{\deviceId,\deviceId'}{\Trees}{\senstate}{\applySubstitution{\e}{\substitution{\overline{\xname}}{\overline{\anyvalue}}}}{\vtree}$, while using the following standard lemmas.

Let $\TtypEnv=\overline{\xname}:\overline{\type}$, $\expTypJud{\OStypEnv}{\emptyset}{\overline{\anyvalue}}{\overline{\type}}$. If $\expTypJud{\LTStypEnv}{\TtypEnv}{\e}{\type}$, then $\expTypJud{\LTStypEnv}{\emptyset}{\applySubstitution{\e}{\substitution{\overline{\xname}}{\overline{\anyvalue}}}}{\type}$.

Straightforward by induction on application of the typing rules for expressions in Figure <ref>.

Let $\LTStypEnv'\supseteq\LTStypEnv$, $\TtypEnv'\supseteq\TtypEnv$ be such that $\domof{\LTStypEnv'}\cap\domof{\TtypEnv'}=\emptyset$. If $\expTypJud{\LTStypEnv}{\TtypEnv}{\e}{\type}$, then $\expTypJud{\LTStypEnv'}{\TtypEnv'}{\e}{\type}$.

Straightforward by induction on application of the typing rules for expressions in Figure <ref>.

We proceed by induction on the derivation length.

The fact that $\vrootOf{\vtree}$ has type $\type$ can be verified by matching step-by-step every rule in <Ref> with the corresponding rule in <Ref>, while using the inductive hypothesis and two further assumptions: for rule [E-B-APP], that built-in functions $\bname$ respect the given types; for rules [E-NBR] and [E-REP], that $\Trees$ is coherent with $\e$.

Finally, the fact that $\vtree$ has the required sub-trees follows by inductive hypothesis since every rule in <Ref> respects the corresponding row of Definition <ref>, together with the fact that $\Trees$ is coherent with $\e$ (for rules [E-NBR] and [E-REP] only).

§  VS

In this section, we provide a formal account of  the relationship between  and the  minimal core calculus for Aggregate Computing [9].

In <Ref>, we recollect .
In <Ref>, we define a fragment  of , which we call , aimed at ensuring that
each  program is an  program that behaves in the same way.
In <Ref>, we define the fragment  of    which
corresponds to , we call call it   .
Then, in <Ref> we prove the equivalence between  and  – depicted in Figure <ref>.

Pictorial representation of relationship between ,   and their fragments  and .

Finally, in <Ref>, we  point out that  provides a different “flavour” of field computation with respect to ,
though without losing practical expressiveness.

§.§ A Quick Recollection of

The syntax of  programs (according to its original presentation [9]) is the same of  programs (in Figure <ref>), with a richer syntax of values and two other minor differences: the update function $\e_2$ in a $\repK$ construct $\repK (\e_1) \{\e_2\}$ is required to be an anonymous function $\e_2 = (\xname) \toSymK{\e'}$,[We remark that this difference is historical in nature:  could be straightforwardly extended to allow for general update function expressions.] and the language construct for $\foldK$ is replaced by a built-in with the same meaning, so it does not appear in the syntax.
In the richer syntax of  values (given in Figure <ref>), values are divided into local values, which are  the values of , and neighbouring (field) values, which not allowed to appear in source code and arise at runtime.
Neighbouring values are maps $\envmap{\overline\deviceId}{\overline \lvalue}$ from device identifiers to local values. In , they are produced  by
evaluating  the $\nbrK$ construct and returned by some built-in functions.

\begin{array}{lcl@{\hspace{55mm}}r}
%        \PROGRAM & \BNFcce & \overline{\FUNCTION}  \; \e
%                                                                                &   {\footnotesize \mbox{program}} \\[2pt]
%        \FUNCTION & \BNFcce &  \defK \; \fname (\overline{\xname}) \; \{\e\}
%                                                                                &   {\footnotesize \mbox{function declaration}} \\[-2pt]
%        \e & \BNFcce &  \xname \; \BNFmid \; \anyvalue \; \BNFmid \; (\overline{\xname}) \; \toSym{\name} \; \e \; \BNFmid \; \e(\overline{\e}) \; \BNFmid \; \repK(\e)\{ (\xname) \;\texttt{=>}\; \e \} \; \BNFmid \; \nbrK\{\e\}
%                                                                                &   {\footnotesize \mbox{expression}} \\[2pt]
%        \\[-6pt] \hline \\[-6pt]
\anyvalue & \BNFcce & \lvalue   \; \BNFmid \;  \eqhl{\fvalue}   &   {\footnotesize\mbox{value}} \\[2pt]
\fvalue & \BNFcce & \eqhl{\envmap{\overline{\deviceId}}{\overline{\lvalue}}}  &   {\footnotesize\mbox{neighbouring (field) value}} \\[2pt]
\lvalue & \BNFcce & \dcOf{\dc}{\overline{\lvalue}} \; \BNFmid \; \funvalue &   {\footnotesize\mbox{local value}} \\[2pt]
\funvalue & \BNFcce & \bname  \; \BNFmid \; \fname \; \BNFmid \; (\overline{\xname}) \; \toSymK{\e}  &   {\footnotesize \mbox{function value}} \\[2pt]
\end{array}

Syntax of  values – extensions with respect to  values are highlighted in grey.

The Hindley-Milner type system for  [9] is given in <Ref> (excluding the grey rule [T'-FOLD]), and distinguishes between types for local values from those that are not (namely, neighbouring types $\ftype$ for neighbouring values), as well as between types that are allowed to be returned by functions from those that are not.

This induces four different type categories: types $\type$, local types $\ltype$, return types $\rtype$, and local return types
$\stype$—they are illustrated at the bottom of <Ref>.
The main restrictions enforced by this type system in order to ensure the domain alignment property[Domain alignment holds iff the domain of neighbouring values $\fvalue$ obtained from expressions $\e$ is equal to the set of all neighbours which computed the same $\e$ in their previous evaluation round.] are:

* anonymous functions cannot capture variables of neighbouring type;

* $\repK$ statements are demanded to have a local return type;

* neighbouring types can only be built from local return types $\stype$ (i.e., $\ftype = \ftypeOf{\stype}$), since neighbouring values need to be aggregated and this is possible only for return types, and avoiding “neighbouring values of neighbouring values” which may lead to unintentionally heavy computations;

* types of the form $(\overline\type) \to \ftype$ (functions returning neighbouring values) are not return types.
Thus, functions of type $(\overline\type) \to \ftype$ are used almost as in a first-order language. In particular, there is no way to write a non-constant expression $\e$ evaluating to such a function.

The  operational semantics [9] is given as a transition system analogous to that in Section <ref>, but based on a different judgement for the device operational semantics $\bsopsem{\deviceId}{\Trees}{\senstate}{\emain}{\vtree}$.
For sake of completeness, we report the details of the  operational device semantics in Appendix <ref>.

In the remainder of this paper, we assume that the built-in operators of  always include:

* $\mathtt{consthood}(\anyvalue)$, which returns a neighbouring field value constantly equal to its (local) input $\anyvalue$;

* $\mathtt{map}(\funvalue, \overline\fvalue)$, which applies a function $\funvalue$ with local inputs and outputs (of any ariety) pointwise to neighbouring field values $\overline\fvalue$;

* $\foldK(\lvalue, \funvalue, \fvalue)$, which collapses a field $\fvalue$ and starting value $\lvalue$ via an aggregator $\funvalue$ (exactly as in ).

Furthermore, we use $\ifK  (\e_1) \{ \e_2 \} \{ \e_3 \}$ as short for $\muxK(\e_1, () ~\toSymKabs{\e_2}, () ~\toSymKabs{\e_3})()$, as in .

\begin{array}{lclrr}
\textbf{Types:} \\[1pt]
\type	& \BNFcce & \tvar \; \BNFmid \; {\rtype} \; \BNFmid \; \ltype											   &   {\footnotesize \mbox{type}}  &
\multirow{5}{*}{\raisebox{-1.3cm}{
\begin{tikzpicture}[xscale=1.7,yscale=1.1]
\draw[ultra thick] (-0.5,0) circle (1cm);
\draw[ultra thick] (0.5,0) circle (1cm);
\node[draw,rectangle] (TT) at (0, 1.25) {$\type$};
\node[draw,rectangle] (LT) at (-1, 0.5) {$\ltype$};
\node[draw,rectangle] (RT) at (1, 0.5) {$\rtype$};
\node[draw,rectangle] (ST) at (0, -0.5) {$\stype$};
\node (B) at (0.1, 0.5) {$\builtintype$};
\node (TxS) at (0, 0.05) {$(\overline\type) \rightarrow \stype$};
\node (F) at (0.8, -0.4) {$\ftype$};
\node (TxF) at (-0.95, -0.3) {$(\overline\type) \rightarrow \rtype$};
\end{tikzpicture}
\\[2pt]
\ltype	& \BNFcce & \ltvar \; \BNFmid \; {\stype} \; \BNFmid \; (\overline{\type})\to\rtype	 & {\footnotesize \mbox{local type}} \\[2pt]
\rtype	& \BNFcce & \rtvar \; \BNFmid \; \stype \; \BNFmid \; \ftype										  &   {\footnotesize \mbox{return type}} \\[2pt]
\stype	& \BNFcce & \stvar \; \BNFmid \; \builtintype \; \BNFmid \; (\overline{\type})\to\stype	&   {\footnotesize \mbox{local return type}} \\[2pt]
\ftype	& \BNFcce & \ftypeOf{\stype}																							&   {\footnotesize \mbox{neighbouring type}} \\[2pt]
\multicolumn{4}{l}{\textbf{Local type schemes:}} \\[1pt]
\ltypescheme & \BNFcce & \forall\overline{\tvar}\overline{\ltvar}\overline{\rtvar}\overline{\stvar}.\ltype
&   {\footnotesize \mbox{local type scheme}} \\
\end{array} \\
%%%  EXPRESSIONS
\textbf{~~Expression typing:} \hfill \boxed{\expTypJud{\LTStypEnv}{\TtypEnv}{\e}{\type}} \\[5pt]
\begin{array}{c}
\nullsurfaceTyping{T'-VAR}{
\expTypJud{\LTStypEnv}{\TtypEnv, \xname:\type}{\xname}{\type}
\qquad
\surfaceTyping{T'-DAT}{ \quad
\applySubstitution{\stype'}{\substitution{\overline\stvar}{\overline\stype''}} = (\overline{\stype})\rightarrow\stype
\qquad
\expTypJud{\TStypEnv}{\TtypEnv}{\overline{\lvalue}}{\overline{\stype}}
\expTypJud{\TStypEnv,\dc: \forall\overline\stvar. \stype'}{\TtypEnv}{\dc(\overline{\lvalue})}{\stype}
\skiptransition
\surfaceTyping{T'-A-FUN}{  \quad
\overline{\yname}=\FV{(\overline{\xname}) \; \toSymKtag{\name}{\e}} \quad
{\expTypJud{\LTStypEnv}{\TtypEnv}{\overline\yname}{\overline{\ltype}}} \quad
\expTypJud{\LTStypEnv}{\TtypEnv, \overline{\xname} : \overline\type}{\e}{\rtype}
\expTypJud{\LTStypEnv}{\TtypEnv}{(\overline{\xname}) \; \toSymKtag{\name}{\e}}{(\overline\type) \rightarrow \rtype}
\skiptransition
\surfaceTyping{T'-N-FUN}{ \quad
\mbox{$\funvalue$ is a (built-in or declared) function}
\expTypJud{\TStypEnv,\funvalue : \forall\overline\tvar\overline\ltvar\overline\rtvar\overline\stvar.\ltype}{\TtypEnv}{\funvalue}{\applySubstitution{\ltype}{\substitution{\overline\tvar}{\overline\type},~ \substitution{\overline{\ltvar}}{\overline{\ltype}},~ \substitution{\overline{\rtvar}}{\overline{\rtype}},~ \substitution{\overline{\stvar}}{\overline{\stype}}}}
\skiptransition
\surfaceTyping{T'-APP}{ \qquad
\expTypJud{\LTStypEnv}{\TtypEnv}{\e}{(\overline\type)\rightarrow\rtype} \qquad
\expTypJud{\LTStypEnv}{\TtypEnv}{\overline{\e}}{\overline\type}
\expTypJud{\LTStypEnv}{\TtypEnv}{\e(\overline{\e})}{\rtype}
\skiptransition
\surfaceTyping{T'-REP}{ \quad
\expTypJud{\LTStypEnv}{\TtypEnv}{\e_1}{\stype} \qquad
\expTypJud{\LTStypEnv}{\TtypEnv}{(\xname) \toSymK{\e_2}}{\stype \rightarrow \stype}
\expTypJud{\LTStypEnv}{\TtypEnv}{\repK(\e_1)\{(\xname) \toSymK{\e_2}\}}{\stype}
\quad
\surfaceTyping{T'-NBR}{ \quad
\expTypJud{\LTStypEnv}{\TtypEnv}{\e}{\stype}
\expTypJud{\LTStypEnv}{\TtypEnv}{\nbrK\{\e\}}{\ftypeOf{\stype}}
\skiptransition
\eqhl{\surfaceTyping{T'-FOLD}{ \qquad
\begin{array}{ll}
\expTypJud{\TStypEnv}{\TtypEnv}{\e_1}{\stype}
& \quad
\expTypJud{\TStypEnv}{\TtypEnv}{\e_3}{\ftypeOf{\stype} \text{ or } \stype}
\\
\expTypJud{\TStypEnv}{\TtypEnv}{\e_2}{(\stype, \stype) \rightarrow \stype}
& \quad
\expTypJud{\TStypEnv}{\TtypEnv}{\overline\xname}{\overline\ltype}
\quad\text{where}\; \overline\xname = \FV{\e_3}
\end{array}
\expTypJud{\TStypEnv}{\TtypEnv}{\foldK(\e_1,\e_2,\e_3)}{\stype}
\end{array} \\~\\
%%%  FUNCTIONS
\textbf{~~Function typing:} \hfill \boxed{\funTypJud{\LTStypEnv}{\FUNCTION}{\ltypescheme}} \\[5pt]
\qquad \qquad
\begin{array}{c}
\surfaceTyping{T'-FUNCTION}{ \qquad
\begin{array}{ll}
\expTypJud{\LTStypEnv, \fname: (\overline\type)\to\rtype}{\overline{\xname}:\overline{\type}}{\e}{\rtype} \qquad
\overline{\tvar}\overline{\ltvar}\overline{\rtvar}\overline{\stvar}=\FTV{(\overline{\type})\rightarrow\rtype} %\\
%\text{arguments not occurring in } \e \text{ are local}
\end{array}
\funTypJud{\LTStypEnv}{\defK \; \fname (\overline{\xname}) \; \eqSymK{\e}}{
\forall\overline{\tvar}\overline{\ltvar}\overline{\rtvar}\overline{\stvar}.(\overline{\type})\rightarrow\rtype
\end{array} \\~\\
%%%  PROGRAMS
\textbf{~~Program typing:} \hfill {\boxed{\funTypJud{\LTStypEnv_0}{\PROGRAM}{\type}}} \\[5pt]
\qquad \quad
\begin{array}{c}
\surfaceTyping{T'-PROGRAM}{ \\
\FUNCTION_i=(\defK \; \fname_i (\_) \; \_) \qquad
\funTypJud{\LTStypEnv_{i-1}}{\FUNCTION_i}{\ltypescheme_i} \qquad
\LTStypEnv_i=\LTStypEnv_{i-1},\, \fname_i:\ltypescheme_i \qquad
(i \in 1..n) \\
\expTypJud{\LTStypEnv_n}{\emptyset}{\e}{\type}
\funTypJud{{\LTStypEnv_0}}{\FUNCTION_1\cdots\FUNCTION_n  \; \e}{{\type}}
\end{array}
\end{array}$
Hindley-Milner typing for  and  expressions, function declarations, and programs – differences with  typing are highlighted in grey.

§.§ The  Fragment of

is obtained by adding the following two custom restrictions, on how neighbouring field values can be processed, to the Hindley-Milner type system for  [9]:

Built-in functions need to have local arguments, except for the built-ins $\mathtt{map}$ and $\mathtt{foldhood}$.

Expressions of neighbouring type can only be aggregated to local values with a $\foldK$ operator if they do not capture variables of neighbouring types; so that, e.g., aggregating arguments of neighbouring type is never allowed.

[About restriction R1]
In order to show the rationale behind Restriction R1, consider a built-in function  rearranging values $\fvalue(\deviceId)$ relative to neighbours in increasing order of neighbour identifier $\deviceId$, thus effectively mixing up values relative to different neighbours. Formally, applying this function to a neighbouring value $\fvalue = \envmap{\overline\deviceId}{\overline\lvalue}$ (assuming $\deviceId_1 \leq \ldots \leq \deviceId_n$), we obtain the neighbouring value $\fvalue' = \envmap{\deviceId_1}{\lvalue_{\pi_1}}, \ldots, \envmap{\deviceId_n}{\lvalue_{\pi_n}}$ where the permutation $\pi$ is such that $\lvalue_{\pi_1} \leq \ldots \lvalue_{\pi_n}$. This function is conceivable (although artificial) in , but it is not implementable in , hence it is disallowed in . We remark however that all practically used built-in functions in  are definable with respect to those allowed by restriction R1.

[About restriction R2]
In order to show the rationale behind Restriction R2, consider the following   program
def hfc_avghood(x)  // : field(num) -> num
foldhood(0, +, x) / foldhood(0, +, 1)

hfc_avghood(nbrsns-temp()) // : num

which on each device calculates the average temperature of neighbours.
We may suppose that the same code, interpreted as an  program, would  calculate the same quantity.
Instead, it is equivalent to the simpler  program

which yields the temperature of the device where it is evaluated.
If we evaluate the expression  against a neighbour $\deviceId'$,
we obtain  the temperature $t'$ of that neighbour. Unfortunately, in the program the expression occurs outside of the scope of any $\foldK$ construct and so
it is evaluated
against the device $\deviceId$ where it is evaluated.
When function  is applied to $t$ (the temperature of $\deviceId$), the neighbour device $\deviceId'$ is ignored by both $\foldK$ constructs,
which fail to interpret the captured neighbouring value as such. The value of the program on device $\deviceId$
is then $n\cdot t / n = t$, where $n$ is the number of neighbours  of $\deviceId$ (including $\deviceId$ itself)
and $t$ is the value of the temperature on device $\deviceId$.

We remark that an  program computing the average temperature of neighbours also when interpreted as an  program can be conveniently written, by resorting to suitable programming patterns (illustrated in <Ref>). In particular, for the example above, it is sufficient to make  a “by-name” parameter, thus obtaining the following  program:
def hfc_nc_avghood(y)  // : (() -> field(num)) -> num
foldhood(0, +, y()) / foldhood(0, +, 1)

hfc_nc_avghood(() => nbrsns-temp()) // : num

We remark that all  programs considered in previous works [9, 2, 56] actually belong to  (or can straightforwardly  be reformulated in order to do so). The following lemma provides a characterisation of  in terms of the type system in <Ref>.

The type system in <Ref> is a restriction of the Hindley-Milner type system for  [9] enforcing restrictions R1 and R2.

Restriction R1 is implicitly implemented in the definition of $\LTStypEnv_0$, in which the only built-in with field arguments is $\mathtt{map}$.
Restriction R2 is implemented in Rule [T'-FOLD], by requiring each free variable occurring in the third branch to be of local type – in
the type system for  [9] $\foldK$ is a built-in function, so there is no special rule for $\foldK$-expressions.
All the other rules are the same as for the Hindley-Milner type system for  [9].

§.§ The  Fragment of

is the fragment of  that can be typed by rules in <Ref>. These rules are significantly more restrictive then the rules in <Ref>, in particular:

* They acknowledge the existence of the four type categories, in particular of $\ftypeOf{\stype}$;

* They demand that (anonymous and defined) functions have an allowed return type $\rtype$;

* They require the sub-expressions of $\repK$, $\nbrK$ and $\foldK$ to have local return type $\stype$;

* Finally, they require captured variables to have local type, in the body of both anonymous functions and folding expressions.

For convenience in the comparison with , we assume that  comprises the  and  built-ins, even though in  those functions could also be defined as follows.
def consthood(v)  v
def map(f, v, $\ldots$)  f(v, $\ldots$)

The embedding of   as a fragment of  can be formally characterised by means of the following definition and theorem.

The erasure of an  type $\type$ is the type $\erasureof{\type}$ obtained from $\type$ by replacing all occurrences of $\ftypeOf{\ltype}$ with $\ltype$ and dropping the distinction between the different kinds of type variables (i.e., considering each of them as a standard type variable $t$).
Similarly, the erasure of a type scheme $\forall\overline{\tvar}\overline{\ltvar}\overline{\rtvar}\overline{\stvar}.\ltype$ is the type scheme $\forall\overline{\tvar}\overline{\ltvar}\overline{\rtvar}\overline{\stvar}.\erasureof{\ltype}$ (dropping distinction between kinds of variables).
Finally, the erasure of a type environment $\TtypEnv = \overline\xname : \overline\type$ is $\erasureof{\TtypEnv} = \overline\xname : \erasureof{\overline\type}$; and the erasure of a type-scheme environment is $\erasureof{\TStypEnv} = \overline\xname : \erasureof{\overline\ltypescheme}$.

Assume that $\expTypJud{\TStypEnv}{\TtypEnv}{\e}{\type}$ in  . Then $\expTypJud{\erasureof{\TStypEnv}}{\erasureof{\TtypEnv}}{\e}{\erasureof{\type}}$ in .

We proceed by induction on the syntax of $\e$. If $\e = \nbrK\{\e'\}$, then $\type = \ftypeOf{\stype}$ where $\expTypJud{\TStypEnv}{\TtypEnv}{\e'}{\stype}$ by rule [T'-NBR]. By inductive hypothesis, $\expTypJud{\erasureof{\TStypEnv}}{\erasureof{\TtypEnv}}{\e'}{\erasureof{\stype}}$ in . It follows by rule [T-NBR] that $\expTypJud{\erasureof{\TStypEnv}}{\erasureof{\TtypEnv}}{\e}{\erasureof{\stype}}$, and the thesis follows since $\erasureof{\stype} = \erasureof{\ftypeOf{\stype}}$.

In all other cases, the thesis follows since the  rules can be obtained by removing restrictions from their counterparts in : that types are restricted to peculiar kinds $\ltype$, $\rtype$ or $\stype$ (every rule except for [T'-VAR]); that captured variables have local type (in rules [T'-A-FUN] and [T'-FOLD]).

§.§ Equivalence between  and

In order to prove the equivalence between  and , we first need to define what it means for an expression to have an equivalent behaviour in the two languages.

Assume that $\expTypJud{\LTStypEnv}{\TtypEnv}{\e}{\type}$ in / where $\TtypEnv = \overline\xname : \overline\type$. Let $\overline\anyvalue$ be  values of type $\overline\type$, and let $\anyvalue(\deviceId)$ be defined by cases as $\lvalue(\deviceId) = \lvalue$, $\fvalue(\deviceId) = \lvalue$ where $\lvalue$ is such that $\envmap{\deviceId}{\lvalue} \in \fvalue$.

We say that $\applySubstitution{\e}{\substitution{\overline\xname}{\overline\anyvalue}}$ has the same behaviour in  and  whenever:

* if $\type$ is a local type, $\bsopsem{\deviceId}{\Trees}{\senstate}{\applySubstitution{\e}{\substitution{\overline\xname}{\overline\anyvalue}}}{\mkvtree{}{\lvalue}{\overline\vtree}}$ if and only if $\bsopsem{\deviceId,\deviceId}{\Trees}{\senstate}{\applySubstitution{\e}{\substitution{\overline\xname}{\overline\anyvalue(\deviceId)}}}{\mkvtree{}{\lvalue}{\overline\vtree'}}$ for some $\overline\vtree$ and $\overline\vtree'$;

* if $\type$ is a field type, $\bsopsem{\deviceId}{\Trees}{\senstate}{\applySubstitution{\e}{\substitution{\overline\xname}{\overline\anyvalue}}}{\mkvtree{}{\fvalue}{\overline\vtree}}$ if and only if $\bsopsem{\deviceId,\deviceId_i}{\Trees}{\senstate}{\applySubstitution{\e}{\substitution{\overline\xname}{\overline\anyvalue(\deviceId_i)}}}{\mkvtree{}{\lvalue_i}{\overline\vtree'}}$ for some $\overline\vtree$ and $\overline\vtree'$ where $\fvalue = \envmap{\deviceId_i}{\lvalue_i}$.

Assuming that the above coherence condition holds for built-in functions, then it holds for every expression, as shown in the following theorem.

Assume that for every built-in function $\bname$ with local arguments, $\bname(\overline\xname)$ has the same behaviour in  and  for every substitution of $\overline\xname$. Assume that $\expTypJud{\LTStypEnv}{\TtypEnv}{\e}{\type}$ in / where $\TtypEnv = \overline\xname : \overline\type$, and let $\overline\anyvalue$ be  values of type $\overline\type$. Then $\applySubstitution{\e}{\substitution{\overline\xname}{\overline\anyvalue}}$ has the same behaviour in  and .

We proceed by induction on the syntax of closed expressions $\e$, simultaneously for all possible network environments.

* $\e = \anyvalue$: since  rule [E-VAL] is identical to  rule [E-LOC], the thesis holds whenever $\e = \anyvalue$ is a local value. Since field values are not allowed to appear in source  programs, and do not exist in  programs, the thesis follows.

* $\e = \xname$: if $\type$ is a local type, the same reasoning for $\e = \anyvalue$ applies. If $\type$ is a field type and $\xname$ is substituted with $\fvalue$, the evaluation result is $\proj{\fvalue}{\domof{\Trees}}$ in . In , for every $\deviceId \in \domof{\Trees}$, $\applySubstitution{\e}{\substitution{\overline\xname}{\overline\anyvalue(\deviceId)}}$ is $\fvalue(\deviceId)$, which is a local value hence it evaluates to itself by rule [E-VAL], concluding this part of the proof.

* $\e = \e_{n+1}(\overline\e)$: notice that rules [E-B-APP] and [E-D-APP] are identical in  and  (ignoring the neighbour device $\deviceId'$). This concludes the proof in case all $\overline\e$ and the resulting output of $\e_{n+1}$ are local. Otherwise, there are three possibilities:

* $\e_{n+1}$ evaluates to a built-in function, so that the thesis follows by inductive hypothesis and the coherence hypothesis on built-in functions.

* $\e_{n+1}$ evaluates to a user-defined or anonymous function $\fname$. In this case, the domain of computation is restricted both in  and in  to the aligned neighbours $\piBof{\fname}{\Trees}$; which in fact reduces all fields involved in the computation to the new domain, both in  by Rule [E-FLD] and in  by Rule [E-FOLD] (which aggregates only values from devices in $\domof{\Trees}$).

After alignment, in both cases the argument's values are substituted into the body of $\fname$. If all arguments have local type, the substitution is performed in the same way both in  and , hence the result of $\e$ corresponds by inductive hypothesis.
If some argument has field type, then those arguments cannot occur within folding expressions, and are either ignored or manipulated point-wise to form a field result. In this case, the results of $\e$ for every neighbour $\deviceId'$ correspond to the point-wise results of field in , concluding the proof in this case.

* $\e = \repK(\e_1)\{(\xname) \toSymK{\e_2}\}$: the thesis follows (with a further induction on firing events) by noticing that rule [E-REP] in  corresponds to that of  together with the expansion of the anonymous function application.

* $\e = \nbrK\{\e_1\}$: by inductive hypothesis, $\e_1$ is an expression of local type which always evaluates to the same trees in  and . It follows by  rule [E-NBR] that $\e$ in $\deviceId$ evaluates to the field mapping $\overline\deviceId$ to the corresponding values $\overline\anyvalue$ of $\e_1$ in those devices. By  rules [E-NBR] (for $\deviceId_i \neq \deviceId$) and [E-NBR-LOC] (for $\deviceId_i = \deviceId$) it follows that $\bsopsem{\deviceId,\deviceId_i}{\Trees}{\senstate}{\e}{\mkvtree{}{\anyvalue_i}{\overline\vtree}}$ for all $i = 1 \ldots n$.

* $\e = \foldK(\e_1, \e_2, \e_3)$: by inductive hypothesis, $\e_1$ and $\e_2$ evaluate to the same local values $\anyvalue'$, $\funvalue$ while $\e_3$ does not contain free variables of field type and it satisfies that

\[
\bsopsem{\deviceId}{\Trees}{\senstate}{\e_3}{\mkvtree{}{(\envmap{\overline\deviceId}{\overline{\anyvalue}})}{\overline\vtree}} \iff \bsopsem{\deviceId,\overline\deviceId}{\Trees}{\senstate}{\e_3}{\mkvtree{}{\overline\anyvalue}{\overline\vtree}}
\]

By  rule [E-FOLD], the overall result of the expression is then $\funvalue(\anyvalue', \overline\anyvalue)$ (computed two elements at a time), which corresponds to the result of applying $\foldK$ in .

§.§  Expressiveness

In this section, we argue that  is an expressive language for distributed computations. <Ref> shows that  contains many relevant aggregate programs, including those providing universality for distributed computations. In <Ref>, we argue that most of the  programs which are not directly interpretable in  can be automatically refactored (while preserving their behaviour) in order to fit within  (hence ), enlarging the class of aggregate programs expressible in  to virtually all  programs. This process is exemplified in <Ref>, where the self-stabilising fragment of  [56] is ported to  through the refactoring just introduced. Finally, <Ref> argues that the  programs that are not in  can fruitfully extend the expressive power of .

§.§.§  examples: G and T blocks and universality

def G(source, initial, metric, accumulate)
rep ( pair(source, initial) )  (x) =>
foldhood( pair(source, initial), min,
pair(nbrfst(x)+metric(), accumulate(nbrsnd(x))) )

def T(initial, zero, decay)
rep ( initial )  (x) => min(max(decay(x), zero), initial)

The G and T blocks (code reported from literature [56]).

The correspondence between   and  given by Theorem <ref>, although restricted to a fragment of the two languages, is applicable to many relevant aggregate programs, allowing for the automatic transfer of algorithms and properties proven in  to .
As a first paradigmatic example, consider the G and T blocks, proposed as part of a combinator basis able to express most aggregate systems [15]. The  formalisation of their code [56] is reported in <Ref>, and has the same behaviour in  since it actually belongs to /.

// previous round value of v
def older(v, null)
fst(rep (pair(null, null))  (old) => pair(snd(old), v) )

// gathers values from causal past events into a labelled DAG
def gather(node, dag)
let old = older(dag, dag_empty()) in
let next = dag_join(foldhood(old, dag_union, nbrdag), node) in
if (next == node)  dag   gather(node, dag_union(dag, next))

def f_field(e, v...)
f( gather(dag_node(e, v...), dag_node(e, v...)) )

The universal translation of distributed Turing Machines (code reported from literature [2]).

As a further example, consider the code in <Ref>, which is also in / and encodes the behaviour of any distributed Turing Machine (expressed as a function $\funvalue$ taking as input in every firing the whole collection of causally available data) as an  function. This code was used to prove Turing Universality for ,[A programming model for distributed systems is Turing-universal if and only if it is able to replicate the behaviour of any distributed Turing machine.] but in fact it also proves that / hence  are Turing-universal as well (assuming a sufficient collection of built-ins).

§.§.§ Refactoring of  programs into

Despite many common aggregate functions being in /, not every relevant such function belongs to this fragment. In particular, the restrictions imposed by the type system in Figure <ref> prohibit the common pattern of functions with field arguments, folding those arguments in their body. However, refactoring strategies exist that we can use in order to turn most  programs into  while preserving their behaviour, by converting a field argument of a function into a local argument, thus allowing its capture within $\foldK$ statements.

(1) Abstracting: a field argument of a function may be passed “by name” through

\[
( (\xname) \toSymK{ \e_1 } )(\e_2) \quad\longrightarrow\quad ( (\xname) \toSymK{ \applySubstitution{\e_1}{\substitution{\xname}{\xname()}} } )(() \toSymK{\e_2})
\]

This refactoring preserves the behaviour of a program, provided that either (i) the abstracted parameter does not depend on the current domain (e.g., relational sensors such as ), or (ii) the parameter does not occur within branches in the body of the function (so that the evaluation is performed in the function with respect to the same domain as in the argument). If instead it does occur within a branch and depends on the current domain, its deferred evaluation within the function body will generally produce a different result. For example, consider function  counting the number of neighbours in the current domain:
def counthood()  foldhood(0, +, 1)

and suppose that the argument is $\e_2 = \nbrK\{\mathtt{counthood}()\}$, and the function $\e_1$ is

\[
\ifK (\mathtt{temperature}() < 30) \{ 0 \} \{ \foldK(\mathtt{counthood}(), \max, \xname) \}.
\]

This functions returns 0 on “cold” devices; otherwise, it returns the maximum number of total neighbours that any of the hot neighbours has (a metric that may be used, e.g., to trigger an alarm). After the abstracting refactoring, this result changes slightly to the maximum number of hot neighbours that any of the hot neighbours has. This reduces the computed value, possibly reducing the effectiveness of the metric and delaying the triggering of the alarm. However, most programs with this characteristic can still be refactored, by resorting to the following extended refactoring whenever the domain dependency is due to sub-expressions of local type.

(2) Abstracting with parameters: a field argument $\e_2[\overline\e']$ where $\overline\e'$ have local type can be passed as a function with parameters through

\[
( (\xname) \toSymK{ \e_1 } )(\e_2[\overline\e']) \quad\longrightarrow\quad ( (\xname,\overline\yname) \toSymK{ \applySubstitution{\e_1}{\substitution{\xname}{\xname(\overline\yname)}} } )((\overline\yname) \toSymK{\e_2[\overline\yname]}, \overline\e')
\]

This refactoring can address the previous example, by leaving the $\mathtt{counthood}()$ sub-expression (which is the one depending on the current domain and has local type) as a parameter:

\begin{align*}
((\xname,\yname) \toSymK{\ifK (\mathtt{temperature}() < 30) \{ 0 \} \{ \foldK(\mathtt{counthood}(), \max, \xname(\yname)) \}}) \quad \\
((\yname) \toSymK{\nbrK\{\yname\}}, \mathtt{counthood}())
\end{align*}

Assume an  expression $\e$ consists in a function $(\xname) \toSymK{ \e_1 }$ called with a field argument $\e_2[\overline\e']$ where $\overline\e'$ all have local type, and consider the refactored expression $\e''$ as in (2). If the argument $\xname$ does not occur within branches in $\e_1$, then $\e''$ has the same behaviour as $\e$. If the result of $\e_2[\overline\yname]$, for any given values for $\overline\yname$ and for any domain of computation $\domof{\Trees}$, is a field value $\fvalue$ such that $\fvalue(\deviceId)$ does not depend on $\domof{\Trees}$ for any $\deviceId$, then $\e''$ has the same behaviour as $\e$.

First, notice that the semantics of  is compositional except for the set of aligned neighbours: in other words, the evaluation result of an expression depends on the enclosing expression only in the determination of the set of aligned neighbours; once that set is fixed, the result of the expression is fixed too. The effect of refactoring (2) is shifting the evaluation of $\e_2[\overline\e']$ in a different part of the evaluation tree: function call itself (by Rule [E-APP]) to several points in the function body (the occurrences of $\xname$).

If the evaluation of $\e_2[\overline\e']$ does not depend on the domain of evaluation, then this computation shift has no effect, concluding the proof for that case. If $\xname$ does not occur within branches, the set of aligned neighbours for each of its occurrences is the same as the set of aligned neighbours for the function call itself. It follows that the evaluation of $\e_2[\overline\e']$ in place of every occurrence of $\xname$ has to produce the same result as in the argument, concluding the proof.

The following simpler refactoring can address cases when the argument is a simple $\nbrK$-expression, regardless of branches in $\e_1$.

(3) Deferring: an $\nbrK$ in the argument may be transferred into the body as

\[
( (\xname)~\toSymK{ \e_1 } )(\nbrK\{\e_2\}) \quad\longrightarrow\quad ( (\xname)~\toSymK{ \applySubstitution{\e_1}{\substitution{\xname}{\nbrK\{\xname\}}} } )(\e_2)
\]

This refactoring is a simplification of refactoring (2), abstracting $\nbrK\{\e_2\}$ with respect to the parameter $\e_2$ of local type. In fact, refactoring (2) in this case would produce:

\[
( (\xname,\yname) \toSymK{ \applySubstitution{\e_1}{\substitution{\xname}{\xname(\yname)}} } )((\yname) \toSymK{\nbrK\{\yname\}}, \e_2)
\]

and inlining $(\yname) \toSymK{\nbrK\{\yname\}}$ into the occurrences of the first parameter $\xname$ yields exactly the result of refactoring (3).

Notice that the general refactoring (2) and its common special cases (1) and (3) cover practically any realistic situation. In order for neither of those to be applicable, we would need the argument $\e_2$ to be a field expression which depends on the current domain (and not only because of sub-expressions of local type), and which is passed into a function $\e_1$ folding it inside a branching statement: we are not aware of any meaningful or realistic situation meeting these requirements.

Thus, through these refactorings we can convert practically any  program into , hence into , although the resulting refactoring may be extensive: since the refactoring of a function depends on its call patterns, more than one version of a function may be needed to cover all of them. However, this is not an issue for a “native”  programmer, which would just interpret the above refactorings as programming patterns, following them from the start of application development. Interpreted as programming patterns, the above rules suggest deferring $\nbrK$ applications when possible, or using call-by-name instead of call-by-value on field arguments otherwise.

§.§.§ An example: refactoring the self-stabilising fragment of

A paradigmatic example of  programs that can be converted into  through the refactorings in <Ref> is the self-stabilising fragment [56]. We say that a time- and space-distributed data is stabilising iff it remains constant in every point after a certain time $t_0$, and its limit is the value assumed after $t_0$. We say that a distributed program is self-stabilising iff given stabilising inputs and topology, it produces a stabilising output which depends only on the limits of the inputs and topology (and not on the concrete scheduling of events, nor on the input values before stabilisation).

A subset of , called self-stabilising fragment, has been proved in the literature [56] to consist of self-stabilising programs only. This fragment makes use of functions folding field arguments, and thus is not part of  and cannot be directly translated into  preserving its behaviour (or self-stabilisation). However, the refactorings in <Ref> can be applied to obtain the equivalent fragment in Figure <ref> that does belong to /. The self-stabilising fragment combines syntactic requirements with mathematical requirements on functions, annotated in the figure through superscripts on function names.

$\mathsf{C}$ (Converging)
A function $\funvalue(\anyvalue_1, \anyvalue_2, \overline\anyvalue)$ is said converging iff, in every firing, its return value is closer to $\anyvalue_2$ than the maximal distance that the two arguments $\anyvalue_1$ and $\anyvalue_2$ have in any neighbour firing (according to any metric measuring that distance).

$\mathsf{M}$ (Monotonic non-decreasing)
A stateless[A function $\funvalue(\overline\xname)$ is stateless iff given fixed inputs $\overline\anyvalue$ always produces the same output, independently of the environment or specific firing event. In other words, its behaviour corresponds to that of a mathematical function.] function $\funvalue(\xname, \overline\xname)$ with arguments of local type is monotonic non-decreasing in its first argument iff whenever $\lvalue_1 \leq \lvalue_2$, also $\funvalue(\lvalue_1, \overline\lvalue) \leq \funvalue(\lvalue_2, \overline\lvalue)$.

$\mathsf{P}$ (Progressive)
A stateless function $\funvalue(\xname, \overline\xname)$ with local arguments is progressive in its first argument iff $\funvalue(\lvalue, \overline\lvalue) > \lvalue$ or $\funvalue(\lvalue, \overline\lvalue) = \top$ (where $\top$ is the maximal element of the relevant type).

$\mathsf{R}$ (Raising)
A function $\funvalue(\lvalue_1, \lvalue_2, \overline\anyvalue)$ is raising with respect to partial orders $<$, $\vartriangleleft$ iff:
(i) $\funvalue(\lvalue, \lvalue, \overline\anyvalue) = \lvalue$;
(ii) $\funvalue(\lvalue_1, \lvalue_2, \overline\anyvalue) \geq \min(\lvalue_1, \lvalue_2)$;
(iii) either $\funvalue(\lvalue_1, \lvalue_2, \overline\anyvalue) \vartriangleright \lvalue_2$ or $\funvalue(\lvalue_1, \lvalue_2, \overline\anyvalue) = \lvalue_1$.

\begin{array}{lcl@{\hspace{-15pt}}r}
\s & \BNFcce &  \xname \; \BNFmid \; \anyvalue  \; \BNFmid \; \letK \; \xname = \s \; \inK \; \s \; \BNFmid \; \funvalue(\overline\s) \; \BNFmid \; \ifK (\s) \{ \s \} \{ \s \} \; \BNFmid \; \nbrK\{\s\}
&   {\footnotesize \mbox{self-stabilising expression}} \\[3pt]
&&  \; \BNFmid \;  \repK(\e)\{ (\xname) \toSymK{\funvalue^\mathsf{C}(\xname, \s, \overline\e)} \}\\[3pt] % deferring nbrs to function body
&&  \; \BNFmid \;  \repK(\e)\{ (\xname) \toSymK{\funvalue((\yname,\zname) \toSymK{\muxK(\nbrK\{\yname\} < \yname, \nbrK\{\xname\}, \zname)}, \overline\s)} \}\\[3pt] % abstracting the mux expression
&&  \; \BNFmid \;\repK(\e)\{ (\xname) \toSymK{\funvalue^\mathsf{R}(\foldK(\s, \min, \funvalue^\mathsf{MP}(\nbrK\{\xname\}, \overline\s)), \xname, \overline\e)} \} % rewriting of minHoodLoc in terms of foldhood
\end{array}

Syntax of a self-stabilising fragment of field calculus expressions, where self-stabilising expressions $\s$ occurring inside a $\repK$ statement cannot contain free occurrences of the $\repK$-bound variable $\xname$.

Every self-stabilising expression according to the fragment in <Ref> is a self-stabilising  expression.

Notice that the fragment in <Ref> can be obtained from that in <cit.> by means of the following two refactorings.

* In the converging $\repK$ expression $\repK(\e)\{ (\xname) \toSymK{\funvalue^\mathsf{C}(\xname, \s, \overline\e)} \}$, deferring is applied to transfer $\nbrK$ in arguments to the body of the function $\funvalue^\mathsf{C}$, adapting the definition of converging function accordingly. By Theorem <ref>, these expressions have the same behaviour as those in <cit.>, which are self-stabilising by <cit.>.

* In the acyclic $\repK$ expression $\repK(\e)\{ (\xname) \toSymK{\funvalue((\yname,\zname) \toSymK{\muxK(\nbrK\{\yname\} < \yname, \nbrK\{\xname\}, \zname)}, \overline\s)} \}$, abstraction is applied to the first argument with respect to parameters $\yname, \zname$ (whose values are added into the additional parameters $\overline\s$ passed to $\funvalue$). By Theorem <ref>, these expressions have the same behaviour as those in <cit.>, which are self-stabilising by <cit.>.

The rest of the fragment is identical modulo inessential modifications (expansion of the $\nbrlt$ and $\texttt{minHoodLoc}$ functions into their definition), concluding the proof.

§.§.§  programs that cannot be straightforwardly expressed as  programs

As argued in [6], programs such as updatable metrics and combined Boolean restriction are not conveniently expressed in . In the former case, we can use the following general scheme for updatable functions, first proposed in [9]:
def up(injecter)
snd( rep(injecter())
(x) =>  foldhood(injecter(), max, nbrx)

where $\mathtt{injecter}$ is a function returning a pair $\langle \mathtt{version~number}, \mathtt{~function~code} \rangle$, and the built-in operator $\mathtt{max}$ selects the pair with the highest version number among its arguments. This procedure defines a perfectly reasonable “upgradeable function” by spreading functions with higher version number throughout devices. However, it is not allowed by the type system of  for functions returning fields, such as metrics (which usually have type $() \rightarrow \ftypeOf{\ntype}$).
This scheme can instead be used in  (as shown in Section <ref>), and works properly provided that new versions are injected at a slow rate, and an occasionally empty domain of a field-like expression does not produce critical effects.