Undecidability of Asynchronous Session Subtyping
Mario Bravetti
University of Bologna, Department of Computer Science and Engineering / FOCUS INRIA
Mura Anteo Zamboni 7, 40126 Bologna, Italy

arXiv:1611.05026v3 [cs.PL] 19 Jul 2017

Marco Carbone
Department of Computer Science, IT University of Copenhagen
Rued Langgaards Vej 7, 2300 Copenhagen, Denmark

Gianluigi Zavattaro
University of Bologna, Department of Computer Science and Engineering / FOCUS INRIA
Mura Anteo Zamboni 7, 40126 Bologna, Italy

Abstract
Session types are used to describe communication protocols in distributed systems and, as usual in type theories, session subtyping characterizes substitutability of the communicating processes. We investigate the (un)decidability
of subtyping for session types in asynchronously communicating systems. We
first devise a core undecidable subtyping relation that is obtained by imposing
limitations on the structure of types. Then, as a consequence of this initial
undecidability result, we show that (differently from what stated or conjectured
in the literature) the three notions of asynchronous subtyping defined so far for
session types are all undecidable. Namely, we consider the asynchronous session
subtyping by Mostrous and Yoshida [1] for binary sessions, the relation by Chen
et al. [2] for binary sessions under the assumption that every message emitted is
eventually consumed, and the one by Mostrous et al. [3] for multiparty session
types. Finally, by showing that two fragments of the core subtyping relation
are decidable, we evince that further restrictions on the structure of types make
our core subtyping relation decidable.
Keywords: Session Types, Subtyping, Undecidability, Queue Machines

1. Introduction
Session types [4, 5] are types for describing the behaviour of communicating
systems, and can be used as specifications of distributed protocols to be checked
against implementations. Such check, done by means of a typing system, guarantees that communications at any endpoint of the implemented system are
always matched by the corresponding intended partner. As a consequence, it is

Preprint submitted to Journal of LATEX Templates

February 11, 2018

ensured that communication errors, e.g., deadlock, will never occur. This approach provides a compositional way of checking the correctness of distributed
systems.
As an example, consider a simple on-line shop: clients can buy a list of items
by following the protocol expressed by the session type
Sclient = µt. ⊕ {add to cart : t , pay : end}
indicating a recursive behaviour, according to which the client decides whether
to add an item and keep interacting with the store, or to pay and conclude the
session. For the sake of simplicity we consider session types where (the type of)
communicated data is abstracted away.
We call output selection 1 the construct ⊕{l1 : T1 , . . . , ln : Tn }. It is used to
denote a point of choice in the communication protocol: each choice has a label
li and a continuation Ti . In communication protocols, when there is a point of
choice, there is usually a peer that internally takes the decision and the other
involved peers receive communication of the selected branch. Output selection
is used to describe the behaviour of the peer that takes the decision: indeed, in
our example it is the client that decides when to stop adding items to the cart
and then move to the payment.
The symmetric behaviour of the shopping service is represented by the complementary session type
Sservice = µt.&{add to cart : t , pay : end}.
We call input branching 2 the construct &{l1 : T1 , . . . , ln : Tn }. It is used to
describe the behaviour of a peer that receives communication of the selection
done by some other peers. In the example, indeed, the service receives from the
client the decision about the selection.
When composing systems whose interaction protocols have been specified
with session types, it is significant to consider variants of their specifications
that still preserve safety properties. In the above example of the on-line shop,
the client can be safely replaced by another one with session type
Tclient = ⊕{add to cart : ⊕{pay : end}}
indicating that only one item is added to the shopping cart before paying. But
also the shopping service could be safely replaced by another one offering also
the remove from cart functionality:
Tservice = µt.&{add to cart : t , remove from cart : t , pay : end}.
1 In session type terminology [4, 5], this construct is usually simply called selection; we call
it output selection because we consider a simplified syntax for session types in which there is
no specific separate construct for sending one output. Anyway, such an output type could be
seen as an output selection with only one choice.
2 In session type terminology this construct is simply called branching. We call it input
branching for symmetric reasons w.r.t. those discusses in the previous footnote.

2

Formally, subtyping relations have been defined for session types to precisely
capture this safe replacement notion.
Gay and Hole [6] are the first ones who studied subtyping for session types
in a context where protocols involve only two peers (i.e. are binary) and communication is synchronous. Later, Mostrous et al. [3] extended this notion to
multiparty session types with asynchronous communication. Both articles propose an algorithm for checking subtying, but the one proposed by Mostrous et
al. [3], differently from what stated therein, is not always terminating in the
sense that there are cases in which it diverges and never gives an answer. An
example of divergent execution is discussed in the Remark paragraph of §4.4.
Later work by Mostrous and Yoshida [1], Mostrous [7] and Chen et al. [2]
addresses subtyping in variants of an asynchronous setting for binary sessions.
In particular Chen et al. [2] focus on binary sessions in which messages sent
by a partner are guaranteed to be eventually received. Such articles conjecture
that an algorithm for checking asynchronous session subtyping exists, although,
in his PhD thesis, Mostrous [7] expresses a few doubts about the decidability of asynchronous subtyping (pp. 178-180), because of the need for infinite
simulations.
In this work, we prove that the subtyping relations defined by Mostrous
and Yoshida [1], Chen et al. [2], and Mostrous et al. [3] are undecidable. We
proceed by identifying a core asynchronous subtyping relation and show it is
undecidable: all other undecidability results are obtained by reduction from
this initial relation.
The core relation, denoted by <<, is named asynchronous single-choice relation. Such a relation is obtained by first defining (following the approach by
Mostrous and Yoshida [1]) a standard asynchronous subtyping ≤ and then reduce it by imposing additional constraints: T and S are in single-choice relation,
written T << S, if T ≤ S, all output selections in T have a single choice (output
selections are covariant 3 , thus S is allowed have output selections with multiple choices), all input branchings in S have a single choice (input branchings
are contravariant 4 , thus T is allowed to have input branchings with multiple
choices), and additionally both T and S do not have consecutive infinite output
selections. This last condition is added to encompass the subtyping defined by
Chen et al. [2] that, as discussed above, requires all messages to be eventually
received: in fact, if consecutive infinite output selections are not allowed, it is
not possible to indefinitely delay inputs.
For instance, considering the simple on-line shop example, we have:
Tclient <6 < Sclient
because Sclient has consecutive infinite output selections; and
Tservice <6 < Sservice
3 Covariant

means that the bigger type has more choices than the smaller type.
means that the bigger type has less choices than the smaller type.

4 Contravariant

3

because Sservice has input branchings with more than one choice.
If we consider a different behavior for the shopping service, where each input
branching has single choice
0
Sservice
= &{add to cart : &{pay : end}}.
0
we have, instead, Tservice << Sservice
.
The proof of undecidability of << is by reduction from the acceptance problem in queue machines. Queue machines are a Turing powerful computational
model composed of a finite control that consumes and introduces symbols in a
queue, i.e. a First-In First-Out (FIFO) structure. The input to a queue machine is given by a sequence of symbols, ended by a special delimiter $, that
is initially present in the queue. The finite control is defined by a finite set
of states (one of which being the initial state) and a transition function that
given the current state and the consumed symbol, i.e. the one taken from the
beginning of the queue, returns the next state and a sequence of symbols to be
added at the end of the queue. The input is accepted by the queue machine
whenever queue is emptied. As an example, one can define a queue machine
able to accept the strings an bn , with n ≥ 0, by considering a finite control with
the following states:

• an initial state that expects to consume one among two possible symbols:
an a and then move to the second state, or the delimiter $ (thus accepting);
• the second state that cyclically consumes each of the remaining symbols
a, re-introducing them at the end of the queue, and then moves to the
third state by consuming the first b;
• the third state that cyclically consumes each of the remaining symbols
b, re-introducing them at the end of the queue, and then returns to the
initial state by consuming the $ and re-enqueueing it.
Even if queue machines are similar to pushdown-automata, they are strictly
more powerful. For instance, it is trivial to extend the above queue machine
with an additional state in order to accept strings an bn cn , with n ≥ 0. Queue
machines are not only more expressive than pushdown-automata, but they are
Turing complete. Intuitively, this follows from the fact that by using a queue
instead of a stack, it is possible to access any symbol in the structure without
losing the symbols in front. In fact, it is sufficient to re-introduce such symbols
at the end of the queue, as done in the above example e.g. with the symbols a
and b in the second and the third state, respectively. This mechanism makes it
possible to simulate the tape of a Turing machine by using the queue.
Being Turing powerful, acceptance of a string is undecidable for queue machines. We show (Theorem 3.1) that given a queue machine and an input string,
it is alway possible to define two session types T and S such that T << S if and
only if the given input string is not accepted by the considered queue machine.
From this we conclude that the << relation is also undecidable.

4

≤Om
≤s
≤o
≤m
−→

standard binary [1]
orphan-message-free [2]
multiparty [3]
reduces to

≤O s

≤J o

≤Y
<J <U
undecidable
decidable

<<sin

<<sout

Figure 1: Lattice of the asynchronous subtyping relations considered in this paper.

This core undecidability result allows us to prove by reduction the undecidability of ≤ as well as other more complex relations including the three
asynchronous subtypings in the literature discussed above. Namely, we prove
the undecidability of the following subtypings: ≤s that includes also send and
receive actions and corresponds with (a fragment of) the subtyping defined by
Mostrous and Yoshida [1], ≤o that disallows orphan messages and coincides with
the subtyping defined by Chen et al. [2], and ≤m that deals with multiparty
session types and corresponds with the subtyping introduced by Mostrous et
al. [3].
As an additional result, we show that further restrictions on the branching/selection structure of types make our core subtyping relation << decidable.
In fact, by imposing any of two possible restrictions on << — namely, in both
subtype and supertype all input branchings (or all output selections) have one
choice only — the obtained relation turns out to be decidable. We thus define
the subtyping relations <<sin (both types are single-choice on inputs) and <<sout
(both types are single-choice on outputs) by considering the two above restrictions on the asynchronous single-choice relation << and prove that both <<sin
and <<sout are decidable. As a matter of fact, we prove decidability for larger
relations w.r.t. <<sin and <<sout where we do not impose the constraint about
no consecutive infinite outputs.
Figure 1 depicts the relations discussed in this paper as a lattice representing
a 1 −→ 2 order. 1 −→ 2 means that it is possible to algorithmically reduce
the problem of deciding the relation 1 into the problem of deciding 2 . As
discussed above, ≤s , ≤o and ≤m are taken from the literature, while ≤, <<,
<<sin and <<sout are defined in this paper to characterize as tightly as possible

5

the boundary between decidability and undecidability for asynchronous session
subtyping relations. Obviously, when a relation is undecidable all relations
above it (it reduces to) are also undecidable, while when a relation turns out to
be decidable all relations below it (that reduce to it) are decidable as well.
Structure of the paper. In §2 we introduce a core language of session types
with only branching/selection and recursion, and define for it the asynchronous
subtyping relation ≤. In §3 we restrict subtyping to << and we show that such
relation is undecidable. In §4, we discuss how our undecidability result allows
us to prove the undecidability of other asynchronous subtypings, namely ≤, ≤s ,
≤o , ≤m , and subtyping for communicating finite state machines (CFSMs). In
§5 we discuss the two decidable relations <<sin and <<sout , obtained as further
restrictions of <<. Finally, in §6 we comment the related literature and draw
some concluding remarks.
2. Asynchronous Subtyping
In this section, we give a definition of a core session type language and define
the asynchronous subtyping relation ≤ following the approach by Mostrous and
Yoshida [1].
2.1. Session Types
We start by presenting a very simple session type language (with only
branching/selection and recursion) which is sufficient to prove our undecibility result.
Definition 2.1 (Session types). Given a set of labels L, ranged over by l, the
syntax of binary session types is given by the following grammar:
T

::=

⊕{li : Ti }i∈I | &{li : Ti }i∈I | µt.T | t | end

In our session type language we simply consider session termination end, recursive definitions µt.T , with t being the recursion variable, output selection
⊕{li : Ti }i∈I and input branching &{li : Ti }i∈I . Each possible choice is labeled
by a label li , taken from the set of labels L, followed by a session continuation
Ti . Labels in a branching/selection are pairwise distinct.
2.2. Subtyping
We consider a notion of asynchronous subtyping corresponding to the subtyping relation by Mostrous and Yoshida [1] applied to our language. In particular we formalize the property of output anticipation (which, as we will see,
characterizes asynchronous subtyping) by using the notion of input context as
in Chen et al. [2] and Mostrous and Yoshida [1]. In order to define subtyping,
we first need to introduce n-unfolding and input contexts.
The n-unfolding function unfolds nested recursive definitions to depth n.

6

Definition 2.2 (n-unfolding).
unfold0 (T ) = T
unfold1 (⊕{li : Ti }i∈I ) = ⊕{li : unfold1 (Ti )}i∈I
unfold1 (&{li : Ti }i∈I ) = &{li : unfold1 (Ti )}i∈I
unfold1 (µt.T ) = T {µt.T /t}
unfold1 (t) = t
unfold1 (end) = end
unfoldn (T ) = unfold1 (unfoldn−1 (T ))
Definition 2.3 (Input Context). An input context A is a session type with
multiple holes defined by the following syntax:
A ::= [ ]n

|

&{li : Ai }i∈I

An input context A is well-formed whenever all its holes [ ]n , with n ∈ N+ , are
consistently enumerated, i.e. there exists m ≥ 1 such that A includes one and
only one [ ]n for each n ≤ m. Given a well-formed input context A with holes
indexed over {1, . . . , m} and types T1 ,. . . , Tk , we use A[Tk ]k∈{1,...,m} to denote
the type obtained by filling each hole k in A with the corresponding term Tk .
From now on, whenever using contexts we will assume them to be wellformed.
For example, consider the input context
A = &{l1 : []1 , l2 : []2 }
we have:

A[⊕{l : Ti }]i∈{1,2} = & l1 : ⊕{l : T1 }, l2 : ⊕{l : T2 }
We are finally ready to define our notion of subtyping.
Definition 2.4 (Asynchronous Subtyping, ≤). R is a subtyping relation
whenever (T, S) ∈ R implies that:
1. if T = end then ∃n ≥ 0 such that unfoldn (S) = end;
2. if T = ⊕{li : Ti }i∈I then ∃n ≥ 0, A such that
• unfoldn (S) = A[⊕{lj : Skj }j∈Jk ]k∈{1,...,m}

for some Jk ,

• ∀k ∈ {1, . . . , m}.I ⊆ Jk and
• ∀i ∈ I, (Ti , A[Ski ]k∈{1,...,m} ) ∈ R;
3. if T = &{li : Ti }i∈I then ∃n ≥ 0 such that unfoldn (S) = &{lj : Sj }j∈J ,
J ⊆ I and ∀j ∈ J.(Tj , Sj ) ∈ R;
4. if T = µt.T 0 then (T 0 {T /t}, S) ∈ R.
We say that T is a subtype of S, written T ≤ S, if there is a subtyping relation
R such that (T, S) ∈ R.

7

An important characteristic of asynchronous subtyping (formalized by rule 2.
above) is the following one. In a subtype output selections can be anticipated so
to bring them before the input branchings that in the supertype occur in front
of them. For example the type

S = & lbut1 : ⊕{lcoffee : T1 }, lbut2 : ⊕{lcoffee : T2 }
has the following subtype

T = ⊕ lcoffee : &{lbut1 : T1 , lbut2 : T2 }
where the output selection with label lcoffee is anticipated w.r.t. the input
branching with labels lbut1 and lbut2 . That is, since in the supertype the input
branching with labels lbut1 and lbut2 occurs in front of the output selection with
label lcoffee (which is present in all its input branches), such an output selection
can be anticipated so to bring it before the lbut1 /lbut2 input branching.
It is, thus, immediate to verify that, according to Definition 2.4, we have
T ≤ S. In particular, in rule 2. the well-formed input context considered to express the output l anticipation is A = &{lbut1 : []1 , lbut2 : []2 }. By considering
this context, the supertype S can be written as

A[⊕{lcoffee : T1 }]i∈{1,2} = & lbut1 : ⊕{lcoffee : T1 }, lbut2 : ⊕{lcoffee : T2 }
Notice that in general an output selection can be anticipated even if it occurs
in a larger input context, such as, for example
A = &{lbut1 : &{lbut3 : []1 }, lbut2 : []2 }
Conceptually output anticipation reflects the fact that we are considering
asynchronous communication protocols in which messages are stored in queues.
In this setting, it is safe to replace a peer that follows a given protocol with
another one following a modified protocol where outputs are anticipated: in
fact, the difference is simply that such outputs will be stored earlier in the
communication queue.
2.3. Examples
Consider the types
T = µt.&{l : ⊕{l : t}}
S = µt.&{l : &{l : ⊕{l : t}}}
We have T ≤ S as the following infinite set of type pairs is a subtyping relation:



{ T , S , &{l: ⊕{l : T }} , S , ⊕ {l : T } , &{l : ⊕{l : S}} ,
T , &{l : S} , &{l : ⊕{l : T }} , &{l : S} , ⊕ {l : T } , S ,
T , &{l : &{l : S}} , . . . 
T , &{l : &{l : &{l : S}}} , . . .
... }
8

Notice that the types on the r.h.s. (S and subsequent ones) can always mimic the
initial actions of the corresponding type on the l.h.s. (T and subsequent ones).
Pairs are presented above in such a way that: the second one is reached from the
first one by rule 4. of Definition 2.4 (recursion), the third one is reached from the
second one by rule 3. of Definition 2.4 (input), the first one in the subsequent
line is reached from the third one by rule 2. of Definition 2.4 (output), and
similarly (using the same rules) in the subsequent lines. Notice that, every time
an output ⊕{l : } must be mimicked, the r.h.s. must be unfolded, and the
corresponding output is anticipated, since it is preceded by inputs only (i.e. the
output fills an input context). The effect of the anticipation of the output is
that a new input &{l : } is accumulated at the beginning of the r.h.s. It is
worth to observe that every accumulated input &{l : } is eventually consumed
in the simulation game, but the accumulated inputs grows unboundedly.
As another example consider
T = µt.&{
lbut1 : ⊕{lcoffee : t},
lbut2 : ⊕{ltea : t}
}
S = µt.&{
lbut2 : ⊕{
lcoffee : t,
ltea : &{lbut1 : t, lbut2 : t}
}
}
We have T ≤ S for the following reasons. Type T repeatedly alternates input
and output, the input corresponding to an input branching with labels lbut1
and lbut2 (where but stands for “button”), and the output with only one label:
either lcoffee or ltea . Also S infinitely repeats input and output, but, depending
on which of its inputs it performs, the corresponding input branching can have
fewer choices than T (in the case of the input branching with just one label,
i.e. lbut2 ). The output, instead, always corresponds to an output selection with
labels lcoffee and ltea . Such a difference between T and S is not problematic
due to contravariance on input branchings and covariance on output selections.
Type S also differs because after the input with label lbut2 and the output
with label ltea the type &{lbut1 : S, lbut2 : S} is reached, and this term (no
matter which input is chosen) may perform two consecutive inputs, the second
one available upon unfolding of S. Type T does not have two consecutive
inputs because it always alternates input and output. Nevertheless, we still
have T ≤ &{lbut1 : S, lbut2 : S} because, as discussed in the previous example,
according to our notion of asynchronous subtyping (rule 2. of Definition 2.4)
the output in the r.h.s. can be always anticipated to match the output actions
of the l.h.s., if they are preceded by inputs only.

9

3. Core Undecidability Result
In this section we prove our core undecidability result for a restricted subtyping relation. This relation is called asynchronous single-choice subtyping and
corresponds to the restriction of ≤ to pairs of session types (T, S) such that T
has output selections with one choice only, S has input branchings with one
choice only, and both T and S cannot have infinite sequences of outputs.
3.1. Asynchronous single-choice subtyping
In order to formally define such relation we need some preliminary definitions.
Definition 3.1 (Session types with single outputs). Given a set of labels
L, ranged over by l, the syntax of binary session types with single outputs is
given by the following grammar:
T out

::= ⊕{l : T out } | &{li : T out i }i∈I | µt.T out | t | end

Session types with single outputs are all those session types where inputs
can have multiple choices while outputs must be singletons.
Definition 3.2 (Session types with single inputs). Given a set of labels
L, ranged over by l, the syntax of binary session types with single inputs is
given by the following grammar:
T in

::= ⊕{li : T in i }i∈I | &{l : T in } | µt.T in | t | end

Session types with single inputs, instead, are all those session types where
inputs are singletons and outputs may have multiple choices.
Definition 3.3 (Session types with input guarded recursion). The set of
session types T noinf is composed of the session types T that satisfy the following
condition: for every subterm of T of the form µt.R, for some t and R, every
occurrence of t in R is inside a subterterm of R of the form &{li : Si }i∈I , for
some set of labels li and session types Si .
Session types with input guarded recursion have an important property:
there are no consecutive infinite outputs.
The asynchronous single-choice relation is defined as the subset of ≤ where
types on the left-hand side of the relation are with single outputs, types on the
right-hand side are with single inputs, and both types have no infinite sequences
of outputs.
Definition 3.4 (Asynchronous Single-Choice Relation). The asynchronous
single-choice relation << is defined as:
<< = ≤ ∩ (T out × T in ) ∩ (T noinf × T noinf )

10

Remark. Note that the asynchronous single-choice relation is not reflexive. In
fact, any type that has multiple (non single) choices is not related to itself, e.g.,
&{l1 : end, l2 : end} <6 < &{l1 : end, l2 : end} simply because the term on
right-hand side has more than one input branch.
3.2. Queue Machines
The proof of undecidability of the asynchronous single-choice relation is by
reduction from the acceptance problem for queue machines. Queue machines
have been already informally presented in the Introduction, we now report their
formal definition.
Definition 3.5 (Queue machine). A queue machine M is defined by a sixtuple (Q, Σ, Γ, $, s, δ) where:
• Q is a finite set of states;
• Σ ⊂ Γ is a finite set denoting the input alphabet;
• Γ is a finite set denoting the queue alphabet (ranged over by A, B, C, X);
• $ ∈ Γ − Σ is the initial queue symbol;
• s ∈ Q is the start state;
• δ : Q × Γ → Q × Γ∗ is the transition function.
In the Introduction we have informally described a queue machine that
accepts the language an bn , we now present its formal definition. Let M =
({q1 , q2 , q3 , qs }, {a, b}, {a, b, $}, $, q1 , δ) with δ defined as follows:
• δ(q1 , a) = (q2 , ), δ(q1 , $) = (q1 , ), δ(q1 , b) = (qs , b);
• δ(q2 , a) = (q2 , a), δ(q2 , $) = (qs , $), δ(q2 , b) = (q3 , );
• δ(q3 , a) = (qs , a), δ(q3 , $) = (q1 , $), δ(q3 , b) = (q3 , b);
• δ(qs , X) = (qs , X) for X ∈ {a, b, $}.
Differently from the informal definition in the Introduction, here (since, according to Definition 3.5, the transition function δ is expected to be total) we have
to consider an additional sink state which is entered whenever an unexpected
symbol is consumed from the queue. Once this state is entered, it will be no
longer possible to leave it, and every consumed symbol will be simply re-added
to the queue.
We now formally define queue machine computations.
Definition 3.6 (Queue machine computation). A configuration of a queue
machine is an ordered pair (q, γ) where q ∈ Q is its current state and γ ∈ Γ∗ is
the queue (Γ∗ is the Kleene closure of Γ). The starting configuration on an input
string x is (s, x$). The transition relation →M over configurations Q×Γ∗ , leading from a configuration to the next one, is defined as follows. For any p, q ∈ Q,
11

A ∈ Γ and α, γ ∈ Γ∗ we have (p, Aα) →M (q, αγ) whenever δ(p, A) = (q, γ).
A machine M accepts an input x if it eventually terminates on input x, i.e. it
reaches a blocking configuration with the empty queue (notice that, as the transition relation is total, the unique way to terminate is by emptying the queue).
Formally, x is accepted by M if (s, x$) →∗M (q, ) where  is the empty string
and →∗M is the reflexive and transitive closure of →M .
Going back to the queue machine M defined above, if we consider the input
aabb we have the following computation:
(q1 , aabb$) →M (q2 , abb$) →M (q2 , bb$a) →M (q3 , b$a) →M (q3 , $ab) →M
(q1 , ab$) →M (q2 , b$) →M (q3 , $) →M (q1 , $) →M (q1 , )
Hence, we can conclude that the string aabb is accepted by M (as any other
string of type an bn ).
Turing completeness of queue machines is discussed by Kozen [8] (page 354,
solution to exercise 99). A configuration of a Turing machine (tape, current head
position and internal state) can be encoded in a queue, and a queue machine
can simulate each move of the Turing machine by repeatedly consuming and
reproducing the queue contents, only changing the part affected by the move
itself. Formally, given any Turing machine T we have that a string x is accepted
by T if and only if x is accepted by the queuing machine M obtained as the
encoding of T . The undecidability of acceptance of an input string x by a
machine M follows directly from such encoding.
3.3. Modelling Queue Machines with Session Types
Our goal is to construct a pair of types, say T and S, from a given queue
machine M and a given input x, such that: T << S if and only if x is not accepted
by M . Intuitively, type T encodes the finite control of M , i.e., its transition
function δ, starting from its initial state s. And type S encodes the machine
queue that initially contains x$, where x is the input string x = X1 · · · Xn
of length n ≥ 0. The set of labels L for such types T and S is M ’s queue
alphabet Γ.
Formally, the queue of a machine is encoded into a session type as follows:
Definition 3.7 (Queue Encoding). Let M = (Q, Σ, Γ, $, s, δ) be a queue machine and let C1 · · · Cm ∈ Γ∗ , with m ≥ 0. Then, the queue encoding function
[C1 · · · Cm] is defined as:
[C1 · · ·Cm] = &{C1: . . . &{Cm : µt. ⊕ {A : &{A : t}}A∈Γ }}
Given a configuration (q, γ) of M , the encoding of the queue γ = C1 · · · Cm is
thus defined as [C1 · · · Cm].
Note that whenever m = 0, we have []] = µt. ⊕ {A : &{A : t}}A∈Γ . Observe
that we are using a slight abuse of notation: in both output selections and
input branchings, labels lA , with A ∈ Γ, are simply denoted by A.
12

A1?
A1!

.....

Xn?

$?

.....

X1?

Ak!
Ak?
Figure 2: Labelled Transition System of a session type encoding the initial queue X1 · · · Xn $

Figure 2 contains a graphical representation of the queue encoding with
its initial content X1 · · · Xn $. In order to better clarify our development, we
graphically represent session types as labeled transition systems (in the form
of communicating automata [9]), where an output selection ⊕{li : Ti }i∈I is
represented as a choice among alternative output transitions labeled with “li !”,
and an input branching &{li : Ti }i∈I is represented as a choice among alternative
input transitions labeled with “li ?”. Intuitively, we encode a queue containing
symbols C1 · · · Cm with a session type that starts with m inputs with labels
C1 , . . . , Cm , respectively. Thus, in Figure 2, we have C1 · · · Cm = X1 · · · Xn $.
After such sequence of inputs, representing the current queue content, there is
a recursive type representing the capability to enqueue new symbols. Such a
type repeatedly performs an output selection with one choice for each symbol
Ai in the queue alphabet Γ (with k being the cardinality of Γ), followed by an
input labeled with the same symbol Ai .
We now give the definition of the type modelling the finite control of a queue
machine, i.e., the encoding of the transition function δ.
Definition 3.8 (Finite Control Encoding). Let M = (Q, Σ, Γ, $, s, δ) be a
queue machine and let q ∈ Q and S ⊆ Q. Then,

µq.&{A : ⊕{B1A : · · · ⊕ {BnAA : [q 0]S∪q }}}A∈Γ



if q 6∈ S and δ(q, A) = (q 0 , B1A · · · BnAA )
[q]]S =



q
if q ∈ S
The encoding of the transition function of M is then defined as [s]]∅ .
The finite control encoding is a recursively defined term with one recursion
variable q for each state q ∈ Q of the machine. Above, [q]]S is a function that,
given a state q and a set of states S, returns a type representing the possible
behaviour of the queue machine starting from state q. Such behaviour consists
of first reading from the queue (input branching on A ∈ Γ) and then writing on
the queue a sequence of symbols B1A , . . . , BnAA . The parameter S is necessary
13

B11!

.....

Bn11 !

B1k!

.....

Bnk k !

A1?

.....

[[q ]]

[[q1]]

Ak?

[[qk ]]

(for Γ = {Ai |i ≤ k} and δ(q, Ai ) = (qi , B1i · · · Bni i ) for every i.)
Figure 3: Labelled Transition System of a session type encoding a finite control.

for managing the recursive definition of this type. In fact, as the definition of
the encoding function is itself recursive, this parameter keeps track of the states
that have been already encoded (see example below). In Figure 3, we report a
graphical representation of the Labelled Transition System corresponding to the
session type that encodes the queue machine finite control, i.e. the transition
function δ. Each state q ∈ Q is mapped onto a state [q]] of a session type,
which performs an input branching with a choice for each symbol in the queue
alphabet Γ (with k being the cardinality of Γ). Each of these choices represents
a possible character that can be read from the queue. After this initial input
branching, each choice continues with a sequence of outputs labeled with the
symbols that are to be inserted in the queue (after the symbol labeling that
choice has been consumed). This is done according to function δ, assuming
that δ(q, Ai ) = (qi , B1i · · · Bni i ), with ni ≥ 0, for all i in {1, . . . , k}. After the
insertion phase, state [qi] of the session type corresponding to state qi of the
queue machine is reached.
Notice that, queue insertion actually happens in the encoding because, when
the encoding of the finite control performs an output of a B symbol, the encoding
of the queue must mimic such an output, possibly by anticipating it. This has
the effect of adding an input on B at the end of the sequence of initial inputs
of the queue machine encoding.
Observe that our encodings generate terms that belong to the restricted
syntax of session types introduced in the previous section, namely the queue
encoding of Definition 3.7 produces types in T in , while the finite control encoding
of Definition 3.8 produces types in T out .
Example. As an example, consider a queue machine with two states s and q,
any non-empty input and queue alphabets Σ and Γ, and a transition relation
defined as follows: δ(s, A) = (q, A) and δ(q, A) = (s, ), for every queue symbol
A ∈ Γ. We have that
[s]]∅

= µs.&{A : ⊕{A : [q]]{s} }}A∈Γ
= µs.&{A : ⊕{A : µq.&{A : [s]]{s,q} }A∈Γ }}A∈Γ
= µs.&{A : ⊕{A : µq.&{A : s}A∈Γ }}A∈Γ

14

3.4. Properties of the Encodings
We begin by proving that subtyping is preserved by reductions of queue
machines (modulo our encoding), and then we exploit this property (Lemma
3.1) to prove our core undecidability result (Theorem 3.1).
Lemma 3.1. Consider a queue machine M = (Q, Σ, Γ, $, s, δ). If (q, γ) →M
(q 0 , γ 0 ) and [q]]∅ << [γ]] then also [q 0]∅ << [γ 0].
Proof. Assume that (q, γ) →M (q 0 , γ 0 ) with γ = C1 · · · Cm and δ(q, C1 ) =
(q 0 , B1C1 · · · BnCC11 ). Then we have that γ 0 = C2 · · · Cm B1C1 · · · BnCC11 .
Assume now [q]]∅ << [γ]]; this means that there exists an asynchronous subtyping relation R s.t. ([[q]]∅ , [C1 · · · Cm]) ∈ R. By item 4 of Definition 2.4, we
also have

&{A : ⊕{B1A : · · · ⊕ {BnAA : [q 0]∅ }}}A∈Γ , [C1 · · · Cm] ∈ R
where the l.h.s. has been unfolded once. By item 3 of Definition 2.4, the presence
of the above pair in R guarantees also that

⊕{B1C1 : ⊕{B2C1 : · · · ⊕ {BnCC11 : [q 0]∅ }}} , unfoldn0 (&{C2 : · · · &{Cm : Z}}) ∈ R
for some n0 , and with Z = µt. ⊕ {A : &{A : t}}A∈Γ . By item 2 of Definition
2.4, the presence of this last pair in R guarantees also that

⊕{B2C1 : · · · ⊕ {BnCC11 : [q 0]∅ }} , unfoldn1 (&{C2 : · · · &{Cm : &{B1C1 : Z}}}) ∈ R
for some n1 . By repeating the same reasoning on B2C1 , · · · , BnCC11 we conclude
that also

[q 0]∅ , unfoldnC1 (&{C2 : · · · &{Cm : &{B1C1 : · · · &{BnCC11 : Z}}}}) ∈ R
for some nC1 .
We now observe that if an asynchronous subtyping relation R contains
the pair (T, unfoldn (S)), for some n, then we have that also the following is
an asynchronous subtyping relation: R ∪ {(T 0 , S)|T 0 ∈ topUnfold(T )}, where
topUnfold(T ) is the minimal set of types that contains T and such that µt.R ∈
topUnfold(T ) implies R{µt.R/t} ∈ topUnfold(T ).
In the light of this last observation we can now conclude that having

[q 0]∅ , unfoldnC1 (&{C2 : · · · &{Cm : &{B1C1 : · · · &{BnCC11 : Z}}}})
in the asynchronous subtyping relation R implies that
[q 0]∅ << &{C2 : · · · &{Cm : &{B1C1 : · · · &{BnCC11 : Z}}}}
Notice that the r.h.s. corresponds to [γ 0]. Hence we have proved the thesis
[q 0]∅ << [γ 0].

We are now ready to prove our main theorem.
15

Theorem 3.1. Given a queue machine M = (Q, Σ, Γ, $, s, δ), an input string
x, and the two types T = [s]]∅ and S = [x$]], we have that M accepts x if and
only if T <
6 < S.
Proof. We prove the two directions separately.
(Only if part). We first observe that [q]]∅ <
6 < []] for every possible state q.
In fact, [q]]∅ is a recursive definition that upon unfolding begins with an input branching that implies (according to items 3. and 4. of Definition 2.4)
that also []] (once unfolded, if needed) should start with an input branching. But this is false, in that, by definition of the encoding we have []] =
µt. ⊕ {A : &{A : t}}A∈Γ . We can conclude that [s]]∅ <6 < [x$]] because otherwise,
by repeated application of Lemma 3.1, we would have that the termination of
the queue machine, i.e. (s, x$) →∗M (q, ), implies the existence of a state q such
that [q]]∅ << []]. But we have just proved that [q]]∅ << []] does not hold, for every
state q.
(If part). Our aim is to show that if T 6<< S then M accepts x, which
is equivalent to showing that T << S, assuming that M does not accept x.
When a queue machine does not accept an input, the corresponding computation never ends. In our case, this means that there is an infinite sequence
(s, x$) →M (q1 , γ1 ) →M · · · →M (qi , γi ) →M · · · . Let C be the set of reachable
configurations, i.e. C = {(qi , γi ) | i ≥ 0} where we assume (q0 , γ0 ) = (s, x$). We
now define a relation R on types:
R
{

|

=

[q]]∅ , [C1 · · · Cm] ,

&{A : ⊕{B1A : · · · ⊕ {BnAA : [q 0]∅ }}}A∈Γ , [C1 · · · Cm] ,
⊕ {B1C1 : ⊕{B2C1 : · · · ⊕ {BnCC11 : [q 0]∅ }}} , &{C2 : · · · &{Cm : Z}}
⊕ {B2C1 : · · · ⊕ {BnCC11 : [q 0]∅ }} , &{C2 : · · · &{Cm : &{B1C1 : Z}}}
···

[q 0]∅ , &{C2 : · · · &{Cm : &{B1C1 : · · · &{BnCC11 : Z}}}}
(q, C1 · · · Cm ) ∈ C, δ(q, C1 ) = (q 0 , B1C1 · · · BnCC11 ),
Z = µt. ⊕ {A : &{A : t}}A∈Γ }


,

,

Notice that the type pairs listed in the above definition correspond to the
pairs discussed in the proof of Lemma 3.1. We have that the above R is a
subtyping relation because, using a reasoning similar to the one reported in
the proof of Lemma 3.1, it is immediate to see that each of the pairs satisfies the conditions in Definition 2.4 thanks to the presence of the subsequent
pair. The unique pair without a subsequent pair is the last one, but this last
pair corresponds to the first one of the pairs corresponding to the configuration
(q 0 , C2 · · · Cm B1C1 · · · BnCC11 ) ∈ C reached in the queue machine computation af-

ter (q, C1 · · · Cm ), i.e. (q, C1 · · · Cm ) →M (q 0 , C2 · · · Cm B1C1 · · · BnCC11 ). We can
conclude observing that T << S because T = [s]]∅ , S = [x$]] and (s, x$) ∈ C
implies that ([[s]]∅ , [x$]]) belongs to the above subtyping relation R.

As a corollary, we have that the asynchronous single-choice relation is undecidable.
16

Corollary 3.1. Asynchronous single-choice subtyping for binary session types
<< is undecidable.
Proof.
From Theorem 3.1 we know that given any queue machine M =
(Q, Σ, Γ, $, s, δ), an input string x, and the two types T = [s]]∅ and S = [x$]], we
have that M does not accept x if and only if T << S. From the undecidability
of acceptance for queue machines we can conclude the undecidability of <<. 
4. Impact of the Undecidability Result
Starting from our core undecidability result we prove the undecidability of
other subtyping relations starting from ≤. In the following subsections, for the
sake of simplicity, we denote different session type languages with the same
letters T, S, . . . and the actual language will be made clear by the context.
4.1. Undecidability of Asynchronous Subtyping
The undecidability of the asynchronous single-choice relation can be exploited to show that asynchronous subtyping is undecidable. Intuitively, this
follows by the fact that the encoding of a queue machine into << is also a valid
encoding into ≤.
Corollary 4.1. Asynchronous subtyping for binary session types ≤ is undecidable.
Proof. A direct consequence of the undecidability of <<, i.e. ≤ restricted to
the pairs of types belonging to (T out × T in ) ∩ (T noinf × T noinf ).

4.2. Standard Binary Session Types with Asynchronous Subtyping
The syntax proposed in Definition 2.1 allows for the definition of session
types with only output selections and input branchings, and recursion. Standard
binary session types [4] also feature classic send/receive types, containing the
type of the communicated message, dubbed carried type. Carried types can be
primitive types such as bool, nat, . . . or a session type T (modelling delegation).
We define standard binary session types as follows:
Definition 4.1 (Standard Session Types). Standard binary session types are
defined as
T
U

::= . . . as in Definition 2.1 . . . | !hU i.T | ?(U ).T
::= T | bool | nat | . . .

In order to extend subtyping to standard binary session types, we need to
adapt the notion of unfolding. The n-unfolding function is extended as follows:
. . . as in Definition 2.2 . . .
unfold1 (!hU i.T ) = !hU i.unfold1 (T )
unfold1 (?(U ).T ) = ?(U ).unfold1 (T )
17

Moreover, the input context definition becomes:
A ::= . . . as in Definition 2.3 . . .

| ?(U ).A

Finally, the asynchronous subtyping relation for standard binary session
types is given by the following:
Definition 4.2. (Asynchronous Subtyping for Standard Session Types,
≤s ) Asynchronous subtyping for standard session types is defined as in Definition 2.4 where we consider a relation R on both session and primitive types
that satisfies, besides the items in that definition, also the following ones (with
an abuse of notation, we use T and S to range over both session and primitive
types):
5. if T ∈ {bool | nat | . . .} then S = T ;
6. if T = !hU i.T 0 then ∃n ≥ 0, A such that
– unfoldn (S) = A[!hVk i.Sk ]k∈{1,...,m} ,
– ∀k ∈ {1, . . . , m}.(Vk , U ) ∈ R and
– (T, A[Sk ]k∈{1,...,m} ) ∈ R;
7. if T = ?(U ).T 0 then ∃n ≥ 0 such that unfoldn (S) = ?(V ).S 0 and (U, V ) ∈
R and (T 0 , S 0 ) ∈ R.
The undecidability proof applies to this extended setting:
Corollary 4.2. Asynchronous subtyping ≤s for standard binary session types
is undecidable.
Proof. The core session type language in Definition 2.1 on which ≤ is defined is
a fragment of the standard session type language defined in the present section.
The thesis follows from the fact that on this fragment the two subtyping relations
≤ and ≤s coincide.

Remark. It is worth to observe that the asynchronous subtyping relation ≤s
defined above corresponds to the one by Mostrous and Yoshida [1], with the
only difference that the various rules for the different kinds of carried types
considered in that paper are replaced by the simpler rule 5., that considers
primitive types only (carried session types are managed by the rules 6. and 7.).
Hence our undecidability result applies also to the subtyping by Mostrous and
Yoshida [1].
4.3. Carried Types in Selection/Branching and no Orphan Messages
Chen et al. [2] propose a variant of standard binary session types where messages of some type can also be communicated together with a choice performed
within an output selection/input branching. This is defined by the following
syntax.
18

Definition 4.3 (Session types with carried types on choices [2]).
T
U

::= ⊕{li hUi i : Ti }i∈I | &{li (Ui ) : Ti }i∈I | µt.T | t | end
::= T | bool | nat | . . .

This syntax corresponds with the one we have considered in Definition 2.1,
where ⊕{li : Ti }i∈I and &{li : Ti }i∈I are replaced by ⊕{li hUi i : Ti }i∈I and
&{li (Ui ) : Ti }i∈I , respectively. The definition of n-unfolding can be updated
accordingly.
Chen et al. [2] also propose a different definition of subtyping that does
not allow to have orphan messages, i.e., inputs on the right-hand side of the
subtyping relation cannot be indefinitely delayed. We reformulate the subtyping
by Chen et al. [2] (defined on infinite trees) as follows.
Definition 4.4 (Asynchronous Orphan-Message-Free Subtyping, ≤o ).
Asynchronous subtyping for orphan-message-free session types is defined as in
Definition 2.4 where we consider a relation R on both session and primitive
types that satisfies the items in that definition, with items 2. and 3. replaced by
the following corresponding ones, plus the additional rule 5. (also in this case,
we use T and S to range over both session and primitive types):
2. if T = ⊕{li hUi i : Ti }i∈I then ∃n ≥ 0, A such that
– ∃j ∈ I s.t. Tj does not contain input branchings implies A = [ ]1 ,
– unfoldn (S) = A[⊕{lj hVkj i : Skj }j∈Jk ]k∈{1,...,m} ,
– ∀k ∈ {1, . . . , m}.I ⊆ Jk and
– ∀i ∈ I, k ∈ {1, . . . , m}.(Vki , Ui ) ∈ R;
– ∀i ∈ I.(Ti , A[Ski ]k∈{1,...,m} ) ∈ R;
3. if T = &{li (Ui ) : Ti }i∈I then ∃n ≥ 0 such that
unfoldn (S) = &{lj (Vj ) : Sj }j∈J , J ⊆ I and ∀j ∈ J.(Uj , Vj ), (Tj , Sj ) ∈ R;
5. if T ∈ {bool | nat | . . .} then S = T .
The key point in the definition above is rule 2., first item, that guarantees
that if the r.h.s. does not start with the output needed to be mimicked in the
simulation game, and then such output must be anticipated, then all possible
continuations in the l.h.s. must contain at list an input. This implies that
the input in the r.h.s. that have been delayed due to the anticipation, will
be eventually involved in the simulation game, i.e. they will be not delayed
indefinitely. It is worth to notice that this is guaranteed already by the core
relation << because it avoids processes from having consecutive infinite outputs.
Also in this case the undecidability proof applies to this extended setting:
Corollary 4.3. Asynchronous subtyping ≤o for binary session types with carried types in output selections/input branchings and asynchronous orphan-messagefree subtyping is undecidable.

19

Proof. First of all, we observe that our core session language has a one-to-one
correspondence with a fragment of the language given in Definition 4.3, under
the assumption that only one given primitive type can be carried (e.g. bool).
Then, we observe (as already remarked above) that if we consider terms without
consecutive infinite outputs the new additional first item of rule 2. in Definition
4.4 can be omitted without changing the defined relation. In fact, we show
that it is implied by the other conditions. If during the simulation game an
output is anticipated w.r.t. some inputs in the r.h.s. (i.e. we use A 6= [ ]1 in the
application of rule 2.) then the continuations of the simulation game could be
either finite or infinite. For the finite continuations we have that the inputs in
front of the r.h.s. must be eventually consumed otherwise the pair (end, end)
cannot be reached; hence at least one input should be present in the l.h.s. In
the infinite continuations, the fact that the l.h.s. has no consecutive infinite
outputs guarantees the presence in such term of at least one input.
Hence we can conclude that <<, which is defined on terms belonging to T noinf ,
is isomorphic to ≤o restricted to terms without consecutive infinite output. The
undecidability of ≤o thus directly follows from the undecidability of <<.

Remark. It is immediate to conclude that also the subtyping relation by Chen
et al. [2] is undecidable.
4.4. Multiparty session types
We now investigate how our undecidability result can be applied to a version
of multiparty session types given by Mostrous et al. [3]. Multiparty session types
are an extension of binary session types that allow to describe protocols between
several parties. Protocols, specified as global types [5], can then be projected
into local types, formally defined as follows.
Definition 4.5 (Local Types).
T
U

::= k!hU i.T | k?(U ).T | k ⊕ {li : Ti }i∈I | k&{li : Ti }i∈I | µt.T | t | end
::= T | bool | nat | . . .

Local types are a generalisation of the standard binary session types seen in
Definition 4.1, where communications can now be performed on different channels, e.g., a process involved in a session with type k!hU i.k 0 ?(U 0 ).T first outputs
something of type U on channel k, and, then, inputs something of type U 0 from
channel k 0 .
Before introducing our definition of subtyping for local types, we note that
the definition of n-unfolding can be trivially adapted to terms in the definition
above from our initial definition. Moreover, we need to redefine input contexts
for local types: such contexts now contain also outputs, under the assumption
that those outputs are on different channels. This reflects the fact that ordering
is guaranteed to be preserved only by messages sent on the same channel. Technically, we use a parameterized notion of input context Ak where k is assumed
to be the channel of the output to be anticipated.

20

Definition 4.6 (Multiparty input context). A multiparty input context Ak
is a session type with multiple holes defined by the following syntax:
Ak ::= [ ]n | k 0 ?(U ).Ak | k 0 &{li : Ak i }i∈I | k 00 !hU i.Ak | k 00 ⊕ {li : Ak i }i∈I
where we assume that k 0 is any possible channel while k 00 6= k.
We are now ready to define the subtyping relation for local types. The
definition of subtyping we propose is inspired by the one initially proposed
by Mostrous et al. [3]. Unlike the binary case, outputs on a channel can be
anticipated over inputs and outputs on different channels. Moreover, unlike
Mostrous et al. [3], we allow outputs to be anticipated over inputs on the same
channel, and we do not allow inputs over different channels to be swapped. The
former point carries the same intuition as the output anticipation for the binary
case. The latter is a restriction that guarantees that subtyping preserves the
ordering of observable events (input actions) given by the corresponding global
type specification of the protocol. The definition of asynchronous subtyping is
then given as follows:
Definition 4.7 (Multiparty Asynchronous Subtyping, ≤m ).
Asynchronous subtyping for multiparty session types is defined as in Definition 2.4 where we consider a relation R on both session and primitive types
that satisfies the items in that definition, with items 2. and 3. replaced by the
following corresponding ones, plus the additional items 5.–7. (also in this case,
we use T and S to range over both session and primitive types):
Asyncronous subtyping for multiparty session types is defined as in Definition 4.2, by replacing the items about selection, branching, output and input
with:
2. if T = k ⊕ {li : Ti }i∈I then ∃n ≥ 0, Ak such that
– unfoldn (S) = Ak [k ⊕ {lj : Shj }j∈Jh ]h∈{1,...,m} ,
– ∀h ∈ {1, . . . , m}.I ⊆ Jh and
– ∀i ∈ I.(Ti , Ak [Shi ]h∈{1,...,m} ) ∈ R;
3. if T = k&{li : Ti }i∈I then ∃n ≥ 0 such that unfoldn (S) = k&{lj : Sj }j∈J ,
J ⊆ I and ∀j ∈ J.(Tj , Sj ) ∈ R;
5. if T ∈ {bool | nat | . . .} then S = T ;
6. if T = k!hU i.T 0 then ∃n ≥ 0, Ak such that
– unfoldn (S) = Ak [k!hVh i.Sh ]h∈{1,...,m} ,
– ∀h ∈ {1, . . . , m}.(Vh , U ) ∈ R and
– (T, Ak [Sh ]h∈{1,...,m} ) ∈ R;
7. if T = k?(U ).T 0 then ∃n ≥ 0 such that unfoldn (S) = k?(V ).S 0 and
(U, V ) ∈ R and (T 0 , S 0 ) ∈ R.
21

As for the other cases, subtyping is undecidable:
Corollary 4.4. Asynchronous subtyping for multiparty session types is undecidable.
Proof. Similarly to the case for session types with carried types in branching/selection, standard session types defined in Definition 4.1 have a one-to-one
correspondence with a fragment of local types where only one single channel,
e.g., k, is used. Then, the thesis follows from the fact that on such fragment
the two subtyping relations ≤s and ≤m are isomorphic.

Remark. The proof of the previous Lemma does not directly work for the definition of asynchronous subtyping used by Mostrous et al. [3]. This is because
their subtyping relation does not allow to anticipate outputs over inputs on the
same channel, e.g., k!hU i.k?(U 0 ).T is not a subtype of k?(U 0 ).k!hU i.T . However, output anticipation is possible over inputs on different channels, e.g.,
k!hU i.k 0 ?(U 0 ).T is a subtype of k 0 ?(U 0 ).k!hU i.T , assuming k 6= k 0 . The subtyping algorithm proposed by Mostrous et al. [3] correctly checks cases like the
above two examples, but fails to terminate when there is an unbounded accumulation of inputs as in the first example that we have discussed in §2.3. Rephrasing
that example in the syntax of local types, we have that T = µt.k 0 ?(U 0 ).k!hU i.t
and S = µt.k 0 ?(U 0 ).k 0 ?(U 0 ).k!hU i.t are in subtyping relation, even for Mostrous
et al. [3]. Nevertheless, the algorithm proposed in that paper does not terminate because, in this case, it is expected to check infinitely many different pairs
(T, k 0 ?(U 0 ).S), (T, k 0 ?(U 0 ).k 0 ?(U 0 ).S), . . . . In the light of our undecidability
result, we can even conclude the impossibility to check algorithmically the subtyping relation by Mostrous et al. [3]. Consider the proof of our Theorem 3.1:
given a queue machine, we can change both encodings of its finite control and
its queue so that all inputs are on some special channel k and all outputs are
on some special channel k 0 , with k 6= k 0 . As discussed above, outputs on k 0 can
be anticipated w.r.t. inputs on a different channel k, hence the two encodings
will be in a subtyping relation, also for the subtyping by Mostrous et al. [3], if
and only if the encoded machine does not terminate.
4.5. Communicating automata
A Communicating Finite State Machine (CFSM) [9], or more simply a communicating automaton, is defined as a finite automaton (Q, q0 , Σ, δ), where
• Q is a finite set of states
• q0 ∈ Q is the initial state
• Σ is a finite alphabet, and
• δ ⊆ Q × Σ × {!, ?} × Q is a transition set.
We use “?” to represent inputs and “!” to represent outputs (in CFSMs [9] “+”
and “−”, respectively, are used, instead).
22

A CFSM is a labeled transition system that can be employed to graphically
represent a session type (see, e.g., Figures 2 and 3). Note that in general a
CFSM may express more behaviours than the ones described by session types:
it can include non-deterministic and mixed choices, i.e. choices including both
inputs and outputs.
Let T be the set of all session types T and L the alphabet of session types,
we define a transition relation −→ ⊆ T × L × {!, ?} × T , as the least transition
set satisfying the following rules
l !

i∈I

l ?

i∈I

i
⊕{li : Ti }i∈I −→
Ti
i
&{li : Ti }i∈I −→
Ti

α

T {µt.T /t} −→ T 0
α

µt.T −→ T 0
with α ranging over L × {!, ?}.
Given a session type T we define CF SM (T ) as being the communicating
automaton (QT , T, L, δT ), where: L is the alphabet of session types, QT is the
set of terms T 0 which are reachable from T according to −→ relation and δT is
defined as the restriction of −→ to QT × L × {!, ?} × QT . For example Figure
2 depicts CF SM (S) with S being the session type defined in Definition 3.7
(assuming Γ = {Ai | i ≤ k}).
We, thus, get the following result as a consequence of undecidability of ≤.
Any relation  over communicating automata (usually called refinement relation
in this context) that is such that CF SM (T )  CF SM (T 0 ) if and only if T ≤ T 0 ,
i.e. it reduces to our subtyping definition for the subclass of communicating
automata not including non-deterministic and mixed choices, is undecidable.
5. Decidable Fragments of Aynchronous Single-Choice Relation
We now show that we cannot further reduce (w.r.t. branching/selection
structure) the core undecidable fragment: if we consider single-output selection only or single-input branching only, we obtain a decidable relation.
Definition 5.1 (Asynchronous Single-Choice Output Relation).
The asynchronous single-choice output relation <<sout is defined as:
<<sout = << ∩ (T out × T out )
Definition 5.2 (Asynchronous Single-Choice Input Relation).
The asynchronous single-choice input relation <<sin is defined as:
<<sin = << ∩ (T in × T in )

23

Σ, (T, S) ` T ≤a S

Asmp

Σ ` end ≤a end

End

J ⊆ I ∀j ∈ J . Σ ` Tj ≤a Sj
∀n.I ⊆ Jn ∀i ∈ I . Σ ` Ti ≤a A[Sni ]n
Out
In
Σ ` ⊕{li : Ti }i∈I ≤a A[⊕{lj : Snj }j∈Jn ]n
Σ ` &{li : Ti }i∈I ≤a &{lj : Sj }j∈J
Σ, (µt.T, S) ` unfold1 (µt.T ) ≤a S
RecL
Σ ` µt.T ≤a S
T = end ∨ T = &{li : Ti }i∈I Σ, (T, µt.S) ` T ≤a unfold1 (µt.S)
RecR1
Σ ` T ≤a µt.S
n = depth(S, ∅)

n≥1

Σ, (⊕{li : Ti }i∈I , S) ` ⊕{li : Ti }i∈I ≤a unfoldn (S)
RecR2
Σ ` ⊕{li : Ti }i∈I ≤a S

Figure 4: A Procedure for Checking Subtyping

As a matter of fact, we prove decidability for larger relations w.r.t. <<sin
and <<sout where we do not impose the constraint about no consecutive infinite
outputs.
In order to define an algorithm for deciding the two relations above, we
first adapt to our setting the procedure defined in Mostrous et. al [3] and then
improve it to precisely characterize the two relations. The initial procedure is
defined for the unrestricted syntax of session types, i.e. the subtyping ≤; while
the improved version assumes to work on types restricted according to the singlechoice assumptions, i.e. the two new relations <<sin and <<sout . Actually, in
order to have a more general decidability result, we show that it is not necessary
to consider the constraint about no consecutive infinite outputs.
The procedure is defined by the rules reported in Figure 4. In the rules, the
environment Σ is a set of pairs (T, S) used to keep track of previously visited
pairs of types. The procedure successfully terminates either by applying rule
Asmp (which has priority over the other rules) or by applying rule End. In
the former case, a previously visited pair is being visited again, and therefore,
there is no need to proceed further. Rules In and Out are straightforward. The
procedure always unfolds on the left-hand side when necessary (rule RecL). If
this is not the case, but it is necessary to unfold on the right-hand side, it is
possible to apply either RecR1 or RecR2 , depending on whether the left-hand
side type is an input (or an end) or an output, respectively. In the first case, a
single unfolding is sufficient. However, we may need to unfold several times in
the case we need an output. The partial function depth (we write depth(S) = ⊥
if depth is undefined on S) measures the number of unfoldings necessary for

24

anticipating such output. The function is inductively defined as:
depth(end, Γ) = ⊥
depth(⊕{li : Ti }i∈I , Γ) = 0
depth(&{li: Ti }i∈I , Γ) = max{depth(Ti , Γ) | i ∈ I}
⊥
if t ∈ Γ
depth(µt.T, Γ) =
1 + depth(T {µt.T /t}, Γ + {t}) otherwise
In the definition of depth, we assume that max{depth(Ti , Γ) | i ∈ I} = ⊥ if
depth(Ti , Γ) = ⊥ for some i ∈ I. Similarly, 1 + ⊥ = ⊥.
The subtyping procedure, when it has to check whether T ≤ S, applies the
rules from bottom to top starting from the judgement ∅ ` T ≤a S. We write
Σ ` T ≤a S → Σ0 ` T 0 ≤a S 0 if Σ ` T ≤a S matches the consequences of
one of the rules, and Σ0 ` T 0 ≤a S 0 is produced by the corresponding premises.
Σ ` T ≤a S →∗ Σ0 ` T 0 ≤a S 0 is the reflexive and transitive closure of such
relation. We write Σ ` T ≤a S →err to mean that no rule can be applied to the
judgement Σ ` T ≤a S. We give priority to the application of the rule Asmp to
have a deterministic procedure: this is sufficient because all the other rules are
alternative, i.e., given a judgement Σ ` T ≤a S there are no two rules that can
be both applied.
We now prove that the above procedure is a semi-algorithm for checking
whether two types are not in subtyping relation.
Lemma 5.1. Given the types T and S we have ∃Σ0 , T 0 , S 0 . ∅ ` T ≤a S →∗
Σ0 ` T 0 ≤a S 0 →err if and only if T ≤
6 S.
Proof. We prove the two implications separately. We start with the if part and
proceed by contraposition. Assume that it is not true that ∃Σ0, T 0, S 0 . ∅ ` T ≤a S
→∗ Σ0 ` T 0 ≤a S 0 →err . Consider now the relation
R = {(T 0 , S 0 ) | ∃Σ0 . ∅ ` T ≤a S →∗ Σ0 ` T 0 ≤a S 0 }
We show that R is a subtyping relation. Let (T 0 , S 0 ) ∈ R. Then, it is possible
to apply at least one rule to Σ0 ` T 0 ≤a S 0 for the environment Σ0 such that
∅ ` T ≤a S →∗ Σ0 ` T 0 ≤a S 0 . We proceed by cases on T 0 . In the following we use nrec(R) to denote the number of unguarded –not prefixed by some
branching/selection– occurrences of recursions µt.R0 in R for any R0 , t.
• If T 0 = end then item 1 of Definition 2.4 for pair (T 0 , S 0 ) is shown by
induction on k = nrec(S 0 ).
– Base case k = 0. The only rule applicable to Σ0 ` T 0 ≤a S 0 is End,
that immediately yields the desired pair of R.
– Induction case k > 0. The only rules applicable to Σ0 ` T 0 ≤a S 0 are
Asmp and RecR1 . In the case of Asmp we have that (T 0 , S 0 ) ∈ Σ0 ,
hence there exists Σ00 with (T 0 , S 0 ) ∈
/ Σ00 such that ∅ ` T ≤a S →∗
00
0
0
∗
0
0
Σ ` T ≤a S → Σ ` T ≤a S 0 and rule RecR1 has been applied to Σ00 ` T 0 ≤a S 0 . So for some Σ000 (= Σ0 or = Σ00 ) we have
25

that the procedure applies rule RecR1 to Σ000 ` T 0 ≤a S 0 . Hence
Σ000 ` T 0 ≤a S 0 → Σ0000 ` T 0 ≤a unfold1 (S 0 ) . Since nrec(unfold1 (S 0 )) =
k − 1, by induction hypothesis item 3 of Definition 2.4 holds for pair
(T 0 , unfold1 (S 0 )), hence it holds for pair (T 0 , S 0 ).
• If T 0 = ⊕{li : Ti }i∈I then item 2 of Definition 2.4 for pair (T 0 , S 0 ) is shown
as follows:
– If depth(S, ∅) = 0 then the only rule applicable to Σ0 ` T 0 ≤a S 0 is
Out, that immediately yields the desired pairs of R.
– If depth(S, ∅) ≥ 1 then the only rules applicable to Σ0 ` T 0 ≤a S 0 are
Asmp and RecR2 . In the case of Asmp we have that (T 0 , S 0 ) ∈ Σ0 ,
hence there exists Σ00 with (T 0 , S 0 ) ∈
/ Σ00 such that ∅ ` T ≤a S →∗
00
0
0
∗
0
0
Σ ` T ≤a S → Σ ` T ≤a S 0 and rule RecR2 has been applied to Σ00 ` T 0 ≤a S 0 . So for some Σ000 (= Σ0 or = Σ00 ) we have
that the procedure applies rule RecR2 to Σ000 ` T 0 ≤a S 0 . Hence
Σ000 ` T 0 ≤a S 0 → Σ0000 ` T 0 ≤a unfoldk (S 0 ), taking k = depth(S, ∅).
Since depth(unfoldk (S 0 )) = 0, we end up in the previous case. Therefore item 3 of Definition 2.4 holds for pair (T 0 , unfoldk (S 0 )), hence it
holds for pair (T 0 , S 0 ).
• If T 0 = &{li : Ti }i∈I then item 3 of Definition 2.4 for pair (T 0 , S 0 ) is shown
by induction on k = nrec(S 0 ):
– Base case k = 0. The only rule applicable to Σ0 ` T 0 ≤a S 0 is In, that
immediately yields the desired pairs of R.
– Induction case k > 0. The only rules applicable to Σ0 ` T 0 ≤a S 0 are
Asmp and RecR1 . In the case of Asmp we have that (T 0 , S 0 ) ∈ Σ0 ,
hence there exists Σ00 with (T 0 , S 0 ) ∈
/ Σ00 such that ∅ ` T ≤a S →∗
00
0
0
∗
0
0
0
Σ ` T ≤a S → Σ ` T ≤a S and rule RecR1 has been applied
to Σ00 ` T 0 ≤a S 0 . So for some Σ000 (= Σ0 or = Σ00 ) we have that
the procedure applies rule RecR1 to Σ000 ` T 0 ≤a S 0 . Hence Σ000 `
T 0 ≤a S 0 → Σ0000 ` T 0 ≤a unfold1 (S 0 ) . Since nrec(unfold1 (S 0 )) =
k − 1, by induction hypothesis item 3 of Definition 2.4 holds for pair
(T 0 , unfold1 (S 0 )), hence it holds for pair (T 0 , S 0 ).
• If T 0 = µt.T 0 then item 4 of Definition 2.4 for pair (T 0 , S 0 ) holds because
the only rule applicable to Σ0 ` T 0 ≤a S 0 is RecL that immediately yields
the desired pair of R.
We now prove the only if part and proceed by contraposition. Assume that
there exists a relation R that is a subtyping relation such that (T, S) ∈ R.
We say that Σ ` T ≤a S →w Σ0 ` T 0 ≤a S 0 if Σ ` T ≤a S →∗ Σ0 ` T 0 ≤a S 0
and: the last rule applied is one of Out, In or RecL rules; while all previous ones
are RecR1 or RecR2 rules.
We start by showing that if ∃Σ. ∅ ` T ≤a S →∗w Σ ` T 0 ≤a S 0 implies
∃n. (T 0 , unfoldn (S 0 )) ∈ R. The proof is by induction on the length of such

26

computation →∗w of the procedure. The base case is for a 0 length computation:
it yields (T, S) ∈ R which holds. For the inductive case we assume it holds
for all computations of a length k and we show it holds for all computations
of length k + 1, by considering all judgements Σ0 ` T 00 ≤a S 00 such that Σ `
T 0 ≤a S 0 →w Σ0 ` T 00 ≤a S 00 . This is shown by first considering the case
in which rule Asmp applies to Σ ` T 0 ≤a S 0 : in this case there is no such a
judgement and there is nothing to prove. Then we consider the case in which
T 0 = end and Σ ` end ≤a S 0 →∗ Σ000 ` end ≤a end (by applying RecR1
rules) and rule End applies to Σ000 ` end ≤a end. Also in this case there is no
such a judgement Σ0 ` T 00 ≤a S 00 and there is nothing to prove. Finally, we
proceed by an immediate verification that judgements Σ0 ` T 00 ≤a S 00 produced
in remaining cases are required to be in R by items 2, 3 and 4 of Definition
2.4: T 0 = ⊕{li : Ti }i∈I (→w is a possibly empty sequence of RecR2 applications
followed by Out application), T 0 = &{li : Ti }i∈I (→w is a possibly empty
sequence of RecR1 applications followed by In application) or T 0 = µt.T 0 (→w
is simply RecL application).
We finally observe that, considered any judgement Σ ` T 0 ≤a S 0 such that
∃n. (T 0 , unfoldn (S 0 )) ∈ R, we have:
• either rule Asmp applies to Σ ` T 0 ≤a S 0 , or
• T 0 = end and, by item 1 of Definition 2.4, there exists Σ0 such that
Σ ` end ≤a S 0 →∗ Σ0 ` end ≤a end (by applying RecR1 rules) and rule
End is the unique rule applicable to Σ0 ` end ≤a end, with RecR1 being
the unique rule applicable to intermediate judgements, or
• by items 2,3 and 4 of Definition 2.4, there exist Σ0 , T 00 , S 00 such that Σ `
T 0 ≤a S 0 →∗w Σ0 ` T 00 ≤a S 00 , with each intermediate judgement having
a unique applicable rule. In particular this holds for T 0 = ⊕{li : Ti }i∈I
(→w is a possibly empty sequence of RecR2 applications followed by Out
application), T 0 = &{li : Ti }i∈I (→w is a possibly empty sequence of RecR1
applications followed by In application) or T 0 = µt.T 0 (→w is simply RecL
application).

The above procedure is not guaranteed to terminate when T ≤S, in particular
in those cases in which an infinite subtyping relation is needed to prove that
they are in subtyping. For instance, this happens for the cases discussed in the
examples reported in Section 2.3. We now show how to amend the procedure to
terminate at least in the restricted cases discussed above. The new algorithm is
defined by the same rules as before, plus a pair of rules presented below, where
we use judgements Σ ` T ≤t S instead of Σ ` T ≤a S.
Moreover, the new version of the algorithm requires to distinguish among
different instances of the same input branching. More precisely, due to multiple unfoldings we could have that the same input choice appears more than
once. For instance, given µt.&{l : t}, if we apply unfolding twice, we obtain
&{l : &{l : µt.&{l : t}}}. To distinguish different instances of the same input
branching, we assume to have an extended syntax in which such choices are

27

annotated: &α {l : S} denotes an input annotated with a symbol α taken from a
countable set of annotations. Annotations in the same term are assumed to be
pairwise distinct. In the example above, the decorated version of the unfolded
0
term is &α {l : &α {l : µt.&{l : t}}}, for a pair of distinct annotations α and α0 .
As multiple unfoldings can be applied only to the r.h.s. terms of the judgements
Σ ` T ≤t S, we will adopt the syntax extended with annotations only for such
terms.
Algorithmically, in order to have the guarantee that all the annotations
are pairwise distinct, we assume that they are all different in the initial term.
Namely, when we want to check whether T <<sout S or T <<sin S we assume
an annotation function ann(S) that annotates all the input choices in S with
pairwise distinct symbols, and we start the algorithm from the judgement ∅ `
T ≤t ann(S). Moreover, every time an unfolding is applied to the r.h.s. of a
judgement, the algorithm annotates with fresh symbols each added input choice.
Concerning annotations, we omit them when they are irrelevant. For instance, the rules in Figure 4 do not contain annotations, but are used any
way to define also the new algorithm (upon replacement of Σ ` T ≤a S with
Σ ` T ≤t S). The omission of the annotations means that the rules in that
figure can be applied to any annotated judgement Σ ` T ≤t S, to obtain a new
judgement Σ0 ` T 0 ≤t S 0 where the new annotated term S 0 inherits the annotations of S and in case new input branchings are present in S 0 (due to unfolding
in rules RecR1 and RecR2 ) these will be freshly annotated as discussed above.
We assume a function unann(S) that returns the same term but without annotations. We overload the function unann( ) to apply it also to an environment
Σ: unann(Σ) is the environment obtained by removing all annotations from the
r.h.s. of all of its pairs.
We are now ready to present the two additional rules, having the same higher
priority of Asmp:
l1 · · · lm

j > i s < |γ| l1 · · · ln = γ i · (l1 · · · ls )
= γ · (l1 · · · ls ) S ∈ {⊕, µ} & ∈ T unann(S) = unann(S 0 )
j

Σ, (T, &{l1 : . . . &α {lr : . . . &{ln : S} . . .} . . .}) `
T ≤t &α {l1 : . . . &{lm : S 0 } . . .}

Asmp2

S ∈ {⊕, µ}
& 6∈ T
n<m
unann(S) = unann(S 0 )
Asmp3
Σ, (T, &{l1 : . . . &{ln : S} . . .}) ` T ≤t &{l1 : . . . &{lm : S 0 } . . .}
Above S ∈ {⊕, µ} means that S starts with either an output selection or a
recursive definition, while & ∈ T requires the occurrence of at least one input
branching anywhere in the term T .
Intuitively, Asmp2 allows the algorithm to terminate when, after the judgement Σ ` T ≤t R, another judgement Σ0 ` T ≤t R0 is reached such that:
• both R and R0 start with a sequence of input branchings (respectively
labeled with l1 · · · ln and l1 · · · lm );
28

• the label sequences are repetitions of the same pattern, with the second
one strictly longer than the first one (namely, there exist γ, a proper prefix
l1 · · · ls of γ and j > i such that l1 · · · ln = γ i · (l1 · · · ls ) and l1 · · · lm =
γ j · (l1 · · · ls ));
• there exists lr in the initial input sequence of R having an annotation α
that coincides with the annotation of l1 in the initial input sequence of R0
(hence l1 = lr , n ≥ 1 and m ≥ 1)
• after such initial input branchings, both R and R0 continue with the same
term up to annotations (S and S 0 such that unann(S) = unann(S 0 )).
The algorithm can terminate in this case because otherwise it would continue
indefinitely by repeating the same steps performed between the judgements
Σ ` T ≤t R and Σ0 ` T ≤t R0 . During these steps the l.h.s. term T performs
a cycle including: the non-empty sequence of inputs l1 · · · lr−1 (due to the requirement above about the α annotation and the constraint & ∈ T in the rule
premise) that is a repetition of γ, which is matched by the initial part of the
input sequence in the r.h.s.; and a sequence of outputs, which is matched by the
final term S of the r.h.s. that, itself, performs a cycle. While performing this
cycle, S generates new input branchings that strictly extend the initial input
sequence.
The rule Asmp3 allows the algorithm to terminate in the case the potential
infinite repetition includes output selections only. In this case it is sufficient
to check that the l.h.s. cycles without consuming any inputs and that, after a
number of such cycles: the amount of initial accumulated inputs in the r.h.s.
strictly increases and the term after such accumulation performs, itself, a cycle.
Also for the new algorithm we use Σ ` T ≤t S →∗ Σ0 ` T 0 ≤t S 0 to denote
the application of one rule on the former judgement that generates the latter,
and Σ ` T ≤t S →err to denote that no rule can be applied to the judgement
Σ ` T ≤t S.
We now prove that the new algorithm terminates.
Lemma 5.2. Given two types T ∈ T out ∩ T in (resp. T ∈ T out ) and S ∈ T in
(resp. S ∈ T in ∩ T out ), the algorithm applied to initial judgement ∅ ` T ≤t ann(S)
terminates.
Proof. In this proof, we abstract away from the annotations of input actions,
i.e., we denote two types that differ only in the annotations with the same term.
We proceed by contraposition. Assume that there exist T and S such that
the algorithm starting from the initial judgement ∅ ` T ≤t S does not terminate.
Hence, there must exist an infinite sequence of rule applications Σ ` T ≤t S →
Σ1 ` T1 ≤t S1 → . . . → Σn ` Tn ≤t Sn → . . .. In this sequence, infinitely
many unfoldings of recursive definitions will be performed on infinitely many
traversed judgements Σ0 ` T 0 ≤t S 0 . All these pairs (T 0 , S 0 ) must be pairwise
distinct otherwise rule Asmp will be applied to terminate the sequence. This
implies that the environment Σ grows unboundedly in order to contain all these
infinitely many distinct pairs (T 0 , S 0 ).
29

We now prove that all such pairs (T 0 , S 0 ) are of the following form: (Tf ,
&{l1 : . . . &{ln : Sf } . . .}) where Tf and Sf belong to a finite set of terms. The
first term T 0 is obtained from the initial term T by means of consumptions of
initial inputs or outputs (rules In and Out), or single unfoldings of top level
recursive definitions (rules RecL). The set of terms that can be obtained in this
way from the finite initial term T is clearly finite. On the contrary, the second
group of terms S 0 could be obtained by application of different transformations:
in particular Out that allows for the anticipation of outputs prefixed by an
arbitrary sequence of inputs, and RecR2 that can unfold more than one recursive
definition at a time. Concerning the multiple unfoldings of RecR2 , we have that
the depth( ) function guarantees that recursive definitions guarded by an output
operation are never unfolded. In this way a subterm of S 0 prefixed by an output
is taken from a finite set of terms. Obviously, also the set of possible subterms
starting with a recursive definition is finite as well. As S 0 has only input singlechoices, we can conclude that it is of the form &{l1 : . . . &{ln : Sf } . . .} because
it starts with a (possibly empty) sequence of inputs followed by a term Sf ,
guarded by an output or a recursive definition, taken from a finite set.
As infinitely many distinct pairs (T 0 , S 0 ) are introduced in Σ, there are infinitely many distinct pairs having the same Tf and Sf . This guarantees the
existence of an infinite sequence
(Tf , &{l11 : . . . &{ln1 1 : Sf } . . .})
(Tf , &{l12 : . . . &{ln2 2 : Sf } . . .})
···
(Tf , &{l1v : . . . &{lnv v : Sf } . . .})
···
of pairs that are introduced in Σ in this order, and for which nv is strictly
growing.
If Tf does not contain input actions (i.e. & 6∈ Tf ) we have that the rule
Asmp3 could be applied when the second pair in the above sequence (Tf ,
&{l12 : . . . &{ln2 2 : Sf } . . .}) was introduced in Σ. As Asmp3 has priority, it is
necessary to apply this rule, thus terminating successfully the sequence of rule
applications. This contradicts the initial assumption about the infinite sequence
of rule applications.
Now, consider Tf that contains at least one input action. We separate this
case in two subcases: Tf ∈ T out ∩ T in and Tf ∈ T out .
In the first subcase, both inputs and outputs in Tf are single-choices. This
means that, by cycling, Tf performs indefinitely always the same sequence of
input branchings: let γ be the sequence of the corresponding labels. The inputs
accumulated on the r.h.s. term should be consistent, i.e. must have labels of
the form l1v · · · lnv v = γ i · ι, with ι prefix of γ. Consider now the final part ι
of the sequences l1v · · · lnv v that, as discussed above, are all prefixes of γ; as
the different prefixes of γ are finite, we have that there exists an infinite subsequence of pairs (Tf , &{l1v : . . . &{lnv v : Sf } . . .}) all having the same final ι.
Consider now maxIn as the maximal number of inputs between two subsequent

30

outputs in Sf (or its unfolding). We select from this infinite subsequence a
pair (Tf , &{l1k : . . . &{lnk k : Sf } . . .}) with nk > maxIn. We now consider the
subsequent pair in the subsequence (Tf , &{l1w : . . . &{lnww : Sf } . . .}) and the
corresponding sequence of rule applications:
Σk ` Tf ≤t &{l1k : . . . &{lnk k : Sf } . . .} →∗
Σw ` Tf ≤t &{l1w : . . . &{lnww : Sf } . . .}
Let l10 . . . lh0 be the labels of the outputs involved in applications of the rule Out.
Such outputs are present in Sf (and its unfoldings). Let &{l100 : . . . &{lg00 : S 0 } . . .}
(assuming S 0 ∈ {⊕, µ}) be the term obtained from Sf by (unfolding the term
and) consuming the outputs labeled with l10 . . . lh0 . We have that S 0 = Sf . We
conclude considering two possible cases: g ≤ |ι| and g > |ι|.
• If g ≤ |ι|, we have that all the applications of the rule In involve inputs
that are already present in the initial sequence of inputs of the r.h.s. in
(Tf , &{l1k : . . . &{lnk k : Sf } . . .}). This guarantees that it is possible to
apply on the judgement Σf ` Tf ≤t &{l1w : . . . &{lnww : Sf } . . .} the rule
Asmp2. As Asmp2 has priority it is necessary to apply this rule thus terminating successfully the sequence of rule applications. This contradicts
the initial assumption about the infinite sequence of rule applications.
• If g > |ι|, we have that l100 . . . lg00 = ι0 · γ y · ι with ι · ι0 = γ. From the
infinite subsequence we select a pair (Tf , &{l1r : . . . &{lnr r : Sf } . . .}) such
that nr − |ι| is greater than the number of applications of the rule In in
the sequence of rule applications:
Σk ` Tf ≤t &{l1k : . . . &{lnk k : Sf } . . .} →∗
Σw ` Tf ≤t &{l1w : . . . &{lnww : Sf } . . .}
Consider now the same sequence of rule applications starting from the
judgement Σr ` Tf ≤t &{l1r : . . . &{lnr r : Sf } . . .} that introduced (Tf ,
&{l1r : . . . &{lnr r : Sf } . . .}) in the environment. Let
Σq ` Tf ≤t &{l1q : . . . &{lnq q : S 00 } . . .}
be the reached judgement. We have that on this judgement it is possible
to apply Asmp2 because S 00 = Sf and l1q . . . lnq q = γ u · ι · ι0 · γ y · ι. As
discussed in the previous case this contradicts the initial assumption on
the infinite sequence of rule applications.
It remains the final subcase Tf ∈ T out . In this case we have Sf ∈ T in ∩ T out .
As Tf has outputs with single-choice, the rule In will be applied at least once
in the sequence of rule applications between every pair and the subsequent
one. For this reason, it is not restrictive to assume that in all the pairs (Tf ,
&{l1v : . . . &{lnv v : Sf } . . .}) the inputs labeled with l1v · · · lnv v are produced by
previous unfoldings of the same term Sf . As in Sf all the inputs and outputs
are single-choice, there is a predefined sequence of inputs within a cycle from Sf
to Sf again. Let η be the sequence of the labels corresponding to such inputs.
Then we have that the inputs accumulated on the l.h.s. term, labeled with the
sequence of labels l1v · · · lnv v , will be such that l1v · · · lnv v = ρη i , for some ρ suffix
of η. We consider a suffix ρ because during the execution of the algorithm some
previously accumulated input will be consumed to mimick inputs of the l.h.s.
31

term, and ρ represents the part of inputs that have been left from a sequence ρ
that has been only partially consumed. As the suffixes of η are finite, we can
extract an infinite subsequence of pairs that always consider the same suffix ρ.
Namely, for all the pairs, the second term has an initial sequence of inputs with
a sequence of labels belonging to ρη ∗ , for the same ρ. But as ρ is a suffix of η
there exists a rotation γ 0 of η such that all the sequences belong to γ 0∗ ρ0 with
ρ·ρ0 = η. Hence all the sequences l1v · · · lnv v are of the form γ 0i ·ρ0 . By considering
γ = γ 0 and ι = ρ0 we can now conclude with the same arguments used in the
previous subcase.

We now move to the proof of soundness of the algorithm.
Lemma 5.3. Given two types T ∈ T out ∩ T in (resp. T ∈ T out ) and S ∈ T in
(resp. S ∈ T in ∩ T out ), we have that ∅ ` T ≤a S →∗ Σ0 ` T 0 ≤a S 0 →err if and
only if ∅ ` T ≤t ann(S) →∗ Σ00 ` T 00 ≤t S 00 →err .
Proof. We consider the two implications separately starting from the if part.
Assume that ∅ ` T ≤t ann(S) →∗ Σ00 ` T 00 ≤t S 00 →err . In this sequence
of rule applications, the new rules Asmp2 and Asmp3 are never used otherwise the sequence terminates successfully by applying such rules. Hence, by
applying the same sequence of rules, we have ∅ ` T ≤a S →∗ Σ0 ` T 0 ≤a S 0
with T 00 = T 0 , unann(S 00 ) = S 0 and unann(Σ00 ) = Σ0 . We have that Σ0 `
T 0 ≤a S 0 →err , otherwise if a rule could be applied to this judgement, the same
rule could be applied also to Σ00 ` T 00 ≤t S 00 thus contradicting the assumption
Σ00 ` T 00 ≤t S 00 →err .
We now move to the only if part. Assume the existence of the sequence
of rule applications ρa = ∅ ` T ≤a S →∗ Σ0 ` T 0 ≤a S 0 →err . As the algorithm for ∅ ` T ≤t ann(S) considers a superset of rules, we have two possible
cases: either ∅ ` T ≤t ann(S) →∗ Σ00 ` T 00 ≤t S 00 →err by applying the same
sequence of rules, or during the application of this sequence of rules, starting
from ∅ ` T ≤t ann(S), a judgement is reached on which one of the additional rules Asmp2 or Asmp3 can be applied. Namely, there exists a sequence
ρt = ∅ ` T ≤t ann(S) →∗ Σe ` Te ≤t Se , corresponding to a prefix of ρa , such
that either Asmp2 or Asmp3 can be applied on the judgement Σe ` Te ≤t Se . We
conclude the proof by showing that this second case never occurs. We discuss
only Asmp2, as the case for Asmp3 is treated similarly.
If ∅ ` T ≤t S →∗ Σe ` Te ≤t Se and Asmp2 can be applied to Σe ` Te ≤t Se ,
there exists an intermediary judgement Σs ` Ts ≤t Ss , traversed during such sequence of rule applications, that introduces in the environment the pair (Ts , Ss )
used in the above application of the rule Asmp2. Hence ρt has a suffix
Σs ` Ts ≤t Ss →∗ Σe ` Te ≤t Se with:
• Ts = Te ,
• Ss = &{l1 : . . . &{ln : R} . . .} and Se = &{l1 : . . . &{lm : R0 } . . .} with
unann(R) = unann(R0 ), l1 · · · ln = γ i · (l1 · · · ls ), l1 · · · lm = γ j · (l1 · · · ls ) for
i < j and s < |γ|;

32

• during the entire sequence Σs ` Ts ≤a Ss →∗ Σe ` Te ≤a Se only a prefix
l1 · · · lr−1 of the input actions l1 · · · ln is consumed from Ss .
Let Σ0s = unann(Σs ), Ss0 = unann(Ss ), Σ0e = unann(Σe ), and Se0 = unann(Se ).
As ρt corresponds to a prefix of ρa we have that ρa =
∅ ` T ≤a S →∗ Σ0s ` Ts ≤a Ss0 →∗ Σ0e ` Te ≤a Se0 →∗ Σ0 ` T 0 ≤a S 0 →err
This is not possible because we now show that after the sequence Σ0s ` Ts ≤a Ss0
→∗ Σ0e ` Te ≤a Se0 , it is not possible to reach any judgement Σ0 ` T 0 ≤a S 0 such
that Σ0 ` T 0 ≤a S 0 →err . On the basis of the observations listed above we have:
• Ts = Te ,
• Ss0 = &{l1 : . . . &{ln : R} . . .}, Se0 = &{l1 : . . . &{lm : R} . . .} with l1 · · · ln =
γ i · (l1 · · · ls ), l1 · · · lm = γ j · (l1 · · · ls ) for i < j and s < |γ|;
• during the entire sequence Σ0s ` Ts ≤a Ss0 →∗ Σ0e ` Te ≤a Se0 only a prefix
l1 · · · lr−1 of the input actions l1 · · · ln is consumed from Ss0 .
We have that the sequence of rules applied in Σ0s ` Ts ≤a Ss0 →∗ Σ0e ` Te ≤a Se0 is
the unique one that can be applied also to the ending judgement Σ0e ` Te ≤a Se0 .
This is guaranteed by the fact that we are considering single-choice subtyping,
the correspondence of the terms Ts = Te , the availability of the input actions
labeled with l1 · · · lr−1 in Se0 , and the fact that both Ss0 and Se0 have the same
term R at the end of their initial input actions. Consider now the judgement
Σ00e ` Te0 ≤a Se00 reached at the end of such sequence, i.e. Σ0e ` Te ≤a Se0 →∗
Σ00e ` Te0 ≤a Se00 . We have that the same properties listed above hold also for the
new sequence Σ0e ` Te ≤a Se0 →∗ Σ00e ` Te0 ≤a Se00 :
• Te = Te0 , because the same transformations are applied to the l.h.s. terms
by the rules that are applied.
• Se0 = &{l1 : . . . &{lm : R} . . .} and Se00 = &{lv : . . . &{lm : R} . . .} with
l1 · · · lm = γ j · (l1 · · · ls ) and l1 · · · lv = γ (j+(j−i)) · (l1 · · · ls ), where i is
the number of the repetitions of γ in the initial r.h.s. term Ss0 , hence
j − i is the number of new repetitions of γ added during the sequence
of rule applications. From the previous properties we have j > i, hence
j < j + (j − i), and s < |γ|.
• During the entire sequence Σ0e ` Te ≤a Se0 →∗ Σ00e ` Te0 ≤a Se00 only a prefix
l1 · · · lr−1 of the input actions l1 · · · lm is consumed from Se0 .
As these properties continue to hold, we have that the sequence of rules applied
in Σ0e ` Te ≤a Se0 →∗ Σ00e ` Te0 ≤a Se00 can be continued to be applied indefinitely, hence it is not possible to reach any judgement Σ0 ` T 0 ≤a S 0 such that
Σ0 ` T 0 ≤a S 0 →err .

We can finally conclude with the following theorem that states decidability
for more general versions of <<sin and <<sout , where we do not impose related
types to belong to T noinf .

33

Theorem 5.1 (Algorithm Correctness). Given two types T ∈ T out ∩ T in
(resp. T ∈ T out ) and S ∈ T in (resp. S ∈ T in ∩ T out ), we have that ∅ ` T ≤t ann(S)
if and only if T ≤ S.
Proof. It follows immediately from Lemma 5.1, Lemma 5.2 and Lemma 5.3. 
As an obvious consequence of algorithm correctness, we have that the two
relations <<sout and <<sin are decidable.
Corollary 5.1. The asynchronous single-choice output relation <<sout and the
asynchronous single-choice input relation <<sin are decidable.
Proof. In order to verify whether T <<sin S it is sufficient to check that T ∈
T in ∩ T out ∩ T noinf and S ∈ T in ∩ T noinf and then verify whether T ≤ S, which
is decidable for terms belonging to these sets as proved in Theorem 5.1. For
T <<sout S it is possible to proceed in the same way with the only difference that
the check is whether T ∈ T out ∩ T noinf and S ∈ T in ∩ T out ∩ T noinf .

Notice that with respect to the general case, when our algorithm is applied
to the restricted case of <<sout and <<sin , rule Asmp3 and premise & ∈ T of
rule Asmp2 become useless. This follows from the fact that types in T noinf never
satisfy the premises of Asmp3 and always satisfy the premise & ∈ T of rule
Asmp2.
6. Conclusion and Related Work
Related Work. Lange and Yoshida [10] have independently and simultaneously
provided an undecidability result for a class of communicating automata called
asynchronous duplex systems (which are shown to correspond to a class of binary session types). They prove that automata compatibility (checking whether
two automata in parallel can safely interact) is undecidable and then show that
such result makes also asynchronous session types subtyping undecidable. Their
proof consists of an encoding of the termination problem for Turing machines
(rather than our simpler and direct encoding based on queue machines) into
deciding automata compatibility. Most importantly, in order to prove undecidability of a subtyping , a translation M from types to automata is used which
exploits the following result (Theorem 5.1, [10]):
Given two types T and S, we have that T  S if and only if M(T )
is compatible with M(S).
Above, S is the dual of S, the type obtained from S by inverting inputs (outputs)
with outputs (inputs). As compatibility between communicating automata is
a symmetric relation, we have that this approach to prove undecidability of
subtyping can be applied only to dual closed relations , i.e., T  S if and
only if S  T . Among all the subtyping relations in the literature (discussed
in details in Section 4), this property holds only for the definition of subtyping
by Chen et al. [2], where orphan messages are not admitted. For instance, we
have that the type µt. ⊕ {l : t} is a subtype of µt.&{l0 : ⊕{l : t}} but obviously
34

µt. ⊕ {l0 : &{l : t}} is not a subtype of µt.&{l : t}. Moreover, differently
from Lange and Yoshida [10] we show that, to get undecidability, it is sufficient
to consider a restricted version of asynchronous binary session subtyping (<<
relation) that is much less expressive and that cannot be further simplified by
imposing limitations on the branching/selection structure of types (otherwise it
becomes decidable). As shown, this has one plain advantage: it allowed us to
easily show undecidability of various existing subtyping relations.
Concerning decidability, Lange and Yoshida [10] independently and simultaneously proved a result similar to ours (Theorem 5.1). They present an algorithm for deciding subtyping between types T and S, with one between T and
S being a single-choice session type (i.e. a type where every branching/selection
has a single choice) and the other one being a general (any) session type. In
particular, they consider a dual closed subtyping relation defined following the
orphan-message free approach by Chen et al. [2]. On the other hand, we show
(Theorem 5.1) T ≤ S to be decidable when: one between T and S is a singlechoice session type (as for Lange and Yoshida) and the other one is either a type
with single outputs, if it is T , or a type with single inputs, if it is S. We first notice that our ≤ relation is more general with respect to the one used by Lange
and Yoshida in that it does not include the orphan message free constraint.
Moreover, although it may seem that Lange and Yoshida can effectively relate
types that do not fall under our (more restricted) syntactical characterization,
covariance and contravariance prevent any type containing at least one nonsingle input branch and one non-single output selection (both reachable in the
subtyping simulation game) to be related with a single-choice type. We finally
observe that since, differently from the relation used by Lange and Yoshida, our
≤ relation is not dual closed, we need to explicitly carry out two separate proofs
for the two cases of T ≤ S: one where the single-choice session type is T and
another one where it is, instead, S.
Conclusion. We have proven that asynchronous subtyping for session types is
undecidable. Moreover, we have shown that subtyping becomes decidable if we
put some restrictions on the branching/selection structure. As future work, we
plan to search for alternative subtyping relations that enjoy properties similar
to ≤, but are decidable.
References
References
[1] D. Mostrous, N. Yoshida, Session typing and asynchronous subtyping for
the higher-order π-calculus, Inf. Comput. 241 (2015) 227–263.
[2] T. Chen, M. Dezani-Ciancaglini, N. Yoshida, On the preciseness of subtyping in session types, in: 16th International Symposium on Principles and
Practice of Declarative Programming (PPDP’14), ACM, 2014, pp. 135–146.

35

[3] D. Mostrous, N. Yoshida, K. Honda, Global principal typing in partially
commutative asynchronous sessions, in: 18th European Symposium on Programming (ESOP’09), Vol. 5502 of LNCS, Springer, 2009, pp. 316–332.
[4] K. Honda, V. T. Vasconcelos, M. Kubo, Language primitives and type discipline for structured communication-based programming, in: 7th European
Symposium on Programming (ESOP’98), Vol. 1381 of LNCS, Springer,
1998, pp. 122–138.
[5] K. Honda, N. Yoshida, M. Carbone, Multiparty asynchronous session types,
J. ACM 63 (1) (2016) 9.
[6] S. J. Gay, M. Hole, Subtyping for session types in the pi calculus, Acta Inf.
42 (2-3) (2005) 191–225.
[7] D. Mostrous, Session types in concurrent calculi: Higher-order processes
and objects, Ph.D. thesis, Department of Computing, Imperial College of
Science, Technology and Medicine (2009).
[8] D. Kozen, Automata and computability, Springer, New York, 1997.
[9] D. Brand, P. Zafiropulo, On communicating finite-state machines, Journal
of the ACM 30 (2) (1983) 323–342.
[10] J. Lange, N. Yoshida, On the undecidability of asynchronous session subtyping, in: 20th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2017), Vol. 10203 of Lecture
Notes in Computer Science, 2017, pp. 441–457.

36

