Denotational and Operational Preciseness of Subtyping: A Roadmap

Abstract

The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in object-oriented programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different points of view: denotational and operational. The former preciseness is based on the denotation of a type, which is a mathematical object describing the meaning of the type in accordance with the denotations of other expressions from the language. The latter preciseness has been recently developed with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected.

The present paper shows that standard proofs of operational preciseness imply denotational preciseness and gives an overview on this subject.

Partly supported by COST IC1201 BETTY and DART bilateral project between Italy and Serbia.

M. Dezani-Ciancaglini—Partly supported by EU H2020-644235 Rephrase project, EU H2020-644298 HyVar project, ICT COST Actions IC1402 ARVI and Ateneo/CSP project RunVar.

S. Ghilezan et al.—Partly supported by ON 174026 and III 44006 projects of the Ministry of Education, Science and Technological Development, Republic of Serbia.

N. Yoshida—Partly supported by EPSRC EP/K011715/1, EP/K034413/1, and EP/L00058X/1, and EU Project FP7-612985 UpScale.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

A subtyping relation is a pre-order (reflexive and transitive relation) on types that validates the principle: if $\sigma$ is a subtype of $\tau$ (notation $\sigma \le \tau$), then a term of type $\sigma$ may be provided whenever a term of type $\tau$ is needed; see Pierce [35] (Chap. 15) and Harper [20] (Chap. 23).

In this paper we will discuss key properties of subtyping, i.e. denotational and operational preciseness. We will introduce these notions in the next two paragraphs.

Denotational Preciseness. A usual approach to preciseness of subtyping for a calculus is to consider the interpretation of a type $\sigma$ (notation $[\![\sigma ]\!]$) to be a set that describes the meaning of the type in accordance with the denotations of the terms of the calculus, in general a subset of the domain of a model of the calculus.

• A subtyping relation is denotationally sound when $\sigma \le \tau$ implies $[\![\sigma ]\!]\subseteq [\![\tau ]\!]$ and denotationally complete when $[\![\sigma ]\!]\subseteq [\![\tau ]\!]$ implies $\sigma \le \tau$.

• A subtyping relation is denotationally precise if it is both denotationally sound and denotationally complete.

This well-established powerful technique is applied to the pure $\lambda$-calculus with arrow and intersection types by Barendregt et al. [4], to a call-by-value $\lambda$-calculus with arrow, intersection and union types by van Bakel et al. [2] and by Ishihara and Kurata [25], to a wide class of calculi with arrow, union and pair types by Vouillon [38], and to a concurrent $\lambda$-calculus by Dezani and Ghilezan [15]. More recently denotational preciseness was studied for binary sessions [11] and synchronous multiparty sessions [16].

Operational Preciseness. Operational soundness is just the key principle mentioned at the beginning of this section: if $\sigma \le \tau$, then a term of type $\sigma$ may be provided whenever a term of type $\tau$ is needed. As a simple example $\textsf {nat} \le \textsf {real}$ and a natural number can always play the role of a real number. Operational completeness requires that, if $\sigma \not \le \tau$, then there are

• a context expecting a term of type $\tau$ and

• a term of type $\sigma$

such that this context filled with this term behaves badly. As a simple example $\textsf {nat}\not \le \textsf {bool}$, the negation $\lnot$ requires a boolean argument and the term $\lnot 5$ is stuck.

To define formally operational soundness and completeness we need a boolean predicate $\mathsf {bad}$ on terms, standard typing judgements $\varGamma \vdash M:\sigma$ (where $\varGamma$ is a mapping from variables to types and M is a term) and evaluation contexts C.

• A subtyping relation is operationally sound when $\sigma \le \tau$ implies that if (for some $\rho$) $x:\tau \vdash C[x]:\rho$ and $\vdash M:\sigma$, then $\mathsf {bad}(C[M])$ is false, for all C and M.

• A subtyping relation is operationally complete when $\sigma \not \le \tau$ implies that $x:\tau \vdash C[x]:\rho$ and $\vdash M:\sigma$ and $\mathsf {bad}(C[M])$, for some $\rho$, C and M.

• A subtyping relation is operationally precise if it is both operationally sound and operationally complete.

Operational soundness immediately follows from the subject reduction theorem, when the subtyping is used in a subsumption rule. A general methodology to prove operational completeness is the following one:

• [Step 1] Characterise the negation of the subtyping relation by inductive rules.

• [Step 2] For each type $\sigma$ define a characteristic context $C_\sigma$, which behaves well when filled with terms of type $\sigma$.

• [Step 3] For each type $\sigma$ define a characteristic term $M_\sigma$, which has only the types greater than or equal to $\sigma$.

• [Step 4] Show that if $\sigma \not \le \tau$, then $\mathsf {bad}(C_\tau [M_\sigma ])$.

These four steps are the guideline of the proofs in the literature, as we will illustrate in this paper.

Background and Related Work. Ligatti et al. [27] first define operational preciseness of subtyping and apply it to subtyping iso-recursive types. They consider a typed $\lambda$-calculus enriched with naturals, reals, pair and case constructors/destructors, and roll/unroll. The predicate $\mathsf {bad}(M)$ holds when M reduces to a stuck term, i.e. to an irreducible term which is not a value. They propose new algorithmic rules for subtyping iso-recursive types and show that they are operationally precise.

Dezani and Ghilezan [15] adapt the ideas of Ligatti et al. [27] to the setting of the concurrent $\lambda$-calculus with intersection and union types of [14]. For the operational preciseness they take the view that evaluation of well-typed terms always terminates. This means that the predicate $\mathsf {bad}$ coincides with non termination. In this calculus applicative contexts are enough. Notably, soundness and completeness are made more operational by asking that some applications converge instead of being typable. To sum up, the definition of operational preciseness becomes:

• A subtyping $\le$ is operationally precise when $\sigma \le \tau$ if and only if there are no closed terms M, N such that ML converges for all closed terms L of type $\tau$ and N has type $\sigma$ and MN diverges.

The main result of this paper is the operational preciseness of the subtyping induced by the standard set theoretic interpretation of arrow, intersection and union types.

Chen et al. [11] first give a general formulation of preciseness for session calculi, where processes are typed by sets of pairs (channels, session types) [22]. The session types prescribe how the channels can be used for communications. The calculus of processes includes an $\mathsf {error}$ process and $\mathsf {bad}(P)$ holds when process P reduces to $\mathsf {error}$. The typing judgements for closed processes are of the form $\vdash P \triangleright \{a:T\}$, assuring that the process P has a single free channel a whose type is T. The judgement $\vdash C[a:T] \triangleright \emptyset$ means that filling the hole of C with any process P typed by a : T produces a well-typed closed process. We get:

A subtyping $\le$ is precise when, for all session types T and S:

$$ T \leqslant S \iff \left( \begin{array}{@{}l@{}} \text {there do not exist } C \text { and } P \text { such that:}\\ { \vdash C[a:S] \triangleright \emptyset } \text { and } { \vdash P \triangleright \{a:T\}} \text { and } C[P] \longrightarrow ^* \mathsf {error}\end{array} \right) $$

When the only-if direction ($\Rightarrow$) of this formula holds, we say that the subtyping is sound; when the if direction ($\Leftarrow$) holds, we say that the subtyping is complete. The first result of [11] is that the well-known session subtyping, the branching-selection subtyping [13], is sound and complete for the synchronous dyadic calculus. Next, the authors show that in the asynchronous calculus, this subtyping is incomplete for type-safety: that is, there exist session types T and S such that T can safely be considered as a subtype of S, but $T \le S$ is not derivable by the subtyping. They propose an asynchronous subtyping system (inspired by [32]) which is sound and complete for the asynchronous dyadic calculus. The method gives a general guidance to design rigorous channel-based subtypings respecting desired safety properties.

Dezani et al. [16] consider the synchronous version [26] of the multiparty session calculus in [12, 23]. For the operational preciseness they take the view that well-typed sessions never get stuck. Therefore the predicate $\mathsf {bad}$ is true for processes which cannot reduce, but contain pending communications. The preciseness of the branching-selection subtyping [13] is shown using a novel notion of characteristic global type.

A framework which is closely related to the above described works is semantic subtyping. In semantic subtyping, each type is interpreted as the set of values having that type and subtyping is subset inclusion between type interpretations [10]. This gives a precise subtyping as soon as the calculus allows to distinguish operationally values of different types.

Semantic subtyping was first proposed by Castagna and Benzaken through the development of the Duce project [17]. Duce is a modern XML-oriented functional language. Distinctive features of Duce are a powerful pattern matching, first class functions, over-loaded functions, a very rich type system (with arrow, sequence, pair, record, intersection, union, difference type constructs), precise type inference for patterns and error localisation, and a natural interpretation of types as sets of values. It is enriched also with some important implementation aspects: in particular, a dispatch algorithm that demonstrates how static type information can be used to obtain very efficient compilation schemas.

Semantic subtyping has been also studied in [8] for a $\pi$-calculus with a patterned input and in [9] for a session calculus with internal and external choices and typed input. Types are built using a rich set of type constructors including union, intersection and negation: they extend IO-types in [8] and session types in [9]. Semantic subtyping is precise for the calculi of [8, 9, 17], thanks to the type case constructor in [17], and to the blocking of inputs for values of “wrong” types in [8, 9].

Bonsangue et al. [6] recently have developed an elegant coalgebraic foundation for coinductive types, which gives a sound and complete characterisation of semantic subtyping in terms of inclusion of maximal traces.

Outline. Sections 2 and 3 deal with typed extensions of $\lambda$-calculus, and discuss preciseness of iso-recursive and intersection/union types, respectively. Session calculi are considered in Sects. 4 and 5. Section 4 is devoted to synchronous and asynchronous binary types, Sect. 5 instead to synchronous multiparty types. Section 6 shows how the existence of characteristic terms as defined in [Step 3] implies denotational preciseness. Section 7 concludes with some directions for further work.

2 Iso-Recursive Types

In [27] the authors consider a typed $\lambda$-calculus enriched with naturals, reals, pair and case constructors/destructors, and roll/unroll. The syntax of types, terms and values of this calculus (dubbed $L^{\rightarrow \mu }_{+\times }$) is given in Fig. 1.

Fig. 1.

Types, terms and values of $L^{\rightarrow \mu }_{+\times }$.

The operational semantics of $L^{\rightarrow \mu }_{+\times }$ is call-by-value. The operator $\textsf {succ}$ reduces only when the argument is a natural and $\textsf {unroll}$ is the left inverse of $\textsf {roll}$. The remaining reduction rules are standard.

The most interesting subtyping rule tells that $\mu \mathbf t .\sigma$ is a subtype of $\mu \mathbf t .\tau$ if we can derive from $\mu \mathbf t .\sigma \le \mu \mathbf t .\tau$ that their unfolded versions are in the subtype relation. More precisely:

$$\begin{aligned} \frac{\varSigma ,\mu \mathbf t .\sigma \le \mu \mathbf t .\tau \vdash \sigma [\mu \mathbf t .\sigma /\mathbf t ]\le \tau [\mu \mathbf t .\tau /\mathbf t ]}{\varSigma \vdash \mu \mathbf t .\sigma \le \mu \mathbf t .\tau }{} \end{aligned}$$

where $\varSigma$ is a set of subtyping judgments. The type system is as expected, in particular $\textsf {roll}$ and $\textsf {unroll}$ correspond to fold and unfold of recursive types.

The core of the completeness proof is the construction of characteristic contexts and terms for closed types, as discussed in the Introduction. This construction is delicate since some types (for example $\mu \mathbf t .\mathbf t$) are not inhabited. The type inhabitation is decidable and every non inhabited type is subtype of all types. Figure 2 shows some of the characteristic contexts and terms for the types of [27]. Notice that in that paper they are used in the proof without grouping them in a unique definition. We omit the case of the sum type being similar to that of the product type. Also, the characteristic contexts and terms for recursive types are missing, since they are quite tricky depending on the external constructor obtained by unfolding the types.

Fig. 2.

Characteristic contexts and terms, where $M=(\textsf {fun}~g(y:\tau ):\tau _2~=M_{\tau _2})(C_{\tau _1}[x])$ and $\tau$ is the type of $C_{\tau _1}[x]$ when x has type $\tau _1$.

For example $\textsf {nat}\rightarrow \textsf {nat}\not \le \textsf {real}\rightarrow \textsf {nat}$. The characteristic context of $\textsf {real}\rightarrow \textsf {nat}$ is $C_{\textsf {nat}}[[~]M_{\textsf {real}}]=\textsf {succ}([~]2.5)$. The characteristic term of $\textsf {nat}\rightarrow \textsf {nat}$ is

$$\begin{aligned} \textsf {fun}~f(x:\textsf {nat}):\textsf {nat}~=~ (\textsf {fun}~g(y:\textsf {nat}):\textsf {nat}~=~M_{\textsf {nat}})(C_{\textsf {nat}}[x]), \end{aligned}$$

i.e.

$$\begin{aligned} \textsf {fun}~f(x:\textsf {nat}):\textsf {nat}~=~ (\textsf {fun}~g(y:\textsf {nat}):\textsf {nat}~=~5)(\textsf {succ}~x). \end{aligned}$$

The term $C_{\textsf {real}\rightarrow \textsf {nat}}[M_{\textsf {nat}\rightarrow \textsf {nat}}]$ is then

$$\begin{aligned} \textsf {succ}((\textsf {fun}~f(x:\textsf {nat}):\textsf {nat}~=~ (\textsf {fun}~g(y:\textsf {nat}):\textsf {nat}~=~5)(\textsf {succ}~x)) 2.5). \end{aligned}$$

This term reduces to

$$\begin{aligned} \textsf {succ}((\textsf {fun}~g(y:\textsf {nat}):\textsf {nat}~=~5)(\textsf {succ}~2.5)) \end{aligned}$$

which is stuck, since $\textsf {succ}~2.5$ is stuck.

The main result of [27] is:

Theorem 1

The subtyping of $L^{\rightarrow \mu }_{+\times }$ is operationally precise.

3 Intersection and Union Types

In this section, we present and discuss the results from [15] on denotational and operational preciseness of the subtyping relation in the setting of the concurrent $\lambda$-calculus with intersection and union types (dubbed $\lambda _{\oplus \Vert }$) introduced in [14]. The syntax of types, terms, values, and total values of this calculus is given in Fig. 3. The only atomic type is the universal type $\omega$. There are both call-by-name variables (ranged over by x) and call-by-value variables (ranged over by v). The constructor $\oplus$ is the non-deterministic choice and the constructor $\Vert$ is the parallel operator.

Fig. 3.

Types, terms, values, and total values of $\lambda _{\oplus \Vert }$.

The reduction relation formalises the behaviour of a machine which evaluates in a synchronous way parallel compositions, until a value is produced. Partial values, i.e. values which are not total, can be further evaluated, and this is essential for applications of a call-by-value abstraction (rule $(\beta _v\Vert )$). The reduction rules which enable this behaviour are the following

$(\mu _v)$ $\displaystyle \frac{N \longrightarrow N' ~~~ N \not \in \mathsf{Val}}{(\lambda v.M) N \longrightarrow (\lambda v.M)N'}$   $(\beta _v\Vert )$ $\displaystyle \frac{V \longrightarrow V' ~~~~~ V \in \mathsf{Val}}{(\lambda v . M)V \longrightarrow M[V/v]\Vert (\lambda v . M)V'}$

According to [14] a term is convergent if all reduction paths reach values.

The type system with intersection and union types is dually reflecting the conjunctive and disjunctive operational semantics of $\Vert$ and $\oplus$. The subtyping relation on Type, the set of all types, is the smallest pre-order such that

• 1. $\langle Type, \le \rangle$ is a distributive lattice, where $\wedge$ is the meet, $\vee$ is the join, $\omega$ is the top;

• 2. the arrow satisfies

  • (a) $\sigma \rightarrow \omega \le \omega \rightarrow \omega$;

  • (b) $(\sigma \rightarrow \rho )\wedge (\sigma \rightarrow \tau ) \le \sigma \rightarrow \rho \wedge \tau$;

  • (c) $\sigma \ge \sigma ', \tau \le \tau '\Rightarrow \sigma \rightarrow \tau \le \sigma '\rightarrow \tau '$.

Notice that the standard axiom $(\sigma \rightarrow \rho )\wedge (\tau \rightarrow \rho )\le \sigma \vee \tau \rightarrow \rho$ [2, 25] is unsound for $\lambda _{\oplus \Vert }$, as proven in [14].

Regarding operational preciseness, divergent terms are the ones that are not convergent and the predicate $\mathsf {bad}$ coincides with divergence. Closed convergent and divergent terms are completely characterised by the types $\omega \rightarrow \omega$ and $\omega$, respectively [14].

As said in the Introduction, it is enough to consider applicative context, that we call test tems. Figure 4 gives test and characteristic terms, where $\mathbf{I}=\lambda x.x$ and $\varOmega =(\lambda x.xx)(\lambda x.xx)$. For example ${M_{\omega \rightarrow \omega }}=\lambda x. \varOmega$ and ${N_{\omega \rightarrow \omega }}=\lambda v. \mathbf{I}$. More interestingly ${M_{(\omega \rightarrow \omega )\rightarrow \omega \rightarrow \omega }}=\lambda x. ((\lambda v. \mathbf{I})x)(\lambda y. \varOmega )$ applied to a term returns $\lambda y. \varOmega$ only if the term reduces to a value. Similarly ${N_{(\omega \rightarrow \omega )\rightarrow \omega \rightarrow \omega }}=\lambda v. (\lambda v'.\mathbf{I})(v(\lambda x. \varOmega ))$ applied to a term which reduces to a value, first applies this term to $\lambda x. \varOmega$, and then reduces to $\mathbf{I}$ only if the result of this application reduces to a value too.

The key property of test terms is:

• if M is a closed term, then $N_\sigma M$ converges if and only if M has type $\sigma$.

As a consequence $\sigma \not \le \tau$ implies the divergence of ${N_{\tau }}{M_{\sigma }}$, i.e. $\mathsf {bad}({N_{\tau }}{M_{\sigma }})$.

Fig. 4.

Test and characteristic terms.

The denotational preciseness of this subtyping is obtained for the standard set-theoretic interpretation of arrow, intersection and union types. The key tool is the existence of characteristic terms, as shown in Sect. 6.

To sum up, the main result in [15] is:

Theorem 2

(Denotational and Operational Preciseness).

• 1. The subtyping of the $\lambda _{\oplus \Vert }$-calculus is operationally precise.

• 2. The subtyping of the $\lambda _{\oplus \Vert }$-calculus is denotationally precise.

4 Binary Session Types

This section presents results from [11] stating that the well-known branching-selection subtyping (defined in Fig. 7) is precise for the synchronous session calculus. As it happens that this subtyping is incomplete for type-safety for the asynchronous session calculus, the authors propose an asynchronous subtyping relation and prove that it is precise for the asynchronous session calculus.

4.1 Synchronous Session Calculus

A binary session is a series of interactions between two parties, possibly with branching and recursion, and serves as a unit of abstraction for describing communication protocols. The syntax of the synchronous session calculus is given in Fig. 5. The input process $\sum \limits _{i\in I} u{?}l_i(x_i).P_i$ waits on channel $u$ for a label $l_i$ and a channel to replace $x_i$ inside $P_i$ ($i\in I$). The output process sends on channel $u$ the label $l$ and the channel $u'$. The process is a recursive agent and $X\langle \tilde{u}\rangle$ is a recursive variable. The process $( \nu ab ) P$ is a restriction which binds two channels, $a$ and $b$ in $P,$ making them co-channels, i.e. allowing them to communicate.

Fig. 5.

Syntax of synchronous processes.

Fig. 6.

Types and characteristic synchronous processes.

Operational semantics is given by a reduction relation between the synchronous processes. The main rule is

It describes the communication between an output ($a{!}l_k\langle c\rangle .P$) and an input ($\sum _{i\in I} b{?}l_i(x_i).Q_i$) at two co-channels a and b, where the label $l_k$ is selected and channel c replaces $x_k$ into the k-th input branch ($Q_k$). Other rules are standard.

The synchronous session calculus includes an $\mathsf {error}$ process and $\mathsf {bad}(P)$ holds when process $P$ reduces to $\mathsf {error}.$ There are four kinds of processes which generate $\mathsf {error}$: a session with mismatch between corresponding output and input labels, a session where one of two co-channels is missing, a session where two co-channels are both subjects of outputs, and a session where two co-channels are both subjects of inputs.

The syntax of synchronous session types is given in Fig. 6. As usual session duality [22] plays an important rôle for session types. The function $\overline{T}$, defined below, yields the dual of the session type T.

The type system is the standard one for session calculi, see e.g. [13]. The subtyping relation is given in Fig. 7, where the double line in rules indicates that the rules are interpreted coinductively [35] (Chap. 21). The type system enjoys the property of subject reduction, which implies operational soundness of the synchronous subtyping.

Fig. 7.

Synchronous subtyping.

Fig. 8.

Negation of synchronous subtyping.

It can be verified that the relation $\not \trianglelefteq ,$ presented in Fig. 8, is the negation of the synchronous subtyping.

The characteristic process offering communication T on identifier u for the synchronous calculus, denoted by $\mathsf {P}(u,T)$, is given in Fig. 6.

For type $S$ and channel $b,$ the characteristic context is defined as

$$ C_{S,b}= [\;] \mathbin {|}{\mathbf {\mathsf{{P}}}}_{}(b,\overline{S}). $$

Finally, it can be proven that $T\not \leqslant S$ implies

$$ \mathsf {bad}( ( \nu ab ) C_{S,b}[{\mathbf {\mathsf{{P}}}}_{}(a,T)])= \mathsf {bad}( ( \nu ab ) ( {\mathbf {\mathsf{{P}}}}_{}(a,T) \mathbin {|}{\mathbf {\mathsf{{P}}}}_{}(b,\overline{S}) )). $$

For example (omitting $\mathbf {0}$ and final ) let and , then $T\not \le S$. By definition

We get and

Then

$$\begin{array}{lll} ( \nu ab ) C_{S,b}[{\mathbf {\mathsf{{P}}}}_{}(a,T)]&{}=&{} ( \nu ab ) ( {\mathbf {\mathsf{{P}}}}_{}(a,T) \mathbin {|}{\mathbf {\mathsf{{P}}}}_{}(b,\overline{S}))\\ {} &{}=&{} ( \nu ab ) ( ( \nu c_1d_1 ) (a{!}l_1\langle c_1\rangle .a?l_2(x))~|~ ( \nu c_2d_2 ) (b{!}l_2\langle c_2\rangle .b?l_1(y)))\end{array}$$

and this last process reduces to $\mathsf {error}$, since the two co-channels are both subjects of outputs.

In [11], the main result for synchronous subtyping is:

Theorem 3

(Preciseness for Synchronous Session Calculus). The synchronous subtyping relation is operationally precise for the synchronous session calculus.

4.2 Asynchronous Session Calculus

The asynchronous session calculus is obtained from the rules for the synchronous ones by extending the synchronous calculus of Fig. 5 with queues:

A queue is used by channel $a$ to enqueue messages in $h$ and by channel $b$ to dequeue messages from $h$.

Reduction rules for asynchronous processes are obtained from the rules for the synchronous processes by replacing [r-com-sync] with the following two rules:

In presence of queues, reduction to $\mathsf {error}$ includes deadlocks, that are sessions with inputs waiting to dequeue messages from queues that will stay empty, and orphan messages, that are messages in queues that will never be received.

To define asynchronous subtyping, the notion of asynchronous context is introduced, that is a sequence of branchings containing indexed holes:

$$ \mathscr {A}{:}{:} = [ \; ]^{n} \ | \ \& _{i\in I} {?}l_i(S_i).\mathscr {A}_i. $$

The asynchronous subtyping relation is obtained by extending synchronous subtyping relation by the rule:

Using this rule we get for example , which does not hold in the synchronous subtyping, as shown in previous subsection.

The negation rules of asynchronous subtyping are the rules of Fig. 8 excluding rule [n-selbra-sync], extended by the rules of Fig. 9.

Fig. 9.

Negation of asynchronous subtyping.

The characteristic process offering communication T on identifier u for the asynchronous calculus, denoted by ${\mathbf {\mathsf{{P}}}}_{}(u,T)$, is defined as in Fig. 6, but for the case of T being $\bigoplus _{i\in I} {!}l_i\langle S_i\rangle .T_i,$ which becomes:

For type $S$ and channel $b,$ the characteristic context is defined as

For $T\not \leqslant S,$ we can prove that there are $T'\leqslant T$ and $S'\ge S$ such that

Notice that $S'\ge S$ if and only if $\overline{S'}\leqslant \overline{S}$.

For example let and , then $T\not \le S$. By definition

We also get and

Then

where the reduction to $\mathsf {error}$ is due to the mismatch between the input label $l_1$ and the label $l_2$ of the message.

In [11], the main result for asynchronous subtyping is:

Theorem 4

(Preciseness for Asynchronous Subtyping). The asynchronous subtyping relation is operationally precise for the asynchronous session calculus.

5 Multiparty Session Types

In [16] the authors show operational and denotational preciseness of the subtyping introduced in [13] for a simplification of the synchronous multiparty session calculus in [26]. The calculus is obtained by eliminating both shared channels for session initiations and session channels for communications inside sessions.

A multiparty session is a series of interactions between a fixed number of participants, possibly with branching and recursion, and serves as a unit of abstraction for describing communication protocols. The syntax of processes and multiparty sessions is given in Fig. 10. The values are natural numbers $\mathsf {n}$, integers $\mathsf {i}$, and boolean values $\mathsf {true}$ and $\mathsf {false}$. The expressions $\mathsf {e}$ are variables or values or expressions built from expressions by applying the operators $\mathtt{succ}, \mathtt{neg}, \lnot , \oplus ,$ or the relation $>.$ The input process $\mathsf{p} ? \ell (x) .P$ waits for an expression with label $\ell$ from participant $\mathsf{p}$ and the output process $\mathsf{q} ! \ell (\mathsf {e}). Q$ sends the value of expression $\mathsf {e}$ with label $\ell$ to participant $\mathsf{q}$. The external choice $P+ Q$ offers to choose either P or Q. The process $\mu X.P$ is a recursive process. An equi-recursive view is taken, not distinguishing between a process $\mu X.P$ and its unfolding $P\{\mu X.P/X\}$. If $\mathsf{p} \triangleleft P$ is well typed (see typing rules in [16]), then participant $\mathsf{p}$ does not occur in process $P$, since we do not allow self-communications.

Fig. 10.

Processes and multiparty sessions.

Fig. 11.

Sorts, global types and multiparty session types.

The computational rules of multiparty sessions are closed with respect to the structural congruence (defined as expected) and reduction contexts (empty and parallel composition). Here we recall only the main rule [r-comm] which states that participant $\mathsf{q}$ sends the value $\mathsf {v}$ choosing label $\ell _j$ to participant $\mathsf{p}$ which offers inputs on all labels $\ell _i$ with $i\in I$.

The value $\mathsf {v}$ of expression $\mathsf {e}$ (notation $\mathsf {e} \downarrow \mathsf {v}$) is as expected, see [16]. The successor operation $\mathtt{succ}$ is defined only on natural numbers, the negation $\mathtt{neg}$ is defined on integers (and then also on natural numbers), and $\lnot$ is defined only on boolean values. The internal choice $\mathsf {e}_1\oplus \mathsf {e}_2$ evaluates either to the value of $\mathsf {e}_1$ or to the value of $\mathsf {e}_2$.

In order to define the operational preciseness of subtyping it is crucial to formalise when a multiparty session contains communications that will never be executed.

Definition 1

A multiparty session $\mathscr {M}$ is stuck if $\mathscr {M}\not \equiv \mathsf{p} \triangleleft \mathbf {0}$ and there is no multiparty session $\mathscr {M}'$ such that $\mathscr {M}\longrightarrow \mathscr {M}'.$ A multiparty session $\mathscr {M}$ gets stuck, notation $\mathtt{stuck}(\mathscr {M}),$ if it reduces to a stuck multiparty session.

A stuck multiparty session is a bad multiparty session, i.e. $\mathsf {bad}(\mathscr {M})=\mathtt{stuck}(\mathscr {M}).$

The type system is the simplification of that in [26] due to the new formulation of the calculus. Figure 11 contains syntax of sorts, global types and session types.

Global types describe the whole conversation scenarios of multiparty sessions. Session types correspond to projections of global types on the individual participants.

Subsorting on sorts is the minimal reflexive and transitive closure of the relation induced by the rule: . Subtyping $\leqslant$ on session types takes into account the contra-variance of inputs, the covariance of outputs, and the standard rules for intersection and union. Figure 12 gives the coinductive subtyping rules.

Fig. 12.

Subtyping of multiparty session types.

Fig. 13.

Negation of subtyping of multiparty session types.

The proof of operational soundness of subtyping follows from the subsumption rule and the safety theorem of the type system.

The proof of operational completeness comes in four steps as stated in Introduction.

The characterisation of the negation of the subtyping is given in Fig. 13.

The characteristic process ${\mathscr {P}}({\mathsf T})$ of type ${\mathsf T}$ is defined in Fig. 14 by using the operators $\mathtt{succ}$, $\mathtt{neg}$, and $\lnot$ to check if the received values are of the right sort and exploiting the correspondence between external choices and intersections, conditionals and unions.

Fig. 14.

Characteristic processes.

The authors define the characteristic global type ${\mathscr {G}}({\mathsf T},\mathsf{p})$ of type ${\mathsf T}$ for participant $\mathsf{p}$, that describes the communications between $\mathsf{p}$ and all participants which occur in${\mathsf T}$ (notation $\mathtt {pt}\{{\mathsf T}\}$). Moreover, after each communication involving $\mathsf{p}$ and some $\mathsf{q}\in \mathtt {pt}\{{\mathsf T}\}$, participant $\mathsf{q}$ starts a cyclic communication involving all participants in $\mathtt {pt}\{{\mathsf T}\}$ both as receivers and senders. The characteristic context for $\mathsf{p} \triangleleft {\mathscr {P}}({\mathsf T})$ is built using the characteristic global type of type ${\mathsf T}$ for participant $\mathsf{p}$.

We do not give here the definitions of characteristic global types and characteristic contexts, we only show an example. Let ${\mathsf T}=\mathsf{p}_1!\ell _1(\mathtt {nat}).\mathsf{p}_2!\ell _2(\mathtt {nat})$ and ${\mathsf T}'=\mathsf{p}_2!\ell _2(\mathtt {nat}).\mathsf{p}_1!\ell _1(\mathtt {nat})$. Clearly ${\mathsf T}\not \le {\mathsf T}'$ and ${\mathscr {P}}({\mathsf T})=\mathsf{p}_1 ! \ell _1(5). \mathsf{p}_2 ! \ell _2(5)$. The characteristic context for $\mathsf{p} \triangleleft {\mathscr {P}}({\mathsf T})$ is $[~]~|~\mathsf{p}_1 \triangleleft \mathsf{p}_2 ? \ell _2(x) ...~|~\mathsf{p}_2 \triangleleft \mathsf{p} ? \ell _2(x) ...$ and the process

$$\begin{aligned} \mathsf{p} \triangleleft \mathsf{p}_1 ! \ell _1(5). \mathsf{p}_2 ! \ell _2(5) ~|~\mathsf{p}_1 \triangleleft \mathsf{p}_2 ? \ell _2(x) ...~|~\mathsf{p}_2 \triangleleft \mathsf{p} ? \ell _2(x) ... \end{aligned}$$

is stuck, since participant $\mathsf{p}$ wants to send a message to participant $\mathsf{p}_1$, who instead is ready to receive a message from participant $\mathsf{p}_2$, who in turn expects a message from participant $\mathsf{p}$.

The main result of [16] is:

Theorem 5

The synchronous multiparty session subtyping is operationally precise.

6 Characteristic Terms for Denotational Preciseness

It is standard [11, 15, 16, 21] to interpret a type $\sigma$ as the set of closed terms typed by $\sigma$, i.e.

$$\begin{aligned}{}[\![\sigma ]\!]=\{M~ \mid ~\vdash M: \sigma \} \end{aligned}$$

In this case denotational soundness immediately follows from the subsumption rule. Moreover, the existence of characteristic terms as defined in [Step 3] at page 3 implies denotational completeness. By definition characteristic terms enjoy the following key property:

$$\begin{aligned}{\vdash M_\sigma :\tau \ \text {implies}\ \sigma \leqslant \tau .} \end{aligned}$$

We get denotational completeness, since if $\sigma \not \leqslant \tau$, then $M_\sigma \in [\![\sigma ]\!]$, but $M_\sigma \not \in [\![\tau ]\!]$.

Theorem 6

(Denotational Preciseness). The existence of characteristic terms for a subtyping relation implies its denotational preciseness.

This theorem implies the denotational preciseness of the subtypings which are shown to be operationally precise in previous sections. In particular the denotational preciseness of $L^{\rightarrow \mu }_{+\times }$ is new, since Ligatti et al. [27] only consider operational preciseness.

7 Conclusion

The present paper discusses some recent results of preciseness for subtyping of typed functional and concurrent calculi.

Operational completeness requires that all empty (i.e. not inhabited) types are less than all inhabited types. This makes unfeasible an operationally complete subtyping for the pure $\lambda$-calculus, both in the case of polymorphic types [28] and of intersection and union types. In fact inhabitation is undecidable for polymorphic types being equivalent to derivability in second order logic, while [37] shows undecidability of inhabitation for intersection types, which implies undecidability of inhabitation for intersection and union types.

An interesting open problem we plan to study is an extension of $\lambda$-calculus enjoying operational preciseness for the decidable subtypings between polymorphic types discussed in [28, 36].

The formulation of preciseness along with the proof methods and techniques described in this paper could be useful to examine other subtypings and calculi. Our future work includes the applications to higher-order processes [29–31], polymorphic types [7, 18, 19], fair subtypings [33, 34] and contract subtyping [3]. We plan to use the characteristic processes in typecheckers for session types. More precisely, the error messages can show processes of given types when type checking fails. One interesting problem is to find the necessary and sufficient conditions to obtain completeness of the generic subtyping [24]. Such a characterisation would give preciseness for the many type systems which are instances of [24]. The notion of subtyping for session types is clearly connected with that of type duality. Various definitions of dualities are compared in [5], and we plan to investigate if completeness of subtyping can be used in finding the largest safe duality.

A last question we plan to investigate is whether preciseness of subtyping is meaningful for object-oriented calculi [1].