On the Boundary between Decidability and Undecidability of Asynchronous Session Subtyping
Mario Bravetti, Marco Carbone, Gianluigi Zavattaro
TL;DR
This paper explores the boundary between decidability and undecidability in asynchronous session subtyping, identifying a more applicable decidable fragment without buffer limitations or restrictions on multiple choices.
Contribution
It introduces the first decidable fragment of asynchronous session subtyping that allows unlimited buffers and multiple choices, expanding practical applicability.
Findings
Decidability achieved without buffer size restrictions.
Undecidability persists even with covariance and contravariance restrictions.
Identifies the boundary between decidable and undecidable subtyping fragments.
Abstract
Session types are behavioural types for guaranteeing that concurrent programs are free from basic communication errors. Recent work has shown that asynchronous session subtyping is undecidable. However, since session types have become popular in mainstream programming languages in which asynchronous communication is the norm rather than the exception, it is crucial to detect significant decidable subtyping relations. Previous work considered extremely restrictive fragments in which limitations were imposed to the size of communication buffer (at most 1) or to the possibility to express multiple choices (disallowing them completely in one of the compared types). In this work, for the first time, we show decidability of a fragment that does not impose any limitation on communication buffers and allows both the compared types to include multiple choices for either input or output, thus…
Click any figure to enlarge with its caption.
Figure 1Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Distributed systems and fault tolerance · Security and Verification in Computing
On the Boundary between Decidability and
Undecidability of Asynchronous Session Subtyping
Mario Bravetti
University of Bologna, Department of Computer Science and Engineering / INRIA FOCUS
Marco Carbone
Department of Computer Science, IT University of Copenhagen
Gianluigi Zavattaro
University of Bologna, Department of Computer Science and Engineering / INRIA FOCUS
Abstract
Session types are behavioural types for guaranteeing that concurrent programs are free from basic communication errors. Recent work has shown that asynchronous session subtyping is undecidable. However, since session types have become popular in mainstream programming languages in which asynchronous communication is the norm rather than the exception, it is crucial to detect significant decidable subtyping relations. Previous work considered extremely restrictive fragments in which limitations were imposed to the size of communication buffer (at most 1) or to the possibility to express multiple choices (disallowing them completely in one of the compared types). In this work, for the first time, we show decidability of a fragment that does not impose any limitation on communication buffers and allows both the compared types to include multiple choices for either input or output, thus yielding a fragment which is more significant from an applicability viewpoint. In general, we study the boundary between decidability and undecidability by considering several fragments of subtyping. Notably, we show that subtyping remains undecidable even if restricted to not using output covariance and input contravariance.
keywords:
Session Types , Asynchronous Subtyping , Undecidability
††journal: Journal of LaTeX Templates
1 Introduction
Session types [1, 2] are types for controlling the communication behaviour of processes over channels. In a very simple but effective way, they express the pattern of sends and receives that a process must perform. Since they can guarantee freedom from some basic programming errors, session types are becoming popular with many main stream language implementations, e.g., Haskell [3], Go [4] or Rust [5].
As an example, consider a client that invokes service operations by following the protocol expressed by the session type
[TABLE]
indicating that the client decides whether to call operation or and then waits for receiving the corresponding response ( or , respectively). For the sake of simplicity we consider session types where (the type of) communicated data is abstracted away. The symmetric behaviour of the service is represented by the complementary (so-called dual) session type
[TABLE]
indicating that the server receives the call to operation or and then sends the corresponding response ( or , respectively).
We call output selection the construct . It is used to denote a point of choice in the communication protocol: each choice has a label and a continuation . 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 which operation to call. Symmetrically, we call input branching the construct . 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 selected operation.111In session type terminology [1, 6], the output selection/input branching constructs are usually simply called selection/branching; we call them output selection/input branching because we consider a simplified syntax for session types in which there is no specific separate construct for sending one output/receiving one input. Anyway, such output/input types can be seen as an output selection/input branching with only one choice.
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, the client can be safely replaced by another one with session type
[TABLE]
indicating that it can call only one specific service operation. But also the service can be safely replaced by another one accepting an additional operation:
[TABLE]
Subtyping relations have been formally defined for session types, e.g., by Gay and Hole [7] and Chen et al. [8], in order to precisely capture this safe replacement notion. For instance, a subtyping relation like that of Gay and Hole [7] (denoted by ), where processes are assumed to simply communicate via synchronous channels222Here, we focus on the so-called process-oriented subtyping, as opposed to channel-based subtyping [9]., would imply, for the client, that:
[TABLE]
according to the so-called output covariant property, while, for the server
[TABLE]
according to the so-called input contravariant property.
When processes communicate via asynchronous channels, a more generous notion of subtyping like that of Chen et al. [8] can be considered. E.g., a process using an asynchronous channel to call a service operation, that receives the corresponding response and then sends a huge amount of data (requiring heavy computation), could be safely replaced by a more efficient one that computes and sends all the data immediately without waiting for the response:
[TABLE]
Intuitively, this form of asynchronous subtyping reflects the possibility to anticipate the output of the huge data w.r.t. to the input of the response because such data are stored in a buffer waiting for their reader to consume them.
1.1 Previous Results
Recently, Bravetti et al. [10] and Lange and Yoshida [11] have independently shown that asynchronous subtyping (the subtyping relation with output anticipation) is undecidable. In particular, in Bravetti et al., this is done by showing undecidability of the much simpler single-choice relation that is defined as a restriction of asynchronous subtyping where related types are such that: all output selections in have a single choice (output selections are covariant, thus is allowed have output selections with multiple choices) and all input branchings in have a single choice (input branchings are contravariant, thus is allowed to have input branchings with multiple choices). Moreover, those papers prove decidability for very small fragments of the asynchronous subtyping relation: the most significant one basically requires one of the two compared types to be such that all its input branchings and output selections have a single choice. In particular, in Bravetti et al. this is done by showing decidability of the two relations (single-choice input ) and (single-choice output ), both defined as further restrictions of where for related (, resp.) types we additionally require that: all input branchings (output selections, resp.) in and have a single choice. Other decidable fragments, considered by Lange and Yoshida, pose limitations on the communication behaviour that causes communication buffers to store at most one message, or they are used in half duplex modality (messages can be sent in one direction, only if the buffer for the opposite direction has been emptied). Although asynchronous subtyping is undecidable, it is important to reason about more significant cases for which such a relation is decidable. This because session types have become popular in mainstream programming languages, and, in such cases, asynchronous communications are the norm rather than the exception.
1.2 Contributed Results
The aim of this paper is to detect significant decidable fragments of asynchronous session subtyping and to establish a more precise boundary between decidability and undecidability. In particular, concerning decidability, as discussed above, the few decidable fragments of asynchronous subtyping known so far are extremely restrictive: our relations , [10] and the decidable relations considered by Lange and Yoshida [11]. Here, for the first time, we show decidability of a fragment that does not impose any limitation on communication buffers and allows both the subtype and the supertype to include multiple choices (either for input branchings or for output selections), thus opening the possibility for some practical applicability in restricted specific scenarios (e.g. session types for clients/services in web-service systems, see below). More precisely, while (, resp.), being it defined as a restriction of , admits multiple choices only for output selections in the supertype (input branchings in the subtype, resp.), here we consider and show decidability for a much larger relation, we denote by (, resp.). Such a relation is defined as the restriction of the whole relation (instead of the relation), where, in related types, all input branchings (output selections, resp.) must have a single choice. Therefore, differently from (, resp.), in (, resp.) both the subtype and the supertype can include multiple choices for output selections (for input branchings, resp.). The combination of non restricted buffers and presence of multiple choices on both related types requires a totally new approach for guaranteeing the termination of the subtyping algorithm (both for the termination condition itself and for the related decidability proof). For instance, if multiple choices are admitted for input branchings, the termination condition has to deal with complex recurrent patterns to be checked on the leafs of trees representing input branchings (with multiple choices), instead of detecting simple repetitions on strings representing sequences of single-choice inputs (as in previous work [10, 11]).
Concerning undecidability, all previous results [10, 11] exploit the capability of asynchronous subtyping of matching input branchings/output selections by means of covariance/contravariance. We here show that asynchronous subtyping remains undecidable even if we restrict it by disallowing this feature. As asynchronous subtyping is based on the combination of output covariance/input contravariance and output anticipation deriving from asynchronous communication, our result means that (provided that the syntax of types is not constrained) the source of undecidability is to be precisely localized into the output anticipation capability. The undecidability proof has a structure similar to that of Bravetti et al. [10], where the termination problem for queue machines, a well-known Turing-equivalent formalism, is encoded into asynchronous session subtyping. However, differently from Bravetti et al. [10], not having covariance/contravariance makes it impossible to encode queue machines deterministically. As we will see, the need to cope with nondeterminism makes it necessary to restrict the class of encodable queue machines to a new ad-hoc fragment that we introduce in this paper and we prove being Turing-equivalent: single consuming queue machines. Moreover a much more complex encoding, that uses nondeterminism, must be adopted.
In general, the contribution of this work is to analyze restrictions of asynchronous subtyping and classifying them into decidable and undecidable fragments. More precisely, as detailed in the following, we focus on two kinds of restrictions of asynchronous subtyping: limitations to the branching/selection structure and to the communication buffer, giving rise to the numerous relations shown in the lefthand part and righthand part of Figure 1, respectively (see Section 2 for formal definitions of all the relations). The relations are depicted as a lattice according to their inclusion as sets of pairs. Notice that decidability/undecidability is not logically related to set inclusion (e.g. the emptyset and the set of all pairs are both decidable and are the bottom and the top of the lattice).
Concerning asynchronous subtyping itself, we consider the orphan message free notion of subtyping introduced in Chen et al. [8]: it is commonly recognized that a convenient notion of asynchronous subtyping should prevent existence of messages that remain “orphan”, i.e. that are never consumed from the communication buffer. Operationally, this implies that inputs in the supertype cannot be indefinitely delayed by output anticipation: eventually such inputs must be performed by the subtype so to correspondingly consume messages from the buffer. As a side result, in this paper we introduce a new, elegant, way of defining orphan message free asynchronous subtyping. The new definition is based on just adding a constraint about closure under duality to the standard (non orphan message free) coinductive definition of asynchronous subtyping [12]. We thus use such a novel approach based on dual closeness to give a concise definition of asynchronous subtyping: we call the obtained relation. We then show (also included in Figure 1) to be equal to orphan message free subtyping of Chen et al. [8]. We also show that the most significant decidable and undecidable fragments of , i.e. the relation and subtyping without covariance/contravariance, are dual closed subtyping relations according to our new definition.
Limitations to the branching/selection structure. We limit the asynchronous subtyping capability of managing input branchings/output selections, giving rise to the subtyping relations shown in the lefthand part of Figure 1, as follows:
requiring that in both the subtype and the supertype output selections (input branchings, resp.) have a single choice: in this case the (, resp.) subscript is added to ;
- 2.
requiring that each output selection (input branching, resp.) performed by the subtype is matched by an output selection (input branching, resp.) performed by the supertype with the exactly the same total set of labels, i.e. output covariance (input contravariance, resp.) is not admitted: in this case the (, resp.) subscript is added to .
We now summarize our decidability/undecidability results for these relations.
Decidability of asynchronous subtyping for single-in types () or single-out types (). We consider the class of single-in (single-out, resp.) session types, i.e. types where all output selections (input branchings, resp.) have a single choice. We present and prove correct an algorithm for deciding whether two single-out (resp. single-in, by exploiting the closure under duality property) types are in the subtyping relation. From a modeling viewpoint, assuming binary sessions to happen between a single-in and a single-out party, this entails that internal decisions are taken by the single-in party, while the single-out one passively accepts them. This kind of behaviour can occur in, e.g., web-service systems where a client internally chooses a request-response operation [13] and then waits for a corresponding (non branching) input, while the server accepts invocations on several operations but then it reacts by answering on a related response channel (independently of the actual returned data/error); see the examples at the beginning of this Introduction section. Our algorithms for subtyping of single-out/single-in types could thus be used in typing systems for server/client code. With minor variants to the machinery introduced to show decidability of and , we also show that , and are decidable.
- 2.
*Undecidability of Asynchronous Subtyping without Output Covariance and Input Contravariance ().
- As discussed above, subtyping for session types makes use of output covariance and input contravariance: an output is a subtype of an output with more labels , for ; and an input is a subtype of an input with less labels , for . Existing results on the undecidability of asynchronous subtyping exploit its capability of relating types with a different number of branches. We consider a restricted form of subtyping, the relation, which disallows this feature, i.e. which does not use output covariance and input contravariance. We show that, also with such a restriction, subtyping remains undecidable by encoding the termination problem for single consuming queue machines, a Turing-equivalent formalism that (as already explained) we introduce on purpose, into . The same encoding we use for shows also undecidability of , and (thus also providing an alternative proof for the undecidability of with respect to those by Bravetti et al. [10] and Lange and Yoshida [11]).
Limitations to the communication buffer. We limit the communication buffer capability, giving rise to the subtyping relations shown in the righthand part of Figure 1, by restricting the capability of to anticipate outputs: this is equivalent to putting an upper limit to communication buffers between two parties, a common fact in practice. In this context our decidability/undecidability results are the following ones.
Decidability of -bounded Subtyping (), with . In -bounded asynchronous subtyping we restrict the capability of to anticipate outputs: they can only be anticipated w.r.t. a number of inputs that is less or equal to . We give and prove correct an algorithm for deciding whether any two session types are in a -bounded subtyping relation. Notice that, in the case we obtain synchronous subtyping [7]. Moreover, if we consider we have a notion of subtyping along the lines of that, we already mentioned, obtained by Lange and Yoshida [11] imposing restrictions on the communication behaviour.
- 2.
Undecidability of Bounded Asynchronous Subtyping (). We say that a pair of session types is in bounded asynchronous subtyping relation if there exists a such that such pair is in -bounded subtyping relation. Bounded asynchronous subtyping relates types that do not unboundedly put messages in a buffer. For instance, the types
[TABLE]
[TABLE]
are related by asynchronous subtyping but not by bounded asynchronous subtyping: the augmented data production frequency of the subtype requires to store an unbounded amount of huge data. Since in practice buffers are bounded, this could have been an acceptable candidate notion for replacing standard asynchronous subtyping, however we prove that it is undecidable as well. We do this by showing undecidability of a property for queue machines: bounded non termination.
Outline. In Section 2 we present session types and definition of asynchronous subtyping , the novel dual closed reformulation , the fragments of shown in Figure 1 and a discussion about their properties. Section 3 presents all decidability results, notably for -bounded subtyping () and for subtyping over single-in types () and over single-out types (). Section 4 presents all undecidability results, notably for bounded subtyping () and for subtyping without output covariance and input contravariance (). Section 5 discusses related work and Section 6 presents concluding remarks. Detailed proofs of theorems, lemmas and propositions can be found in the Appendix. We chose to put proof technicalities, that often include additional definitions and intermediate results, in the Appendix so not to disrupt the paper prose.
2 Session Types and Asynchronous Subtyping
We begin by formally introducing the various ingredients needed for our technical development.
We start with the formal syntax of binary session types. Similarly to Chen et al. [8] we do not use a dedicated construct for sending an output/receiving an input, we instead represent outputs and inputs directly inside choices. More precisely, we consider output selection , expressing an internal choice among outputs, and input branching , expressing an external choice among inputs. Each possible choice is labeled by a label , taken from a global set of labels , followed by a session continuation . Labels in a branching/selection are assumed to be pairwise distinct.
Definition 2.1** (Session Types)**
Given a set of labels , ranged over by , the syntax of binary session types is given by the following grammar:
[TABLE]
A session type is single-out if, for all of its subterms , . Similarly, a session type is single-in if, for all of its subterms , .
In the sequel, we leave implicit the index set in input branchings and output selections when it is already clear from the denotation of the types. Note also that we abstract from the type of the message that could be sent over the channel, since this is orthogonal to our theory. Types and denote standard tail recursion for recursive types. We assume recursion to be guarded: in , the recursion variable occurs within the scope of an output or an input type. In the following, we will consider closed terms only, i.e., types with all recursion variables occurring under the scope of a corresponding definition . Type denotes the type of a channel that can no longer be used.
In our development, it is crucial to count the number of times we need to unfold a recursion . This is formalised by the following function:
Definition 2.2** (-unfolding)**
[TABLE]
The definition of asynchronous subtyping uses the notion of input context, a type context consisting of a sequence of inputs preceding holes where types can be placed:
Definition 2.3** (Input Context)**
*An input context is a session type with multiple holes defined by the syntax: .
An input context is well-formed whenever all its holes , with , are consistently enumerated, i.e. there exists such that includes one and only one for each . Given a well-formed input context with holes indexed over and types ,…, , we use to denote the type obtained by filling each hole in with the corresponding term .*
From now on, whenever using input contexts we will assume them to be well-formed, unless otherwise specified.
For example, consider the input context
[TABLE]
we have:
[TABLE]
We start by considering the standard notion of asynchronous subtyping given by Chen et al. [8]. We choose it because of its orphan message free property that is commonly recognized to be convenient: only subtypes are allowed that do not cause incoming messages to remain “orphan” (because they are never consumed from the communication buffer). In the definition of asynchronous subtyping given by Chen et al., orphan message freedom causes a specific dedicated constraint to be included (which is, e.g., instead not present in the asynchronous subtyping definition by Mostrous and Yoshida [12]). We now formally present the asynchronous subtyping relation , rephrased w.r.t. that of Chen et al. [8] in a technical format that is convenient for showing our results, which follows a coinductive simulation-like definition.
Definition 2.4** (Asynchronous Subtyping, )**
* is an asynchronous subtyping relation if implies that:*
if then such that ; 2. 2.
if then such that
- (a)
,
- (b)
,
- (c)
* and*
- (d)
if then (no orphan message constraint); 3. 3.
if then such that , and ; 4. 4.
if then .
where with “” we mean that contains at least an input branching. is an asynchronous subtype of , written , if there is an asynchronous subtyping relation such that .
Intuitively, two types and are related by , whenever is able to simulate , but with a few twists: type is allowed to anticipate outputs nested in its syntax tree (asynchrony); and, output and input types enjoy covariance and contravariance, respectively. Moreover, the above definition includes the no orphan message constraint [8], namely: we allow the supertype inputs to be delayed only if also the subtype contains some input.
A synchronous subtyping relation like that of Gay and Hole [7] is obtained by requiring that, in item 2. of the above Definition 2.4, it always holds .
Example 2.5
Consider and . We have because the following is an asynchronous subtyping relation:
[TABLE]
Note that the relation contains infinitely many pairs that differ in the sequence of inputs, alternatively labeled with and , that are accumulated at the beginning of the r.h.s. type.
We now introduce an alternative way of defining orphan message free asynchronous subtyping, which is more elegant/concise: it obtains the orphan message freedom property by requiring closure under duality of the type relation being defined instead of making use of an explicit orphan message free constraint as in Definition 2.4.
For session types, we define the usual notion of duality: given a session type , its dual is defined as: , , , , and . In the sequel, we say that a relation on session types is dual closed if implies .
Definition 2.6** (Asynchronous Dual Closed Subtyping,
)**
* is an asynchronous dual closed subtyping relation whenever it is dual closed and implies , , and of Definition 2.4, plus a modified version of where the last constraint (the no orphan message constraint) is removed.*
* is an asynchronous dual closed subtype of , written , if there is an asynchronous dual closed subtyping relation such that .*
We observe that our definition is formally different from the ones found in literature. In particular, with respect to that by Mostrous and Yoshida [12], it additionally requires the subtyping relation to be dual closed. Below, we state that the dual closeness requirement is equivalent to imposing the orphan message free constraint, i.e. the last item of condition 2 in Definition 2.4 (both guarantee orphan-message freedom):
Theorem 2.7
Given two session types and , we have if and only if .
2.1 Subtyping Relation Restrictions
As already discussed in the Introduction, we focus on two kinds of restrictions of asynchronous subtyping: limitations to the branching/selection structure and to the communication buffer, giving rise to the numerous relations shown in the lefthand part and righthand part of Figure 1, respectively.
We now define fragments of obtained by posing limitations to the branching/selection structure.
Definition 2.8
Restrictions of the asynchronous subtyping relation are denoted by adding subscripts to the notation, with the following meaning:
whenever we add subscript (, resp.) we additionally require in Definition 2.4 both and to be single-out (single-in, resp.),
- 2.
whenever we add subscript (, resp.) we additionally require in Definition 2.4 in point 2. (* in point 3., resp.).*
The latter means that each output selection (input branching, resp.) performed by the subtype is matched by an output selection (input branching, resp.) performed by the supertype with the exactly the same total set of labels, i.e. output covariance (input contravariance, resp.) is not admitted.
Notice that, while it holds that , not all fragments of are asynchronous dual closed subtyping relations. For instance this does not hold for , , and , which perform a limitation, but not its “dual” one. It holds, instead, for the following two relations that we will show to be in the boundary between decidability and undecidability.
Proposition 2.9
The relation and the relation are asynchronous dual closed subtyping relations.
Dual closeness of the relation is a direct consequence of the fact that if and only if , which obviously derives from dual closeness of and from the dual of a single-in type being a single-out type and vice-versa. This fact, together with the following proposition, will be used to infer decidability of and relations from that of and , respectively.
Proposition 2.10
The and relations are such that: if and only if .
We now consider variants of obtained by posing limitations to the communication buffer.
We can define a variant decidable relation by putting an upper-bound to the messages that can be buffered. Technically speaking, when an output in the r.h.s. is anticipated during the subtyping simulation, we impose a bound to the number of inputs that are in front of such output.
We say that an input context is -bounded if the maximal number of nested inputs in is less or equal to .
Definition 2.11** (-bounded Asynchronous Subtyping, with )**
- The -bounded asynchronous subtyping is defined as in Definition 2.4, with the only difference that the input context in item is required to be -bounded.*
Notice that the case yields synchronous subtyping: since is the only [math]-bounded input context, we obviously have .
Lange and Yoshida [11] show the decidability of asynchronous subtyping for a subclass of session types, called alternating, that in our setting corresponds to impose that every output in a subtype is immediately followed by an input, while every input in a supertype is followed by an output. For instance, this property is satisfied by the following pair of types:
[TABLE]
It is not difficult to see that . The key point of the proof of decidability of asynchronous subtyping for alternating session types by Lange and Yoshida is the observation that if and are alternating, then if and only if .
As we explained in the Introduction, we also consider the more generic notion of bounded asynchronous subtyping. This relation is in our opinion of interest because it reflects real cases in which it is possible to assume bounded buffers, without an a priory knowledge of the actual bound.
Definition 2.12** (Bounded Asynchronous Subtyping, )**
*We say that is a bounded asynchronous subtype of , written , if there exists such that . *
3 Decidability Results
We now present decidability results for -bounded asynchronous subtyping and asynchronous subtyping for single-out/single-in session types.
3.1 A Subtyping Procedure
We start by giving a procedure (an algorithm that does not necessarily terminate) for the general subtyping relation, which is known to be undecidable [10, 11]. Such a procedure is inspired by the one proposed by Mostrous et al. [14] for asynchronous subtyping in multiparty session types. In order to do so, we introduce two functions on the syntax of types. The function calculates how many unfolding are necessary for bringing an output outside a recursion. If that is not possible, the function is undefined (denoted by ).
Definition 3.1** (outDepth)**
*The partial function is inductively defined as follows: *
[TABLE]
where , if for some ; similarly, .
As an example of application of consider, for any and , . On the other hand, consider the type T_{\textsf{e}x}=\&\Big{\{}l_{1}:\mu\mathbf{t}.\oplus\!\big{\{}l_{2}:T_{1}\big{\}},\ l_{3}:\mu\mathbf{t}.\&\!\big{\{}l_{4}:\mu\mathbf{t}^{\prime}.\oplus\!\{l_{5}:T_{2}\}\big{\}}\Big{\}}: clearly, 0pt\big{(}T_{\textsf{e}x}\big{)}=2. We then define ), a variant of the unfolding function given in Definition 2.2, which unfolds only where it is necessary, in order to reach an output:
Definition 3.2** (outUnf)**
The output unfolding is a partial function defined whenever is defined. Given , is computed using the same inductive rules of , excluding the rule for that, instead of recursively unfolding , returns the same term .
The function above differs from : for example, \mathsf{unfold}^{2}\big{(}T_{\textsf{e}x}\big{)} would unfold twice both subterms and \mu\mathbf{t}.\&\!\big{\{}l_{4}:\mu\mathbf{t}^{\prime}.\oplus\!\{l_{5}:T_{2}\}\big{\}}. On the other hand, applying to the same term would unfold once the term reached with and twice the one reached with .
In the subtyping procedure defined below we make use of in order to have that recursive definitions under the scope of an output are never unfolded. This guarantees that during the execution of the procedure, even if the set of reached terms could be unbounded, all the subterms starting with an output are taken from a bounded set of terms. This is important to guarantee termination333Technically speaking, this property of the unfolding is used in the proof of Theorem 3.11. of the algorithm that we will define in Section 3.3 as an extension of the procedure described below.
Subtyping Procedure. An environment is a set containing pairs , where and are types. Judgements are triples of the form which intuitively read as “in order to succeed, the procedure must check whether is a subtype of , provided that pairs in have already been visited”. Our subtyping procedure, applied to the types and , consists of deriving the state space of our judgments using the rules in Figure 2 bottom-up starting from the initial judgement . More precisely, we use the transition relation to indicate that if matches the conclusions of one of the rules in Figure 2, then is produced by the corresponding premises. The procedure explores the reachable judgements according to this transition relation. We give highest priority to rule Asmp, thus ensuring that at most one rule is applicable.444The priority of Asmp is sufficient because all the other rules are alternative, i.e., given a judgement there are no two rules different from Asmp that can be both applied. The idea behind is to avoid cycles when dealing with recursive types. Rules and deal with the case in which we need to unfold recursion in the type on the right-hand side. If the type on the left-hand side is not an output then the procedure simply adds the current pair to and continues. On the other hand, if an output must be found, we apply which checks whether such output is available. Rule Out allows nested outputs to be anticipated (when not under recursion) and condition \big{(}\mathcal{A}\neq[\,]^{1}\big{)}\Rightarrow\forall i\in I.\&\in T_{i} makes sure there are no orphan messages. The remaining rules are self-explanatory. is the reflexive and transitive closure of the transition relation among judgements. We write if the judgement matches the conclusion of one of the axioms Asmp or End, and to mean that no rule can be applied to . Due to input branching and output selection, the rules In and Out could generate branching also in the state space to be explored by the procedure. Namely, given a judgement , there are several subsequent judgements sucht that . The procedure could (i) successfully terminate because all the explored branches reach a successful judgement , (ii) terminate with an error in case at least one judgement is reached, or (iii) diverge because no branch terminates with an error and at least one branch never reaches a succesful judgement.
Example 3.3
Consider T=\mu\mathbf{t}.\oplus\big{\{}l_{1}:\&\{l_{2}:\mathbf{t}\}\big{\}} and S=\mu\mathbf{t}.\oplus\Big{\{}l_{1}:\&\big{\{}l_{2}:\&\{l_{2}:\mathbf{t}\}\big{\}}\Big{\}}. Clearly, the two types and are related by asynchronous subtyping, i.e. . However, the subtyping procedure on does not terminate:
[TABLE]
*Notice that the last step above is obtained by application of the rule Out by considering the input context . *
The example above shows that the procedure could diverge; the next result proves that this can happen only if the checked types are in subtyping relation. More precisely, types and are not in subtyping relation if and only if the procedure on terminates with an error; formally
Proposition 3.4
Given the types and , we have that there exist such that if and only if .
This means that: if then the procedure on surely terminates with an error; if, instead, then the procedure terminates successfully or diverges.
3.2 -bounded Asynchronous Subtyping
In the previous subsection we have shown that the standard subtyping procedure does not terminate in general. In order to guarantee termination, Lange and Yoshida [11] have considered limitations to the communication buffer, like half-duplex (in this case asynchronous and synchronous subtyping coincides) or alternating protocols (in this case the buffer will store at most one message). We now prove a more general decidability result. We show that, for every , we can define an algorithm for the notion of -bounded asynchronous subtyping introduced in Section 2.1, building on the subtyping procedure defined previously.
We consider an algorithm, that we denote with , obtained from the above procedure for simply by imposing that the input context , used in rule Out in Figure 2, is always -bounded. Then, the following result holds:
Theorem 3.5
The algorithm for always terminates and, given the types and , there exist such that if and only if .
3.3 Asynchronous Subtyping for Single-Out or Single-In
Types
In Example 3.3 we have seen that, if we consider the terms T=\mu\mathbf{t}.\oplus\big{\{}l_{1}:\&\{l_{2}:\mathbf{t}\}\big{\}} and S=\mu\mathbf{t}.\oplus\Big{\{}l_{1}:\&\big{\{}l_{2}:\&\{l_{2}:\mathbf{t}\}\big{\}}\Big{\}}, the subtyping procedure in Figure 2 applied to does not terminate. The problem is that the termination rule Asmp cannot be applied because the term on the r.h.s. (i.e. the supertype) generates always new terms in the form \&\Big{\{}l_{2}:\&\big{\{}l_{2}:\dots\&\{l_{2}:S\}\dots\big{\}}\Big{\}}.
Notice that, in this particular example, these infinitely many distinct terms are obtained by adding single inputs (i.e. single-choice input branchings) in front of the term in the r.h.s.: we call this linear input accumulation.
For simple cases like this one, solutions have been proposed by Lange and Yoshida [11] and Bravetti et al. [10]. The idea is to extend the subtyping procedure in Figure 2 with additional termination rules able to detect when it is no longer necessary to continue because it entered a deterministic loop (where the only possible future behavior of the procedure is to repeat indefinitely the same linear input accumulation). This approach holds only under two assumptions, both satisfied by the subtyping relations considered in Lange and Yoshida [11] and Bravetti et al. [10]: while checking subtyping output selections in the l.h.s. (i.e. the subtype) are always single-choice and the same holds for input branchings in the r.h.s. (i.e. the supertype). This implies that there is a linear input accumulation, which is the repetition of a specific sequence of input labels. The combination of these two assumptions guarantees that the subtyping procedure proceeds deterministically: this makes it possible to detect whether it enters a loop because the unique kind of loops are the deterministic ones.
In this section we show that it is possible to relax at least one of these two assumptions: either deal with the case in which the input accumulation is not linear, or deal with the case in which output selections in the l.h.s. are not single-choice. More precisely, the two cases that we consider are the following ones: subtyping between single-out session types (where input branchings in the r.h.s. are not constrained to be single-choice as in previous approaches) and subtyping between single-in session types (where output selections in the l.h.s. are not constrained to be single-choice as in previous approaches), i.e. the two relations and , respectively, that we introduced in Section 2.1. The idea is to find an algorithm for one of the two cases and apply it also to the other one by exploiting type duality.
In the single-in case we surely have linear input accumulation but the subtyping procedure is no longer deterministic due to non-single output selections in the l.h.s. that have multiple possible continuations. This causes the approach proposed in Lange and Yoshida [11] and Bravetti et al. [10] to fail because now the procedure can incur in nondeterministic loops (so it is not guaranteed to repeat indefinitely the accumulation behavior detected by the additional termination rule they consider). On the other hand, in the single-out case we loose the linear input accumulation but we do not have output selections to cause the problematic nondeterminism discussed above.
The latter advantage led us to opt for the single-out case, which we were able to manage by adopting a totally new approach where the input accumulation is represented in the form of a tree (thus accounting for all possible alternative accumulated input behaviors at the same time).
We start with an example of subtyping between single-out types that cannot be managed with the approach in Lange and Yoshida [11] and Bravetti et al. [10] because there is non-linear input accumulation.
Example 3.6
Consider T=\mu\mathbf{t}.\oplus\big{\{}l_{1}:\&\{l_{2}:\mathbf{t},l_{3}:\mathbf{t}\}\big{\}} and S=\mu\mathbf{t}.\oplus\Big{\{}l_{1}:\&\big{\{}l_{2}:\&\{l_{2}:\mathbf{t}\},l_{3}:\mathbf{t}\big{\}}\Big{\}}. We now comment the application of the subtyping procedure on .
[TABLE]
At this point, the subtyping procedure has two continuations, one for the label and one for the label . In case of label we reach the judgement:
[TABLE]
on which the termination rule Asmp can be applied. In case of label we have:
[TABLE]
*Notice that in the last judgement, the r.h.s. has a non-linear input accumulation starting with an input choice on two labels and . *
3.3.1 Asynchronous Subtyping for Single-Out Types
We now present our novel approach to asynchronous subtyping that can be applied to single-out types, hence also to the types in the above Example 3.6, that will be used as a running example in this section. As anticipated, the main novelty is the ability to deal with non-linear input accumulation by representing it as a tree. We need to be able to extract the leafs from these trees: this is done by the leaf set function defined as follows.
Definition 3.7** (Leaf Set)**
Given a session type , we write if is not of the form . Given a session type , we define
[TABLE]
The leaf set of a session type is the set of subterms different from inputs that are reachable from its root through a path of inputs. For example, the leaf set of the term is . If we consider the r.h.s. term in the last judgement in Example 3.6, we have that \mathsf{leafSet}(\&\big{\{}l_{2}:\&\{l_{2}:S\},l_{3}:S\big{\}})=\{S\}.
During the check of subtyping, according to Figure 2 (rule Out), when a term in the r.h.s. having input accumulation has to mimic an output in front of the l.h.s., such output must be present in front of all the leafs of the tree. In this case, the checking continues by anticipating the output from all the leafs. The following auxiliary function output anticipation indicates the way a term changes after having anticipated a sequence of outputs. Notice that in the definition we make use of the assumption on single-out session types, by considering single-choice output selections.
Definition 3.8** (Output Anticipation)**
Partial function , with single-out session type and sequence of labels, is inductively defined as follows:
[TABLE]
We say that can infinitely anticipate outputs, written , if there exists an infinite sequence of labels such that is defined for every .
The function anticipates all outputs in the sequence . For example, the function applied to and the sequence would return the same term, while it would be undefined with the sequence . If we go back to our running Example 3.6, we have that \mathsf{antOut}(S,l_{1})=\&\big{\{}l_{2}:\&\{l_{2}:S\},l_{3}:S\big{\}}. Moreover, we have that holds because the label can be infinitely anticipated.
The definition of is not algorithmic in that it quantifies on every possible natural number . Nevertheless, as we show below, it can be decided by checking whether for every session type obtained from by means of output anticipations, all the terms populating its leaf set can anticipate the same output label. Although such process may generate infinitely many session types, the terms populating the leaf sets are finite and are over-approximated by the function , which always returns a finite set and is defined as:
Definition 3.9** (Reachable Types)**
- Given a single-out session type , is the minimal set of session types such that:*
- 1.
; 2. 2.
* implies for every ;* 3. 3.
* implies ;* 4. 4.
* implies .*
Notice that is populated by those session types obtained by consuming in sequence the initial inputs and outputs, and by unfolding recursion only when it is at the top level. As an example, consider the session type of the Example 3.6. We have
\begin{array}[]{l}\mathsf{reach}(S)\!=\!\Big{\{}S,\oplus\big{\{}l_{1}\!:\&\big{\{}l_{2}\!:\&\{l_{2}\!:S\},l_{3}\!:S\big{\}}\big{\}},\&\big{\{}l_{2}\!:\&\{l_{2}\!:S\},l_{3}\!:S\big{\}},\&\{l_{2}\!:S\}\Big{\}}\\[8.5359pt] \end{array}
For every type , we have that the terms in are finite; in fact, during the generation of such terms, eventually the term or a term already considered is reached. The latter occurs after consumption of all the inputs and outputs in front of a recursion variable already unfolded.
Proposition 3.10
Given a single-out session type , is finite and it is decidable whether .
Subtyping algorithm for single-out types. We are now ready to present the new termination condition that once added to the subtyping procedure in Figure 2 makes it a valid algorithm for checking subtyping for single-out types. The termination condition is defined as an additional rule, named Asmp2, that complements the already defined Asmp rule by detecting those cases in which the subtyping procedure in Figure 2 does not terminate.
The new rule is defined parametrically on the session type , which is the type on the right-hand side of the initial pair of types to be checked (i.e. the algorithm is intended to check , for some type ). We start from the initial judgement and then apply from bottom to top the rules in Figure 2, where is replaced by , plus the following additional rule:
[TABLE]
We first observe that this termination rule can be applied to the last judgement of our running Example 3.6. We have already seen that , holds, \mathsf{antOut}(S,l_{1})=\&\big{\{}l_{2}:\&\{l_{2}:S\},l_{3}:S\big{\}} and that \mathsf{leafSet}(\&\big{\{}l_{2}:\&\{l_{2}:S\},l_{3}:S\big{\}})=\{S\}. We now observe that and , hence we can conclude that we can apply the above termination rule Asmp2 to the last judgement in Example 3.6 by instantiating and .
The first property of the new algorithm that we prove is termination. Intuitively, we have that this new termination rule guarantees to catch all those cases where the term on the right grows indefinitely, by anticipating outputs and accumulating inputs. These infinitely many distinct types are anyway obtainable starting from the finite set , by means of output anticipations. Hence there exists that can generate infinitely many of these types: this guarantees to be true. As observed above, the leaves of such infinitely many terms are themselves taken from the finite set . This guarantees that the algorithm, among the types that can be obtained from , visits two terms having the same leaf set. These, even if syntactically different, are equivalent as far as the subtyping game is regarded.
Concerning the precise definition of the algorithm, in order to avoid the possibility of applying two distinct rules to the same judgement, we give rule Asmp2 the same priority as rule Asmp (both rules have highest priority). Also in this case, we use to denote that the latter can be obtained from the former by one rule application, and , to denote that there is no rule that can be applied to the judgement .
We can now state the termination and soundness of the algorithm:
Theorem 3.11
Given two single-out session types and , the algorithm applied to the initial judgement terminates.
Theorem 3.12
Given two single-out session types and , we have that there exist such that if and only if there exist such that .
Finally, we can conclude the decidability of asynchronous subtyping for single-out session types.
Corollary 3.13** (Decidability for Single-out Types)**
Asynchronous subtyping for single-out session types is decidable.
We now show that the above decidability results hold also for the relation (where we further restrict the asynchronous subtyping relation not to admit contravariance on input branchings). In the algorithm we just modify the rule of Figure 2 by changing the constraint in the premise into , thus obtaining modified versions of (and ) and (and ). We have that Proposition 3.4, where relation is considered instead of , termination Theorem 3.11 and soundness Theorem 3.12, where the modified judgments and are considered, still hold (they are proved with exactly the same proofs as those reported in B for the original statements).
Corollary 3.14
Asynchronous subtyping for single-out session types without input contravariance is decidable.
3.3.2 Asynchronous Subtyping for Single-in Types
First of all we notice that an obvious consequence of Corollary 3.13 is that also is decidable (we just have to add a preliminary check verifying that both types are single-in). Moreover, exploiting dual closeness, i.e. the fact that if and only if (see Section 2.1), we can use the algorithm presented for single-out types also for the case of single-in types.
Corollary 3.15** (Decidability for Single-in Types)**
Asynchronous subtyping for single-in session types is decidable.
We can therefore identify an asynchronous dual closed subtyping relation that stands in the boundary of decidability.
Corollary 3.16** (Decidability for Single-in or Single-out Types)**
- The asynchronous dual closed subtyping relation is decidable.*
Finally, similarly as we did for , by exploiting Proposition 2.10 we can use the modified algorithm employed for subtyping for deciding the remaining relation .
Corollary 3.17
Asynchronous subtyping for single-in session types without output covariance is decidable.
4 Undecidability Results
We now move to undecidability results. We first consider bounded asynchronous subtyping . The proof in this case is a variant of the proof we already presented in our previous work [10], where we encoded the problem of checking (non) termination in queue machines (a well-known Turing powerful formalism) into checking session subtyping. Technically speaking, we resort to a different property, namely bounded non termination, that we here show to be undecidable for queue machines.
The second, and main, undecidability result concerns subtyping without output covariance and input contravariance . The proof in this case requires deep modifications to our proof technique, due to the impossibility to exploit covariance/contravariance in the queue machine encoding. We deal with the absence of covariance/contravariance by saturating each point of choice on the entire considered alphabet. This has a strong impact on the encoding because it introduces additional choices, in the session types, whose continuations do not correspond to the behaviour of the considered queue machine. This problem is solved by ensuring that these additional choices and the corresponding continuations are irrelevant as far as subtyping checking is concerned. Such solution, however, works only for a fragment of queue machines (that we call single-consuming queue machines) that we prove to be Turing complete as well.
We consider this second result interesting for the following reason: the previous undecidability proofs [10, 11] made use of both output covariance/input contravariance (already present in synchronous session subtyping) and output anticipation (specific for asynchronous subtyping), hence our new proof shows that (provided that the syntax of types is not constrained, e.g, imposing single choices for output selections or input branchings) the source of undecidability is to be precisely localized into the latter, as the former is not necessary to prove undecidability.
We first report the definition of queue machines.
4.1 Queue Machines
Queue machines are a formalism similar to pushdown automata, but with a queue instead of a stack. Queue machines are Turing-equivalent [15].
Definition 4.1** (Queue Machine)**
A queue machine is defined by a six-tuple (Q,\Sigma,\Gamma,\,s,\delta)$ where:
* is a finite set of states;*
- 2.
* is a finite set denoting the input alphabet;*
- 3.
* is a finite set denoting the queue alphabet;*
- 4.
\\in\Gamma-\Sigma$* is the initial queue symbol;*
- 5.
* is the start state;*
- 6.
* is the transition function.*
A configuration of a queue machine is an ordered pair where is its current state and is the content of the queue ( is the Kleene closure of ). The starting configuration on an input string is (s,x\)\rightarrow_{M}(p,A\alpha)\rightarrow_{M}(q,\alpha\gamma)\delta(p,A)=(q,\gamma)MxxM(s,x$)\rightarrow_{M}^{}(q,\epsilon)\epsilon\rightarrow_{M}^{}\rightarrow_{M}$. Intuitively, a queue machines is a Turing machine with a special tape that works as a FIFO queue.
The Turing completeness of queue machines is discussed by Kozen [15] (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. The undecidability of termination for queue machines follows directly from such encoding.
4.2 Bounded Asynchronous Subtyping
We now consider the notion of bounded asynchronous subtyping we introduced in Section 2.1,
The proof of undecidability of follows the approach we already used to prove the undecidability of single-choice asynchronous subtyping [10] (that we have commented in the Introduction). The idea is to define, given a queue machine and its input , two session types and , such that is a subtype of if and only if does not accept . More precisely, the type models the finite control of the queue machine while the type models the queue that initially contains the sequence $x$$.
More precisely, the encoding of queue machines is as follows [10].
Definition 4.2** (Queue Machine Encoding)**
Let M=(Q,\Sigma,\Gamma,\,s,\delta)C_{1},\cdots,C_{m}\in\Gammam\geq 0q\in Q\mathcal{S}\subseteq Q[![{q}]!]^{\mathcal{S}}[![{C_{1}\cdots C_{m}}]!]are defined as in Figure [3](#S4.F3)(a) and Figure [3](#S4.F3)(b) respectively. The initial encoding ofMx[![{s}]!]^{\emptyset}[![{x$}]!]$.
The basic idea behind the encoding of the finite control is to use a recursively defined type with a recursion variable for each state of the encoded queue machine . The type corresponding to the recursion variable starts with an input with multiple choices, one for each possible symbol that can be consumed from the queue. The continuation is composed of a sequence of single-choice inputs labeled with the symbols , where are the symbols enqueued by the queue machine when, in state , consumes from the queue. Assuming that is the new state of after execution of this step (i.e. ), the type becomes the one corresponding to the recursion variable .
On the other hand, the type modeling the queue with contents is denoted with : this type starts with a sequence of single-choice inputs labeled with the symbols , followed by a recursive type. Such type starts with an output with multiple-choices, one for each symbols that can be enqueued, followed by a single-choice input having the same label. This particular type has the following property: if one label of the multiple-choice output is selected for anticipation during the subtyping simulation game, the corresponding single-choice input labeled with is enqueued at the end of the sequence of inputs preceding the recursive definition. This perfectly corresponds to the behaviour of the queue in the modeled queue machine.
As mentioned above, this encoding has been already used to prove the undecidability of [10]. More precisely, we proved that given a queue machine M=(Q,\Sigma,\Gamma,\,s,\delta)x[![{s}]!]^{\emptyset}{<!!<}[![{x$}]!]xMMxMx[![{s}]!]^{\emptyset}\not!!{\leq_{\mathsf{bound}}}[![{x$}]!]$, in particular, those cases in which the subtyping simulation game generates unbounded accumulation of inputs. For this reason we have to consider a more complex undecidable property for queue machines: bounded non termination, i.e., the ability of a queue machine to have an infinite computation while keeping the length of the queue bounded. We now define the notion of boundedness for queue machines and then prove that bounded non termination is undecidable.
Definition 4.3** (Queue Machine Boundedness)**
Let be a queue machine and a possible input. We say that is bound on input if there exists such that, for every and such that (s,x\)\rightarrow_{M}^{}(q,\gamma)|\gamma|\leq k$.*
Lemma 4.4
Given a queue machine and an input , it is undecidable whether does not terminate and is bound on .
Following the proof technique we already used to prove undecidability of , i.e. by reducing the termination problem for queue machines into subtyping checking [10], we can prove also the undecidability of by reduction from the bounded non termination problem.
Theorem 4.5
Given a queue machine M=(Q,\Sigma,\Gamma,\,s,\delta)x[![{s}]!]^{\emptyset}{\leq_{\mathsf{bound}}}[![{x$}]!]Mx$.
Corollary 4.6
Bounded asynchronous subtyping is undecidable.
4.3 Undecidability of Asynchronous Subtyping without Output
Covariance and Input Contravariance
We now move to the proof of undecidability of , the asynchronous subyping relation, we introduced in Section 2.1, that does not admit output covariance and input contravariance by imposing matching choices to have the same set of labels.
The proof technique is still based on an encoding of queue machines, but we have to significantly improve the encoding discussed in the previous subsection. In fact, the encoding of Figure 3 exploits both input contravariance (in the matching between the multiple-choice input at the beginning of the encoding of the finite control and the initial single-choice inputs of the queue encoding) and output covariance (in the matching between the multiple-choice output at the beginning of the recursive part of the queue encoding and the single-choice outputs in the encoding of the finite control).
The new encoding that we propose saturates all choices, both inputs and outputs, with labels corresponding to the entire queue alphabet. The addition of these labels and of the corresponding continuations, introduces new possible paths in the subtyping simulation game. We are able to make these additional behaviour irrelevant, but at the price of restricting the class of encoded queue machines. These queue machines are named single consuming queue machines; their characteristic is to guarantee that in two subsequence actions, at least one of the two will enqueue symbols.
Definition 4.7** (Single Consuming Queue machine)**
We say that a queue machine M=(Q,\Sigma,\Gamma,\,s,\delta)\delta(q,a)=(q^{\prime},\epsilon)qaq^{\prime}bq^{\prime\prime}\delta(q^{\prime},b)=(q^{\prime\prime},\epsilon)$.
We have that single consuming queue machines are still Turing-complete (see C.2 for the detailed proof based on an encoding of queue machines into single consuming queue machines):
Theorem 4.8
*Given a single consuming queue machine and an input , the termination of on is undecidable. *
We prove the undecidability of by encoding single consuming queue machines into the subtyping simulation game. Following the approach already discussed in the previous subsection, given a queue machine, our encoding generates a pair of types, say and , such that encodes the finite control and encodes the queue. Then, the subtyping simulates the execution of the machine.
We are now ready to present the definition of the new encoding where we make use of the following new notation: .
Definition 4.9** (Encoding Single Consuming Queue machines)**
Let M=(Q,\Sigma,\Gamma,\,s,\delta)q\in Q\mathcal{S}\subseteq QC_{1},\cdots,C_{m}\in\Gammam\geq 0{[![![{q}]!]!]}^{\mathcal{S}}[![![{C_{1}\cdots C_{m}}]!]!]$ are defined as in Figure 4(a) and Figure 4(b) respectively.
As discussed in the previous subsection, the idea is that the type encoding the finite control is able to perform an input on each of the symbols in , and continue according to the definition of the transition function . The type representing the queue then matches such input with the correct symbol depending on the state of the queue. For instance, in the encoding described in the previous subsection, if we denote with and the types representing the finite control and the queue respectively, and if and symbol is on the head of the queue, we have and : type is able to react to any symbol that may be present on the queue (like the transition function ), while type reacts with the actual value on the queue, symbol . Unfortunately, such idea exploits contravariance for inputs. Therefore, it must be the case, in the new encoding, that the input in is of the form . We make sure that if label is selected then the simulation of the queue machine continues. Otherwise, an infinite subtyping simulation game is started (starting from in the example).
Also the insertion of symbols in the queue was simulated in the encoding of the previous subsection by exploiting output covariance. The type representing the finite control performs a single-choice output that is matched by a multiple-choice output having the effect of adding a corresponding symbol at the end of the input accumulated in the type modeling the queue. Also in this case, we have to add choices to the type modeling the finite control: also in this case we ensure that these extra paths start an infinite subtyping simulation game.
These additional paths make the subtyping simulation game highly non-deterministic and such that several paths that the game can take differ from what the encoded machine does. We discuss in detail the various cases which our encoding in Figure 4 can be in:
The encoding of the finite control reads the correct symbol. We represent the machine reading a symbol from the queue while being in state , with an input type of the form , where each branch corresponds to a possible symbol that can be read. On the other hand, a queue is encoded as an input type of the form \&\big{(}\big{\{}C_{1}:[\![\![{C_{2}\ldots C_{m}}]\!]\!]\big{\}}\uplus\big{\{}{A^{\prime}:T^{\prime\prime}}\big{\}}_{A^{\prime}\in\Gamma\setminus\{C_{1}\}}\big{)} where the branch with label represents the actual content of the queue. Hence, in the simulation game, if the finite control reads symbol and this is matched by the correct symbol in the queue, then the type deals with inserting symbols into the queue. 2. 2.
The encoding of the finite control reads the wrong symbol. In this case, the encoding of the finite control picks a symbol that is not that in the queue head. In order to match it, the encoding of the queue will take \big{\{}{A^{\prime}:T^{\prime\prime}}\big{\}}_{A^{\prime}\in\Gamma\setminus\{C_{1}\}}. Type is designed in a way that it can match every move of the finite control, by repeatedly alternating two inputs with a subsequent output on every queue symbol. Note that, since inputs cannot be anticipated, matching every move is feasible only if the encoded machine is single consuming. 3. 3.
The encoding of the finite control writes the correct symbol. Once the finite control has read a symbol, it performs , which simulates the writing of into the queue. If then it moves to the encoding of the next state according to function . Otherwise, it translates to the type \oplus\big{(}\big{\{}B_{1}:{\{\!\!\{{B_{2}\ldots B_{m}}\}\!\!\}}_{r}^{\mathcal{T}}\big{\}}\uplus\big{\{}{A^{\prime}:T^{\prime}}\big{\}}_{A^{\prime}\in\Gamma\setminus\{B_{1}\}}\big{)}. The queue, in order to match (and , …, ) can always anticipate outputs with the term \mu\mathbf{t}\oplus\big{\{}A:\&\big{(}\big{\{}A:\mathbf{t}\big{\}}\uplus\big{\{}A^{\prime}:T^{\prime\prime}\big{\}}_{A^{\prime}\in\Gamma\setminus\{A\}}\big{)}\big{\}}_{A\in\Gamma} which, after consuming a label will add an input with label , simulating the adding of to the queue. 4. 4.
The encoding of the finite control writes the wrong symbol. In this case, the finite control writes a symbol to the queue with \oplus\big{(}\big{\{}B_{1}:{\{\!\!\{{B_{2}\ldots B_{m}}\}\!\!\}}_{r}^{\mathcal{T}}\big{\}}\uplus\big{\{}{A^{\prime}:T^{\prime}}\big{\}}_{A^{\prime}\in\Gamma\setminus\{B_{1}\}}\big{)}. However, the simulation executes the wrong output (with any ) and continues as . In this case, continues removing and adding any value from the queue, indefinitely. Note that it may remove the wrong value from the queue overlapping with case 2. In this case, the requirement that the queue machine is single consuming is not necessary.
Example 4.10
In order to further clarify our encoding, consider a queue machine with states (where is the starting state), queue alphabet and transition relation such that and , for every . Clearly, the machine terminates on any input. The encoding of the finite control is the following session type:
[TABLE]
[TABLE]
*Assume, e.g., that the queue initially contains the string . The machine will empty the queue by visiting state twice and terminate in state with the empty queue. If we now run the subtyping simulation game between the encoding of finite control above and the encoding of the queue we will end up with two types that are not in subtyping: the encoding of the state starting with an input and the encoding of the empty queue that does not match it. *
The encoding of the finite-control and of the queue are such that the following properties hold: given a queue machine with initial state and initial queue symbol \$$, if Mx({[![![{s}]!]!]}^{\emptyset},[![![{x$}]!]!]){[![![{s}]!]!]}^{\emptyset}{\leq}_{\mathsf{tin,tout}}[![![{x$}]!]!]Mx$. We thus have the following:
Theorem 4.11
Given a single consuming queue machine M=(Q,\Sigma,\Gamma,\,s,\delta)x\in\Sigma^{}{[![![{s}]!]!]}^{\emptyset}{\leq}_{\mathsf{tin,tout}}[![![{x$}]!]!]Mx$.*
We can therefore conclude that subtyping without output covariance and input contravariance is undecidable.
Corollary 4.12** (Undecidability of Subtying without Co/contravariance)**
The asynchronous dual closed subtyping relation is undecidable.
In the same way we can also show that and are undecidable and provide an alternative proof of undecidability of . This because, since for the types obtained with the encoding (for which the ability to match via covariance/contravariance is irrelevant) obviously such relations coincide, i.e. {[\![\![{s}]\!]\!]}^{\emptyset}{\leq}_{\mathsf{tin,tout}}[\![\![{x\}]!]!]{[![![{s}]!]!]}^{\emptyset}{\leq}{\mathsf{tin}}[![![{x$}]!]!]{[![![{s}]!]!]}^{\emptyset}{\leq}{\mathsf{tout}}[![![{x$}]!]!]{[![![{s}]!]!]}^{\emptyset}{\leq}[![![{x$}]!]!], Theorem [4.11](#S4.Thmproposition11) holds also if we replace the {\leq}_{\mathsf{tin,tout}}$ relation with one of such relations.
Corollary 4.13
Asynchronous subtyping relations , and are undecidable.
5 Related Work
Subtyping for Session Types. Subtyping for session types was first introduced by Gay and Hole [7]555The Gay and Hole subtyping is contravariant on outputs and covariant on inputs. This is because a channel-based subtyping [9] is considered instead of our process-oriented subtyping. for a session-based -calculus where communication is synchronous, i.e., an output directly synchronises with an input. In such case, the relation allows no output anticipation. However, as in our case, outputs are covariant and inputs are contravariant.
To the best of our knowledge, Mostrous et al. [14] were the first to adapt the notion of session subtyping to an asynchronous setting. Their computation model is a session -calculus with asynchronous communication that makes use of session queues for maintaining the order in which messages are sent. They introduce the idea of output anticipation, which is also a main feature of our theory. Mostrous and Yoshida [12] extended the notion of asynchronous subtyping to session types for the higher-order -calculus. In the same article, Mostrous and Yoshida observe that their definition of asynchronous subtyping allows orphan messages. Orphan message are prohibited with the definition of subtyping given by Chen et al. [8]. In their article, they show that such a definition is both sound and complete w.r.t. type safety and orphan message freedom.
Undecidability Results. Mostrous et al. [14] proposed a procedure to check asynchronous subtyping for multiparty session types. Differently from what stated therein, the procedure does not terminate due to unbounded message accumulation in the queues, e.g. for the terms in Example 3.3. Such a procedure inspired the one we presented in Section 3.1. The problem of unbounded accumulation was observed by Mostrous and Yoshida [12]. The impossibility to define a correct algorithm has been independently proved by Lange and Yoshida [11] and Bravetti et. al [10]. Lange and Yoshida [11] reduce Turing machine termination into a notion of compatibility for communicating automata and, then, transfer such a result to session types. This proof technique applies only to dual closed subtyping relations, like the one by Chen et al. [8]. The proof by Bravetti et. al [10], on the other hand, exploits a direct encoding of queue machines into session subtyping. This made it possible to prove undecidability of all the other notions of asynchronous subtyping in the literature. Unlike the encoding in this paper (Figure 4), both encodings take advantage of the use of output covariance and input contravariance. For example, by exploiting this feature, the queue machine encoding by Bravetti et al. [10] (Figure 3) is much simpler than the encoding we need to use here. We notice that our results on undecidability focus on binary session types. However, it is immediate to generalise this kind of undecidability results from binary to multiparty sessions (binary session types are just multiparty session types with only two roles [10]).
Decidability Results. Synchronous subtyping for binary session types is decidable [7]. Both Bravetti et al. [10] and Lange and Yoshida [11] investigate fragments of session types for which asynchronous subtyping becomes decidable. However, such fragments are much more limited, and far from having practical applications, with respect to those considered here. Both address cases where one of the compared types is a single-choice session type, i.e. all its branchings and selections are single-choice. Thus they are both, basically, special cases of our subtyping for single-in or single-out types (). In particular, Lange and Yoshida give an algorithm for deciding subtyping between a general session type and a single-choice session type. Although it may seem that such case is not properly included in our decidable subtyping relation for single-out/single-in types, covariance and contravariance ensure that all types containing at least one multiple input branch and one multiple output selection (both reachable in the subtyping simulation game) cannot be related with a single-choice type. Bravetti et al. [10] prove decidability for relations and that pose an analogous restriction to the branching/selection structure, but that allow for orphan messages. and are fragments where related types are such that, either is single-choice and is single-in (), or is single-out and is single-choice (). For types that do not produce orphan messages, the sutyping of Bravetti et al. [10] is just a special case of our single-in () and single-out () session subtyping.
Additionally, Lange and Yoshida state the decidability of subtyping for half-duplex communication [16] and alternating machines: the former coincides with synchronous subtyping while the latter can be reduced to -bounded asynchronous subtyping as discussed in Section 3.2.
Comparison with our Previous Work [10]. Concerning decidability results, the approaches taken in this and our previous paper are both based on initially considering a (non always terminating) subtyping procedure , inspired from Mostrous et al. [14], and then presenting a subtyping algorithm obtained by adding a new termination Asmp2 rule to the definition of the procedure (the further additional Asmp3 rule in our previous work is not needed when dealing with orphan message-free subtyping, as we do here). Such an Asmp2 rule is crucial to guarantee the termination of the algorithm: the structure of the Asmp2 rule and the related proof of algorithm correctness and termination constitute the main contribution of this paper (as far as decidability results are concerned). In particular, since here multiple choices are admitted for input branchings, the termination condition Asmp2 needs to deal with input accumulation in the form of a tree, instead of simple linear accumulation as in our previous work (see the discussion at the beginning Section 3.3 for details about this comparison). As a consequence Asmp2 is completely modified: it has to deal with complex recurrent patterns to be checked on the leaves of trees representing input branchings (with multiple choices), instead of detecting simple repetitions on strings representing sequences of single-choice inputs. A detailed comparison follows. Concerning the subtyping procedure , the one considered in this paper (Figure 2) is novel in just two details: an additional orphan message-free condition is considered in the Out rule (because here, we consider orphan message-free subtyping) and the usage of the unfolding instead of (so to perform the minimal needed per-branch unfolding). The latter is needed in this paper because, when the procedure is turned into a subtyping algorithm , we have to deal, in the new Asmp2 termination condition, with input trees instead of strings. Correctness of w.r.t. asynchronous subtyping is stated by Proposition 3.4 in this paper, which corresponds to Lemma 5.1 of our previous work [10]. Differently from the proof of that Lemma, here we need to cope with the different way of performing unfolding of right-hand terms in the asynchronous subtyping definition (via ) and in (via ). Termination of the algorithm is stated by Theorem 3.11 in this paper, which corresponds to Lemma 5.2 of our previous work [10]. Here due to the new structure of the Asmp2 rule, the proof is based on a much more complex characterization of right-hand types produced, starting from the initial one, by the subtyping algorithm. Such types are characterized as with being a sequence of output labels and being a type such that and . For the proof in this paper it is thus crucial to show, that is finite and is decidable, as stated by Proposition 3.10, which has no counterpart in our previous work. Correctness of the algorithm w.r.t. procedure is stated by Theorem 3.12 in this paper, which corresponds to Lemma 5.3 of our previous work. In both papers correctness follows from the following property: whenever the termination rule Asmp2 is applied by the algorithm, the subtyping procedure is guaranteed to proceed forever. However, being Asmp2 completely different, here we need to perform a totally new proof. In particular, in our previous work we simply had to prove the existence of a cycle causing the initial input string in the right-hand type to get longer in a repetitive way, here, instead, we have to manage the more complex case of input trees: this entails considering all possible branchings in order to prove that the subtyping procedure proceeds forever.
Concerning undecidability results, both the approaches taken in the two papers are based on resorting to undecidability of queue machines via a suitable encoding of them into subtyping. In particular, for showing undecidability of bounded asynchronous subtyping () we resort to the same encoding as in our previous work, but we consider a more complex property of queue machines that we show to be undecidable: bounded non termination. On the other hand, for showing undecidability of asynchronous subtyping without output covariance and input contravariance (), we need to introduce the novel class of single consuming queue machines and to perform a much more complex encoding which, differently from the previous one, uses nondeterminism (in order to avoid usage of covariance and contravariance, spurious nondeterministic paths that proceed forever have to be added by the encoding). The undecidability proof thus becomes significantly more complex in that the above encoding makes it much more intricated to relate the queue machine behaviour with the subtyping game and the novel class of queue machines. Moreover, introducing a new restricted class of queue machines requires showing them to be Turing-equivalent (by providing an encoding of standard queue machines into them).
6 Conclusion
In this article, we have shed light on the boundaries between decidability and undecidability of asynchronous session subtyping by analyzing two kinds of restrictions: to the branching/selection structure of inputs/outputs and to the capabilities of the communication buffer. In particular, considering all the relations in Figure 1, we have shown: decidability for those in the lower part, notably of -bounded subtyping and of subtyping over single-out or single-in session types; and the undecidability for those in the upper part, notably of bounded subtyping and of subtyping without output covariance and input contravariance.
As future work, we plan to develop typing systems for server/client code in the context of web services, exploiting our subtyping algorithms for single-out/single-in session types. Note that, in practice, server code typically connects, as a client, to other services (e.g. a database server) using another binary session, according to the commonly used multitier architecture. Thus, in general, when typing code, we would use for a specific session one of the two algorithms above depending if the code is playing the role of the client or of the server in that session.
Moreover, we plan to investigate whether other kinds of restriction w.r.t. the two above allow us to obtain a decidable relation (thus retaining general branching/selection structure for both inputs and outputs and not limiting communication buffers).
References
- [1]
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.
- [2]
K. Honda, N. Yoshida, M. Carbone, Multiparty asynchronous session types, in: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2008), 2008, pp. 273–284.
- [3]
S. Lindley, J. G. Morris, Embedding session types in Haskell, in: Proceedings of the 9th International Symposium on Haskell (Haskell 2016), 2016, pp. 133–145.
- [4]
N. Ng, N. Yoshida, Static deadlock detection for concurrent Go by global session graph synthesis, in: Proceedings of the 25th International Conference on Compiler Construction (CC 2016), 2016, pp. 174–184.
- [5]
T. B. L. Jespersen, P. Munksgaard, K. F. Larsen, Session types for Rust, in: Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming, WGP@ICFP 2015, 2015, pp. 13–22.
- [6]
K. Honda, N. Yoshida, M. Carbone, Multiparty asynchronous session types, J. ACM 63 (1) (2016) 9.
- [7]
S. J. Gay, M. Hole, Subtyping for session types in the pi calculus, Acta Inf. 42 (2-3) (2005) 191–225.
doi:10.1007/s00236-005-0177-z.
- [8]
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.
- [9]
S. J. Gay, Subtyping supports safe session substitution, in: A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, 2016, pp. 95–108.
doi:10.1007/978-3-319-30936-1_5.
- [10]
M. Bravetti, M. Carbone, G. Zavattaro, Undecidability of asynchronous session subtyping, Inf. Comput. To appear.
URL http://arxiv.org/abs/1611.05026
- [11]
J. Lange, N. Yoshida, On the undecidability of asynchronous session subtyping, in: Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, 2017, pp. 441–457.
doi:10.1007/978-3-662-54458-7_26.
- [12]
D. Mostrous, N. Yoshida, Session typing and asynchronous subtyping for the higher-order -calculus, Inf. Comput. 241 (2015) 227–263.
- [13]
E. Christensen, F. Curbera, G. Meredith, S. Weerawarana, Web Services Description Language (WSDL), Tech. rep., W3C (2001).
URL https://www.w3.org/TR/wsdl
- [14]
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.
doi:10.1007/978-3-642-00590-9_23.
- [15]
D. Kozen, Automata and computability, Springer, New York, 1997.
- [16]
G. Cécé, A. Finkel, Verification of programs with half-duplex communication, Inf. Comput. 202 (2) (2005) 166–190.
Appendix A Proofs of Section 2
A.1 Proof of Theorem 2.7 and Propositions 2.9 and 2.10
We start by proving Theorem 2.7. This is done by separately showing, as preliminary lemmas, both implications (one in each direction) to hold. The proof of such lemmas will be then also exploited to prove Propositions 2.9 and 2.10.
Lemma A.1
Given two session types and , we have that implies .
Proof. Given an asynchronous dual closed subtyping relation we show that is also a (orphan-message-free) subtyping relation. To this aim we need to prove that if and then the additional item in of Definition 2.4 holds, i.e.
if then
From it follows that , after some possible unfoldings, starts with an input (it must be in the form ). As is an asynchronous dual closed subtyping relation we have . We observe that , after some possible unfoldings, starts with an output and . For item of Definition 2.6, we have that , for some input context . This means that all contain at least an output selection, which implies that all contain at least one input branching. \qed
The following lemma states that implies . This is proved by showing that given we have also because there exists an asynchronous dual closed subtyping relation s.t. . Such relation is defined as follows: . The proof that each pair satisfies the items in Definition 2.6 has only one complex case, namely, the one in which we assume , and (case numbered 2b in the proof). In this case we have to reason on all initial output paths of and use the no orphan message constraint of Definition 2.4 to be sure that such paths cannot be infinite, i.e. they eventually end in a state performing an input choice, and moreover each of these reachable input choices must match with the initial input choice of .
Lemma A.2
Given two session types and , we have that implies .
Proof. We show that, given , it is possible to define an asynchronous dual closed subtyping relation s.t. . Consider
[TABLE]
The relation is dual closed by definition. It remains to show that it satisfies the four items in Definition 2.6. Let . There are two cases: or . In the first case all the item holds by definition of orphan-message-free subtyping relation. We consider now the second case, i.e. , and proceeds with a case analysis.
.
We have . Having , by definition of , in particular by applications of item (with ) and one application of item , it follows that . Hence , then we can conclude what requested, i.e., such that . 2. 2.
.
We have . Having , by definition of , we have two possible cases.
- (a)
By applications of item (with ) and one application of item , it follows that , with and with for every . Hence , then we can conclude what requested, i.e., , and . Notice that we have used the fact that and we have considered an input context . 2. (b)
By applications of item (with ) and one application of item , it follows that (hence with ), and , with and with . Hence . We now observe that there exists an input context and such that with . This follows from the fact that : by repeated application of the rule 2. of Definition 2.4 (that includes the no orphan message constraint), we have the guarantee that along all branches of (and its unfoldings) it is guaranteed to reach an input branching, and by application of rule 3. (in particular the contra-variance on input branchings), the labels of such choices include the set of labels of the initial input branching of . We conclude by showing that what is requested, i.e., , actually holds. This follows from the fact that , which is a consequence of . In fact, this implies that also because an orphan-message-free subtyping relation is still such even if we add pairs assuming already in the relation. Having and , it is easy to see that, given an orphan-message-free subtyping relation such that , the relation obtained by enriching with the pairs , where and types , with , are such that , is still an orphan-message-free subtyping relation. Above we adopt an abuse of notation for input contexts: does not have holes numbered consistently from to , but some numbers in could be missing. 3. 3.
.
We have . Having , by definition of , in particular by applications of item (with ) and one application of item , it follows that , with , and with for every . Hence , then we can conclude what requested, i.e., , and . Notice that we have used the fact that . 4. 4.
.
We first observe that implies . This directly follows from the fact that if belongs to an orphan-message-free subtyping relation, then the same relation enriched with the pair is still an orphan-message-free subtyping relation. We now proceed by considering . As , we have . By the above observation we have that implies what requested, i.e., . \qed
Theorem 2.7.
Given two session types and , we have if and only if .
Proof. Direct consequence of Lemmas A.1 and A.2. \qed
Proposition 2.9.
The relation and the relation are asynchronous dual closed subtyping relations. *
Proof. We first show that is an asynchronous dual closed subtyping relation. We consider and show that it is an asynchronous subtyping relation when in Definition 2.4 we require in item 2. and in item 3. to hold. This implies , thus showing that is dual closed. Given , we show that implies items 1.-4. of Definition 2.4 (where we require in item 2. and in item 3.), apart from the no orphan message constraint of item 2., by case analysis on the structure of type exactly as in the proof of Lemma A.2 (where is considered instead of and all subset inclusions related to covariance/contravariance are replaced by subset equalities). Concerning the no orphan message constraint of item 2., in the case 2.a of the proof of Lemma A.2 just an input context arises (so it obviously holds); in the case 2.b, instead, a generic input context arises: if then this means that , after some possible unfoldings, starts with an output and the constraint is an immediate consequence of the fact that (as in the proof of Lemma A.1).
We now show that is an asynchronous dual closed subtyping relation. We use and to denote the set of single-in and single-out session types, respectively. We have , due to Theorem 2.7. We now show that, for any , all constraints considered by Definition 2.6 hold. We take , the other case is dealt with symmetrically. Since we have that satisfies all constraints in items 1.-4. of Definition 2.6: we just have to additionally observe that, since all reached pairs belong to , they also obviously belong to . Concerning the duality constraint, from , we have , hence . \qed
Proposition 2.10.
The and relations are such that: if and only if . *
Proof. Concerning the only if part, we show as follows. We consider and show that it is an asynchronous subtyping relation when in Definition 2.4 we require in item 3. to hold and related types to be both single-out. Given , we obviously have that and are both single-out and we show that implies items 1.-4. of Definition 2.4 (where in item 3. we require ) as in the proof of Proposition 2.9. The only difference is that, when resorting to the case analysis in the proof of Lemma A.2 we consider instead of and we replace all subset inclusions related to covariance/contravariance in item 3. and the subset inclusion in item 2. by equalities.
Concerning the if part, we show in a completely symmetric way by observing that is an asynchronous subtyping relation when in Definition 2.4 we require in item 2. to hold and related types to be both single-in. In this case, when resorting to the case analysis in the proof of Lemma A.2 we consider instead of and we replace all subset inclusions related to covariance/contravariance in item 2., apart from , by equalities. \qed
Appendix B Proofs of Section 3
B.1 Proof of Proposition 3.4
Proposition 3.4 states that the procedure defined in Figure 2 is a semi-algorithm for checking whether . The proof of the proposition is divided in two parts. The first one shows that if it is not possible to reach a judgement in which no rule can be applied, i.e. there exist no such that , then it is possible to define an asynchronous subtyping relation such that . The second part shows that if then the procedure either continues indefinitely or terminates successfully by application of the Asmp or End rules.
Proposition 3.4.
Given the types and , we have that there exist such that if and only if . *
Proof. We prove the two implications separately.
We start with the only if part and proceed by contraposition, i.e, we assume that it is not true that and show that .
In order to do this we need to perform a preliminary observation: under the assumption that it is not true that , even if we remove rule Asmp from the procedure it is still impossible to reach a judgement , i.e. a judgement on which no rule can be applied. This can be showed as follows. Let be our decision procedure under the assumption that Asmp is not used. Observe that the set of pairs in the judgements is irrelevant for the decision procedure because Asmp is the unique rule influenced by it. Now, by contraposition, assume . Since the standard procedure cannot reach , we must have that there exists an intermediary judgement where Asmp is applied. That is, there exists such that (notice the use of the standard procedure), and . Within the sequence of rule applications we consider the last judgement such that (such judgement exists as the first one already has this property). It is not restrictive to assume that in the sequence there are no two judgements and with and (otherwise we can shorten the sequence by removing the steps between the judgements and ,666The sequence of rules applied to can be applied also to because, as already observed, is not sensitive to the differences between and . obtaining a new one having the same properties but without the second judgement ). Consider now, in the standard application of the procedure , the intermediary judgement that added to the environment. We have that (otherwise rule Asmp was applied that does not introduce any new pair in ) and moreover as the sets of type pairs grow monotonically during the execution of the decision procedure . These last observations guarantee that there exists a standard application of the procedure simply by considering from the same rules used in the sequence . This holds because the pairs of types in the judgements traversed by this sequence are not in (due to the assumption on the judgement ) hence also not in , and moreover such pairs are all distinct (guaranteed by the assumption on the absence of two judgements and with and ).
Consider now the relation where is the minimal set of judgements satisfying the following:
;
- 2.
if and , without applying rule Asmp or , then ;
- 3.
if and by applying , then .
We observe that to each judgement it is always possible to apply at least one rule. In fact, if this is not possible, we would have also for a judgement with and less unfolded than . In fact, the unique difference between the judgements in and those reachable without adopting Asmp is that those in are more unfolded (see the difference between used in rule and used in the definition of ).
We finally show that is an (orphan-message-free) subtyping relation according to Definition 2.4. Let . Then and it is possible to apply at least one rule to . We proceed by cases on .
If then item of Definition 2.4 for pair is shown by induction on , i.e. the number of unguarded (not prefixed by some input or output) occurrences of recursions in for any .
- (a)
Base case . The only rule applicable to is End, that immediately yields the desired pair of .
- (b)
Induction case . The only rules applicable to are Asmp and . In the case of Asmp we have that , hence there exists with such that . can be applied to . So for some ( or ) we have that the procedure applies rule to . Hence . Since , by induction hypothesis item of Definition 2.4 holds for pair , hence it holds for pair .
- 2.
If then item of Definition 2.4 for pair is shown as follows.
- (a)
If then the only rule applicable to is Out, that immediately yields the desired pairs of .
- (b)
If then the only rules applicable to are Asmp and . In the case of Asmp we have that , hence there exists with such that . can be applied to . So for some ( or ) we have that the procedure applies rule to . Hence . Since , we end up in the previous case. Therefore item of Definition 2.4 holds for pair , hence it holds for pair .
- 3.
If then item of Definition 2.4 for pair is shown by induction on .
- (a)
Base case . The only rule applicable to is In, that immediately yields the desired pairs of .
- (b)
Induction case . The only rules applicable to are Asmp and . In the case of Asmp we have that , hence there exists with such that . can be applied to . So for some ( or ) we have that the procedure applies rule to . Hence . Since , by induction hypothesis item of Definition 2.4 holds for pair , hence it holds for pair .
- 4.
If then item of Definition 2.4 for pair holds because the only rule applicable to is RecL that immediately yields the desired pair of .
We now prove the if part and proceed by contraposition. We assume that and show that there exist no , such that . So we can assume the existence of a relation that is an (orphan-message-free) subtyping relation, according to Definition 2.4, such that .
We say that if and: the last rule applied is one of Out, In or RecL rules; while all previous ones are or rules. As another notation we use input-output-end contexts defined as the input contexts in Definition 2.3 with the difference that also the output construct and are part of the grammar in the definition.
We start by showing that implies , , for some and , and . The proof is by induction on the length of such computation . The base case is for a [math] length computation: it yields which holds. For the inductive case we assume it to hold for all computations of a length and we show it to holds for all computations of length , by considering all judgements such that . This is shown by first considering the case in which rule Asmp applies to : in this case there is no such a judgement and there is nothing to prove. Then we consider the case in which and (by applying rules) and rule End applies to . Also in this case there is no such a judgement and there is nothing to prove. Finally, we proceed by an immediate verification that judgements produced in remaining cases are required to be in by items , and of Definition 2.4: ( is a possibly empty sequence of applications followed by Out application), ( is a possibly empty sequence of applications followed by In application) or ( is simply RecL application).
We finally observe that, given a judgement such that , , for some and , and we have:
either rule Asmp applies to , or
- 2.
and, by item of Definition 2.4, there exists such that (by applying rules) and rule End is the unique rule applicable to , with being the unique rule applicable to intermediate judgements, or
- 3.
by items , and of Definition 2.4, there exist such that , with each intermediate judgement having a unique applicable rule. In particular this holds for ( is a possibly empty sequence of applications followed by Out application), ( is a possibly empty sequence of applications followed by In application) or ( is simply RecL application). \qed
B.2 Proof of Theorem 3.5
Theorem 3.5 states that indeed provides an algorithm for checking whether , this is proved in the following by also resorting to the proof of Proposition 3.4.
Theorem 3.5.
- The algorithm for always terminates and, given the types and , there exist such that if and only if .
Proof. We first observe that the decision algorithm for -bounded asynchronous subtyping terminates. By contraposition, if the algorithm does not terminate, there exists an infinite sequence . Along this infinite sequence infinitely many distinct pairs will be added to . As only finitely many distinct terms can be reached as first element of the pairs, there will be infinitely many distinct terms as second element. Such terms will have unbounded depth, but this is not possible due to the constraint added to rule Out that impose the use of -bounded input contexts.
We now prove that, given the types and , there exist such that if and only if .
We start with the if part and proceed by contraposition. We assume that it is not true that and we build a relation that we show to be a -bounded Asynchronous Subtyping relation. The relation is built from the judgments exactly as we did for the subtyping procedure in the first part (the if part) of the proof of Proposition 3.4. In such a proof we show to be an orphan-message-free subtyping relation, hence we just have to show it to be -bounded. It is immediate to observe that, since when applying rule Out to a judgment we require the input context to be -bounded, we may include in only pairs that satisfy the same constraint in item of -bounded Asynchronous Subtyping relation definition (Definition 2.11), because otherwise we would have by possibly applying / rules. Hence, as justified in Proposition 3.4 this would lead to violating the assumption that the algorithm does not reach an error. The justification provided there still holds because judgments and , with and that just differ for the level of internal unfoldings, behave equivalently with respect to errors due to -boundedness violations. This because the -boundedness of context is established by the Out rule after unfolding in / all recursions occurring before the first output of every possible branch by means of the / rules.
We now prove the only if part and proceed by contraposition. We assume that and show that there exist no , such that . If then also . So we can assume the existence of a relation that is an orphan-message-free subtyping relation such that . We then use exactly the same proof as that of the second part (the only if part) of the proof of Proposition 3.4 to establish a correspondance between judgements , such that , and pairs in (see the construction of the corresponding pair in the proof of Proposition 3.4). Since includes only pairs that satisfy the constraint in item of -bounded Asynchronous Subtyping relation definition (Definition 2.11) requiring context to be -bounded; and since any judgment such that implies there is in a corresponding pair , with differing from just for the level of internal unfoldings, we have that reachable judgments cannot be such that: , by possibly applying / rules, and due to not satisfying the requirement about the input context to be -bounded in the rule Out. This because the difference in unfolding levels between and (inside judgment and the corresponding pair in ) is not significant: the -boundedness of context is established both in the rule Out and in item of definition after unfolding all recursions occurring before the first output of every possible branch.
This observation makes it possible to carry out the proof as in Proposition 3.4, hence to show that there exist no , such that . \qed
B.3 Proof of Proposition 3.10
We start by providing the proof of the first part of Proposition 3.10, i.e. finiteness of for single-out session types , as a separate preliminary lemma, then we move to proving the second part, i.e. decidability of .
Lemma B.1
Given a single-out session type , is finite.
Proof. We now define a finite set of session types , and then we prove that it satisfies all the constraints in Definition 3.9. Hence by definition, from which finiteness of follows.
It is not restrictive to assume that all the recursion variables of are distinct: let be such variables. We consider the rewriting variables . Let be such that occurs in ; let be with that replaces ; and similarly let be with that replaces each occurrence of and . We now consider the rewriting rules and . Given one of the above term containing rewriting variables, we denote with the session type obtained by repeated application of the rewriting rules in the following way: if occurs inside a subterm apply , otherwise apply . We now define another closure function on sets of terms : \mathsf{subterms}(\mathcal{S})=\{S^{\prime}|\mbox{S^{\prime}S\in\mathcal{S}}\}. Consider finally . We have that is finite and it satisfies all the constraints in Definition 3.9. \qed
We now report some definitions and preliminary results used in the proof of Proposition 3.10 concerning the second part about decidability of for single-out session types . We introduce the relation : intuitively, if and are terms in capable of anticipating the same infinite sequence of outputs. For instance, assuming that the following and belong to , for some session type , we have that because they can anticipate the sequence of outputs and , indefinitely.
Definition B.2
Let be a single-out session type. A relation over is an relation if implies: there exist such that and , with for all and . We say that if there is an relation such that .
Notice that itself is an relation because, obviously, the union of two relations is an relation and is finite. Moreover notice that, given a term , all terms (with ) for which are always such that as well (because never unfolds recursions occurring inside terms ). Finally, notice that is decidable in that it is a relation over , which is a finite set.
Definition B.3
* is the field of , that is the set of session types such that there exists with or .*
Lemma B.4
* is an equivalence relation on .*
Proof. The reflexive, symmetric and transitive closure of an relation is an relation, hence this holds true for as well. \qed
Lemma B.5
Let . We have that if and only if .
Proof. We prove the two implications separately, starting from the if part, e.g. by assuming . By Lemma B.4 we have . We now prove by induction on that for every there exists such that is defined. If it is sufficient to consider where (with and that exist by Definition B.2). Consider now that is defined. By Definition 3.8, we have with . As , we can apply times Definition B.2 to conclude that , for every . This guarantees the existence of the input contexts , session types , and label such that such that . This implies that it is possible to define hence also by taking .
We now move to the only if part assuming that there exists an infinite label sequence such that, for every , is defined. Let be the minimal relation such that and: , for any , implies . We now show that above is an relation. Considered any in , we have that there exists , with , such that, for some , , we have: and , with for all and . This holds, according to the definition of : for by taking and by observing that pairs because they are added to in the case ; for any added to in the case , by taking and by observing that pairs because they are among the pairs that are added to in the case . \qed
Proposition 3.10.
Given a single-out session type , is finite and it is decidable whether .
Proof. Direct consequence of Lemmas B.1, Lemma B.5 and the finiteness of . \qed
B.4 Proof of Theorem 3.11
Theorem 3.11 states that, for single-out session types and , the algorithm provided by indeed terminates. The proof is based on characterizing terms such that for any judgment reached by the algorithm. In particular, we show that any such term can be obtained by anticipating a sequence of output labels in a term belonging to the finite set . This preliminary result is proved by means of the following lemma and corollary.
Lemma B.6 states that given a type at the right hand side of a judgement reachable during the execution of our algorithm, i.e. for some initial types and , the type (and the types in ) can be obtained from the initial type (or one of the types in ) by means of anticipation of a sequence of output labels, i.e. for all there exist and a sequence of labels such that . There is only one case in which this property is not guaranteed to hold, namely, when the last applied rule in is . As a counter-example, consider for instance
[TABLE]
where denotes application of the sequence of rules RecL, , Out and . We have that the last type is different from , for every and every sequence of labels .
Lemma B.6
Consider two single-out session types and . Given a judgement such that , in such a way that the final rule applied is not , we have that for all there exist and a sequence of labels such that .
Proof. By induction on the length of the sequence of rule applications . In the base case we have . Consider now . Obviously with because .
In the inductive case we proceed by case analysis on the last rule application . We have two possible cases:
We can apply the induction hypotheses on the judgement . Hence for all there exist and a sequence of labels such that . Consider now . We proceed by cases on the applied rule.
For the rules In, and Out with we have that hence also because if then by definition of .
If the rule is Out with we have that with and such that and is the label of the anticipated output. We limit our analysis to the case in which (in the other cases we can proceed as above). This happens if is obtained by applying rule of Definition 3.9 to remove some but not all the inputs in front of one of the output anticipated in . Consider now the term being like but without the output anticipation. Formally, is defined as follows. Denoted with we know that for all there exists a such that . This means that is . Hence, being reachable from by consuming some inputs of the input context only, we have that there exists such that is , where, considered the hole corresponding to the hole , we have that and . Therefore, the previously mentioned term is , where, considered corresponding to , we have that . We conclude by observing that , hence there exist and such that . But , hence proving the thesis.
- 2.
We cannot apply the induction hypotheses on the judgement because the rule used to obtain is . As cannot be applied in sequence, it is surely possible to apply the induction hypothesis on the previous judgement such that . Then we have that for all we have with and a sequence of labels . We also have that the rule applied in is Out, which is the only rule that can applied after . Let be the label of the output involved in the application of the Out rule. Consider now . We consider two possible cases:
- (a)
is obtained from by consuming inputs present in the input context used in the last application of the rule Out. Consider now obtained from by consuming the same inputs and performing the needed unfoldings. Obviously : hence, by induction hypothesis, with . We have hence proving the thesis.
- (b)
is obtained from by consuming strictly more than a sequence of inputs present in the input context used in the last application of the rule Out. This means that where is a term starting with an output that populates one of the holes of in . But the terms starting with an output that can occur in , assuming , are already in . In fact the rules do not perform transformations under outputs, excluding those strictly performed by top level unfoldings. Hence , which implies from which the thesis trivially follows (because ). \qed
Corollary B.7
Consider two single-out session types and . Given a judgement such that and a pair , we have that for some and a sequence of labels .
Proof. Let and consider the sequence of rule applications that preceeds the application of the rule that introduces in . Such rule must be one of RecL, or : hence on the judgement it is possible to apply one of these three rules. Since after the application of a rule the uniqe applicable rule is Out, we have the guarantee that the last rule in is not . Hence it is possible to apply Lemma B.6, from which the thesis directly follows. \qed
Theorem 3.11.
Given two single-out session types and , the algorithm applied to the initial judgement terminates.
Proof. Assume by contraposition that there exists single-out session types and such that the algorithm applied to the initial judgement does not terminate. This means that there exists an infinite sequence of rule applications . Within this infinite sequence, there are infinitely many applications of the unfolding rules RecL, or , that implies the existence of infinitely many distinct pairs that are introduced in the environment (assuming that ranges over the instances of application of such rules). All these pairs are distinct, otherwise the precedence of the Asmp rule would have blocked the algorithm. It is obvious that the distinct r.h.s. are finitely many, because every , which is a finite set. On the contrary, the distinct are infinitely many, but Corollary B.7 guarantees that for each of them, there exists and a sequence of labels such that .
Due to the finiteness of the possible and , there exists and such that there exists an infinite subsequence of such that and . It is not restrictive to consider for every . The presence of infinitely many distinct for which is defined, guarantees . Moreover, this guarantees also the possibility to define an infinite subsequence such that . We now consider the leaf sets . These sets are defined on a finite domain because the subterms of such types starting with a recursive definition or an output, and preceded by inputs only, are taken from . This because the algorithm does not apply transformations under recursive definitions or outputs, excluding the effect of the standard top level unfolding of previous recursive definitions, which is considered in the definition of . Hence there are only finitely many distinct , that guarantees the existence of such that . Consider now the judgement . We know that , , , , , and . Hence it is possible to apply to such judgement the rule . As has priority, it should be applied on this judgement thus blocking the sequence of rule applications. But this contradicts the initial assumption of non termination of the algorithm. \qed
B.5 Proof of Theorem 3.12
The soundness Theorem 3.12 states that the algorithm reaches if and only if the procedure does so. This is proved in the following by resorting to some preliminary definitions and results.
In Definition B.2 we have defined the relation among types that have the same infinite sequence of outputs that can be anticipated. But, in order to have a decidable relation, we had to limit to types belonging to the set . Now, we define a more general relation applicable to types having (once unfolded) the following shape: any possible input context with holes filled with single outputs having a continuation belonging to . This extension of the is necessary because the execution of the subtyping algorithm can generate new terms (as a consequence of output anticipations) having this specific shape.
Definition B.8
Let , be single-out session types. We say that if there exist such that and , with for all and .
Moreover, is the field of .
Notice that, all terms , with and , with , are in . Moreover, notice that is obviously an equivalence relation on .
Lemma B.9
Let and for some . We have that .
Proof. We have to show that there exist for which we have , with for all . We denote , with . For any , with , considered and terms with such that , we have that . This is easily shown by induction on , applying the definition of (the base case is directly derived from ). The case yields the desired result. \qed
Lemma B.10
Let and . We have that .
Proof. It is easy to see that implies . This because causes a leaf belonging to both and to yield the same new set of leaves in both and . By definition of we have that exist such that , with for all . Similarly, there exist such that , with for all . From the fact that we have that and that: for all , with , there exists , with , such that ; and, vice versa, for all , with , there exists , with , such that . Therefore we conclude that . \qed
In order to prove Theorem 3.12 we also need to consider a simplified subtyping procedure, whose judgments are denoted by , and the notions of IO steps, blocking judgments and blocking paths.
Simplified Subtyping Procedure. We here denote by the judgements of the subtyping procedure that is defined exactly as our procedure (defined in Section 3.1 and based on applications of the rules therein over judgments of the form ) with the only difference that the Asmp rule is removed (i.e. the subtyping procedure whose transitions were denoted by in the proof of Proposition 3.4). Since, in the absence of the Asmp rule the content of environment is never accessed for reading, it has no actual effect on the procedure (on rule applications) and can be removed as well, together with updates on such environment made by the rules. As a consequence we will denote judgments just by for some and . Here, differently from the notation used in the proof of Proposition 3.4, since we adopt a new notation for judgements, we will simply use: to denote that the latter can be obtained from the former by one rule application. Finally, as usual, denotes that there is no rule that can be applied to the judgement .
Definition B.11
*A blocking judgment , denoted by , is a judgment such that, for some we have: by applying rules RecL, and only. *
Definition B.12
An IO step , denoted by , with is a sequence of rule applications such that the last applied rule is an In (in the case , where is the input label singling out which of the rule premises we consider), or an Out rule (in the case , where is the output label singling out which of the rule premises we consider) and all other rule applications concern RecL, and rules only.
Definition B.13
, with , is a blocking path for judgment if there exist such that (where and in the case ).
Lemma B.14
Let and , be such that: and . If , with , is a blocking path for then there exists an long prefix of , with , that is a blocking path for .
Proof.
The proof is by induction on .
We start by proving the base case . That is , i.e. for some we have: by applying rules RecL, and only.
We first observe that is not possible for any . This because: if we had for some , then with for some , hence we would have that also ; and if we had for some , then, since , we would have that also .
Therefore, given that it is not possible that by applying rules RecL, and only (because otherwise would not be defined), we conclude (notice that the number of times a RecL, or is applicable to a judgment is finite because we do not have unguarded recursion and cannot be consecutively applied for more than one time).
We now consider the induction case for blocking path of length .
We first consider the case for some . Given that is defined and that , we deduce that is: either (possibly preceded by some recursion operators), for some ; or (possibly preceded by some recursion operators), for some terms and labels such that for some . In the first case we have , hence the the lemma trivially holds; in the second case we have and we proceed with the proof. We have that there exist , , such that and , with and . In particular is obtained from by removing all its initial (single-)outputs (and intertwined recursions, that are unfolded) until the first input is reached, which is also removed, thus yielding for the such that . This corresponds, in the definition of (Definition 3.9), to repeatedly applying, starting from , rules and and finally rule , thus yielding . Notice that is the sequence of labels of the initial outputs that were removed during this procedure and that, obviously, .
Now, in order to be able to apply the induction hypothesis we have also to show that . We observe that . This holds because is a term, with for some , possibly preceded by some recursion operators, and from the following observations: obviously, for any , it holds ; and . In the same way, we have .
It is therefore possible to apply the induction hypothesis to and that possesses the shorter blocking path .
Finally, we consider the case for some . Since and , we have that also . In particular, we have that there exists such that and , where, obviously, . Moreover, since it is immediate to show (by applying the definitions of , and ) that also .
It is therefore possible to apply the induction hypothesis to and that possesses the shorter blocking path . \qed
Theorem 3.12.
*Given two single-out session types and , we have that there exist such that if and only if there exist such that . *
Proof. We consider the two implications separately starting from the if part. Assume that . In this sequence of rule applications, the new rule is never used otherwise the sequence would terminate successfully by applying such a rule. Hence, by applying the same sequence of rules, we have with , and . We have that , otherwise if a rule could be applied to this judgement, the same rule could be applied also to thus contradicting the assumption .
We now move to the only if part. Assume that and that, by contradiction, does not hold.
From (since in this sequence of rule applications the Asmp rule is never used, otherwise the sequence would terminate successfully by applying such a rule), by applying the same sequence of rules, we have .
We now observe that, since we assumed (by contradiction) that we do not get the error when using the procedure, there must exist at least a triple such that: (and correspondingly because the Asmp and rules, that would have led to successful termination, cannot have been applied), successfully terminates by applying the Asmp or rule, and has a blocking path.
Let us now consider one of such triples (possessing the above stated properties) that has a blocking path of minimal length, i.e. there is no other triple of the kind above such that has a shorter blocking path. Let be such a path. Since the Asmp or rule is applied to , we have (in the case of Asmp this is obtained by Corollary B.7).
We now consider such that was used in the premise of Asmp or rule: in the case of the Asmp rule, in the case of the rule. Moreover, let us also consider to be the environment such that , where is the judgment to which the rule that caused to be inserted in the environment was applied.
We now observe that there exists a long prefix of , with , that is a blocking path for . This is obvious in the case ; it is due to Lemma B.14 in the case : we obtain as needed by such a Lemma from the statements in the premise of rule and by applying Lemmas B.5, B.9 and B.10.
Since we assumed (by contradiction) that does not hold, this would be possible only if there existed a triple such that: there is a sequence of rule applications that is a prefix of the sequence of rule applications of the blocking path for ; and successfully terminates by applying the Asmp or rule. Notice that such a sequence should necessarily include the application of, at least, an In rule (causing the algorithm to branch), because otherwise (given that ) we could not have that successfully terminates by applying the Asmp or rule.
However the existence of such a triple is not possible, because would have a long blocking path with (being such a path strictly shorter than that of ), thus violating the minimality assumption about the blocking path length of the triple. \qed
Appendix C Proofs of Section 4
C.1 Proof of Lemma 4.4 and Theorem 4.5
We here prove Lemma 4.4 and Theorem 4.5 that show undecidability of by reduction from the bounded non termination problem.
Lemma 4.4.
Given a queue machine and an input , it is undecidable whether does not terminate and is bound on .
Proof. We first prove that boundedness is undecidable. If, by contraposition, boundedness was decidable, termination could be decided by first checking boundedness, and then perform a finite state analysis of the queue machine behaviour. More precisely, termination on bounded queue machines can be decided by forward exploration of the reachable configurations until a terminating configuration is found, or a cycle is detected by reaching an already visited configuration.
We now conclude by observing that given a queue machine and the input , it is not possible to decide whether does not terminate and is bound on . Assume by contraposition one could decide the above property of queue machines. Then boundedness could be decided as follows: transform in a new machine that behaves like plus an additional special symbol which is enqueued every time it is dequeued; boundedness of on input can be decided by checking the above property on and input (in fact never terminates and is bound on if and only if is bound on ). \qed
Theorem 4.5.
Given a queue machine M=(Q,\Sigma,\Gamma,\,s,\delta)x[![{s}]!]^{\emptyset}{\leq_{\mathsf{bound}}}[![{x$}]!]Mx$.*
Proof. We need a preliminary result: given , if then we also have that . In fact, assuming and , we have . Having , by one application of item 4. of Definition 2.4, one application of item 3., and applications of item 2., we can conclude that .
We now observe that if is not bound on we have that it is not possible to have [\![{s}]\!]^{\emptyset}{\leq_{\mathsf{bound}}}[\![{x\}]!][![{s}]!]^{\emptyset}{\leq_{\mathsf{bound}}}[![{x$}]!][![{q^{\prime}}]!]^{\emptyset}{\leq_{\mathsf{bound}}}[![{\gamma^{\prime}}]!](q^{\prime},\gamma^{\prime})Mxkk(q^{\prime},\gamma^{\prime})[![{q^{\prime}}]!]^{\emptyset}[![{\gamma^{\prime}}]!]kk$ to the input context.
Now we observe that [\![{s}]\!]^{\emptyset}{\leq_{\mathsf{bound}}}[\![{x\}]!]Mx. Following the *(Only if part)* of the proof of Theorem 3.1 [[10](#bib.bib10)] stating the undecidability of {<!!<}[![{s}]!]^{\emptyset}{\leq_{\mathsf{bound}}}[![{x$}]!]MMx$ in the light of the previous observation.
Consider now that does not terminate. As in the (If part) of the same proof mentioned above, we define \mathcal{C}=\{(q_{i},\gamma_{i})\ |\ (s,x\)=(q_{0},\gamma_{0})\rightarrow_{M}(q_{1},\gamma_{1})\rightarrow_{M}\cdots\rightarrow_{M}(q_{i},\gamma_{i}),i\geq 0}\mathcal{R}$ on types:
[TABLE]
Following the proof of Theorem 3.1 [10] we show that this relation is an asynchronous subtyping relation. Moreover boundedness of on guarantees boundedness on the length of the reachable queue contents , that implies boundedness of the depth of the input contexts of the r.h.s. of all the pairs in . This proves that [\![{s}]\!]^{\emptyset}{\leq_{\mathsf{bound}}}[\![{x\}]!]$. \qed
C.2 Proof of Theorem 4.8
Theorem 4.8 states that, given a single consuming queue machine and an input , termination of on is undecidable. The theorem is proved by resorting to Turing completeness of queue machines. In order to do this we preliminarily provide an encoding from a queue machine into a single-consuming queue machine and two lemmas that guarantee that, given a queue machine and an input , terminates on if and only if the single-consuming queue machine terminates on .
Definition C.1
Let M=(\{q_{1},..,q_{n}\},\Sigma,\Gamma,\,s,\delta)#\Gamma[![{M}]!]({q_{1},..,q_{n},q_{1}^{\prime},..,q_{n}^{\prime}},\Sigma,\Gamma\cup{#},$,s,\delta^{\prime})\delta^{\prime}$ defined as follows:
* if *
- 2.
* if with *
- 3.
**
- 4.
* if *
- 5.
* if with *
- 6.
**
Given a configuration of , we denote with the configuration where , if , or , if , while is obtained from by removing each instance of the special symbol .
Example C.2
We now comment the construction that, given a queue machine , returns a single-consuming queue machine. As an example, consider M=(\{q_{1},q_{2}\},\{a\},\{a,\},$,q_{1},\delta)\delta\delta(q_{1},a)=(q_{2},\epsilon)\delta(q_{1},$)=(q_{1},$)\delta(q_{2},a)=(q_{2},a)\delta(q_{2},$)=(q_{2},\epsilon)"a"a$[![{M}]!]=({q_{1},q_{2},q^{\prime}{1},q^{\prime}{2}},{a},{a,$,#},$,q_{1},\delta^{\prime})\delta^{\prime}\delta^{\prime}(q_{1},a)=(q^{\prime}{2},\epsilon)\delta^{\prime}(q{1},$)=(q_{1},$)\delta^{\prime}(q_{1},#)=(q_{1}^{\prime},\epsilon)\delta^{\prime}(q_{2},a)=(q_{2},a)\delta^{\prime}(q_{2},$)=(q_{2}^{\prime},\epsilon)\delta^{\prime}(q_{2},#)=(q_{2}^{\prime},\epsilon)\delta^{\prime}(q^{\prime}{1},a)=(q{2},#)\delta^{\prime}(q^{\prime}{1},$)=(q{1},$)\delta^{\prime}(q^{\prime}{1},#)=(q{1},#)\delta^{\prime}(q^{\prime}{2},a)=(q{2},a)\delta^{\prime}(q^{\prime}{2},$)=(q{2}^{\prime},#)\delta^{\prime}(q^{\prime}{2},#)=(q{2},#)"a"a$$#[![{M}]!]q_{i}^{\prime}$ that always enqueue some symbol.
Lemma C.3
Let M=(Q,\Sigma,\Gamma,\,s,\delta)x\in\Sigma^{}(s,x$)\rightarrow_{M}^{}(q,\gamma)(q^{\prime},\gamma^{\prime})(s,x$)\rightarrow_{[![{M}]!]}^{}(q^{\prime},\gamma^{\prime}){!!{{(q^{\prime},\gamma^{\prime})}}!!}=(q,\gamma)$.*
Proof. By induction on the number of steps in the sequence (s,x\)\rightarrow_{M}^{*}(q,\gamma)[![{M}]!]#[![{M}]!]#M$. \qed
Lemma C.4
Let M=(Q,\Sigma,\Gamma,\,s,\delta)x\in\Sigma^{}(s,x$)\rightarrow_{[![{M}]!]}^{}(q,\gamma)(s,x$)\rightarrow_{M}^{}{!!{{(q,\gamma)}}!!}$.*
Proof. By induction on the number of steps in the sequence (s,x\)\rightarrow_{[![{M}]!]}^{*}(q,\gamma)\gamma#M(q^{\prime},\gamma^{\prime}){!!{{(q,\gamma)}}!!}={!!{{(q^{\prime},\gamma^{\prime})}}!!}$. \qed
Theorem 4.8.
Given a single consuming queue machine and an input , the termination of on is undecidable.
Proof. The thesis directly follows from the Turing completeness of queue machines, and the two above Lemmas that guarantee that given a queue machine and an input , terminates on if and only if the single-consuming queue machine terminates on . This is guaranteed by the fact that if reaches a configuration with the queue containing only instances of , it is guaranteed to eventually terminate by emptying the queue. \qed
C.3 Proof of Theorem 4.11
Theorem 4.11 states that a single-consuming queue machine does not terminate if and only if the types obtained by the encoding of Figure 4 are in the relation. The proof is done by separately showing, as preliminary lemmas, both implications (one in each direction) to hold.
Concerning such lemmas and their proof, we need to introduce some preliminary notation. Given a sequence of queue symbols , we denote with the set of session types that can be obtained from by independently replacing each occurrence, inside it, of the term defined in Figure 4 with , for some sequence of labels with (distinguished label sequences can be considered for replacing different occurrences of inside ). Observe that is well defined because can anticipate every possible sequence of outputs. Moreover, for simplicity, we will consider the asynchronous subtyping relation instead of . Nevertheless, we will apply such relation on types that have all their choices labeled on the same set of labels, hence the two relations obviously coincide on such types.
Lemma C.5
Given a single-consuming queue machine \Gamma,\,s,\delta)x\in\Sigma^{}{[![![{s}]!]!]}^{\emptyset}{\leq}[![![{x$}]!]!]Mx$.*
Proof. We need a preliminary result: given and a term , if then there exists such that . In fact, assuming and , we have . Consider now . Having , by one application of item 4. of Definition 2.4, one application of item 3., and applications of item 2., we can conclude that there exists such that .
We now prove the thesis by showing that assuming that accepts we have {[\![\![{s}]\!]\!]}^{\emptyset}\not\!\!{\leq}\ [\![\![{x\}]!]!]Mx(s,x$)\rightarrow_{M}^{}(q,\epsilon){[![![{s}]!]!]}^{\emptyset}{\leq}[![![{x$}]!]!](s,x$)\rightarrow_{M}^{}(q,\epsilon)S^{\prime}\in[![![{\epsilon}]!]!]{u}{[![![{q}]!]!]}^{\emptyset}{\leq}S^{\prime}{[![![{q}]!]!]}^{\emptyset}is a recursive definition that upon unfolding begins with an input that implies (according to items 4. and 3. of Definition [2.4](#S2.Thmproposition4)) that alsoS^{\prime}[![![{\epsilon}]!]!]=\mu\mathbf{t}\oplus\Big{{}A:&\Big{(}\big{{}A:\mathbf{t}\big{}}\uplus\big{{}A^{\prime}:T^{\prime\prime}\big{}}{A^{\prime}\in\Gamma\setminus{A}}\Big{)}\Big{}}_{A\in\Gamma}$. \qed
Lemma C.6
Given a single-consuming queue machine \Gamma,\,s,\delta)x\in\Sigma^{}Mx{[![![{s}]!]!]}^{\emptyset}{\leq}[![![{x$}]!]!]$.*
Proof. Assuming that does not accept we show that {[\![\![{s}]\!]\!]}^{\emptyset}{\leq}[\![\![{x\}]!]!](s,x$)=(q_{0},\gamma_{0})\rightarrow_{M}(q_{1},\gamma_{1})\rightarrow_{M}\cdots\rightarrow_{M}(q_{i},\gamma_{i})\rightarrow_{M}\cdots\mathcal{C}\mathcal{C}={(q_{i},\gamma_{i})\ |\ i\geq 0}\mathcal{R}T^{\prime}T^{\prime\prime}are as in Figure [4](#S4.F4),T_{0}=\oplus{A:T^{\prime\prime}}{A\in\Gamma}T{n}=&{A:T_{n-1}}_{A\in\Gamma}$:
[TABLE]
We have that the above is an asynchronous subtyping relation because each of the pairs satisfies the conditions in Definition 2.4 thanks to the presence of other pairs in . We can conclude observing that (s,x\)\in{\mathcal{C}}({[![![{q}]!]!]}^{\emptyset},[![![{x$}]!]!]){\mathcal{R}}{[![![{q}]!]!]}^{\emptyset}{\leq}[![![{x$}]!]!]$. \qed
Theorem 4.11.
- Given a single consuming queue machine M=(Q,\Sigma,\Gamma,\,s,\delta)x\in\Sigma^{}{[![![{s}]!]!]}^{\emptyset}{\leq}_{\mathsf{tin,tout}}[![![{x$}]!]!]Mx$.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] 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. doi:10.1007/B Fb 0053567 . · doi ↗
- 2[2] K. Honda, N. Yoshida, M. Carbone, Multiparty asynchronous session types, in: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2008), 2008, pp. 273–284. doi:10.1145/1328438.1328472 . · doi ↗
- 3[3] S. Lindley, J. G. Morris, Embedding session types in Haskell, in: Proceedings of the 9th International Symposium on Haskell (Haskell 2016), 2016, pp. 133–145. doi:10.1145/2976002.2976018 . · doi ↗
- 4[4] N. Ng, N. Yoshida, Static deadlock detection for concurrent Go by global session graph synthesis, in: Proceedings of the 25th International Conference on Compiler Construction (CC 2016), 2016, pp. 174–184. doi:10.1145/2892208.2892232 . · doi ↗
- 5[5] T. B. L. Jespersen, P. Munksgaard, K. F. Larsen, Session types for Rust, in: Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming, WGP@ICFP 2015, 2015, pp. 13–22. doi:10.1145/2808098.2808100 . · doi ↗
- 6[6] K. Honda, N. Yoshida, M. Carbone, Multiparty asynchronous session types, J. ACM 63 (1) (2016) 9. doi:10.1145/2827695 . · doi ↗
- 7[7] S. J. Gay, M. Hole, Subtyping for session types in the pi calculus, Acta Inf. 42 (2-3) (2005) 191–225. doi:10.1007/s 00236-005-0177-z . · doi ↗
- 8[8] 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. doi:10.1145/2643135.2643138 . · doi ↗