Session types are a type-based approach to the verification of message-passing programs.
They specify communication structures essential for program correctness; a session type says what and when should be exchanged through a channel.
Central to session-typed languages are sequencing constructs
in types and processes that explicitly specify the order of actions in a protocol.

In this paper we study session types without sequencing.
The resulting framework of minimal session types is arguably the simplest form of session types one could conceive.
In the context of a core process calculus with sessions and higher-order concurrency (abstraction-passing),
we establish two main technical results.
First, we prove that every process $P$ typable with standard session types can be compiled down into a process $\D{P}$ typable with minimal session types.
Second, we prove that $P$ and $\D{P}$ are behaviorally equivalent.
These results indicate that having sequencing constructs in processes and session types is convenient but redundant: only sequentiality in processes is truly indispensable, as it can correctly codify sequentiality in types.

Our developments draw inspiration from work by Parrow on behavior-preserving decompositions of untyped processes.
By casting Parrow's results in the realm of typed processes, our developments reveal a conceptually simple formulation of session types and a
principled avenue to the integration of session types into programming languages without sequencing in types.

§ INTRODUCTION

Session types are a type-based approach to the verification of message-passing programs.
A session type specifies what and when should be exchanged through a channel.
This makes session types a useful tool to enforce safety and liveness properties related to communication correctness.
Originated in the realm of concurrency theory, session types have had a significant impact on the foundations of programming languages [14], but also on their practice [1].
Our goal in this work is to understand to what extent session types can admit simpler, more fundamental formulations.
This foundational question has concrete practical ramifications, as we discuss next.

In session-typed languages, sequencing constructs in types and processes specify the intended structure of message-passing protocols.
For example, in the session type $S = \btinp{\mathsf{int}} \btinp{\mathsf{int}} \btout{\mathsf{bool}} \tinact$, sequencing (denoted `$;$') allows us to specify a protocol for a channel that first receives (?)
two integers, then sends (!)
a boolean, and finally ends.
As such, $S$ could type a service that checks for integer equality.
Sequencing in types goes hand-in-hand with sequencing in processes, which is specified using prefix constructs (denoted `$.$').
The $\pi$-calculus process $P = \binp{s}{x_1} \binp{s}{x_2} \bout{s}{x_1=x_2} \inact$ is an implementation of the equality service: it first expects two values on name $s$, then outputs a boolean on $s$, and finally stops.
Thus, name $s$ in $P$ conforms to the session type $S$.
Session types can also specify sequencing within labeled choices and recursion; these typed constructs are also in close match with their respective process expressions.

Session types have been originally developed as a typing discipline for $\pi$-calculus for the analysis of message-passing protocols between exactly two parties [12].
Since then session types have been extended in many directions.
We find, for instance, multiparty session types [13], and extensions with dependent types, assertions, exceptions, and time (cf. [8, 14] for surveys).
All these extensions seek to address natural research questions on the expressivity and applicability of session types theories.

Here we address a different, if opposite, question: is there a minimal formulation of session types?
This is an appealing question from a theoretical perspective, but seems particularly relevant to the practice of session types: identifying the “core” of session types could enable their integration in languages whose type systems do not have certain advanced constructs present in session types, such as sequencing.
For instance, the Go programming language offers primitive support for message-passing concurrency; it comes with a static verification mechanism which can only enforce that messages exchanged along channels correspond with their declared payload types—it cannot ensure essential correctness properties associated with the ordering of messages and the structure of the protocols.
This observation has motivated the development of advanced static verification tools based on session types for Go programs; see, e.g., [20, 19].

This paper identifies and studies the properties of an elementary formulation of session types, which we call minimal session types.
Minimal session types are session types without sequencing.
That is, in
session types such as `$\btout{U} S$' and `$\btinp{U} S$', we stipulate that $S$ can only correspond to $\tinact$, the type of the terminated protocol.

Adopting minimal session types entails dispensing with sequencing, which is arguably the most distinctive feature of session types.
While this may appear as a far too drastic restriction, it turns out that it is not:
we show that for every process $P$ typable under standard (non minimal) session types, there is a  decomposition of $P$, denoted $\D{P}$, a process that
codifies the sequencing information given by the session types (protocols) of $P$ using additional synchronizations, extracted from its protocols.
<Ref> illustrates the key idea of the decomposition using the process $P$ and session type $S$ motivated above.
Because $P$ contains three actions in sequence (as stipulated by $S$), its decomposition  $\D{P}$ consists of three processes in parallel—each of them implementing one action of $P$—as well as of mechanisms for orchestrating these parallel processes: the synchronizations on names $c_2, \ldots, c_5$ ensure that the sequencing in $P$ is preserved and that received names are properly propagated. These three parallel processes are typable with minimal session types (in the figure, they are given below each process), which are obtained by suitably “slicing” $S$.

Our main finding is that $\D{P}$ satisfies two important properties: first, it is well-typed using minimal session types (static correctness); second, it is behaviorally equivalent to $P$ (dynamic correctness).
These properties ensure that having sequencing in both types and processes is convenient but redundant: only sequencing at the level of processes is truly indispensable.

ann = [draw=none,fill=none,right]

[draw,dotted](A) at (, 0) $P = \binp{s}{x_1}\binp{s}{x_2}\bout{s}{x_1 = x_2} \inact$;
[draw=none] at (,-0.45) $s : {?({\mathsf{int}})}; {?({\mathsf{int}})};
{!\langle {\mathsf{bool}}\rangle};\tinact$;
[draw,dotted] (B) at (, )̣ $\D{P}$;
[->, thick] (,-0.575 - 0.2) – (,+̣0.3);
[draw,dotted] (T1) at (-3.0,) $\cbpropinp{2}{}\binp{s_1}{x_1}\cbapropout{3}{x_1}$;
at (-1.5,) $\parallel$;
[draw,dotted] (T2) at (,) $\cbpropinp{3}{y_1}\binp{s_2}{x_2}\cbapropout{4}{y_1, x_2}$;
at (+1.45, ) $\parallel$;
[draw,dotted] (T3) at (+3.0,) $\cbpropinp{4}{x_1, x_2}\bout{s_3}{x_1 = x_2}\cbapropout{5}{}$;
at (-3.0,-0.45) $s_1:{?({\mathsf{int}})};\tinact$;
at (-3.0,-0.75) $\prop_2:{?()};\tinact$;
at (,-0.45) $s_2:{?({\mathsf{int}})};\tinact$;
at (,-0.75) $\prop_3:{?({\mathsf{int}})};\tinact$;
at (+3.0,-0.45) $s_3:{!\langle{\mathsf{bool}}\rangle};\tinact$;
at (+3.0,-0.75) $\prop_4:{?({\mathsf{int}, \mathsf{int}})};\tinact$;
[->, color=magenta, thick](-2.5,+0.25) edge[bend left] node [left]  (-1,+0.25);
[->, color=magenta, thick](+0.5,+0.25) edge[bend left] node [left]  (+2,+0.25);
[draw=none] ;
[->, color=magenta, thick] (B) edge[bend right=22] node [left]  (T1);
[<-, color=magenta, thick] (B) edge[bend left=22] node [left]  (T3);

The process decomposition, illustrated. Arrows in magenta indicate synchronizations orchestrated by the decomposition $\D{P}$.

The definition of $\D{P}$ is interesting on its own, as it draws inspiration from a known result by Parrow [21], who showed that any untyped $\pi$-calculus process can be decomposed as a collection of trio processes, i.e., processes with at most three nested prefixes [21].

The question of how to relate session types with other type systems has attracted interest in the past.
Session types have been encoded into, for instance, generic types [9] and linear types [7, 5, 6].
As such, these prior studies concern the relative expressiveness of session types, where the expressivity of session types stands with respect to that of some other type system.
In sharp contrast, we study the absolute expressiveness of session types: how session types can be explained in terms of themselves.
To our knowledge, this is the first study of its kind.

Session types have been developed on top of different process languages (mainly, dialects of the $\pi$-calculus), and so choosing the target language for minimal session types is an important decision in our developments.
In this paper, our target language is , the core process calculus for session-based concurrency studied by Kouzapas et al. [17, 18].
is a very small language, which only supports passing of abstractions (i.e., functions from names to processes) and lacks name-passing and recursion.
Nonetheless, is very expressive, because both features can be encoded in in a fully abstract way.
Moreover, has a well-developed theory of behavioral equivalences [18].
The combination of minimal number of features and expressivity makes an excellent candidate for studying a minimal formulation of session types.
Indeed, as we will see, several aspects of our decomposition take advantage of the higher-order nature of  .
Being a higher-order language, is very different from the (untyped, first-order) $\pi$-calculus considered by Parrow [21].
Therefore, our technical results arise in a context very different from Parrow's.

Contributions & Outline.
In summary, in this paper we present the following contributions:

* We identify the class of minimal session types (MST) as a simple fragment of standard session types for without sequencing that retains its absolute expressiveness (<Ref>).

* We show how to decompose standard session types into minimal session types, and how to decompose processes typable with standard session types into processes typable with minimal session types. This is a result of static correctness (<Ref>).

* We show that the decomposition of a process is behaviorally equivalent to the original process. This is a result of dynamic correctness, formalized in terms of MST bisimulations, a typed behavioral equivalence that we introduce here (<Ref>).

* We develop optimizations and extensions of our decomposition that bear witness to its robustness.

The rest of the paper is organized as follows.
In s:lang we recall the preliminaries on the session type system for , which is the core process calculus for session-based concurrency on which we base our developments.
In s:decomp we present minimal session types, and the decomposition of well-typed processes into minimal session types processes, accompanied by explanations and examples.
In ss:dynamic we show the correctness of the decomposition, by establishing an MST bisimulation between an process and its decomposition.
In s:opt we examine two optimizations of the decomposition that are enabled by the higher-order nature of our setting.
In ss:exti we discuss extensions of our approach to consider constructs for branching and selection.
Finally, in s:rw we elaborate further on related work and in s:concl we present some closing remarks.
The appendix contains omitted definitions and proofs.

Differences with the conference version.
An earlier version of this paper was presented at ECOOP 2019 [3].
The current paper revises the conference version, includes further examples, and incorporates a major addition: ss:dynamic on dynamic correctness, including the notion of an MST bisimulation and the constructed bisimulation relation,  is completely new to this presentation.

Throughout the paper we use different colors (such as pink  and green) to improve readability.
However, the usage of colors is not indispensable, and the paper can be followed in black-and-white.

§ THE SOURCE LANGUAGE

We start by recalling the syntax, semantics, and type system for , the higher-order process calculus for session-based concurrency studied by Kouzapas et al. [17, 18]. Our presentation of follows the aforementioned papers, which concern definitions and results for , the super-calculus of with name-passing, abstraction-passing, and recursion.

is arguably the simplest language for session types: it supports
passing of abstractions (functions from names to processes)
but does not support name-passing nor process recursion.
Still, is very expressive:  it can encode name-passing, recursion, and polyadic communication via type-preserving encodings that are fully-abstract with respect to  contextual equivalence [17].

§.§ Syntax and Semantics

The syntax of names, variables, values, and processes  is defined as follows:

\begin{align*}
n, m  & \bnfis a,b \bnfbar s, \dual{s}
\qquad \quad
u,w   \bnfis n \bnfbar x,y,z
\qquad \quad
V,W   \bnfis {x,y,z} \bnfbar {\abs{x}{P}}
\\[1mm]
& \bnfis
\bout{u}{V}{P}  \sbnfbar  \binp{u}{x}{P} \sbnfbar
\sbnfbar P\Par Q \sbnfbar \news{n} P
\sbnfbar \inact
\end{align*}

We use $a,b,c, \dots$ to range over shared names, and $s, \dual{s}, \dots$ to range over session names. Shared names are used for unrestricted, non-deterministic interactions; session names are used for linear, deterministic interactions. We write $n, m$ to denote session or shared names, and assume that the sets of session and shared names are disjoint. The dual of a name $n$ is denoted $\dual{n}$; we define $\dual{\dual{s}} = s$ and $\dual{a} = a$, i.e., duality is only relevant for session names. Variables are denoted with $x, y, z, \dots$. An abstraction $\abs{x}{P}$ is a process $P$ with parameter $x$.
Values $V,W, \ldots$ include variables and abstractions, but not names.

is the application
which substitutes name $u$ on abstraction $V$. Constructs for
inaction $\inact$,  parallel composition $P_1 \Par P_2$, and
name restriction $\news{n} P$ are standard.
lacks name-passing and recursion, but they are expressible in the language (see ex:np below).

To enhance readability, we often omit trailing $\inact$'s, so we write, e.g.,
$\about{u}{V}{}$ instead of  $\bout{u}{V}{\inact}$.
Also, we write
$\bout{u}{}{P}$ and $\binp{u}{}{P}$ whenever the exchanged value is not relevant (cf. r:prefix).

Restriction for shared names $\news{a} P$ is as usual; session name restriction $\news{s} P$ simultaneously binds session names $s$ and $\dual{s}$ in $P$.
Functions $\fv{P}$, $\fn{P}$, and $\fs{P}$ denote, respectively, the sets of free
variables, names, and session names in $P$, and are defined as expected.
If $\fv{P} = \emptyset$, we call $P$ closed.
We write $P\subst{u}{y}$ (resp., $P\subst{V}{y}$) for the capture-avoiding substitution of name $u$ (resp.,  value $V$) for $y$ in process $P$.
We identify processes up to consistent renaming of bound names, writing $\scong_\alpha$ for this congruence.
We shall rely on Barendregt's variable convention, under which free and bound names are different in every mathematical context.

The  operational semantics of is defined in terms of a reduction relation,
denoted $\red$.
Reduction is closed under structural congruence,
denoted $\scong$, which is defined as the smallest congruence on processes such that:

\begin{align*}
P \Par \inact \scong P
\quad
P_1 \Par P_2 \scong P_2 \Par P_1
\quad
P_1 \Par (P_2 \Par P_3) \scong (P_1 \Par P_2) \Par P_3
\quad
\news{n} \inact \scong \inact
\\[1mm]
P \Par \news{n} Q \scong \news{n}(P \Par Q)
\ (n \notin \fn{P})
\quad
P \scong Q \textrm{ if } P \scong_\alpha Q
\end{align*}

We assume the expected extension of $\scong$ to values $V$.
The reduction relation expresses the behavior of processes; it is defined as follows:

\begin{align*}
\appl{(\abs{x}{P})}{u}   & \red  P \subst{u}{x}
& \orule{App} &
\\\bout{n}{V} P \Par \binp{\dual{n}}{x} Q & \red  P \Par Q \subst{V}{x}
& \orule{Pass} &
\\P \red P'\Rightarrow  \news{n} P   & \red    \news{n} P'
& \orule{Res} &
\\P \red P'  \Rightarrow    P \Par Q  & \red   P' \Par Q
& \orule{Par} &
\\P \scong Q \red Q' \scong P'  \Rightarrow  P  & \red  P'
& \orule{Cong} &
\end{align*}

Rule $\orule{App}$ defines  name application ($\beta$-reduction). Rule $\orule{Pass}$ defines a
shared or session interaction, depending on the nature of $n$.
Other rules are standard $\pi$-calculus rules.
We write
$\red^k$ for a $k$-step reduction, and
$\red^\ast$ for the reflexive, transitive closure of $\red$.

We illustrate processes and their semantics by means of an example.

[Encoding Name-Passing]

The calculus lacks the name-passing primitives of .
Hence, it cannot express reductions of the form

\begin{align}
\bout{n}{m} P \Par \binp{\dual{n}}{x} Q  \red  P \Par Q \subst{m}{x}
\label{red:ex}
\end{align}

Fortunately,  name-passing can be
encoded in in a fully-abstract way: as shown in [17], one can use abstraction passing to “pack” a name.
To this end, f:np defines the required syntactic sugar, at the level of processes and types.
Then, the reduction (<ref>) can be mimicked as

\begin{align*}
{\bout{n}{\namepass{m}} P \Par \binp{\dual{n}}{\namepass{x}} Q} =~~ & \bbout{n}{ \abs{z}{\,\binp{z}{x} (\appl{x}{m})} } {P}  \Par \binp{\dual n}{y} \newsp{s}{\appl{y}{s} \Par \about{\dual{s}}{\abs{x}{{Q}}}}
\\
\red~~ &  {P}  \Par \newsp{s}{\appl{\abs{z}{\,\binp{z}{x} (\appl{x}{m})}}{s} \Par \about{\dual{s}}{\abs{x}{{Q}}}}
\\
\red~~ &  {P}  \Par \newsp{s}{\binp{s}{x} (\appl{x}{m}) \Par \about{\dual{s}}{\abs{x}{{Q}}}}
\\
\red~~ &  {P}  \Par \appl{(\abs{x}{{Q}})}{m}
\\
\red~~ &  {P}  \Par {Q}\subst{m}{x}
\end{align*}

\begin{align*}
\bout{t}{\namepass{\tilde u}}P & \triangleq \about{t}{\lambda z. \abinp{z}{x}.(x\ {\tilde u})}.P\\
\binp{t}{\namepass{\tilde x}}Q & \triangleq \abinp{t}{y}.\big(\news {z}(y\ z \Par \about{z}{\lambda {\tilde x}. Q})\big)
\\ \vspace{2mm}
{\namepass{\wtd S}} &\defas \lhot{(\btinp{\lhot{\namepasstyp{\wtd S}}}\tinact)} \\
{\namepass{\chtype{\wtd S}}} &\defas
\lhot{(\btinp{\lhot{\chtype{\namepasstyp{\wtd S}}}}\tinact)}
\\
\namepass{\lhot{\wtd C}} &\defas  \lhot{\namepasstyp{\wtd C}}
\\
\namepass{\shot{\wtd C}} &\defas  \shot{\namepasstyp{\wtd C}}
\\
\namepasstyp{\btout{{U}}S} &\defas
\\
\namepasstyp{\btinp{{U}}S} &\defas
\\
\namepasstyp{C_1,\ldots,C_n} &\defas
\namepasstyp{C_1}, \ldots, \namepasstyp{C_n}
\end{align*}

Encoding name passing in

as presented above allows only for monadic communication, i.e., the exchange of tuples of values with length 1.
We will find it convenient to use with polyadic communication, i.e., the exchange of tuples of values $\widetilde{V} = (V_1,\ldots,V_k)$, with length $\len{\widetilde{V}} = k$.
We will use similar notation for tuples of names and variables, and we will use $\epsilon$ to denote the empty tuple.

In , polyadicity appears in session synchronizations and applications, but not in synchronizations on shared names. This entails having the following reduction rules:

\begin{align*}
\appl{(\abs{\widetilde{x}}{P})}{\widetilde{u}}   & \red  P \subst{\widetilde{u}}{\widetilde{x}}
\\
\bout{s}{\widetilde{V}} P \Par \binp{\dual{s}}{\widetilde{x}} Q & \red  P \Par Q \subst{\widetilde{V}}{\widetilde{x}}
\end{align*}

where the simultaneous substitutions
and $P\subst{\widetilde{V}}{\widetilde{x}}$
are as expected.
This polyadic can be readily encoded into (monadic)  [18]; for this reason, by a slight
abuse of notation we will often write when we actually mean “polyadic ”.

We discuss two simple examples that illustrate   how can implement mechanisms resembling servers and forms of partial instantiation; these mechanisms shall come in handy later, when defining the process decomposition in <Ref>.

[A Server of a Kind]

Let $S_a$ denote the process $\binp{a}{x} (\appl{x}{r})$, which receives an abstraction on the shared name $a$ and then applies it to $r$. Consider the following process composition:

\begin{align*}
P &= 	\news{r}\news{a}\big(\bout{a}{V} \inact  \Par \bout{a}{W} \inact  \Par S_a
\Par \binp{\dual r}{x_1}\binp{\dual r}{x_2}Q \big)
\\
V& = \abs{y}{(\bout{y}{V'}S_a\subst{y}{r})}
\\
W& = \abs{z}{(\bout{z}{W'}S_a\subst{z}{r})}
\end{align*}

where $V'$ and $W'$ are some unspecified shared values.
In $P$, process $S_a$ operates as a server that provides $r$ upon an invocation on  $a$.
Dually, the outputs on $a$ are requests to this server.
One possible reduction sequence for $P$ is the following:

\begin{align*}
& \red
\news{r} \news{a}\big(\bout{a}{W} \inact  \Par \appl{V}{r} \Par
\binp{\dual r}{x_1}\binp{\dual r}{x_2}Q  \big)
\\
& \red
\news{r} \news{a}\big(\bout{a}{W} \inact  \Par \bout{r}{V'}S_a \Par
\binp{\dual r}{x_1}\binp{\dual r}{x_2}Q \big)
\\
& 		\red
\news{r} \news{a}\big(\bout{a}{W} \inact  \Par S_a \Par
\binp{\dual r}{x_2}Q\subst{V'}{x_1}  \big) = P'
\end{align*}

In this reduction sequence, the value $V$ in the first request is instantiated with the name $r$ by consuming a copy of $S_a$ available in $P$.
However, a copy of the server $S_a$ is restored through the value $V$, after an communication on $r$.
This way, in $P'$ the exchange of $W'$ on $r$ can take place:

P' \red^\ast
\news{r}\news{a}\big(S_a \Par Q\subst{V'}{x_1}\subst{W'}{x_2}\big)

[Partial Instantiation]

Let $S_a$ and $S_b$ be servers as defined in the previous 	example:

\begin{align*}
S_a = \binp{a}{x} (\appl{x}{r}) \qquad \qquad
S_b = \binp{b}{x} (\appl{x}{v})
\end{align*}

Further, let $R$ be a process in which requests to $S_a$ and $S_b$ are nested within abstractions:

\begin{align*}
R & = \abbout{a}{\abs{y}\about{b}{\abs{z}\appl{V}{(y,z)}}}
\end{align*}

Notice how the polyadic application `$\appl{V}{(y,z)}$' is enclosed in the innermost abstraction.
Now consider the following composition:

\begin{align*}
P = \news{a,b}  R \Par S_a \Par S_b
\end{align*}

The structure of $R$ induces a form of partial instantiation for $y, z$, implemented by combining synchronizations and $\beta$-reductions. To see this, let us inspect one possible reduction chain for $P$:

\begin{align*}
P &\red \news{b} \left(\appl{\abs{y}\about{b}{\abs{z}\appl{V}{(y,z)}}}{r}\right) \Par  S_b
\\
&\red \news{b}{\about{b}{\abs{z}\appl{V}{(r,z)}}} \Par  S_b = P'
\end{align*}

The first request of $R$, aimed to obtain name $r$,  is
realized by the first reduction, i.e., the communication with $S_a$ on name $a$:
the result is the application of the top-level abstraction to $r$.
Subsequently, the application step  substitutes
$y$ with $r$.
Hence, in $P'$,
names in the nested application  are only partially instantiated: at this point, we have `$\appl{V}{(r,z)}$'.

Process  $P'$ can then execute the same steps to instantiate  $z$ with name $v$
by interacting with $S_b$.
After two reductions, we obtain the fully instantiated application  $\appl{V}{(r,v)}$:

\begin{align*}
P' & \red \appl{{\abs{z}\appl{V}{(r,z)}}}{v}
\red \appl{V}{(r,v)}
\end{align*}

§.§ Session Types for

We give essential definitions and properties for the session type system for , following [18].

Let us write $\Proc$ to denote the process type.
The syntax of value types $U$, channel types $C$, and session types $S$ for is defined as follows:
\begin{align*}
U & \bnfis		\shot{C} \bnfbar \lhot{C}
\qquad \qquad
C  \bnfis		S \bnfbar  {\chtype{U}}
\\
S & \bnfis  \btout{U} S \bnfbar \btinp{U} S \bnfbar  \trec{t}{S} \bnfbar \vart{t}   \bnfbar 	\tinact
\end{align*}

As we have seen, only admits the exchange of abstractions; accordingly,
value types include $\shot{C}$ and $\lhot{C}$, which denote shared and
linear higher-order types, respectively. Channel types include session
types and the shared types $\chtype{U}$.

Session types follow the standard binary session type syntax [12], in which sequencing specifies communication structures.
This way, the output type $\btout{U} S$ describes a session in which first a value of type $U$ is sent, and then the session proceeds as $S$.
Dually, the input type $\btinp{U} S$ describes a session in which first a value of type $U$ is received, and then the session proceeds as $S$.
In examples, we often assume basic types (such as $\mathsf{int}$, $\mathsf{bool}$, $\mathsf{str}$) are exchanged in communications.
Session types also include recursive types $\trec{t}{S}$, in which the variable $\vart{t}$ is assumed to occur guarded in $S$, i.e., types such as $\trec{t}{\vart{t}}$ are not allowed.
In most cases, recursive types will be tail-recursive, although instances of non-tail-recursive session types will also be relevant (cf.
Finally, type $\tinact$ is the type of the terminated protocol.

As mentioned in the introduction, we shall study session types in which the continuation $S$ in $\btout{U} S$  and $\btinp{U} S$ is always $\tinact$.
Given this, we may sometimes omit trailing $\tinact$'s and write
$\btoutt{U}$  and $\btinpt{U}$
rather than
$\btout{U} \tinact$  and $\btinp{U} \tinact$, respectively.

In theories of session types  duality is a key notion:
implementations derived from dual session types will respect their protocols at run-time, avoiding communication errors.
Intuitively, duality is  obtained by
exchanging $!$ by $?$ (and vice versa), including the fixed point construction.
We write $S \dualof T$ if session types $S$ and $T$ are dual according to this intuition;
the formal definition is coinductive, and given in [18] (see also [10]).

We consider shared, linear, and session
environments, denoted $\Gamma$, $\Lambda$, and $\Delta$, resp.:

\begin{align*}
\Gamma  & \bnfis  \emptyset \bnfbar \Gamma \cat \varp{x}: \shot{C}
\bnfbar \Gamma \cat u: \chtype{U}
\\
\Lambda  & \bnfis  \emptyset \bnfbar \Lambda \cat \AT{x}{\lhot{C}}
\\
\Delta    & \bnfis   \emptyset \bnfbar \Delta \cat \AT{u}{S}
\end{align*}

$\Gamma$ maps variables and shared names to value types; $\Lambda$ maps variables to
$\Delta$  maps
session names to session types.
While $\Gamma$ admits weakening, contraction, and exchange principles,
both $\Lambda$ and $\Delta$
only subject to exchange.
The domains of $\Gamma,
\Lambda$, and $\Delta$ are assumed pairwise distinct.
We write $\Delta_1\cdot \Delta_2$ to denote the disjoint union of $\Delta_1$ and $\Delta_2$.

We write $\Gamma\backslash x$ to denote the environment obtained from $\Gamma$ by removing the assignment $x : \shot{C}$, for some $C$.
Notations $\Delta\backslash u$ and $\Gamma\backslash \widetilde{x}$ are defined similarly and have the expected readings.
With a slight abuse of notation, given a tuple of variables $\widetilde x$, we sometimes write $(\Gamma, \Delta)(\widetilde x)$ to denote the tuple of types assigned to the variables in $\widetilde x$ by the environments $\Gamma$ and $\Delta$.

The typing judgements for values $V$ and processes $P$ are denoted

\[
\Gamma; \Lambda; \Delta \proves V \hastype U \qquad \text{and} \qquad\Gamma; \Lambda; \Delta \proves P \hastype \Proc
\]

\[
\begin{array}{c}
\inferrule[(Sess)]{}{\Gamma; \emptyset; \set{u:S} \proves u \hastype S}
\qquad
\inferrule[(Sh)]{}{\Gamma \cat u : U; \emptyset; \emptyset \proves u \hastype U}
\\ \\
\inferrule[(LVar)]{}{\Gamma; \set{x: \lhot{C}}; \emptyset \proves x \hastype \lhot{C}}
\qquad
\inferrule[(RVar)]{}{\Gamma \cat \rvar{X}: \Delta; \emptyset; \Delta  \proves \rvar{X} \hastype \Proc}
\\  \\
\inferrule[(Abs)]{
\Gamma; \Lambda; \Delta_1 \proves P \hastype \Proc
\quad
\Gamma; \es; \Delta_2 \proves x \hastype C
\Gamma\backslash x; \Lambda; \Delta_1 \backslash \Delta_2 \proves \abs{{x}}{P} \hastype \lhot{{C}}
\quad
\inferrule[(App)]{
{\Gamma; \Lambda; \Delta_1 \proves V \hastype \ghot{C} ~~
\leadsto\, \in \{\lollipop, \sharedop\} \quad
\Gamma; \es; \Delta_2 \proves u \hastype C
\Gamma; \Lambda; \Delta_1 \cat \Delta_2 \proves \appl{V}{u} \hastype \Proc

\\  \\
\inferrule[(Prom)]{
\Gamma; \emptyset; \emptyset \proves V \hastype
\lhot{C}
\Gamma; \emptyset; \emptyset \proves V \hastype
\shot{C}
\quad
\inferrule[(EProm)]{
\Gamma; \Lambda \cat x : \lhot{C}; \Delta \proves P \hastype \Proc
\Gamma \cat x:\shot{C}; \Lambda; \Delta \proves P \hastype \Proc
\quad
\inferrule[(End)]{
\Gamma; \Lambda; \Delta  \proves P \hastype T \quad u \not\in \dom{\Gamma, \Lambda,\Delta}
\Gamma; \Lambda; \Delta \cat u: \tinact  \proves P \hastype \Proc
\\  \\
\inferrule[(Rec)]{
\Gamma \cat \rvar{X}: \Delta; \emptyset; \Delta  \proves P \hastype \Proc
\Gamma ; \emptyset; \Delta  \proves \recp{X}{P} \hastype \Proc
\qquad
\inferrule[(Par)]{
\Gamma; \Lambda_{i}; \Delta_{i} \proves P_{i} \hastype \Proc \quad i=1,2
\Gamma; \Lambda_{1} \cat \Lambda_2; \Delta_{1} \cat \Delta_2 \proves P_1 \Par P_2 \hastype \Proc
\qquad
\inferrule[(Nil)]{ }{\Gamma; \emptyset; \emptyset \proves \inact \hastype \Proc}
\\  \\
\inferrule[(Req)]{
\begin{array}{c}
\Gamma; \Lambda; \Delta_1 \proves P \hastype \Proc
\quad
\Gamma; \es; \es \proves u \hastype	\chtype{U}
\\
\Gamma; \es; \Delta_2 \proves V \hastype U
\end{array}
\Gamma; \Lambda; \Delta_1 \cat \Delta_2 \proves \bout{u}{V} P \hastype \Proc
\inferrule[(Acc)]{
\begin{array}{c}
\Gamma; \Lambda_1; \Delta_1 \proves P \hastype \Proc
\quad
\Gamma; \emptyset; \emptyset \proves u \hastype \chtype{U}
\\
\Gamma; \Lambda_2; \Delta_2 \proves x \hastype U
\end{array}
\Gamma\backslash x; \Lambda_1 \backslash \Lambda_2; \Delta_1 \backslash \Delta_2 \proves \binp{u}{x} P \hastype \Proc
\\  \\
\inferrule[(Send)]{
u:S \in \Delta_1 \cat \Delta_2 \quad
\Gamma; \Lambda_1; \Delta_1 \proves P \hastype \Proc
\quad
\Gamma; \Lambda_2; \Delta_2 \proves V \hastype U
\Gamma; \Lambda_1 \cat \Lambda_2; ((\Delta_1 \cat \Delta_2) \setminus u:S) \cat u:\btout{U} S \proves \bout{u}{V} P \hastype \Proc
\\  \\
\inferrule[(Rcv)]{
\Gamma; \Lambda_1; \Delta_1 \cat u: S \proves P \hastype \Proc
\quad
\Gamma; \Lambda_2; \Delta_2 \proves {x} \hastype {U}
\Gamma \backslash x; \Lambda_1\backslash \Lambda_2; \Delta_1\backslash \Delta_2 \cat u: \btinp{U} S \vdash \binp{u}{{x}} P \hastype \Proc
\\ \\
\inferrule[(ResS)]{
\Gamma; \Lambda; \Delta \cat s:S_1 \cat \dual{s}: S_2 \proves P \hastype \Proc \quad S_1 \dualof S_2
\Gamma; \Lambda; \Delta \proves \news{s} P \hastype \Proc
\qquad
\inferrule[(Res)]{
\Gamma\cat a:\chtype{S} ; \Lambda; \Delta \proves P \hastype \Proc
\Gamma; \Lambda; \Delta \proves \news{a} P \hastype \Proc
\end{array}
\]

Typing Rules for $\HO$.

fig:typerulesmys shows the typing rules; we briefly describe them and refer the reader to [18] for a full account.
The shared type $\shot{C}$ is derived using Rule (Prom) only
if the value has a linear type with an empty linear
Rule (EProm) allows us to freely use a shared
type variable as linear.
Abstraction values are typed with Rule (Abs).
Application typing
is governed by Rule (App):
the type $C$ of an application name $u$
must match the type of the application variable $x$ ($\lhot{C}$ or $\shot{C}$).
Rules (Req) and (Acc) type interaction along shared names; the type of the sent/received object $V$ (i.e., $U$) should match the type of the subject $s$ ($\chtype{U}$).
In Rule (Send), the type $U$ of the value $V$ should appear as a prefix in the session type $\btout{U} S$ of $u$.
Rule (Rcv) is its dual.

To state type soundness, we require two auxiliary definitions on session environments.
First, a session environment $\Delta$ is balanced (written $\balan{\Delta}$) if whenever $s: S_1, \dual{s}: S_2 \in \Delta$ then $S_1 \dualof S_2$.
Second, we define the reduction relation $\red$ on session environments as:

\begin{eqnarray*}
\Delta \cat s: \btout{U} S_1 \cat \dual{s}: \btinp{U} S_2 & \red &
\Delta \cat s: S_1 \cat \dual{s}: S_2\\\Delta \cat s: \btsel{l_i: S_i}_{i \in I} \cat \dual{s}: \btbra{l_i: S_i'}_{i \in I} &\red&
\Delta \cat s: S_k \cat \dual{s}: S_k' \ (k \in I)
\end{eqnarray*}

Suppose $\Gamma; \es; \Delta \proves P \hastype \Proc$
Then $P \red P'$ implies $\Gamma; \es; \Delta'  \proves P' \hastype \Proc$
and $\Delta = \Delta'$ or $\Delta \red \Delta'$
with $\balan{\Delta'}$.

When using processes with polyadic communication (cf. r:poly),
we shall assume the extension of the type system defined in [18].

[Typing name-passing constructs]
In ex:np we recalled how to encode name-passing constructs in ; now we show that this translation is typed.
Following the name-passing encoding from [17]
we define a syntactic sugar for types.
The following typing rules for name-passing are derivable:

Γ; Λ_1; Δ_1 P   Γ; Λ_2; Δ_2 b C

Γ; Λ_1 Λ_2; Δ_1 Δ_2 t:Ctb P

Γ; Λ_1; Δ_1 P   Γ; Λ_2; Δ_2 x C

Γ\x; Λ_1\Λ_2; Δ_1 \Δ_2 t: C⊢tx P

[Typing Recursive Servers]

Here we show how to type the processes from <Ref>. Let us define:

\begin{align*}
T = \trec{t}{\btout{U}\vart{t}} \qquad
C = \chtype{\lhot{T}}
\end{align*}

where $U$ is some value type. We recall process $P$
from <Ref> with the additional typing information on bound names
$r$ and $a$:

\begin{align*}
P &= 	\news{r:T}\news{a : C}\big(\bout{a}{V} \inact  \Par \bout{a}{W} \inact  \Par S_a
\Par \binp{\dual r}{x_1}\binp{\dual r}{x_2}Q \big)
\\
V& = \abs{y}{(\bout{y}{V'}S_a\subst{y}{r})}
\\
W& = \abs{z}{(\bout{z}{W'}S_a\subst{z}{r})}
\end{align*}

where $S_a$ stands for $\binp{a}{x} (\appl{x}{r})$.
Let us assume
there is a shared environment
$\Gamma$ under which $V'$ and $W'$ implement type $U$:

\begin{align}
\label{dt:ex1-asm1}
\Gamma;\es; \es &\proves
V' \hastype U \\
\label{dt:ex1-asm2}
\Gamma;\es; \es &\proves
W' \hastype U
\end{align}

Also, we assume  that process $\binp{\dual r}{x_1}\binp{\dual r}{x_2}Q$ is well-typed under
the following environments:

\begin{align}
\label{dt:ex1-asm3}
\Gamma \cat a:C; \es ; \dual r: \dual T  \proves
\binp{\dual r}{x_1}\binp{\dual r}{x_2}Q \hastype \Proc
\end{align}

Under these assumptions,
it holds that the body of process  $P$ correctly implements name $a$
with type $C$, i.e.,

$$  \Gamma;\es; r : T \proves
\news{a : C}
\big(\bout{a}{V} \inact  \Par \bout{a}{W} \inact  \Par S_a \big)  \hastype \Proc$$

We detail the corresponding typing derivations:

\begin{align}
\label{dt:ex-2}
\AxiomC{}
\LeftLabel{\scriptsize (LVar)}
\UnaryInfC{$\Gamma \cat a:C; x:\lhot{T}; \es \proves x \hastype \lhot{T}$}
\AxiomC{}
\LeftLabel{\scriptsize (Sess)}
\UnaryInfC{$\Gamma \cat a:C;\es;y:T \proves y \hastype T$}
\LeftLabel{\scriptsize (App)}
\BinaryInfC{
$\Gamma \cat a:C;x:\lhot{T}; y:T \proves  \appl{x}{y}  \hastype \Proc$
\DisplayProof
\end{align}

\begin{align}
\label{dt:ex-5}
\AxiomC{\eqref{dt:ex-2}}
\AxiomC{}
\LeftLabel{\scriptsize (Sh)}
\UnaryInfC{
$\Gamma \cat a:C;\es; \es \proves a \hastype \chtype{\lhot{T}}$
\AxiomC{}
\LeftLabel{\scriptsize (LVar)}
\UnaryInfC{$
\Gamma \cat a:C;x:\lhot{T}; \es \proves x \hastype \lhot{T}
\LeftLabel{\scriptsize (Acc)}
\TrinaryInfC{
$\Gamma \cat a:C;\es; y:T \proves \binp{a}{x} (\appl{x}{y})  \hastype \Proc$
\DisplayProof
\end{align}

\begin{align}
\label{dt:ex-4}
\AxiomC{
\eqref{dt:ex-5}
\AxiomC{\eqref{dt:ex1-asm1}}
\LeftLabel{\scriptsize (Send)}
\BinaryInfC{
$\Gamma \cat a:C;\es; y:T \proves
\bout{y}{V'}S_a\subst{y}{r}  \hastype \Proc$
\AxiomC{}
\LeftLabel{\scriptsize (Sess)}
\UnaryInfC{
$\Gamma \cat a:C;\es; y:T \proves y \hastype T$
\LeftLabel{\scriptsize (Abs)}
\BinaryInfC{
$\Gamma \cat a:C;\es;\es \proves V \hastype \lhot{T}$
\DisplayProof
\end{align}

\begin{align}
\label{dt:ex-6}
\AxiomC{}
\LeftLabel{\scriptsize (Nil)}
\UnaryInfC{
$\Gamma \cat a:C;\es;\es \proves \inact  \hastype \Proc$
\AxiomC{}
\LeftLabel{\scriptsize (Sh)}
\UnaryInfC{
$\Gamma \cat a:C;\es;\es \proves a \hastype \chtype{\lhot{T}}$
\AxiomC{
\eqref{dt:ex-4}
\LeftLabel{\scriptsize (Req)}
\TrinaryInfC{$\Gamma \cat a:C;\es;\es \proves \bout{a}{V} \inact  \hastype \Proc$}
\DisplayProof
\end{align}

In the following derivation tree the
right-hand side is shown similarly to (<ref>)
using assumption (<ref>) instead of (<ref>):

\begin{align}
\label{dt:ex-8}
\AxiomC{
\eqref{dt:ex-6}
\AxiomC{}
\UnaryInfC{
$\Gamma \cat a:C;\es;\es \proves \bout{a}{W} \inact  \hastype \Proc$
\LeftLabel{\scriptsize (Par)}
\BinaryInfC{
$\Gamma \cat a:C;\es;\es \proves \bout{a}{V} \inact  \Par \bout{a}{W} \inact
\hastype \Proc$
\DisplayProof
\end{align}

Finally we have:

\begin{align*}
\AxiomC{\eqref{dt:ex-8}}
\AxiomC{}
\UnaryInfC{$\Gamma \cat a:C;\es; r : T \proves S_a  \hastype \Proc$}
\LeftLabel{\scriptsize (Par)}
\BinaryInfC{
$\Gamma \cat a:C;\es; r : T \proves
\bout{a}{V} \inact  \Par \bout{a}{W} \inact  \Par S_a
\Par \binp{\dual r}{x_1}\binp{\dual r}{x_2}Q
\hastype \Proc$
\AxiomC{\eqref{dt:ex1-asm3}}
\LeftLabel{\scriptsize (Par)}
\BinaryInfC{
$\Gamma \cat a:C;\es; r : T \cat \dual r : \dual T \proves
\bout{a}{V} \inact  \Par \bout{a}{W} \inact  \Par S_a
\Par \binp{\dual r}{x_1}\binp{\dual r}{x_2}Q
\hastype \Proc$
\LeftLabel{\scriptsize (Res)}
\UnaryInfC{
$\Gamma;\es; r : T \cat \dual r : \dual T \proves
\news{a : C}\big(\bout{a}{V} \inact  \Par \bout{a}{W} \inact  \Par S_a
\Par \binp{\dual r}{x_1}\binp{\dual r}{x_2}Q \big)
\hastype \Proc$
\LeftLabel{\scriptsize (ResS)}
\UnaryInfC{
$\Gamma;\es; \es \proves
\news{r:T}\news{a : C}\big(\bout{a}{V} \inact  \Par \bout{a}{W} \inact  \Par S_a
\Par \binp{\dual r}{x_1}\binp{\dual r}{x_2}Q \big)
\hastype \Proc$
\DisplayProof
\end{align*}

Above, we have omitted details of the right-hand
side derivation; it the same as (<ref>)
with name $y$ substituted with $r$.

[Typing Nested Abstractions]
Here we show how to type process $P$ from <Ref>.
Let types $C_1$ and $C_2$ be defined as
$C_i = \chtype{\lhot{S_i}} $
where $i \in \{1,2\}$ and $S_i$ stands for a tail-recursive type.
For simplicity, we assume that value $V$ has the following typing:

\begin{align}
\label{dt:ex2-a}
a:C_1 \cat b:C_2; \es; \es \proves V \hastype
\lhot{(S_1,S_2)}
\end{align}

The following holds:

\begin{align}
\label{eq:ex2-types-goal}
\es; \es; \es \proves \news{a : C_1} \news{b:C_2}  R \Par S_a \Par S_b
\hastype \Proc
\end{align}

In the following typing derivations, we rely on the following two  typing rules for polyadic elements; they  can be derived from monadic typing rules
from <Ref> (see <Ref>
for details):

$\Gamma;\es;\wtd u:\wtd S
\proves \wtd u \hastype \wtd S$

$\leadsto \in \{\multimap,\rightarrow \}$
$\Gamma;\Lambda;\Delta_1 \proves V \hastype \wtd C \leadsto \diamond$
$\Gamma;\es;\Delta_2 \proves \wtd u \hastype \wtd C$
$\Gamma;\Lambda;\Delta_1 \cat \Delta_2 \proves
\appl{V}{\wtd u}$

Now, we detail the typing derivations that
show (<ref>):

\begin{align}
\label{dt:ex2-t5}
\AxiomC{\eqref{dt:ex2-a}}
\AxiomC{}
\LeftLabel{\scriptsize (PolySess)}
\UnaryInfC{
$a:C_1 \cat b:C_2; \es; y : S_1 \cat z:S_2 \proves y,z \hastype S_1,S_2$
\LeftLabel{\scriptsize (PolyApp)}
\BinaryInfC{
$a:C_1 \cat b:C_2; \es; y : S_1 \cat z:S_2 \proves \appl{V}{(y,z)} \hastype \Proc$
\DisplayProof
\end{align}

\begin{align}
\label{dt:ex2-t4}
\AxiomC{\eqref{dt:ex2-t5}}
\AxiomC{}
\LeftLabel{\scriptsize (Sess)}
\UnaryInfC{
$a:C_1 \cat b:C_2; \es;z:S_2 \proves z \hastype S_2$
\LeftLabel{\scriptsize (Abs)}
\BinaryInfC{
$a:C_1 \cat b:C_2; \es; y : S_1 \proves \abs{z}\appl{V}{(y,z)} \hastype \lhot{S_2}$
\DisplayProof
\end{align}

\begin{align}
\label{dt:ex2-t3}
\AxiomC{}
\LeftLabel{\scriptsize (Nil)}
\UnaryInfC{$a:C_1 \cat b:C_2; \es; \es \proves \inact \hastype \Proc$}
\AxiomC{}
\LeftLabel{\scriptsize (Sh)}
\UnaryInfC{$a:C_1 \cat b:C_2; \es; \es \proves b \hastype \chtype{\lhot{S_2}}$}
\AxiomC{
\eqref{dt:ex2-t4}
\LeftLabel{\scriptsize (Req)}
\TrinaryInfC{
$a:C_1 \cat b:C_2; \es; y:S_1 \proves
\about{b}{\abs{z}\appl{V}{(y,z)}}
\hastype \Proc$
\DisplayProof
\end{align}

\begin{align}
\label{dt:ex2-t2}
\AxiomC{
\eqref{dt:ex2-t3}
\AxiomC{}
\LeftLabel{\scriptsize (Sess)}
\UnaryInfC{
$a:C_1 \cat b:C_2; \es; y:S_1 \proves y \hastype S_1$
\LeftLabel{\scriptsize (Abs)}
\BinaryInfC{
$a:C_1 \cat b:C_2; \es; \es \proves
{\abs{y}\about{b}{\abs{z}\appl{V}{(y,z)}}} \hastype \lhot{S_1}$
\DisplayProof
\end{align}

\begin{align}
\label{dt:ex2-t1}
\AxiomC{$a:C_1 \cat b:C_2; \es; \es \proves \inact \hastype \Proc$}
\AxiomC{}
\LeftLabel{\scriptsize (Sh)}
\UnaryInfC{$a:C_1 \cat b:C_2; \es; \es \proves a \hastype \chtype{\lhot{S_1}}$}
\AxiomC{
\eqref{dt:ex2-t2}
\LeftLabel{\scriptsize (Req)}
\TrinaryInfC{
$a:C_1 \cat b:C_2; \es; \es \proves
\abbout{a}{\abs{y}\about{b}{\abs{z}\appl{V}{(y,z)}}}
\hastype \Proc$
\DisplayProof
\end{align}

Finally we have:

\begin{align*}
\AxiomC{
\eqref{dt:ex2-t1}
\AxiomC{}
\LeftLabel{}
\UnaryInfC{
$a:C_1 \cat b:C_2; \es; \es \proves S_a  \hastype \Proc$
\LeftLabel{\scriptsize (Par)}
\BinaryInfC{
$a:C_1 \cat b:C_2; \es; \es \proves  R \Par S_a
\hastype \Proc$
\AxiomC{}
\LeftLabel{}
\UnaryInfC{
$a:C_1 \cat b:C_2; \es; \es \proves  S_b
\hastype \Proc$
\LeftLabel{\scriptsize (Par)}
\BinaryInfC{
$a:C_1 \cat b:C_2; \es; \es \proves   R \Par S_a \Par S_b
\hastype \Proc$
\LeftLabel{\scriptsize (Res)}
\UnaryInfC{
$a:C_1; \es; \es \proves  \news{b:C_2}  R \Par S_a \Par S_b
\hastype \Proc$
\LeftLabel{\scriptsize (Res)}
\UnaryInfC{
$\es; \es; \es \proves \news{a : C_1} \news{b:C_2}  R \Par S_a \Par S_b
\hastype \Proc$
\DisplayProof
\end{align*}

In the above typing derivation, we remark that   the  judgments

\begin{align}
\label{j:sa}
a:C_1 \cat b:C_2; \es; \es &\proves S_a  \hastype \Proc \\
\label{j:sb}
a:C_1 \cat b:C_2; \es; \es &\proves  S_b
\hastype \Proc
\end{align}

are shown similarly as in (<ref>)
from <Ref>.
to derive (<ref>) reusing
the derivation tree from (<ref>)
we need to substitute $y$ with $r$ and then weaken
the shared environment (<ref>)
with $b:C_2$ (see <Ref>).
by substituting $a$ with $b$ and $y$ with $r$
in the derivation tree (<ref>)
then by weakening the shared environment with $a:C_1$ in
its conclusion we can obtain (<ref>).

[Type Annotations]
We shall often annotate bound names and variables with their respective type.
We will write, e.g., $\news{s:S}P$ to denote that the type of $s$ in $P$ is $S$.
Similarly for values: we shall write $\abs{u:C}{P}$.
Also, letting $\leadsto \in \{\lollipop, \sharedop\}$, we may write
$\abs{u:\slhotup{C}}{P}$ to denote that the value is linear (if $\leadsto = \lollipop$) or shared (if $\leadsto = \sharedop$).
That is, we write $\abs{u:\slhotup{C}}{P}$ if
$\Gamma ; \Lambda; \Delta \proves \abs{{u}}{P} \hastype \slhot{{C}}$, for some $\Gamma$, $\Lambda$, and $\Delta$.

Having introduced the core session process language , we now move to detail its type-preserving decomposition into minimal session types.

§ DECOMPOSING SESSION-TYPED PROCESSES

In this section we define minimal session types and present a decomposition of well-typed processes: given a process $P$ typable with (standard) session types, our decomposition returns a process denoted $\D{P}$, typable with minimal session types.

The definition of  $\D{P}$ follows Parrow's trio processes for the $\pi$-calculus [21].
A trio process is a process with at most three sequential prefixes.
Roughly speaking, if $P$ is a process with $k$ sequential actions, then $\D{P}$ will contain $k$ trios running in parallel: each of them will enact exactly one action from $P$.
The decomposition is carefully designed to ensure that trios trigger each other by preserving the sequencing in $P$.

This section is organized as follows.
First, in <Ref>, we use examples to discuss some key ideas of the decomposition.
Then, in <Ref>, we give the full definitions of minimal session types and the decomposition functions.
We define decomposition functions for types $\Gt{-}$ and for processes $\D{-}$.
The former “slices” a session type $S$ and returns a list of minimal session types, corresponding to individual actions in $S$; the latter breaks down an process into a parallel composition of processes.
We demonstrate these notions on a number of examples in <Ref>.
Finally, in <Ref> we establish the static correctness result (<Ref>):
if $P$ is well-typed
under session types $S_1, \ldots, S_n$, then $\D{P}$ is typable using the
minimal session types $\Gt{S_1}, \ldots, \Gt{S_n}$.
The issue of dynamic correctness, i.e., the operational correspondence between $P$ and $\D{P}$, is treated separately in <Ref>.

We use colors to differentiate the operations on processes (in pink) and on types (in green).
The usage of the colors is for visual aid only, and is not important for the mathematical content of the presented material.

§.§ Key Ideas

ann = [draw=none,fill=none,right]

[] (L1) at (-*1.5-0.1, 1.5) Source process $P_1$:;

[draw, ] (P1) at (-*1.5, 0.5) $P_1$;
[draw, ] (P2) at (-/2.0, 0.5) $P_2$;
[draw, ] (P3) at (/2.0, 0.5) $P_3$;
[draw, circle] (P4) at (*1.5, 0.5) $\inact$;

[->, color=black](P1) edge[] node [above]
$u:\abinp{}{\mathsf{str}}$ (P2);
[->, color=black](P2) edge[] node [above]
$u:\abinp{}{\mathsf{int}}$ (P3);
[->, color=black](P3) edge[] node [above]
$u:\about{}{\mathsf{bool}}$ (P4);

ann = [draw=none,fill=none,right]
[align=left] (L2) at (-*1.25, -0.5) Decomposed process $\D{P_1}$:;

[draw, ] (T1) at (-*1.5, -)̣ $Q_1$;
[draw, ] (T11) at (-*1.5, --̣) $Q'_1$;

[->, color=black](T1) edge[] node [left]
$u_1:\abinp{}{\mathsf{str}}$ (T11);

at (-, -)̣ $\parallel$;
[draw, ] (T2) at (-/2.0, -)̣ $Q_2$;
[draw, ] (T22) at (-/2.0, --̣) $Q'_2$;

[->, color=black](T2) edge[] node [left]
$u_2:\abinp{}{\mathsf{int}}$ (T22);

at (0, -)̣ $\parallel$;
[draw, ] (T3) at (/2.0, -)̣ $Q_3$;
[draw, ] (T33) at (/2.0, --̣) $Q'_3$;
[->, color=black](T3) edge[] node [left]
$u_3:\about{}{\mathsf{bool}}$ (T33);

at (, -)̣ $\parallel$;

[draw, ] (T4) at (*1.5, -)̣ $Q_4$;

[->, dashed, color=red, align=left](T11) edge[bend left=25] node [pos=0.05, right]
$x:\mathsf{str}$ (T2);
[->, dashed, color=red, align=left](T22) edge[bend left=25] node [pos=0.05, right]
$x:\mathsf{str}$, $y:\mathsf{int}$ (T3);
[->, dashed, color=red](T33) edge[bend left=20] node [left]  (T4);

[draw=none] ;

Our decomposition function
$\D{-}$, illustrated. Nodes
represent process states, `$\parallel$' represents
parallel composition of processes, black arrows stand for actions, and red arrows
indicate synchronizations that preserve the sequentiality of the source process by activating trios and propagating (bound) values.

Consider a process $P_1$ that implements the (standard) session type $S=\btinp{\mathsf{str}}\btinp{\mathsf{int}}\btout{\mathsf{bool}}\tinact$ along name $u$.
In process $P_1$, name $u$ is not a single-use resource; rather, it is used several times to implement the communication actions in $S$; fig:decomp (top) graphically depicts the actions and the corresponding states.

The decomposition $\D{P_1}$ is illustrated
in the bottom part of fig:decomp: it is defined as the parallel composition of four processes
$Q_i$ (for $i \in \{1, \ldots, 4\}$).
Each process $Q_1$, $Q_2$, and $Q_3$ mimic one action of $P_1$ on an indexed name $u_i$, while $Q_4$ simulates the termination   of the session.
This way, a single name $u$ in $P_1$ is decomposed into a sequence of names $u_1,u_2,u_3$ in $\D{P_1}$.

The processes $Q_1$, $Q_2$, $Q_3$, and $Q_4$ are composed in parallel, but we would like to retain the same sequentiality of actions on the channels $u_i$ as we have on the channel $u$.
To that end, each process $Q_i$, with the exception of $Q_1$, does not perform its designated action on $u_i$ until it gets activated by the previous process.
In turn, after $Q_i$ performs an action on $u_i$ it evolves to a state $Q'_i$, which is responsible for activating the next process $Q_{i+1}$.
In fig:decomp, the activations are indicated by red arrows.
In general, the decomposition orchestrates the activation of sub-processes, following the sequencing prescribed by the session types of the given process.
Therefore, assuming a well-typed source process, our decomposition codifies the sequentiality in
session types into the process level.

The activation mechanism includes the propagation of values across sub-processes (cf. the labels on red arrows).
This establishes a flow of values from sub-processes binding them to those that use them (i.e., it makes  variable bindings explicit).  For example, in $P_1$, the Boolean value being sent over as part of the session $S$ might depend on the previously received string and integer values.
Therefore, both of those values have to be propagated to the process $Q_3$, which is responsible for sending out the Boolean.

In this example a single name $u : S$ is decomposed into a sequence $\wtd u = (u_1,\ldots,u_n)$: each $u_i \in \wtd u$ is a single-use resource, as prescribed by its minimal session type.
Such is the case for non-recursive types $S$.
When $S$ is recursive, the situation is more interesting: each action of $S$ can be repeated many times, and therefore the names $\wtd u$ should be propagated across trios to enable potentially many uses.
As an example, consider the recursive session type
$S=\trec{t}{\btinp{\mathsf{int}}\btout{\mathsf{\mathsf{int}}}}{\vart{t}}$, in which an input and an output actions are repeated indefinitely.
Consider the following process

\begin{align*}
\underbrace{\bout{r}{-z}}_{{T_2}}
\underbrace{\binp{r}{z}}_{{T_3}}
\underbrace{\bout{r}{z}}_{{T_4}}
\underbrace{\appl{V}{r}}_{{T_5}}
\end{align*}

which makes use of the channel $r : S$ and where $V$ has type $\shot{S}$.
fig:rec-subfig2 (top) gives the first four actions of $R_1$ and the corresponding sates: the body of type $S$ prescribes two actions on name $r$, performed sequentially in $R_1$ and $R_2$; subsequent actions (enabled in $R_3$
and $R_4$) correspond to a “new instance” of the body of $S$.

The decomposition $\D{R_1}$, depicted in fig:rec-subfig2 (bottom), generates a trio process for each prefix in $R_1$; we denote prefixes with their corresponding trios ${T_1}, \ldots, {T_5}$.
The type decomposition function on types, $\Gt{-}$, slices $S$ into two minimal tail-recursive types: $M_1 = \trec{t}\btinp{\textsf{int}}\vart{t}$ and $M_2 = \trec{t}\btout{\textsf{int}}\vart{t}$.

In the recursive case, a key idea is that trios that mimic actions prescribed by a recursive session types should reuse names, which should be propagated across trios.
This way, for instance, trios $T_1$ and $T_3$ mimic the same (input) action, and so they both should use the same name ($r_1$).
To achieve this, we devise a mechanism that propagates names with tail-recursive types (such as $(r_1,r_2)$) through the trios.
These propagation actions are represented by blue arrows in fig:rec-subfig2 (bottom).
In our example, $T_3$ gathers the complete decomposition of names from preceding trios $(r_1,r_2)$; it mimics an input action on $r_1$ and makes $(r_1,r_2)$ available to future trios (i.e., $T_4$ and $T_5$).

Since the same tail-recursive names can be (re)used infinitely often, we propagate tail-recursive names through the following process.
All the names ${\wtd r}$ corresponding to the decomposition of a tail-recursive name $r$ are bound in the process

$$\recprov{r}{x}{\wtd r},$$

which is similar to the servers discussed in <Ref>.
We call these processes recursive propagators, and each tail-recursive name in the original process $P$ has a dedicated propagator in $\D{P}$ on the channel $\prop^{r}$.
Whenever a trio has to perform an action $\alpha(r_i)$ on one of the decomposed tail-recursive names (i.e., a decomposition of an input action `$\binp{r}{y}$' or an output action `$\bout{r}{V}$' on the name $r$), it first has to request the name from the corresponding recursive propagator by performing an output action $\abbout{\prop^r}{N}$, where value $N$ is the abstraction

$$N = \abs{\wtd z} \alpha({z_i}).\big(\apropout{k+1}{\wtd w} \Par \recprov{r}{x}{\wtd z} \big).$$

A synchronization on $\prop^r$ will result in the reduction:

\[
\recprov{r}{x}{\wtd r} \Par \abbout{\prop^r}{N} \red \alpha({r_i}).\big(\apropout{k+1}{\wtd w} \Par
\recprov{r}{x}{\wtd r}
\big).
\]

The resulting process first simulates $\alpha(r)$  and subsequently  reinstates the recursive propagator on $\prop^r$, for the benefit of the other trios requiring access to the names $\wtd r$.
See  <Ref> below (Page ex:recdec) for further illustration of this method.

This decomposition strategy handles processes with recursive types which are simple and contractive.
That is, recursive types of the form $\trec{t}{S}$, where the body $S \neq \vart{t}$ does not itself contain recursive types.
Unless stated otherwise, we consider tail-recursive session types such as, e.g., $S = \trec{t}\btinp{\mathsf{int}}\btinp{\mathsf{bool}}\btout{\mathsf{bool}}\vart{t}$.
Non-tail-recursive session types such as $\trec{t}{\btinp{\shot{(\widetilde T,\vart{t})}}\tinact}$,  used in the fully-abstract encoding of into  [17], can also be accommodated; see <Ref> below.

ann = [draw=none,fill=none,right]

[] (L1) at (-*2.0-0.175, 6.0) Source process $R_1$:;

[draw, ] (P1) at (-2*, 5) $R_1$;
[draw, ] (P2) at (-, 5) $R_2$;
[draw, ] (P3) at (0, 5) $R_3$;

[draw, circle] (P4) at (, 5) $R_4$;

[draw, circle] (P5) at (2*, 5) $R_5$;

[->, color=black](P1) edge[] node [above]
$r:\abinp{}{\mathsf{int}}$ (P2);
[->, color=black](P2) edge[] node [above]
$r:\about{}{\mathsf{int}}$ (P3);
[->, color=black](P3) edge[] node [above]
$r:\abinp{}{\mathsf{int}}$ (P4);
[->, color=black](P4) edge[] node [above]
$r:\about{}{\mathsf{int}}$ (P5);

[] (L2) at (-*1.75-0.1, +1) Decomposed process $\D{R_1}$:;

[draw, ] (T1) at (-2*, ) $T_1$;
[draw, ] (T11) at (-2*, -) $T'_1$;

[->, color=black, align=center](T1) edge[] node [pos=0.8, left]
$\abinp{}{\mathsf{int}}$ (T11);

at (-1.5*,) $\parallel$;
[draw, ] (T2) at (-,) $T_2$;
[draw, ] (T22) at (-, -) $T'_2$;

[->, color=black, align=center](T2) edge[] node [pos=0.8, left]
$\about{}{\mathsf{int}}$ (T22);

at (-0.5*, ) $\parallel$;
[draw, ] (T3) at (0, ) $T_3$;
[draw, ] (T33) at (0, -) $T'_3$;
[->, color=black](T3) edge[] node [pos=0.8, left]
$r_1:$$\abinp{}{\mathsf{int}}$ (T33);

at (0.5*, ) $\parallel$;

[draw, ] (T4) at (, ) $T_4$;
[draw, ] (T44) at (, -) $T'_4$;

[->, color=black](T4) edge[] node [pos=0.8, left]
$r_2:$$\about{}{\mathsf{int}}$ (T44);

at (1.5*, ) $\parallel$;

[draw, ] (T5) at (2*, ) $T_5$;

[->, dashed, color=blue](T11)
edge[bend left=] node
[pos=, left] $r_1$,$r_2$ (T2);
[->, dashed, color=blue](T22)
edge[bend left=] node [pos=, left] $r_1$,$r_2$ (T3);
[->, dashed, color=blue](T33)
edge[bend left=] node [pos=, left] $r_1$,$r_2$ (T4);
[->, dashed, color=blue](T44)
edge[bend left=] node [pos=, left] $r_1$,$r_2$ (T5);

Decomposition of processes with recursive session types, illustrated. Dashed blue arrows represent the propagation of tail-recursive names ($r_1$,$r_2$) across trios.

§.§ The Decomposition

Here we formally present the decomposition of processes.
We start introducing some preliminary definitions, including the definition of an auxiliary function, called the breakdown function.

Following Parrow [21] we adopt some useful terminology
and notation on trios.
The context of a trio is a tuple of variables
$\widetilde x$, possibly empty, which  makes variable bindings explicit.
We use
a reserved set of propagator names (or simply propagators),
denoted with $\prop_k, \prop_{k+1}, \ldots$, to carry contexts and trigger the
subsequent trio. A process with less than three sequential prefixes is called a
degenerate trio. Also, a leading trio is the one that receives a
context, performs an action, and triggers the next trio; a control trio
only activates other trios.

The breakdown function works on both processes and values. The breakdown of
process $P$ is denoted by $\B{k}{\tilde x}{P}$, where $k$ is the index for the
propagators $\prop_k$, and $\widetilde x$ is the context to be received by the
previous trio. Similarly, the breakdown  of a value $V$ is denoted by
$\V{k}{\tilde x}{V}$.

§.§.§ Minimal Session Types and Decomposing Types

We start by introducing minimal session types as a fragment of <Ref>:

The syntax of minimal session types for is defined as follows:

\begin{align*}
U & \bnfis		\shot{\widetilde{C}} \bnfbar \lhot{\widetilde{C}}
\\
C  & \bnfis		M  \bnfbar  {\chtype{U}}
\\
M &
\bnfis 	\mugamma  \bnfbar  \btout{\widetilde{U}} \mugamma
\bnfbar \btinp{\widetilde{U}} \mugamma \bnfbar \trec{t}{M }	\\
\mugamma & \bnfis \tinact \bnfbar \vart{t}
\end{align*}

The above definition is minimal in its use of sequencing, which is only present in
recursive session types such as $\trec{t}{\btout{U}\vart{t}}$ and
$\trec{t}{\btinp{U}\vart{t}}$—these are  tail-recursive session types with exactly one session prefix.
Clearly, this minimal type structure induces a reduced set of typable processes.
A type system for based on minimal session types can be straightforwardly obtained by specializing the definitions, typing rules, and results summarized in sec:types.
We refer to processes and terms typeable with minimal session types as MST processes and terms, respectively.

We now define how to “slice” a standard session type into a list of
minimal session types.
We need the following auxiliary definition.

Let $C$ be a channel type.

* We write $\tr(C)$  to indicate that $C$ is a tail-recursive session type.

* Given $u:C$, we write $\lin{u}$ if a session type (i.e. $C = S$ for some $S$) that is not tail recursive.

With a slight abuse of notation, we write $\tr(u)$ to mean $u:C$ and $\tr(C)$ (and similarly for $\neg \tr(u)$).

Given the session, higher-order, and shared types of <Ref>, the type decomposition function  $\Gt{-}$ is defined using the auxiliary function $\Rt{-}$ as in <Ref>.
We write $\len{\Gt{S}}$ to denote the length of  $\Gt{S}$ (and similarly for $\Rt{-}$).

\begin{align*}
\Gt{\btout{U}{S}} &=
\begin{cases}
\btoutt{\Gt{U}}   &  \text{if $S = \tinact$} \\
\btoutt{\Gt{U}}\, ,\Gt{S} & \text{otherwise}
\end{cases}
\\
\Gt{\btinp{U}{S}} &=
\begin{cases}
\btinpt{\Gt{U}}  &  \text{if $S = \tinact$} \\
\btinpt{\Gt{U}} \, , \Gt{S} & \text{otherwise}
\end{cases}
\\
\Gt{\trec{t}{S}} & =
\begin{cases}
\Rt{S} & \text{if $\tr(\trec{t}{S})$} \\
\trec{t}{\Gt{S}} & \text{if $\neg\tr(\trec{t}{S})$ and $\Gt{S}$ is a singleton}
\end{cases}
\\
\Gt{\tinact} &= \tinact
\\
\Gt{\vart{t}} & = \vart{t}
\\
\Gt{\lhot{C}} &= \lhot{\Gt{C}}
\\
\Gt{\shot{C}} &= \shot{\Gt{C}}
\\
\Gt{\chtype{U}} &= \chtype{\Gt{U}}
\\
\Rt{\vart{t}} & = \epsilon
\\
\Rt{\btout{U}S} &= \trec{t}{\btout{\Gt{U}}} \tvar{t}, \Rt{S}
\\
\Rt{\btinp{U}S} & = \trec{t}{\btinp{\Gt{U}}} \tvar{t}, \Rt{S}
\end{align*}

Decomposing session types into minimal session types (<Ref>)

The decomposition is self-explanatory;
intuitively, if a session type $S$ contains $k$ input/output actions, the list $\Gt{S}$ will contain $k$ minimal session types.
For a tail recursive $\trec{t}{S}$, $\Gt{\trec{t}{S}}$ is a list of minimal recursive session types, obtained
using the auxiliary function $\Rt{-}$ on   $S$: if $S$ has $k$ prefixes
then the list  $\Gt{\trec{t}{S}}$ will contain $k$ minimal recursive session types.

We illustrate <Ref> with three examples.
[Decomposition a Non-recursive Type]
Let $S = \btinp{\mathsf{int}} \btinp{\mathsf{int}} \btout{\mathsf{bool}} \tinact$ be the session type given in s:intro.
Then $\Gt{S}$ denotes the list   $\btinpt{\mathsf{int}}  \, ,  \btinpt{\mathsf{int}}   \, , \btoutt{\mathsf{bool}} $.

[Decomposing a Recursive Type]

Let $S = \trec{t}S'$ be a recursive session type, with
By <Ref>, since $S$ is tail-recursive,  $\Gt{S} = \Rt{S'}$.
Further, $\Rt{S'} = \trec{t}\btinp{\mathsf{\Gt{int}}} \vart{t},
\Rt{\btinp{\mathsf{bool}}\btout{\mathsf{bool}}\vart{t}}$. By definition of
$\Rt{-}$, we obtain
$$\Gt{S} = \trec{t}\btinp{\mathsf{int}} \vart{t},~
\trec{t}\btinp{\mathsf{bool}} \vart{t},~ \trec{t}\btout{\mathsf{bool}}
\vart{t}, \Rt{t}$$
(using $\Gt{\mathsf{int}} = \mathsf{int}$ and
$\Gt{\mathsf{bool}} = \mathsf{bool}$). Since $\Rt{\vart{t}} = \epsilon$, we
$$\Gt{S} = \trec{t}\btinp{\mathsf{int}} \vart{t},~
\trec{t}\btinp{\mathsf{bool}} \vart{t},~ \trec{t}\btout{\mathsf{bool}}
\vart{t}$$

In addition to tail-recursive types that are handled by $\Rt{-}$, we need to
support non-tail-recursive types of form $\trec{t}{\btinp{\shot{(\widetilde
T,\vart{t})}}\tinact}$ that are essential for the encoding of recursion in into .
The following example illustrates such a decomposition.
[Decomposing a Non-tail-recursive Type]

$S =
\trec{t}{\btinp{\shot{(\btinp{\mathsf{str}}\btout{\mathsf{str}}\tinact,
\vart{t})}}\tinact}$
be a non-tail-recursive type. We obtain the following decomposition:

\begin{align*}
\Gt{S} &= \trec{t}{\Gt{\btinp{\shot{(\btinp{\mathsf{str}}
\btout{\mathsf{str}}\tinact, \vart{t})}}\tinact}} \\
&= \trec{t}{{?({\Gt{\shot{(\btinp{\mathsf{str}}
\btout{\mathsf{str}}\tinact,\vart{t})}}})}}
\\
\trec{t}{\btinpt{{{{\shot{(\btinpt{\mathsf{str}},
\btoutt{\mathsf{str}},\vart{t})}}}}}} = M
\end{align*}

We can see that we have generated
minimal non-tail-recursive type $M$.

Now, we illustrate the encoding of recursive
processes into from [17] using the
non-tail-recursive type  $S$ given in the above example.
[Encoding Recursion]

Consider the process
$P = \recp{X}\binp{a}{m}\bout{a}{m}X$, which contains recursion and so it  is not an $\HO$ process.
Still, $P$ can be encoded into $\HO$ as follows [17]:

\begin{align*}
\map{P} = \binp{a}{m}\bout{a}{m} \news{s}
{(\appl{V}{(a,s)} \Par \about{\dual s}{V})}
\end{align*}

where the value $V$ is an abstraction that potentially reduces to $\map{P}$:

\begin{align*}
V = \abs{(x_a,y_1)}\binp{y_1}{z_x}\binp{x_a}{m}
\bout{x_a}{m}\news{s}
{(\appl{z_x}{(x_a,s)} \Par \bout{\dual s}{z_x}\inact)}
\end{align*}

As detailed in [17], this encoding relies on non-tail-recursive types.
In particular, the bound name $s$ in $\map{P}$ is typed
with the following type, discussed above in ex:ntrsts:

\begin{align*}
S = \trec{t}{\btinp{\shot{(\btinp{\mathsf{str}}\btout{\mathsf{str}}\tinact,
\vart{t})}}\tinact}
\end{align*}

We compose $\map P$ with an appropriate client process to illustrate the encoding of recursion. Below $R$ stands for some unspecified process such that $a \in \rfn{R}$:

\begin{align*}
\map{P} \Par \bout{a}{W} \binp{a}{b}R  & \red^2 \news{s}
{(\appl{V}{(a,s)} \Par \about{\dual s}{V})} \Par R \\
&  \red  \news{s} {(\binp{s}{z_x}\binp{a}{m}
\bout{a}{m}\news{s'}
{(\appl{z_x}{(a,s')} \Par \about{\dual {s'}}{z_x})} \Par \about{\dual s}{V})} \Par R \\
& \red \binp{a}{m}
\bout{a}{m}\news{s'}
{(\appl{V}{(a,s')} \Par \about{\dual {s'}}{V})} \Par R
\\
& = \map{P} \Par R
\end{align*}

§.§.§ Decomposing Processes

As we have seen, each session type $S$ is decomposed into $\Gt{S}$, a list  of minimal session types.
Accordingly, given an assignment $s : S$, we decompose $s$ into a series of names, one for each action in $S$.
We use indexed names to formalize the names used by minimally typed processes.
Formally, an indexed name is a pair $(n, i)$ with $i \in \mathbb{N}$, which we denote as $n_i$.
We refer to processes with indexed names  as indexed processes.

The decomposition of processes is defined in <Ref>, and it relies on a breakdown function, denoted $\B{k}{\tilde x}{-}$, which operates on indexed processes.
Before we dive into those functions we present some auxiliary definitions.

To handle the unfolding of recursive types, we shall use the following auxiliary function, which decomposes guarded recursive types, by first ignoring all the actions until the recursion.

Let $S$ be a session type. The function $\Rts{}{s}{-}$: is defined as follows

\begin{align*}
\Rts{}{s}{\trec{t}{S}} & = \Rt{S}
\\
\Rts{}{s}{\btinp{U}S} & = \Rts{}{s}{S}
\\
\Rts{}{s}{\btout{U}S} & = \Rts{}{s}{S}
\end{align*}

Let $T = \btinp{\mathsf{bool}}\btout{\mathsf{bool}}S$ be a derived unfolding
of  $S$ from ex:rtype. Then, by <Ref>,
$\Rts{}{s}{T}$ is the list of minimal recursive types obtained as follows:
first, $\Rts{}{s}{T} = \Rts{}{s}{\btout{\mathsf{bool}}\trec{t}S'}$ and after
one more step, $\Rts{}{s}{\btout{\mathsf{bool}}\trec{t}S'} =
\Rts{}{s}{\trec{t}S'}$. Finally, we have $\Rts{}{s}{\trec{t}S'} = \Rt{S'}$.
We get the same list of minimal types as in ex:rtype: $\Rts{}{s}{T}
= \trec{t}{\btinp{\mathsf{int}}\vart{t}},
\trec{t}{\btinp{\mathsf{bool}}\vart{t}}, \trec{t}{\btout{\mathsf{bool}}
\vart{t}}$.

Given an unfolded recursive session type $S$, the auxiliary function $\indT{S}$ returns the position of the top-most prefix of $S$ within its body.

Let $S$ be an (unfolded) recursive session type. The function $\indT{S}$ is defined as follows:

\begin{align*}
\indT{S} = \begin{cases}
\indTaux{S'\subst{S}{\vart{t}}}{0} & \text{if} \ S =\trec{t}{S'} \\
\indTaux{S}{0} & \text{otherwise}
\end{cases}
\end{align*}

where $ \indTaux{S}{l}$:

\begin{align*}
\indTaux{\trec{t}{S}}{l} & = \len{\Rt{S}} - l + 1
\\
\indTaux{\btout{U}S}{l}  & = \indTaux{S}{l+1}
\\
\indTaux{\btinp{U}S}{l} & = \indTaux{S}{l+1}
\end{align*}

$S' = \btinp{\mathsf{bool}}\btout{\mathsf{bool}}S$ where
$S$ is as in ex:rtype.
Then $\indT{S'} = 2$ since the top-most prefix of $S'$ (`$\btinp{\mathsf{bool}}$') is
the second prefix in the body of $S$.

In order to determine the required number of propagators ($\prop_k, \prop_{k+1}, \ldots$) required in the breakdown of processes and  values, we  define the degree of a process:

Let $P$ be an process.
The degree of $P$, denoted $\plen{P}$, is defined as

$$ \plen{P} =
\begin{cases}
\plen{Q} + 1 & \text{if $P = \bout{u_i}{V}Q$ or $P=\binp{u_i}{y}Q$}
\\
\plen{P'} & \text{if $P = \news{s:S}P'$}
\\
\plen{Q} + \plen{R} + 1 & \text{if $P = Q \Par R$}
\\
1 & \text{if $P = \appl{V}{u_i}$ or $P = \inact$}
\end{cases}

We define an auxiliary function that “initializes” the indices of a tuple of
names, for turning a regular process into an indexed process.

Let $\widetilde u = (a,b,s,s',r,r',\ldots)$ be a finite tuple of names.
We shall write $\mathsf{init}(\widetilde u)$ to denote the tuple of indexed names

Let $n_i$ be an indexed name. We define $\nextn{n_i} = \linecondit{\lin{n_i}}{\incrname{n}{i}}{\{\}}$.

Recall that we write
`$\apropinp{k}{}$' and  `$\apropout{k}{}$'
to denote input and output prefixes in which the value communicated along $\prop_k$ is not relevant.
While `$\apropinp{k}{}$' stands for `$\apropinp{k}{x}$',
`$\apropout{k}{}$' stands for `$\apropout{k}{\abs{x}{\inact}}$'.
Their corresponding minimal types are
which are
denoted by
$\btinpt{-}$ and  $\btoutt{-}$, respectively.

Given a typed process $P$, we write $\rfn{P}$ to denote the set of free names of
$P$ whose types are recursive. As mentioned above, for each $r \in \rfn{P}$ with
$r : {S}$ we shall rely on a  control trio of the form
$\binp{\prop^r}{x}\appl{x}{\widetilde r}$, where $\widetilde{r} = r_1, \ldots,

Let $P$ be a closed process with $\widetilde u = \fn{P}$ and $\widetilde v = \rfn{P}$.
The decomposition of $P$, denoted $\D{P}$, is
defined as:

\D{P} = \news{\widetilde \prop}\news{\widetilde \prop_r}\Big(
\propout{k}{} \inact \Par \B{k}{\epsilon}{P\sigma} \Par \prod_{r \in \tilde{v} }
\recprov{r}{x}{\wtd r}
\Big)

where: $k >0$;
$\widetilde \prop = (\prop_k,\ldots,\prop_{k+\plen{P}-1})$;
$\widetilde{\prop_r} = \bigcup_{r\in \tilde{v}}\prop^r$;
$\sigma = \subst{\mathsf{init}(\widetilde u)}{\widetilde u}$.

Notice that when $\rfn{P} = \emptyset$, then
\D{P} = \news{\widetilde \prop}(
\propout{k}{} \inact \Par \B{k}{\epsilon}{P\sigma})
We now discuss the breakdown of process $P$, denoted $\B{k}{\tilde x}{P}$.

The Breakdown Function.
Given  a context $\widetilde x$ and a  $k>0$, the breakdown of an indexed
process $P$, denoted $\B{k}{\tilde x}{P}$, is defined recursively on the structure of processes. The definition of $\B{k}{\tilde x}{-}$ relies on an auxiliary
breakdown function on values, denoted  $\V{k}{\tilde x}{-}$.
When $V = y$, then the breakdown function is simply the identity:
$\V{}{\tilde x}{y} = y$.

$\B{k}{\tilde x}{P}$

$\bullet~ \neg\tr(S)$:

$\propinp{k}{\wtd x}
\bbout{u_i}{\V{k+1}{\tilde y}{V\sigma}}
\apropout{k+1}{\wtd w}  \Par \B{k+1}{\tilde w}{Q\sigma}$

$\bullet~ \tr(S)$:

$\propinp{k}{\wtd x}
\abbout{\prop^u}{N_V}   \Par
\B{k+1}{\tilde w}{Q}$

$N_V = \abs{\wtd z}
{\bbout{z_{\indT{S}}}{\V{k+1}{\tilde y}{V}}}{} \big(\apropout{k+1}{\wtd w} \Par
\recprov{u}{x}{\wtd z}\big)

$\widetilde y = \fv{V}$

$\widetilde w = \fv{Q}$

$\sigma = \nextn{u_i}$

$\wtd z = (z_1,\ldots,z_{\len{\Rts{}{s}{S}}})$

$\bullet~ \tr(S)$:

$\propinp{k}{\wtd x}\binp{u_i}{y} \apropout{k+1}{\wtd w}
\Par \B{k+1}{\tilde w}{Q\sigma}$

$\bullet~ \neg\tr(S)$:

$\propinp{k}{\wtd x}\abbout{\prop^u}
\Par \B{k+1}{\tilde w}{Q}$

$N_y = \abs{\wtd z}{\binp{z_{\indT{S}}}{y} \big(\apropout{k+1}{\wtd w} \Par
\recprov{u}{x}{\wtd z}} \big)$

$\wtd w = \fv{Q} $

$\sigma = \nextn{u_i}$

$\wtd z = (z_1,\ldots,z_{\len{\Rts{}{s}{S}}})$

$\appl{V}{(\wtd r, u_i)}$

$\propinp{k}{\widetilde x}\overbracket{\prop^{r_1}!\big\langle
\lambda \widetilde z_1. \prop^{r_2}!\langle\lambda \widetilde z_2.\cdots.
\prop^{r_n}!\langle \lambda \widetilde z_n.}^{n = |\tilde r|}
Q \rangle \,\rangle \big\rangle$

$Q = \appl{\V{k+1}{\tilde x}{V}}{(\widetilde z_1,\ldots,
\widetilde z_n, \widetilde m)}$

$\forall r_i \in \widetilde r.(r_i: S_i \wedge \mathsf{tr}(S_i) \wedge$

$\wtd{z_i} = (z^i_1,\ldots,z^i_{\len{\Rts{}{s}{S_i}}}))$

$\wtd m = (u_i, \ldots, u_{i+\len{\Gt{C}}-1})$

$\bullet \neg\tr(C):$

$\news{\widetilde{s}:\Gt{C}}{\,\B{k}{\tilde x}

$\bullet ~\tr(C):$

\news{c^s}
\recprov{s}{x}{\wtd s}
\Par$

\recprov{\bar s}{x}{\wtd {\dual s}}
\Par$
$\B{k}{\tilde x}{P'\sigma}$

$\wtd x = \fv{P'}$

$\wtd{s} = (s_1,\ldots,s_{\len{\Gt{C}}})$

$\wtd {\dual{s}} = (\dual{s_1},\ldots,\dual{s_{\len{\Gt{C}}}})$

$\sigma=\subst{s_1 \dual{s_1}}{s \dual{s}}$

$Q \Par R$

$\propinp{k}{\wtd x} \propout{k+1}{\wtd y}
\apropout{k+\degree+1}{\wtd w}   \Par \B{k+1}{\tilde y}{Q} \Par \B{k+\degree+1}{\tilde w}{R}$

$\wtd y  = \fv{Q}$

$\wtd w = \fv{R}$

$\degree = \plen{Q}$

$\V{}{\tilde x}{V}$

$\abs{(\wtd y z)}P$

$\abs{(\widetilde{y^1},\ldots,\widetilde{y^n}, \widetilde z):
\slhotup{(\widetilde{M})}}{N}$

$\widetilde{M} = (\Gt{S_1},\ldots,\Gt{S_n}, \Gt{C})$

$N = \news{\widetilde \prop} \news{\widetilde \prop_r}
\prod_{i \in \len{\widetilde y}}
(\recprov{y_i}{x}{\wtd y^i})
\Par \apropout{1}{\widetilde x}
\Par$

$\B{1}{\tilde x}{P \subst{z_1}{z}}$

$\wtd y z : \wtd S C$

$\forall y_i \in \widetilde y.(y_i: S_i \wedge \mathsf{tr}(S_i) \wedge$

$\widetilde{y^i} = (y^i_1,\ldots,y^i_{\len{\Gt{S_i}}}))$

$\widetilde z = (z_1,\ldots,z_{\len{\Gt{C}}})$

$\wtd \prop = (\prop_1,\ldots,\prop_{\plen{P}})$

$\widetilde{\prop_r} = \bigcup_{r\in \tilde{y}}\prop^r$

The breakdown function for processes and values.

The breakdown function relies on type information, in two ways.
First, names are decomposed based on their session types.
Second, for most constructs the shape of decomposed process depends on whether the associated session type is tail-recursive or not.
The definition of the breakdown function is given in t:bdowncore.
Next, we describe each of the cases of the definition.
In ss:examples (Page ss:examples) we develop several examples.

The decomposition of $\bout{u_i}{V}Q$ is arguably the most interesting case, as both the sent value $V$ and the continuation $Q$ have to be decomposed.
We distinguish two cases:

* If $\neg\tr(u_i)$ then  $u_i$ is linear or shared, and then we have:

\begin{align*}
\B{k}{{\tilde x}}{\bout{u_i}{V}Q} =
\propinp{k}{\widetilde x}
\bbout{u_i}{\V{}{\tilde y}{V\sigma}}
\apropout{k+1}{\wtd w}  \Par
\B{k+1}{\tilde w}{Q\sigma}
\end{align*}

This decomposition consists of a leading trio that
mimics an output action in parallel with the breakdown of  $Q$.
The context  $\wtd x$ must include the free variables of $V$ and $Q$, which are
denoted $\wtd y$ and $\wtd w$, respectively. These tuples are not
necessarily disjoint: variables with shared types can appear free in both $V$
and $Q$. The value $V$ is then broken down with parameters $\wtd
y$ and $k+1$; the latter serves to consistently generate propagators for the
trios in the breakdown of $V$, denoted $\V{}{\tilde y}{V\sigma}$ (see below).
The substitution $\sigma$  increments the index of session
names; it is applied to both $V$ and $Q$ before they are broken down.
By taking $\sigma = \nextn{u_i}$ we
distinguish two cases (see <Ref>):

* If name $u_i$ is linear (i.e., it has a session type) then its future
occurrences are renamed into $u_{i+1}$, and $\sigma = \subst{u_{i+1}}{u_i}$;

* Otherwise, if $u_i$ is shared, then $\sigma = \{\}$.

Note that if $u_i$ is linear then it appears either in $V$ or $Q$  and $\sigma$
affects only one of them. The last prefix   activates the
breakdown of  $Q$ with its corresponding context $\wtd w$.

In case $V  = y$, the same strategy applies; because $\V{k}{\tilde y}{y\sigma} = y$, we have:

\begin{align*}
\B{k}{\tilde x}{\bout{u_i}{y}Q} =
\binp{c_k}{\widetilde x} \bout{u_i}{y} \apropout{k+1}{\wtd w}
\Par \B{k+1}{\tilde w}{Q\sigma}
\end{align*}

Notice that variable $y$ is not propagated further if it does not appear free in $Q$.

* If $\tr(u_i)$ then $u_i$ is tail-recursive and then we have:

\begin{align*}
\B{k}{\tilde x}{\bout{u_i}{V}Q}=~~&\propinp{k}{\wtd x}
\abbout{\prop^u}{N_V} \Par
\B{k+1}{\tilde w}{Q} \\
\text{where:}~~
N_V =~~& \abs{\wtd z}
{\bbout{z_{\indT{S}}}{\V{}{\tilde y}{V}}}
\big(\apropout{k+1}{\wtd w} \Par
\recprov{u}{x}{\wtd z}
\big)
\end{align*}

The decomposition consists of a leading trio that mimics the output action
running in parallel with the breakdown of  $Q$. After receiving the context
$\widetilde x$, the leading trio sends an abstraction $N_V$ along $\prop^u$, which
performs several tasks. First, $N_V$ collects the sequence of names $\tilde u$;
then, it mimics the output action of $P$ along one of such names ($u_{\indT{S}}$) and
triggers the next trio, with context $\wtd w$; finally, it reinstates the
server on $\prop^u$ for the next trio that uses $u$.
Notice that indexing is not relevant in this case.

In case $V = y$, we have $\V{}{\tilde y}{y\sigma}=y$ and $\plen{y}=0$, hence:

\begin{align*}
\B{k}{\tilde x}{\bout{u_i}{y}Q} =
\propinp{k}{\wtd x} \abbout{\prop^u}
{\abs{\wtd z}{\bout{z_{\indT{S}}}{y}}
\big(\apropout{k+1}{\wtd w} \Par
\recprov{u}{x}{\wtd z}
\big) }
\Par \B{k+1}{\tilde w}{Q}
\end{align*}

To decompose a process $\binp{u_i}{y}Q$ we distinguish two cases, as before:
1  name $u_i$ is linear or shared or 2 tail-recursive.
In case 1, the breakdown   is defined as follows:

\begin{align*}
\B{k}{\tilde x}{\binp{u_i}{y}Q} =
\propinp{k}{\wtd x}\binp{u_i}{y} \apropout{k+1}{\wtd w}
\Par \B{k+1}{\tilde w}{Q\sigma}
\end{align*}

where $\wtd w = \fv{Q}$.
A leading trio mimics the input action and possibly extends the context with the
received variable $y$. The substitution $\sigma$ is defined as in the output

In case 2, when $u_i$ has tail-recursive session type $S$, the decomposition is as in the output case:

\begin{align*}
\B{k}{\tilde x}{\binp{u_i}{y}Q}=\propinp{k}{\wtd x}\abbout{\prop^u}
{\abs{\wtd z}{\binp{z_{\indT{S}}}{y}
\big(\apropout{k+1}{\wtd w} \Par
\recprov{u}{x}{\wtd z}
\big)}}
\Par \B{k+1}{\tilde w}{Q}
\end{align*}

For simplicity we consider the breakdown of applications of the form $\appl{V}{(\wtd r, u_i)}$, where
every $r_i \in \wtd r$ is such that $\tr(r_i)$ and only  $u_i$ is such that $\neg\tr(u_i)$.
The general case (involving different orders in names and multiple names with non-recursive types) is similar. We have:

\begin{align*}
\B{k}{\tilde x}{\appl{V}{(\widetilde r, u_i)}} = &
\propinp{k}{\widetilde x}\overbracket{\prop^{r_1}!\big\langle
\lambda \widetilde z_1. \prop^{r_2}!\langle\lambda
\widetilde z_2.\cdots.
\prop^{r_n}!\langle \lambda \widetilde z_n.}^{n = |\tilde r|}
\appl{\V{}{\tilde x}{V}}{(\widetilde z_1,\ldots,
\widetilde z_n, \widetilde m)} \rangle \,\rangle \big\rangle
\end{align*}

Let us first discuss how names in $(\wtd r, u_i)$ are decomposed using types.
Letting $|\tilde
r| = n$ and $i \in \{1,\ldots,n\}$, for each $r_i \in \widetilde r$ (with
$r_i:S_i$) we generate a sequence $\wtd
z_i=(z^i_1,\ldots,z^i_{\len{\Rts{}{s}{S_i}}})$ as in the output case.
We decompose name $u_i$ (with $u_i:C$) as $\wtd m = (u_i,\ldots,u_{i+\len{\Gt{C}}-1})$.

The decomposition first receives a context $\wtd x$ for value $V$: we break down $V$
with $\wtd x$ as a context since these variables need to be propagated to the
abstracted process.
Subsequently, an output on $\prop^{r_1}$ sends a value containing $n$ abstractions that occur nested
within output prefixes—this is similar to the mechanism for partial instantiation shown in 	<Ref>.
For each $j \in \{1,\ldots,n-1\}$, each abstraction
binds $\widetilde z_j$ and sends the next abstraction along $\prop^{r_{j+1}}$.
The innermost abstraction abstracts over $\widetilde z_n$ and encloses
the process $\appl{\V{}{\tilde x}{V}}{(\widetilde z_1,\ldots, \widetilde z_n,
\widetilde m)}$, which effectively mimics the  application.
This abstraction nesting binds all variables $\widetilde z_i$, the
decompositions of all tail-recursive names ($\wtd r$).

The breakdown of a value application of the form
$\appl{y}{(\widetilde r, u_i)}$ results into the following specific case:

\B{k}{\tilde x}{\appl{y}{(\widetilde r, u_i)}} =
\propinp{k}{\widetilde x}\overbracket{\prop^{r_1}!\big\langle
\lambda \widetilde z_1. \prop^{r_2}!\langle\lambda \widetilde z_2.\cdots.
\prop^{r_n}!\langle \lambda \widetilde z_n.}^{n = |\tilde r|}
\appl{y}{(\widetilde z_1,\ldots,
\widetilde z_n, \widetilde m)} \rangle \,\rangle \big\rangle

The decomposition of $\news{s:C}{P'}$ depends on $C$:

* If $\neg\tr(C)$  then
\begin{align*}
\B{k}{\tilde x}{\news{s:C}{P'}}
\news{\widetilde{s}:\Gt{C}}{\,\B{k}{\tilde x}
\end{align*}

By construction, $\widetilde x = \fv{P'}$. Similarly as in the decomposition of
$u_i$ into $\widetilde m$ discussed above, we use the type $C$ of $s$ to obtain
the tuple $\widetilde s$ of length $\len{\Gt{C}}$.
We initialize the index of
$s$ in $P'$ by applying the substitution $\sigma$. This substitution depends on
$C$: if it is a shared type then $\sigma = \subst{s_1}{s}$; otherwise, if $C$ is
a session type, then $\sigma = \subst{s_1\dual{s_1}}{s\dual{s}}$.

* Otherwise, if $\tr(C)$ then we have:

\begin{align*}
\B{k}{\tilde x}{\news{s:C}{P'}} =
\news{\widetilde{s}:\mathcal{R}(S)}
\news{c^s}
\recprov{s}{x}{\wtd s}
\Par
\news{c^{\bar{s}}}
\recprov{\bar{s}}{x}{\wtd{\dual s}}
\Par
\B{k}{\tilde x}{P'}
\end{align*}

We decompose $s$ into $\wtd{s} = (s_1,\ldots,s_{\len{\Gt{S}}})$ and
$\dual{s}$ into $\widetilde{\dual{s}} =
(\dual{s_1},\ldots,\dual{s_{\len{\Gt{S}}}})$. Notice
that as $\tr(C)$ we have
$C \equiv \trec{t}S$, therefore $\Gt{C} = \Rt{S}$.
The breakdown introduces two servers in parallel with the breakdown of
$P'$; they provide names for $s$ and $\dual{s}$ along $\prop^s$
and $\prop^{\dual{s}}$, respectively. The server on $\prop^s$ (resp.
$\prop^{\dual{s}}$) receives a value
and applies it to the sequence $\widetilde s$ (resp.
$\widetilde{\dual{s}}$). We restrict over $\widetilde s$ and propagators
$\prop^s$ and $\prop^{\dual{s}}$.

The breakdown of a process $Q \Par R$ is as follows:

\B{k}{\tilde x}{Q \Par R}
\propinp{k}{\widetilde x} \propout{k+1}{\wtd y}
\apropout{k+\degree+1}{\wtd w}   \Par
\B{k+1}{\tilde y}{Q} \Par \B{k+\degree+1}{\tilde w}{R}

A control trio triggers the breakdowns of $Q$ and $R$; it does not mimic any
action of the source process. The tuple $\wtd y \subseteq \wtd x$ (resp. $\wtd
w \subseteq \wtd x$) collects the free variables in  $Q$ (resp. $R$). To avoid
name conflicts, the trigger for the breakdown of  $R$ is $\dual
{c_{k+\degree+1}}$, with $\degree = \plen{Q}$.

To breakdown $\inact$, we define a degenerate trio with only one input prefix
that receives a context that by construction will always be empty (i.e., $\widetilde x = \epsilon$, cf. <Ref>):

\B{k}{\tilde x}{\inact}
\propinp{k}{}\inact

For simplicity, let us consider   values of the form
$V=\abs{(\widetilde y, z):\slhotup{(\widetilde S, C)}}P$,
where $\tr(y_i)$ holds for every $y_i \in \widetilde y$ and $\neg \tr(z)$, and
$\leadsto \in \{\lollipop, \sharedop\}$.
The general case is defined similarly.
We have:

\begin{align*}
\V{}{\tilde x}{\abs{(\widetilde y, z):\slhotup{(\widetilde S, C)}}P} & =
\abs{(\widetilde{y^1},\ldots,\widetilde{y^n}, \widetilde z):
\slhotup{(\widetilde{M})}}{N}  \quad \text{where:}
\\
\widetilde{M} & =\Gt{S_1},\ldots,\Gt{S_n}, \Gt{C}
\\
N & = \news{\widetilde \prop}
\news{\wtd \prop_r}
\prod_{i \in \len{\widetilde y}}
\recprov{y_i}{x}{\wtd y^i}
\Par \apropout{1}{\widetilde x}
\Par \B{1}{\tilde x}{P \subst{z_1}{z}}
\end{align*}

Every $y_i$ (with $y_i : S_i$) is
decomposed into $\widetilde y^i=(y_1,\ldots,y_{\len{\Gt{S_i}}})$. We use
$C$ to decompose $z$ into $\widetilde{z}$.
We abstract over $\wtd
y^1,\ldots,\wtd y^n, \wtd z$;
the body of the abstraction (i.e. $N$) is the composition of recursive names
propagators, the control trio, and the breakdown of $P$, with name index
initialized with the substitution $\subst{z_1}{z}$.
For every $y_i \in \widetilde y$ there is a server
$\recprov{y_i}{x}{\wtd y^i}$
as a subprocess in the
abstracted composition—the rationale for these servers is as in previous cases.
We restrict the
$\wtd \prop = (\prop_1,\ldots,\prop_{\plen{P}})$: this
enables us to type the value in a shared environment when $\leadsto =
\rightarrow$.
Also, we restrict special propagator names $\wtd \prop_r
= \bigcup_{r\in \tilde{v}}\prop^r$.

§.§ The Decomposition by Example

We illustrate the decompositions by means of several examples.

§.§.§ Decomposing Processes with Non-Recursive Names

Consider process $P = \news{u} (Q \Par R)$
whose body implements end-points of channel $u$ with
session type $S=\btinp{U}\btinp{\textsf{bool}}\tinact$,
with $U=\lhot{(\btinp{\textsf{bool}}\tinact)}$,

\begin{align*}
Q &= \binp{u}{x}
\overbrace{\binp{u}{y}
\news{s}\big( \appl{x}{\dual s} \Par \about{s}{y} \big)}^{Q'}
\\
R &= \bout{\dual u}{V}\bout{\dual u}{\textsf{true}}\inact
\\
V &= \abs{z}\binp{z}{b}\inact
\end{align*}

The process $P$ reduces as follows:

\begin{align*}
P &\red
\news{u}\left( \binp{u}{y}
\news{s}\big( \appl{V}{\dual s} \Par \about{s}{y} \big)
\Par
\bout{\dual u}{\textsf{true}}\inact\right)
\red
\news{s}\big( \appl{V}{\dual s} \Par \about{s}{\textsf{true}} \big)
\\
\red
\news{s}\big( \binp{\dual s}{b}\inact  \Par \about{s}{\textsf{true}} \big)
= P'
\end{align*}

By <Ref> we have that the decomposition of $P$ is as

\begin{align*}
\D{P}=
\news{\prop_1, \ldots, \prop_{10}}(\apropout{1}{} \Par
\B{1}{\epsilon}{P\sigma})
\end{align*}

$\sigma = \subst{u_1 \dual u_1}{u \dual u}$. We have:

\begin{align*}
\B{1}{\epsilon}{P\sigma} &=
\news{u_1,u_2} \propinp{1}{}\propout{2}{}\apropout{3}{}
\Par \B{2}{\epsilon}{Q\sigma} \Par \B{8}{\epsilon}{R\sigma}
\end{align*}

The breakdowns of sub-processes $Q$ and $R$ are
as follows:

\begin{align*}
\B{2}{\epsilon}{Q\sigma} &=
\propinp{2}{}\binp{u_1}{x}\apropout{3}{x}
\Par
\B{3}{\epsilon}{Q'\sigma'}
\\
\B{3}{x}{Q'\sigma'} &=
\propinp{3}{x}\binp{u_2}{y}\apropout{4}{x,y}
\Par
\B{4}{}{\news{s}\big( \appl{x}{\dual s} \Par \about{s}{y} \big)}
\\
\B{4}{x,y}{\news{s}\big( \appl{x}{\dual s} \Par \about{s}{y} \big)} &=
\news{s_1}
\big(
\propinp{4}{x,y}\propout{5}{x}\apropout{6}{y}
\Par
\propinp{5}{x}\appl{x}{\dual s_1}
\Par
\propinp{6}{y}\bout{s_1}{y}\apropout{7}{}
\Par \propinp{7}{}\inact
\big)
\\
\B{8}{\epsilon}{R\sigma} &=
\propinp{8}{}\bout{\dual u_1}{\V{}{\epsilon}{V}}\apropout{9}{}
\Par
\B{9}{\epsilon}{\bout{u_2}{\textsf{true}}\inact}
\\
\B{9}{\epsilon}{\bout{u_2}{\textsf{true}}\inact}
\propinp{9}{}\bout{\dual u_2}{\textsf{true}}\apropout{10}{} \Par
\propinp{10}{}\inact
\\
\V{}{\epsilon}{V} &= \abs{z_1}
\apropoutv{^V_1}{} \Par \propinpv{^V_1}{}
\binp{z_1}{b}\apropoutv{^V_2}{}
\Par \propinpv{^V_2}{}\inact)
\end{align*}

where $\sigma'= \subst{u_2 \dual u_2}{u \dual u}$.
By $\Gt{-}$ from <Ref> we decompose $S$ into
$M_1$ and $M_2$ given as follows:

\begin{align*}
\\
\end{align*}

Above we may notice that
We remark that $\D{P}$ accordingly
implements indexed names $u_1,u_2$ typed with

Let us inspect the reductions of $\D{P}$.
First, there are three synchronizations on $\prop_1,\prop_2$, and $\prop_8$:

\begin{align*}
\D{P} &\red
\news{\prop_2,\ldots,\prop_{10}}
\news{u_1,u_2}
\propout{2}{}\apropout{8}{}
\Par \B{2}{\epsilon}{Q\sigma} \Par \B{8}{\epsilon}{R\sigma}
\\
\news{\prop_3,\ldots, \prop_7,\prop_9, \prop_{10}}
\highlighta{\binp{u_1}{x}}\apropout{3}{x}
\Par
\B{3}{\epsilon}{Q'\sigma'}
\\
\qquad
\Par
\highlighta{\bout{\dual u_1}{\V{}{\epsilon}{V}}}\apropout{9}{}
\quad \Par
\B{9}{\epsilon}{\bout{u_2}{\textsf{true}}\inact}
= D^1
\end{align*}

After reductions on propagators, $D^1$ is able to mimic the original synchronization
on channel $u$ (highlighted above). It is followed by
two administrative reductions on $\prop_3$ and $\prop_9$:

\begin{align*}
D^1 &\red
\news{\prop_3,\ldots, \prop_7,\prop_9, \prop_{10}}
\apropout{3}{\V{}{\epsilon}{V}}
\Par
\propinp{3}{x}\binp{u_2}{y}\apropout{4}{x,y}
\Par
\B{4}{}{\news{s}\big( \appl{x}{\dual s} \Par \about{s}{y} \big)}
\Par
\\
& \qquad
\apropout{9}{}
\Par
\propinp{9}{}\bout{\dual u_2}{\textsf{true}}\apropout{10}{} \Par
\propinp{10}{}\inact
\\
& \red^2
\news{\prop_4,\ldots, \prop_7, \prop_{10}}
\highlighta{\binp{u_2}{y}}\apropout{4}{\V{}{\epsilon}{V},y}
\Par
\\
\quad
\news{s_1}
\big(
\propinp{4}{x,y}\propout{5}{x}\apropout{6}{y}
\Par
\propinp{5}{x}\appl{x}{\dual s_1}
\Par
\propinp{6}{y}\bout{s_1}{y}\apropout{7}{}
\Par \propinp{7}{}\inact
\big)
\Par
\\
& \qquad
\highlighta{\bout{\dual u_2}{\textsf{true}}}\apropout{10}{} \Par
\propinp{10}{}\inact = D^2
\end{align*}

Similarly, $D^2$ can mimic the next synchronization of
the original process on name $u_2$. Following up on that,
syncronization on $\prop_{10}$ takes place:

\begin{align*}
D^2 &\red^2
\news{\prop_4, \ldots, \prop_7}
\apropout{4}{\V{}{\epsilon}{V},\textsf{true}}
\Par
\\
\quad
\news{s_1}
\big(
\propinp{4}{x,y}\propout{5}{x}\apropout{6}{y}
\Par
\propinp{5}{x}\appl{x}{\dual s_1}
\Par
\propinp{6}{y}\bout{s_1}{y}\apropout{7}{}
\Par \propinp{7}{}\inact
\big) = D^3
\end{align*}

Now, we can see that the next three reductions on $\prop_4$,
$\prop_5$, and $\prop_6$
appropriately propagate values $\V{}{\epsilon}{V}$
and $\textsf{true}$ to the breakdown of sub-processes.
Subsequently, value $\V{}{\epsilon}{V}$ is applied to
name $\dual s_1$:

\begin{align*}
\news{\prop_5, \ldots, \prop_7}
\news{s_1}
\big(
\propout{5}{\V{}{\epsilon}{V}}\apropout{6}{\textsf{true}}
\Par
\propinp{5}{x}\appl{x}{\dual s_1}
\Par
\propinp{6}{y}\bout{s_1}{y}\apropout{7}{}
\Par \propinp{7}{}\inact
\big)
\\
\red^2
\news{\prop_7}
\news{s_1}
\big(
\appl{\V{}{\epsilon}{V}}{\dual s_1}
\Par \bout{s_1}{\textsf{true}}\apropout{7}{}
\Par \propinp{7}{}\inact
\big)
\\
\red
\news{\prop_7}
\news{s_1}
\apropoutv{^V_1}{} \Par \propinpv{^V_1}{}
\binp{s_1}{b}\apropoutv{^V_2}{}
\Par \propinpv{^V_2}{}\inact)
\Par
\bout{s_1}{\textsf{true}}\apropout{7}{}
\Par \propinp{7}{}\inact = D^4
\end{align*}

Finally, after syncronization on $\prop^V_1$
we reach the process $D^5$ that is clearly able to simulate $P'$, and its internal communication on the channel $s$:

\begin{align*}
D^4 \red
\news{\prop_7}
\news{s_1}
\binp{s_1}{b}\apropoutv{^V_2}{}
\Par \propinpv{^V_2}{}\inact)
\Par
\bout{s_1}{\textsf{true}}\apropout{7}{}
\Par \propinp{7}{}\inact = D^5
\end{align*}

$\hfill \lhd$

[Breaking Down Name-Passing]

Consider the following process $P$, in which a channel $m$ is passed, through which a boolean value is sent back:

\begin{align*}
P = \news{u}(\bout{u}{\namepass{m}} \abinp{\dual m}{b}  \Par
\binp{\dual u}{\namepass{x}} \about{x}{\textsf{true}} )
\end{align*}

After expanding the syntactic sugar of name-passing, we get a process $P = \news{u} (Q \Par R)$, where

\begin{align*}
& Q = \bout{u}{V}
\binp{\dual m}{y}\news{s}{(\appl{y}{s} \Par
\about{\dual s}{\abs{b}{\inact}}
)} & V = \abs{z}\binp{z}{x}(\appl{x}{m})\\
& R = \binp{\dual u}{y}\news{s}{(\appl{y}{s} \Par
\about{\dual s}{W})} & W =\abs{x}{\about{x}{W'}} \text{ with }W' = \abs{z}\binp{z}{x}(\appl{x}{\textsf{true})}
\end{align*}

Note that to mimic the name-passing synchronization, we require exactly four reduction steps:

\begin{align}
\label{ex:reduction-chain}
&P \red^4  \map { \abinp{\dual m}{b}  \Par
\about{m}{\textsf{true}}  } \red^4 \inact
\end{align}

We will now investigate the decomposition of $P$ and its reduction chain.
First, we use <Ref> to compute $\plen{Q} = 6$, and similarly, $\plen{R} = 5$.
Therefore, $\plen{{P}} = 12$.
Following <Ref>, we see that $\sigma = \subst{m_1\dual{m_1}}{m\dual m}$, which we silently apply.
Taking $k=1$, the breakdown of $P$ and its subprocesses is shown in <Ref>.

\begin{align*}
\D{P} & = \news{\prop_1,\ldots, \prop_{12}} \Big(
\apropout{1}{}   \Par
\news{u_1}\big( \propinp{1}{} \propout{2}{} \apropout{8}{}   \Par
\B{2}{\epsilon}{Q} \Par \B{8}{\epsilon}{R} \big) \Big)
\\
\B{2}{\epsilon}{Q} & = \propinp{2}{} \bout{u_1}{\V{}{\epsilon}{V}}
\apropout{3}{}  \Par \propinp{3}{} \binp{\dual{m_1}}{y} \apropout{4}{y}
\Par
\\
&   \qquad \news{s_1}(\propinp{4}{y}\propout{5}{y}\apropout{6}{}  \Par
\propinp{5}{y}(\appl{y}{s_1}) \Par
\propinp{6}{}\bout{\dual {s_1}}{\V{}{\epsilon}{\abs{b}{\inact}}}
\apropout{7}{}  \Par \apropinp{7}{}  )
\\
\B{8}{\epsilon}{R} & =
\propinp{8}{}\binp{\dual {u_1}}{y}\apropout{9}{y}  \Par
\\
& \qquad \news{s_1}\big( \propinp{9}{y}\propout{10}{y}\apropout{11}{}
\Par \propinp{10}{y}(\appl{y}{s_1}) \Par
\propinp{11}{}\bout{\dual{s_1}}{\V{}{\epsilon}{W}}\apropout{12}{}  \Par
\apropinp{12}{}  \big)
\\
\V{}{\epsilon}{V} & =
\abs{z_1}{
\news{\prop^V_1, \prop^V_2}
(\apropoutv{^V_1}{}  \Par
\propinpv{^V_1}{} \binp{z_1}{x} \apropoutv{^V_2}{x}   \Par
\propinpv{^V_2}{x} (\appl{x}{m_1}) )}
\\
\V{}{\epsilon}{\abs{b}{\inact}} & =
\abs{b_1}{
\news{\prop^b_1}
(\apropoutv{^b_1}{}  \Par
\apropinpv{^b_1}{})}
\\
\V{}{\epsilon}{W} & =
\abs{x_1}{
\news{\prop^W_{1}, \prop^W_{2}}
( \apropoutv{^W_1}{}
\Par \propinpv{^W_1}{} \bout{x_1}{\V{}{\epsilon}{W'}}
\apropoutv{^W_2}{}   \Par \apropinpv{^W_2}{}  )}
\\
\V{}{\epsilon}{W'} &  = \abs{z_1}
{ \news{\prop^{W'}_{1}, \prop^{W'}_{2}}
\Par \propinpv{^{W'}_{1}}{} \binp{z_1}{x}
\apropoutv{^{W'}_{2}}{x}  \Par
\propinpv{^{W'}_{2}}{x} (\appl{x}{\textsf{true}}) )}
\end{align*}

The decomposition on processes discussed in ex:bdnp.

In t:examp we have omitted substitutions that have no effect and trailing $\inact$s.
The first interesting action appears after synchronizations on $\prop_1$, $\prop_2$, and $\prop_{8}$.
At that point, the process will be ready to mimic the first action that is performed by $P $, i.e., $u_1$ will send $\V{}{\epsilon}{V}$, the breakdown of $V$, from the breakdown of $Q$ to the breakdown of $R$.
Next, $\prop_{9}$ and $\prop_{10}$ will synchronize, and $\V{}{\epsilon}{V}$ is passed further along, until $s_1$ is ready to be applied to it in the breakdown of $R$.
At this point, we know that ${P} \red^{7} \news{\wtd \prop}P'$, where $\widetilde \prop = (\prop_3,\ldots,\prop_{12})$, and

\begin{align*}
P' = &~
\apropout{3}{} \Par \propinp{3}{} \binp{ \dual{m_1}}{y}
\apropout{4}{y}
\\
& \Par
\news{s_1}(\propinp{4}{y}\propout{5}{y}\apropout{6}{} \Par
\propinp{5}{y}\appl{y}{s_1} \Par
\propinp{6}{}\bout{\dual {s_1}}
\Par \apropinp{7}{})\\
& \Par
\news{s_1}\big(  \appl{\V{}{\epsilon}{V}}{s_1} \Par
\bout{\dual{s_1}}{\V{}{\epsilon}{W}}\apropout{12}{} \Par
\apropinp{12}{} \big)
\end{align*}

After $s_1$ is applied, the trio guarded by $c_3$ will be activated, where
$z_1$ has been substituted by $s_1$. Then $\dual{s_1}$ and $s_1$ will
synchronize, and the breakdown of $W$ is passed along. Then $c_4$ and $c_{19}$
synchronize, and now $m_1$ is ready to be applied to $\V{}{\epsilon}{W}$,
which was the input for $c_4$ in the breakdown of $V$. After this application,
$\prop_3$ and $\prop{^W_1}$ can synchronize with their duals, and we know that
$\news{\widetilde c}P' \red^8 \news{\widetilde{c}'}P''$, where
$\widetilde{c}'=(\prop_4,\ldots,\prop_{7},\prop{^{W'}_2})$, and

\begin{align*}
P'' = & ~\binp{\dual{m_1}}{y} \apropout{4}{y}
\Par
\bout{m_1}{\V{}{\epsilon}{W'}} \apropoutv{^{W'}_2}{}  \Par
\apropinpv{^{W'}_2}{}
\\
& \Par \news{s_1}(\propinp{4}{y}\propout{5}{y}\apropout{6}{} \Par
\propinp{5}{y}\appl{y}{s_1} \Par
\propinp{6}{}\bout{\dual {s_1}}{\V{}{\epsilon}{\abs{b}{\inact}}}
\apropout{7}{}
\Par \apropinp{7}{} )
\end{align*}

Remarkably, $P''$ is standing by to mimic the encoded exchange of value . Indeed, the decomposition of the four-step reduced process in (<ref>) will reduce in three steps to a process that is equal (up to $\scong_\alpha$) to the process we obtained here. This strongly suggests  a tight operational correspondence between a process and its decomposition, which we will explore in <Ref>.  $\lhd$

§.§.§ Decomposing Processes with Recursive Names

Next, we illustrate the decomposition of processes involving names with
tail-recursive types. Recall process $R_1$, which  we used in ss:key to
motivate the need for recursive propagators:

\begin{align*}
\end{align*}

Two following examples illustrate the low-level workings of the propagation
mechanism of the decomposition
in fig:rec-subfig2.
The first example illustrates how the
propagation of recursive names works in the case of
input and output actions on names with recursive types (the “first part” of
$R_1$). The second example shows how an application where a value is applied to
a tuple of names with recursive names is broken down (the “second part” of

[Decomposing Processes with Recursive Names (I)]

Let $P = \binp{r}{x}\bout{r}{x}P'$ be a process where $r$ has type
$S=\trec{t}{\btinp{\mathsf{int}}\btout{\mathsf{\mathsf{int}}}}{\vart{t}}$ and $r
\in \fn{P'}$.
By def:decomp we have:

\begin{align*}
\D{P} = \news{\wtd \prop}\news{\prop^r}
\big(
\apropout{1}{} \Par  \B{1}{\epsilon}{P} \Par
\recprov{r}{x}{(r_1,r_2)}
\big)
\end{align*}

where $\wtd \prop = (\prop_1, \ldots, \prop_{\len{P}})$.
The control trio in the parallel composition provides a
decomposition of $r$ on name $\prop^r$, which is shared.
The decomposition $\B{1}{\epsilon}{P}$ is
defined as follows:

\begin{align*}
\B{1}{\epsilon}{P} & =
\apropout{1}{} \Par  \propinp{1}{} \aproprout{r}{N_1}  \Par
\propinp{2}{y} \aproprout{r}{N_2}
\Par \B{3}{\epsilon}{P'}
\big)
\\
N_1 & = \abs{(z_1, z_2)}\binp{z_1}{x}
\recprov{r}{x}{(z_1, z_2)}
\\
N_2 & = \abs{(z_1, z_2)}\bout{z_2}{x}\propout{3}{}
\recprov{r}{x}{(z_1,z_2)}
\end{align*}

Each trio in $\B{1}{\epsilon}{P}$ that mimics some action on $r$
requests the sequence $\tilde r$ from the server on $\prop^r$. We can see that
this request is realized by a higher-order communication: trios send
abstractions ($N_1$ and $N_2$) to the server; these abstractions contain
further actions of trios and it will be applied to the sequence $\tilde r$.
Hence, the formal arguments for these values are meant to correspond to
$\tilde r$.

After two reductions (the trio activation on $\prop_1$
and the communication on $\prop^r$), we have:

\begin{align*}
\D{P} \red^2
\news{\prop_2, \ldots, \prop_{\plen{P}}}\,
\binp{r_1}{x}\propout{2}{x}
\recprov{r}{x}{(r_1,r_2)}
\Par
\propinp{2}{y} \aproprout{r}{N_2}
\Par \B{3}{\epsilon}{P'} = P_1
\end{align*}

By synchronizing with the top-level server on $\prop^r$, the bound names
in $N_1$ are instantiated with $r_1,r_2$.
Now, the first trio in $P_1$ is able
to mimic the action on $r_1$ that is followed by the activation of the next
trio on $\prop_2$. Then, the server on $\prop^r$ gets reinstantiated making names $r_1,r_2$
available for future trios.
The break down of the output action follows the same pattern.

To define $\B{1}{\epsilon}{P}$ in a compositional way, names
$(r_1,r_2)$ should be provided to its first trio; they cannot be known
beforehand. To this end, we introduce a new  control trio that will hold these

\begin{align*}
\proprinp{r}{b}{\appl{b}{(r_1, r_2)}}
\end{align*}

where the shared name $\prop^r$ provides a decomposition of the
(recursive) name $r$. The intention is that each name with a recursive type $r$
will get its own dedicated propagator channel $\prop^r$. Since there is only one
recursive name in $P$, its decomposition will be of the following form:

\begin{align*}
\D{P} = \news{\tilde \prop}\news{\prop^r}
\big( \proprinp{r}{b}{\appl{b}{(r_1,r_2)}} \Par
\propout{1}{}\inact \Par  \B{1}{\epsilon}{P} \big)
\end{align*}

The new control trio can be seen as a server that provides names: each trio that
mimics some action on $r$ should request the sequence $\tilde r$ from the server
on $\prop^r$. This request will be realized by a higher-order communication:
trios should send an abstraction to the server; such an abstraction will contain
further actions of a trio and it will be applied to the sequence $\tilde r$.
Following this idea, we may refine the definition of $\D{P}$ by expanding

\begin{align*}
\D{P} = \news{\tilde \prop}\news{\prop^r}
\big( \proprinp{r}{b}{\appl{b}{(r_1,r_2)}} \Par
\propout{1}{}\inact \Par  \propinp{1}{} \proprout{r}{N_1} \inact \Par
\propinp{2}{y} \proprout{r}{N_2} \inact
\Par \B{3}{\epsilon}{P'}
\big)
\end{align*}

The trios involving names with recursive types have now a different shape. After
being triggered by a previous trio, rather than immediately mimicking an action,
they will send an abstraction to the server available on $\prop^r$. The
abstractions $N_1$ and $N_2$ are defined as follows:

\begin{align*}
N_1 = \abs{(z_1, z_2)}\binp{z_1}{x}\propout{2}{x}\proprinp{r}{b}{
\appl{b}{(z_1,z_2)}}
\quad
N_2 = \abs{(z_1, z_2)}\bout{z_2}{x}\propout{3}{}
\proprinp{r}{b}{\appl{b}{(z_1,z_2)}}
\end{align*}

Hence, the formal arguments for these values are meant to correspond to $\tilde
r$. The server on name $\prop^r$ will appropriately instantiate these names.
Notice that all names in $\tilde r$ are propagated, even if the abstractions
only use some of them. For instance, $N_1$ only uses $r_1$, whereas $N_2$
uses $r_2$. After simulating an action on $r_i$ and activating the next
trio, these values reinstate the server on $\prop^r$ for the benefit of
future trios mimicking actions on $r$.

[Decomposing Processes with Recursive Names (II)]

$S = \trec{\vart{t}}\btinp{\mathsf{int}}\btout{\mathsf{int}} \vart{t}$
$T = \trec{\vart{t}}\btinp{\mathsf{bool}}\btout{\mathsf{bool}} \vart{t}$, and
define $Q = \appl{V}{(u,v)}$ as a process where $u : S$ and $v : T$, where $V$
is some value of type $\shot{(S, T)}$.
By def:decomp,
the  decomposition of $Q$ is as in the previous example, except that now there
are two servers, one for $u$ and one for $v$:

\begin{align*}
\D{Q} & = \news{\prop_1 \tilde \prop}\news{\prop^u \prop^v} \big(
\recprov{u}{x}{(u_1, u_2)} \Par
\recprov{v}{x}{(v_1, v_2)} \Par
\apropout{1}{} \Par
\B{1}{\epsilon}{Q}
\big)
\\
\B{1}{\epsilon}{Q} & = \propinp{1}{}\abbout{\prop^u}{\abs{(x_1,x_2)}{
\aproprout{v}{\abs{(y_1,y_2)}{\appl{\V{}{\epsilon}{V}}{(x_1,x_2,y_1,y_2)}}}
\end{align*}

with $\tilde \prop = (\prop_2,\ldots,\prop_{\plen{Q}})$. Process $Q$
is broken down in such a way that it communicates with both servers to collect
$\tilde u$ and $\tilde v$.
To  this end, $\B{1}{\epsilon}{Q}$ is a process in which abstractions are
nested using output prefixes and whose innermost process is an application.
After successive communications with multiple servers this innermost
application will have collected all names in $\tilde u$ and $\tilde v$.

Observe that we use two nested outputs, one for each name with recursive types
in $Q$.
We now look at the reductions of $\D{Q}$ to analyze how the communication of nested abstractions allows us to collect all name sequences needed. After the first reduction along $\prop_1$ we have:

\begin{align*}
\D{Q} \red & \news{\tilde \prop}\news{\prop^u \prop^v} \big(
\recprov{u}{x}{(u_1, u_2)} \Par
\recprov{v}{x}{(v_1, v_2)} \Par
\\
& \qquad \qquad \qquad  \abbout{\prop^u}{\abs{(x_1,x_2)}{
\aproprout{v}{\abs{(y_1,y_2)}{\appl{\V{}{\epsilon}{V}}{(x_1,x_2,y_1,y_2)}}}}} \big)
= R^1
\end{align*}

From $R^1$ we have a synchronization along  name $\prop^u$:

\begin{align*}
R^1 \red & \news{\tilde \prop}\news{\prop^u \prop^v} \big(
\appl{(\abs{(x_1,x_2)}{
\aproprout{v}{\abs{(y_1,y_2)}{\appl{\V{}{\epsilon}{V}}{(x_1,x_2,y_1,y_2)}}}})}{(u_1,u_2)} \Par
\recprov{v}{x}{(v_1, v_2)}
\big)
= R^2
\end{align*}

Upon receiving the value, the server applies it to $(u_1,u_2)$, thus
obtaining the following process:

\begin{align*}
R^2 \red & \news{\tilde \prop}\news{\prop^u \prop^v} \big(
\aproprout{v}{\abs{(y_1,y_2)}{\appl{\V{}{\epsilon}{V}}{(u_1,u_2},y_1,y_2)}} \Par
\recprov{v}{x}{(v_1, v_2)}
\big)  = R^3
\end{align*}

Up to here, we have partially  instantiated name variables of a value
with the sequence $\tilde u$. Next, the first trio in $R^3$ can communicate with the server on name $\prop^v$:

\begin{align*}
R^3 \red & \news{\tilde \prop}\news{\prop^u \prop^v} \big( \appl{\abs{(y_1,y_2)}{\appl{\V{2}{\epsilon}{V}}{(u_1,u_2,y_1,y_2)}}}{(v_1,v_2)}\big)
\\
\red & \news{\tilde \prop}\news{\prop^u \prop^v}
\big( {\appl{\V{}{\epsilon}{V}}{(u_1,u_2,v_1,v_2)}}\big)
\end{align*}

This completes the instantiation of name variables with appropriate sequences of names with recursive types.
At this point, $\D{Q}$ can proceed to mimic the application in $Q$.

[Breakdown of Recursion Encoding]
We recall process $\map{P}$ from <Ref>:

\begin{align*}
\map{P} &= \binp{a}{m}\bout{a}{m} \news{s}
{(\appl{V}{(a,s)} \Par \about{\dual s}{V})}  \\
V & = \abs{(x_a,y_1)}\binp{y_1}{z_x}\binp{x_a}{m}
\bout{x_a}{m}\news{s}
{(\appl{z_x}{(x_a,s)} \Par \bout{\dual s}{z_x}\inact)}
\end{align*}

Here, bound name $s$ is typed with $S$, from <Ref>, defined as:

\begin{align*}
S = \trec{t}{\btinp{\shot{(\btinp{\mathsf{str}}\btout{\mathsf{str}}\tinact,
\vart{t})}}\tinact}
\end{align*}

We now analyze $\D{\map{P}}$ and its reduction chain.
By <Ref>, we have $\plen{\map P} = 7$.
Then, we choose $k=1$ and observe that $\sigma =
\subst{a_1\dual{a_1}}{a\dual a}$. Following <Ref>, we get:

\begin{align*}
&\D{\map P} = \news{\prop_1,\ldots,\prop_7}
\news{\prop^a}(
\recprov{a}{x}{(a_1, a_2)}
\Par
\apropout{1}{}  \Par \B{1}{\epsilon}{\map P\sigma})\\
&\B{1}{\epsilon}{\map P} =
\propinp{1}{} \about{\prop^a}{\abs{(z_1,z_2)}\binp{z_1}
\recprov{a}{x}{(z_1, z_2)}
\\
&\qquad \qquad
\Par
\propinp{2}{m}
\about{\prop^a}{\abs{(z_1,z_2)}\bout{z_2}
\recprov{a}{x}{(z_1, z_2)}
\\
&\qquad \qquad \Par \news{s_1}\big(\propinp{3}{} \propout{4} {}
\apropout{5}{}
\Par
\propinp{4}{}\about{\dual{\prop^a}}
\\
&\qquad \qquad \qquad \quad
\Par \propinp{5}{}\bout{\dual s_1}{\V{6}{\epsilon}{V}}\apropout{7}{}
\Par \apropinp{7}{}\big)
\end{align*}

In accordance with ex:ntrsts, the type of $s_1$ in the decomposed process is

\begin{align*}
M = \trec{t}{\btinpt{{{{\shot{(\btinpt{\mathsf{str}},
\btoutt{\mathsf{str}},\vart{t})}}}}}}.
\end{align*}

The decomposition relies twice on $\V{}{\epsilon}{V}$, the breakdown of value $V$, which we give below.
For this, we observe that $V$
is an abstraction of a process $Q$ with $\len Q = 7$.
We also $\alpha$-convert the process abstracted in $\V{}{\epsilon}{V}$
renaming bound propagators $\prop_1,\ldots,\prop_7$ to
$\prop^V_1,\ldots,\prop^V_7$ to avoid name clashes.

\begin{align*}
\V{}{\epsilon}{V} & = \abs{(x_{a_1},x_{a_2},y_1)}
{	\news{\prop{^V_1},\ldots,\prop{^V_7}} \big (
\apropoutv{^V_1}{}  \Par \B{1}{\epsilon}{Q}
\subst{\prop{^V_1},\ldots,\prop{^V_7}}
{\prop{_1},\ldots,\prop{_7}}} \Par
\recprovx{x_{a}}{x}{(x_{a_1},x_{a_2})}
\big)
\\
\B{1}{\epsilon}{Q} & = \propinpv{_1}{}\binp{y_1}{z_x}
\apropout{2}{z_x}
\\
& \quad
\Par
\propinp{2}{z_x}\about{\prop^a}
\recprov{a}{x}{(z_1, z_2)}
\\
& \quad \Par
\propinp{3}{z_x}\about{\prop^a}
{\abs{(z_1,z_2)}{\bout{z_2}{m}} \propout{4}{z_x}
\recprov{a}{x}{(z_1, z_2)}
\\
& \quad \Par \news{s_1}\big(\propinp{4}{x_z} \propout{5}{z_x}
\apropout{6}{z_x} \Par
\\
&\quad \qquad  \qquad \propinp{5}{z_x}
\about{\prop^a}{\abs{(z_1,z_2)}\appl{z_x}{(z_1,z_2,s_1)}}
\Par \propinp{6}{z_x} \bout{\dual{s_1}}{z_x}
\apropout{7}{} \Par \apropinp{7}{}\big)
\end{align*}

We follow the reduction chain on $\D{\map P}$ until it is ready to mimic the first action with channel $a$, which is an input. First, $\prop_1$ will synchronize, after which $\prop^a$ sends the abstraction to which then $(a_1,a_2)$ is applied. We obtain $\D{\map P} \red^3 \news{c_2,\ldots, c_7,c^a}P'$, where

\begin{align*}
& P' = \binp{a_1}
\recprov{a}{x}{(a_1, a_2)}
\\
&\qquad \qquad \Par
\propinp{2}{m}
\about{\prop^a}{\abs{(z_1,z_2)}\bout{z_2}
\recprov{a}{x}{(z_1, z_2)}
\\
&\qquad \qquad \Par \news{s_1}\big(\propinp{3}{} \propout{4} {}
\propout{5}{}
\Par
\propinp{4}{}\about{\dual{\prop^a}}
{\abs{(z_1,z_2)}\appl{\V{}{\epsilon}{V}}{(z_1,z_2,s_1)}} \Par
\\
&\qquad \qquad \qquad \qquad  \propinp{5}{}\bout{\dual s_1}
\Par \apropinp{7}{}\big)
\end{align*}

Note that this process is awaiting an input on channel $a_1$, after which
$c_2$ can synchronize with its dual. At that point, $c^a$ is ready to receive
another abstraction that mimics an input on $a_1$. This strongly suggests a
tight operational correspondence between a process $P$ and its decomposition
in the case where $P$ performs higher-order recursion.
$\hfill \lhd$

§.§ Static Correctness

Having presented and illustrated our decomposition, we may now state its technical results.
Given an environment $\Delta = \Delta_1, \Delta_2$, below we write $\Delta_1 \circ \Delta_2$ to indicate the split of $\Delta$ into a $\Delta_1$ containing non-recursive names and a $\Delta_2$ containing recursive names.

We extend the decomposition function $\Gt{-}$ to typing
environments in the obvious way.
We rely on the following notation.
Given a tuple of names $\widetilde{s} = s_1, \ldots, s_n$ and a tuple of
(session) types $\widetilde{S} = S_1, \ldots, S_n$ of the same length, we write
$\widetilde{s}:\widetilde{S}$ to denote a list of typing assignments $s_1:S_1,
\ldots, s_n:S_n$.

Let $\Gamma$, $\Lambda$, and $\Delta$ be typing environments.
We define $\Gt{\Gamma}$, $\Gt{\Lambda}$, and $\Gt{\Delta}$ inductively as follows:

\begin{align*}
\Gt{\Delta \cat u_i:S} &= \Gt{\Delta},(u_i,\ldots,u_{i+\len{\Gt{S}}-1}) : \Gt{S} \\
\Gt{\Gamma \cat u_i:\chtype{U}} &= \Gt{\Gamma} \cat u_i : \Gt{\chtype{U}} \\
\Gt{\Gamma \cat x:U} &= \Gt{\Gamma} \cat x:\Gt{U} \\
\Gt{\Lambda \cat x:U} &= \Gt{\Lambda} \cat x:\Gt{U} \\
\Gt{\emptyset} &=  \emptyset
\end{align*}

Let $P$ be an indexed process and $V$ be a value.

* If $\Gamma;\Lambda;\Delta \circ  \envR \proves P \hastype \Proc$ then
$\Gt{\Gamma_1}\cat \envPropR;\es;\Gt{\Delta} \cat \Theta \proves \B{k}{\tilde x}{P} \hastype \Proc$,

* $k > 0$

* $\widetilde r = \text{dom}(\envR)$

* $\envPropR = \prod_{r \in \tilde r} c^r:\chtype{\lhot{\Rts{}{s}{\envR(r )}}}$

* $\widetilde x = \fv{P}$

* $\Gamma_1=\Gamma \setminus \widetilde x$

* $\text{dom}(\Theta) =
\{\prop_k,\ldots,\prop_{k+\plen{P}-1}\} \cup
\{\dual{\prop_{k+1}},\ldots,\dual{\prop_{k+\plen{P}-1}}\}$

* $\Theta(\prop_k)=
\btinpt{U_1, \ldots, U_n} $, where $(\Gt{\Gamma}\cat\Gt{\Lambda})(\widetilde x) = (x_1 : U_1, \ldots, x_n : U_n)$

* $\balan{\Theta}$

* If $\Gamma;\Lambda;\Delta \circ  \envR \proves V \hastype
\lhot{\wtd T}$ then
$\Gt{\Gamma} \cat \envPropR; \Gt{\Lambda};\Gt{\Delta} \proves
\V{k}{\tilde x}{V} \hastype \lhot{\Gt{\wtd T}}$,

* $\wtd x = \fv{V}$

* $\envPropR = \prod_{r \in \tilde r} c^r:\chtype{\lhot{\Rts{}{s}{\envR(r)}}}$

By mutual induction on the structure of $P$ and $V$.
See Appendix <ref> for details.

Using the above lemma we can prove our static correctness result, which explains how our decomposition induces minimal session types.

[Static Correctness]thmdecompcore

Let $P$ be a closed process (i.e. $\fv{P} = \emptyset$) with $\widetilde u = \fn{P}$.
If $\Gamma;\es;\Delta \circ  \envR \proves P \hastype \Proc$,
then $\Gt{\Gamma
\sigma};\es;\Gt{\Delta\sigma}  \cat \Gt{\envR \sigma} \proves \D{P} \hastype
\Proc$, where $\sigma = \subst{\mathsf{init}(\widetilde u)}{\widetilde u}$.

Directly from the definitions, using t:typecore.
See Appendix <ref> for details.

§ DYNAMIC CORRECTNESS

In this section, we establish the dynamic correctness of our decomposition, stated in terms of a typed behavioral equivalence.
More specifically, we would like to show that any typed process $P$ is equivalent to its decomposition $\D{P}$.
But how do we even state it formally?
Both $P$ and $\D{P}$ are typed $\HO$ processes (as any minimally typed process is also an $\HO$ process), so we can consider compare them as $\HO$ terms inside the $\HO$ type system.
The conventional notion of typed equivalence for $\HO$ processes is contextual equivalence, which is given a local characterization in terms of higher-order bisimulations [18].
In our case, however, contextual equivalence is not the right choice: contextual equivalence applies to processes of the same type, whereas the process $P$ and its decomposition $\D{P}$ have different types and typing contexts.
Instead of using contextual equivalence, we generalize the notion of higher-order bisimilarity to a notion that we call MST bisimilarity, which relates processes of (potentially) different types.

This section is organized as follows.
In sec:hobisim we recall the notion of higher-order bisimulation, used for characterizing behavioral equivalence in , and discuss its limitations for our purposes.
We use higher-order bisimulation as a basis to give a formal definition of MST bisimulation in sec:mstbisim, which we will use as a notion of behavioral equivalence for comparing $P$ and $\D{P}$.
In order to show that our decomposition is correct, in sec:relationS we exhibit a bisimulation relation $\relS$ which relates a process and its decomposition, containing a number of intermediate pairs, working from a motivating example in sec:motexample.
Finally, in sec:opcorrproof we show that $\relS$ is indeed an MST bisimulation.

§.§ Behavioral Equivalence in and its Limitations

Let us begin by recalling the notion of bisimulation, defined in [18] to characterize contextual equivalence of processes.

A typed relation $\Re$ is an bisimulation if
for all $\horelm{\Gamma_1;\Lambda_1;\Delta_1}{P_1}{\ \Re \ }

* Whenever
{\hby{\news{\widetilde{m_1}} \bactout{n}{V_1}}}
then there exist
$Q_2$, $\Delta'_2$, and $\Lambda'_2$ such that
where, for a fresh $t$,

\[
\Gamma_1; \Lambda_1; \Delta''_1 \proves
{\newsp{\widetilde{m_1}}{P_2 \Par \htrigger{t}{V_1}}}
\ \Re\
\Gamma_2; \Lambda_2; \Delta''_2\proves
{\newsp{\widetilde{m_2}}{Q_2 \Par \htrigger{t}{V_2}}}
\]

* Whenever
{\Lambda_1'; \Delta_1'}{P_2}$, with
$\ell$ not an output, then there exist
$Q_2$, $\Lambda_2'$, and $\Delta'_2$ such that
$\horelm{\Gamma_1;\Lambda_1';\Delta_1'}{P_2}{\ \Re \ }

* The symmetric cases of 1, 2.

The largest such bisimulation is called bisimilarity, denoted by $\hob$.

There are two points worth highlighting in this definition.
Firstly, the labeled transition system $\hby{\ell}$ used in the definition of $\hob$ is what is called the refined transition system, different from the standard labeled transition system for the higher-order $\pi$-calculus.
The idea behind the refined transition system is that we want to disallow arbitrary inputs $P \hby{x(V)} P'$; having to consider such transitions in the definition of bisimilarity is undesirable, because it involves input of an arbitrary (higher-order) value $V$, making the definition very much non-local and ensuring that the bisimulations are very large.
As it turns out, due to the typed nature of the system, it suffices to consider inputs of the processes of a very particular kind—characteristic values, defined based on the type.

Secondly, because the inputs are restricted in the refined LTS, there is some price to pay in the handling of the outputs.
If an output action ${P_1}\hby{\news{\widetilde{m_1}} \bactout{n}{V_1}}{P_2}$ is matched by an output action ${Q_1}\Hby{\news{\widetilde{m_2}} \bactout{n}{V_2}}{Q_2}$, then we need to ensure that that the output processes $V_1$ and $V_2$ are somehow related.
We have to ensure this in the output clause, because on the receiving end transitions inputing values $V_1$ or $V_2$ might not even be considered.
To that extent, we package the values $V_1$ or $V_2$ in trigger processes (denoted $\htrigger{t}{V_1}$ and $\htrigger{t}{V_2}$), which are defined based on the typing.
We then make them part of the processes that are considered at the “next step” of the bisimulation.

This notion of bisimilarity works for processes of the same type.
For our case, we need to compare processes of different, but related types.
To that extent we make several changes to the definition above.
Firstly, during the decomposition a single name $x$ in a source process is decomposed into a sequence of names $x_1, \dots, x_k$ in the target process.
So in the definition of MST bisimilarity we match an action on a name $x$ with an action on an indexed name $x_i$.
Secondly, such discrepancy between names might arise in input and output values.
This also needs to be considered as part of the definition.
For this, we need to accommodate the difference between characteristic values and trigger processes for MST and HO.
In the next subsection we work out the details sketched above.

§.§ MST Bisimilarity

In this section we define a generalized version of bisimilarity allowing for comparing MST and process terms.
Our goal is to define MST bisimilarity (denoted $\mstb$), a typed behavioral equivalence, which we give in <Ref>.
To define $\mstb$, we require some auxiliary definitions, in particular:

* A refined LTS on typed processes (<Ref>);

* A relation $\valuesrelate$ on values (<Ref>) and on names (<Ref>);

* A revised notion of trigger processes  (<Ref>).

Refined LTS and characteristic values.
The idea behind defining the refined LTS is to restrict the input of arbitrary processes (values) and make the transition system image-finite (modulo names).

The refined LTS for is defined in [18] in three layers.
First comes the untyped LTS $P \by{\ell} P'$, which describes reductions of untyped processes in the usual style of the LTS semantics for $\pi$-calculus.
Secondly, there is a notion  of the environmental LTS $(\Gamma_1; \Lambda_1; \Delta_1) \by{\ell} (\Gamma_2; \Lambda_2; \Delta_2)$, which describes reductions of typing environments.
This LTS describes the way a typing context can evolve in accordance with its session types.
On top of these layers there are notions of  refined environmental LTS and  refined LTS for processes.
The former restricts the environmental LTS to inputs on characteristic values, as we discussed in <Ref>.
Finally, the refined LTS for processes restricts the untyped LTS to those actions which are supported by the refined environmental LTS.

We follow this approach for defining the refined LTS for MST processes.
Both the untyped LTS for processes and the environmental LTS for MST processes coincides with the same LTSs for (or, to be more precise, with its restriction to minimal session types).
It remains, then, to define the refined environmental LTS for MST processes, with the idea that the
refined LTS restricts inputs to the inputs on minimal characteristic values and minimal trigger values.

Given a value type $\slhot{C}$ and fresh (indexed) name $\tni$, the minimal trigger
value  on $\tni$ of type $\slhot{\Gt{C}}$ is defined as the abstraction

$$\abs{\wtd x}\binp{\tni}{y}\appl{y}{\wtd x}$$
where $\wtd x =

Let $u$ be a name and $i > 0$.
We define  $\mapcharm{-}{u}_i$ and $\omapcharm{-}$ on types as follows.

\[
\begin{array}{rclcrcl}
\mapcharm{\btinp{L} S}{u}_i
\binp{u_i}{x} (\bout{\tni}{\namepass{u_{i+1},
\ldots,u_{i+\len{\Gt{S}}}}}
\inact \Par
\mapcharm{L}{x}_i)
&\qquad &
\omapcharm{S}  & \defeq &  \wtd s ~~ (\len{\wtd s} =
\len{\Gt{S}}, \wtd s \textrm{ fresh})
\\
\mapcharm{\btout{L} S}{u}_i
\bout{u_i}{\omapcharm{L}}
\bout{\tni}{\namepass{u_{i+1}, \ldots,u_{i+\len{\Gt{S}}}}} \inact
\omapcharm{\chtype{L}} &\defeq& a_1 ~~ (a_1 \textrm{ fresh})
\\
\mapcharm{\tinact}{u}_i
& \defeq &
\inact
\omapcharm{\shot{C}} &\defeq&  \abs{(x_1,\ldots,x_{\len{\Gt{C}}})}{\mapcharm{C}{x}_1}
\\

\mapcharm{ \trec{t}{S} }{u}_i &\defeq& \mapcharm{S \subst{\tinact}{\vart{t}} }{u}_i

\omapcharm{\lhot{C}} & \defeq &  \abs{(x_1,\ldots,x_{\len{\Gt{C}}})}{\mapcharm{C}{x}_1}
\\
\mapcharm{\chtype{L}}{u}_i
\bout{u_1}{\omapcharm{L}} \bout{\tni}{\namepass{u_1}} \inact
\\
\mapcharm{\shot{C}}{x}_i
\appl{x}{\omapcharm{C}}
\\
\mapcharm{\lhot{C}}{x}_i
&\defeq &
\appl{x}{\omapcharm{C}}
\end{array}
\]

where $\tni$ is a fresh (indexed) name.
In this definition we use name-passing constructs, as outlined in <Ref>.

The refined LTS, denoted $\mhby{~\ell~}$, is defined
on top of the environmental LTS using the following rules:

(Γ_1; Λ_1; Δ_1) ℓ (Γ_2; Λ_2; Δ_2)
ℓ≠ nV

(Γ_1; Λ_1; Δ_1)  ℓ  (Γ_2; Λ_2; Δ_2)

(Γ_1; Λ_1; Δ_1) nV (Γ_2; Λ_2; Δ_2)
(V L)
∨(V  xy (yx))
with $\tni$ fresh

(Γ_1; Λ_1; Δ_1) nV (Γ_2; Λ_2; Δ_2)

where $\abs{{\wtd x}}{\binp{\tni}{y} (\appl{y}{{\wtd x}})}$ is
a minimal trigger value of type $\Gt{C}$ (<Ref>).
Finally, the refined LTS for MST processes is just a combination of the untyped LTS with the refined environmental LTS:

The environmental refined LTS extends to the typed refined LTS on processes.
We write $\horelm{\Gamma_1;\Lambda_1;\Delta_1}{P_1}{\mhby{~\ell~}}{\Lambda'_1;\Delta'_1}{P_2}$

* $P_1 \by{\ell} P_2$, and

* $(\Gamma_1; \Lambda_1; \Delta_1) \mhby{~\ell~} (\Gamma_2; \Lambda_2; \Delta_2)$.

We write $\Mhby{\ell}$ for the weak version of the transition $\mhby{\ell}$.
Notice that while the untyped LTS and the non-refined environmental LTS coincide
with that of , the refinement that we impose on the environmental LTS is
different from its counterpart. Specifically in Rule MRcv we take
special care to use minimal
characteristic processes $\omapcharm{-}$, instead of general characteristic process $\omapchar{-}$
as defined in [18].

Relating trigger and characteristic values.
As we mentioned earlier, the notion of bisimulation that we consider requires matching transitions of the source term with the transitions of the target MST term.
However, the two transitions might differ on the inputs of characteristic values.
We accommodate for that difference by establishing a relation between the trigger and characteristic values of and MST.

We define the relation $\valuesrelate$ between processes and indexed processes inductively as:

\frac{
\len{\tilde x} = \len{\Gt{C}}
\abs{x:C}{\binp{t}{y}\appl{y}{x}}
\valuesrelate
\abs{\tilde x: \Gt{C}}\binp{\tni}{y}\appl{y}{\tilde x}
\qquad
\frac{}{
\omapchar{\slhot{C}} \valuesrelate \omapcharm{\slhot{C}}{}}

where $\abs{{\wtd x}:\Gt{C}}{\binp{\tni}{y} (\appl{y}{{\wtd x}})}$ is
a minimal trigger value of type $\slhot{\Gt{C}}$  (<Ref>)
and  $\omapchar{-}$ denotes the characteristic values
defined in [18].
We write $\abs{x:C}{\binp{\tni}{y}\appl{y}{x}}$ to mean that value
$\abs{x}{\binp{\tni}{y}\appl{y}{x}}$ is of type $ \slhot{C}$.

Trigger processes and MST bisimilarity.
Before we give the definition of MST bisimilarity, we establish the following notations:

Given a name $n$, we write $\iname{n}$ to either denote
$n$ or any indexed name $n_i$, with $i > 0$.

Given a value $V$, a trigger process for a fresh (indexed) name
$\tni$ is defined as:

\[
\htrigger{\tni}{V} \defeq \binp{\tni}{\wtd{x}}(V\ \wtd{x})
\]

where $\len{\wtd x} = \len{\wtd C}$ for $V : \slhot{\wtd C}$.

If $\Gamma; \Lambda; \Delta \proves V \hastype \slhot{\wtd C}$,
then $\Gamma; \Lambda; \Delta, \tni : \btinpt{\wtd{C}} \proves \htrigger{\tni}{V} \hastype \Proc$.

Finally, we are ready to formally define  bisimilarity.

A typed relation $\Re$ is an MST bisimulation if
for all $\horelm{\Gamma_1;\Lambda_1;\Delta_1}{P_1}{\ \Re \ }

* Whenever
{\hby{\news{\widetilde{m_1}} \bactout{n}{V_1}}}
then there exist
$Q_2$, $\Delta'_2$, and $\Lambda'_2$ such that
where, for a fresh $t$,

\[
\Gamma_1; \Lambda_1; \Delta''_1 \proves
{\newsp{\widetilde{m_1}}{P_2 \Par \htrigger{t}{V_1}}}
\ \Re\
\Gamma_2; \Lambda_2; \Delta''_2\proves
{\newsp{\widetilde{m_2}}{Q_2 \Par \htrigger{\iname t}{V_2}}}
\]

* Whenever $\horelm{\Gamma_1; \Lambda_1; \Delta_1}{P_1}
then there exist  $Q_2$, $\Lambda_2'$, and $\Delta_2'$ such that
{\Lambda'_2, \Delta_2'}{Q_2}$
$V_1 \valuesrelate V_2$
$\horelm{\Gamma_1;\Lambda_1';\Delta_1'}{P_2}{\ \Re \ }

* The symmetric cases of 1 and 2.

The largest such bisimulation is called MST bisimilarity, denoted by $\mstb$.

In all clauses,
we use the refined LTS (<Ref>) and rely on notation
$\iname{n}$ (<Ref>). In the output clause, we use the
triggers (<Ref>). In the input clause, we use the
relation $\valuesrelate$ on values (<Ref>).

We discuss differences between MST bisimilarity and higher-order bisimilarity as defined in [18].
First, an action in $P_1$ must be matched by an action on an indexed name in $Q_1$, and refined LTS actions in $P_1$ are matched by minimal refined
LTS actions in $Q_1$  (<Ref>). As a consequence of the latter,
in the input case the observed values are not identical but related by $\valuesrelate$ (<Ref>).
In other words, whenever $P_1$
receives a trigger or a characteristic value, then $Q_1$ should receive their minimal
counterparts (<Ref> and <Ref>). Further, as names could be
indexed on the right-hand side, the typing environments could differ for open processes, so the MST bisimilarity assumes different typing environments on both sides.

§.§ The Bisimulation Relation

Our goal is to complement our static correctness result (<Ref>) by
proving the following statement about the  decomposition of processes (<Ref>):

Let $P$ be an process such that $\Gamma;\Delta;\Lambda \proves P \hastype \Proc$.
We have

$$\horelm{\Gamma;\Lambda;\Delta}{P}{\ \mstb \ }

To show that $P$ and $\D{P}$ are MST-bisimilar, we provide a concrete bisimulation relation $\relS$  that contains $(P,\D{P})$.
Defining $\relS$ to be just the set of such pairs is, however, not going to work; instead, the relation $\relS$ should also contain pairs corresponding to “intermediate” states in which the process and its decomposition may get “desynchronized”.
Before we give the concrete definition of $\relS$ we look at an example, illustrating the need for such intermediate pairs.

§.§.§ A Motivating Example

Consider the following process:

\begin{align*}
P_1 = \binp{u}{t}\binp{v}{x}
\news{s : S}(\bout{u}{x}\inact \Par \appl{t}{s}  \Par \bout{\dual s}{x}\inact)
\Par \bout{\dual v}{V}\inact
\end{align*}

where $u : \btinp{\chtype{U_t}}\btout{U_{V}}\tinact$ and $v:S$ with
$S = {\btinpt{U_V}}$, $U_t = \shot{S}$, and
$U_V$ is some shared value type, i.e. $U_V = \shot{S_V}$, for some
session type $S_V$.
Further, $V$ is some value, such that $V = \abs{y:S_V}R$.

Thus, $P_1$ is typed using the typing of its constituents:

$\es; \es; \dual{v} : \dual{S}
\fCenter\proves \bout{\dual v}{V}\inact \hastype \Proc$
$\es; \es; u : \btinp{\chtype{U_t}}\btout{U_{V}}\tinact, v:S \fCenter\proves
\binp{u}{t}\binp{v}{x}
\news{s : S}(\bout{u}{x}\inact \Par \appl{t}{s}  \Par \bout{\dual s}{x}\inact)
\hastype \Proc$
$\es; \es; u: \btinp{\chtype{U_t}}\btout{U_V}\tinact, v:S, \dual{v} :
\dual{S}
\fCenter\proves P_1 \hastype \Proc$

The decomposition of $P_1$ is as follows:

\begin{align*}
\D{P_1} & = \news{\wtd{\prop}} \left( \apropout{1}{} \Par
\B{1}{\epsilon}{P_1}\right) \\
& = \news{\wtd{\prop}} \big( \apropout{1}{} \Par
\apropinp{1}{}. \apropout{2}{}.\apropout{11}{}  \\
& \quad\qquad \Par \apropinp{2}{}.\binp{u_1}{t}\apropout{3}{t}
\Par \apropinp{3}{t}.\binp{v_1}{x}\apropout{4}{t,x} \\
& \quad\qquad\qquad \Par \news{s_1}
\apropout{5}{x}.\apropout{6}{t, x} \Par
\propinp{5}{x}\bout{u_2}{x}\apropout{6}{} \Par \apropinp{6}{} \Par
\\
& \qquad\qquad\qquad
\Par \propinp{7}{t,x}\propout{8}{t}\apropout{9}{x} \Par
\apropinp{8}{t}.\appl{t}{s_1}
\Par \apropinp{9}{x}.\bout{\dual{s_1}}{x}\apropout{10}{} \Par
\apropinp{10}{}) \\
& \quad\qquad \Par \apropinp{11}{}.\bout{\dual{v_1}}{\V{12}{\epsilon}{V}}
\apropout{12}{} \Par \apropinp{12}{}
\big),
\end{align*}

where $\wtd \prop = c_1,\ldots,c_{12}$.
Let us write $Q_1$ for the decomposition $\D{P_1}$.

[shorten >=0.5pt,node distance=1.60cm,on grid,auto]
[state] (p_1)  $P_1$;
[state] (p_2) [right=2.5cm  of p_1] $P_2$;
[state] (p_3) [right=2.5cm of p_2] $P_3$;
[state, fill=blue!20](p_4) [above right=3.0 cm of p_3] $P_4$;
[state](p_5) [below right=3 cm of p_3] $P_5$;
[state, fill=blue!20](p_6) [right=3.0 cm of p_4] $P_6$;
[state](p_7) [right=3.0 cm of p_5] $P_7$;
[state, fill=blue!20] (p_8) [below right=3.0 cm of p_6]$P_8$;

(p_1) edge node $\abinp{u}{\textcolor{blue}{V_c}}$ (p_2)
(p_2) edge node $\tau$ (p_3)

(p_3) edge node $\about{u}{V}$ (p_4)
(p_3) edge node $\tau$ (p_5)
(p_4) edge node $\tau$ (p_6)
(p_5) edge node $\tau$ (p_7)
(p_5) edge node $\about{u}{V}$ (p_6)
(p_7) edge node $\about{u}{V}$ (p_8)
(p_6) edge node $\tau$ (p_8)

[state] (q_1) [below=6cm of p_1, xshift=0cm] $Q_1$;
[state] (q1_1) [below=cm  of q_1, xshift=cm] $Q'_1$;
[state] (q1_2) [below=cm  of q1_1, xshift=cm] $Q''_1$;

[state] (q_2) [right=2.5cm  of q_1] $Q_2$;
[state] (q2_1) [below=cm  of q_2, xshift=cm] $Q'_2$;
[state] (q2_2) [below=cm  of q2_1, xshift=cm] $Q''_2$;

[state] (q_3) [right=2.5cm of q_2] $Q_3$;
[state] (q3_1) [below=cm  of q_3, xshift=cm] $Q'_3$;
[state] (q3_2) [below=cm  of q3_1, xshift=cm] $Q''_3$;

[state, fill=blue!20](q_4) [above right=5.5 cm of q3_2, xshift=-2cm] $Q_4$;
[state, fill=blue!20] (q4_1) [below=cm  of q_4, xshift=cm] $Q'_4$;
[state, fill=blue!20] (q4_2) [below=cm  of q4_1, xshift=cm] $Q''_4$;

[state](q_5) [below right=5.5 cm of q3_2, xshift=-2cm] $Q_5$;
[state] (q5_1) [above=cm  of q_5, xshift=cm] $Q'_5$;
[state] (q5_2) [above=cm  of q5_1, xshift=cm] $Q''_5$;

[state, fill=blue!20](q_6) [right=3 cm of q_4] $Q_6$;
[state, fill=blue!20] (q6_1) [below=cm  of q_6, xshift=cm] $Q'_6$;
[state, fill=blue!20] (q6_2) [below=cm  of q6_1, xshift=cm] $Q''_6$;

[state](q_7) [right=3 cm of q_5] $Q_7$;
[state] (q7_1) [above=cm  of q_7, xshift=cm] $Q'_7$;
[state] (q7_2) [above=cm  of q7_1, xshift=cm] $Q''_7$;

[state, fill=blue!20] (q_8) [right=7.5cm of q3_2]$Q_8$;

(q1_2) edge [pos=0.9, left] node $\abinp{u_1}{\textcolor{blue}{V^m_c}}$ (q_2)
(q_1) edge node $\tau$ (q1_1)
(q1_1) edge node $\tau$ (q1_2)

(q2_2) edge [pos=0.8, left] node $\tau$ (q_3)
(q_2) edge node $\tau$ (q2_1)
(q2_1) edge node $\tau$ (q2_2)

(q3_2) edge [pos=0.8, left] node $\about{u_2}{\V{}{}{V}}$ (q_4)
(q_3) edge node $\tau$ (q3_1)
(q3_1) edge node $\tau$ (q3_2)

(q3_2) edge node $\tau$ (q_5)
(q4_2) edge node $\tau$ (q_6)
(q_4) edge node $\tau$ (q4_1)
(q4_1) edge node $\tau$ (q4_2)

(q5_2) edge node $\tau$ (q_7)
(q_5) edge node $\tau$ (q5_1)
(q5_1) edge node $\tau$ (q5_2)

(q5_2) edge [pos=0.3, left] node $\about{u_2}{\V{}{}{V}}$ (q_6)
(q7_2) edge [pos=0.8, left] node $\about{u_2}{\V{}{}{V}}$ (q_8)
(q_7) edge node $\tau$ (q7_1)
(q7_1) edge node $\tau$ (q7_2)

(q6_2) edge node $\tau$ (q_8)
(q_6) edge node $\tau$ (q6_1)
(q6_1) edge node $\tau$ (q6_2)

(p_1) edge [line width=mm, -, dotted] node  (q_1)
(p_2) edge [line width=mm, -, dotted] node  (q_2)
(p_3) edge [line width=mm, -, dotted] node  (q_3)
(p_4) edge [line width=mm, -, dotted] node  (q_4)
(p_5) edge [line width=mm, -, dotted] node  (q_5)
(p_6) edge [line width=mm, -, dotted] node  (q_6)
(p_7) edge [line width=mm, -, dotted] node  (q_7)
(p_8) edge [line width=mm, -, dotted] node  (q_8)

Transitions of $P_1$ and $Q_1 = \D{P_1}$ in sec:motexample.
The blue nodes represent processes that contain characteristic values
and trigger processes induced by the bisimilarites defined in [18].

We wish to show $P_1 ~\mstb~ Q_1$. For this, we must exhibit a relation $\mathcal{S}$ included  in $\mstb$ such that $(P_1,  \D{P_1}) \in  \relS$.
To illustrate the notions required to define the additional pairs, we consider possible transitions of $P_1$ and $Q_1$, denoted schematically in <Ref>.
First, let us consider a possible (refined) transition of $P_1$, an input on $u$ of a characteristic value:

\begin{align*}
P_1 \by{\bactinp{u}{\textcolor{blue}{V_C}}}
\binp{v}{x}
\news{s : S}(\bout{u}{x}\inact \Par \appl{\textcolor{blue}{V_C}}{s}
\Par \bout{\dual s}{x}\inact)
\Par \bout{\dual v}{V}\inact = P_2
\end{align*}

where $\textcolor{blue}{V_C} = \omapchar{U_t} =
\abs{y:S} \binp{y}{x'}(\bout{}{}\inact \Par \appl{x'}{s'})$ is the  characteristic value of $U_t$.[We use blue to denote characteristic values and trigger processes that do no occur in the original process, but  which are induced by the bisimilarities defined in [18].]
Process $Q_1$ can weakly match this input action on the indexed name $u_1$.