Another situation where the permissive behaviour of  is crucial is that of combined Boolean restriction. In this setting, a field-like expression $\e$ needs to be restricted to those devices agreeing on the value of $n$ Boolean parameters $\bname_1, \ldots, \bname_n$, before being folded with $\foldK(\anyvalue, \funvalue, \e)$. This rather abstract example might be concretely instantiated, e.g., in case an aggregation needs to be executed separately on devices with different configurations. In , this effect can be achieved only by restricting on each of the $2^n$ possibilities for the parameters, as in the following.
if (b1        b2        ... bn) foldhood(v, f, e)
if (!b1        b2        ... bn) foldhood(v, f, e)
if (b1        !b2        ... bn) foldhood(v, f, e)  ...

However, such a program might be infeasibly large even for small values of $n$. On the other hand, in  the above program can be concisely rewritten as:
foldhood(v, f, e + if (b1) nbr0 nbr0 + if (b2) nbr0 nbr0 + ...)

whose size is linear in $n$.[In this code we assumed that $\xname$ has numerical type, but similar code can be obtained for any type by defining a binary operator which is the identity on its first argument.] The domain of the $i$-th 0-valued field-like subexpression above is equal to the set of devices agreeing on $\bname_i$, hence by intersecting all of them the resulting domain corresponds to the set of devices agreeing on each of the $n$ given parameters.

§ : AN IMPLEMENTATION OF THE

In this section,
we present ,
an implementation of  embedded in the Scala programming language.

While external (or standalone) domain-specific languages (DSLs)
have their own syntax and semantics,
internal DSLs are embedded into some other language [61].

Developing an internal DSL
brings major benefits in terms of reuse
of features, toolchain support, and familiarity with
the host language—at the expense of the syntactical and semantical constraints imposed by the host.

Scala has been chosen as the host language of
for its
its feature set (it provides mechanisms supporting the creation of expressive APIs and  DSLs [7])
its ability to target and reuse libraries from various execution platforms
(such as the JVM, but also Javascript through the ScalaJS project [34]).

With respect to other field calculi,
lends itself to smooth implementation in Scala,
as e.g. there are no neighbouring fields to be dealt with
at the typing, syntactical, and semantical level.

A Scala expression of type  is automatically interpreted in  as an aggregate program producing a field of , completely fulfilling the “everything is a field” view.

§.§ The Scala implementation of

The following interface, implemented as a Scala trait, represents the basic  constructs as methods:

trait Constructs
// Key constructs
def rep[A](init: => A)(fun: (A) => A): A
def foldhood[A](init: => A)(aggr: (A, A) => A)(expr: => A): A
def nbr[A](expr: => A): A
def aggregate[A](b: => A): A

// Abstract types
type ID;         // type of device identifiers
type LSNS, NSNS; // type of local and neighbour sensor names

// Contextual, but foundational
def mid(): ID
def sense[A](name: LSNS): A
def nbrvar[A](name: NSNS): A

In Scala, methods are introduced with the  keyword,
can be generic (with type parameters specified in square brackets),
may accept multiple parameter lists,
and specify a return type at the end of the signature (when this is not given the compiler attempts inference).

Function types may take the form , which is actually syntactic sugar over ;
curried function types can be written as  ( is right associative).

Tuple types may take the form , which is actually syntactic sugar over ;
similarly, a literal tuple value can be denoted as .

By-name parameters, denoted with type ,
capture expressions or blocks of code that are passed unevaluated to the method and are actually evaluated every time the parameter is used—they are basically syntactic sugar over 0-ary function types.

As a relevant note on syntax, especially useful in DSLs to render constructs with code blocks, unary parameter lists in a method can be called also with curly brackets instead of parentheses.

E.g., all the following are valid invocations for  method above: , , , .

Finally, nullary methods can be invoked without parentheses;
e.g.,  is a valid method call just like .

First of all, notice that the input and output types of the constructs (especially |nbr|) are proper, i.e., no field-like datatype appears in the signatures.

Then, compare trait |Construct| with the  syntax from <Ref>.

Beside the curried form of |rep| and |foldhood|, the only significant difference is an additional construct |aggregate| which is used to turn standard Scala functions/methods into field calculus functions, i.e., as units of alignment (refer to <Ref> for details).

We report here the encoding of $\ifK$, which is called |branch| in  due to the fact that |if| is a reserved keyword in Scala:

def branch[A](cond: => Boolean)(th: => A)(el: => A): A =
mux(cond)(() => aggregate th )(() => aggregate el )()

Namely, the |th|en and |el|se expressions are passed unevaluated (as by-named arguments) to |branch|, and there used in the bodies of two corresponding lambdas, wrapped with |aggregate| (which could be seen as a form of tagging).

The |mux| on |cond| is used to select one of those functions, which is then invoked straight on via operator |()|.

Moreover, it is crucial to note that
the programming patterns discussed in <Ref> (abstraction and deferring)
are supported
in a syntactically transparent way
thanks to the Scala support of by-name parameters.

Indeed, the refactoring shown in <Ref>
are automatically applied.

Finally, in practice, an aggregate program can be defined in
by extending class |AggregateProgram| and implementing a method called |main| which defines the main program expression.

This class provides an implementation of the |Constructs| trait: by subclassing it, the syntax and semantics of the  DSL is made available within the subclass definition, such that its objects could be used both for simulation purposes or to encapsulate the aggregate logic in actual distributed implementations.

class GradientProgram extends AggregateProgram
with Gradients        // brings gradient() in
with StandardSensors  // brings nbrRange() in

// Custom definitions
def isSource = sense[Boolean]("source")

// Main expression
def main(): (Int,Double) =
// Return a 2-element tuple (round count, gradient value)
(rep(0)(r=>r+1), gradient(isSource, nbrRange))

A full description of  is beyond the scope of this paper: the interested reader can refer to [26] for more details.

§.§ On pragmatics: neighbouring fields vs computation against a neighbour

In this section, we provide a hint to the practical issues that / solve, enabling easy implementations and a clean support for  aggregate programming.

Consider the  expression of the classic gradient algorithm (cf. <Ref>):

rep(Double.PositiveInfinity)  case d =>
mux(source)  0.0   minHood(nbr(d) + metric())

and focus on expression |nbr(d)+metric()|.

While in / the latter is a sum of two local values, computed against aligned neighbours (by the |*hood| operator), in the field calculus it would be a sum of two neighbouring fields.

While in a standalone DSL, implementations may transparently
lift local operators to work with fields (i.e., collection-like objects),
this would not typically be easy or even possible in internal DSLs.

Suppose a neighbouring field of |T|-typed objects is represented as an instance of type |Field[T]|.

In a purely functional world, two fields could be combined with a “classical” |map2| function:

map2(nbr(d), metric(), _+_)

However, this would introduce some clutter in aggregate programs
and require a versatile set of functional combinators.

In a powerful object-oriented language with mechanisms like extension methods (such as Scala or C#), it would be possibly to manually add specific operators to work with fields.
implicit class NumericField[T:Numeric](f: Field[T])
def +(f2: Field[T]): Field[T] = map2(f, f2, implicitly[Numeric[T]].plus(_,_))
// ...

// Assuming nbr(d) has type Field[Double]
nbr(d) + metric // possible by Scala's implicits (cf.

This example leverages Scala's pimp-my-library idiom [47], which uses implicits to enable automatic, compile-time conversion of a |Field| of |Numeric|s to a |NumericField| that could accept a method |+|.

However, the lifting of local operators to fields would be manual, and not automatic—introducing a overhead on library development.

Some language could provide advanced features to mitigate this issue (e.g., through powerful compile-time macro mechanisms), but in this case we would pose severe constraints on the host language for the internal DSL, hence limiting the development environment where aggregate programming could be supported.

§ CASE STUDY

The goal of this section is to show how /
can be used to eloquently express collective behaviour.

More specifically, the goal is not to show that /
necessarily provide a better programming support with respect to e.g. /Protelis—though the Scala embedding does provide various practical benefits, through reuse of Scala's powerful type system and features.

Indeed, the benefit of  lies in a conceptual frugality
(by avoiding the “neighbouring field” notion)
that leads to a different computational model (cf., <Ref>)
with easier DSL embeddability in mainstream programming languages (cf. <Ref>).

Therefore, this section shows that such a model and implementation can be used to smoothly program increasingly complex field coordination-based systems.

In particular, we apply the programming model to the context of

edge computing [51]
and ad-hoc cloudlets [19] (introduced in <Ref>).

Evaluation of correctness of the proposed solution is performed by simulation.
The source code, configuration files, and instructions for launching the experiments and reproducing the presented results is publicly available at an online repository[<https://github.com/metaphori/experiments-neighbours-calculus>.].

§.§ Ad-hoc Edge Computing Support

Edge computing [51]
is a recent paradigm that aims to bring
cloud-like functionality (e.g., virtualisation, elastic provisioning of resources, and “anything-as-a-service”) closer to end devices
at the edge of the network.
Its goal is to ultimately improve the Quality of Service (QoS) of situated systems as in the IoT,
e.g., through reduction of communication latencies, bandwidth and energy consumption,
essentially achieved by shortening the round-trip path of data to/from elastic resource pools.

In this case study for , we focus on ad-hoc edge computing—i.e.,
a decentralised form of edge computing
that does not rely on pre-existing infrastructure
but is rather supported by a large-scale network of devices
logically interacting in a peer-to-peer fashion.

This may also be a first step for merging volunteer computing [35] and edge computing into
a form of volunteer edge computing
where devices with spare resources make them available (possibly
by incentives) to nearby users.

We assume to operate in a region of a smart city
where hundreds of devices willing to offer resources
run the aggregate computing middleware
and may hence participate in the Aggregate Edge Computing (AEC) application.
In a vision of smart city operating systems,
it is indeed sensible to assume that devices willing to fully benefit from smart city services
are asked to give their “social contribution” by participating in the system as well, where, of course, we also assume proper security and privacy systems are in place.

The system is open, in the sense that devices may
enter or leave the system as they like.
For this paper we abstract from the way in which tasks are assigned to devices.

The goal of AEC is to support a self-organisation process
to monitor resource availability and usage (i.e., load) in the system,
and spread information as well as directives
which can be exploited by devices for decentralised control activities
and by users for determining advantageous deployment options.

The idea is to provide support for edge computing by leveraging
the space-time distribution of resources.
Managing edge resources in a collective, space-time-oriented fashion
is meant to provide the following benefits:
(i) it makes straightforward to exploit the locality principles that often sustain IoT, CPS, and smart city applications,
(ii) it allows us to assume that devices are only able to communicate with other nearby devices through short-range wireless technologies (e.g., $10$ to $100$ meters range);
(iii) it allows us to relate the spatio-temporal distribution of resources
with human social activity;
(iv) it provides a natural way to handle collective metrics
and take into account contextual data and constraints at multiple scales.

§.§ Model and Design

We model devices of the AEC system as self-aware, situated entities
that can sense
the resources they own (e.g., number of CPUs, memory, and storage)
and their current levels of utilisation.

def getLocalProcessing() = sense[ProcessingStat]("processing")
def getLocalStorage() = sense[StorageStat]("storage")
// ...
def getLocalResources() = LocalStats(getLocalProcessing, getLocalStorage, ...)

Data can be easily modelled in Scala with case classes (i.e., algebraic data types with built-in equality, pattern matching support, etc.).

// Just for simplcity of exposition, CPUs are not shared.
case class ProcessingStat(numCPUs: Int = 0, mHz: Int = 0, numCPUsInUse: Int = 0)

trait DiskType; case object HDD extends DiskType; case object SSD extends DiskType
case class StorageStat(MiBs: Int = 0, dtype: DiskType = HDD, MiBsInUse: Int = 0)

case class LocalStats(ps: ProcessingStat, ss: StorageStat, ...)

We also assume the devices can communicate with other devices
in their vicinity—i.e., the neighbouring relationship is basically spatial.

To divide the complexity of the resource monitoring task,
we split the whole environment
into manageable areas (which may also be called cloudlets)
that can be monitored and controlled more easily.

In order to solve issues related to distributed consensus,
we want the system to resiliently self-organise to elect a leader in each area,
so as to provide consistent views of the state of areas
as well as enacting global decisions for an area.

That is, the leaders effectively act as decentralised management points
which are responsible for orchestrating a subset of devices in the system—so, in a sense, we apply a hybrid approach that combines
orchestration and choreography as suggested in [55].

In practice, leaders act as sinks of contributions from the devices of the
corresponding area, and as propagators of area-wide context information
back to its feeders;
but, in order to implement such a process,
we need mechanisms for resiliently streaming information
across dynamic space-time regions.

The following section shows library functions that can be used
to streamline the implementation of aforementioned mechanisms.

§.§ Building Blocks

Implementing the above ideas requires a careful crafting of the aggregate specification.

There is need of identifying some recurrent patterns
(e.g., peer-to-peer propagation of information in- and out-ward an area)
that may come handy in many situations.

They can then be used to raise the abstraction level
through a reusable API that hides low-level detail (e.g. the interplay of  and )
only exposing the functional contract
expressing the relationship between input fields and output fields.

In doing so, we progressively move from a device-centric view
(i.e., local sensing and neighbour-oriented communication)
to an aggregate view (i.e., collective behaviour and data)
of the system, regaining declarativity and intent.

In this case study,
we leverage the following building blocks,
which are available in the  standard library.

case class Gradient(algorithm: (Boolean,()=>Double)=>Double,
source: Boolean, metric: () => Double)
def G[V](gradient: Gradient, field: V, acc: V => V): V
def C[P: Bounded, V](potential: P, acc: (V, V) => V, local: V, Null: V): V
def S(grain: Double, metric: () => Double): Boolean

Their implementation is already described in other papers [14, 56]
so here we present them by a functional perspective
and just provide some insight about how they could work internally.

Recall the notion of gradient from <Ref>:
a field computation that,
from a Boolean field denoting a region,
returns the field of minimum distances from that region.

The gradient field is key in spatial computations
because it provides a direction from any point to a target:
by descending (or ascending, resp.) the gradient field, i.e.,
by following the minimum (or maximum, resp.) values locally observed,
one moves close (or away, resp.) to a certain target.

With case class , we package together the algorithm
and input fields—e.g., it may be useful to ensure that both a particular gradient
and another function using it adopt the same metric.

The gradient-cast operator, also known as , is a generalised form of the gradient computation
that accumulates values through a function
along a gradient field, starting with the given
at sources and new devices.

So, functionally  maps a source field and a field of values
to a field whose values are progressively transformed, distance-wise,
from source values.

For instance, a gradient field can be constructed via  as follows.

val src = sense[Boolean]("source")
val classicGradient = Gradient(gradient(_,_), src, nbrRange)
G[Double](classicGradient, mux(src) 0  inf , _+classicGradient.metric())

With , it is also trivial to define a  function for propagating
information outward from a source, by ascending the potential field.

def broadcast[V](source: Boolean, field: V): V =
G[V](classicGradient, field, (v: V) => v)

A change of  where  is true
basically generates a new wave
in this continuous streaming of information.

Notice that  has a value everywhere
but only the value of the  is selected
and then identically preserved in the propagation.

Also, notice that both  and  may
admit a different signature where the “potential field”
is given as input and not calculated internally.

Dual to the gradient-cast operator is the converge-cast operator,
also known as :
indeed, the conceptually inverse notion of a propagation from a point outward
is a propagation inward, from the edge towards a point.

umulates a  field
along some  field
(yielding  if no direction to descend can be found),
where the final results of the accumulation
end up collected at points of zero potential.

In the signature above, we show that we may abstract from the concrete
type  of the potential field (which is usually a ),
provided that there exists an ordering over  values—as
enforced by the context bound constraint  (which is the mechanism
for the typeclass idiom in Scala [47], where the method may be called provided
an implicit instance of type  can be statically resolved).

It is also worth pointing out that both  and
are self-stabilising operators,
whose compositions are also self-stabilising [56] (see the discussion in <Ref>);
hence, there are formal guarantees that programs built using only
self-stabilising constructs like  and
will eventually reach a fixpoint once inputs stop changing.

The last fundamental building block that we cover is the sparse-choice operator, also known as ,
which yields a Boolean field holding
in correspondence of elected nodes (also called leaders)
which are selected in a manner such that adjacent leaders
are at about distance .

In practice, it performs a leader election process
which also results in a split of the space
into areas of a diameter which is approximately ,
since any connected device will be at a distance at most
from a leader (think of a gradient from the leader field).

Internally, an implementation of
may work by performing a distance competition among devices:
initially, every device will propose itself as a leader,
but initially assigned random values (ultimately discriminated by device IDs in case of breakeven) will be used to break symmetry (e.g., by selecting the minimum);
if the gradient from the currently selected leader is larger than
at a device, then it will start another competition for leadership of another area.

§.§.§ Upgradeable functions

The case study also uses the notion of upgradeable function

explained in <Ref>.

The idea is to support hot upgrades of application algorithms
by allowing injection of versioned functions at some device of the system
and then spreading such novel versions through a gossiping process
that eventually settles everywhere the function of the higher version.

Concretely, we model versioned functions and injectors as types of the form

case class Fun[R](ver: Int, fun: ()=>R)
type Injecter[R] = () => Fun[R]

and define a function ,
def up[R](injecter: Injecter[R]): Fun[R] = rep(injecter()) f =>
foldhood(injecter())((f1,f2) => if(f1.ver>f2.ver) f1 else f2)(nbrf)

to handle the upgrade process
through corresponding propagation and selection of functions.

§.§ Implementation

Considering the modelling and library functions
covered in previous sections,
the core specification of the case study can be expressed
as in the following  program.

class AdhocCloud extends AggregateProgram
with StandardSensors with BlockG with BlockC with FieldUtils

val grain = 150 // parameter: mean distance between leaders

def main =
// Get a metric for S, dynamically
var Smetric = up[Double](metricInjecter(k)).fun
// Resilient leader election
val leaders = S(grain, Smetric)
// Use the standard neighbouring range metric for the other operations
val metric = nbrRange
// Potential field to leaders
val potential = gradient(leaders, metric)
// Query local resources
val localResources = getLocalResources()
// Collect resources information towards leaders
val resourcesPerArea =
C[Double,Stats](potential, _++_, Map(mid->localResources), Map())
// Broadcast from leaders outwards aggregated statistics
val allResourcesInArea = broadcast(potential, metric,
// ...

The flow is simple and reasoning is simplified by the
collective stance and compositionality of Aggregate Computing:
we use  to split the system into cloudlets
monitored by corresponding leaders
(where the metric used to create the areas can be dynamically updated);
we build a gradient from leaders to set the pathways for collecting
data into leaders and propagating the determinations of leaders to their workers;
and finally, we use those pathways to stream
the cloudlet-wise estimation of resource availability and usage to all the members.

By the way, notice that this resource monitoring example represents the application of a more general pattern [24] that finds application in other large-scale, distributed coordination scenarios such as for situated problem solving [25] and client/server task allocation [27].

§.§ Evaluation: Correctness

[Initial metric.]

[Updated metric.]
A visual representation of the scenario, with two snapshots taken before and after a hot update of the metric.
The big red squares represent leader nodes. Superimposed with any leader is a semi-transparent blue ball whose intensity is proportional to the amount of resources available in the corresponding area. Other nodes have a colour representing the gradient field towards leaders (warmer, red-like colours for nodes close to the leader, and colder, green-like colours for peripheral nodes).
The updated metric in (b) provides an overestimation of distances which results
in smaller areas or, equivalently, in more cloudlets (and leaders).

These graphs show the load estimation capability at leader nodes,
for different round-wise probabilities of leader failure (leading to a disproportionate  number of failures ($150$ to $250$) in the considered timespan). The plots are obtained by taking the mean of $30$ runs with different random seeds.
The scenario is modelled as follows: the spikes of high load start at time $t=200$ and $t=500$, the new metric is injected at time $t=450$, and we can observe that,
after such upgrade, the system is able to perform a much more precise estimation of CPU usage.

The system has been simulated in the Alchemist simulator [49, 23]—a graphical snapshot is given by <Ref>[Full-size colour pictures are available at the provided repository.],
whereas <Ref> provides empirical evidence of its correctness.
The simulated system consists of $400$ devices, each with a random amount of resources,
dispersed unevenly around the downtown of Cesena, Italy. Mobility is not considered.
A certain level of load is simulated in the system,
and we perturb it with spikes of high load.
The goal of the system is to reactively adjust the estimate of the load.
As for additional perturbations,
we also introduce a probability for temporary failure of leaders.
Finally, in order to show the positive impact of updatable metrics,
we inject a new metric to fine tune the dimension of areas at runtime—other aspects of configuration can be examined in the repository.

§ RELATED WORK

Scenarios like the IoT, CPS, smart cities, and the like,
foster a vision of rich computational ecosystems
providing services by leveraging strict cooperation of large collectives of smart devices, which mostly operate in a contextual way.

Engineering complex behaviour in these settings calls for approaches (from formal languages to execution platforms) providing some abstraction of the notion of ensemble, neglecting as much as possible the more traditional view of focussing on the single device and the messages it exchanges with peers.

Several works developed in different research communities share this attempt, often using different terminology, witnessed by various surveys, focussing on organisation of aggregates of devices
[12, 57], on developing frameworks for general-purpose self-organisation [40], addressing the issue of autonomic communication [30], and so on.

By factoring out common ideas from these works, and neglecting the diversity in lower-level concepts, one can identify families of approaches which have relations with the programming framework developed in this paper.

So, whereas the main related work is deeply covered in <Ref>,
in the following we comprehensively describe the research area in which our contribution can be positioned.

§.§.§ Device abstraction

A first family is that of languages providing some form of abstraction over device behaviour and interaction.

TOTA [43] and SAPERE [64] define platforms for pervasive computing focussing on agent coordination, where agents indirectly interact by injecting/perceiving “tuples” equipped with diffusion and aggregation behaviour (Java-defined in TOTA, declaratively specified by rules in SAPERE), and resulting in “fields of tuples” spread over the network; such works provide archetypal approaches to create computational fields that were an inspiration for Aggregate Computing and /—though, differently from them, we provide an expressive language to better control the shape and dynamics of fields over time.

Hood [62] defines data types to model an agent's neighbourhood and attributes, with operations to read/modify such attributes across neighbours, and a platform optimising execution of such operations by proper caching techniques;  provides a comparable neighbourhood abstraction, in that operator  is essentially used to declaratively access the set of neighbours as well as to combine observation of neighbours' attributes (indicated by the expression passed as argument) with modification of the same attribute locally.

Finally, works such as SCEL [31, 5] and ActorSpace [17] rely on so-called attribute-based communication, where each actor/agent exposes a list of attributes, and communication can be directed to the group of actors whose attribute match a given pattern;  can achieve a similar expressiveness with construct , by which one can define subcomputations carried on by a subset  of nodes, which are those that execute the same branch and hence remain actually “observable” by operator .

Generally speaking, it is worth noting that Aggregate Computing and / address the key feature of fitting useful device abstractions (such as neighbourhood, message exchange, attribute-based filtering) into a purely functional approach, which can then smoothly interoperate with more traditional programming frameworks and languages.

§.§.§ Geometric/topological abstractions
Another class of related approaches falls under the umbrella of languages to express geometric constructs and topological patterns. In fact, in several application contexts concerning environment sensing and controlling, what is key is the physical (geometric, topological) shape that coalitions of mobile agents take, or that certain data items create while diffusing in the environment. In the Growing Point Language [21], an amorphous medium [13] (essentially defined by an ad-hoc network) can be programmed by a nature-inspired approach of “botanical computing”, where computational processes are seen as “growing points” increasingly expanding across neighbours until reaching a fixpoint shape defined by declarative constraints; / and Aggregate Programming work on similar hypothesis on structure and behaviour of the underlying network, though adopting a different functional paradigm that is more expressive as it can address dynamical aspects as well, and which could be used as a lower-level language to reproduce the expressiveness of the growing point abstraction. The Origami Shape Language defined in [44] is used to achieve similar goals of the Growing Point Language though focussing on programming a “computational surface”, intended as a set of small devices working independently of their density in the surface: this language defines geometrical constructs to create basic regions and compose them, which could be turned into an API of / blocks to be functionally composed to achieve similar complex geometrical structures. In general, due to the universal character of field computations [2], one could consider / as a viable implementation framework for a number of approaches to organise the shape of computational entities in a physical environment, with the additional byproduct of leveraging the theory of field computations to assess formal validity of certain properties, such as density independence as developed in [16] or self-stabilisation in [56].

§.§.§ WSN-based discovery and streaming
A number of works originating in the context of information systems for sensor networks, such as TinyDB [42], Regiment [46], and Cougar [63], address the problem of gathering information extracted from sensors in a given region of space, aggregating them somehow, and redirecting results over the devices in another region. They either focus on spatial query languages (Cougar), diffusion/aggregation policies (TinyDB) or functional models to express and manipulate streams of events (Regiment). Similar approaches for mobile ad-hoc networks (MANET) have been considered that do not use data-oriented techniques but rather focus on services: SpatialViews [45] works by abstracting a MANET into spatial views that can be iterated on to visit nodes and request services; AmbientTalk [59] is another language for MANETs that provides resilience against transient network partitions by automatically buffering sent messages. A clear advantage of functional-based field computations as supported in / is that the various bricks of information collection, aggregation, diffusion, can be defined with the same language, wrapped in homogeneous components represented by / functions, and composed to create more complex applications as exemplified in Section <ref>, while leveraging the discovery of nearby services through an actor-based runtime.

§.§.§ Distributed/parallel computing
Aggregate Computing and its incarnation in  can evidently be considered as a declarative model for distributed programming, relying on abstractions and assumptions to make it easy to express certain kinds of programs by delegating important features (e.g., synthesising the concrete execution plan) to an underlying platform. As a notable example, we can draw a bridge with big data processing frameworks like MapReduce [32] and its derivation Apache Spark [65]: they essentially provide a highly declarative language of stream processing (based on simple map, reduce, filter and fold operations) and delegate to the underlying platform the duty of breaking tasks into smaller chunks to be allocated by the available computational/storage resources. An approach which is execution-wise technically more similar to the one developed in this paper is given by Bulk-Synchronous Parallel (BSP)-inspired frameworks, such as the large-scale graph processing framework Apache Giraph [53], which defines computations in terms of transformation of large graphs of data, typically stored in a distributed database.

In this respect, / can be seen as relying on a similar approach to achieve a more complex goal, namely, that of declaratively specifying a dynamic collective behaviour (based on distributed field computation), ultimately digesting information coming from distributed sensors and producing instructions for actuators, in such a way so as to make it breakable into smaller pieces (single rounds of computations) allocated to each device in the network.

§.§.§ Service choreographies
Choreographies [48] are an approach to service composition
where the interaction protocol of collaborative workflows is specified by a global viewpoint.
So, they define the cooperative contract of multiple parties
playing certain roles and collaborating to achieve a global goal.

There are strong similarities with Aggregate Computing; indeed, aggregate programs
(i) globally define the interactions supporting a collective computation, cf. the  construct;
(ii) define services which are fundamentally collaborative in nature;
and (iii) define roles for devices implicitly by the set of (sub-)computations executed by them or, equivalently, by the set of domain branches that they select in the collective workflow.

By contrast, however, while classical choreographies usually express goal-oriented workflows where the roles are few and statically assigned to parties,
aggregate computations typically carry on continuous processes
where devices repeatedly participate in the collective service
and can also play different roles across time depending on the context.
Additionally, choreographies abstract from the particular services carried on by the involved parties,
focussing instead only on when and what messages are exchanged,
whereas aggregate programs specify computations,
which are collective and yield global results represented as fields.
Moreover, interaction in field computations is only possible (by alignment)
between entities playing the same (sub-)computation,
and is neighbour-driven (rather than peer-to-peer and role-driven).
Finally, choreographies and choreographic programming [41]
mainly focus on checking conformance or building correct-by-construction concurrent programs (e.g., deadlock-free), but do little for functional composability of adaptive behaviours, which is instead the core of Aggregate Computing.

§.§.§ Spatial computing languages

Aggregate Computing directly descends from the class of so-called general-purpose spatial computing languages, all addressing the problem of engineering distributed (or parallel) computing by providing mechanisms to manipulate data structures diffused in space and evolving in time. Notable examples include the StarLisp approach for parallel computing [39], the SDEF programming system inspired by systolic computing [36], and topological computing with MGS [37]. They typically provide specific abstractions that significantly differ from that of computational fields: for instance, MGS defines computations over manifolds, the goal of which is to alter the manifold itself as a way to represent input-output transformation.

Specific programming languages to work with computational fields have been introduced as well, with the Proto [10] programming language as common ancestor, and  [50] as its Java-oriented DSL version.

The field calculus, deeply described and compared to in Section <ref>, has been designed as common core calculus for such languages, and for studying behavioural properties and semantic aspects [16, 56, 9]. Though rather similar to those languages,
evolved in a different way: its design is profoundly influenced by the need of smoothly integrating field computations in the syntactic, semantic, and typing structures of modern, conventional languages (like Scala—see <Ref>), and this required key semantic changes that motivated a more general and expressive calculus, as presented in this paper.

§ CONCLUSIONS

Aggregate Computing is a recent paradigm
for “holistically” engineering CASs and
smart situated ecosystems,
that aims to exploit, both functionally
and operationally, the increasing computational capabilities of
our environments—as fostered by driver scenarios like IoT, CPS, and smart cities.

It formally builds on computational fields and corresponding calculi
to functionally compose macro behavioural specifications
that capture, in a declarative way, the adaptive logic for
turning local activity into global, resilient behaviour.

In order to promote conceptual frugality and foster smooth embedding of this programming model in mainstream languages,
we propose a field calculus variant, called ,
which substitutes the notion of a “neighbouring field”
with a novel notion of a “computation against a neighbour”.

We formalise  and thoroughly compare to the higher-order field calculus (HFC),
stressing differences in expressiveness
and identifying a common fragment
allowing straightforward transfer of interesting properties
such as self-stabilisation.

To witness the benefits of the novel calculus, we cover the  aggregate programming language, which implements  as a DSL embedded in Scala.

Finally, we use a simulated case study in edge computing
to show that / are effectively expressive in practice.

The availability of a Scala-based implementation of field computations naturally suggests a number of future works.

From the linguistic viewpoint, it is interesting the study the interplay of field programs with advanced functional programming techniques, like the use of monads to structure the specification of increasingly complex field computations and field processes [28, 29], or the use of implicit parameters to define common contexts for library functions, there included the ability of dynamically select the most proper implementation of building blocks for the application at hand [56].

At the  platform level, instead, we plan to deeply investigate and implement techniques for infrastructure- and QoS-aware
adaptation of deployment and execution strategies for aggregate system execution, along the lines of [22].

This is to determine suitable application partitioning schemas and build a monitoring and control plan to effectively carry out configuration transitions.

The case study we discussed in the paper also suggests the importance of collective, self-adaptive/self-organising techniques
for (decentralised) edge computing and volunteer computing in ad-hoc cloudlets.

In particular, a question relates to how much such edge computing systems
need orchestration, what benefits and challenges
can emerge from a hybrid approach that brings self-organising processes in,
and how aggregate techniques allows us to tackle such integration of paradigms.

§  OPERATIONAL DEVICE SEMANTICS

We now present the  operational device semantics, modelling computation of a device within one round, as developed in literature [9] and reported in <Ref>. The network semantics of  is not reported, since it is the same as that of  (cf. <Ref>). The  device semantics is based on value-trees and value-tree environments, as that of . The syntax of them, together with the auxiliary functions and syntactic shorthands, are not reported here since they are the same as in  (cf. <Ref>). The derived judgements are slightly different, and follow the form $\bsopsem{\deviceId}{\Trees}{\senstate}{\e}{\vtree}$, to be read “expression $\e$ evaluates to  value-tree $\vtree$ on device $\deviceId$  with respect to the value-tree environment $\Trees$ and sensor state $\senstate$”.

[1]
%%%  EVALUATION RULES
%\textbf{Rules for expression evaluation:} \hspace{5.7cm} %\hfill
%  \boxed{\bsopsem{\deviceId}{\Trees}{{\senstate}}{\e}{\vtree}}
\begin{array}{c}
\nullsurfaceTyping{E-LOC}{
\bsopsem{\deviceId}{\Trees}{{\senstate}}{\lvalue}{\mkvtree{E-LOC}{\lvalue}{}}
\qquad\qquad
\surfaceTyping{E-FLD}{\qquad \fvalue' = \proj{\fvalue}{\domof{\Trees}\cup\{\deviceId\}}}{
\bsopsem{\deviceId}{\Trees}{{\senstate}}{\fvalue}{\mkvtree{E-FLD}{\fvalue'}{}}
\skiptransition\\[-3pt]
\surfaceTyping{E-B-APP}{\quad
\begin{array}{ll}
\bsopsem{\deviceId}{\piIof{1}{\Trees}}{\senstate}{\e}{\vtree}
\bsopsem{\deviceId}{\piIof{i+1}{\Trees}}{\senstate}{\e_i}{\vtree_i}  \quad \text{for all}\; i \in 1, \ldots, n
\\
\bname = \vrootOf{\vtree}
\anyvalue=\builtinop{{\bname}}{\deviceId}{\Trees{,\senstate}}(\vrootOf{\overline{\vtree}})
\end{array}
\bsopsem{\deviceId}{\Trees}{{\senstate}}{\e(\overline{\e})}{\mkvtree{E-B-APP}{\anyvalue}{\vtree,\overline{\vtree},\anyvalue}}
\skiptransition\\
\surfaceTyping{E-D-APP}{ \quad
\begin{array}{ll}
\bsopsem{\deviceId}{\piIof{1}{\Trees}}{\senstate}{\e}{\vtree}
\bsopsem{\deviceId}{\piIof{i+1}{\Trees}}{\senstate}{\e_i}{\vtree_i}  \quad \text{for all}\; i \in 1, \ldots, n
\\
\funvalue = \vrootOf{\vtree} {\text{ is not a built-in}}
\bsopsem{\deviceId}{\piBof{\funvalue}{\Trees}}{{\senstate}}{\applySubstitution{\body{\funvalue}}{\substitution{\args{\funvalue}}{\vrootOf{\overline{\vtree}}}}}{\vtree'}
\end{array}
\bsopsem{\deviceId}{\Trees}{{\senstate}}{\e(\overline{\e})}{\mkvtree{E-D-APP}{\vrootOf{\vtree'}}{\vtree,\overline{\vtree},\vtree'}}
\skiptransition\\
\surfaceTyping{E-NBR}{
\qquad
\Trees_1=\piIof{1}{\Trees}
\qquad
\bsopsem{\deviceId}{\Trees_1}{{\senstate}}{\e}{\vtree_1}
\qquad
\fvalue=\mapupdate{\vrootOf{\Trees_{1}}}{\envmap{\deviceId}{\vrootOf{\vtree_1}}}
\bsopsem{\deviceId}{\Trees}{{\senstate}}{\nbrK\{\e\}}{\mkvtree{E-NBR}{\fvalue}{\vtree_1}}
\skiptransition\\
\surfaceTyping{E-REP}{
\begin{array}{ll}
\bsopsem{\deviceId}{\piIof{1}{\Trees}}{{\senstate}}{\e_1}{\vtree_1} & \lvalue_1=\vrootOf{\vtree_{1}}\\
\bsopsem{\deviceId}{\piIof{2}{\Trees}}{{\senstate}}{\applySubstitution{\e_2}{\substitution{\xname}{\lvalue_0}}}{\vtree_2}~~& \lvalue_2=\vrootOf{\vtree_{2}}
\end{array}
\quad
\lvalue_0 = \left\{\begin{array}{lc}
\vrootOf{\piIof{2}{\Trees}}(\deviceId) & \mbox{if} \;  \deviceId \in \domof{\Trees} \\
\lvalue_1 & \mbox{otherwise}
\end{array}\right.
\!\!\!\!
\bsopsem{\deviceId}{\Trees}{{\senstate}}{\repK(\e_1)\{(\xname) \; \toSymK{\e_2}\}}{\mkvtree{E-REP}{\lvalue_2}{\vtree_1,\vtree_2}}
\end{array}
\end{array}$

Big-step rules for  expression evaluation.

Rules [E-LOC] and [E-FLD] model the evaluation of expressions that are either a local value or a neighbouring field value, respectively. For instance, evaluating the expression $\mathtt{1}$ produces (by rule  [E-LOC]) the value-tree $\mkvtree{E-LOC}{1}{}$, while evaluating the expression $\mathtt{+}$ produces the value-tree $\mkvtree{E-LOC}{+}{}$. Note that, in order to ensure that domain alignment is obeyed, rule [E-FLD] restricts the domain of the neighbouring field value $\fvalue$ to the domain of $\Trees$ augmented by $\deviceId$.

Rule [E-B-APP] models the application of built-in functions. It is used to evaluate expressions of the form $\e(\e_1 \cdots \e_n)$ such that the evaluation of $\e$ produces a value-tree $\vtree$ whose root $\rho(\vtree)$ is a built-in function $\bname$. It produces the value-tree $\mkvtree{E-B-APP}{\anyvalue}{\vtree,\vtree_{1},\ldots,\vtree_{n},\anyvalue}$, where  $\vtree_{1},\ldots,\vtree_{n}$ are the value-trees produced by the evaluation of the actual parameters $\e_{1},\ldots,\e_{n}$ ($n\ge 0$) and $\anyvalue$ is the value returned by the function.

Rule [E-B-APP]  exploits the special auxiliary function $\builtinop{\bname}{\deviceId}{\Trees, \senstate}$, whose actual definition is abstracted away, in order to allow for customised sets of built-in functions. This auxiliary function is such that $\builtinop{\bname}{\deviceId}{\Trees, \senstate}(\overline\anyvalue)$ computes the result of applying built-in function $\bname$ to values $\overline\anyvalue$ in the current environment and sensor state of device $\deviceId$. We require that $\builtinop{\bname}{\deviceId}{\Trees, \senstate}(\overline\anyvalue)$ always yields values of the expected type $\type$ where $\bname$ has a suitable type $(\overline{\type}) \to \type$.

Rule [E-D-APP] models the application of user-defined or anonymous functions, i.e., it is used to evaluate expressions of the form $\e(\e_1 \cdots \e_n)$ such that the evaluation of $\e$ produces a value-tree $\vtree$ whose root  $\funvalue=\vrootOf{\vtree}$ is a user-defined function name or an anonymous function value.
It is similar to rule [E-B-APP], except for the last subtree $\vtree'$ of the result, which is produced by evaluating the body of the function $\funvalue$ with respect to the value-tree environment $\piBof{{\funvalue}}{\Trees}$ containing only the value-trees associated to the evaluation of functions with the same name as $\funvalue$.

The evaluation of rule [E-REP] depends on whether it is performed against a tree environment with or without $\deviceId$ in its domain. If it is present, $\lvalue_0$ is obtained from it (being the previously computed value for the $\repK$ construct), otherwise it is set to the result of $\e_1$. The evaluation concludes substituting $\lvalue_0$ for $\xname$ in the body of $\e_2$. Notice that this substitution corresponds to the result of applying $(\xname) \toSymK{\e_2}(\lvalue_0)$ according to rule [E-D-APP] (skipping some branches of the resulting value-tree).

Value-trees also support modelling information exchange through the $\nbrK$ construct, as of rule [E-NBR].
In this rule, the neighbours' values for $\e$ are extracted into a neighbouring field value as $\fvalue = \vrootOf{\Trees_1}$. Then $\fvalue(\deviceId)$ is updated to the more recent value $\lvalue = \vrootOf{\vtree_1}$, as represented by the notation $\mapupdate{\fvalue}{\envmap{\deviceId}{\lvalue}}$.

[1]
Giorgio Audrito, Jacob Beal, Ferruccio Damiani, Danilo Pianini, and Mirko
Field-based coordination with the share operator.
Logical Methods in Computer Science, 16(4), 2020.

[2]
Giorgio Audrito, Jacob Beal, Ferruccio Damiani, and Mirko Viroli.
Space-time universality of field calculus.
In Giovanna Di Marzo Serugendo and Michele Loreti, editors, Coordination Models and Languages, volume 10852 of Lecture Notes in
Computer Science, pages 1–20. Springer, 2018.

[3]
Stuart Anderson, Nicolas Bredeche, A.E. Eiben, George Kampis, and Maarten van
Adaptive collective systems: herding black sheep.

[4]
Giorgio Audrito, Roberto Casadei, Ferruccio Damiani, and Mirko Viroli.
Compositional blocks for optimal self-healing gradients.
In 11th IEEE International Conference on Self-Adaptive and
Self-Organizing Systems, SASO 2017, Tucson, AZ, USA, September 18-22,
2017, pages 91–100. IEEE Computer Society, 2017.

[5]
Yehia Abd Alrahman, Rocco De Nicola, and Michele Loreti.
Programming of cas systems by relying on attribute-based
In International Symposium on Leveraging Applications of Formal
Methods, pages 539–553. Springer, 2016.

[6]
Giorgio Audrito, Ferruccio Damiani, Mirko Viroli, and Roberto Casadei.
Run-time management of computation domains in field calculus.
In Foundations and Applications of Self* Systems, IEEE
International Workshops on, pages 192–197. IEEE, 2016.

[7]
Cyrille Artho, Klaus Havelund, Rahul Kumar, and Yoriyuki Yamagata.
Domain-specific languages with scala.
In ICFEM, volume 9407 of Lecture Notes in Computer
Science, pages 1–16. Springer, 2015.

[8]
Giorgio Audrito.
FCPP: an efficient and extensible field calculus framework.
In Proceedings of the 1st International Conference on Autonomic
Computing and Self-Organizing Systems, ACSOS, pages 153–159. IEEE
Computer Society, 2020.

[9]
Giorgio Audrito, Mirko Viroli, Ferruccio Damiani, Danilo Pianini, and Jacob
A higher-order calculus of computational fields.
ACM Transactions on Computational Logic, 20(1):5:1–5:55, 2019.

[10]
Jacob Beal and Jonathan Bachrach.
Infrastructure for engineered emergence in sensor/actuator networks.
IEEE Intelligent Systems, 21:10–19, March/April 2006.

[11]
Eric Bonabeau, Marco Dorigo, and Guy Theraulaz.
Swarm Intelligence: From Natural to Artificial Systems.
Santa Fe Institute Studies in the Sciences of Complexity. Oxford
University Press, Inc., 1999.

[12]
Jacob Beal, Stefan Dulman, Kyle Usbeck, Mirko Viroli, and Nikolaus Correll.
Organizing the aggregate: Languages for spatial computing.
In Marjan Mernik, editor, Formal and Practical Aspects of
Domain-Specific Languages: Recent Developments, chapter 16, pages 436–501.
IGI Global, 2013.
A longer version available at: http://arxiv.org/abs/1202.5509.

[13]
J. Beal.
Amorphous medium language.
In Large-Scale Multi-Agent Systems Workshop (LSMAS), pages
1–7, July 2005.
Available at http://jakebeal.com/.

[14]
Jacob Beal, Danilo Pianini, and Mirko Viroli.
Aggregate programming for the Internet of Things.
IEEE Computer, 48(9), 2015.

[15]
Jacob Beal and Mirko Viroli.
Building blocks for aggregate programming of self-organising
In Eighth IEEE International Conference on Self-Adaptive and
Self-Organizing Systems Workshops, SASOW 2014, London, United Kingdom,
September 8-12, 2014, pages 8–13. IEEE Computer Society, 2014.

[16]
Jacob Beal, Mirko Viroli, Danilo Pianini, and Ferruccio Damiani.
Self-adaptation to device distribution in the Internet of Things.
ACM Transaction on Autonomous and Adaptive Systems,
12(3):12:1–12:29, September 2017.

[17]
Christian J Callsen and Gul Agha.
Open heterogeneous computing in actorspace.
Journal of Parallel and Distributed Computing, 21(3):289–300,

[18]
Roberto Casadei, Alessandro Aldini, and Mirko Viroli.
Towards attack-resistant aggregate computing using trust mechanisms.
Science of Computer Programming, 2018.

[19]
Min Chen, Yixue Hao, Yong Li, Chin-Feng Lai, and Di Wu.
On the computation offloading at ad hoc cloudlet: architecture and
service modes.
IEEE Communications Magazine, 53(6):18–24, 2015.

[20]
Alonzo Church.
A set of postulates for the foundation of logic.
Annals of Mathematics, 33(2):346–366, 1932.

[21]
Daniel Coore.
Botanical computing: a developmental approach to generating
interconnect topologies on an amorphous computer.
PhD thesis, Massachusetts Institute of Technology, 1999.

[22]
Roberto Casadei, Danilo Pianini, Andrea Placuzzi, Mirko Viroli, and Danny
Pulverization in cyber-physical systems: Engineering the
self-organizing logic separated from deployment.
Future Internet, 12(11):203, 2020.

[23]
Roberto Casadei, Danilo Pianini, and Mirko Viroli.
Simulating large-scale aggregate mass with alchemist and scala.
In Computer Science and Information Systems (FedCSIS), 2016
Federated Conference on, pages 1495–1504. IEEE, 2016.

[24]
Roberto Casadei, Danilo Pianini, Mirko Viroli, and Antonio Natali.
Self-organising coordination regions: A pattern for edge computing.
In Hanne Riis Nielson and Emilio Tuosto, editors, Coordination
Models and Languages, pages 182–199, Cham, 2019. Springer International

[25]
Roberto Casadei, Christos Tsigkanos, Mirko Viroli, and Schahram Dustdar.
Engineering resilient collaborative edge-enabled iot.
In 2019 IEEE International Conference on Services Computing
(SCC), pages 36–45, July 2019.

[26]
Roberto Casadei and Mirko Viroli.
Programming actor-based collective adaptive systems.
In Alessandro Ricci and Philipp Haller, editors, Programming
with Actors: State-of-the-Art and Research Perspectives, volume 10789 of
Lecture Notes in Computer Science, pages 94–122. Springer
International Publishing, 2018.

[27]
Roberto Casadei and Mirko Viroli.
Coordinating computation at the edge: a decentralized,
self-organizing, spatial approach.
In 2019 Fourth International Conference on Fog and Mobile Edge
Computing (FMEC), pages 60–67, June 2019.

[28]
Roberto Casadei, Mirko Viroli, Giorgio Audrito, Danilo Pianini, and Ferruccio
Aggregate processes in field calculus.
In Hanne Riis Nielson and Emilio Tuosto, editors, Coordination
Models and Languages, pages 200–217, Cham, 2019. Springer International

[29]
Roberto Casadei, Mirko Viroli, Giorgio Audrito, Danilo Pianini, and Ferruccio
Engineering collective intelligence at the edge with aggregate
Engineering Applications of Artificial Intelligence, 97:104081,

[30]
Simon Dobson, Spyros Denazis, Antonio Fernández, Dominique Gaïti, Erol
Gelenbe, Fabio Massacci, Paddy Nixon, Fabrice Saffre, Nikita Schmidt, and
Franco Zambonelli.
A survey of autonomic communications.
TAAS, 1(2):223–259, 2006.

[31]
Rocco De Nicola, Gianluigi Ferrari, Michele Loreti, and Rosario Pugliese.
A language-based approach to autonomic computing.
In Formal Methods for Components and Objects, volume 7542 of
Lecture Notes in Computer Science, pages 25–48, 2013.

[32]
Jeffrey Dean and Sanjay Ghemawat.
Mapreduce: simplified data processing on large clusters.
Communications of the ACM, 51(1):107–113, 2008.

[33]
Luis Damas and Robin Milner.
Principal type-schemes for functional programs.
In Symposium on Principles of Programming Languages, POPL '82,
pages 207–212. ACM, 1982.

[34]
Sébastien Jean R Doeraene.
Cross-platform language design.
Technical report, EPFL, 2018.

[35]
Muhammad Nouman Durrani and Jawwad A Shamsi.
Volunteer computing: requirements, challenges, and solutions.
Journal of Network and Computer Applications, 39:369–380,

[36]
Bradley R. Engstrom and Peter R. Cappello.
The SDEF programming system.
Journal of Parallel and Distributed Computing, 7(2):201 – 231,

[37]
Jean-Louis Giavitto, Olivier Michel, Julien Cohen, and Antoine Spicher.
Computations in space and space in computations.
In Unconventional Programming Paradigms, volume 3566 of Lecture Notes in Computer Science, pages 137–152. Springer, Berlin, 2005.

[38]
Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler.
Featherweight Java: A minimal core calculus for Java and GJ.
ACM Transactions on Programming Languages and Systems, 23(3),

[39]
C. Lasser, J.P. Massar, J. Miney, and L. Dayton.
Starlisp Reference Manual.
Thinking Machines Corporation, 1988.

[40]
Marco Mamei, Ronaldo Menezes, Robert Tolksdorf, and Franco Zambonelli.
Case studies for self-organization in computer science.
Journal of Systems Architecture, 52(8-9):443–460, 2006.

[41]
Fabrizio Montesi.
Choreographic programming.
IT-Universitetet i København, 2014.

[42]
Samuel R. Madden, Robert Szewczyk, Michael J. Franklin, and David Culler.
Supporting aggregate queries over ad-hoc wireless sensor networks.
In Workshop on Mobile Computing and Systems Applications, 2002.

[43]
Marco Mamei and Franco Zambonelli.
Programming pervasive and mobile computing applications: The tota
ACM Trans. on Software Engineering Methodologies, 18(4):1–56,

[44]
Radhika Nagpal.
Programmable pattern-formation and scale-independence.
In Unifying themes in complex systems IV, pages 275–282.
Springer, 2008.

[45]
Yang Ni, Ulrich Kremer, Adrian Stere, and Liviu Iftode.
Programming ad-hoc networks of mobile and resource-constrained
ACM SIGPLAN Notices, 40(6):249–260, 2005.

[46]
Ryan Newton and Matt Welsh.
Region streams: Functional macroprogramming for sensor networks.
In Workshop on Data Management for Sensor Networks, pages
78–87, aug 2004.

[47]
Bruno CdS Oliveira, Adriaan Moors, and Martin Odersky.
Type classes as objects and implicits.
In ACM Sigplan Notices, volume 45, pages 341–360. ACM, 2010.

[48]
Chris Peltz.
Web services orchestration and choreography.
Computer, 36(10):46–52, 2003.

[49]
Danilo Pianini, Sara Montagna, and Mirko Viroli.
Chemical-oriented simulation of computational systems with
Journal of Simulation, 2013.

[50]
Danilo Pianini, Mirko Viroli, and Jacob Beal.
Protelis: Practical aggregate programming.
In ACM Symposium on Applied Computing 2015, pages 1846–1853,
April 2015.

[51]
Weisong Shi, Jie Cao, Quan Zhang, Youhuizi Li, and Lanyu Xu.
Edge computing: Vision and challenges.
IEEE Internet of Things Journal, 3(5):637–646, 2016.

[52]
Tony Sloane.
Experiences with Domain-specific Language Embedding in Scala.
In Julia Lawall and Laurent Réveillère, editors, Domain-Specific Program Development, page 7, Nashville, United States,

[53]
Sherif Sakr, Faisal Moeen Orakzai, Ibrahim Abdelaziz, and Zuhair Khayyat.
Large-Scale graph processing using Apache giraph.
Springer, 2016.

[54]
Tadeusz M Szuba.
Computational collective intelligence.
John Wiley & Sons, Inc., 2001.

[55]
Karima Velasquez, David Perez Abreu, Marcio RM Assis, Carlos Senna, Diego F
Aranha, Luiz F Bittencourt, Nuno Laranjeiro, Marilia Curado, Marco Vieira,
Edmundo Monteiro, et al.
Fog orchestration for the internet of everything: state-of-the-art
and research challenges.
Journal of Internet Services and Applications, 9(1):14, 2018.

[56]
Mirko Viroli, Giorgio Audrito, Jacob Beal, Ferruccio Damiani, and Danilo
Engineering resilient collective adaptive systems by
ACM Trans. Model. Comput. Simul., 28(2):16:1–16:28, March

[57]
Mirko Viroli, Jacob Beal, Ferruccio Damiani, Giorgio Audrito, Roberto Casadei,
and Danilo Pianini.
From distributed coordination to field calculus and aggregate
Journal of Logical and Algebraic Methods in Programming,
109:100486, 2019.

[58]
Mirko Viroli, Jacob Beal, Ferruccio Damiani, and Danilo Pianini.
Efficient engineering of complex self-organising systems by
self-stabilising fields.
In Self-Adaptive and Self-Organizing Systems (SASO), 2015 IEEE
9th International Conference on, pages 81–90. IEEE, Sept 2015.

[59]
Tom Van Cutsem, Elisa Gonzalez Boix, Christophe Scholliers, Andoni Lombide
Carreton, Dries Harnie, Kevin Pinte, and Wolfgang De Meuter.
Ambienttalk: programming responsive mobile peer-to-peer applications
with actors.
Computer Languages, Systems & Structures, 40(3-4):112–136,

[60]
Mirko Viroli, Roberto Casadei, and Danilo Pianini.
On execution platforms for large-scale aggregate computing.
In Proceedings of the 2016 ACM International Joint Conference on
Pervasive and Ubiquitous Computing: Adjunct, pages 1321–1326. ACM, 2016.

[61]
M. Voelter.
DSL Engineering: Designing, Implementing and Using
Domain-specific Languages.
CreateSpace Independent Publishing Platform, 2013.

[62]
Kamin Whitehouse, Cory Sharp, Eric Brewer, and David Culler.
Hood: a neighborhood abstraction for sensor networks.
In Proceedings of the 2nd international conference on Mobile
systems, applications, and services. ACM Press, 2004.

[63]
Yong Yao and Johannes Gehrke.
The cougar approach to in-network query processing in sensor
SIGMOD Record, 31:2002, 2002.

[64]
Franco Zambonelli, Andrea Omicini, Bernhard Anzengruber, Gabriella Castelli,
Francesco L. De Angelis, Giovanna Di Marzo Serugendo, Simon Dobson, Jose Luis
Fernandez-Marquez, Alois Ferscha, Marco Mamei, Stefano Mariani, Ambra
Molesini, Sara Montagna, Jussi Nieminen, Danilo Pianini, Matteo Risoldi,
Alberto Rosi, Graeme Stevenson, Mirko Viroli, and Juan Ye.
Developing pervasive multi-agent systems with nature-inspired
Pervasive and Mobile Computing, 17, Part B(0):236 – 252, 2015.
10 years of Pervasive Computing' In Honor of Chatschik Bisdikian.

[65]
Matei Zaharia, Reynold S Xin, Patrick Wendell, Tathagata Das, Michael Armbrust,
Ankur Dave, Xiangrui Meng, Josh Rosen, Shivaram Venkataraman, Michael J
Franklin, et al.
Apache spark: a unified engine for big data processing.
Communications of the ACM, 59(11):56–65, 2016.

§ TEMPORARILY REMOVED

§.§ Domains and Interactions in Field-Aware

The first restriction (field-aware , Section <ref>) discards the  programs whose behaviour is not easily understood and characterised, allowing for additional properties characterising the interaction structure of a program, by analysing the domain of expressions.
[Domain of a  expression]
The domain of a closed expression $\e$ in a round on device $\deviceId$ with value-tree environment $\Trees$ and sensor-state $\senstate$ is:

\[
\{\deviceId'\in\domof{\Trees} \cup \{\deviceId\} : ~  \exists \vtree ~ \text{s.t.} ~ \bsopsem{\deviceId,\deviceId'}{\Trees}{\senstate}{\e}{\vtree} \text{ holds} \}.
\]

Notice that the domain of an expression $\e$ corresponds to the set of neighbours considered by a $\foldK$-expression of the form $\foldK(...)(...)\{\e\}$
(see Rule [E-FOLD] in Figure <ref>).

[Domain of an expression]
Consider the following expression, where $\svalue: () \rightarrow \ntype$ is a built-in integer sensor which evaluates to $s_\deviceId$ on device $\deviceId$.

\[
\ifK(\svalue()<4)\{\nbrK\{2\}\}\{\nbrK\{3\}\} * \ifK(\svalue()>0)\{\nbrK\{5\}\}\{\nbrK\{7\}\} * \nbrK\{11\}
\]

The evaluation of the above expression $\e_1 * \e_2 * \e_3$ (where $\e_1$, $\e_2$ are the two $\ifK$-expressions and $\e_3$ is the
$\nbrK\{11\}$ expression) fails in the following cases:

* if the first branch's condition $\svalue()<4$ evaluated differently in device $\deviceId'$, the evaluation of $\e_1$ would fail: in fact, $\deviceId'$ would be discarded from $\Theta$ by Rule[Recall that $\ifK$ is a shorthand for a functional application (see end of Section <ref>).] [E-D-APP] thus preventing later application of rule [E-NBR];

* similarly, if the second branch's condition $\svalue()>0$ evaluated differently in device $\deviceId'$, the evaluation of $\e_2$ would fail.

Thus only devices which evaluated both $\svalue()<4$ and $\svalue()>0$ in the same way $\deviceId$ did belong to the domain. This behaviour can be understood as implicitly combining expressions $\e_1$ and $\e_2$ by taking the intersection of their domains, which in the sample expression above gives the set of devices whose value of $\svalue()$ belongs to the same element of the partition $\{\ldots, -1, 0\}$, $\{1,2,3\}$, $\{4, 5, \ldots\}$.

Accordingly, in Field-Aware  we can prove the following properties.

Domain Coherence
The domain of an expression $\e$ in field-aware  corresponds to the set of neighbours which in their last round evaluated the same field-like subexpressions of $\e$ that are not contained in local-like subexpressions of $\e$.

Domain Partitioning
The evaluation of a $\foldK$-expression $\e$ in field-aware  determines a partition of the events occurring in a network, so that the third branch of $\e$ (excluding nested $\foldK$-subexpressions) is evaluated in isolation in each of the sets forming the partition.

Domain Restriction
The evaluation of a function application $\e(\overline\e)$ in field-aware  proceeds in isolation in the sets of events evaluating $\e$ to a same function $\funvalue$.

Queste spiegazioni sono basate su “forward-references” a field-like, local-like, field-aware... e non sono molto intuitive.

[MV – questa prima frase e' molto negativa espressa cosi'.. andrebbe detto meglio.. anche perche' la questione e' cruciale]

In , it is not possible to statically determine when and where neighbour interaction is exploited. In this section we  define a more restrictive type system (Figure <ref>), which discriminates between field- and local-like expressions (i.e., exploiting neighbour interaction or not). In this restricted type system, we will be able to characterise the domain of expressions, and interaction shape of various constructs.

§.§.§ Field-aware typing and expressions

Neighbourhood interaction can be captured by the following definition.

[Field- and Local-Like  Expression]
Let $\e$ be an expression with free variables $\FV{\e} = \overline\xname$ and type $\e : \type$ with respect to assumptions $\overline\xname : \overline\type$. We say that $\e$ is field-like (resp. local-like) if for all $\overline\anyvalue : \overline\type$ and for all $\Trees$ coherent with $\e$, $\senstate, \deviceId$ and $\deviceId' \notin \domof{\Trees} \cup \{\deviceId\}$, we have that $\bsopsemFAIL{\deviceId,\deviceId'}{\Trees}{\senstate}{\applySubstitution{\e}{\substitution{\overline\xname}{\overline\anyvalue}}}$ holds (resp. does not hold).

For example, given $\svalue: () \rightarrow \ntype$ as in Example <ref>, $\nbrK\{\svalue()\}$ is a field-like expression while $\foldK(0)(+)\{\nbrK\{\svalue()\}\}$ is not. Notice that (both closed and open) expressions may be neither field-like nor local-like, such as the following ones.

\[
\begin{array}{c}
\ifK \; (\xname) \; \{ \nbrK\{\svalue()\} \} \; \{ 0 \}
\\
\repK \; (0) \; \{(\xname) \; \toSymK{\; \ifK \; (\xname == 0) \; \{ 1 \} \; \{ \nbrK\{\svalue()\} \} \;} \}
\end{array}
\]

Thus, identifying field- and local-like expressions may not be trivial in its most general form. However, in some cases the syntax of an expression may be enough to determine its “field” or “local” status.

Let $\e$ be an expression with free variables $\FV{\e} = \overline\xname$ and type $\e : \type$ with respect to assumptions $\overline\xname : \overline\type$, and assume $\overline\anyvalue : \overline\type$ given. Then, if $\bsopsemFAIL{\deviceId,\deviceId'}{\Trees}{\senstate}{\applySubstitution{\e}{\substitution{\overline\xname}{\overline\anyvalue}}}$ holds for some $\deviceId'$, it also hold for every $\deviceId'' \notin \domof{\Trees} \cup \{\deviceId\}$. Thus, failure for all $\deviceId' \notin \domof{\Trees} \cup \{\deviceId\}$ is equivalent to failure for some $\deviceId'$, and failure for no $\deviceId' \notin \domof{\Trees} \cup \{\deviceId\}$ is equivalent to failure for no $\deviceId'$.

A well-typed expression $\e$ is:

* field-like if it is an $\nbrK$-expression  $\nbrK\{\e\}$, a relational sensor call $\snvalue(\overline\e)$, or a function call $\e(\e_1,...,\e_n)$ where at least one argument $\e_i$ ($1 \leq i \leq n$) is a field-like expression;

* local-like if it is a value $\anyvalue$, a $\repK$-expression $\repK (\e) \{\e\}$, or a $\foldK$-expression $\foldK (\e) (\e) \{\e\}$.

In order to fully characterize field-like expressions, we need a way to reject those expressions that are neither field-like nor local-like. This can be accomplished through the type system given in Figure <ref> for . This type system differs from the one presented in Figure <ref> by introducing a separate field type $\ftypeOf{\ltype}$ for field-like expressions, separating local type variables $\ltvar$ from general type variables $\tvar$, restricting the types allowed for functions, and updating the rules accordingly. In particular, functions can either be fully local $(\overline\ltype) \to \ltype$ or have field return type $(\overline\type) \to \ftype$: that is, functions are not allowed to “collapse” field arguments into local values. Furthermore, functions with field arguments can be applied only if they are values.[Applying a non-constant function $\e$ (evaluating to $\funvalue$ on $\deviceId$) to field arguments $\overline\e$ may result in breaking all the domain properties. In fact, such an application $\e(\overline\e)$ may not fail on neighbours $\deviceId'$ which evaluated $\e$ to a different function $\funvalue'$ (breaking domain coherence and restriction), as long as the evaluation of $\funvalue(\overline\e)$ does not involve the computation of $\nbrK$-statements or relational built-in applications. This may result in one-sided communication if $\funvalue'$ involves the computation of $\nbrK$-statements instead (breaking domain partitioning).]

%%%  TYPES
<EMAIL_ADDRESS>\multicolumn{4}{l}{\textbf{Types:}} \\[1pt]
\type	& \BNFcce & \tvar \; \BNFmid \; \ftype \; \BNFmid \; \ltype
&   {\footnotesize \mbox{type}} \\
\ltype	& \BNFcce & \ltvar \; \BNFmid \; \builtintype \; \BNFmid \; (\overline\ltype)\to\ltype \; \BNFmid \; (\overline\type)\to\ftype
& {\footnotesize \mbox{local type}} \\
\ftype	& \BNFcce & \ftypeOf{\ltype}
&   {\footnotesize \mbox{field type}} \\[2pt]
\multicolumn{4}{l}{\textbf{Local type schemes:}} \\[1pt]
\ltypescheme & \BNFcce & \forall\overline{\tvar}\overline{\ltvar}.\ltype
&   {\footnotesize \mbox{local type scheme}} \\
\end{array} \\[38pt]
\hline\\[-8pt]
%%%  EXPRESSIONS
\textbf{~~Expression typing:} \hfill \boxed{\expTypJud{\LTStypEnv}{\TtypEnv}{\e}{\type}} \\[5pt]
\quad
\begin{array}{c}
\nullsurfaceTyping{T'-VAR}{
\expTypJud{\LTStypEnv}{\TtypEnv, \xname:\type}{\xname}{\type}
\qquad
\surfaceTyping{T'-DAT}{ \quad
\applySubstitution{\ltype'}{\substitution{\overline\ltvar}{\overline\ltype''}} = (\overline{\ltype})\rightarrow\ltype
\qquad
\expTypJud{\TStypEnv}{\TtypEnv}{\overline{\lvalue}}{\overline{\ltype}}
\expTypJud{\TStypEnv,\dc: \forall\overline\ltvar. \ltype'}{\TtypEnv}{\dc(\overline{\lvalue})}{\ltype}
\skiptransition
\surfaceTyping{T'-A-FUN}{  \quad
\expTypJud{\LTStypEnv}{\TtypEnv, \overline{\xname} : \overline\type}{\e}{\type}
\expTypJud{\LTStypEnv}{\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\overline\ltvar.\ltype}{\TtypEnv}{\funvalue}{\applySubstitution{\ltype}{\substitution{\overline\tvar}{\overline\type},~ \substitution{\overline{\ltvar}}{\overline{\ltype}}}}
\skiptransition
\surfaceTyping{T'-V-APP}{ \qquad
\expTypJud{\LTStypEnv}{\TtypEnv}{\funvalue}{(\overline\type)\rightarrow\type} \qquad
\expTypJud{\LTStypEnv}{\TtypEnv}{\overline{\e}}{\overline\type}
\expTypJud{\LTStypEnv}{\TtypEnv}{\funvalue(\overline{\e})}{\type}
\skiptransition
\surfaceTyping{T'-E-APP}{ \qquad
\expTypJud{\LTStypEnv}{\TtypEnv}{\e}{(\overline\ltype)\rightarrow\type} \qquad
\expTypJud{\LTStypEnv}{\TtypEnv}{\overline{\e}}{\overline\ltype} \qquad
\e \text{ is not a value}
\expTypJud{\LTStypEnv}{\TtypEnv}{\e(\overline{\e})}{\type}
\skiptransition
\surfaceTyping{T'-REP}{ \quad
\expTypJud{\LTStypEnv}{\TtypEnv}{\e_1}{\ltype} \qquad
\expTypJud{\LTStypEnv}{\TtypEnv}{\e_2}{\ltype \rightarrow \ltype}
\expTypJud{\LTStypEnv}{\TtypEnv}{\repK(\e_1)\{\e_2\}}{\ltype}
\qquad
\surfaceTyping{T'-NBR}{ \quad
\expTypJud{\LTStypEnv}{\TtypEnv}{\e}{\ltype}
\expTypJud{\LTStypEnv}{\TtypEnv}{\nbrK\{\e\}}{\ftypeOf{\ltype}}
\skiptransition
\surfaceTyping{T'-FOLD}{ \qquad
\begin{array}{ll}
\expTypJud{\TStypEnv}{\TtypEnv}{\e_1}{\ltype}
& \quad
\expTypJud{\TStypEnv}{\TtypEnv}{\e_3}{\ftypeOf{\ltype} \text{ or } \ltype}
\\
\expTypJud{\TStypEnv}{\TtypEnv}{\e_2}{(\ltype, \ltype) \rightarrow \ltype}
& \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\} }{\ltype}
\end{array} \\~\\
%%%  FUNCTIONS
\textbf{~~Function typing:} \hfill \boxed{\funTypJud{\LTStypEnv}{\FUNCTION}{\ltypescheme}} \\[5pt]
\qquad \qquad
\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}\overline{\ltvar}=\FTV{(\overline{\type})\rightarrow\type}
\funTypJud{\TStypEnv}{\defK \; \fname (\overline{\xname}) \; \eqSymK{\e}}{\forall\overline{\tvar}\overline{\ltvar}.(\overline{\type})\rightarrow\type}
\end{array} \\~\\
%%%  PROGRAMS
\textbf{~~Program typing:} \hfill {\boxed{\funTypJud{\LTStypEnv_0}{\PROGRAM}{\type}}} \\[5pt]
\qquad \quad
\begin{array}{c}
\surfaceTyping{T'-PROGRAM}{
\\
\TStypEnv_0=\OStypEnv
\\
\FUNCTION_i = \defK \; \fname_i (\_) \; \eqSymK{\_}
\qquad
\funTypJud{\TStypEnv_{i-1}}{\FUNCTION_i}{\ltypescheme_i}
\qquad
\TStypEnv_i=\TStypEnv_{i-1},\, \fname_i:\ltypescheme_i
\qquad
(i \in 1..n)
\\
\expTypJud{\TStypEnv_n}{\emptyset}{\e}{\ltype}
\proTypJud{\FUNCTION_1\cdots\FUNCTION_n  \; \e}{\ltype}
\end{array}
\end{array}$
Field-aware Hindley-Milner typing for  expressions, function declarations, and programs.

Rules [T'-VAR], [T'-A-FUN] are identical to their counterparts in Figure <ref>. Rules [T'-N-FUN] and [T'-FUNCTION] are identical except for acknowledging the existence of two kinds of type variables. Rules [T'-DAT], [T'-REP], [T'-PROGRAM] are obtained from their counterparts by requiring each involved type to be local. Rule [T'-NBR] for $\nbrK$-expressions requires the argument to be local, converting it into the corresponding field type. Rule [T'-V-APP] is identical to rule [T-APP] with the additional requirement of the function to be applied being a value, and the implicit requirement that the function type $(\overline\type) \to \type$ belongs to the types $(\overline\ltype) \to \ltype$, $(\overline\type) \to \ftype$ accepted by the type system. Rule [T'-E-APP] covers the case where the function to be applied is given by an expression, and has the additional requirement for this function to have local arguments. Rule [T'-FOLD] requires the first two expressions to be local, allowing the third to (possibly) be of the corresponding field type. Furthermore, it requires each free variable occurring in the third branch to be of local type. In fact, folding statements cannot capture field variables, as their evaluation “resets” the neighbour $\deviceId'$ and thus is not able to correctly interpret captured field values as fields. For example, the  program:
def avghood(x) = @@
foldhood(0)(+)x / foldhood(0)(+)1

which we may think to calculate the average temperature of neighbours, is instead fully equivalent to the simpler program $\nbrK\{\texttt{sns-temp}()\}$. If we evaluate the main expression against a neighbour $\deviceId'$, we obtain as argument the temperature $t$ of that neighbour. Then, the function is applied obtaining as value $nt / n = t$ where $n$ is the number of neighbours (since the body of the $\foldhoodK$ statements are constants, from the point of view of the applied function).

The erasure of a field-aware type $\type$ is the “standard” type $\erasureof{\type}$ obtained from $\type$ by replacing all the occurrences of $\ftypeOf{\ltype}$ with $\ltype$ and dropping the distinction between the different kinds of type variables (i.e., by considering each of them as a standard type variable $t$).

Let $\PROGRAM$ be an $\FSCAFI$ program well typed according to the field-aware type system, with field-aware type $\type$. Then:

* $\PROGRAM$ is well typed according to the standard type system with type $\erasureof{\type}$;

* The main expression of $\PROGRAM$ is field-like if and only if $\type$ is of the form $\ftypeOf{\ltype}$.

§.§.§ Expression domains and interactions

For expressions that are well-typed by the field-aware type system, the domain coherence can be reformulated in a more understandable way, and gives rise to interesting exploitable consequences.

We say that $\e'$ is a proper field-like subexpression of $\e$ if and only if each subexpression of $\e$ containing $\e'$ is field-like.

The domain of an expression $\e$ with field-aware type $\ftypeOf{\ltype}$ corresponds to the set of neighbours which in their last round evaluated the same proper field-like subexpressions of $\e$.

The evaluation of a $\foldK$-expression $\e$ determines a partition of the events occurring in a network, so that the third branch of $\e$ (excluding nested $\foldK$-subexpressions) is evaluated in isolation in each of the sets forming the partition.

In the evaluation of a function application $\e(\overline\e)$, the sets of events evaluating $\e$ to a same function $\funvalue$ compute the body of $\funvalue$ in isolation.

§.§ Field-Like and Local-Like Expressions

[Field- and Local-Like Equivalent Definitions]lem:flikedef
Let $\e$ be a well-typed expression with free variables $\FV{\e} = \overline\xname$. Then,

if $\bsopsemFAIL{\deviceId,\deviceId'}{\Trees}{\senstate}{\applySubstitution{\e}{\substitution{\overline\xname}{\overline\anyvalue}}}$ holds for some $\deviceId'$, it also hold for every $\deviceId'' \notin \domof{\Trees} \cup \{\deviceId\}$. Thus, failure for all $\deviceId' \notin \domof{\Trees} \cup \{\deviceId\}$ is equivalent to failure for some $\deviceId'$, and failure for no $\deviceId' \notin \domof{\Trees} \cup \{\deviceId\}$ is equivalent to failure for no $\deviceId'$.

Let $\deviceId'$ be such that the evaluation fails. If $\deviceId'$ is used at some point to guide branching, it must be able to influence evaluation of the branching guard through a relational sensor application or $\nbrK$-expression, which will fail for all $\deviceId'' \notin \domof{\Trees} \cup \{\deviceId\}$. Otherwise, the same subexpressions of $\e$ will be evaluated for any $\deviceId'' \notin \domof{\Trees} \cup \{\deviceId\}$. Since the evaluation failed for $\deviceId'$, at least one of them must be a relational sensor application or $\nbrK$-expression, which will fail for all $\deviceId'' \notin \domof{\Trees} \cup \{\deviceId\}$.

[Partial Characterisation of Field- and Local-Like  Expressions]prop:fieldcriterion
A well-typed expression $\e$ is:

* field-like if it is an $\nbrK$-expression  $\nbrK\{\e\}$, a relational sensor call $\snvalue(\overline\e)$, or a function call $\e(\e_1,...,\e_n)$ where at least one argument $\e_i$ ($1 \leq i \leq n$) is a field-like expression;

* local-like if it is a value $\anyvalue$, a $\repK$-expression $\repK (\e) \{\e\}$, or a $\foldK$-expression $\foldK (\e) (\e) \{\e\}$.

If $\e$ is an $\nbrK$-expression, a relational sensor call, or a function call with a field-like argument $\e_i$, then it fails for all $\deviceId' \notin \domof{\Trees} \cup \{\deviceId\}$ by rules [E-NBR-FAIL], [E-R-APP-FAIL] and [E-APP-ARG-FAIL] for $m = i-1$ respectively (together with the fact that $\e_i$ is field-like for the third case).

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.

[Refined typing for ]thm:fieldtypes
Let $\PROGRAM$ be an $\FSCAFI$ program well typed according to the field-aware type system, with field-aware type $\type$. Then:

* $\PROGRAM$ is well typed according to the standard type system with type $\erasureof{\type}$;

* The main expression of $\PROGRAM$ is field-like if and only if $\type$ is of the form $\ftypeOf{\ltype}$.

* Notice that every rule in Figure <ref> can be obtained by the corresponding rule in Figure <ref> by collapsing local and field types into a single category and erasing $\ftypeOf{\cdot}$ when present. Thus, every derivation of a type $\type$ for $\PROGRAM$ correspond to a derivation of $\erasureof{\type}$ in the standard type system with the corresponding rules.

* We prove this part by induction on formulas $\e$. If $\e$ is a value, $\repK$-statement or $\foldK$-statement, it is local-like by Proposition <ref> and is correctly given a local type in the field-aware type system. If $\e$ is a $\nbrK$-statement, it is field-like by Proposition <ref> and is correctly given a field type. The only remaining case is when $\e' = \e(\overline\e)$ is a function application.

Assume now that $\e$ is a local function $(\overline\ltype) \to \ltype$.  By inductive hypothesis, the evaluation of $\e$ and $\overline\e$ does not fail for any neighbour $\deviceId'$. By inductive hypothesis, neither can the body, concluding the proof in this case. Since no expression can have type $(\overline\type) \to \ltype$ unless all $\overline\type$ are local, the only remaining possibility is that $\e$ has field return type. Thus, its body has been given a type $\ftypeOf{\ltype}$, and by inductive hypothesis its evaluation fails for $\deviceId'$ outside of the domain of $\Trees$, concluding the proof.

§.§ Expression Domains and Device Interactions

[Node Ancestors]
A node $\vtree$ in a value-tree is an ancestor of another node $\vtree'$ if $\vtree'$ is a sub-tree of $\vtree$. A node $\vtree = \mkvtree{}{\anyvalue}{\overline\vtree}$ in a value-tree is a leftmost-ancestor (resp. rightmost-ancestor) of another node $\vtree'$ if $\vtree' = \vtree$ or it is a sub-tree of the first (resp. last) sub-tree $\vtree_1$ of $\vtree$. A node $\vtree$ is a value-tree is a proper ancestor (resp. leftmost-ancestor, rightmost-ancestor) of another node $\vtree'$ if in addition $\vtree \neq \vtree'$.

The oriented notions of leftmost- and rightmost-ancestors will be useful to characterise the behaviour of function calls, since for them the first and last sub-branches have a different meaning and implementation characteristics.

[Value-Tree Nodes]
We identify the following nodes in value-trees:

* Function call nodes,
which are produced by function calls (rules [E-B-APP], [E-D-APP]).

* Barrier nodes,
which are nodes that are not function call nodes.

* Field nodes,
which are produced by $\nbrK$-expressions or by relational sensor calls (rule [E-NBR] or rule [E-B-APP] where the root of the first sub-branch is a relational built-in sensor).

* Proper field nodes,
which are field nodes without barrier proper ancestors nor function call proper leftmost-ancestors.

Intuitively, field nodes are those which may originate failures, barrier nodes are those which do not propagate failures, function call nodes propagate failures except on their leftmost sub-branch, hence proper field nodes are those possibly originating failures that are propagated all the way through the evaluation.

[Value-Tree Alignment]
A node $\vtree'_1$ in a value-tree $\vtree_1$ is corresponding to a node $\vtree'_2$ in another value-tree $\vtree_2$ if they are obtained by following the same path in their respective value-trees.

A node in a value-tree $\vtree$ is aligned with a corresponding one in a value-tree $\vtree'$ if their function call rightmost-ancestors[Note that this may include the node itself as improper ancestor, if the node is obtained by a relational built-in call.] are pairwise corresponding and obtained by the evaluation of identical functions (i.e., the root of their first sub-branches are functions with identical names).

A value-tree $\vtree'$ is aligned with another value-tree $\vtree$ if every proper field node in $\vtree$ is aligned with the corresponding node in $\vtree'$.

Suppose that $\bsopsem{\deviceId,\deviceId}{\Trees}{\senstate}{\e}{\vtree}$. Then, $\bsopsemFAIL{\deviceId,\deviceId'}{\Trees}{\senstate}{\e}{}$ for some $\deviceId' \in \domof{\Trees}$ if and only if $\Trees(\deviceId')$ is not aligned with $\vtree$.

First, notice that by Lemma <ref> failures cannot be generated by $\repK$- or $\foldK$-expressions (no rules for the failure of such expressions exist), nor by the evaluation of the argument $\e$ of an $\nbrK\{\e\}$ expression (rule [E-NBR-FAIL] is not influenced by the evaluation of such $\e$, which only occurs with $\deviceId' = \deviceId$ in [E-NBR-LOC]). Since such expressions are those evaluating to barrier nodes, it follows that descendants of barrier nodes cannot generate failures, and are correctly ignored by the alignment relation.

Furthermore, failures cannot be generated by the evaluation of the function $\e$ in a function call $\e(\overline\e)$ expression (as it is evaluated with $\deviceId = \deviceId'$ in [E-B-APP] and [E-D-APP]), thus leftmost-descendants of function call nodes cannot generate failures either and are correctly ignored by the alignment relation.

Notice now that failures are generated only by rules [E-NBR-FAIL] and [E-R-APP-FAIL], which correspond to field nodes, in case $\deviceId'$ is not in the domain of the (possibly) restricted current value-tree environment. If a field node is not proper, such failures are absorbed or prevented by enclosing statements, as shown above. If instead a field node is proper, rules [E-APP-ARG-FAIL] and [E-D-APP-FAIL] ensure that failures are propagated together with the reference neighbour $\deviceId'$ (which is also propagated in case of success by rules [E-B-APP] and [E-D-APP]). Thus, failure occurs if and only if $\deviceId'$ gets filtered out of the current value-tree environment in a proper field node.

Notice that the value-tree environment is restricted only in built-in function calls (rules [E-B-APP] and [E-R-APP-FAIL]) and in the rightmost sub-branch of defined function calls (rule [E-D-APP] and [E-D-APP-FAIL]); and $\deviceId'$ is filtered out iff the function applied in $\vtree$ has a different name than the one applied in the corresponding node in $\Trees(\deviceId')$ (by definition of $\piB{\funvalue}$). Thus, a failure occurs iff a (possibly improper) rightmost-ancestor of a proper field node corresponds to the application of a different function, that is, iff $\vtree$ and $\Trees(\deviceId')$ are not aligned, concluding the proof. We should also argument that evaluating an expression against different $\deviceId'$ results in the same tree structure (if succeeds).

[Field-Aware Domain Coherence]thm:domain-coherence
The domain of an expression $\e$ with field-aware type $\ftypeOf{\ltype}$ corresponds to the set of neighbours which in their last round evaluated the same proper field-like subexpressions of $\e$.

Let $\e$ be well-typed by the field-aware type system. Then, the induced relation of alignment between value-trees is an equivalence relation, i.e., is reflexive, symmetrical and transitive.

Verifying that a node is aligned to itself is straightforward, concluding that alignment is reflexive. TODO: symmetrical. Suppose now that $\vtree_1$ is aligned with $\vtree_2$, and $\vtree_2$ with $\vtree_3$. Consider any proper field node $\vtree'_1$ in $\vtree_1$, the corresponding node $\vtree'_2$ in $\vtree_2$, and the further corresponding node $\vtree'_3$ in $\vtree_3$. Any function call rightmost-ancestor of $\vtree'_1$ corresponds to an identical one of $\vtree'_2$, which in turns correspond to an identical one of $\vtree'_3$. It follows that the node $\vtree'_1$ is aligned with the node $\vtree'_3$, concluding the proof.

[Domain Partitioning]cor:domain-partitioning
The evaluation of a $\foldK$-expression $\e$ determines a partition of the events occurring in a network, so that the third branch of $\e$ (excluding nested $\foldK$-subexpressions) is evaluated in isolation in each of the sets forming the partition.

Consider the evaluation of a $\foldK$-statement $\foldK(\e_1)(\e_2)\{\e_3\}$ producing value-trees $\mkvtree{}{\anyvalue}{\vtree_1, \vtree_2, \vtree_3}$ in each event. Partition the events according to the alignment equivalence relation (Lemma <ref>) on the $\vtree_3$ value-tree. By Lemma <ref> the evaluation of $\e_3$ with respect to a neighbour $\deviceId$ in the same partition produces a value, whereas it fails for $\deviceId$ in a different partition. Since the only statements that (possibly) introduces new neighbours are $\foldK$-statements, the evaluation of the third branch of $\e$ (excluding nested $\foldK$-subexpressions) occurs in isolation in each equivalence class.

[Domain Restriction]cor:domain-restriction
In the evaluation of a function application $\e(\overline\e)$, the sets of events evaluating $\e$ to a same function $\funvalue$ compute the body of $\funvalue$ in isolation.

Events computing the application of a different function can produce aligned value-trees only if the body is fully local (i.e., does not contain proper $\nbrK$-expression or relational built-ins) so that the evaluation of the body is performed in isolation in each device. If the body is not fully local, the evaluation produces not-aligned value-trees thus is performed in isolation in the different sets by Theorem <ref>.

§.§ Interpreter

Operational semantics as implemented in .

TODO: temporarily put here, but probably to be dropped entirely?

Component  extends components  and .

This is where the operational semantics described in <Ref> is implemented, i.e., where the machinery that maps contexts to exports is structured in terms of data structures and functions.

An export is essentially a partial value-tree containing only the information that needs to be preserved across rounds and communicated to neighbours so as to support alignment.

The nodes of the tree that represent an export are given by slots,
implemented as an Scala algebraic data type .

Intuitively, the result of an  expression (slot ) has to be stored so that it can be shared with the neighbours,
and so has the result of a  expression (slot ) to supports its stateful dynamics across rounds.

A slot is also needed for aggregate functions ()—since they are units of alignment.

Conversely, a slot  is not strictly necessary but it comes useful for optimisations.

trait Semantics extends Core with Language
trait Slot extends Serializable
sealed case class Nbr[A](index: Int) extends Slot
sealed case class Rep[A](index: Int) extends Slot
sealed case class FunCall[A](index: Int, funId: Any) extends Slot
sealed case class FoldHood[A](index: Int) extends Slot

Internally, an export is a data structure consisting of a map from paths to values.
A path is an ordered list of slots;
in order to distinguish multiple occurrences of the same operator at the same level,
slots have an  property that gets incremented at each nesting level.

Now let's focus on how the operational semantics of the field calculus is implemented in .

An aggregate computation consists in a distributed and repeated execution of a field calculus program.

In the context of a single device, the program is run again and again, on a round-by-round basis.

Each computation round is launched with a context and ultimately yields an export.

A field calculus programs has an entry point where the computation starts;
from there, the computation unfolds as a succession of method calls, handled by the interpreter,
which result in a progressive evolution of the virtual machine state and construction of the export.

The virtual machine resets its state (actually by building a fresh new one) at the beginning of each round.

The entry point for the interpreter is the following  method:
// Big step evaluation: !$\bsopsem{\deviceId,\deviceId}{\Trees}{\senstate}{\e}{\vtree}$!
def round(c: CONTEXT, e: => Any): EXPORT =
vm = new RoundVMImpl(c)   // Context c includes !$\deviceId$! and !$\Trees$!
val result = e            // Program expression !$\e$! is run
vm.registerRoot(result)   // Final result !$\rho(\vtree)$! is registered
vm.export                 // Return the export of the computation: !$\vtree$!

The  object, of type  (whose interface is reported in Figure <ref>),
provides a set of utility methods for
(i) inspecting the input context,
(ii) inspecting and manipulating the evaluation context, that is, the moves used to decide and evolve the state of the machine,
and (iii) recording the export result.

Internally to work, it keeps a sort of stack to track, freeze, and restore the evaluation context at specific locations of the export tree.

trait RoundVM
def export: EXPORT
def registerRoot(v: Any): Unit
def self: ID
def neighbour: Option[ID]
def index: Int
def previousRoundVal[A]: Option[A]
def neighbourVal[A]: A
def foldedEval[A](expr: => A)(id: ID): Option[A]
def localSense[A](name: LSNS): A
def neighbourSense[A](name: NSNS): A
def nest[A](slot: Slot)(write: Boolean)(expr: => A): A
def locally[A](a: => A): A
def alignedNeighbours(): List[ID]
def elicitAggregateFunctionTag(): Any

Interface for the machinery of the interpreter.

In trait , the core semantics of the field calculus is defined, in a rather succint way.

There is a clear pattern in this implementation:
excluding  and ,
which only need to query the VM for sensor values,
the other constructs start off by nesting the evaluation,
which effectively simulates the positioning of the interpreter at a child node in the value-tree.

The calls to  specify the slot  that has to be followed,
a flag  indicating whether the export has to be written at that position in the value-tree,
and the corresponding expression  to be evaluated at that point.

It should be noted that only  may choose not to write an export node,
depending on the neighbour with respect to evaluation is going on.

is implemented by nesting evaluation in a  node
and executing the stateful transformation in a local context:
is called with the result of the current export node as obtained in the previous round (which is available in the input ), if present, or with  otherwise.

Since fields are not reified in  as values and data types,
the VM has to consider two modes of operation:
one where evaluation is carried out with respect to a certain neighbour,
and the default one in which evaluation is purely local.

Thus, in the implementation of the semantics, it is necessary to specify the mode in which lazy subexpressions are evaluated:
is used to save the neighbour that is currently considered (possibly none),
resetting evaluation to a local context for the execution of expression ,
and finally restoring the tracking neighbour;
by contrast,  is used to evaluate  on behalf of device .

creates a nested node where
a value corresponding to  is obtained for each aligned neighbour
(nodes that are actually not aligned will be associated with a local value )
and the resulting collection is functionally folded with initial local value  and aggregation function .

Note that  is the only construct that calls , that is, it is the sole operator that can evaluate an expression “in the context of” a neighbour device.

is the interaction/communication construct of the field calculus.

It nests evaluation in a corresponding node but chooses to actually execute  and write the resulting value at such export location
if the current execution context is local or if the neighbour which is fold on is ,
otherwise it is not a local context and the corresponding  is simply returned.

In other words,  is used either in a purely local context (i.e., outside ), where it just evaluates the given expression without any additional semantics,
or in a  within , where the semantics depends on the neighbour considered:
if it is , then the expression is evaluated and the export is written,
otherwise  is called to get the neighbour's export from the input context.

is the construct used to wrap functions that need to have an “aggregate” semantics, i.e., that need to be units of alignment.

As a consequence, it creates an export node which is tagged by an identifier, issued by the VM,
that depends on the location in source code where the aggregate function is defined
(for instance, this can be achieved by inspecting the stack trace).

The logic is trivial:  is simply executed;
the point is that, by nesting on a slot that coincide with the function identity,
only the neighbours that will have the same export node (i.e., that will execute the same aggregate function) will be aligned and thus able to interact.

and  are used to access a purely local sensor and a neighbouring sensor , respectively.

The key difference between the two is that,
whereas  only inspects the local context,
is much like , that is,
it takes into consideration the neighbour on which the interpreter is folding.

Also note that, if no sensor of the given  is available, both operators will raise an exception.

Crucially however, when  is used within  (which is the only useful way to use it), any exception would be suppressed by  and then mapped to  in .

§.§ Overall Comparison of  and

We now compare  static and dynamic semantics with those of . However closely correlated, they have some intrinsic differences summarised in Table <ref> and discussed in the remainder of this section.

Field values     Simulated but not constructed; cannot be passed to functions     Constructed during evaluation

Built-in operators     Relational sensors and functions on local data (can be applied to fields pointwise or through $\foldK$)     Anything; including non-positional functions on fields like

Types     Same as host language     $\type$, $\ftypeOf{\type}$ for any $\type$ in the host language

Expressions allowed     Anything accepted by the host language     Custom restrictions to be implemented

Safety     Type preservation     Type preservation and domain alignment

Default domain management     Permissive     Restrictive

Comparison between  and .

§.§.§ Field values and built-in operators

Neighbouring field values (values mapping neighbours to data, representing device interaction) do not exist in , and interaction is only possible through operator $\foldK$. However, a notion of “field-like expression” can be given so that in most cases, the translation of an  expression into  produces a field-like expression if and only if the original expression had field type.

[Local- and Field-Like Expressions]
Let $\e$ be an  valid expression. We say that $\e$ is local-like iff the outcome $\vtree$ of its evaluation $\bsopsem{\deviceId,\deviceId'}{\Trees}{\senstate}{\e}{\vtree}$ does not depend on the neighbour device $\deviceId'$, for any choice of an environment $\Trees$ and current device $\deviceId$. Conversely, we say that $\e$ is field-like iff it is not local-like.

Notice by inspecting rules [E-VAL], [E-REP], [E-FOLD] that any expression $\e$ of the form $\anyvalue$, $\repK (\e) \{\e\}$ or $\foldK(\e)(\e)\{\e\}$ is always local-like (cf. the discussion at the end of <Ref>); $\e(\overline\e)$ can also be local-like assuming that $\e,\body{\e},\overline\e$ are local-like; while an expression $\nbrK\{\e\}$ is field-like unless $\e$ is constantly equal to a certain value (e.g., $\nbrK\{1\}$). This latter example shows that the notion of “field-like” in  does not coincide with “field type” in . However, in both languages a constant $\nbrK$-expression such as $\nbrK\{\anyvalue\}$ can be replaced almost everywhere[More precisely, everywhere in  while in  it needs not to be directly fed to a folding function $\funvalue$ (in which case it would not respect the type signature of $\funvalue$).] with the local expression $\anyvalue$ without changing the meaning of a program, since every local function is implicitly overloaded to accept any combination of local and field parameters.

As we shall see in Theorem <ref>,  is able to simulate conveniently most of the uses of neighbouring field values, but not all of them. In fact, passing field-like values as function arguments cannot be technically done; and even simulating it can be problematic in some corner cases, when:

* The argument to be passed depends on the domain (set of devices) on which it is evaluated. For example, expression $\nbrK \{ \foldK(0)(+)\{1\} \}$ (which counts the number of neighbours) depends on the domain while $\nbrK\{ \texttt{temperature}() + 1 \}$ does not.

* The argument to be passed cannot be constructed with a single $\nbrK$ operation. Notice that expressions like $\nbrK\{\e_1\} + \nbrK\{\e_2\}$ can be rewritten as $\nbrK\{\e_1+\e_2\}$, while $\nbrK\{\xname\}+\texttt{nbrRange}()$ does not. Thus one of the simplest examples failing both (1) and (2) could be:

\[
\texttt{nbrRange}() / \foldK(0)(+)\{1\}
\]

which computes distances with neighbour devices, scaled by the number of the source device's neighbours.

* The argument is folded by the function inside branching statements. Combining this request with the previous ones, we can obtain the following minimal  example:
def restrictedsum(valid, dist)
if (valid)
foldhood(0, +, dist)

restrictedsum( temperature() > 0, nbrRange() / foldhood(0, +, 1) )

of a program whose -behaviour cannot be emulated by any  program.[Without aggregating “field” values into objects of type .] In particular, the following direct  translation of the program fails to reproduce the same behaviour.
def restrictedsum(valid, dist) =
branch (valid)

restrictedsum( temperature() > 0, nbrRange() / foldhood(0)(+)1 )

In fact, the translated  interprets  as a local argument (computed as the distance of a device from itself—that is, zero—divided by the number of its neighbours), which is then multiplied by the number of neighbours with positive temperature; obtaining an output that is constantly zero.

Furthermore, the absence of concrete neighbouring fields values poses some restrictions on which built-in operators are expressible in : non-positional functions on fields, like $\texttt{shufflehood}: \ftypeOf{\type} \to \ftypeOf{\type}$ (which shuffles the values in the range of a field) cannot be defined. Even though these operators are seldom of some use in practice, it still contributes to the class of programs covered by  and not by .

§.§.§ Static semantics

Since field values do not exist in it,  is able to inherit the type system and structure of the host language as is, thus making it possible to implement it as a library. On the other hand,  gives a more expressive type system which need to be implemented as a compiler extension (which is often pragmatically undesirable), and poses additional limitations on allowed constructs.
In particular,  allows the following constructs that are forbidden in :[All of these constructs are inevitably allowed since field types simply does not exist in .]

Functions returning “functions returning fields” Consider such an -function $\funvalue$ re-interpreted in . Since $\funvalue(\e)$ is a function returning fields in , it evaluates to an expression containing either $\nbrK$ or neighbour-aware relational sensor $\snvalue$. If $\funvalue(\e)(\e')$ is not enclosed in a $\foldK$ statement, it is not interpreted as a field in  and no issues can occur. If instead it is enclosed in a $\foldK$ statement, it will be interpreted as a neighbouring field with range restricted to those devices which evaluated $\funvalue(\e)$ to the same function. Since the $\foldK$ statement evaluates its main expression against every available neighbour, its evaluation fails whenever $\funvalue(\e)$ is not the same function in every (connected) device.

These statements might seem practically useless, and are in fact dangerous in some situations. However, they are perfectly acceptable in others (provided that failed terms are “ignored” somehow, as we shall show in the following) hence give additional expressiveness to the language.

Nested $\nbrK$ statements In , nested $\nbrK$ statements (without a folding operator in the middle) would define a “field of fields” and are therefore forbidden. In , an $\nbrK\{\e\}$ statement works as an annotation marking the subexpression $\e$ as “neighbour-sensitive”. Thus nested $\nbrK$ statements are easily allowed: in fact, by carefully inspecting rules [E-NBR], [E-NBR-LOC] it is apparent that in nested $\nbrK$ statements the inner $\nbrK$ can be removed without changing the meaning of the expression.
This flexibility can also allow for increased code reuse. For instance, consider the following function:
def st() =

Translated in , this function would compute a field of neighbour's temperatures scaled by a certain sensitivity. In , we have two additional uses for this function:

* If $\texttt{st}$ is not enclosed into a $\foldK$, it will just compute the current device's temperature scaled by sensitivity;

* If $\texttt{st}$ is directly enclosed into a $\foldK$, it is interpreted as in : e.g., $\foldK(0)(\texttt{+})\{\texttt{st}()\}$ computes the sum of temperatures of neighbours scaled by the device's sensitivity;

* If $\texttt{st}$ is enclosed in another $\nbrK$, as in $\foldK(0)(\texttt{+})\{\nbrK\{\texttt{st}()\}\}$, it computes the field of temperatures of neighbours each scaled by its own sensitivity.

Thus nested $\nbrK$-statements increase language expressiveness by enhancing code reusability, at the cost of an additional complexity: using such features requires deep understanding of the underlying semantics.

Capturing variables of field type In  anonymous function definitions cannot contain variables of field type. The following example of such an expression $\e$ is given in audrito2019tocl:
((x) => pickHood(nbr() => minHood(x + nbrmid)))(nbrmid)()

In  such expressions are interpreted as all variables $\xname$ had local status, and are only later substituted pointwise with a field-like expression (i.e., containing $\nbrK$).

For instance, let us consider how an expression like $\foldK(0)(\texttt{+})\{\e\}$ would be interpreted in  on a device $\deviceId$. First, $\e$ is evaluated against no neighbour leading to the partially evaluated expression:
pickHood(nbr() =>

Then pickHood is called[Even though pickHood and minHood do not exist in , we treat them as shortcuts for the corresponding $\foldK$ statements.] against every neighbour (no alignment has yet occurred). Each neighbour's value-tree has a different copy of the anonymous function with its own $\deviceId'$. Thus the expression evaluates to:
(() =>

for some random $\deviceId'$. In order to perform the function application, the environment $\Trees$ is then restricted to only those neighbours which randomly picked the same $\deviceId'$ (possibly none). Then minHood is evaluated in such restricted environment, returning $\deviceId' + \deviceId''$ where $\deviceId''$ is the least neighbour which also picked $\deviceId'$.

Afterwards, $\e$ is evaluated against every neighbour $\deviceId'$ leading to the partially evaluated expression:
pickHood(nbr() =>

As before no alignment as yet occurred, and the evaluation proceeds similarly.

It is now clear that the above expression does not produce runtime errors in , even though its behaviour is unnatural and likely not very useful in practice. This observation leads to the following style guideline: avoid moving anonymous functions which capture variables between devices. In fact, we obtain unnatural behaviour even if the captured variables are of “local” type (a possibility that is allowed by ).

§.§ Translating HFC into  with Concrete Fields

Figure <ref> provides a translation of  programs into , showing that the latter is at least as expressive as the former. Since in both cases tags $\name$ are added when evaluation starts, we did not include them into the translation. Notice that we did not provide a translation for neighbouring field values: however, this is not an issue since these values are not allowed to appear in  source programs but only at intermediate stages of their evaluation. The only non-trivial translation rules in Figure <ref> are that for variables $\xname$ and $\nbrK$-expressions $\nbrK\{\e\}$. The rule for variables injects a call to a function $\mathtt{align}$, which reduces the domain of a value of type $\ftypeOf{\type}$ to the current domain of evaluation $\domof{\Trees}$ without changing its values. The rule for $\nbrK$-expressions relies on several components:

* both  basic constructs $\nbrK$ and $\foldK$;

* the type $\mathtt{ID}$ and the built-in function $\mathtt{mid}$ of type $() \rightarrow \mathtt{ID}$, which returns the identifier of the current
device;[Bot the  function $\mathtt{mid}$ and the type  $\mathtt{ID}$ are available in the standard  library.]

* the type $\ftypeOf{\type}$ for every type $\type$,[This type is implemented in the  standard library upon the
built-in class $\mathtt{Map[ID,\type]}$.] endowed with:

* for each natural $n$: the constructor $\mathtt{Field}_n$
of type scheme $\forall t.(\mathtt{ID},t,...,\mathtt{ID},t)\rightarrow\ftypeOf{t}$
such that $\mathtt{Field}_n(\deviceId_1, \anyvalue_1, \ldots, \deviceId_n, \anyvalue_n)$
builds a $\ftypeOf{\type}$ value representing $\envmap{\deviceId_1}{\anyvalue_1},...,\envmap{\deviceId_n}{\anyvalue_n}$; and
the built-in function $\mathtt{field}_n$ of the same type scheme
such that $\mathtt{field}_n(\deviceId_1, \anyvalue_1, \ldots, \deviceId_n, \anyvalue_n)$ returns
$\mathtt{Field}_n(\deviceId_1, \anyvalue_1, \ldots, \deviceId_n, \anyvalue_n)$;

* the union operator $\texttt{++}$ of type scheme  $\forall t.(\ftypeOf{t},\ftypeOf{t}) \rightarrow \ftypeOf{t}$,
such that

\[
\begin{array}{r}
\texttt{++}(\mathtt{Field}_p(\deviceId_1, \anyvalue_1, \ldots, \deviceId_p, \anyvalue_p),
\mathtt{Field}_q(\deviceId'_1, \anyvalue'_1, \ldots, \deviceId'_q, \anyvalue'_q)) \; = \mbox{$\qquad\qquad\qquad\qquad$}
\\
\mathtt{Field}_{p+q}(\deviceId_1, \anyvalue_1, \ldots, \deviceId_p, \anyvalue_p,\deviceId'_1, \anyvalue'_1, \ldots, \deviceId'_q, \anyvalue'_q).
\end{array}
\]

\begin{align*}
\trans{S}{\overline{\FUNCTION}  \; \e} ~&\triangleq~ \trans{S}{\overline\FUNCTION} \trans{S}{\e} \\
\trans{S}{\defK \; \fname (\overline{\xname}) \; \{\e\}} ~&\triangleq~ \defK \; \fname (\overline{\xname}) \; \eqSymK{\trans{S}{\e}} \\
\trans{S}{\xname} ~&\triangleq~ \mathtt{align}(\xname) \\
\trans{S}{\e} ~&\triangleq~ \e \quad \text{for } \e = \bname, \fname \\
\trans{S}{\dcOf{\dc}{\overline{\lvalue}}} ~&\triangleq~ \dcOf{\dc}{\trans{S}{\overline{\lvalue}}} \\
\trans{S}{(\overline{\xname}) \; \toSym{} \; \e} ~&\triangleq~ (\overline{\xname}) \; \toSymKtag{}{\trans{S}{\e}} \\
\trans{S}{\e(\overline{\e})} ~&\triangleq~ \trans{S}{\e}(\trans{S}{\overline\e}) \\
\trans{S}{\repK(\e)\{ (\xname) \;\texttt{=>}\; \e \}} ~&\triangleq~ \repK(\e)\{ (\xname) \; \toSymKtag{}{\trans{S}{\e}} \} \\
\trans{S}{\nbrK\{\e\}} ~&\triangleq~ \foldK(\mathtt{Field}_0())(\texttt{++})\{\nbrK\{\mathtt{field}_1(\mathtt{mid}(), \trans{S}{\e})\}\}
\end{align*}

Translation function $\trans{S}{\cdot}$ of  programs into .

This translation preserves the types of expressions and program behaviour.

Let $\PROGRAM_H$ be a well-typed  program, and let $\PROGRAM_S = \trans{S}{\PROGRAM_H}$ be obtained by applying the translation in Figure <ref>. Assume that every built-in operator of  is available in  either as built-in or defined function.
Then $\PROGRAM_S$ is a well-typed  program and $\bsopsem{\deviceId}{\Trees}{\senstate}{\emain}{\vtree}$ holds for  if and only if $\bsopsem{\deviceId,\deviceId}{\Trees}{\senstate}{\emain}{\vtree}$ holds for .

First, notice that Rules [E-VAL], [E-B-APP], [E-D-APP] and [E-REP] are identical in  and , except for the presence of $\deviceId'$ (which is however ignored by all those rules). The  rule [E-FLD] (which reduces a field value to the current domain) is fully simulated by the insertion of calls to $\mathtt{align}$ around every variable $\xname$: in fact, a field value can have a domain larger than the current domain only when it is passed as argument to a function. Finally, the  rule [E-NBR] is correctly simulated by $\trans{S}{\nbrK\{\e\}}$ in , as it unites together the singleton fields $\fvalue_i = \envmap{\deviceId_i}{\anyvalue_i}$ corresponding to the values $\anyvalue_i$ of $\e$ in each neighbour $\deviceId_i$.

We remark that the commonly used  built-in operator on fields are always expressible in terms of two basic functions:

* $\mathtt{fmap}_i: ((\overline\type) \rightarrow \type, \ftypeOf{\overline\type}) \rightarrow \ftypeOf{\type}$, which applies its first argument pointwise on its following arguments;

* $\mathtt{freduce}: ((\type, \type) \rightarrow \type, \ftypeOf{\type})$, which combines all values in its second argument according to the binary function given as first argument.

Both of these operators are easily implemented in .

§.§ Embedding Field Computations in a Host Language

A first key problem in embedding field computations in a host language lies in the potential mismatch between the representation of local values (values of local, standard types) and the representation of field expressions.

For the former, one would seek for the natural representation of the host language,  e.g., literal  representing a local value of type .

For the latter, one has to combine the natural representation with the additional constructs manipulating fields; namely,  as in field calculus, literal  (or some variation) should represent a computational field equal to $1$ in all space-time points of the local device's neighbourhood: this should in principle be given a type type , inheriting all the operations one would use over the local counterpart  (, , and so on), since in field calculus  is the sum of two fields giving a field of $3$ in all space-time points.

As a consequence, standard types such as numbers, Booleans, characters, objects, and the corresponding operators, need to be coherently lifted in order to work under the field interpretation.

That is, given any type , the type  should support all the operations provided by  but lifted to the field context:

for instance, expression $\texttt{e}_1+\texttt{e}_2$ where $\texttt{e}_1$ and $\texttt{e}_2$ have type  should naturally give an element of type .

Ideally, the type system should continue to do its job with field types, and field expressions should be written in a notation which is analogously simple as the local counterpart.

A second key problem stems from the declarativeness and compositionality of field computations: the host language should provide the means for defining blocks of code
and for controlling when and how these are executed, mainly by deferring their evaluation until a later time and properly contextualising them to the local information available in each device.

These mechanisms should also be lightweight so as to keep the impact on the user-side of the DSL as little as possible.

For instance, using Java as host language would require many expression to be wrapped in a 0-ary lambda, which would clutter code.

The third, key technical difficulty is to properly deal with the interaction model of field computations, which is neighbour-driven.

Field computations are equipped with a (logical or physical) notion of neighbourhood that basically expresses the boundary of direct communication, i.e., what devices can be reached by a given device through a communication act occurring in a certain position of computation.

The observation of values that a device reads from its neighbours is typically modelled by reification into a neighbouring value (a map from neighbours to values), which can be manipulated functionally until being collapsed back to a local value by means of some folding operator—e.g., computing the minimum value.

This requires one to explicitly differentiate, syntactically and semantically, the two classes of types, neighbouring types and local types, raising the issue of how to lift standard local operators to neighbour types.

Thanks to the features of the Scala programming language, and as detailed in this paper,  handles this problem with a twist:

* the same type, say , is used both for local types and neighbouring types;

* the notion of computation over neighbouring values is semantically turned into a notion of computation “against” a neighbour (namely, a computation whose outcome depends on recent result of computation in that neighbour), hence there is no longer need of two kinds of type;

* folding operations are the triggers for a universal quantification process, iterating computations against all pertinent neighbours.

Such changes, impacting theory and practice of field computations as described in this paper, enable expressive and smooth integration with Scala programming.