lemmatheoremlemma corollarytheoremcorollary propositiontheoremproposition
exampletheoremexample definitiontheoremdefinition conventiontheoremconvention
remarktheoremremark notationtheoremnotation

# Compilation of Coordinated Choice

Yuki Nishida  Atsushi Igarashi

###### Abstract

Recently, we have proposed _coordinated choices_ , which are nondeterministic
choices equipped with names. The main characteristic of coordinated choices is
that they synchronize nondeterministic decision among choices of the same
name.

The motivation of the synchronization mechanism is to solve a theoretical
problem. So, as a practical programming language, we still want to use
coordinated choices like standard ones. In other words, we want to avoid
synchronization. Now, there are two problems: (i) practically, it is a bit
complicated work to write a program using coordinated choices in which
execution synchronization never happens; and (ii) theoretically, it is unknown
whether any programs using standard choices can be written by using only
coordinated ones.

In this paper, we define two simply typed lambda calculi called
$\lambda^{\parallel}$ equipped with standard choices and
$\lambda^{\parallel\omega}$ equipped with coordinated choices, and give
compilation rules from the former into the latter. The challenge is to show
the correctness of the compilation because behavioral correspondence between
expressions before and after compiling cannot be defined directly by the
compilation rules. For the challenge, we give an effect system for
$\lambda^{\parallel\omega}$ that characterizes expressions in which execution
synchronization never happens. Then, we show that all compiled expressions can
be typed by the effect system. As a result, we can easily show the correctness
because the main concern of the correctness is whether synchronization happens
or not.

##  1 Introduction

_Nondeterministic choice_ , written $(M_{{\mathrm{1}}}\parallel
M_{{\mathrm{2}}})$ in this paper, is a rather well-known construct formalizing
nondeterministic computation. Nondeterminism is typically accomplished by the
following two operational rules: $(M_{{\mathrm{1}}}\parallel
M_{{\mathrm{2}}})\longrightarrow M_{{\mathrm{1}}}$ and
$(M_{{\mathrm{1}}}\parallel M_{{\mathrm{2}}})\longrightarrow
M_{{\mathrm{2}}}$. So, for example, $(1\parallel 2)+(3\parallel 4)$ is
evaluated into one of the three possible values: $4,5,6$.

Recently, we had proposed _coordinated choices_ [4], written
$(M_{{\mathrm{1}}}\parallel^{\Phi}M_{{\mathrm{2}}})$. It is a kind of
nondeterministic choice but equipped with a name $\Phi$. The characteristic
point of coordinated choices is that nondeterministic evaluation is
synchronized among choices of the same name. That means, for instance,
$(1\parallel^{\mathsf{A}}2)+(3\parallel^{\mathsf{A}}4)$ only results $4,6$.
The essential purpose of developing coordinated choices is to solve a
theoretical problem that happens when we try to introduce nondeterministic
choices into a dependently typed system. In other words, the proposed system
does not have nondeterministic choices.

Now, it is a natural and important demand for practically and theoretically,
how we use coordinated choices like standard ones. In this paper, we consider
how to simulate usual choices with coordinated choices. Concretely, we give a
compilation algorithm from a simply typed lambda calculus with
nondeterministic choices into one with coordinated choices; and show an
evaluation in the former calculus is simulated by the latter calculus, and
vice versa.

##  2 Compilation

In this section, we introduce the compilation rules and discuss the
correctness of the given rules. First of all, we recall how a coordinated
choice is synchronized. The following is an example of a reduction sequence in
which synchronization happens.

$\displaystyle\mathtt{add}\,(1\parallel^{\mathsf{A}}2)\,(3\parallel^{\mathsf{A}}4)$
$\displaystyle\mathrel{\overset{\varnothing}{\longrightarrow}{}^{\ast}}{}(\mathtt{add}\,1\parallel^{\mathsf{A}}\mathtt{add}\,2)\,(3\parallel^{\mathsf{A}}4)$
$\displaystyle\mathrel{\overset{\varnothing}{\longrightarrow}{}^{\ast}}{}(\mathtt{add}\,1\,(3\parallel^{\mathsf{A}}4)\parallel^{\mathsf{A}}\mathtt{add}\,2\,(3\parallel^{\mathsf{A}}4))$
$\displaystyle\mathrel{\overset{\varnothing}{\longrightarrow}{}^{\ast}}{}(\mathtt{add}\,1\,3\parallel^{\mathsf{A}}\mathtt{add}\,2\,4)$
$\displaystyle\mathrel{\overset{\varnothing}{\longrightarrow}{}^{\ast}}{}(4\parallel^{\mathsf{A}}6)$

In the previous work, we had made two design decision to formalize
nondeterministic choices. One is that we express the possibility of execution
as of the form of a choice rather than branches of reduction sequences as we
have seen in Section 1. So, the result of execution above becomes the choice,
which expresses the possible results are only 4 and 6. Another is that we
adopt _call-time_ semantics [1], which makes nondeterministic choice happening
before a function call. The distribution of the first argument for add in the
first line, for example, accomplishes this semantics.

The devices that enable synchronization are following rules, which are used in
the evaluation from the second line to the third line.

$M_{{\mathrm{1}}}\mathrel{\overset{\Delta\cup\\{\Phi_{+}\\}}{\longrightarrow}}M^{\prime}_{{\mathrm{1}}}$
$(M_{{\mathrm{1}}}\parallel^{\Phi}M_{{\mathrm{2}}})\mathrel{\overset{\Delta}{\longrightarrow}}(M^{\prime}_{{\mathrm{1}}}\parallel^{\Phi}M_{{\mathrm{2}}})$
$M_{{\mathrm{1}}}\mathrel{\overset{\Delta\cup\\{\Phi_{+}\\}}{\longrightarrow}}M^{\prime}_{{\mathrm{1}}}$
$(M_{{\mathrm{1}}}\parallel^{\Phi}M_{{\mathrm{2}}})\mathrel{\overset{\Delta\cup\\{\Phi_{+}\\}}{\longrightarrow}}M_{{\mathrm{1}}}$

So, concentrating on one step of an evaluation, we can easily find that a
sufficient condition to prevent synchronization is that every name of choices
in an expression before the evaluation is distinct. However, this condition is
easily broken by evaluation since some reduction rules, e.g., $(\lambda
x.M)\,V\mathrel{\overset{\Delta}{\longrightarrow}}M[x\coloneq V]$, duplicate
an expression. In other words, it is easy to prevent synchronization in the
first step of an evaluation, but it is hard to prevent synchronization in
every step after the first step of an evaluation.

The following reduction sequence shows synchronization caused by duplication
of an expression. In the first line, recursive call of $f$ duplicates the name
$A$.

$\displaystyle(\mu f.\lambda x.(f\,x\parallel^{\mathsf{A}}f\,x))\,0$
$\displaystyle\mathrel{\overset{\varnothing}{\longrightarrow}{}^{\ast}}{}(f^{\prime}\,0\parallel^{\mathsf{A}}f^{\prime}\,0)$
$\displaystyle\mathrel{\overset{\varnothing}{\longrightarrow}{}^{\ast}}{}((f^{\prime}\,0\parallel^{\mathsf{A}}f^{\prime}\,0)\parallel^{\mathsf{A}}(f^{\prime}\,0\parallel^{\mathsf{A}}f^{\prime}\,0))$
$\displaystyle\mathrel{\overset{\varnothing}{\longrightarrow}{}^{\ast}}{}(f^{\prime}\,0\parallel^{\mathsf{A}}f^{\prime}\,0)\mathrel{\overset{\varnothing}{\longrightarrow}{}^{\ast}}{}\dots,$
where $f^{\prime}=\mu f.\lambda x.(f\,x\parallel^{\mathsf{A}}f\,x)$.

To avoid the synchronization, the proposed system also has name abstraction
mechanism, i.e., name abstractions $\Lambda\alpha.M$; name applications
$M\,\Phi$; and name concatenations $\Phi_{{\mathrm{1}}}\Phi_{{\mathrm{2}}}$.
Fortunately, thanks to call-by-value semantics, names that will be duplicated
and become a cause of synchronization only occur in the body of lambda
abstractions. So we abstract names (giving a name containing variables)
occurring in the body of lambda abstractions and instantiate the names as
distinct ones where the lambda abstractions are called. The following two
evaluation sequences show the effect of this idea.

$\displaystyle(\mu f.\lambda
x.\Lambda\alpha.(f\,x\,\alpha\mdwhtcircle\parallel^{\alpha}f\,x\,\alpha\mdblkcircle))\,0\,\mdwhtcircle$
$\displaystyle\mathrel{\overset{\varnothing}{\longrightarrow}{}^{\ast}}{}$
$\displaystyle(f^{\prime}\,0\,\mdwhtcircle\mdwhtcircle\parallel^{\mdwhtcircle}f^{\prime}\,\mdwhtcircle\mdblkcircle)$
$\displaystyle\mathrel{\overset{\varnothing}{\longrightarrow}{}^{\ast}}{}$
$\displaystyle((f^{\prime}\,0\,\mdwhtcircle\mdwhtcircle\mdwhtcircle\parallel^{\mdwhtcircle\mdwhtcircle}f^{\prime}\,0\,\mdwhtcircle\mdwhtcircle\mdblkcircle)\parallel^{\mdwhtcircle}(f^{\prime}\,0\,\mdwhtcircle\mdblkcircle\mdwhtcircle\parallel^{\mdwhtcircle\mdblkcircle}f^{\prime}\,0\,\mdwhtcircle\mdblkcircle\mdblkcircle)),$
where $f^{\prime}=\mu f.\lambda
x.\Lambda\alpha.(f\,x\,\alpha\mdwhtcircle\parallel^{\alpha}f\,x\,\alpha\mdblkcircle)$.

In the first sequence, the duplicated name $\Phi$ causes synchronization. In
the second sequence, on the other hand, the name of a coordinated choice
becomes different one at every time that a lambda abstraction is applied (so
synchronization does not happen).

$\displaystyle\lBrack x\rBrack^{\alpha}_{\bar{\Phi}}$ $\displaystyle=x$
$\displaystyle\lBrack
e_{{\mathrm{1}}}\,e_{{\mathrm{2}}}\rBrack^{\alpha}_{\bar{\Phi}}$
$\displaystyle=\lBrack
e_{{\mathrm{1}}}\rBrack^{\alpha}_{\bar{\Phi}\mdwhtcircle\mdwhtcircle}\,\lBrack
e_{{\mathrm{2}}}\rBrack^{\alpha}_{\bar{\Phi}\mdwhtcircle\mdblkcircle}\,\alpha\bar{\Phi}\mdblkcircle$
$\displaystyle\lBrack\lambda x.e\rBrack^{\alpha}_{\bar{\Phi}}$
$\displaystyle=\lambda x.\Lambda\beta.\lBrack e\rBrack^{\beta}_{\bar{\Phi}}$
$\displaystyle\lBrack\mu f.e\rBrack^{\alpha}_{\bar{\Phi}}$ $\displaystyle=\mu
f.\lBrack e\rBrack^{\alpha}_{\bar{\Phi}}$
$\displaystyle\lBrack(e_{{\mathrm{1}}}\parallel
e_{{\mathrm{2}}})\rBrack^{\alpha}_{\bar{\Phi}}$ $\displaystyle=(\lBrack
e_{{\mathrm{1}}}\rBrack^{\alpha}_{\bar{\Phi}\mdwhtcircle}\parallel^{\alpha\bar{\Phi}\mdblkcircle}\lBrack
e_{{\mathrm{2}}}\rBrack^{\alpha}_{\bar{\Phi}\mdwhtcircle})$ Figure 1:
Compilation of expressions

Summing up the discussion, concrete compilation rules become the ones in
Figure 1. The function $\lBrack\cdot\rBrack^{\alpha}_{\omega}$ gives the
compilation, where $\alpha$ and $\omega$ are additional parameters, called
_seeds_ , used for generating distinct names during a compilation. Note that
the same seeds are given for the sub-expressions’ compilation of a choice. It
does not cause a problem because the left and right sides of a choice are
completely separated, i.e., the sub-expressions never collaborate.

###  2.1 Correctness of compilation

The main contribution of this paper is that we have formally shown that the
compilation is _correct_. Informally, correctness of a compilation is stated
as—a compiled expression behaves the same as the original expression does.
This behavioral correspondence between compiled expressions and original
expressions is formally defined as a binary relation, called _bisimulation_
[2], between them. For instance, if we use the compilation rules as the
relation, what we need to show is stated as the following two propositions.

######  Proposition .

If $\lBrack e\rBrack^{\alpha}_{\bar{\Phi}}=M$ and $e\longrightarrow
e^{\prime}$, then
$M\mathrel{\overset{\Delta}{\longrightarrow}{}^{\ast}}M^{\prime}$ and $\lBrack
e^{\prime}\rBrack^{\alpha}_{\bar{\Phi}}=M^{\prime}$.

######  Proposition .

If $\lBrack e\rBrack^{\alpha}_{\bar{\Phi}}=M$ and
$M\mathrel{\overset{\Delta}{\longrightarrow}}M^{\prime}$, then
$e\longrightarrow^{\ast}e^{\prime}$ and $\lBrack
e^{\prime}\rBrack^{\alpha}_{\bar{\Phi}}=M^{\prime}$.

However, we can easily find a counter-example for the reduction $(\lambda
x.x)\,\lambda x.x\longrightarrow\lambda x.x$ as follows.

$\displaystyle\lBrack(\lambda x.x)\,\lambda x.x\rBrack^{\alpha}_{\bar{\Phi}}$
$\displaystyle=\lBrack\lambda
x.x\rBrack^{\alpha}_{\bar{\Phi}\mdwhtcircle\mdwhtcircle}\,\lBrack\lambda
x.x\rBrack^{\alpha}_{\bar{\Phi}\mdwhtcircle\mdblkcircle}\,\alpha\bar{\Phi}\mdblkcircle$
$\displaystyle=(\lambda x.\Lambda\beta.x)\,\lBrack\lambda
x.x\rBrack^{\alpha}_{\bar{\Phi}\mdwhtcircle\mdblkcircle}\,\alpha\bar{\Phi}\mdblkcircle\overset{\Delta}{\longrightarrow}\lBrack\lambda
x.x\rBrack^{\alpha}_{\bar{\Phi}\mdwhtcircle\mdblkcircle}$

A seed is alternated by the reduction. Unfortunately, weakening the
proposition as follows does not help us, because, if a sub-expression (for
example, the argument part of an application) is evaluated, only the seed for
the sub-expression part is alternated and the whole expression after the
evaluation does not follow the compilation rule.

######  Proposition .

If $\lBrack e\rBrack^{\alpha}_{\bar{\Phi}}=M$ and $e\longrightarrow
e^{\prime}$, then $M\mathrel{\overset{\Delta}{\longrightarrow}}M^{\prime}$ and
$\lBrack e^{\prime}\rBrack^{\alpha}_{\bar{\Phi}^{\prime}}=M^{\prime}$ for some
$\bar{\Phi}^{\prime}$.

Ultimately, we believe that the relation cannot be obtained directly by a
compilation algorithm. That means it is not because of how the compilation
rules are defined. To prevent coordination of coordinated choice, we need to
give distinct names for each coordinated choice, which is a sub-expression,
but as we have seen in the counter-example, a sub-expression could pop-up to
the top level, which leads us to an inconsistency.

Summarizing the discussion, we could see that coordination does not happen in
the first step of the evaluation for a complied expression; but we cannot
guarantee the property after the first step because an expression can have no
relation to the compilation rules. So, we take another indirect strategy.
Firstly, we define a relation characterizing expressions that do not cause
coordination and is preserved by an evaluation, and then we show the image of
the compilation is included in the relation. After accomplishing this, we can
easily obtain a bisimulation relation since the compilation just inserts name
abstractions and applications—an evaluation after compilation just involves
(R-Sigma) reduction in some points.

##  3 Formal System

We formalize the idea as $\lambda^{\parallel}$, a simply typed lambda calculus
with a fix-point operator and _non-collapse_ choices, and
$\lambda^{\parallel\omega}$, a simply typed lambda calculus with a fix-point
operator and coordinated choice; and give a compilation rule from the former
to the latter.

###  3.1 Source Language: $\lambda^{\parallel}$

$T$ | $\Coloneq$ |  $\mathrm{nat}$ $|$ $T_{{\mathrm{1}}}\rightarrow T_{{\mathrm{2}}}$
---|---|---
$e$ | $\Coloneq$ |  $x$ $|$ $e_{{\mathrm{1}}}\,e_{{\mathrm{2}}}$ $|$ $\lambda x.e$ $|$ $\mu f.e$ $|$ $(e_{{\mathrm{1}}}\parallel e_{{\mathrm{2}}})$
$\Gamma$ | $\Coloneq$ |  $\varnothing$ $|$ $\Gamma,x\mathord{:}T$
$v$ | $\Coloneq$ |  $\lambda x.e$
Figure 2: Syntax of $\lambda^{\parallel}$

$(\lambda x.e)\,v\longrightarrow e[x\coloneq v]$ (SR-Beta)

$\mu f.\lambda x.e\longrightarrow(\lambda x.e)[f\coloneq\mu f.\lambda x.e]$
(SR-Fix)

$(e_{{\mathrm{11}}}\parallel
e_{{\mathrm{12}}})\,e_{{\mathrm{2}}}\longrightarrow(e_{{\mathrm{11}}}\,e_{{\mathrm{2}}}\parallel
e_{{\mathrm{12}}}\,e_{{\mathrm{2}}})$ (SR-DistAppL)

$v\,(e_{{\mathrm{21}}}\parallel
e_{{\mathrm{22}}})\longrightarrow(v\,e_{{\mathrm{21}}}\parallel
v\,e_{{\mathrm{22}}})$ (SR-DistAppR)

$e_{{\mathrm{1}}}\longrightarrow e^{\prime}_{{\mathrm{1}}}$ (SR-AppL)
$e_{{\mathrm{1}}}\,e_{{\mathrm{2}}}\longrightarrow
e^{\prime}_{{\mathrm{1}}}\,e_{{\mathrm{2}}}$ $e_{{\mathrm{2}}}\longrightarrow
e^{\prime}_{{\mathrm{2}}}$ (SR-AppR) $v\,e_{{\mathrm{2}}}\longrightarrow
v\,e^{\prime}_{{\mathrm{2}}}$ $e_{{\mathrm{1}}}\longrightarrow
e^{\prime}_{{\mathrm{1}}}$ (SR-ChoiceL) $(e_{{\mathrm{1}}}\parallel
e_{{\mathrm{2}}})\longrightarrow(e^{\prime}_{{\mathrm{1}}}\parallel
e_{{\mathrm{2}}})$ $e_{{\mathrm{2}}}\longrightarrow e^{\prime}_{{\mathrm{2}}}$
(SR-ChoiceR) $(e_{{\mathrm{1}}}\parallel
e_{{\mathrm{2}}})\longrightarrow(e_{{\mathrm{1}}}\parallel
e^{\prime}_{{\mathrm{2}}})$

Figure 3: Operational semantics of $\lambda^{\parallel}$

$\varnothing\,\mathrm{ok}$ (SW-Empty)

$\Gamma\,\mathrm{ok}$ $(x\notin\mathrm{dom}(\Gamma))$ (SW-Push)
$\Gamma,x\mathord{:}T\,\mathrm{ok}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\text{$\Gamma\,\mathrm{ok}$}\quad\quad\text{$(x\mathord{:}T\in\Gamma)$}\end{array}}{\begin{array}[]{@{}c@{}}\text{$\Gamma\vdash
x:T$}\end{array}}$ (ST-Var)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\text{$\Gamma\vdash
e_{{\mathrm{1}}}:T_{{\mathrm{1}}}\rightarrow
T_{{\mathrm{2}}}$}\quad\quad\text{$\Gamma\vdash
e_{{\mathrm{2}}}:T_{{\mathrm{1}}}$}\end{array}}{\begin{array}[]{@{}c@{}}\text{$\Gamma\vdash
e_{{\mathrm{1}}}\,e_{{\mathrm{2}}}:T_{{\mathrm{2}}}$}\end{array}}$ (ST-App)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\text{$\Gamma,x\mathord{:}T_{{\mathrm{1}}}\vdash
e:T_{{\mathrm{2}}}$}\end{array}}{\begin{array}[]{@{}c@{}}\text{$\Gamma\vdash\lambda
x.e:T_{{\mathrm{1}}}\rightarrow T_{{\mathrm{2}}}$}\end{array}}$ (ST-Abs)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\text{$\Gamma,f\mathord{:}T_{{\mathrm{1}}}\rightarrow
T_{{\mathrm{2}}}\vdash\lambda x.e:T_{{\mathrm{1}}}\rightarrow
T_{{\mathrm{2}}}$}\end{array}}{\begin{array}[]{@{}c@{}}\text{$\Gamma\vdash\mu
f.\lambda x.e:T_{{\mathrm{1}}}\rightarrow T_{{\mathrm{2}}}$}\end{array}}$ (ST-
Fix)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\text{$\Gamma\vdash
e_{{\mathrm{1}}}:T$}\quad\quad\text{$\Gamma\vdash
e_{{\mathrm{2}}}:T$}\end{array}}{\begin{array}[]{@{}c@{}}\text{$\Gamma\vdash(e_{{\mathrm{1}}}\parallel
e_{{\mathrm{2}}}):T$}\end{array}}$ (ST-Choice)

Figure 4: Typing rules for $\lambda^{\parallel}$

The syntax, semantics, and type system of $\lambda^{\parallel\omega}$ are
defined as Figure 2, Figure 3, and Figure 4, respectively. Those are standard
ones for a simply typed lambda calculus and with straightforward extensions
for a fix-point operator $\mu f.e$ and non-collapse choices
$(e_{{\mathrm{1}}}\parallel e_{{\mathrm{2}}})$. “Non-collapse” means that a
choice dose not really choose an alternative (like $(e_{{\mathrm{1}}}\parallel
e_{{\mathrm{2}}})\longrightarrow e_{{\mathrm{1}}}$) as coordinated choice does
not, but also it never coordinate alternatives.

###  3.2 Target Language: $\lambda^{\parallel\omega}$

$\Phi$ | $\Coloneq$ |  $\alpha$ $|$ $\epsilon$ $|$ $\mdwhtcircle$ $|$ $\mdblkcircle$ $|$ $\Phi_{{\mathrm{1}}}\Phi_{{\mathrm{2}}}$
---|---|---
$\varphi$ | $\Coloneq$ |  $\varnothing$ $|$ $\Phi$ $|$ $\varphi_{{\mathrm{1}}}\varphi_{{\mathrm{2}}}$ $|$ $\varphi_{{\mathrm{1}}}+\varphi_{{\mathrm{2}}}$ $|$ $\varphi^{\ast}$
$\tau$ | $\Coloneq$ |  $\mathrm{nat}$ $|$ $\tau_{{\mathrm{1}}}\overset{\varphi}{\rightarrow}\tau_{{\mathrm{2}}}$ $|$ $\forall\alpha.^{\varphi}\tau$
$M$ | $\Coloneq$ |  $x$ $|$ $M_{{\mathrm{1}}}\,M_{{\mathrm{2}}}$ $|$ $\lambda x.M$ $|$ $M\,\Phi$ $|$ $\Lambda\alpha.M$ $|$ $\mu f.M$ $|$ $(M_{{\mathrm{1}}}\parallel^{\Phi}M_{{\mathrm{2}}})$
$\Xi$ | $\Coloneq$ |  $\varnothing$ $|$ $\Xi,x\mathord{:}\tau$ $|$ $\Xi,\alpha$
$V$ | $\Coloneq$ |  $\lambda x.M$ $|$ $\Lambda\alpha.M$
Figure 5: Syntax of $\lambda^{\parallel\omega}$

$(\lambda x.M)\,V\mathrel{\overset{\Delta}{\longrightarrow}}M[x\coloneq V]$
(TR-Beta)

$(\Lambda\alpha.M)\,\Phi\mathrel{\overset{\Delta}{\longrightarrow}}M[\alpha\coloneq\Phi]$
(TR-Sigma)

$\mu f.\lambda x.M\mathrel{\overset{\Delta}{\longrightarrow}}(\lambda
x.M)[f\coloneq\mu f.\lambda x.M]$ (TR-Fix)

$(M_{{\mathrm{1}}}\parallel^{\Phi}M_{{\mathrm{2}}})\,M_{{\mathrm{3}}}\mathrel{\overset{\Delta}{\longrightarrow}}(M_{{\mathrm{1}}}\,M_{{\mathrm{3}}}\parallel^{\Phi}M_{{\mathrm{2}}}\,M_{{\mathrm{3}}})$
(TR-DistAppL)

$V\,(M_{{\mathrm{1}}}\parallel^{\Phi}M_{{\mathrm{2}}})\mathrel{\overset{\Delta}{\longrightarrow}}(V\,M_{{\mathrm{1}}}\parallel^{\Phi}V\,M_{{\mathrm{2}}})$
(TR-DistAppR)

$(M_{{\mathrm{1}}}\parallel^{\Phi_{{\mathrm{1}}}}M_{{\mathrm{2}}})\,\Phi_{{\mathrm{2}}}\mathrel{\overset{\Delta}{\longrightarrow}}(M_{{\mathrm{1}}}\,\Phi_{{\mathrm{2}}}\parallel^{\Phi_{{\mathrm{1}}}}M_{{\mathrm{2}}}\,\Phi_{{\mathrm{2}}})$
(TR-DistSApp)

$M_{{\mathrm{1}}}\mathrel{\overset{\Delta}{\longrightarrow}}M^{\prime}_{{\mathrm{1}}}$
(TR-AppL)
$M_{{\mathrm{1}}}\,M_{{\mathrm{2}}}\mathrel{\overset{\Delta}{\longrightarrow}}M^{\prime}_{{\mathrm{1}}}\,M_{{\mathrm{2}}}$
$M\mathrel{\overset{\Delta}{\longrightarrow}}M^{\prime}$ (TR-AppR)
$V\,M\mathrel{\overset{\Delta}{\longrightarrow}}V\,M^{\prime}$
$M\mathrel{\overset{\Delta}{\longrightarrow}}M^{\prime}$ (TR-SApp)
$M\,\Phi\mathrel{\overset{\Delta}{\longrightarrow}}M^{\prime}\,\Phi$
$M_{{\mathrm{1}}}\mathrel{\overset{\Delta\cup\\{\Phi_{+}\\}}{\longrightarrow}}M^{\prime}_{{\mathrm{1}}}$
(TR-ChoiceL)
$(M_{{\mathrm{1}}}\parallel^{\Phi}M_{{\mathrm{2}}})\mathrel{\overset{\Delta}{\longrightarrow}}(M^{\prime}_{{\mathrm{1}}}\parallel^{\Phi}M_{{\mathrm{2}}})$
$M_{{\mathrm{2}}}\mathrel{\overset{\Delta\cup\\{\Phi_{-}\\}}{\longrightarrow}}M^{\prime}_{{\mathrm{2}}}$
(TR-ChoiceR)
$(M_{{\mathrm{1}}}\parallel^{\Phi}M_{{\mathrm{2}}})\mathrel{\overset{\Delta}{\longrightarrow}}(M_{{\mathrm{1}}}\parallel^{\Phi}M^{\prime}_{{\mathrm{2}}})$
$(M_{{\mathrm{1}}}\parallel^{\Phi}M_{{\mathrm{2}}})\mathrel{\overset{\Delta\cup\\{\Phi_{+}\\}}{\longrightarrow}}M_{{\mathrm{1}}}$
(TR-WorldL)
$(M_{{\mathrm{1}}}\parallel^{\Phi}M_{{\mathrm{2}}})\mathrel{\overset{\Delta\cup\\{\Phi_{-}\\}}{\longrightarrow}}M_{{\mathrm{2}}}$
(TR-WorldR)

Figure 6: Operational semantics of $\lambda^{\parallel\omega}$

The syntax and semantics of $\lambda^{\parallel\omega}$ are shown in Figure 5
and Figure 6, respectively. As far as the semantics,
$\lambda^{\parallel\omega}$ is just a simply typed lambda calculus with
coordinated choice, c.f. $\lambda^{H\parallel^{\Phi}}$. An interesting part of
$\lambda^{\parallel\omega}$ is an _effect_ system [3], which is a kind of type
system. The effect system of $\lambda^{\parallel\omega}$ estimates names
happening during execution and rejects an expression that will cause
synchronization, and so this is the relation that we have mentioned at the
last of Section 2.

We range over effects with a meta-variable $\varphi$. Effects of
$\lambda^{\parallel\omega}$ are denoted by regular expressions: the empty set
$\varnothing$; literal strings $\Phi$ including the empty string $\epsilon$;
concatenations $\varphi_{{\mathrm{1}}}\varphi_{{\mathrm{2}}}$; alternations
$\varphi_{{\mathrm{1}}}+\varphi_{{\mathrm{2}}}$; and Kleene star
$\varphi^{\ast}$.

Function types and forall types are annotated by effects, which express the
effect happening when a function is used. Forall types
$\forall\alpha.^{\varphi}\tau$ bind $\alpha$ in $\varphi$ and $\tau$.

######  Definition .

A _closed_ term is one in which both free variables and free name variables
are empty. We denote closed terms with over-barred meta-variables, e.g.,
$\bar{\Phi},\bar{\varphi}$.

######  Definition .

We denote the language, a set of names, represented by an effect $\varphi$ as
$\mathbb{L}(\varphi)$.

###  3.3 Effect System

$\mathrm{nat}\mathrel{<\\!:}\mathrm{nat}$ (TS-Nat)

$\tau_{{\mathrm{21}}}\mathrel{<\\!:}\tau_{{\mathrm{11}}}$
$\tau_{{\mathrm{12}}}\mathrel{<\\!:}\tau_{{\mathrm{22}}}$
$(\mathbb{L}(\varphi_{{\mathrm{1}}})\subseteq\mathbb{L}(\varphi_{{\mathrm{2}}}))$
(TS-Arrow)
$\tau_{{\mathrm{11}}}\overset{\varphi_{{\mathrm{1}}}}{\rightarrow}\tau_{{\mathrm{12}}}\mathrel{<\\!:}\tau_{{\mathrm{21}}}\overset{\varphi_{{\mathrm{2}}}}{\rightarrow}\tau_{{\mathrm{22}}}$
$\tau_{{\mathrm{1}}}\mathrel{<\\!:}\tau_{{\mathrm{2}}}$
$(\mathbb{L}(\varphi_{{\mathrm{1}}})\subseteq\mathbb{L}(\varphi_{{\mathrm{2}}}))$
(TS-Forall)
$\forall\alpha.^{\varphi_{{\mathrm{1}}}}\tau_{{\mathrm{1}}}\mathrel{<\\!:}\forall\alpha.^{\varphi_{{\mathrm{2}}}}\tau_{{\mathrm{2}}}$

Figure 7: Effect system of $\lambda^{\parallel\omega}$ (1): subtyping rules

$\varnothing\,\mathrm{ok}$ (TW-Empty)

$\Xi\,\mathrm{ok}$ $\Xi\Vdash\tau$ $(x\notin\mathrm{dom}(\Xi))$ (TW-Push)
$\Xi,x\mathord{:}\tau\,\mathrm{ok}$ $\Xi\,\mathrm{ok}$
$(\alpha\notin\mathrm{ndom}(\Xi))$ (TW-PushS) $\Xi,\alpha\,\mathrm{ok}$

$\Xi\,\mathrm{ok}$ $(\alpha\in\Xi)$ (TW-NVar) $\Xi\Vdash\alpha$
$\Xi\,\mathrm{ok}$ (TW-Eps) $\Xi\Vdash\epsilon$ $\Xi\,\mathrm{ok}$ (TW-On)
$\Xi\Vdash\mdwhtcircle$ $\Xi\,\mathrm{ok}$ (TW-Off) $\Xi\Vdash\mdblkcircle$
$\Xi\Vdash\Phi_{{\mathrm{1}}}$ $\Xi\Vdash\Phi_{{\mathrm{2}}}$ (TW-Append)
$\Xi\Vdash\Phi_{{\mathrm{1}}}\Phi_{{\mathrm{2}}}$ $\Xi\,\mathrm{ok}$ (TW-
Empty) $\Xi\Vdash\mathsf{A}$ $\Xi\Vdash\varphi_{{\mathrm{1}}}$
$\Xi\Vdash\varphi_{{\mathrm{2}}}$ (TW-Dot)
$\Xi\Vdash\varphi_{{\mathrm{1}}}\varphi_{{\mathrm{2}}}$
$\Xi\Vdash\varphi_{{\mathrm{1}}}$ $\Xi\Vdash\varphi_{{\mathrm{2}}}$ (TW-Plus)
$\Xi\Vdash\varphi_{{\mathrm{1}}}+\varphi_{{\mathrm{2}}}$ $\Xi\Vdash\varphi$
(TW-Star) $\Xi\Vdash\varphi^{\ast}$ $\Xi\,\mathrm{ok}$ (TW-Nat)
$\Xi\Vdash\mathrm{nat}$ $\Xi\Vdash\tau_{{\mathrm{1}}}$
$\Xi\Vdash\tau_{{\mathrm{2}}}$ $\Xi\Vdash\varphi$ (TW-Arrow)
$\Xi\Vdash\tau_{{\mathrm{1}}}\overset{\varphi}{\rightarrow}\tau_{{\mathrm{2}}}$
$\Xi,\alpha\Vdash\tau$ $\Xi,\alpha\Vdash\varphi$ (TW-Forall)
$\Xi\Vdash\forall\alpha.^{\varphi}\tau$

Figure 8: Effect system of $\lambda^{\parallel\omega}$ (2): well-formedness
rules

$\Xi\,\mathrm{ok}$ $(x\mathord{:}\tau\in\Xi)$ (TT-Var) $\Xi\vdash
x:\tau\mathrel{\&}\mathsf{A}$ $\Xi\vdash
M_{{\mathrm{1}}}:\tau_{{\mathrm{1}}}\overset{\Phi\bar{\varphi}_{{\mathrm{1}}}}{\rightarrow}\tau_{{\mathrm{2}}}\mathrel{\&}\Phi\bar{\varphi}_{{\mathrm{2}}}$
$\Xi\vdash
M_{{\mathrm{2}}}:\tau_{{\mathrm{1}}}\mathrel{\&}\Phi\bar{\varphi}_{{\mathrm{3}}}$
$(\biguplus_{k\in\\{1,2,3\\}}\mathbb{L}(\bar{\varphi}_{k}))$ (TT-App)
$\Xi\vdash
M_{{\mathrm{1}}}\,M_{{\mathrm{2}}}:\tau\mathrel{\&}\Phi(\bar{\varphi}_{{\mathrm{1}}}+\bar{\varphi}_{{\mathrm{2}}}+\bar{\varphi}_{{\mathrm{3}}})$
$\Xi,x\mathord{:}\tau_{{\mathrm{1}}}\vdash
M:\tau_{{\mathrm{2}}}\mathrel{\&}\varphi$ (TT-Abs) $\Xi\vdash\lambda
x.M:\tau_{{\mathrm{1}}}\overset{\varphi}{\rightarrow}\tau_{{\mathrm{2}}}\mathrel{\&}\mathsf{A}$
$\Xi\vdash
M:\forall\alpha.^{\varphi_{{\mathrm{1}}}}\tau\mathrel{\&}\Phi^{\prime}\bar{\varphi}_{{\mathrm{2}}}$
$\Xi\Vdash\Phi$
$(\mathbb{L}(\varphi_{{\mathrm{1}}}[\alpha\coloneq\Phi])\subseteq\mathbb{L}(\Phi^{\prime}\bar{\varphi}_{{\mathrm{3}}}))$
$(\mathbb{L}(\bar{\varphi}_{{\mathrm{2}}})\uplus\mathbb{L}(\bar{\varphi}_{{\mathrm{3}}}))$
(TT-SApp) $\Xi\vdash
M\,\Phi:\tau[\alpha\coloneq\Phi]\mathrel{\&}\Phi^{\prime}(\bar{\varphi}_{{\mathrm{2}}}+\bar{\varphi}_{{\mathrm{3}}})$
$\Xi,\alpha\vdash M:\tau\mathrel{\&}\varphi$ (TT-SAbs)
$\Xi\vdash\Lambda\alpha.M:\forall\alpha.^{\varphi}\tau\mathrel{\&}\mathsf{A}$
$\Xi,f\mathord{:}\tau_{{\mathrm{1}}}\overset{\varphi}{\rightarrow}\tau_{{\mathrm{2}}}\vdash\lambda
x.M:\tau_{{\mathrm{1}}}\overset{\varphi}{\rightarrow}\tau_{{\mathrm{2}}}\mathrel{\&}\mathsf{A}$
(TT-Fix) $\Xi\vdash\mu f.\lambda
x.M:\tau_{{\mathrm{1}}}\overset{\varphi}{\rightarrow}\tau_{{\mathrm{2}}}\mathrel{\&}\mathsf{A}$
$\Xi\vdash
M_{{\mathrm{1}}}:\tau\mathrel{\&}\Phi^{\prime}\bar{\varphi}_{{\mathrm{1}}}$
$\Xi\vdash
M_{{\mathrm{2}}}:\tau\mathrel{\&}\Phi^{\prime}\bar{\varphi}_{{\mathrm{1}}}$
$\Xi\Vdash\Phi$
$(\mathbb{L}(\Phi)\subseteq\mathbb{L}(\Phi^{\prime}\bar{\varphi}_{{\mathrm{2}}}))$
$(\mathbb{L}(\bar{\varphi}_{{\mathrm{1}}})\uplus\mathbb{L}(\bar{\varphi}_{{\mathrm{2}}}))$
(TT-Choice)
$\Xi\vdash(M_{{\mathrm{1}}}\parallel^{\Phi}M_{{\mathrm{2}}}):\tau\mathrel{\&}\Phi^{\prime}(\bar{\varphi}_{{\mathrm{1}}}+\bar{\varphi}_{{\mathrm{2}}})$
$\Xi\vdash M:\tau_{{\mathrm{1}}}\mathrel{\&}\varphi_{{\mathrm{1}}}$
$\Xi\Vdash\tau_{{\mathrm{2}}}$ $\Xi\Vdash\varphi_{{\mathrm{2}}}$
$\tau_{{\mathrm{1}}}\mathrel{<\\!:}\tau_{{\mathrm{2}}}$
$(\mathbb{L}(\varphi_{{\mathrm{1}}})\subseteq\mathbb{L}(\varphi_{{\mathrm{2}}}))$
(TT-Sub) $\Xi\vdash M:\tau_{{\mathrm{2}}}\mathrel{\&}\varphi_{{\mathrm{2}}}$

Figure 9: Effect system of $\lambda^{\parallel\omega}$ (3): typing rules

The effect system for $\lambda^{\parallel\omega}$ consists of the subtyping
relation $\tau_{{\mathrm{1}}}\mathrel{<\\!:}\tau_{{\mathrm{2}}}$; the well-
formedness relations $\Xi\,\mathrm{ok}$, $\Xi\Vdash\Phi$, $\Xi\Vdash\varphi$,
and $\Xi\Vdash\tau$; and typing relation $\Xi\vdash
M:\tau\mathrel{\&}\varphi$.

Well-formedness rules just check a closedness of types by (TW-NVar) and (TW-
Forall).

Typing rules are the heart of the effect system. The judgment $\Xi\vdash
M:\tau\mathrel{\&}\varphi$ denotes a usual typing relation by the left side of
& and what names will occur during evaluation of $M$ by the right side of &.
So, ignoring the right side of &, rules are already familiar. For the effect
part, the rules become complicated because of showing meta-properties.

(TT-Var), (TT-Abs), (TT-SAbs), and (TT-Fix) are rather easy. Corresponding
expressions for those are never evaluated (fix-point operator is evaluated but
soon reaches a value); and therefore, those produce no names examined. This is
why the effect part of those rules becomes empty. Note that functions’ body is
evaluated when an argument is given; so the effect of the body is recorded on
types and added at an application point, c.f. (TT-Abs) and (TT-App).

(TT-App), (TT-SApp), and (TT-Choice) have complicated side-conditions. To
explain the rules, we will starts from the following rather ideal and simple
rule for coordinate choices.

$\Xi\vdash M_{{\mathrm{1}}}:\tau\mathrel{\&}\varphi_{{\mathrm{1}}}$ $\Xi\vdash
M_{{\mathrm{2}}}:\tau\mathrel{\&}\varphi_{{\mathrm{2}}}$ $\Xi\Vdash\Phi$
$\Xi\vdash(M_{{\mathrm{1}}}\parallel^{\Phi}M_{{\mathrm{2}}}):\tau\mathrel{\&}\varphi_{{\mathrm{1}}}+\varphi_{{\mathrm{2}}}+\Phi$

This rule just estimate the names which occur along an evaluation and impose
no restriction. $M_{{\mathrm{1}}}$ will cause names represented by the regular
expression $\varphi_{{\mathrm{1}}}$, $M_{{\mathrm{2}}}$ will cause names
represented by the regular expression $\varphi_{{\mathrm{2}}}$, and the choice
itself already causes the name $\Phi$. So the whole effect is the alternation
of those.

The next step is to introduce a restriction to the rule. The idea of
restriction is so simple—coordination never happens if names of sub-
expressions do not overlap. So the rule will become the following.

$\Xi\vdash M_{{\mathrm{1}}}:\tau\mathrel{\&}\varphi_{{\mathrm{1}}}$ $\Xi\vdash
M_{{\mathrm{2}}}:\tau\mathrel{\&}\varphi_{{\mathrm{2}}}$ $\Xi\Vdash\Phi$
$(\mathbb{L}(\varphi_{{\mathrm{1}}})\uplus\mathbb{L}(\varphi_{{\mathrm{2}}})\uplus\mathbb{L}(\Phi))$
$\Xi\vdash(M_{{\mathrm{1}}}\parallel^{\Phi}M_{{\mathrm{2}}}):\tau\mathrel{\&}\varphi_{{\mathrm{1}}}+\varphi_{{\mathrm{2}}}+\Phi$

The last step comes from a technical reason. The naive side-condition breaks
subject reduction lemma. We need the following property for the subject
reduction lemma.

######  Proposition .

If $\Xi,\alpha\vdash M:\tau\mathrel{\&}\varphi$ and
$\mathrm{fnv}(\Phi)\subseteq\mathrm{ndom}(\Xi)$, then $\Xi\vdash
M[\alpha\coloneq\Phi]:\tau[\alpha\coloneq\Phi]\mathrel{\&}\varphi[\alpha\coloneq\Phi]$.

However, the name substitution for the effect breaks the disjunctivity. (For
instance, $\mathbb{L}(\alpha)$ and $\mathbb{L}(\mdwhtcircle)$ are disjunctive,
but $\mathbb{L}(\alpha[\alpha\coloneq\mdwhtcircle])$ and
$\mathbb{L}(\mdwhtcircle[\alpha\coloneq\mdwhtcircle])$ are not.)

To amend the problem we adopt more specific side-condition as follows and make
the effect in the conclusion as
$\Phi^{\prime}(\bar{\varphi}_{{\mathrm{1}}}+\bar{\varphi}_{{\mathrm{2}}}+\bar{\varphi}_{{\mathrm{3}}})$.

$\displaystyle\mathbb{L}(\varphi_{{\mathrm{1}}})\subseteq\mathbb{L}(\Phi^{\prime}\bar{\varphi}_{{\mathrm{1}}})$
$\displaystyle\mathbb{L}(\varphi_{{\mathrm{2}}})\subseteq\mathbb{L}(\Phi^{\prime}\bar{\varphi}_{{\mathrm{2}}})$
$\displaystyle\mathbb{L}(\Phi)\subseteq\mathbb{L}(\Phi^{\prime}\bar{\varphi}_{{\mathrm{3}}})$
$\displaystyle\mathbb{L}(\bar{\varphi}_{{\mathrm{1}}})\uplus\mathbb{L}(\bar{\varphi}_{{\mathrm{2}}})\uplus\mathbb{L}(\bar{\varphi}_{{\mathrm{3}}})$

The point is that string variables are gathered into the prefix and name
disjunctivity is guaranteed by the closed effects, which are not altered by a
substitution. Indeed, this side-condition quite respects the compilation
rules, which create a fresh name by appending the constants
$\mdwhtcircle,\mdblkcircle$ to the tail of seed and a string variable is
pushed to the head of the seed.

The (TT-Choice) is almost obtained. We can drive away the first two subset
relation into (TT-Sub). Additionally, it can be seen that the effects from
left and right side of a choice, namely $\varphi_{{\mathrm{1}}}$ and
$\varphi_{{\mathrm{2}}}$, need not be distinct since both sides never
collaborate. So, we can take one large effect $\bar{\varphi}$ which subsume
$\varphi_{{\mathrm{1}}}$ and $\varphi_{{\mathrm{2}}}$ instead of
$\bar{\varphi}_{{\mathrm{1}}}$ and $\bar{\varphi}_{{\mathrm{2}}}$, i.e.,
$\mathbb{L}(\varphi_{{\mathrm{1}}})\subseteq\mathbb{L}(\Phi^{\prime}\bar{\varphi})$
and
$\mathbb{L}(\varphi_{{\mathrm{2}}})\subseteq\mathbb{L}(\Phi^{\prime}\bar{\varphi})$.

(TT-App) and (TT-SApp) are constructed in a similar manner.

##  4 Property

In the proof of this section, we implicitly use well-known properties about
regular expressions, e.g., $\mathbb{L}(\epsilon\varphi)=\mathbb{L}(\varphi)$,
$\mathbb{L}(\varphi_{{\mathrm{1}}}(\varphi_{{\mathrm{2}}}+\varphi_{{\mathrm{3}}}))=\mathbb{L}(\varphi_{{\mathrm{1}}}\varphi_{{\mathrm{2}}}+\varphi_{{\mathrm{1}}}\varphi_{{\mathrm{3}}})$,
etc. This is one reason we have not fully mechanized the proofs yet.

###  4.1 Type Soundness of $\lambda^{\parallel\omega}$

We start from investigation for the effect system: the effect system prevents
coordination by Section 4.1 and the property is preserved by the reduction by
Section 4.1.

######  Lemma  (Substitution).

If $\Xi,x\mathord{:}\tau^{\prime}\vdash M:\tau\mathrel{\&}\varphi$ and
$\Xi\vdash M^{\prime}:\tau^{\prime}\mathrel{\&}\mathsf{A}$, then $\Xi\vdash
M[x\coloneq M^{\prime}]:\tau\mathrel{\&}\varphi$.

######  Lemma  (Name substitution).

If $\Xi,\alpha\vdash M:\tau\mathrel{\&}\varphi$ and
$\mathrm{fnv}(\Phi)\subseteq\mathrm{ndom}(\Xi)$, then $\Xi\vdash
M[\alpha\coloneq\Phi]:\tau[\alpha\coloneq\Phi]\mathrel{\&}\varphi[\alpha\coloneq\Phi]$.

######  Lemma  (Subject reduction).

If $\varnothing\vdash M:\tau\mathrel{\&}\varphi$ and
$M\mathrel{\overset{\Delta}{\longrightarrow}}M^{\prime}$, then
$\varnothing\vdash M^{\prime}:\tau\mathrel{\&}\varphi$.

######  Definition .

Non-coordinated reduction relation, denoted as $M\Longrightarrow M^{\prime}$,
is derived from the rules in Figure 6 by replacing
$\overset{\Delta}{\longrightarrow}$ with $\Longrightarrow$ and removing (TR-
WorldL) and (TR-WorldR).

######  Lemma .

If $\varnothing\vdash M:\tau\mathrel{\&}\varphi$,
$M\mathrel{\overset{\Delta}{\longrightarrow}}M^{\prime}$, and
$\mathbb{L}(\varphi)\uplus\\{\omega\mid\omega_{+}\in\Delta\vee\omega_{-}\in\Delta\\}$;
then $M\Longrightarrow M^{\prime}$.

######  Corollary  (Non-coordination).

If $\varnothing\vdash M:\tau\mathrel{\&}\varphi$ and
$M\mathrel{\overset{\varnothing}{\longrightarrow}}M^{\prime}$, then
$M\Longrightarrow M^{\prime}$.

###  4.2 Soundness of Compilation

Towards the goal we show a well-typed expression in $\lambda^{\parallel}$ is
mapped into a well-typed expression in $\lambda^{\parallel\omega}$ by the
compilation.

######  Definition  (Compilation for types).

Compilation for types is given as follows.

$\displaystyle\lBrack\mathrm{nat}\rBrack$ $\displaystyle=\mathrm{nat}$
$\displaystyle\lBrack T_{{\mathrm{1}}}\rightarrow T_{{\mathrm{2}}}\rBrack$
$\displaystyle=\lBrack
T_{{\mathrm{1}}}\rBrack\overset{\mathsf{A}}{\rightarrow}\forall\alpha.^{\alpha(\mdwhtcircle\mdblkcircle)^{\ast}}\lBrack
T_{{\mathrm{2}}}\rBrack$

######  Definition  (Compilation for typing environment).

Compilation for typing environment is given by the following obvious way.

$\displaystyle\lBrack\varnothing\rBrack$ $\displaystyle=\varnothing$
$\displaystyle\lBrack\Gamma,x\mathord{:}T\rBrack$
$\displaystyle=\lBrack\Gamma\rBrack,x\mathord{:}\lBrack T\rBrack$

######  Lemma .

$\varnothing\Vdash\lBrack T\rBrack$.

######  Lemma .

$\lBrack\Gamma\rBrack\,\mathrm{ok}$.

######  Lemma .

If $\Gamma\vdash e:T$, then $\lBrack\Gamma\rBrack,\alpha\vdash\lBrack
e\rBrack^{\alpha}_{\bar{\Phi}}:\lBrack
T\rBrack\mathrel{\&}\alpha\bar{\Phi}(\mdwhtcircle\mdblkcircle)^{\ast}$.

###### Proof.

The proof is by induction on the given derivation. ∎

###  4.3 Bisimulation

Next we show a well-typed expression in $\lambda^{\parallel\omega}$ behaves as
same as the expression of $\lambda^{\parallel}$ which is obtained by erasing
the name related parts.

######  Definition  (strong bisimulation between $\lambda^{\parallel}$ and
$\lambda^{\parallel\omega}$).

A binary relation $R$ between $\lambda^{\parallel}$ and
$\lambda^{\parallel\omega}$ expressions is called _strong bisimulation_ iff
the following conditions hold.

  * •

If $e\mathrel{R}M$ and $e\longrightarrow e^{\prime}$, then
$M\mathrel{\overset{\varnothing}{\longrightarrow}}M^{\prime}$ and
$e^{\prime}\mathrel{R}M^{\prime}$.

  * •

If $e\mathrel{R}M$ and
$M\mathrel{\overset{\varnothing}{\longrightarrow}}M^{\prime}$, then
$e\longrightarrow e^{\prime}$ and $e^{\prime}\mathrel{R}M^{\prime}$.

######  Definition  (weak bisimulation between $\lambda^{\parallel}$ and
$\lambda^{\parallel\omega}$).

A binary relation $R$ between $\lambda^{\parallel}$ and
$\lambda^{\parallel\omega}$ expressions is called _weak bisimulation_ iff the
following conditions hold.

  * •

If $e\mathrel{R}M$ and $e\longrightarrow e^{\prime}$, then
$M\mathrel{\overset{\varnothing}{\longrightarrow}{}^{\ast}}M^{\prime}$ and
$e^{\prime}\mathrel{R}M^{\prime}$.

  * •

If $e\mathrel{R}M$ and
$M\mathrel{\overset{\varnothing}{\longrightarrow}}M^{\prime}$, then
$e\longrightarrow^{\ast}e^{\prime}$ and $e^{\prime}\mathrel{R}M^{\prime}$.

######  Definition  (weak bisimulation for $\lambda^{\parallel}$).

We also call a binary relation $R$ between $\lambda^{\parallel}$ expressions
weak bisimulation iff the following conditions hold.

  * •

If $e_{{\mathrm{1}}}\mathrel{R}e_{{\mathrm{2}}}$ and
$e_{{\mathrm{1}}}\longrightarrow e^{\prime}_{{\mathrm{1}}}$, then
$e_{{\mathrm{2}}}\longrightarrow^{\ast}e^{\prime}_{{\mathrm{2}}}$ and
$e^{\prime}_{{\mathrm{1}}}\mathrel{R}e^{\prime}_{{\mathrm{2}}}$.

  * •

If $e_{{\mathrm{1}}}\mathrel{R}e_{{\mathrm{2}}}$ and
$e_{{\mathrm{2}}}\longrightarrow e^{\prime}_{{\mathrm{2}}}$, then
$e_{{\mathrm{1}}}\longrightarrow^{\ast}e^{\prime}_{{\mathrm{1}}}$ and
$e^{\prime}_{{\mathrm{1}}}\mathrel{R}e^{\prime}_{{\mathrm{2}}}$.

$\displaystyle\lfloor x\rfloor$ $\displaystyle=x$ $\displaystyle\lfloor
M_{{\mathrm{1}}}\,M_{{\mathrm{2}}}\rfloor$ $\displaystyle=\lfloor
M_{{\mathrm{1}}}\rfloor\,\lfloor M_{{\mathrm{2}}}\rfloor$
$\displaystyle\lfloor\lambda x.M\rfloor$ $\displaystyle=\lambda x.\lfloor
M\rfloor$ $\displaystyle\lfloor M\,\Phi\rfloor$ $\displaystyle=\lfloor
M\rfloor\,\lambda x.x$ $\displaystyle\lfloor\Lambda\alpha.M\rfloor$
$\displaystyle=\lambda x.\lfloor M\rfloor$ where $x$ is fresh
$\displaystyle\lfloor\mu f.M\rfloor$ $\displaystyle=\mu f.\lfloor M\rfloor$
$\displaystyle\lfloor(M_{{\mathrm{1}}}\parallel^{\Phi}M_{{\mathrm{2}}})\rfloor$
$\displaystyle=(\lfloor M_{{\mathrm{1}}}\rfloor\parallel\lfloor
M_{{\mathrm{2}}}\rfloor)$ Figure 10: Name erasure function

######  Definition .

We define the _name erasure_ function $\lfloor\cdot\rfloor$ from
$\lambda^{\parallel\omega}$ expressions into $\lambda^{\parallel}$ expressions
as in Figure 10. The important point of the definition is that name
abstractions and applications are replaced by dummy lambda abstractions and
applications. If we do not do that, i.e., just erase the name abstractions and
applications, it will happens that a value of $\lambda^{\parallel\omega}$,
which cannot be evaluated, is evaluated in $\lambda^{\parallel}$ after
applying the name erasure function. (Consider $\Lambda\alpha.(\lambda
x.x)\,\lambda x.x$ and name erased expression $(\lambda x.x)\,\lambda x.x$.)

######  Lemma .

$\lfloor M[x\coloneq M^{\prime}]\rfloor=\lfloor M\rfloor[x\coloneq\lfloor
M^{\prime}\rfloor]$.

###### Proof.

The proof is routine by structural induction on $M$. ∎

######  Lemma .

$\lfloor M[\alpha\coloneq\Phi]\rfloor=\lfloor M\rfloor$.

###### Proof.

The proof is routine by structural induction on $M$. ∎

######  Lemma .

If $\varnothing\vdash M:\tau\mathrel{\&}\varphi$ and $\lfloor
M\rfloor\longrightarrow e^{\prime}$, then
$M\mathrel{\overset{\varnothing}{\longrightarrow}}M^{\prime}$ and $\lfloor
M^{\prime}\rfloor=e^{\prime}$.

###### Proof.

The proof is by induction on the given derivation of $\varnothing\vdash
M:\tau\mathrel{\&}\varphi$. Note that well-typedness of $M$ is necessary
because function applications and name applications are collapsed by name
erasing. ∎

######  Lemma .

If $M\Longrightarrow M^{\prime}$, then $\lfloor M\rfloor\longrightarrow\lfloor
M^{\prime}\rfloor$.

###### Proof.

The proof is by induction on the given derivation. ∎

######  Corollary .

If $\varnothing\vdash M:\tau\mathrel{\&}\varphi$ and
$M\mathrel{\overset{\varnothing}{\longrightarrow}}M^{\prime}$, then $\lfloor
M\rfloor\longrightarrow\lfloor M^{\prime}\rfloor$.

###### Proof.

This is a corollary of Section 4.1 and Section 4.3. ∎

######  Definition .

We give the binary relation between source expressions and target expressions,
written $e\sim M$ as follows.

$\displaystyle e\sim M\iff\varnothing\vdash
M:\tau\mathrel{\&}\varphi\wedge\lfloor M\rfloor=e$

######  Corollary .

$\sim$ is a strong bisimulation.

###### Proof.

This is a corollary of Section 4.1, Section 4.3, and Section 4.3. ∎

######  Corollary .

If $\varnothing\vdash e:T$, then $\lfloor\lBrack
e\rBrack^{\alpha}_{\bar{\Phi}}[\alpha\coloneq\epsilon]\rfloor\sim\lBrack
e\rBrack^{\alpha}_{\bar{\Phi}}[\alpha\coloneq\epsilon]$.

###### Proof.

This is a corollary of Section 4.1 and Section 4.2. ∎

$\displaystyle\lceil x\rceil$ $\displaystyle=x$ $\displaystyle\lceil
e_{{\mathrm{1}}}\,e_{{\mathrm{2}}}\rceil$ $\displaystyle=\lceil
e_{{\mathrm{1}}}\rceil\,\lceil e_{{\mathrm{2}}}\rceil\,\lambda x.x$
$\displaystyle\lceil\lambda x.e\rceil$ $\displaystyle=\lambda x.\lambda
y.\lceil e\rceil$ where $y$ is fresh $\displaystyle\lceil\mu f.e\rceil$
$\displaystyle=\mu f.\lceil e\rceil$
$\displaystyle\lceil(e_{{\mathrm{1}}}\parallel e_{{\mathrm{2}}})\rceil$
$\displaystyle=(\lceil e_{{\mathrm{1}}}\rceil\parallel\lceil
e_{{\mathrm{2}}}\rceil)$ Figure 11: Pseudo compilation

######  Definition .

We define the _pseudo compilation_ from/to $\lambda^{\parallel}$ expressions
as shown in Figure 11. This function is not essential for our discussion, but
we use the function for convenience writing in the following.

######  Lemma .

$\lfloor\lBrack e\rBrack^{\alpha}_{\bar{\Phi}}\rfloor=\lceil e\rceil$.

######  Lemma .

$\lceil e[x\coloneq e^{\prime}]\rceil=\lceil e\rceil[x\coloneq\lceil
e^{\prime}\rceil]$.

######  Lemma .

If $\lceil e\rceil\longrightarrow e^{\prime}$, then
$e\longrightarrow^{\ast}e^{\prime\prime}$ and $\lceil
e^{\prime\prime}\rceil=e^{\prime}$.

######  Lemma .

If $e\longrightarrow e^{\prime}$, then $\lceil
e\rceil\longrightarrow^{\ast}e^{\prime\prime}$ and $\lceil
e^{\prime}\rceil=e^{\prime\prime}$.

######  Definition .

We give the binary relation between $\lambda^{\parallel}$ expressions, denoted
by $\approx$, as $e\approx\lceil e\rceil$.

######  Corollary .

The binary relation $e\approx\lceil e\rceil$ is a weak bisimulation.

######  Theorem 4.1.

If $\varnothing\vdash e:T$, then $e\approx\vysmwhtcircle\sim\lBrack
e\rBrack^{\alpha}_{\epsilon}[\alpha\coloneq\epsilon]$.

The result is a bit blurred since expressions before and after compilation are
related by two relations. More directly, the correspondence can be shown as
follows.

$\displaystyle\begin{aligned} e&\longrightarrow^{\ast}e^{\prime}\\\ \lBrack
e\rBrack^{\alpha}_{\epsilon}[\alpha\coloneq\epsilon]&\mathrel{\overset{\varnothing}{\longrightarrow^{\ast}}}M^{\prime}\\\
\end{aligned}\quad\text{and}\quad\lceil e^{\prime}\rceil=\lfloor
M^{\prime}\rfloor$

##  5 Conclusion

We give a compilation algorithm from $\lambda^{\parallel}$, a simply typed
lambda calculus with nondeterministic choices, into
$\lambda^{\parallel\omega}$, a simply typed lambda calculus with coordinated
choices; and show the compilation is sound and correct.

## References

  * [1] Matthew Hennessy and Edward A. Ashcroft.  Parameter-passing mechanisms and nondeterminism.  In John E. Hopcroft, Emily P. Friedman, and Michael A. Harrison, editors, Proceedings of the 9th Annual ACM Symposium on Theory of Computing, May 4-6, 1977, Boulder, Colorado, USA, pages 306–311. ACM, 1977\.
  * [2] Robin Milner.  Communication and concurrency.  PHI Series in computer science. Prentice Hall, 1989.
  * [3] Flemming Nielson and Hanne Riis Nielson.  Type and effect systems.  In Ernst-Rüdiger Olderog and Bernhard Steffen, editors, Correct System Design, Recent Insight and Advances, (to Hans Langmaack on the occasion of his retirement from his professorship at the University of Kiel), volume 1710 of Lecture Notes in Computer Science, pages 114–136. Springer, 1999.
  * [4] Yuki Nishida and Atsushi Igarashi.  Nondeterministic manifest contracts.  In David Sabel and Peter Thiemann, editors, Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018, pages 16:1–16:13. ACM, 2018.