names  X  x, y, z, u, v, w
locations  L  p, q, l
π-terms  P, Q ::= x(y).P | \overline{x} < y > .P | νx.P | P |Q | P + Q |!P | 0
placement  Γ : X → L written as set {x▷p, y▷q, … }

Γ.x▷p is Γ extended with placing x▷p

Γ + Γ′ ::= Γ ∪ Γ′ iff ∀x ∈ dom(Γ) ∩ dom(Γ′).Γ(x) = Γ′(x)

placed π-term Δ; Γ ⊢ P with fn(P) ⊆ dom(Γ) and cod(Γ) ⊆ Δ ⊆ L

placing rules

(New)  \frac{Δ; Γ.x▷p ⊢ P}{Δ; Γ ⊢ νx.P}  (eNull) Δ; Γ ⊢ 0  \frac{Δ; Γ ⊢ P}{Δ; Γ ⊢ !P} (eBang)
(In)  \frac{Δ.q; Γ.x▷p.y▷q ⊢ P}{Δ; Γ.x▷p ⊢ x(y).P}  \frac{Δ; Γ ⊢ P  Δ′; Γ′ ⊢ Q}{Δ ∪ Δ′; Γ + Γ′ ⊢ P |Q}  (Par)
(Out) \frac{Δ; Γ.x▷p.y▷q ⊢ P}{Δ; Γ.x▷p ⊢ \overline{x} < y > .P}  \frac{Δ; Γ ⊢ P  Δ′; Γ′ ⊢ Q}{Δ ∪ Δ′; Γ + Γ′ ⊢ P + Q}  (Sum)

Figure 1: The located π-calculus

1 Motivation

The starting point is the λ − dist calculus from Sekiguchi and Yonezawa. This calculus can be seen as a formalisation of distributed computing. This is done in two steps. First encoding of code mobility by enriching the lambda-calculus by locations p and new expressions go and < e > as formation of a movable packet of code. The new redex go p moves the smallest enclosing packet to the location p.

The second step is encoding of data mobility. This is done by introducing variables and a recursive defined movement of data associated with code movement.

The following tries to look at distributed computing even more fundamental. To have distribution in the lambda-calculus you have to introduce the new notions location and mobility. The π-calculus offers already a notion of mobility. In the following a notion of location is introduced into the π-calculus by a type discipline similar to the sorting of π-calculus. In fact the typing discipline is simpler than sorting and it is orthogonal to sorting.

A very interesting result would be how to encode λ − dist (and the various features of distributed computing as found in Oblique, Facile, Java) in the located π-calculus.

It looks promising to use type checking for analysis of behaviour of distributed algorithms. On the implementation side the location type discipline would we useful to add in the PICT language.

2 The system

Theorem (fixed location property): If a process P can be located as Δ; Γ ⊢ P and P reduces to Q (i.e. P ⟶^{∗} Q) then Q can also be located as Δ; Γ ⊢ Q. proof: Simple corollary of the similar property for the explicit located π-calculus.□

The explicit located π-calculus is given by annotating every name in the πcalculus with a location. So explicit located pre-processes are given by the following grammar:

R, S ::= x▷p(y▷q)R | \overline{x▷p} < y▷q > .R | νx▷p.R | R|S | R + S |!R | 0

The derivation for an explicit located process Δ; Γ ⊢ R can be obtained by the following rule system. The rule system is gained by simply annotating the processes with locations.

(eNew)  \frac{Δ; Γ.x▷p ⊢ R}{Δ; Γ ⊢ νx▷p.R}  (eNull) Δ; Γ ⊢ 0  \frac{Δ; Γ ⊢ R}{Δ; Γ ⊢ !R} (eBang)
(eIn)  \frac{Δ.q; Γ.x▷p.y▷q ⊢ R}{Δ; Γ.x▷p ⊢ x▷p(y▷q)R}  \frac{Δ; Γ ⊢ R  Δ′; Γ′ ⊢ S}{Δ ∪ Δ′; Γ + Γ′ ⊢ R|S}  (ePar)
(eOut) \frac{Δ; Γ.x▷p.y▷q ⊢ R}{Δ; Γ.x▷p ⊢ \overline{x▷p} < y▷q > .R}  \frac{Δ; Γ ⊢ R  Δ′; Γ′ ⊢ S}{Δ ∪ Δ′; Γ + Γ′ ⊢ R + S}  (eSum)

Proposition (derivation correspondence): To every explicitly located preprocess R there exists either a unique derivation d_{R} : Δ; Γ ⊢ R with Γ = fn(P) and Δ = cod(Γ) or there is no derivation at all for R. proof: simple structural induction on the structure of pre-process R. □

The reaction is location conscious. Communication is only allowed with names located at the same place. Further locations are passed during a reaction.

(ereact) R′ + \overline{x▷p} < y▷q > .R | x▷p(z▷l).S + S′ ⟶ R|S[y/x, q/l]

The reaction has to be extended on contexts :

\begin{aligned}& C ::= [ ] | C|R | νx▷p.C \\ (ereact) & \frac{R ≡ C[S]  S → S′  C[S′] ≡ R′}{R → R′} \end{aligned}

The connection between the implicit and the explicit located π-calculus can be stated by the erasure operation |.| so that P = |R| is the implicit process gained from the explicit process by erasing all location annotations from R.

\begin{aligned}|x▷p(y▷q)R| & = & x(y).|R| & |\overline{x▷p} < y▷q > .R| & = & \overline{x} < y > .|R| \\ |R|S| & = & |R| | |S| & |R + S| & = & |R| + |S| \\ |νx▷p.R| & = & νx.|R| & |0| & = & 0 \end{aligned}

The erasure can be extended on rules and on derivations.

Proposition (soundness) If the explicit located process Δ; Γ ⊢ R can be derived in the rule system, then the implicit located process Δ; Γ ⊢ |R| can be derived proof: Assume d is the derivation of Δ; Γ ⊢ R then apply the erasure on the derivation. |d| is the derivation of Δ; Γ ⊢ |R| shown by structural induction on d.□

Proposition (completeness): Given a derivation d : Δ; Γ ⊢ P of an implicit located process there there exists a derivation d^{∗} : Δ; Γ ⊢ R of an explicit located process such that |d^{∗}| = d. proof: Annotate every free name x ∈ fn(P) by the location Γ(x) and annotate every bound name by a fresh location. This annotation operation gives an explicit pre-term P^{∗}. to complete the proof We take P^{∗} for R and apply the “derivation correspondence” proposition to get the derivation d_{P^{∗}} : Δ; Γ ⊢ P^{∗}. The proof is done by induction on the derivation d. □

The annotation of location in the explicit calculus doesn’t restrict the reaction. Proposition (well located): Given an explicit located process Δ; Γ ⊢ R then every redex R ≡ C[R′ + \overline{x▷p′} < y▷q > .R|x▷p(z▷l).S + S′] has satisfies p′ = p.

Proposition (reaction correspondence): The located processes P and P^{∗}

(a) or the located processes R and |R| correspond by reaction.

(a) If P → Q there is a reaction P^{∗} → R such that Q = |R|.

(b) If R → S there is a reaction |R| → P such that |R| = P.

proof: Apply “well located” proposition. □

Definition A location substitution θ : Δ → Δ′ is a map of locations. By structural induction we define the application θR of a location substitution θ on an explicit pre-process R as renaming of the location annotations. We extend the operation of θ on derivations d : Δ; Γ ⊢ R of explicit located processes to get a new derivation θd : Δ′; Γ ⊢ θR.

A placing substitution ϕ : Δ; Γ → Δ′; Γ′ consists of a locations substitution θ_{ϕ} : Δ → Δ′ and a map on the placement names ϕ_{X} : dom(Γ) → dom(Γ′) which respects the location substitution θ(Γ(x)) = Γ′(ϕ_{X} (x)). We define by structural induction the application ϕR of placing substitution ϕ on an explicit pre-term R as a renaming of the location annotations and names of R. The operation of ϕ is extended on a derivation d : Δ; Γ ⊢ R to get a new derivation ϕd : Δ′; Γ′ ⊢ ϕR.

Proposition (subject reduction) Given an explicit located term Δ; Γ ⊢ R if the process reacts as R → S then S is a located term Δ; Γ ⊢ S. proof: We haven to prove placing is invariant under structural equivalence ≡. This is an easy structural on derivation for every case of ≡ equation.

The prove for the invariance under reaction by observing that the reaction

(ereact) R′ + \overline{x▷p} < y▷q > .R|x▷p(z▷l).S + S′ ⟶ R|S[y/x, q/l]

uses an operation [y/z, q/l] which is in fact a placing substitution. So the definition above applies to get a new derivation for the reading process S. □

To put all things together we can prove the ”fixed location” theorem. Take a implicit located process Δ; Γ ⊢ P and a reaction P → Q then P^{∗} is a explicit located process which reactions corresponds to P. So there is a reaction P^{∗} → R with |R| = Q. Now we apply the ”subject reduction” lemma on R to get an explicit located process d : Δ; Γ ⊢ R. Applying the erasure operation on this derivation we get the desired result |d| : Δ; Γ ⊢ |R| = Q □.