# Circular Proofs as Session-Typed Processes:
A Local Validity Condition

Farzaneh Derakhshan  Philosophy Department, Carnegie Mellon University,
Pittsburgh, PA, 15213 USA<EMAIL_ADDRESS>and  Frank Pfenning
Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, 15213
USA<EMAIL_ADDRESS>
###### Abstract.

Proof theory provides a foundation for studying and reasoning about
programming languages, most directly based on the well-known Curry-Howard
isomorphism between intuitionistic logic and the typed lambda-calculus. More
recently, a correspondence between intuitionistic linear logic and the
session-typed pi-calculus has been discovered. In this paper, we establish an
extension of the latter correspondence for a fragment of substructural logic
with least and greatest fixed points. We describe the computational
interpretation of the resulting infinitary proof system as session-typed
processes, and provide an effectively decidable local criterion to recognize
mutually recursive processes corresponding to valid circular proofs as
introduced by Fortier and Santocanale. We show that our algorithm imposes a
stricter requirement than Fortier and Santocanale’s guard condition, but is
local and compositional and therefore more suitable as the basis for a
programming language.

###### Key words and phrases:

Circular proofs, session types, subsingleton logic, fixed points, progress,
termination, linear logic, substructural logic

## Introduction

Proof theory provides a solid ground for studying and reasoning about
programming languages. This logical foundation is mostly based on the well-
known Curry-Howard isomorphism [How69] that establishes a correspondence
between natural deduction and the typed $\lambda$-calculus by mapping
propositions to types, proofs to well-typed programs, and proof reduction to
computation. More recently, Caires et al. [CP10, CPT16] introduced a
correspondence between intuitionistic linear logic [GL87] and the session-
typed $\pi$-calculus [Wad12] that relates linear propositions to session
types, proofs in the sequent calculus to concurrent processes, and cut
reduction to computation. In this paper, we expand the latter for a fragment
of intuitionistic linear logic called _subsingleton logic_ in which the
antecedent of each sequent consists of at most one formula. We consider the
sequent calculus of subsingleton logic with least and greatest fixed points
and their corresponding rules [DP16, DeY20]. We closely follow Fortier and
Santocanale’s [FS13] development in singleton logic, where the antecedent
consists of exactly one formula.

Fortier and Santoconale [FS13, San02d] extend the sequent calculus for
singleton logic with rules for least and greatest fixed points. A naive
extension, however, loses the cut elimination property so they call
derivations _pre-proofs_. _Circular pre-proofs_ are distinguished as a subset
of derivations which are regular in the sense that they can be represented as
finite trees with loops. They then impose a validity condition (which we call
the _FS guard condition_) on pre-proofs to single out a class of pre-proofs
that satisfy cut elimination. Moreover, they provide a cut elimination
algorithm and show that it locally terminates on derivations that satisfy the
guard condition. In addition, Santocanale and Fortier [FS13, San02d, San02a,
San02b] introduced categorical and game semantics for interpreting cut
elimination in singleton logic.

In a related line of research, Baelde et al. [BDS16, Bae12] add least and
greatest fixed points to the sequent calculus for the multiplicative additive
fragment of linear logic (MALL) that results in the loss of the cut
elimination property. They also introduced a validity condition to distinguish
circular proofs from infinite pre-proofs. Using Büchi automata, Doumane
[Dou17] showed that the validity condition for identifying circular proofs in
MALL with fixed points is PSPACE decidable. Nollet et al. [NST18] introduced a
polynomial time algorithm for locally identifying a stricter version of
Baelde’s condition in MALL with fixed points.

In this paper, we study (mutually) recursive session-typed processes and their
correspondence with circular pre-proofs in subsingleton logic with fixed
points. We introduce an algorithm to check a stricter version of the FS guard
condition. Our algorithm is local in the sense that we check validity of each
process definition separately, and it is stricter in the sense that it accepts
a proper subset of the proofs recognized by the FS guard condition. We further
introduce a synchronous computational semantics of cut reduction in
subsingleton logic with fixed points in the context of session types, based on
a key step in Fortier and Santocanale’s cut elimination algorithm, which is
compatible with prior operational interpretations of session-typed programming
languages [TCP13]. We show preservation and a strong version of the progress
property that ensures that each valid process communicates along its left or
right interface in a finite number of steps. A key aspect of our type system
is that validity is a compositional property (as we generally expect from type
systems) so that the composition of valid programs defined over the same
signature are also valid and therefore also satisfy strong progress. In other
words, we identify a set of processes such that their corresponding
derivations are not only closed under cut elimination, but also closed under
cut introduction (i.e. strong progress is preserved when processes are joined
by cut).

In the session type system, a singleton judgment $A\vdash B$ is annotated as
$x:A\vdash\mathtt{P}::(y:B)$ which is understood as: process $\mathtt{P}$ uses
a service of type $A$ offered along channel $x$ by a process on its left and
provides a service of type $B$ along channel $y$ to a process on its right
[DP16]. The left and right interfaces of a process in the session type system
inherit the symmetry of the left and right rules in the sequent calculus. Each
process interacts with other processes along its pair of left and right
interfaces, which correspond to the left and right sides of a sequent. For
example, two processes $\mathtt{P}$ and $\mathtt{Q}$ with the typing
$x:A\vdash\mathtt{P}::(y:B)$ and $y:B\vdash\mathtt{Q}::(z:C)$ can be composed
so they interact with each other using channel $y$. Process $\mathtt{P}$
provides a service of type $B$ and offers it along channel $y$ and process
$\mathtt{Q}$ uses this service to provide its own service of type $C$. This
interaction along channel $y$ can be of two forms: (i) process $\mathtt{P}$
sends a message to the right, and process $\mathtt{Q}$ receives it from the
left, or (ii) process $\mathtt{Q}$ sends a message to the left and process
$\mathtt{P}$ receives it from the right. In the first case, the session type
$B$ is a _positive_ type, and in the second case it is a _negative_ type.
Least fixed points have a positive polarity while greatest fixed points are
negative [LM16]. As we will see in Sections 5 and 6, due to the interactive
nature of computation some types that would be considered “empty” (that is,
have no closed values) may still be of interest here.

DeYoung and Pfenning [DP16, Pfe16] provide a representation of Turing machines
in the session-typed rule system of subsingleton logic with general
equirecursive types. This shows that cut reduction on circular pre-proofs in
subsingleton logic with equirecursive types has the computational power of
Turing machines. Using this encoding on isorecursive types, we show that
recognizing all programs that satisfy a strong progress property is
undecidable, since this property can be encoded as termination of a Turing
machine on a given input. However, with our algorithm, we can decide validity
of a subset of Turing machines represented as session-typed processes in
subsingleton logic with isorecursive fixed points.

In summary, the principal contribution of our paper is to extend the Curry-
Howard interpretation of proofs in subsingleton logic as communicating
processes to include least and greatest fixed points. A circular proof is thus
represented as a collection of mutually recursive process definitions. We
develop a compositional criterion for validity of such programs, which is
local in the sense that each process definition can be checked independently.
Local validity in turn implies a strong progress property on programs and cut
elimination on the circular proofs they correspond to.

The structure of the remainder of the paper is as follows. In Section 1 we
introduce subsingleton logic with fixed points, and then examine it in the
context of session-typed communication (Section 2). We provide a process
notation with a synchronous operational semantics in Section 3 and a range of
examples in Section 4. We then develop a local validity condition through a
sequence of refinements in Sections 5–8. We capture this condition on
infinitary proofs in Section 9 and reduce it to a finitary algorithm in
Section 10. We prove that local validity implies Fortier and Santocanale’s
guard condition (Section 11) and therefore cut elimination. In Section 12 we
explore the computational consequences of this, including the strong progress
property, which states that every valid configuration of processes will either
be empty or attempt to communicate along external channels after a finite
number of steps. We conclude by illustrating some limitations of our algorithm
(Section 13) and pointing to some additional related and future work (Section
14).

##  1\. Subsingleton Logic with Fixed Points

Subsingleton logic is a fragment of intuitionistic linear logic [GL87, CCP03]
in which the antecedent and succedent of each judgment consist of at most one
proposition. This reduces consideration to the additive connectives and
multiplicative units, because the left or right rules of other connectives
would violate this restriction. The expressive power of pure subsingleton
logic is rather limited, among other things due to the absence of the
exponential $!A$. However, we can recover significant expressive power by
adding least and greatest fixed points, which can be done without violating
the subsingleton restriction. We think of subsingleton logic as a laboratory
in which to study the properties and behaviors of least and greatest fixed
points in their simplest nontrivial form, following the seminal work of
Fortier and Santocanale [FS13].

The syntax of propositions follows the grammar

$A,B::=A\oplus B\mid 0\mid A\&B\mid\top\mid 1\mid\bot\mid t$

where $t$ ranges over a set of propositional variables denoting least or
greatest fixed points. Rather than including these directly as $\mu t.\,A$ and
$\nu t.\,A$, we define them in a _signature_ $\Sigma$ which records some
important additional information, namely their relative _priority_.

$\Sigma::=\cdot\mid\Sigma,t=^{i}_{\mu}A\mid\Sigma,t=^{i}_{\nu}A,$

with the conditions that

  * •

if $t=^{i}_{a}A\in\Sigma$ and $t^{\prime}=^{i}_{b}B\in\Sigma$, then $a=b$, and

  * •

if $t=^{i}_{a}A\in\Sigma$ and $t=^{j}_{b}B\in\Sigma$, then $i=j$ and $A=B$.

For a fixed point $t$ defined as $t=^{i}_{a}A$ in $\Sigma$ the subscript $a$
is the polarity of $t$: if $a=\mu$, then $t$ is a fixed point with positive
polarity and if $a=\nu$, then it is of negative polarity. Finitely
representable least fixed points (e.g., natural numbers and lists) can be
represented in this system as defined propositional variables with positive
polarity, while the potentially infinite greatest fixed points (e.g., streams
and infinite depth trees) are represented as those with negative polarity.

The superscript $i$ is the priority of $t$. Fortier and Santocanale
interpreted the priority of fixed points in their system as the order in which
the least and greatest fixed point equations are solved in the semantics
[FS13]. We use them syntactically as central information to determine local
validity of circular proofs. We write $p(t)=i$ for the priority of $t$, and
$\epsilon(i)=a$ for the polarity of propositional variable $t$ with priority
$i$. The condition on $\Sigma$ ensures that $\epsilon$ is a well-defined
function.

The basic judgment of the subsingleton sequent calculus has the form
$\omega\vdash_{\Sigma}\gamma$, where $\omega$ and $\gamma$ are either empty or
a single proposition $A$ and $\Sigma$ is a signature. Since the signature
never changes in the rules, we omit it from the turnstile symbol. The rules of
subsingleton logic with fixed points are summarized in Figure 1, constituting
a slight generalization of Fortier and Santocanale’s. When the fixed points in
the last row are included, this set of rules must be interpreted as
_infinitary_ , meaning that a judgment may have an infinite derivation in this
system.

$A\vdash A$ | $\omega\vdash\gamma\lx@proof@logical@and\omega\vdash AA\vdash\gamma$
---|---
$\omega\vdash A\oplus B\omega\vdash A$ | $\omega\vdash A\oplus B\omega\vdash B$ | $A\oplus B\vdash\gamma\lx@proof@logical@and A\vdash\gamma B\vdash\gamma$
$\omega\vdash A\&B\lx@proof@logical@and\omega\vdash A\omega\vdash B$ | $A\&B\vdash\gamma A\vdash\gamma$ | $A\&B\vdash\gamma B\vdash\gamma$
$\cdot\vdash 1$ | $1\vdash\gamma\cdot\vdash\gamma$ | $\omega\vdash\bot\omega\vdash\cdot$ | $\bot\vdash\cdot$
$\omega\vdash t\lx@proof@logical@and\omega\vdash At=_{\mu}^{i}A\in\Sigma$ | $t\vdash\gamma\lx@proof@logical@and A\vdash\gamma t=_{\mu}^{i}A\in\Sigma$ | $\omega\vdash t\lx@proof@logical@and\omega\vdash At=_{\nu}^{i}A\in\Sigma$ | $t\vdash\gamma\lx@proof@logical@and A\vdash\gamma t=_{\nu}^{i}A\in\Sigma$

Figure 1. Infinitary sequent calculus for subsingleton logic with fixed
points.

Even a cut-free derivation may be of infinite length since each defined
propositional variable may be unfolded infinitely many times. Also, cut
elimination no longer holds for the derivations after adding fixed point
rules. What the rules define then are the so-called _pre-proofs_. In
particular, we are interested in _circular pre-proofs_ , which are the pre-
proofs that can be illustrated as finite trees with loops [Dou17].

Fortier and Santocanale [FS13] introduced a guard condition for identifying
circular _proofs_ among all infinite pre-proofs in singleton logic with fixed
points. Their guard condition states that every cycle should be supported by
the unfolding of a positive (least) fixed point on the antecedent or a
negative (greatest) fixed point on the succedent. Since they allow mutual
dependency of least and greatest fixed points, they need to consider the
priority of each fixed point as well. The supporting fixed point for each
cycle has to be of the highest priority among all fixed points that are
unfolded infinitely in the cycle. They proved that the guarded subset of
derivations enjoys the cut elimination property; in particular, a cut
composing any two guarded derivations can be eliminated effectively.

As an example, the following circular pre-proof defined on the signature
$\mathsf{nat}=^{1}_{\mu}\mathsf{1}\oplus\mathsf{nat}$ depicts an infinite pre-
proof that consists of repetitive application of $\mu R$ followed by $\oplus
R$:

$\cdot\vdash\mathsf{nat}\cdot\vdash\mathsf{1}\oplus\mathsf{nat}\cdot\vdash\mathsf{nat}$

It is not guarded and turns out not to be locally valid either. On the other
hand, on the signature $\mathsf{conat}=_{\nu}^{1}\mathsf{1}\ \&\
\mathsf{conat}$, we can define a circular pre-proof using greatest fixed
points that is guarded and locally valid:

$\cdot\vdash\mathsf{conat}\cdot\vdash\mathsf{1}\&\
\mathsf{conat}\lx@proof@logical@and\cdot\vdash\mathsf{1}\cdot\vdash\mathsf{conat}$

##  2\. Fixed Points in the Context of Session Types

Session types [Hon93, HVK98] describe the communication behavior of
interacting processes. _Binary session types_ , where each channel has two
endpoints, have been recognized as arising from linear logic (either in its
intuitionistic [CP10, CPT16] or classical [Wad12] formulation) by a Curry-
Howard interpretation of propositions as types, proofs as programs, and cut
reduction as communication. In the context of programming, recursive session
types have also been considered [TCP13, LM16], and they seem to fit smoothly,
just as recursive types fit well into functional programming languages.
However, they come at a price, since we abandon the Curry-Howard
correspondence.

In this paper we show that this is not necessarily the case: we can remain on
a sound logical footing as long as we (a) refine general recursive session
types into least and greatest fixed points, (b) are prepared to accept
circular proofs, and (c) impose conditions under which recursively defined
processes correspond to valid circular proofs. General (nonlinear) type theory
has followed a similar path, isolating inductive and coinductive types with a
variety of conditions to ensure validity of proofs. In the setting of
subsingleton logic, however, we find many more symmetries than typically
present in traditional type theories, which appear to be naturally biased
towards least fixed points and inductive reasoning.

Under the Curry-Howard interpretation a subsingleton judgment
$A\vdash_{\Sigma}B$ is annotated as

$x:A\vdash_{\Sigma}\mathtt{P}::(y:B)$

where $x$ and $y$ are two different channels and $A$ and $B$ are their
corresponding session types. One can understand this judgment as: process
$\mathtt{P}$ provides a service of type $B$ along channel $y$ while using
channel $x$ of type $A$, a service that is provided by another process along
channel $x$ [DP16]. We can form a chain of processes
$\mathtt{P}_{0},\mathtt{P}_{1},\cdots,\mathtt{P}_{n}$ with the typing

$\cdot\vdash\mathtt{P}_{0}::(x_{0}:A_{0}),\quad
x_{0}:A_{0}\vdash\mathtt{P}_{1}::(x_{1}:A_{1}),\quad\cdots\quad
x_{n-1}:A_{n-1}\vdash\mathtt{P}_{n}::(x_{n}:A_{n})$

which we write as

$\mathtt{P}_{0}\mid_{x_{0}}\mathtt{P}_{1}\mid_{x_{1}}\cdots\;\mid_{x_{n-1}}\mathtt{P}_{n}$

in analogy with the notation for parallel composition for processes $P\mid Q$,
although here it is not commutative. In such a chain, process
$\mathtt{P}_{i+1}$ uses a service of type $A_{i}$ provided by the process
$\mathtt{P}_{i}$ along the channel $x_{i}$, and provides its own service of
type $A_{i+1}$ along the channel $x_{i+1}$. Process $\mathtt{P}_{0}$ provides
a service of type $A_{0}$ along channel $x_{0}$ without using any services.
So, a process in the session type system, instead of being reduced to a value
as in functional programming, interacts with both its left and right
interfaces by sending and receiving messages. Processes $\mathtt{P}_{i}$ and
$\mathtt{P}_{i+1}$, for example, communicate with each other along the channel
$x_{i}$ of type $A_{i}$: if process $\mathtt{P}_{i}$ sends a message along
channel $x_{i}$ to the right and process $\mathtt{P}_{i+1}$ receives it from
the left (along the same channel), session type $A_{i}$ is called a _positive_
type. Conversely, if process $\mathtt{P}_{i+1}$ sends a message along channel
$x_{i}$ to the left and process $\mathtt{P}_{i}$ receives it from the right
(along the same channel), session type $A_{i}$ is called a _negative_ type. In
Section 4 we show in detail that this symmetric behavior of left and right
session types results in a symmetric behaviour of least and greatest fixed
point types.

In general, in a chain of processes, the leftmost type may not be empty. Also,
strictly speaking, the names of the channels are redundant since every process
has two distinguished ports: one to the left and one to the right, either one
of which may be empty. Because of this, we may sometimes omit the channel
name, but in the theory we present in this paper it is convenient to always
refer to communication channels by unique names.

For programming examples, it is helpful to allow not just two, but any finite
number of alternatives for internal ($\oplus$) and external ($\&$) choice.
Such finitary choices can equally well be interpreted as propositions, so this
is not a departure from the proofs as programs interpretation.

######  Definition 1.

We define session types with the following grammar, where $L$ ranges over
finite sets of labels denoted by $\ell$ and $k$.

$A::={\oplus}\\{\ell:A_{\ell}\\}_{\ell\in
L}\mid{\&}\\{\ell:A_{\ell}\\}_{\ell\in L}\mid 1\mid\bot\mid t$

where $t$ ranges over a denumerable set of type variables whose definition is
given in a signature $\Sigma$ as before. The binary disjunction and
conjunction are defined as $A\oplus B=\oplus\\{\pi_{1}:A,\pi_{2}:B\\}$ and
$A\&B=\&\\{\pi_{1}:A,\pi_{2}:B\\}$, respectively. Similarly, we define
$0=\oplus\\{\\}$ and $\top=\&\\{\\}$.

As a first programming-related example, consider natural numbers in unary form
($\mathsf{nat}$) and infinite streams of natural numbers ($\mathsf{stream}$).

######  Example 2.1 (Natural numbers on demand).

$\displaystyle\mathsf{nat}=^{1}_{\mu}\oplus\\{\mathit{z}:\mathsf{1},\mathit{s}:\mathsf{nat}\\}$
$\displaystyle\mathsf{ctrl}=^{2}_{\nu}\&\\{\mathit{now}:\mathsf{nat},\ \
\mathit{notyet}:\mathsf{ctrl}\\}$

In this example, $\Sigma$ consists of an inductive and a coinductive type;
these are, respectively: (i) the type of natural numbers ($\mathsf{nat}$)
built using two constructors for ${\mathit{zero}}$ and $\mathit{successor}$,
and (ii) a type to demand access to a number if desired ($\mathsf{ctrl}$)
defined using two destructors for $\mathit{now}$ to obtain the number and
$\mathit{notyet}$ to postpone access, possibly indefinitely. Here, the
priorities of $\mathsf{nat}$ and $\mathsf{stream}$ are, respectively, $1$ and
$2$, understood as “ _$\mathsf{nat}$ has higher priority than
$\mathsf{stream}$_”.

######  Example 2.2 (Binary numbers in standard form).

As another example consider the signature with two types with positive
polarity and the same priority: $\mathsf{std}$ and $\mathsf{pos}$. Here,
$\mathsf{std}$ is the type of standard bit strings, i.e., bit strings
terminated with $\$$ without any leading $0$ bits, and $\mathsf{pos}$ is the
type of positive standard bit strings, i.e., all standard bit strings except
$\$$. Note that in our representation the least significant bit is sent first.

$\displaystyle\mathsf{std}=^{1}_{\mu}\oplus\\{\mathit{b0}:\mathsf{pos},\mathit{b1}:\mathsf{std},\$:\mathsf{1}\\}$
$\displaystyle\mathsf{pos}=^{1}_{\mu}\oplus\\{\mathit{b0}:\mathsf{pos},\mathit{b1}:\mathsf{std}\\}$

######  Example 2.3 (Bits and cobits).

$\displaystyle\mathsf{bits}=^{1}_{\mu}\oplus\\{\mathit{b0}:\mathsf{bits},\
\mathit{b1}:\mathsf{bits}\\}$
$\displaystyle\mathsf{cobits}=^{2}_{\nu}\&\\{\mathit{b0}:\mathsf{cobits},\
\mathit{b1}:\mathsf{cobits}\\}$

In a functional language, the type $\mathsf{cobits}$ would be a greatest fixed
point (an infinite stream of bits), while $\mathsf{bits}$ is recognized as an
empty type. However, in the session type system, we treat them in a symmetric
way. $\mathsf{bits}$ is an infinite sequence of bits with positive polarity.
And its dual type, $\mathsf{cobits}$, is an infinite stream of bits with
negative polarity. In Examples 5.9 and 5.10, in Section 5, we further
illustrate the symmetry of these types by providing two recursive processes
having them as their interfaces. Even though we can, for example, write
transducers of type $\mathsf{bits}\vdash\mathsf{bits}$ inside the language, we
cannot write a _valid_ process of type $\cdot\vdash\mathsf{bits}$ that
_produces_ an infinite stream of bits.

##  3\. A Synchronous Operational Semantics

The operational semantics for process expressions under the proofs-as-programs
interpretation of linear logic has been treated exhaustively elsewhere [CP10,
CPT16, TCP13, Gri16]. We therefore only briefly sketch the operational
semantics here. Communication is _synchronous_ , which means both sender and
receiver block until they synchronize. Asynchronous communication can be
modeled using a process with just one output action followed by forwarding
[GV10, DCPT12]. However, a significant difference to much prior work is that
we treat types in an isorecursive way, that is, a message is sent to unfold
the definition of a type $t$. This message is written as $\mu_{t}$ for a least
fixed point and $\nu_{t}$ for a greatest fixed point. The language of process
expressions and their operational semantics presented in this section is
suitable for general isorecursive types, if those are desired in an
implementation. The resulting language then satisfies a weaker progress
property sometimes called _global progress_ (see, for example, [CP10]).

######  Definition 3.4.

Processes are defined as follows over the signature $\Sigma$:

$\begin{aligned} P,Q::=\ \ &{y\leftarrow x}&identity\\\ &\mid(x\leftarrow
P_{x};Q_{x})&cut\\\ &\mid Lx.k;P\mid\mathbf{case}\,Rx\ (\ell\Rightarrow
Q_{\ell})_{\ell\in L}&\&\\{\ell:A_{\ell}\\}_{\ell\in L}\\\ &\mid
Rx.k;P\mid\mathbf{case}\,Lx\ (\ell\Rightarrow Q_{\ell})_{\ell\in
L}&\phantom{something}\oplus\\{\ell:A_{\ell}\\}_{\ell\in L}\\\
&\mid\mathbf{close}\,Rx\mid\mathbf{wait}\,Lx;Q&1\\\
&\mid\mathbf{close}\,Lx\mid\mathbf{wait}\,Rx;Q&\bot\\\ &\mid
Rx.\mu_{t};P\mid\mathbf{case}\,Lx\ (\mu_{t}\Rightarrow P)&t=_{\mu}A\\\ &\mid
Lx.\nu_{t};P\mid\mathbf{case}\,Rx\ (\nu_{t}\Rightarrow P)&t=_{\nu}A\\\
&\mid{y\leftarrow X\leftarrow x}&call\end{aligned}$

where $X,Y,\ldots$ are process variables, and $x,y,\ldots$ are channel names.
In $(x\leftarrow P_{x};Q_{x})$, the variable $x$ is bound and represents a
channel connecting the two processes. Throughout the paper, we may subscript
processes with bound variables if they are allowed to occur in them. In the
programming examples, we may write $y\leftarrow X\leftarrow x;Q_{y}$ instead
of $(y\leftarrow(y\leftarrow X\leftarrow x);Q_{y})$ when a new process
executing $X$ is spawned. The left and right session types a process interacts
with are uniquely labelled with channel names:

$x:A\vdash P::(y:B).$

We read this as

Process $P$ uses channel $x$ of type $A$ and provides a service of type $B$
along channel $y$.

However, since a process might not use any service provided along its left
channel, e.g. $\cdot\vdash P::(y:B),$ or it might not provide any service
along its right channel, e.g. $x:A\vdash Q::(\cdot)$, the labelling of
processes is generalized to be of the form:

$\bar{x}:\omega\vdash P::(\bar{y}:\gamma),$

where $\bar{x}$ ($\bar{y}$) is either empty or $x$ ($y$), and $\omega$
($\gamma$) is empty given that $\bar{x}$ ($\bar{y}$) is empty.

Process definitions are of the form $\bar{x}:\omega\vdash
X=P_{\bar{x},\bar{y}}::(\bar{y}:\gamma)$ representing that variable $X$ is
defined as process $P$. A program $\mathcal{P}$ is defined as a pair $\langle
V,S\rangle$, where $V$ is a finite set of process definitions, and $S$ is the
main process variable.111For the sake of simplicity, we may only refer to
process variables in $V$ when their definition is clear from the context.
Figure 2 shows the logical rules annotated with processes in the context of
session types. This set of rules inherits the full symmetry of its underlying
sequent calculus. They interpret _pre-proofs_ : as can be seen in the rule
Def, the typing rules inherit the infinitary nature of deductions from the
logical rules in Figure 1 and are therefore not directly useful for type
checking.222The rule Def corresponds to forming cycles in the circular
derivations of the system of Figure 1. We obtain a finitary system to check
_circular_ pre-proofs by removing the first premise from the Def rule and
checking each process definition in $V$ separately, under the hypothesis that
all process definitions are well-typed. Since the system is entirely syntax-
directed we may sometimes equate (well-typed) programs with their typing
derivations. This system rules out communication mismatches without forcing
processes to actually communicate along their external channels. In order to
also enforce this the rules need to track additional information (see rules in
Figures 3 (infinitary) and 4 (finitary) in Sections 9 and 10).

All processes we consider in this paper provide a service along their right
channel so in the remainder of the paper we restrict the sequents to be of the
form $\bar{x}:\omega\vdash P::(y:A)$. We therefore do not need to consider the
rules for type $\perp$ anymore, but the results of this paper easily
generalize to the fully symmetric calculus.

$x:A\vdash y\leftarrow x::(y:A)$ | $\bar{x}:\omega\vdash(w\leftarrow P_{w};Q_{w})::(\bar{y}:\gamma)\lx@proof@logical@and\bar{x}:\omega\vdash P_{w}::(w:A)w:A\vdash Q_{w}::(\bar{y}:\gamma)$
---|---
$\bar{x}:\omega\vdash Ry.k;P::(y:\oplus\\{\ell:A_{\ell}\\}_{\ell\in L})\bar{x}:\omega\vdash P::(y:A_{k})\quad(k\in L)$ | $x:\oplus\\{\ell:A_{\ell}\\}_{\ell\in L}\vdash\mathbf{case}\,Lx\ (\ell\Rightarrow P_{\ell})_{\ell\in L}::(\bar{y}:\gamma)\forall\ell\in L\quad x:A_{\ell}\vdash P_{\ell}::(\bar{y}:\gamma)$
$\bar{x}:\omega\vdash\mathbf{case}\,Ry\ (\ell\Rightarrow P_{\ell})_{\ell\in L}::(y:\&\\{\ell:A_{\ell}\\}_{\ell\in L})\bar{x}:\omega\vdash P_{\ell}::(y:A_{\ell})\quad\forall\ell\in L$ | $x:\&\\{\ell:A_{\ell}\\}_{\ell\in L}\vdash Lx.k;P::(\bar{y}:\gamma)k\in L\quad x:A_{k}\vdash P::(\bar{y}:\gamma)$
$\cdot\vdash\mathbf{close}\,Ry::(y:1)$ | $x:1\vdash\mathbf{wait}\,Lx;Q::(\bar{y}:\gamma).\vdash Q::(\bar{y}:\gamma)$
$\bar{x}:A\vdash\mathbf{wait}\,Ry;Q::(y:\bot)\bar{x}:A\vdash Q::\cdot$ | $x:\bot\vdash\mathbf{close}\,Lx::\cdot$
$\bar{x}:\omega\vdash Ry.\mu_{t};P_{y}::(y:t)\lx@proof@logical@and\bar{x}:\omega\vdash P_{y}::(y:A)t=_{\mu}^{i}A$ | $x:t\vdash\mathbf{case}\,Lx\ (\mu_{t}\Rightarrow Q_{x})::(\bar{y}:\gamma)\lx@proof@logical@and x:A\vdash Q_{x}::(\bar{y}:\gamma)t=_{\mu}^{i}A$
$\bar{x}:\omega\vdash\mathbf{case}\,Ry\ (\nu_{t}\Rightarrow P_{y})::(y:t)\lx@proof@logical@and\bar{x}:\omega\vdash P_{y}::(y:A)t=_{\nu}^{i}A$ | $x:t\vdash Lx.\nu_{t};Q_{x}::(\bar{y}:\gamma)\lx@proof@logical@and x:A\vdash Q_{x}::(\bar{y}:\gamma)t=_{\nu}^{i}A$

$\bar{x}:\omega\vdash\bar{y}\leftarrow
X\leftarrow\bar{x}::(\bar{y}:\gamma)\lx@proof@logical@and\bar{x}:\omega\vdash
P_{\bar{x},\bar{y}}::(\bar{y}:\gamma)\bar{u}:\omega\vdash
X=P_{\bar{u},\bar{w}}::(\bar{w}:\gamma)\in V$

Figure 2. Process assignment for subsingleton logic with fixed points
(infinitary).

The computational semantics is defined on configurations

$P_{0}\mid_{\,x_{1}}\cdots\mid_{\,x_{n}}P_{n}$

where $\mid$ is associative and has unit $(\cdot)$ but is not commutative. The
following transitions can be applied anywhere in a configuration:

$\begin{array}[]{lcll}P_{x}\mid_{x}(y\leftarrow
x)\mid_{y}Q_{y}&\mapsto&P_{z}\mid_{z}Q_{z}&\mbox{($z$ fresh), forward}\\\
(x\leftarrow P_{x}\mathrel{;}Q_{x})&\mapsto&P_{z}\mid_{z}Q_{z}&\mbox{($z$
fresh), spawn}\\\
(Rx.k\mathrel{;}P)\mid_{x}\mathbf{case}\,Lx\,(\ell\Rightarrow
Q_{\ell})_{\ell\in L}&\mapsto&P\mid_{x}Q_{k}&\mbox{send label $k\in L$
right}\\\ \mathbf{case}\,Rx\,(\ell\Rightarrow P_{\ell})_{\ell\in
L}\mid_{x}(Lx.k\mathrel{;}Q)&\mapsto&P_{k}\mid_{x}Q&\mbox{send label $k\in L$
left}\\\
\mathbf{close}\,Rx\mid_{x}(\mathbf{wait}\,Lx\mathrel{;}Q)&\mapsto&Q&\mbox{close
channel right}\\\
(\mathbf{wait}\,Rx\mathrel{;}P)\mid_{x}\mathbf{close}\,Lx&\mapsto&P&\mbox{close
channel left}\\\
(Rx.\mu_{t}\mathrel{;}P)\mid_{x}\mathbf{case}\,Lx\,(\mu_{t}\Rightarrow
Q)&\mapsto&P\mid_{x}Q&\mbox{send $\mu_{t}$ unfolding message right}\\\
\mathbf{case}\,Rx\,(\nu_{t}\Rightarrow
P)\mid_{x}(Lx.\nu_{t}\mathrel{;}Q)&\mapsto&P\mid_{x}Q&\mbox{send $\nu_{t}$
unfolding message left}\\\ \bar{y}\leftarrow
X\leftarrow\bar{x}&\mapsto&P_{\bar{x},\bar{y}}&\mbox{where
$\bar{u}:\omega\vdash X=P_{\bar{u},\bar{w}}::(\bar{w}:\gamma)\in
V$}\end{array}$

The forward rule removes process $y\leftarrow x$ from the configuration and
replaces both channels $x$ and $y$ in the rest of the configuration with a
fresh channel $z$. The rule for $x\leftarrow P_{x}\,;Q_{z}$ spawns process
$P_{z}$ and continues as $Q_{z}$. To ensure uniqueness of channels, we need
$z$ to be a fresh channel. For internal choice, $Rx.k;P$ sends label $k$ along
channel $x$ to the process on its right and continues as $P$. The process on
the right, $\mathbf{case}\,Lx\,(\ell\Rightarrow Q_{\ell})$, receives the label
$k$ sent from the left along channel $x$, and chooses the branch with label
$k$ to continue with $Q_{k}$. The last transition rule unfolds the definition
of a process variable $X$ while instantiating the left and right channels
$\bar{u}$ and $\bar{w}$ in the process definition with proper channel names,
$\bar{x}$ and $\bar{y}$ respectively.

##  4\. Ensuring communication and local validity

In this section we motivate our algorithm as an effectively decidable
compositional and local criterion which ensures that a program always
terminates either in an empty configuration or one attempting to communicate
along external channels. By defining type variables in the signature and
process variables in the program, we can generate (mutually) recursive
processes which correspond to circular pre-proofs in the sequent calculus. In
Examples 4.5 and 4.6, we provide such recursive processes along with
explanations of their computational steps and their corresponding derivations.

######  Example 4.5.

Take the signature

$\Sigma_{1}:=\mathsf{nat}=^{1}_{\mu}\oplus\\{\mathit{z}:\mathsf{1},\mathit{s}:\mathsf{nat}\\}.$

We define a process

$\begin{aligned} \cdot\vdash\mathtt{Loop}::(y:\mathsf{nat})\\\ \end{aligned},$

where $\mathtt{Loop}$ is defined as

$\displaystyle y\leftarrow\mathtt{Loop}\leftarrow\cdot=\ $ $\displaystyle
Ry.\mu_{nat};$ $\displaystyle\phantom{lospace}\%\ \textit{send}\ \mu_{nat}\
\textit{to right}$ (i) $\displaystyle\phantom{low}Ry.s;$
$\displaystyle\phantom{lospace}\%\ \textit{send label}\ \mathit{s}\ \textit{to
right}$ (ii)
$\displaystyle\phantom{lows}y\leftarrow\mathtt{Loop}\leftarrow\cdot$
$\displaystyle\phantom{lospace}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\%\
\textit{recursive call}}\ $ (iii)

$\mathcal{P}_{1}:=\langle\\{\mathtt{Loop}\\},\mathtt{Loop}\rangle$ forms a
program over the signature $\Sigma_{1}$. It (i) sends a positive fixed point
unfolding message to the right, (ii) sends the label $\ \mathit{s}$, as
another message corresponding to $\mathit{successor}$, to the right, (iii)
calls itself and loops back to (i). The program runs forever, sending
successor labels to the right, without receiving any fixed point unfolding
messages from the left or the right. We can obtain the following infinite
derivation in the system of Figure 1 via the Curry-Howard correspondence of
the unique typing derivation of process $\mathtt{Loop}$:

$\cdot\vdash\mathsf{nat}\cdot\vdash\oplus\\{\mathit{z}:\mathsf{1},\mathit{s}:\mathsf{nat}\\}\cdot\vdash\mathsf{nat}$

######  Example 4.6.

Define process

$\displaystyle x:\mathsf{nat}\vdash\mathtt{Block}::(y:\mathsf{1})$

over the signature $\Sigma_{1}$ as

$\displaystyle y\leftarrow\mathtt{Block}\leftarrow x=$
$\displaystyle\phantom{small}\mathbf{case}\,Lx\ (\mu_{nat}\Rightarrow$
$\displaystyle\%\ \textit{receive}\ \mu_{nat}\ \textit{from left}$ (i)
$\displaystyle\phantom{smallspac}\mathbf{case}\,Lx$ $\displaystyle\%\
\textit{receive a label}\ \textit{from left}$ (ii)
$\displaystyle\phantom{smallspaceti}(\ z\Rightarrow\mathbf{wait}\,Lx;$
$\displaystyle\%\ \textit{wait for}\ x\ \textit{to close}$ (ii-a)
$\displaystyle\phantom{smallspacetimestwo}\mathbf{close}\,Ry$
$\displaystyle\%\ \textit{close}\ y$ $\displaystyle\phantom{smallspaceti}\mid
s\Rightarrow y\leftarrow\mathtt{Block}\leftarrow x))$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\%\
\textit{recursive call }}$ (ii-b)

$\mathcal{P}_{2}:=\langle\\{\mathtt{Block}\\},\mathtt{Block}\rangle$ forms a
program over the signature $\Sigma_{1}$:
(i) $\mathtt{Block}$ waits, until it receives a positive fixed point unfolding
message from the left, (ii) waits for another message from the left to
determine the path it will continue with:
(a) If the message is a $\ \mathit{z}\ $ label, (ii-a) the program waits until
a closing message is received from the left. Upon receiving that message, it
closes the left and then the right channel.
(b) If the message is an $\ \mathit{s}\ $ label, (ii-b) the program calls
itself and loops back to (i).
Process $\mathtt{Block}$ corresponds to the following infinite derivation:

$\mathsf{nat}\vdash\mathsf{1}\oplus\\{\mathit{z}:\mathsf{1},\mathit{s}:\mathsf{nat}\\}\vdash\mathsf{1}\lx@proof@logical@and\mathsf{1}\vdash\mathsf{1}\cdot\vdash\mathsf{1}\mathsf{nat}\vdash\mathsf{1}$

Derivations corresponding to both of these programs are cut-free. Also no
internal loop takes place during their computation, in the sense that they
both communicate with their left or right channels after finite number of
steps. For process $\mathtt{Loop}$ this communication is restricted to sending
infinitely many unfolding and successor messages to the right. Process
$\mathtt{Block}$, on the other hand, receives the same type of messages after
finite number of steps as long as they are provided by a process on its left.
Composing these two processes as in
$x\leftarrow\mathtt{Loop}\leftarrow\cdot\mid
y\leftarrow\mathtt{Block}\leftarrow x$ results in an internal loop: process
$\mathtt{Loop}$ keeps providing unfolding and successor messages for process
$\mathtt{Block}$ so that they both can continue the computation and call
themselves recursively. Because of this internal loop, the composition is not
acceptable: it never communicates with its left (empty channel) or right
(channel $y$). The infinite derivation corresponding to the composition
$x\leftarrow\mathtt{Loop}\leftarrow\cdot\mid
y\leftarrow\mathtt{Block}\leftarrow x$ therefore should be rejected as
invalid:

$\cdot\vdash\mathsf{1}\lx@proof@logical@and\cdot\vdash\mathsf{nat}\cdot\vdash\oplus\\{\mathit{z}:\mathsf{1},\mathit{s}:\mathsf{nat}\\}\cdot\vdash\mathsf{nat}\mathsf{nat}\vdash\mathsf{1}\oplus\\{\mathit{z}:\mathsf{1},\mathit{s}:\mathsf{nat}\\}\vdash\mathsf{1}\lx@proof@logical@and\mathsf{1}\vdash\mathsf{1}\cdot\vdash\mathsf{1}\mathsf{nat}\vdash\mathsf{1}$

The cut elimination algorithm introduced by Fortier and Santocanale uses a
reduction function Treat that may never halt. They proved that for derivations
satisfying the guard condition Treat is locally terminating since it always
halts on guarded proofs [FS13]. The above derivation is an example of one that
does not satisfy the FS guard condition and the cut elimination algorithm does
not locally terminate on it.

The progress property for a configuration of processes ensures that during its
computation it either: (i) takes a step; (ii) is empty; or (iii) communicates
along its left or right channel. Without (mutually) recursive processes, this
property is enough to make sure that computation never gets stuck. Having
(mutually) recursive processes and fixed points, however, this property is not
strong enough to restrict internal loops. The composition
$x\leftarrow\mathtt{Loop}\leftarrow\cdot\mid
y\leftarrow\mathtt{Block}\leftarrow x$, for example, satisfies the progress
property but it never interacts with any other external process. We introduce
a stronger form of the progress property, in the sense that it requires one of
the conditions (ii) or (iii) to hold after a finite number of computation
steps.

Like cut elimination, strong progress is not compositional. Processes
$\mathtt{Loop}$ and $\mathtt{Block}$ both satisfy the strong progress property
but their composition $x\leftarrow\mathtt{Loop}\leftarrow\cdot\mid
y\leftarrow\mathtt{Block}\leftarrow x$ does not. We will show in Section 12
that FS validity implies strong progress. But, in contrast to strong progress,
FS validity is compositional in the sense that composition of two disjoint
valid programs is also valid. However, the FS guard condition is not local.
Locality is particularly important from the programming point of view. It is
the combination of two properties that are pervasive and often implicit in the
study of programming languages. First, the algorithm is syntax-directed,
following the structure of the program and second, it checks each process
definition separately, requiring only the signature and the types of other
processes but not their definition. One advantage is indeed asymptotic
complexity, and, furthermore, a practically very efficient implementation. In
Remark 11.42 we show that the time complexity of our validity algorithm is
linear in the total input, which consists of the signature and the process
definitions. Another is precision of error messages: locality implies that
there is an exact program location where the condition is violated. Validity
is a complex property, so the value of precise error messages cannot be
overestimated. The final advantage is modularity: all we care about a process
is its interface, not its definition, which means we can revise definitions
individually without breaking validity of the rest of the program as long as
we respect their interface. Our goal is to construct a locally checkable
validity condition that accepts (a subset of) programs satisfying strong
progress and is compositional.

In functional programming languages a program is called terminating if it
reduces to a value in a finite number of steps, and is called productive if
every piece of the output is generated in finite number of steps (even if the
program potentially runs forever). As in the current work, the theoretical
underpinnings for terminating and productive programs are also least and
greatest fixed points, respectively, but due to the functional nature of
computation they take a different and less symmetric form than here (see, for
example, [BM13, Gra16]).

In our system of session types, least and greatest fixed points correspond to
defined type variables with positive and negative polarity, respectively, and
their behaviors are quite symmetric: As in Definition 3.4, an unfolding
message $\mu_{t}$ for a type variable $t$ with positive polarity is received
from the left and sent to the right, while for a variable $t$ with negative
polarity, the unfolding message $\nu_{t}$ is received from the right and sent
to the left. Going back to Examples 4.5 and 4.6, process $\mathtt{Loop}$ seems
less acceptable than process $\mathtt{Block}$: process $\mathtt{Loop}$ does
not receive any least or greatest fixed point unfolding messages. It is
neither a terminating nor a productive process. We want our algorithm to
accept process $\mathtt{Block}$ rather than $\mathtt{Loop}$, since it cannot
accept both. This motivates a definition of finite reactivity on session-typed
processes.

######  Definition 4.7.

A program defined over a signature $\Sigma$ is (finitely) reactive to the left
if for a positive fixed point $t\in\Sigma$ with priority $i$ it does not
continue forever without receiving a fixed point unfolding message $\mu_{t}$
from the left infinitely often. Moreover, for any negative fixed point
$s\in\Sigma$ with priority $j<i$, the program does not send infinitely many
$\nu_{s}$ messages to the left.
A program is (finitely) reactive to the right if for a negative fixed point
$t\in\Sigma$ with priority $i$ it does not continue forever without receiving
a fixed point unfolding message $\nu_{t}$ from the right infinitely often.
Moreover, for any positive fixed point $s\in\Sigma$ with priority $j<i$, the
program does not send infinitely many $\mu_{s}$ messages to the right.
A program is called (finitely) reactive if it is either reactive to the right
or to the left.

By this definition, process $\mathtt{Block}$ is reactive while process
$\mathtt{Loop}$ is not. Finite reactivity corresponds to the FS guard
condition on the underlying circular derivation of a process. Although
reactivity is not local we use it as a motivation behind our algorithm. We
construct our local validity condition one step at a time. In each step, we
expand the condition to accept one more family of interesting finitely
reactive programs, provided that we can check the condition locally. We first
establish a local algorithm for programs with only direct recursion. We expand
the algorithm further to support mutual recursions as well. Then we examine a
subtlety regarding the cut rule to accept more programs locally. The reader
may skip to Section 10 which provides our complete finitary algorithm. Later,
in Sections 11 and 12 we prove that our algorithm ensures the FS guard
condition and strong progress.

Priorities of type variables in a signature are central to ensure that a
process defined based on them satisfies strong progress. Throughout the paper
we assume that the priorities are assigned (by a programmer) based on the
intuition of why strong progress holds. We conclude this section with an
example of a reactive process $\mathtt{Copy}$. This process, similar to
$\mathtt{Block}$, receives a natural number from the left but instead of
consuming it, sends it over to the right along a channel of type
$\mathsf{nat}$.

######  Example 4.8.

With signature

$\Sigma_{1}:=\mathsf{nat}=^{1}_{\mu}\oplus\\{\mathit{z}:\mathsf{1},\mathit{s}:\mathsf{nat}\\}$

we define process $\mathtt{Copy}$

$\displaystyle x:\mathsf{nat}\vdash\mathtt{Copy}::(y:\mathsf{nat})$

as

$\displaystyle y\leftarrow\mathtt{Copy}\leftarrow x=$
$\displaystyle\phantom{small}\mathbf{case}\,Lx\ (\mu_{nat}\Rightarrow$
$\displaystyle\%\ \textit{receive}\ \mu_{nat}\ \textit{from left}$ (i)
$\displaystyle\phantom{smallspac}\mathbf{case}\,Lx$ $\displaystyle\%\
\textit{receive a label}\ \textit{from left}$ (ii)
$\displaystyle\phantom{smallspacetim}(\ z\Rightarrow Ry.\mu_{nat};$
$\displaystyle\%\ \textit{send}\ \mu_{nat}\ \textit{ to right}$ (ii-a)
$\displaystyle\phantom{smallspacetimestwoplu}Ry.z;$ $\displaystyle\%\
\textit{send label}\ \mathit{z}\ \textit{ to right}$
$\displaystyle\phantom{smallspacetimestwoplus}\mathbf{wait}\,Lx;$
$\displaystyle\%\ \textit{wait for}\ x\ \textit{to close}$
$\displaystyle\phantom{smallspacetimestwopluson}\mathbf{close}\,Ry$
$\displaystyle\%\ \textit{close}\ y$ $\displaystyle\phantom{smallspacetix}\mid
s\Rightarrow Ry.\mu_{nat};$ $\displaystyle\%\ \textit{send}\ \mu_{nat}\ to\
\textit{right}$ (ii-b) $\displaystyle\phantom{smallspacetimestwoplu}Ry.s;$
$\displaystyle\%\ \textit{send label}\ \mathit{s}\ \textit{to right}$
$\displaystyle\phantom{smallspacetimestwoplus}y\leftarrow\mathtt{Copy}\leftarrow
x))$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\%\
\textit{recursive call}}$

This is an example of a recursive process, and
$\mathcal{P}_{3}:=\langle\\{\mathtt{Copy}\\},\mathtt{Copy}\rangle$ forms a
left reactive program over the signature $\Sigma_{1}$:
(i) It waits until it receives a positive fixed point unfolding message from
the left, (ii) waits for another message from the left to determine the path
it will continue with:
(a) If the message is a $\ \mathit{z}\ $ label, (ii-a) the program sends a
positive fixed point unfolding message to the right, followed by the label $\
\mathit{z}$, and then waits until a closing message is received from the left.
Upon receiving that message, it closes the right channel.
(b) If the message is an $\ \mathit{s}\ $ label, (ii-b) the program sends a
positive fixed point unfolding message to the right, followed by the label $\
\mathit{s}\ $, and then calls itself and loops back to (i).
The computational content of $\mathtt{Copy}$ is to simply copy a natural
number given from the left to the right. Process $\mathtt{Copy}$ does not
involve spawning (its underlying derivation is cut-free) and satisfies the
strong progress property. This property is preserved when composed with
$\mathtt{Block}$ as $y\leftarrow\mathtt{Copy}\leftarrow x\mid
z\leftarrow\mathtt{Block}\leftarrow y$.

##  5\. Local Validity Algorithm: Naive Version

In this section we develop a first naive version of our local validity
algorithm using Examples 5.9-5.10.

######  Example 5.9.

Let the signature be

$\Sigma_{2}:=\\\ \mathsf{bits}=^{1}_{\mu}\oplus\\{\mathit{b0}:\mathsf{bits},\
\mathit{b1}:\mathsf{bits}\\}$

and define the process $\mathtt{BitNegate}$

$\displaystyle x:\mathsf{bits}\vdash\mathtt{BitNegate}::(y:\mathsf{bits})$

with

$\displaystyle y\leftarrow\mathtt{BitNegate}\leftarrow x=$
$\displaystyle\phantom{small}\mathbf{case}\,Lx\ (\mu_{bits}\Rightarrow$
$\displaystyle\%\ \textit{receive}\ \mu_{bits}\ \textit{from left}$ (i)
$\displaystyle\phantom{smallspac}\mathbf{case}\,Lx$ $\displaystyle\%\
\textit{receive a label}\ \textit{from left}$ (ii)
$\displaystyle\phantom{smallspaceti}(\ \mathit{b0}\Rightarrow Ry.\mu_{bits};$
$\displaystyle\%\ \textit{send}\ \mu_{bits}\ \textit{ to right}$ (ii-a)
$\displaystyle\phantom{smallspacetimestwoplu}Ry.b1;$ $\displaystyle\%\
\textit{send label}\ \mathit{b1}\ \textit{ to right}$
$\displaystyle\phantom{smallspacetimestwoplus}y\leftarrow\mathtt{BitNegate}\leftarrow
x$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\%\
\textit{recursive call}}$
$\displaystyle\phantom{smallspaceti}\mid\mathit{b1}\Rightarrow Ry.\mu_{bits};$
$\displaystyle\%\ \textit{send}\ \mu_{bits}to\ \textit{right}$ (ii-b)
$\displaystyle\phantom{smallspacetimestwoplu}Ry.b0;$ $\displaystyle\%\
\textit{send label}\ \mathit{b0}\textit{ to right}$
$\displaystyle\phantom{smallspacetimestwoplus}y\leftarrow\mathtt{BitNegate}\leftarrow
x))$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\%\
\textit{recursive call}}$

$\mathcal{P}_{4}:=\langle\\{\mathtt{BitNegate}\\},\mathtt{BitNegate}\rangle$
forms a left reactive program over the signature $\Sigma_{2}$ quite similar to
$\mathtt{Copy}$. Computationally, $\mathtt{BitNegate}$ is a buffer with one
bit capacity that receives a bit from the left and stores it until a process
on its right asks for it. After that, the bit is negated and sent to the right
and the buffer becomes free to receive another bit.

######  Example 5.10.

Dual to Example 5.9, we can define $\mathtt{coBitNegate}$. Let the signature
be

$\Sigma_{3}:=\\\ \mathsf{cobits}=^{1}_{\nu}\&\\{\mathit{b0}:\mathsf{cobits},\
\mathit{b1}:\mathsf{cobits}\\}$

with process

$\displaystyle
x:\mathsf{cobits}\vdash\mathtt{coBitNegate}::(y:\mathsf{cobits})$

where $\mathtt{coBitNegate}$ is defined as

$\displaystyle y\leftarrow\mathtt{coBitNegate}\leftarrow x=$
$\displaystyle\phantom{small}\mathbf{case}\,Ry\ (\nu_{cobits}\Rightarrow$
$\displaystyle\%\ \textit{receive}\ \nu_{cobits}\ \textit{from right}$ (i)
$\displaystyle\phantom{smallspac}\mathbf{case}\,Ry$ $\displaystyle\%\
\textit{receive a label}\ \textit{from right}$ (ii)
$\displaystyle\phantom{smallspaceti}(\ \mathit{b0}\Rightarrow
Lx.\nu_{cobits};$ $\displaystyle\%\ \textit{send}\ \nu_{cobits}\ \textit{ to
left}$ (ii-a) $\displaystyle\phantom{smallspacetimestwoplu}Lx.b1;$
$\displaystyle\%\ \textit{send label}\ \mathit{b1}\ \textit{ to left}$
$\displaystyle\phantom{smallspacetimestwoplus}y\leftarrow\mathtt{coBitNegate}\leftarrow
x$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\%\
\textit{recursive call}}$
$\displaystyle\phantom{smallspaceti}\mid\mathit{b1}\Rightarrow
Lx.\nu_{cobits};$ $\displaystyle\%\ \textit{send}\ \nu_{cobits}\ \textit{to
left}$ (ii-b) $\displaystyle\phantom{smallspacetimestwoplu}Lx.b0;$
$\displaystyle\%\ \textit{send label}\ \mathit{b0}\ \textit{to left}$
$\displaystyle\phantom{smallspacetimestwoplus}y\leftarrow\mathtt{coBitNegate}\leftarrow
x))$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\%\
\textit{recursive call}}$

$\mathcal{P}_{5}:=\langle\\{\mathtt{coBitNegate}\\},\mathtt{coBitNegate}\rangle$
forms a right reactive program over the signature $\Sigma_{3}$.
Computationally, $\mathtt{coBitNegate}$ is a buffer with one bit capacity. In
contrast to $\mathtt{BitNegate}$ in Example 5.9, its types have negative
polarity: it receives a bit from the right, and stores it until a process on
its left asks for it. After that the bit is negated and sent to the left and
the buffer becomes free to receive another bit.

######  Remark 5.11.

The property that assures the reactivity of the previous examples lies in
their step (i) in which the program blocks until an unfolding message is
received, i.e., the program can only continue the computation if it receives a
message at step (i), and even after receiving the message it can only take
finitely many steps further before the computation ends or another unfolding
message is needed.

We first develop a naive version of our algorithm which captures the property
explained in Remark 5.11: associate an initial integer value (say $0$) to each
channel and define the basic step of our algorithm to be _decreasing_ the
value associated to a channel _by one_ whenever it _receives_ a fixed point
unfolding message. Also, for a reason that is explained later in Remark 6.13,
whenever a channel _sends_ a fixed point unfolding message its value is
_increased by one_. Then at each recursive call, the value of the left and
right channels are compared to their initial value.

For instance, in Example 4.8, in step (i) where the process receives a
$\mu_{nat}$ message via the left channel ($x$), the value associated with $x$
is decreased by one, while in steps (ii-a) and (ii-b) in which the process
sends a $\mu_{nat}$ message via the right channel ($y$) the value associated
with $y$ is increased by one:

$\displaystyle x$ $\displaystyle\phantom{space}y$ $\displaystyle
y\leftarrow\mathtt{Copy}\leftarrow x=$ $\displaystyle 0$
$\displaystyle\phantom{space}0$
$\displaystyle\mathbf{case}\,Lx\,(\mu_{nat}\Rightarrow$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}-1}$
$\displaystyle\phantom{space}0$
$\displaystyle\phantom{caseLx(\mu_{nat}}\mathbf{case}\,Lx\,(\mathit{z}\Rightarrow
Ry.\mu_{nat};$ $\displaystyle-1$
$\displaystyle\phantom{space}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$
$\displaystyle\phantom{caseLx(\mu_{nat}\Rightarrow
caseLx(z\Rightarrow}R.z;\mathbf{wait}\,Lx;\mathbf{close}\,Ry$
$\displaystyle-1$ $\displaystyle\phantom{space}1$
$\displaystyle\phantom{caseLx(\mu_{nat}\Rightarrow cas}\mathit{s}\Rightarrow
Ry.\mu_{nat};$ $\displaystyle-1$
$\displaystyle\phantom{space}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$
$\displaystyle\phantom{caseLx(\mu_{nat}\Rightarrow
caseLx\mathit{s}\Rightarrow}Ry.s;y\leftarrow\mathtt{Copy}\leftarrow x))$
$\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}-1}$
$\displaystyle\phantom{space}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$

When the recursive call occurs, channel $x$ has the value
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}-1}<0$,
meaning that at some point in the computation it received a positive fixed
point unfolding message. We can simply compare the value of the list $[x,y]$
lexicographically at the beginning and just before the recursive call:
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[-1,1]}$
being less than $[0,0]$ exactly captures the property observed in Remark 5.11
for the particular signature $\Sigma_{1}$. Note that by the definition of
$\Sigma_{1}$, $y$ never receives a fixed point unfolding message, so its value
never decreases, and $x$ never sends a fixed point unfolding message, thus its
value never increases.

The same criteria works for the program $\mathcal{P}_{3}$ over the signature
$\Sigma_{2}$ defined in Example 5.9, since $\Sigma_{2}$ also contains only one
positive fixed point:

$\displaystyle x$ $\displaystyle\phantom{space}y$ $\displaystyle
y\leftarrow\mathtt{BitNegate}\leftarrow x=$ $\displaystyle 0$
$\displaystyle\phantom{space}0$ $\displaystyle\mathbf{case}\,Lx\
(\mu_{bits}\Rightarrow$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}-1}$
$\displaystyle\phantom{space}0$
$\displaystyle\phantom{caseLx}\mathbf{case}\,Lx\ (b0\Rightarrow
Ry.\mu_{bits};\ $ $\displaystyle-1$
$\displaystyle\phantom{space}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$
$\displaystyle\phantom{caseLx(\mu_{nat}\Rightarrow
Ry.}Ry.b1;y\leftarrow\mathtt{BitNegate}\leftarrow x$
$\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}-1}$
$\displaystyle\phantom{space}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$
$\displaystyle\phantom{caseLx(\mu_{nat}\Rightarrow(}\mathit{b1}\Rightarrow
Ry.\mu_{bits};$ $\displaystyle-1$
$\displaystyle\phantom{space}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$
$\displaystyle\phantom{caseLx(\mu_{nat}\Rightarrow
Ry.}Ry.b0;y\leftarrow\mathtt{BitNegate}\leftarrow x))$
$\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}-1}$
$\displaystyle\phantom{space}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$

At both recursive calls the value of the list $[x,y]$ is less than $[0,0]$:
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[-1,1]}<[0,0]$.

However, for a program defined on a signature with a negative polarity such as
the one defined in Example 5.10, this condition does not work:

$\displaystyle x$ $\displaystyle\phantom{space}y$ $\displaystyle
y\leftarrow\mathtt{coBitNegate}\leftarrow x=$ $\displaystyle 0$
$\displaystyle\phantom{space}0$ $\displaystyle\mathbf{case}\,Ry\
(\nu_{cobits}\Rightarrow$ $\displaystyle{0}$
$\displaystyle\phantom{spac}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}-1}$
$\displaystyle\phantom{caseLx}\mathbf{case}\,Ry\ (b0\Rightarrow
Lx.\nu_{cobits};\ $
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$
$\displaystyle\phantom{spac}{-1}$
$\displaystyle\phantom{caseLx(\mu_{nat}\Rightarrow
Ry.}Lx.b1;y\leftarrow\mathtt{coBitNegate}\leftarrow x$
$\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$
$\displaystyle\phantom{spac}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}-1}$
$\displaystyle\phantom{caseLx(\mu_{nat}\Rightarrow(}\mathit{b1}\Rightarrow
Lx.\nu_{cobits};$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$
$\displaystyle\phantom{spac}{-1}$
$\displaystyle\phantom{caseLx(\mu_{nat}\Rightarrow
Ry.}Lx.b0;y\leftarrow\mathtt{coBitNegate}\leftarrow x))$
$\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}1}$
$\displaystyle\phantom{spac}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}-1}$

By the definition of $\Sigma_{3}$, $y$ only receives unfolding fixed point
messages, so its value only decreases. On the other hand, $x$ cannot receive
an unfolding fixed point from the left and thus its value never decreases. In
this case the property in Remark 5.11 is captured by comparing the initial
value of the list $[y,x]$, instead of $[x,y]$, with its value just before the
recursive call:
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[-1,1]}<[0,0]$.

For a signature with only a single recursive type we can form a list by
looking at the polarity of its type such that the value of the channel that
receives the unfolding message comes first, and the value of the other one
comes second.

##  6\. Priorities in the Local Validity Algorithm

The property explained in Remark 5.11 of previous section is not strict
enough, particularly when the signature has more than one recursive type. In
that case not all programs that are waiting for a fixed point unfolding
message before a recursive call are reactive.

######  Example 6.12.

Consider the signature

$\displaystyle\Sigma_{4}:=$
$\displaystyle\mathsf{ack}=^{1}_{\mu}\oplus\\{\mathit{ack}:\mathsf{astream}\\},$
$\displaystyle\mathsf{astream}=^{2}_{\nu}\&\\{\mathit{head}:\mathsf{ack},\ \
\mathit{tail}:\mathsf{astream}\\},$
$\displaystyle\mathsf{nat}=^{3}_{\mu}\oplus\\{\mathit{z}:1,\ \
\mathit{s}:nat\\}$

$\mathsf{ack}$ is a type with positive polarity that, upon unfolding,
describes a protocol requiring an acknowledgment message to be sent to the
right (or be received from the left). $\mathsf{astream}$ is a type with
negative polarity of a potentially infinite stream where its $\mathit{head}$
is always followed by an acknowledgement while $\mathit{tail}$ is not.

$\mathcal{P}_{6}:=\langle\\{\mathtt{Ping},\mathtt{Pong},\mathtt{PingPong}\\},\mathtt{PingPong}\rangle$
forms a program over the signature $\Sigma_{4}$ with the typing of its
processes

$\begin{array}[]{l}x:\mathsf{nat}\vdash\mathtt{Ping}::(w:\mathsf{astream})\\\
w:\mathsf{astream}\vdash\mathtt{Pong}::(y:\mathsf{nat})\\\
x:\mathsf{nat}\vdash\mathtt{PingPong}::(y:\mathsf{nat})\end{array}$

We define processes $\mathtt{Ping}$, $\mathtt{Pong}$, and $\mathtt{PingPong}$
over $\Sigma_{4}$ as:

$\displaystyle y\leftarrow\mathtt{PingPong}\leftarrow x=$
$\displaystyle\phantom{smal}w\leftarrow\mathtt{Ping}\leftarrow x;$
$\displaystyle\%\ \textit{spawn process}\ \mathtt{Ping}$ (i)
$\displaystyle\phantom{smallspace}y\leftarrow\mathtt{Pong}\leftarrow w$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\%\
\textit{continue with a tail call}}$ $\displaystyle
y\leftarrow\mathtt{Pong}\leftarrow w=$
$\displaystyle\phantom{smal}Lw.\nu_{astream};$ $\displaystyle\%\
\textit{send}\ \mathit{\nu_{astream}}\ \textit{to left}$ (ii-$\mathtt{Pong}$)
$\displaystyle\phantom{smalls}Lw.\mathit{head};$ $\displaystyle\%\
\textit{send label}\ \mathit{head}\ \textit{to left}$ (iii-$\mathtt{Pong}$)
$\displaystyle\phantom{smallsp}\mathbf{case}\,Lw\ (\mu_{ack}\Rightarrow$
$\displaystyle\%\ \textit{receive}\ \mathit{\mu_{ack}}\ \textit{from left}$
(iv-$\mathtt{Pong}$) $\displaystyle\phantom{smallspace}\mathbf{case}\,Lw\ ($
$\displaystyle\%\ \textit{receive a label from left}$
$\displaystyle\phantom{smallspacetimestwo}ack\Rightarrow Ry.\mu_{nat};$
$\displaystyle\%\ \textit{send}\ \mathit{\mu_{nat}}\ \textit{to right}$
$\displaystyle\phantom{smallspacetimestwoplu}Ry.s;$ $\displaystyle\%\
\textit{send label}\ \mathit{s}\ \textit{to right}$
$\displaystyle\phantom{smallspacetimestwopluso}y\leftarrow\mathtt{Pong}\leftarrow
w))$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\%\
\textit{recursive call}}$ $\displaystyle w\leftarrow\mathtt{Ping}\leftarrow
x=$ $\displaystyle\phantom{smal}\mathbf{case}\,Rw\ (\nu_{astream}\Rightarrow$
$\displaystyle\%\ \textit{receive }\mathit{\nu_{astream}}\textit{from right}$
(ii-$\mathtt{Ping}$) $\displaystyle\phantom{smallsp}\mathbf{case}\,Rw\ ($
$\displaystyle\%\ \textit{receive a label from right}$
$\displaystyle\phantom{smallspacetimes}\mathit{head}\Rightarrow Rw.\mu_{ack};$
$\displaystyle\%\ \textit{send}\ \mu_{ack}\ \textit{to right}$
(iii-$\mathtt{Ping}$)
$\displaystyle\phantom{smallspacetimestwopluson}Rw.\mathit{ack};$
$\displaystyle\%\ \textit{send label}\ \mathit{ack}\ \textit{to right}$
$\displaystyle\phantom{smallspacetimestwoplusonean}w\leftarrow\mathtt{Ping}\leftarrow
x$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\%\
\textit{recursive call}}$
$\displaystyle\phantom{smallspacetimes}\mid\mathit{tail}\Rightarrow
w\leftarrow\mathtt{Ping}\leftarrow x))$ $\displaystyle{\%\ \textit{recursive
call}}$

(i) Program $\mathcal{P}_{6}$ starting from $\mathtt{PingPong}$, spawns a new
process $\mathtt{Ping}$ and continues as $\mathtt{Pong}$:
(ii-$\mathtt{Pong}$) Process $\mathtt{Pong}$ sends an $\mathsf{astream}$
unfolding and then a $\mathit{head}$ message to the left, and then
(iii-$\mathtt{Pong}$) waits for an acknowledgment, i.e., $\mathit{ack}$, from
the left.
(ii-$\mathtt{Ping}$) At the same time process $\mathtt{Ping}$ waits for an
$\mathsf{astream}$ fixed point unfolding message from the right, which becomes
available after step (ii-$\mathtt{Pong}$). Upon receiving the message, it
waits to receive either $\mathit{head}$ or $\mathit{tail}$ from the right,
which is also available from (ii-$\mathtt{Pong}$) and is actually a
$\mathit{head}$. So (iii-$\mathtt{Ping}$) it continues with the path
corresponding to $\mathit{head}$, and acknowledges receipt of the previous
messages by sending an unfolding messages and the label $\mathit{ack}$ to the
right, and then it calls itself (ii-$\mathtt{Ping}$).
(iv-$\mathtt{Pong}$) Process $\mathtt{Pong}$ now receives the two messages
sent at (iii-$\mathtt{Ping}$) and thus can continue by sending a
$\mathsf{nat}$ unfolding message and the label $\mathit{s}$ to the right, and
finally calling itself (ii-$\mathtt{Pong}$).
Although both recursive processes $\mathtt{Ping}$ and $\mathtt{Pong}$ at some
point wait for a fixed point unfolding message, this program runs infinitely
without receiving any messages from the outside, and thus is not reactive.

The back-and-forth exchange of fixed point unfolding messages between two
processes in the previous example can arise when at least two mutually
recursive types with different polarities are in the signature. This is why we
need to incorporate priorities of the type variables into the validity
checking algorithm.

######  Remark 6.13.

In Example 6.12, for instance, waiting to receive an unfolding message
$\nu_{astream}$ of priority 2 in line (ii-$\mathtt{Ping}$) is not enough to
ensure validity of the recursive call because later in line
(iii-$\mathtt{Ping}$) the process sends an unfolding message of a higher
priority (1).

To prevent validity of such a call we form a list for each process. This list
stores the information of the fixed point unfolding messages that the process
received and sent before a recursive call for each type variable in their
order of priority.

######  Example 6.14.

Consider the signature and program $\mathcal{P}_{6}$ as defined in Example
6.12. For the process $x:\mathsf{nat}\vdash w\leftarrow\mathtt{Ping}\leftarrow
x::(w:\mathsf{astream})$ form the list

$[\mathsf{ack}-\mathit{received},\mathsf{ack}-\mathit{sent},\mathsf{astream}-\mathit{received},\mathsf{astream}-\mathit{sent},\mathsf{nat}-\mathit{received},\mathsf{nat}-\mathit{sent}].$

Types with positive polarity, i.e., $\mathsf{ack}$ and $\mathsf{nat}$, receive
messages from the left channel ($x$) and send messages to the right channel
($w$), while those with negative polarity, i.e., $\mathsf{astream}$, receive
from the right channel ($w$) and send to the left one ($x$). Thus, the above
list can be rewritten as

$[x_{\mathsf{ack}},w_{\mathsf{ack}},w_{\mathsf{astream}},x_{\mathsf{astream}},x_{\mathsf{nat}},w_{\mathsf{nat}}].$

To keep track of the sent/received messages, we start with $[0,0,0,0,0,0]$ as
the value of the list, when the process
$x:\mathsf{nat}\vdash\mathtt{Ping}::(w:\mathsf{astream})$ is first spawned.
Then, similar to the first version of our algorithm, on the steps in which the
process receives a fixed point unfolding message, the value of the
corresponding element of the list is decreased by one. And on the steps it
sends a fixed point unfolding message, the corresponding value is increased by
one:

$\displaystyle w\leftarrow\mathtt{Ping}\leftarrow x=$
$\displaystyle\phantom{caseRw}[0,0\ ,0\ ,0,0,0]$
$\displaystyle\phantom{\mathtt{Ping}=}\mathbf{case}\,Rw\
(\nu_{astream}\Rightarrow$
$\displaystyle[0,0,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}-1},0,0,0]$
$\displaystyle\phantom{caseRw(\nu_{astream})}\mathbf{case}\,Rw\
(\mathit{head}\Rightarrow Rw.\mu_{ack};$
$\displaystyle[0,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1},-1,0,0,0]$
$\displaystyle\phantom{caseRw(\nu_{astream}\Rightarrow caseRw(head\ \
}Rw.\mathit{ack};w\leftarrow\mathtt{Ping}\leftarrow x$
$\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[0,1,-1,0,0,0]}$
$\displaystyle\phantom{caseRw(\nu_{astream}\Rightarrow
casex}\mid\mathit{tail}\Rightarrow w\leftarrow\mathtt{Ping}\leftarrow x))$
$\displaystyle[0,0,-1,0,0,0]$

The two last lines are the values of the list on which process $\mathtt{Ping}$
calls itself recursively. The validity condition as described in Remark 6.13
holds iff the value of the list at the time of the recursive call is less than
the value the process started with, in lexicographical order. Here, for
example,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[0,1,-1,0]}\not<[0,0,0,0]$,
and the validity condition does not hold for this recursive call.

We leave it to the reader to verify that no matter how we assign priorities of
the type variables in $\Sigma_{4}$, our condition rejects $\mathtt{PingPong}$.

The following definition captures the idea of forming lists described above.
Rather than directly referring to type variables such as $\mathsf{ack}$ or
$\mathsf{astream}$ we just refer to their priorities, since that is the
relevant information.

######  Definition 6.15.

For a process

$\bar{x}:\omega\vdash P::(y:B),$

over the signature $\Sigma$, define $list(\bar{x},y)=[f_{i}]_{i\leq n}$ such
that

  1. (1)

$f_{i}=(\bar{x}_{i},y_{i})$ if $\epsilon(i)=\mu$, and

  2. (2)

$f_{i}=(y_{i},\bar{x}_{i})$ if $\epsilon(i)=\nu,$

where $n$ is the lowest priority in $\Sigma.$

In the remainder of this section we use $n$ to denote the lowest priority in
$\Sigma$ (which is numerically maximal).

######  Example 6.16.

Consider the signature $\Sigma_{1}$ and program
$\mathcal{P}_{3}:=\langle\\{\mathtt{Copy}\\},\mathtt{Copy}\rangle$, from
Example 4.8:
$\Sigma_{1}:=\mathsf{nat}=^{1}_{\mu}\oplus\\{\mathit{z}:\mathsf{1},\mathit{s}:\mathsf{nat}\\},$
and

$\displaystyle y\leftarrow\mathtt{Copy}\leftarrow x=\mathbf{case}\,Lx\
(\mu_{nat}\Rightarrow\mathbf{case}\,Lx\ $ $\displaystyle(\ z\Rightarrow
Ry.\mu_{nat};Ry.z;\mathbf{wait}\,Lx;\mathbf{close}\,Ry$ $\displaystyle\mid
s\Rightarrow Ry.\mu_{nat};Ry.s;y\leftarrow\mathtt{Copy}\leftarrow x))$

By Definition 6.15, for process
$x:\mathsf{nat}\vdash\mathtt{Copy}::(y:\mathsf{nat})$, we have $n=1$, and
$list(x,y)=[(x_{1},y_{1})]$ since $\epsilon(1)=\mu$. Just as for the naive
version of the algorithm, we can trace the value of $list(x,y)$:

$\displaystyle y\leftarrow\mathtt{Copy}\leftarrow x=$ $\displaystyle[0,0]$
$\displaystyle\mathbf{case}\,Lx\ (\mu_{nat}\Rightarrow$
$\displaystyle[{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}-1},0]$
$\displaystyle\phantom{caseLx(\mu_{nat}}\mathbf{case}\,Lx\
(\mathit{z}\Rightarrow Ry.\mu_{nat};$
$\displaystyle[-1,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}]$
$\displaystyle\phantom{caseLx(\mu_{nat}\Rightarrow
caseLx(z\Rightarrow}R.z;\mathbf{wait}\,Lx;\mathbf{close}\,Ry$
$\displaystyle{[-1,1]}$ $\displaystyle\phantom{caseLx(\mu_{nat}\Rightarrow
case}\mid\mathit{s}\Rightarrow Ry.\mu_{nat};$
$\displaystyle[-1,{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}]$
$\displaystyle\phantom{caseLx(\mu_{nat}\Rightarrow
caseLx\mathit{s}\Rightarrow}Ry.s;y\leftarrow\mathtt{Copy}\leftarrow x$
$\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[-1,1]}$

Here,
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[-1,1]}<[0,0]$
and the recursive call is classified as valid.

To capture the idea of decreasing/increasing the value of the elements of
$list(\\_,\\_)$ by one, as depicted in Example 6.14 and Example 6.16, we
assume that a channel transforms into a new generation of itself after sending
or receiving a fixed point unfolding message.

######  Example 6.17.

Process $x:\mathsf{nat}\vdash y\leftarrow\mathtt{Copy}\leftarrow
x::(y:\mathsf{nat})$ in Example 6.16 starts its computation with the initial
generation of its left and right channels:

$x^{0}:\mathsf{nat}\vdash y^{0}\leftarrow\mathtt{Copy}\leftarrow
x^{0}::(y^{0}:\mathsf{nat}).$

The channels evolve as the process sends or receives a fixed point unfolding
message along them:

$\displaystyle y^{0}\leftarrow\mathtt{Copy}\leftarrow x^{0}$
$\displaystyle=\phantom{caseL{x^{0}}(\mu_{nat}}$
$\displaystyle\mathbf{case}\,L{x^{0}}\ (\mu_{nat}\Rightarrow$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}x^{0}\rightsquigarrow
x^{1}}$ $\displaystyle\phantom{caseL{x^{1}}(\mu_{nat}}\mathbf{case}\,L{x^{1}}\
(\mathit{z}\Rightarrow R{y^{0}}.\mu_{nat};$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}y^{0}\rightsquigarrow
y^{1}}$ $\displaystyle\phantom{caseL{x^{1}}(\mu_{nat}\Rightarrow
caseL{x^{1}}(z\Rightarrow}R{y^{1}}.z;\mathbf{wait}\,L{y^{1}};\mathbf{close}\,R{x^{1}}$
$\displaystyle\phantom{caseL{x^{0}}(\mu_{nat}\Rightarrow
case}\mid\mathit{s}\Rightarrow R{y^{0}}.\mu_{nat};$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}y^{0}\rightsquigarrow
y^{1}}$ $\displaystyle\phantom{caseL{x^{0}}(\mu_{nat}\Rightarrow
caseL{x^{1}}\mathit{s}\Rightarrow}R{y^{1}}.s;y^{1}\leftarrow\mathtt{Copy}\leftarrow
x^{1}))$

On the last line the process

$x^{1}:\mathsf{nat}\vdash y^{1}\leftarrow\mathtt{Copy}\leftarrow
x^{1}::(y^{1}:\mathsf{nat})$

is called recursively with a new generation of variables.

In the inference rules introduced in Section 9, instead of recording the value
of each element of $list(\ \\_,\\_)$ as we did in Example 6.14 and Example
6.16, we introduce $\Omega$ to track the relation between different
generations of a channel indexed by their priority of types.

######  Remark 6.18.

Generally speaking, $x^{\alpha+1}_{i}<x^{\alpha}_{i}$ is added to $\Omega$,
when $x^{\alpha}$ receives a fixed point unfolding message for a type with
priority $i$ and transforms to $x^{\alpha+1}$. This corresponds to the
decrease by one in the previous examples.

If $x^{\alpha}$ sends a fixed point unfolding message for a type with priority
$i$ is _sent_ on $x^{\alpha}$, which then evolves to $x^{\alpha+1}$,
$x^{\alpha}_{i}$ and $x^{\alpha+1}_{i}$ are considered to be incomparable in
$\Omega$. This corresponds to increase by one in the previous examples, since
for the sake of lexicographically comparing the value of $list(\ \\_,\\_)$ at
the first call of a process to its value just before a recursive call, there
is no difference whether $x^{\alpha+1}$ is greater than $x^{\alpha}$ or
incomparable to it.

When $x^{\alpha}$ receives/sends a fixed point unfolding message of a type
with priority $i$ and transforms to $x^{\alpha+1}$, for any type with priority
$j\neq i$, the value of $x^{\alpha}_{j}$ and $x^{\alpha+1}_{j}$ must remain
equal. In these steps, we add $x^{\alpha}_{j}=x^{\alpha+1}_{j}$ for $j\neq i$
to $\Omega$.

A process in the formalization of the intuition above is therefore typed as

$x^{\alpha}:A\vdash_{\Omega}P::(y^{\beta}:B),$

where $x^{\alpha}$ is the $\alpha$-th generation of channel $x$. The syntax
and operational semantics of the processes with generational channels are the
same as the corresponding definitions introduced in Section 3; we simply
ignore generations over the channels to match processes with the previous
definitions. We enforce the assumption that channel $x^{\alpha}$ transforms to
its next generation $x^{\alpha+1}$ upon sending/receiving a fixed point
unfolding message in the typing rules of Section 9.

The relation between the channels indexed by their priority of types is built
step by step in $\Omega$ and represented by $\leq$. The reflexive transitive
closure of $\Omega$ forms a partial order $\leq_{\Omega}$. We extend
$\leq_{\Omega}$ to the list of channels indexed by the priority of their types
considered lexicographically. We may omit subscript $\Omega$ from
$\leq_{\Omega}$ whenever it is clear from the context. In the next examples,
we present the set of relations $\Omega$ in the rightmost column.

##  7\. Mutual Recursion in the Local Validity Condition

In examples of previous sections, the recursive calls were not _mutual_. In
the general case, a process may call any other process variable in the
program, and this call can be mutually recursive. In this section, we
incorporate mutual recursive calls into our algorithm.

######  Example 7.19.

Recall signature $\Sigma_{4}$ from Example 6.12

$\displaystyle\Sigma_{4}:=$
$\displaystyle\mathsf{ack}=^{1}_{\mu}\oplus\\{\mathit{ack}:\mathsf{astream}\\},$
$\displaystyle\mathsf{astream}=^{2}_{\nu}\&\\{\mathit{head}:\mathsf{ack},\ \
\mathit{tail}:\mathsf{astream}\\},$
$\displaystyle\mathsf{nat}=^{3}_{\mu}\oplus\\{\mathit{z}:1,\ \
\mathit{s}:nat\\}$

Define program
$\mathcal{P}_{7}=\langle\\{\mathtt{Idle},\mathtt{Producer}\\},\mathtt{Producer}\rangle$,
where

$\begin{array}[]{l}z:\mathsf{ack}\vdash w\leftarrow\mathtt{Idle}\leftarrow
z::(w:\mathsf{nat})\\\ x:\mathsf{astream}\vdash
y\leftarrow\mathtt{Producer}\leftarrow x::(y:\mathsf{nat}),\end{array}$

and processes $\mathtt{Idle}$ (or simply $\mathtt{I}$) and $\mathtt{Producer}$
(or simply $\mathtt{P}$ ) are defined as:

$\begin{array}[]{l}w\leftarrow\mathtt{I}\leftarrow z=\mathbf{case}\,Lz\
(\mu_{ack}\Rightarrow\mathbf{case}\,L{z}\ (\mathit{ack}\Rightarrow
Rw.\mu_{nat};Rw.\mathit{s};w\leftarrow\mathtt{P}\leftarrow z))\\\\[4.30554pt]
y\leftarrow\mathtt{P}\leftarrow
x=Lx.\nu_{astream};Lx.\mathit{head};y\leftarrow\mathtt{I}\leftarrow
x.\end{array}$

We have $list(x,y)=[(x_{1},y_{1}),(y_{2},x_{2}),(x_{3},y_{3})]$ and
$list(z,w)=[(z_{1},w_{1}),(w_{2},z_{2}),(z_{3},w_{3})]$ since
$\epsilon(1)=\epsilon(3)=\mu$ and $\epsilon(2)=\nu$.

By analyzing the behavior of this program step by step, we see that it is a
reactive program that counts the number of acknowledgements received from the
left. The program starts with the process
$x^{0}:\mathsf{astream}\vdash_{\emptyset}y^{0}\leftarrow\mathtt{Producer}\leftarrow
x^{0}::(y^{0}:\mathsf{nat})$. It first sends one message to left to unfold the
negative fixed point type, and its left channel evolves to a next generation.
Then another message is sent to the left to request the $\mathit{head}$ of the
stream and after that it calls process $y^{0}\leftarrow\mathtt{Idle}\leftarrow
x^{1}$.

$\displaystyle y^{0}\leftarrow\mathtt{Producer}\leftarrow x^{0}=$
$\displaystyle\phantom{Lx^{0}.\nu_{astream};}\phantom{L.\nu}[0,0,0,0,0,0]$
$\displaystyle\phantom{sma}Lx^{0}.\nu_{astream};$
$\displaystyle\phantom{L.\nu}[0,0,0,1,0,0]$
$\displaystyle\phantom{L.\nu}x^{1}_{1}=x^{0}_{1},x^{1}_{3}=x^{0}_{3}$
$\displaystyle\phantom{smallsp}Lx^{1}.\mathit{head};y^{0}\leftarrow\mathtt{Idle}\leftarrow
x^{1}$
$\displaystyle\phantom{L.\nu}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[0,0,0,1,0,0]}$

Process $x^{1}:\mathsf{ack}\vdash y^{0}\leftarrow\mathtt{Idle}\leftarrow
x^{1}::(y^{0}:\mathsf{nat})$, then waits to receive an acknowledgment from the
left via a positive fixed point unfolding message for $\mathsf{ack}$ and its
left channel transforms into a new generation upon receiving it. Then it waits
for the label $\mathit{ack}$, upon receiving it, sends one message to the
right to unfold the positive fixed point $\mathsf{nat}$ (and this time the
right channel evolves). Then it sends the label $\mathit{s}$ to the right and
calls $y^{1}\leftarrow\mathtt{Producer}\leftarrow x^{2}$ recursively:

$\displaystyle y^{0}\leftarrow\mathtt{Idle}\leftarrow x^{1}=$
$\displaystyle\phantom{caseLx^{1}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[0,0,\
0,\ 1,\ 0,0]}$ $\displaystyle\phantom{sma}\mathbf{case}\,Lx^{1}\
(\mu_{ack}\Rightarrow$ $\displaystyle[-1,0,0,1,0,0]$
$\displaystyle\phantom{L}x^{2}_{1}<x^{1}_{1},x^{2}_{2}=x^{1}_{2},x^{2}_{3}=x^{1}_{3}$
$\displaystyle\phantom{smallsp}\mathbf{case}\,Lx^{2}\ (\mathit{ack}\Rightarrow
Ry^{0}.\mu_{nat};$ $\displaystyle[-1,0,0,1,0,1]$
$\displaystyle\phantom{Lx^{0}.\nu}y^{1}_{1}=y^{0}_{1},y^{1}_{2}=y^{0}_{2}$
$\displaystyle\phantom{smallspace}Ry^{1}.\mathit{s};y^{1}\leftarrow\mathtt{Producer}\leftarrow
x^{2}))$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[-1,0,0,1,0,1]}$

Observe that the actual recursive call for $\mathtt{Producer}$ occurs at the
last line (in red) above, where $\mathtt{Producer}$ eventually calls itself.
At that point the value of $list(x^{2},y^{1})$ is recorded as
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[-1,0,0,1,0,1]}$,
which is less than the value of $list(x^{0},y^{0})$ when $\mathtt{Producer}$
was called for the first time:

${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[-1,0,0,1,0,1]}<{[0,0,0,0,0,0]}.$

The same observation can be made by considering the relations introduced in
the last column

${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}list(x^{2},y^{1})}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[(x^{2}_{1},y^{1}_{1}),(y^{1}_{2},x^{2}_{2}),(x^{2}_{3},y^{1}_{3})]}<[(x^{0}_{1},y^{0}_{1}),(y^{0}_{2},x^{0}_{2}),(x^{0}_{3},y^{0}_{3})]=list(x^{0},y^{0})$

since $x^{2}_{1}<x^{1}_{1}=x^{0}_{1}$. This recursive call is valid regardless
of the fact that
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[0,0,0,1,0,0]}\not<{[0,0,0,0,0,0]},$
i.e.

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}list(x^{1},y^{0})}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[(x^{1}_{1},y^{0}_{1}),(y^{0}_{2},x^{1}_{2}),(x^{1}_{3},y^{0}_{3})]}\not<[(x^{0}_{1},y^{0}_{1}),(y^{0}_{2},x^{0}_{2}),(x^{0}_{3},y^{0}_{3})]=list(x^{0},y^{0})$

since $x^{1}_{1}=x^{0}_{1}$ but $x^{1}_{2}$ is incomparable to $x^{0}_{2}$.
Similarly, we can observe that the actual recursive call on $\mathtt{Idle}$,
where $\mathtt{Idle}$ eventually calls itself, is valid.

To account for this situation, we introduce an order on process variables and
trace the last seen variable on the path leading to the recursive call. In
this example we define $\mathtt{Idle}$ to be less than $\mathtt{Producer}$ at
position $2$ ($\mathtt{I}\subset_{2}\mathtt{P}$), i.e.:

> We incorporate process variables $\mathtt{Producer}$ and $\mathtt{Idle}$
> into the lexicographical order on $list(\\_,\\_)$ such that their values are
> placed exactly before the element in the list corresponding to the sent
> unfolding messages of the type with priority $2$.

We now trace the ordering as follows:

$\displaystyle y^{0}\leftarrow\mathtt{Producer}\leftarrow x^{0}=$
$\displaystyle\phantom{L}[0,0,0,\mathtt{P},0,0,0]$
$\displaystyle\phantom{small}Lx^{0}.\nu_{astream};$
$\displaystyle\phantom{L}[0,0,0,\mathtt{P},1,0,0]$
$\displaystyle\phantom{Lx^{0}.\nu}x^{1}_{1}=x^{0}_{1},x^{1}_{3}=x^{0}_{3}$
$\displaystyle\phantom{Lx^{0}.\nu_{strea}}Lx^{1}.\mathit{head};y^{0}\leftarrow\mathtt{Idle}\leftarrow
x^{1}$
$\displaystyle\phantom{L}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[0,0,0,\mathtt{I},1,0,0]}$
$\displaystyle y^{0}\leftarrow\mathtt{Idle}\leftarrow x^{1}=$
$\displaystyle\phantom{L}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[0,0,0,\mathtt{I},1,0,0]}$
$\displaystyle\phantom{small}\mathbf{case}\,Lx^{1}(\mu_{ack}\Rightarrow$
$\displaystyle[-1,0,0,\mathtt{I},1,0,0]$
$\displaystyle\phantom{L.\nu}x^{2}_{1}<x^{1}_{1},x^{2}_{2}=x^{1}_{2},x^{2}_{3}=x^{1}_{3}$
$\displaystyle\phantom{smallspa}\mathbf{case}\,Lx^{2}(\mathit{ack}\Rightarrow
Ry^{0}.\mu_{nat};$ $\displaystyle[-1,0,0,\mathtt{I},1,0,1]$
$\displaystyle\phantom{L.\nu}y^{1}_{1}=y^{0}_{1},y^{1}_{2}=y^{0}_{2}$
$\displaystyle\phantom{caseeLx^{1}(label}Ry^{1}.\mathit{s};y^{1}\leftarrow\mathtt{Producer}\leftarrow
x^{2}$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[-1,0,0,\mathtt{P},1,0,1]}$

${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[-1,0,0,\mathtt{P},1,0,1]}<{[0,0,0,\mathtt{I},1,0,0]}$
and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[0,0,0,\mathtt{I},1,0,0]}<{[0,0,0,\mathtt{P},0,0,0]}$
hold, and both mutually recursive calls are recognized to be valid, as they
are, without a need to substitute process definitions.

However, not every relation over the process variables forms a partial order.
For instance, having both $\mathtt{P}\subset_{2}\mathtt{I}$ and
$\mathtt{I}\subset_{2}\mathtt{P}$ violates the antisymmetry condition.
Introducing the position of process variables into $list(\\_,\\_)$ is also a
delicate issue. For example, if we have both $\mathtt{I}\subset_{1}\mathtt{P}$
and $\mathtt{I}\subset_{2}\mathtt{P}$, it is not determined where to insert
the value of $\mathtt{Producer}$ and $\mathtt{Idle}$ on the $list(\\_,\\_)$.
Definition 7.20 captures the idea of Example 7.19. It defines the relation
$\subseteq$, given that the programmer introduces a family of partial orders
such that their domains partition the set of process variables $V$. We again
assume that the programmer defines this family based on the intuition of why a
program satisfies strong progress. Definition 7.19 ensures that $\subseteq$ is
a well-defined partial order and it is uniquely determined in which position
of $list(\\_,\\_)$ the process variables shall be inserted. Definition 7.22
gives the lexicographic order on $list(\\_,\\_)$ augmented with the
$\subseteq$ relation.

######  Definition 7.20.

Consider a program $\mathcal{P}=\langle V,S\rangle$ defined over a signature
$\Sigma$. Let $\\{\subseteq_{i}\\}_{0\leq i\leq n}$ be a disjoint family of
partial orders whose domains partition the set of process variables $V$, where
(a) $X\cong_{i}Y$ iff $X\subseteq_{i}Y$ and $Y\subseteq_{i}X$, and (b)
$X\subset_{i}Y$ iff $X\subseteq_{i}Y$ but $X\not\cong_{i}Y$.

We define $\subseteq$ as $\bigcup_{i\leq n}\subseteq_{i}$, i.e. $F\subseteq G$
iff $F\subseteq_{i}G$ for some (unique) $i\leq n$. It is straightforward to
see that $\subseteq$ is a partial order over the set of process variables $V$.
Moreover, we define (c) $X\cong Y$ iff $X\cong_{i}Y$ for some (unique) $i$,
and (d) $X\subset Y$ iff $X\subset_{i}Y$ for some (unique) $i$.

To integrate the order on process variables ($\subset$) with the order $<$, we
need a prefix of the list from Definition 6.15. We give the following
definition of $list(x,y,j)$ to crop $list(x,y)$ exactly before the element
corresponding to a sent fixed point unfolding message for types with priority
$j$.

######  Definition 7.21.

For a process

$\bar{x}:A\vdash P::y:B,$

over signature $\Sigma$, and $0\leq j\leq n$, define $list(\bar{x},y,j)$, as a
prefix of the list $list(\bar{x},y)=[v_{i}]_{i\leq n}$ by

  1. (1)

$[]$ if $i=0$,

  2. (2)

$[[v_{i}]_{i<j},\ (\bar{x}_{j})]$ if $\epsilon(j)=\mu$,

  3. (3)

$[[v_{i}]_{i<j},\ (y_{j})]$ if $\epsilon(j)=\nu$.

We use these prefixes in the following definition.

######  Definition 7.22.

Using the orders $\subset$ and $\leq$, we define a new combined order
$(\subset,<)$ (used in the local validity condition in Section 10).

$F,list(\bar{x},y)\ (\subset,<)\ G,list(\bar{z},w)\ $

iff

  1. (1)

If $F\subset G$, i.e., $F\subset_{i}G$ for a unique $i$, then
$list(\bar{x},y,i)\leq list(\bar{z},w,i)$, otherwise,

  2. (2)

if $F\cong G$ and $list(\bar{x},y)<list(\bar{z},w)$, otherwise

  3. (3)

$list(\bar{x},y,\min(i,j))<list(\bar{z},w,\min(i,j))$, where $F$ is in the
domain of $\subseteq_{i}$ and $G$ is in the domain of $\subseteq_{j}$.

By conditions of Definition 7.20, $(\subset,<)$ is an irreflexive and
transitive relation and thus a strict partial order.

######  Example 7.23.

Consider the signature of Example 7.19

$\displaystyle\Sigma_{4}:=$
$\displaystyle\mathsf{ack}=^{1}_{\mu}\oplus\\{\mathit{ack}:\mathsf{astream}\\},$
$\displaystyle\mathsf{astream}=^{2}_{\nu}\&\\{\mathit{head}:\mathsf{ack},\ \
\mathit{tail}:\mathsf{astream}\\},$
$\displaystyle\mathsf{nat}=^{3}_{\mu}\oplus\\{\mathit{z}:1,\ \
\mathit{s}:nat\\}$

and program
$\mathcal{P}_{7}:=\langle\\{\mathtt{Idle},\mathtt{Producer}\\},\mathtt{Producer}\rangle$
with the relation $\subset$ defined over process variables as
$\mathtt{Idle}\subset_{2}\mathtt{Producer}$. For process
$x:\mathsf{astream}\vdash\mathtt{Producer}::(y:\mathsf{nat})$:

$\begin{array}[]{l}list(x,y)=[(x_{1},y_{1}),(y_{2},x_{2}),(x_{3},y_{3})],\\\
list(x,y,3)=[(x_{1},y_{1}),(y_{2},x_{2}),(x_{3})],\\\
list(x,y,2)=[(x_{1},y_{1}),(y_{2})],\\\ list(x,y,1)=[(x_{1})],\
\mathit{and}\\\ list(x,y,0)=[].\end{array}$

To check the validity of the recursive calls in Example 7.19 we observe that

  * •

$\mathtt{Producer},list(x^{2},y^{1})\,(\subset,<)\,\mathtt{Idle},list(x^{1},y^{0})$
since $list(x^{2},y^{1},2)<list(x^{1},y^{0},2)$, and

  * •

$\mathtt{Idle},list(x^{1},y^{0})\,(\subset,<)\,\mathtt{Producer},list(x^{0},y^{0})$
since $list(x^{1},y^{0},2)=list(x^{0},y^{0},2)$ and
${\mathtt{Idle}\subset_{2}\mathtt{Producer}}$.

##  8\. A Modified Rule for Cut

There is a subtle aspect of local validity that we have not discussed yet. We
need to relate a fresh channel, created by spawning a new process, with the
previously existing channels. Process $y^{\alpha}:A\vdash(x\leftarrow
P_{x};Q_{x})::(z^{\beta}:B)$, for example, creates a fresh channel $w^{0}$,
spawns process $P_{w^{0}}$ providing along channel $w^{0}$, and then continues
as $Q_{w^{0}}$. For the sake of our algorithm, we need to identify the
relation between $w^{0}$, $y^{\alpha}$, and $z^{\beta}$. Since $w^{0}$ is a
fresh channel, a naive idea is to make $w^{0}$ incomparable to any other
channel for any type variable $t\in\Sigma$. To represent this incomparability
in our examples we write “$\infty$” for the value of the fresh channel. While
sound, we will see in Example 8.24 that we can improve on this naive approach
to cover more valid processes.

######  Example 8.24.

Define the signature

$\displaystyle\Sigma_{5}:=$
$\displaystyle\mathsf{ctr}=^{1}_{\nu}\&\\{\mathit{inc}:\mathsf{ctr},\ \
\mathit{val}:\mathsf{bin}\\},$
$\displaystyle\mathsf{bin}=^{2}_{\mu}\oplus\\{\mathit{b0}:\mathsf{bin},\mathit{b1}:\mathsf{bin},\mathit{\$}:\mathsf{1}\\}.$

which provides numbers in binary representation as well as an interface to a
counter. We explore the following program
$\mathcal{P}_{8}=\langle\\{\mathtt{BinSucc},\mathtt{Counter},\mathtt{NumBits},\mathtt{BitCount}\\},\mathtt{BitCount}\rangle,$
where

$\begin{array}[]{l}x:\mathsf{bin}\vdash y\leftarrow\mathtt{BinSucc}\leftarrow
x::(y:\mathsf{bin})\\\ x:\mathsf{bin}\vdash
y\leftarrow\mathtt{Counter}\leftarrow x::(y:\mathsf{ctr})\\\
x:\mathsf{bin}\vdash y\leftarrow\mathtt{NumBits}\leftarrow
x::(y:\mathsf{bin})\\\ x:\mathsf{bin}\vdash
y\leftarrow\mathtt{BitCount}\leftarrow x::(y:\mathsf{ctr})\\\ \end{array}$

We define the relation $\subset$ on process variables as
$\mathtt{BinSucc}\subset_{0}\mathtt{Counter}\subset_{0}\mathtt{BitCount}$ and
$\mathtt{BinSucc}\subset_{0}\mathtt{NumBits}\subset_{0}\mathtt{BitCount}$. The
process definitions are as follows, shown here already with their termination
analysis.

$\displaystyle w^{\beta}\leftarrow\mathtt{BinSucc}\leftarrow z^{\alpha}=$
$\displaystyle\phantom{caseLz^{\alpha}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[0,0,\
0,\ 0]}$ $\displaystyle\phantom{sma}\mathbf{case}\,Lz^{\alpha}\
(\mu_{bin}\Rightarrow$ $\displaystyle[0,0,-1,0]$
$\displaystyle\phantom{L}z^{\alpha+1}_{1}=z^{\alpha}_{1},z^{\alpha+1}_{2}<z^{\alpha}_{2}$
$\displaystyle\phantom{smallsp}\mathbf{case}\,Lz^{\alpha+1}\
(\mathit{b0}\Rightarrow Rw^{\beta}.\mu_{bin};$ $\displaystyle{[0,0,-1,1]}$
$\displaystyle{\phantom{Lz^{0}.\nu}w^{\beta+1}_{1}=w^{\beta}_{1}}$
$\displaystyle\phantom{smallspacemorethanthat}Rw^{\beta+1}.\mathit{b1};w^{\beta+1}\leftarrow
z^{\alpha+1}$ $\displaystyle{[0,0,-1,1]}$
$\displaystyle\phantom{smallspacemorexx}\mid\mathit{b1}\Rightarrow
Rw^{\beta}.\mu_{bin};$ $\displaystyle{[0,0,-1,1]}$
$\displaystyle{\phantom{Lz^{0}.\nu}w^{\beta+1}_{1}=w^{\beta}_{1}}$
$\displaystyle\phantom{smallspacemorethanthat}Rw^{\beta+1}.\mathit{b0};w^{\beta+1}\leftarrow\mathtt{BinSucc}\leftarrow
z^{\alpha+1}$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[0,0,-1,1]}$
$\displaystyle\phantom{smallspacemorexx}\mid\mathit{\$}\Rightarrow
Rw^{\beta}.\mu_{\mathsf{bin}};Rw^{\beta+1}.b1;\ $ $\displaystyle{[0,0,-1,1]}$
$\displaystyle{\phantom{Lz^{0}.\nu}w^{\beta+1}_{1}=w^{\beta}_{1}}$
$\displaystyle\phantom{smallspacemorethanthat}Rw^{\beta+1}.\mu_{\mathsf{bin}};Rw^{\beta+2}.\$;\
w^{\beta+2}\leftarrow z^{\alpha+1}))$ $\displaystyle{[0,0,-2,2]}$
$\displaystyle{\phantom{Lz^{0}.\nu}w^{\beta+2}_{1}=w^{\beta+1}_{1}}$
$\displaystyle y^{\beta}\leftarrow\mathtt{Counter}\leftarrow w^{\alpha}=$
$\displaystyle\phantom{caseRy^{\beta}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[0,0,\
0,\ 0]}$ $\displaystyle\phantom{sma}\mathbf{case}\,Ry^{\beta}\
(\nu_{ctr}\Rightarrow$ $\displaystyle[-1,0,0,0]$
$\displaystyle\phantom{L}y^{\beta+1}_{1}<y^{\beta}_{1},y^{\beta+1}_{2}=y^{\beta}_{2}$
$\displaystyle\phantom{smallsp}\mathbf{case}\,Ry^{\beta+1}\
(\mathit{inc}\Rightarrow z^{0}\leftarrow\mathtt{BinSucc}\leftarrow
w^{\alpha};$ $\displaystyle{\mathtt{BinSucc}\subset_{0}\mathtt{Counter}}$
$\displaystyle\phantom{smallspacemorethanthat}y^{\beta+1}\leftarrow\mathtt{Counter}\leftarrow
z^{0}$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[-1,\
\infty,\ \infty,0]}$
$\displaystyle\phantom{smallspacemorexx}\mid\mathit{val}\Rightarrow
y^{\beta+1}\leftarrow w^{\alpha}))$ $\displaystyle{[-1,0,0,0]}$ $\displaystyle
w^{\beta}\leftarrow\mathtt{NumBits}\leftarrow x^{\alpha}=$
$\displaystyle\phantom{caseLx^{\alpha}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[0,0,\
0,\ 0]}$ $\displaystyle\phantom{sma}\mathbf{case}\,Lx^{\alpha}\
(\mu_{bin}\Rightarrow$ $\displaystyle[0,0,-1,0]$
$\displaystyle\phantom{L}x^{\alpha+1}_{1}=x^{\alpha}_{1},x^{\alpha+1}_{2}<x^{\alpha}_{2}$
$\displaystyle\phantom{smallsp}\mathbf{case}\,Lx^{\alpha+1}\
(\mathit{b0}\Rightarrow z^{0}\leftarrow\mathtt{NumBits}\leftarrow
x^{\alpha+1};$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[?,0,-1,?]}$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\phantom{Lx^{0}.\nu}z^{0}_{1}\stackrel{{\scriptstyle?}}{{=}}w^{\beta}_{1},z_{2}^{0}\stackrel{{\scriptstyle?}}{{=}}w^{\beta}_{2}}$
$\displaystyle\phantom{smallspacemorethanthat}w^{\beta}\leftarrow\mathtt{BinSucc}\leftarrow
z^{0}$ $\displaystyle\mathtt{BinSucc}\subset_{0}\mathtt{NumBits}$
$\displaystyle\phantom{smallspacemorexx}\mid\mathit{b1}\Rightarrow
z^{0}\leftarrow\mathtt{NumBits}\leftarrow x^{\alpha+1};$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[?,0,-1,?]}$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\phantom{Lx^{0}.\nu}z^{0}_{1}\stackrel{{\scriptstyle?}}{{=}}w^{\beta}_{1},z_{2}^{0}\stackrel{{\scriptstyle?}}{{=}}w^{\beta}_{2}}$
$\displaystyle\phantom{smallspacemorethanthatxx}w^{\beta}\leftarrow\mathtt{BinSucc}\leftarrow
z^{0}$ $\displaystyle\mathtt{BinSucc}\subset_{0}\mathtt{NumBits}$
$\displaystyle\phantom{smallspacemorexx}\mid\mathit{\$}\Rightarrow
Rw^{\beta}.\mu_{\mathsf{bin}};Rw^{\beta+1}.\$;\ w^{\beta+1}\leftarrow
x^{\alpha+1}))$ $\displaystyle{[0,0,-1,1]}$ $\displaystyle
y^{\beta}\leftarrow\mathtt{BitCount}\leftarrow
x^{\alpha}=w^{0}\leftarrow\mathtt{NumBits}\leftarrow
x^{\alpha};y^{\beta}\leftarrow\mathtt{Counter}\leftarrow w^{0}$

The program starts with process $\mathtt{BitCount}$ which creates a fresh
channel $w^{0}$, spawns a new process
$w^{0}\leftarrow\mathtt{NumBits}\leftarrow x^{\alpha}$, and continues as
$y^{\beta}\leftarrow\mathtt{Counter}\leftarrow w^{0}$.

Process $y^{\beta}\leftarrow\mathtt{Counter}\leftarrow w^{\alpha}$ as its name
suggests works as a counter where $w:\mathit{bin}$ is the current value of the
counter. When it receives an increment message $\mathit{inc}$ it computes the
successor of $w$, accessible through channel $z$. If it receives a
$\mathit{val}$ message it simply forwards the current value ($w$) to the
client ($y$). Note that in this process, both calls valid according to the
condition developed so far. This is also true for the binary successor process
$\mathtt{BinSucc}$, which presents no challenges. The only recursive call
represents the “carry” of binary addition when a number with lowest bit
$\mathit{b1}$ has to be incremented.

The process $w^{\beta}\leftarrow\mathtt{NumBits}\leftarrow x^{\alpha}$ counts
the number of bits in the binary number $x$ and sends the result along $w$,
also in the form of a binary number. It calls itself recursively for every bit
received along $x$ and increments the result $z$ to be returned along $w$.
Note that if there are no leading zeros, this computes essentially the integer
logarithm of $x$. The process $\mathtt{NumBits}$ is reactive. However with our
approach toward spawning a new process, the recursive calls have the list
value $[\infty,0,-1,\infty]\not<[0,0,0,0]$, meaning that the local validity
condition developed so far fails.

Note that we cannot just define $z_{1}^{0}=w_{1}^{\beta}$ and
$z_{2}^{0}=w_{2}^{\beta}$, or $z_{1}^{0}=z_{2}^{0}=0$. Channel $z^{0}$ is a
fresh one and its relation with the future generations depends on how it
evolves in the process $w^{\beta}\leftarrow\mathtt{BinSucc}\leftarrow z^{0}$.
But by definition of type $\mathsf{bin}$, no matter how $z^{0}:\mathsf{bin}$
evolves to some $z^{\eta}$ in process $\mathtt{BinSucc}$, it won’t be the case
that $z^{\eta}:\mathsf{ctr}$. In other words, the type $\mathsf{ctr}$ is not
visible from $\mathsf{bin}$ and for any generation $\eta$, channel $z^{\eta}$
does not send or receive a $\mathsf{ctr}$ unfolding message. So in this
recursive call, the value of $z_{1}^{\eta}$ is not important anymore and we
safely put $z_{1}^{0}=w^{\beta}_{1}$. In the improved version of the condition
we have:

$\displaystyle w^{\beta}\leftarrow\mathtt{NumBits}\leftarrow x^{\alpha}=$
$\displaystyle\phantom{caseLx^{\alpha}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[0,0,\
0,\ 0]}$ $\displaystyle\phantom{sma}\mathbf{case}\,Lx^{\alpha}\
(\mu_{bin}\Rightarrow$ $\displaystyle[0,0,-1,0]$
$\displaystyle\phantom{L}x^{\alpha+1}_{1}=x^{\alpha}_{1},x^{\alpha+1}_{2}<x^{\alpha}_{2}$
$\displaystyle\phantom{smallsp}\mathbf{case}\,Lx^{\alpha+1}\
(\mathit{b0}\Rightarrow z^{0}\leftarrow\mathtt{NumBits}\leftarrow
x^{\alpha+1};$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[0,0,-1,\infty]}$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\phantom{Lx^{0}.\nu}z^{0}_{1}=w^{\beta}_{1}}$
$\displaystyle\phantom{smallspacemorethanthat}w^{\beta}\leftarrow\mathtt{BinSucc}\leftarrow
z^{0}$ $\displaystyle\mathtt{BinSucc}\subset_{0}\mathtt{NumBits}$
$\displaystyle\phantom{smallspacemorexx}\mid\mathit{b1}\Rightarrow
z^{0}\leftarrow\mathtt{NumBits}\leftarrow x^{\alpha+1};$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[0,0,-1,\infty]}$
$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\phantom{Lx^{0}.\nu}z^{0}_{1}=w^{\beta}_{1}}$
$\displaystyle\phantom{smallspacemorethanthat}w^{\beta}\leftarrow\mathtt{BinSucc}\leftarrow
z^{0}$ $\displaystyle\mathtt{BinSucc}\subset_{0}\mathtt{NumBits}$
$\displaystyle\phantom{smallspacemorexx}\mid\mathit{\$}\Rightarrow
Rw^{\beta}.\mu_{\mathsf{bin}};Rw^{\beta+1}.\$;\ w^{\beta+1}\leftarrow
x^{\alpha+1}))$ $\displaystyle{[0,0,-1,1]}$

This version of the algorithm recognizes both recursive calls as valid. In the
following definition we capture the idea of visibility from a type more
formally.

######  Definition 8.25.

For type $A$ in a given signature $\Sigma$ and a set of type variables
$\Delta$, we define $\mathtt{c}(A;\Delta)$ inductively as:

$\begin{array}[]{l}\mathtt{c}(1;\Delta)=\emptyset,\\\
\mathtt{c}(\oplus\\{\ell:A_{\ell}\\}_{\ell\in
L};\Delta)=\mathtt{c}(\&\\{\ell:A_{\ell}\\}_{\ell\in
L};\Delta)=\bigcup_{\ell\in L}\mathtt{c}(A_{\ell};\Delta),\\\
\mathtt{c}(t;\Delta)=\\{t\\}\cup\mathtt{c}(A;\Delta\cup\\{t\\})\ \text{if}\
t=_{a}\ A\in\Sigma\ \text{and}\ t\not\in\Delta,\\\
\mathtt{c}(t;\Delta)=\\{t\\}\ \text{if}\ t=_{a}A\in\Sigma\ \text{and}\
t\in\Delta.\end{array}$

We put priority $i$ in the set $\mathtt{c}(A)$ iff for some type variable $t$
with $i=p(t)$, $t\in\mathtt{c}(A;\emptyset)$. We say that _priority $i$ is
visible from type $A$_ if and only if $i\in\mathtt{c}(A)$.

In Example 8.24, we have
$\mathtt{c}(\mathsf{bin})=\\{p(\mathsf{bin})\\}=\\{2\\}$ and
$\mathtt{c}(\mathsf{ctr})=\\{p(\mathsf{bin}),p(\mathsf{ctr})\\}=\\{1,2\\}$
which means that $\mathsf{bin}$ is visible from $\mathsf{ctr}$ but not the
other way around. This expresses that the definition of $\mathsf{ctr}$
references $\mathsf{bin}$, but the definition of $\mathsf{bin}$ does not
reference $\mathsf{ctr}$.

##  9\. Typing Rules for Session-Typed Processes with Channel Ordering

In this section we introduce inference rules for session-typed processes
corresponding to derivations in subsingleton logic with fixed points. This is
a refinement of the inference rules in Figure 2 to account for channel
generations and orderings introduced in previous sections. The judgments are
of the form

$\bar{x}^{\alpha}:\omega\vdash_{\Omega}P::(y^{\beta}:A),$

where $P$ is a process, and $x^{\alpha}$ (the $\alpha$-th generation of
channel $x$) and $y^{\beta}$ (the $\beta$-th generation of channel $y$) are
its left and right channels of types $\omega$ and $A$, respectively. The order
relation between the generations of left and right channels indexed by their
priority of types is built step by step in $\Omega$ when reading the rules
from the conclusion to the premises. We only consider judgments in which all
variables $x^{\alpha^{\prime}}$ occurring in $\Omega$ are such that
$\alpha^{\prime}\leq\alpha$ and, similarly, for $y^{\beta^{\prime}}$ in
$\Omega$ we have $\beta^{\prime}\leq\beta$. This presupposition guarantees
that if we construct a derivation bottom-up, any future generations for $x$
and $y$ are fresh and not yet constrained by $\Omega$. All our rules, again
read bottom-up, will preserve this property.

We fix a signature $\Sigma$ as in Definition 1, a finite set of process
definitions $V$ over $\Sigma$ as in Definition 3.4, and define
$\bar{x}^{\alpha}:\omega\vdash_{\Omega}P::(y^{\beta}:A)$ with the rules in
Figure 3. To preserve freshness of channels and their future generations in
$\Omega$, the channel introduced by Cut rule must be distinct from any
variable mentioned in $\Omega$. Similar to its underlying sequent calculus in
Section 3, this system is infinitary, i.e., an infinite derivation may be
produced for a given program. However, we can remove the first premise from
the Def rule and check typing for each process definition in $V$ separately.

Programs derived in this system are all well-typed, but not necessarily
_valid_. It is, however, the basis for our finitary condition in Section 10
and in Section 11 where we prove that local validity is stricter than Fortier
and Santocanale’s guard condition.

$x^{\alpha}:A\vdash_{\Omega}y^{\beta}\leftarrow x^{\alpha}::(y^{\beta}:A)$

$\bar{x}^{\alpha}:\omega\vdash_{\Omega}(w\leftarrow
P_{w};Q_{w})::(y^{\beta}:C)\lx@proof@logical@and\bar{x}^{\alpha}:\omega\vdash_{\Omega\cup\mathtt{r}(y^{\beta})}P_{w^{0}}::(w^{0}:A)\mathtt{r}(v)=\\{w^{0}_{i}=v_{i}\mid
i\not\in\mathtt{c}(A)\,\mbox{and}\,i\leq
n\\}w^{0}:A\vdash_{\Omega\cup\mathtt{r}(\bar{x}^{\alpha})}Q_{w^{0}}::(y^{\beta}:C)$

$\bar{x}^{\alpha}:\omega\vdash_{\Omega}Ry^{\beta}.k;P::(y^{\beta}:\oplus\\{\ell:A_{\ell}\\}_{\ell\in L})\bar{x}^{\alpha}:\omega\vdash_{\Omega}P::(y^{\beta}:A_{k})\quad(k\in L)$ | $x^{\alpha}:\oplus\\{\ell:A_{\ell}\\}_{\ell\in L}\vdash_{\Omega}\mathbf{case}\,Lx^{\alpha}\ (\ell\Rightarrow P_{\ell})::(y^{\beta}:C)\forall\ell\in L\quad x^{\alpha}:A_{\ell}\vdash_{\Omega}P_{\ell}::(y^{\beta}:C)$
---|---
$\bar{x}^{\alpha}:\omega\vdash_{\Omega}\mathbf{case}\,Ry^{\beta}\ (\ell\Rightarrow P_{\ell})::(y^{\beta}:\&\\{\ell:A_{\ell}\\}_{\ell\in L})\forall\ell\in L\quad\bar{x}^{\alpha}:\omega\vdash_{\Omega}P_{\ell}::(y^{\beta}:A_{\ell})$ | $x^{\alpha}:\&\\{\ell:A_{l}\\}_{\ell\in L}\vdash_{\Omega}Lx^{\alpha}.k;P::(y^{\beta}:C)k\in L\quad x^{\alpha}:A_{k}\vdash_{\Omega}P::(y^{\beta}:C)$
$.\vdash_{\Omega}\mathbf{close}\,Ry^{\beta}::(y^{\beta}:1)$ | $x^{\alpha}:1\vdash_{\Omega}\mathbf{wait}\,Lx^{\alpha};Q::(y^{\beta}:A).\vdash_{\Omega}Q::(y^{\beta}:A)$

$\bar{x}^{\alpha}:\omega\vdash_{\Omega}Ry^{\beta}.\mu_{t};P_{y^{\beta}}::(y^{\beta}:t)\lx@proof@logical@and\bar{x}^{\alpha}:\omega\vdash_{\Omega^{\prime}}P_{y^{\beta+1}}::(y^{\beta+1}:A)\Omega^{\prime}=\Omega\cup\\{(y^{\beta})_{p(s)}=(y^{\beta+1})_{p(s)}\mid
p(s)\neq p(t)\\}t=_{\mu}A$

$x^{\alpha}:t\vdash_{\Omega}\mathbf{case}\,Lx^{\alpha}\ (\mu_{t}\Rightarrow
Q_{x^{\alpha}})::(y^{\beta}:C)\lx@proof@logical@and
x^{\alpha+1}:A\vdash_{\Omega^{\prime}}Q_{x^{\alpha+1}}::(y^{\beta}:C)\Omega^{\prime}=\Omega\cup\\{x^{\alpha+1}_{p(t)}<x^{\alpha}_{p(t)}\\}\cup\\{x^{\alpha+1}_{p(s)}=x^{\alpha}_{p(s)}\mid
p(s)\neq p(t)\\}t=_{\mu}A$

$\bar{x}^{\alpha}:\omega\vdash_{\Omega}\mathbf{case}\,Ry^{\beta}\
(\nu_{t}\Rightarrow
P_{y^{\beta}})::(y^{\beta}:t)\lx@proof@logical@and\bar{x}^{\alpha}:\omega\vdash_{\Omega^{\prime}}P_{y^{\beta+1}}::(y^{\beta+1}:A)\Omega^{\prime}=\Omega\cup\\{y^{\beta+1}_{p(t)}<y^{\beta}_{p(t)}\\}\cup\\{y^{\beta+1}_{p(s)}=y^{\beta}_{p(s)}\mid
p(s)\neq p(t)\\}t=_{\nu}A$

$x^{\alpha}:t\vdash_{\Omega}Lx^{\alpha}.\nu_{t};Q_{x^{\alpha}}::(y^{\beta}:C)\lx@proof@logical@and
x^{\alpha+1}:A\vdash_{\Omega^{\prime}}Q_{x^{\alpha+1}}::(y^{\beta}:C)\Omega^{\prime}=\Omega\cup\\{(x^{\alpha+1})_{p(s)}=(x^{\alpha})_{p(s)}\mid
p(s)\neq p(t)\\}t=_{\nu}A$

$\bar{x}^{\alpha}:\omega\vdash_{\Omega}y^{\beta}\leftarrow
X\leftarrow\bar{x}^{\alpha}::(y^{\beta}:C)\lx@proof@logical@and\bar{x}^{\alpha}:\omega\vdash_{\Omega}P_{\bar{x}^{\alpha},y^{\beta}}::(y^{\beta}:C)\bar{u}:\omega\vdash
X=P_{\bar{u},w}::(w:C)\in V$

Figure 3. Infinitary Typing Rules for Processes with Channel Ordering

##  10\. A Local Validity Condition

In Sections 4 to 7.22, using several examples, we developed an algorithm for
identifying valid programs. Illustrating the full algorithm based on the
inference rules in Section 9 was postponed to this section. We reserve for the
next section our main result that the programs accepted by this algorithm
satisfy the guard condition introduced by Fortier and Santocanale [FS13].

The condition checked by our algorithm is a _local_ one in the sense that we
check validity of each process definition in a program separately. The
algorithm works on the sequents of the form

$\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;\bar{z}^{\alpha}:\omega\vdash_{\Omega,\subset}P::(w^{\beta}:C),$

where $\bar{u}^{\gamma}$ is the left channel of the process the algorithm
started with and can be either empty or $u^{\gamma}$. Similarly, $v^{\delta}$
is the right channel of the process the algorithm started with (which cannot
be empty). And $X$ is the last process variable a definition rule has been
applied to (reading the rules bottom-up). Again, in this judgment the
(in)equalities in $\Omega$ can only relate variables $z$ and $w$ from earlier
generations to guarantee freshness of later generations.

Generally speaking, when analysis of the program starts with
$\bar{u}^{\gamma}:\omega\vdash v^{\delta}\leftarrow
X\leftarrow\bar{u}^{\gamma}::(v^{\delta}:B)$, a snapshot of the channels
$\bar{u}^{\gamma}$ and $v^{\delta}$ and the process variable $X$ are saved.
Whenever the process reaches a call $\bar{z}^{\alpha}:\\_\vdash
w^{\beta}\leftarrow Y\leftarrow\bar{z}^{\alpha}::(w^{\beta}:\\_)$, the
algorithm compares $X,list(\bar{u}^{\gamma},v^{\delta})$ and
$Y,list(\bar{z}^{\alpha},w^{\beta})$ using the $(\subset,<)$ order to
determine if the call is (locally) valid. This comparison is made by the Call
rule in the rules in Figure 4, and is local in the sense that only the
interface of a process is consulted at each call site, not its definition.
Since it otherwise follows the structure of the program it is also local in
the sense of Pierce and Turner [PT00].

######  Definition 10.26.

A program $\mathcal{P}=\langle V,S\rangle$ over signature $\Sigma$ and a fixed
order $\subset$ satisfying the properties in Definition 7.20 is locally valid
iff for every $\bar{z}:A\vdash X=P_{\bar{z},w}::(w:C)\in V$, there is a
derivation for

$\langle\bar{z}^{0},X,w^{0}\rangle;\bar{z}^{0}:\omega\vdash_{\emptyset,\subset}P_{\bar{z}^{0},w^{0}}::(w^{0}:C)$

in the rule system in Figure 4. This set of rules is _finitary_ so it can be
directly interpreted as an algorithm. This results from substituting the Def
rule (of Figure 3) with the Call rule (of Figure 4). Again, to guarantee
freshness of future generations of channels, the channel introduced by Cut
rule is distinct from other variables mentioned in $\Omega$.

$\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;z^{\alpha}:A\vdash_{\Omega,\subset}w^{\beta}\leftarrow
z^{\alpha}::(w^{\beta}:A)$

$\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;\bar{z}^{\alpha}:\omega\vdash_{\Omega\subset}(x\leftarrow
P_{x};Q_{x})::(w^{\beta}:C)\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;\bar{z}^{\alpha}:\omega\vdash_{\Omega\cup\mathtt{r}(w^{\beta}),\subset}P_{x^{0}}::(x^{0}:A)\mathtt{r}(y)=\\{x^{0}_{i}=y_{i}\mid
i\not\in\mathtt{c}(A)\,\mbox{and}\,i\leq n\\}\ \
\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;x^{0}:A\vdash_{\Omega\cup\mathtt{r}(\bar{z}^{\alpha}),\subset}Q_{x^{0}}::(w^{\beta}:C)$

$\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;\bar{z}^{\alpha}:\omega\vdash_{\Omega,\subset}Rw^{\beta}.k;P::(w^{\beta}:\oplus\\{\ell:A_{l}\\}_{\ell\in
L})\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;\bar{z}^{\alpha}:\omega\vdash_{\Omega,\subset}P::(w^{\beta}:A_{k})\quad(k\in
L)$

$\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;z^{\alpha}:\oplus\\{\ell:A\\}_{\ell\in
L}\vdash_{\Omega,\subset}\mathbf{case}\,Lz^{\alpha}\ (\ell\Rightarrow
P_{\ell})::(w^{\beta}:C)\forall\ell\in
L\quad\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;z^{\alpha}:A_{\ell}\vdash_{\Omega,\subset}P_{\ell}::(w^{\beta}:C)$

$\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;\bar{z}^{\alpha}:\omega\vdash_{\Omega,\subset}\mathbf{case}\,Rw^{\beta}\
(\ell\Rightarrow P_{\ell})::(w^{\beta}:\&\\{\ell:A_{\ell}\\}_{\ell\in
L})\forall\ell\in
L\quad\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;\bar{z}^{\alpha}:\omega\vdash_{\Omega,\subset}P_{\ell}::(w^{\beta}:A_{\ell})$

$\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;z^{\alpha}:\&\\{\ell:A_{\ell}\\}_{\ell\in
L}\vdash_{\Omega,\subset}Lz^{\alpha}.k;P::(w^{\beta}:C)(k\in
L)\quad\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;z^{\alpha}:A_{k}\vdash_{\Omega,\subset}P::(w^{\beta}:C)$

$\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;\cdot\vdash_{\Omega,\subset}\mathbf{close}\,R::(w^{\beta}:1)$ | $\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;z^{\alpha}:1\vdash_{\Omega,\subset}\mathbf{wait}\,Lz^{\alpha};Q::(w^{\beta}:A)\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;\cdot\vdash_{\Omega,\subset}Q::(w^{\beta}:A)$
---|---

$\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;\bar{z}^{\alpha}:\omega\vdash_{\Omega,\subset}Rw^{\beta}.\mu_{t};P_{w^{\beta}}::(w^{\beta}:t)\lx@proof@logical@and\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;\bar{z}^{\alpha}:\omega\vdash_{\Omega^{\prime},\subset}P_{w^{\beta+1}}::(w^{\beta+1}:A)\Omega^{\prime}=\Omega\cup\\{w^{\beta}_{p(s)}=w^{\beta+1}_{p(s)}\mid
p(s)\neq p(t)\\}t=_{\mu}A$

$\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;z^{\alpha}:t\vdash_{\Omega,\subset}\mathbf{case}\,Lz^{\alpha}\
(\mu_{t}\Rightarrow
Q_{z^{\alpha}})::(w^{\beta}:C)\lx@proof@logical@and\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;z^{\alpha+1}:A\vdash_{\Omega^{\prime},\subset}Q_{z^{\alpha+1}}:(w^{\beta}::C)\Omega^{\prime}=\Omega\cup\\{z^{\alpha+1}_{p(t)}<z^{\alpha}_{p(t)}\\}\cup\\{z^{\alpha+1}_{p(s)}=z^{\alpha}_{p(s)}\mid
p(s)\neq p(t)\\}t=_{\mu}A$

$\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;\bar{z}^{\alpha}:\omega\vdash_{\Omega,\subset}\mathbf{case}\,Rw^{\beta}\
(\nu_{t}\Rightarrow
P_{w^{\beta}})::(w^{\beta}:t)\lx@proof@logical@and\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;\bar{z}^{\alpha}:\omega\vdash_{\Omega^{\prime},\subset}P_{w^{\beta+1}}::(w^{\beta+1}:A)\Omega^{\prime}=\Omega\cup\\{w^{\beta+1}_{p(t)}<w^{\beta}_{p(t)}\\}\cup\\{w^{\beta+1}_{p(s)}=w^{\beta}_{p(s)}\mid
p(s)\neq p(t)\\}t=_{\nu}A$

$\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;z^{\alpha}:t\vdash_{\Omega,\subset}Lz^{\alpha}.\nu_{t};Q_{z^{\alpha}}::(w^{\beta}:C)\lx@proof@logical@and\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;z^{\alpha+1}:A\vdash_{\Omega^{\prime},\subset}Q_{z^{\alpha+1}}::(w^{\beta}:C)\Omega^{\prime}=\Omega\cup\\{z^{\alpha+1}_{p(s)}=z^{\alpha}_{p(s)}\mid
p(s)\neq p(t)\\}t=_{\nu}A$

$\langle\bar{u}^{\gamma},X,v^{\delta}\rangle;\bar{z}^{\alpha}:\omega\vdash_{\Omega,\subset}w^{\beta}\leftarrow
Y\leftarrow\bar{z}^{\alpha}::(w^{\beta}:C)\lx@proof@logical@and
Y,list(\bar{z}^{\alpha},w^{\beta})\ (\subset,<_{\Omega})\
X,list(\bar{u}^{\gamma},v^{\delta})\bar{x}:\omega\vdash
Y=P_{\bar{x},y}::(y:C)\in V$

Figure 4. Finitary Rules for Local Validity

The starting point of the algorithm can be of an arbitrary form

$\langle\bar{z}^{\alpha},X,w^{\beta}\rangle;\bar{z}^{\alpha}:\omega\vdash_{\Omega,\subset}P_{z^{\alpha},w^{\beta}}::(w^{\beta}:C),$

as long as $\bar{z}^{\alpha+i}$ and $w^{\beta+i}$ do not occur in $\Omega$ for
every $i>0$. In both the inference rules and the algorithm, it is implicitly
assumed that the next generation of channels introduced in the $\mu/\nu-R/L$
rules do not occur in $\Omega$. Having this condition we can convert a proof
for

$\langle\bar{z}^{0},X,w^{0}\rangle;\bar{z}^{0}:\omega\vdash_{\emptyset,\subset}P_{z^{0},w^{0}}::(w^{0}:C),$

to a proof for

$\langle\bar{z}^{\alpha},X,w^{\beta}\rangle;\bar{z}^{\alpha}:\omega\vdash_{\Omega,\subset}P_{z^{\alpha},w^{\beta}}::(w^{\beta}:C),$

by rewriting each $\bar{z}^{\gamma}$ and $w^{\delta}$ in the proof as
$\bar{z}^{\gamma+\alpha}$ and $w^{\delta+\beta}$, respectively. This simple
proposition is used in the next section where we prove that every locally
valid process accepted by our algorithm is a valid proof according to the FS
guard condition.

######  Proposition 10.27.

If there is a deduction of

$\langle\bar{z}^{0},X,w^{0}\rangle;\bar{z}^{0}:\omega\vdash_{\emptyset,\subset}P_{z^{0},w^{0}}::(w^{0}:C),$

then there is also a deduction of

$\langle\bar{z}^{\alpha},X,w^{\beta}\rangle;\bar{z}^{\alpha}:\omega\vdash_{\Omega,\subset}P_{z^{\alpha},w^{\beta}}::(w^{\beta}:C),$

if for all $0<i$, $\bar{z}^{\alpha+i}$ and $w^{\beta+i}$ do not occur in
$\Omega$.

######  Proof 10.28.

By substitution, as explained above.

To show the algorithm in action we run it over program
$\mathcal{P}_{3}:=\langle\\{\mathtt{Copy}\\},\mathtt{Copy}\rangle$ previously
defined in Example 4.8.

######  Example 10.29.

Consider program
$\mathcal{P}_{3}:=\langle\\{\mathtt{Copy}\\},\mathtt{Copy}\rangle$ over
signature $\Sigma_{1}$ where $\mathtt{Copy}$ has types
$x:\mathsf{nat}\vdash\mathtt{Copy}::(y:\mathsf{nat})$.

$\displaystyle\Sigma_{1}:=\mathsf{nat}=^{1}_{\mu}\oplus\\{\mathit{z}:\mathsf{1},\mathit{s}:\mathsf{nat}\\},$
$\displaystyle y\leftarrow\mathtt{Copy}\leftarrow x=\mathbf{case}\,Lx\
(\mu_{nat}\Rightarrow\mathbf{case}\,Lx\ $ $\displaystyle(\ z\Rightarrow
Ry.\mu_{nat};Ry.z;\mathbf{wait}\,Lx;\mathbf{close}\,Ry$ $\displaystyle\mid
s\Rightarrow Ry.\mu_{nat};Ry.s;y\leftarrow\mathtt{Copy}\leftarrow x)).$

In this example, following Definition 7.20 the programmer has to define
$\mathtt{Copy}\subseteq_{1}\mathtt{Copy}$ since the only priority in $\Sigma$
is $1$. To verify local validity of this program we run our algorithm over the
definition of $\mathtt{Copy}$. Here we show the interesting branch of the
constructed derivation:

$\small x^{0}:\mathsf{nat}\vdash_{\emptyset}\mathbf{case}\,Lx^{0}\
(\mu_{nat}\Rightarrow\cdots)::(y^{0}:\mathsf{nat})x^{1}:1\oplus\mathsf{nat}\vdash_{\\{x^{1}_{1}<x^{0}_{1}\\}}\mathbf{case}\,Lx^{1}\
(\cdots)::(y^{0}:\mathsf{nat})\lx@proof@logical@and
x^{1}:\mathsf{1}\vdash_{\\{x^{1}_{1}<x^{0}_{1}\\}}Ry^{0}.\mu_{nat};\cdots::(y^{0}:\mathsf{nat})x^{1}:\mathsf{nat}\vdash_{\\{x^{1}_{1}<x^{0}_{1}\\}}Ry^{0}.\mu_{nat};\cdots::(y^{0}:\mathsf{nat})x^{1}:\mathsf{nat}\vdash_{\\{x^{1}_{1}<x^{0}_{1}\\}}Ry^{1}.s;\cdots::(y^{1}:1\oplus\mathsf{nat})x^{1}:\mathsf{nat}\vdash_{\\{x^{1}_{1}<x^{0}_{1}\\}}y^{1}\leftarrow\mathtt{Copy}\leftarrow
x^{1}::(y^{1}:\mathsf{nat})\lx@proof@logical@and[x^{1}_{1},\mathtt{Copy},y^{1}_{1}]\,(\subset,<_{\\{x^{1}_{1}<x^{0}_{1}\\}})\,[x^{0}_{1},\mathtt{Copy},y^{0}_{1}]\
\
x:\mathsf{nat}\vdash\mathtt{Copy}=(\mathbf{case}\,Lx\,(\cdots))_{x,y}::(y:\mathsf{nat})\in
V$

As being checked by the Call rule,
$[x^{1}_{1},\mathtt{Copy},y^{1}_{1}]\,(\subset,<_{\\{x^{1}_{1}<x^{0}_{1}\\}})\,[x^{0}_{1},\mathtt{Copy},y^{0}_{1}]$
and the recursive call is accepted. In this particular setting in which
$\mathsf{Copy}$ calls _itself_ recursively, the condition of the Call rule can
be reduced to
$[x^{1}_{1},y^{1}_{1}]\,<_{\\{x^{1}_{1}<x^{0}_{1}\\}}\,[x^{0}_{1},y^{0}_{1}]$.

Note that at a meta-level the generations on channel names and the set
$\Omega$ are both used for bookkeeping purposes. We showed in this example
that using the rules of Figure 4 as an algorithm we can annotate the given
definition of a process variable with the generations and the set $\Omega$.

##  11\. Local Validity and Guard Conditions

Fortier and Santocanale [FS13] introduced a guard condition for identifying
valid circular proofs among all infinite pre-proofs in the singleton logic
with fixed points. They showed that the pre-proofs satisfying this condition,
which is based on the definition of left $\mu$\- and right $\nu$-traces, enjoy
the cut elimination property. In this section, we translate their guard
condition into the context of session-typed concurrency and generalize it for
subsingleton logic. It is straightforward to show that the cut elimination
property holds for a proof in subsingleton logic if it satisfies the
generalized version of the guard condition. The key idea is that cut
reductions for individual rules stay untouched in subsingleton logic and rules
for the new constant $1$ only provide more options for the cut reduction
algorithm to terminate. We prove that all locally valid programs in the
session typed system, determined by the algorithm in Section 10, also satisfy
the guard condition. We conclude that our algorithm imposes a stricter but
local version of validity on the session-typed programs corresponding to
circular pre-proofs.

Here we adapt definitions of the left and right traceable paths, left $\mu$-
and right $\nu$-traces, and then validity to our session type system.

######  Definition 11.30.

Consider path $\mathbb{P}$ in the (infinite) typing derivation of a program
$\mathcal{Q}=\langle V,S\rangle$ defined on a signature $\Sigma$:

${\bar{z}^{\alpha}:\omega\vdash_{\Omega}Q::(w^{\beta}:C)\vdots{\bar{x}^{\gamma}:\omega^{\prime}\vdash_{\Omega^{\prime}}Q^{\prime}::(y^{\delta}:C^{\prime})}}$

$\mathbb{P}$ is called left traceable if $\bar{z}$ and $\bar{x}$ are non-empty
and $\bar{z}=\bar{x}$. It is called right traceable if $w=y$.

Moreover, $\mathbb{P}$ is called a _cycle_ over program $\mathcal{Q}$, if for
some $X\in V$, we have $Q=w^{\beta}\leftarrow X\leftarrow\bar{z}^{\alpha}$ and
$Q^{\prime}=y^{\delta}\leftarrow X\leftarrow\bar{x}^{\gamma}$.

######  Definition 11.31.

A path $\mathbb{P}$ in the (infinite) typing derivation of a program
$\mathcal{Q}=\langle V,S\rangle$ defined over signature $\Sigma$ is a left
$\mu$-trace if (i) it is left-traceable, (ii) there is a left fixed point rule
applied on it, and (iii) the highest priority of its left fixed point rule is
$i\leq n$ such that $\epsilon(i)=\mu$. Dually, $\mathbb{P}$ is a right
$\nu$-trace if (i) it is right-traceable, (ii) there is a right fixed point
rule applied on it, and (iii) the highest priority of its right fixed point is
$i\leq n$ such that $\epsilon(i)=\nu$.

######  Definition 11.32 (FS guard condition on cycles).

A program $\mathcal{Q}=\langle V,S\rangle$ defined on Signature $\Sigma$
satisfies the FS guard condition if every cycle $\mathbb{C}$

${\bar{z}^{\alpha}:\omega\vdash_{\Omega}w^{\beta}\leftarrow
X\leftarrow\bar{z}^{\alpha}::(w^{\beta}:C)\vdots{\bar{x}^{\gamma}:\omega^{\prime}\vdash_{\Omega^{\prime}}y^{\delta}\leftarrow
X\leftarrow\bar{x}^{\gamma}::(y^{\delta}:C^{\prime})}}$

over $\mathcal{Q}$ is either a left $\mu$-trace or a right $\nu$-trace.
Similarly, we say a single cycle $\mathbb{C}$ satisfies the guard condition if
it is either a left $\mu$-trace or a right $\nu$-trace.

Definitions 11.30-11.32 are equivalent to the definitions of the same concepts
by Fortier and Santocanale using our own notation. As an example, consider
program $\mathcal{P}_{3}:=\langle\\{\mathtt{Copy}\\},\mathtt{Copy}\rangle$
over signature $\Sigma_{1}$, defined in Example 4.8, where $\mathtt{Copy}$ has
types $x:\mathsf{nat}\vdash\mathtt{Copy}::(y:\mathsf{nat})$.

$\displaystyle\Sigma_{1}:=\mathsf{nat}=^{1}_{\mu}\oplus\\{\mathit{z}:\mathsf{1},\mathit{s}:\mathsf{nat}\\}$
$\displaystyle y\leftarrow\mathtt{Copy}\leftarrow x=\mathbf{case}\,Lx\
(\mu_{nat}\Rightarrow\mathbf{case}\,Lx\ $ $\displaystyle(\ z\Rightarrow
Ry.\mu_{nat};Ry.z;\mathbf{wait}\,Lx;\mathbf{close}\,Ry$ $\displaystyle\mid
s\Rightarrow Ry.\mu_{nat};Ry.s;y\leftarrow\mathtt{Copy}\leftarrow x))$

Consider the first several steps of the derivation of the program starting
with
$x^{0}:\mathsf{nat}\vdash_{\emptyset}y^{0}\leftarrow\mathtt{Copy}\leftarrow
x^{0}::(y^{0}:\mathsf{nat})$:

$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}x^{0}:\mathsf{nat}\vdash_{\emptyset}y^{0}\leftarrow\mathtt{Copy}\leftarrow
x^{0}::(y^{0}:\mathsf{nat})x^{0}:\mathsf{nat}\vdash_{\emptyset}\mathbf{case}\,Lx^{0}\
(\mu_{nat}\Rightarrow\cdots)::(y^{0}:\mathsf{nat})x^{1}:1\oplus\mathsf{nat}\vdash_{\\{x^{1}_{1}<x^{0}_{1}\\}}\mathbf{case}\,Lx^{1}\
(\cdots)::(y^{0}:\mathsf{nat})\lx@proof@logical@and
x^{1}:\mathsf{1}\vdash_{\\{x^{1}_{1}<x^{0}_{1}\\}}Ry^{0}.\mu_{nat};\cdots::(y^{0}:\mathsf{nat})x^{1}:\mathsf{nat}\vdash_{\\{x^{1}_{1}<x^{0}_{1}\\}}Ry^{0}.\mu_{nat};\cdots::(y^{0}:\mathsf{nat})x^{1}:\mathsf{nat}\vdash_{\\{x^{1}_{1}<x^{0}_{1}\\}}Ry^{1}.s;\cdots::(y^{1}:1\oplus\mathsf{nat})\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}x^{1}:\mathsf{nat}\vdash_{\\{x^{1}_{1}<x^{0}_{1}\\}}y^{1}\leftarrow\mathtt{Copy}\leftarrow
x^{1}::(y^{1}:\mathsf{nat})$

The path between

${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}x^{0}:\mathsf{nat}\vdash_{\emptyset}y^{0}\leftarrow\mathtt{Copy}\leftarrow
x^{0}::(y^{0}:\mathsf{nat})}$

and

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}x^{1}:\mathsf{nat}\vdash_{\\{x^{1}_{1}<x^{0}_{1}\\}}y^{1}\leftarrow\mathtt{Copy}\leftarrow
x^{1}::(y^{1}:\mathsf{nat})}$

is by definition both left traceable and right traceable, but it is only a
left $\mu$-trace and not a right $\nu$-trace: the highest priority of a fixed
point applied on the left-hand side on this path belongs to a positive type;
this application of the $\mu L$ rule added $x^{1}_{1}<x^{0}_{1}$ to the set
defining the $<$ order. However, there is no negative fixed point rule applied
on the right, and $y_{1}^{1}$ and $y_{1}^{0}$ are incomparable to each other.

This cycle satisfies the guard condition by being a left $\mu$-trace. We
showed in Example 10.29 that it is also accepted by our algorithm since
$list(x^{1},y^{1})=[(x^{1}_{1},y^{1}_{1})]<[(x^{0}_{1},y^{0}_{1})]=list(x^{0},y^{0})$.

Here, we can observe that being a left $\mu$-trace coincides with having the
relation $x^{1}_{1}<x^{0}_{1}$ between the left channels, and not being a
right $\nu$-trace coincides with not having the relation $y^{1}_{1}<y^{0}_{1}$
for the right channels. We can generalize this observation to every path and
every signature with $n$ priorities.

######  Definition 11.33.

Consider a signature $\Sigma$ and a channel $x^{\gamma}$. We define the list
$[x^{\gamma}]$ as $[x_{1}^{\gamma},\cdots,x_{n}^{\gamma}]$.

######  Theorem 11.34.

A cycle $\mathbb{C}$

${\bar{z}^{\alpha}:\omega\vdash_{\Omega}w^{\beta}\leftarrow
X\leftarrow\bar{z}^{\alpha}::(w^{\beta}:C)\vdots{\bar{x}^{\gamma}:\omega^{\prime}\vdash_{\Omega^{\prime}}y^{\delta}\leftarrow
X\leftarrow\bar{x}^{\gamma}::(y^{\delta}:C^{\prime})}}$

on a program $\mathcal{Q}=\langle V,S\rangle$ defined over Signature $\Sigma$
is a left $\mu$-trace if $\bar{x}$ and $\bar{z}$ are non-empty and the list
$[x^{\gamma}]=[x_{1}^{\gamma},\cdots,x_{n}^{\gamma}]$ is lexicographically
less than the list $[z^{\alpha}]=[z_{1}^{\alpha},\cdots,z_{n}^{\alpha}]$ by
the order $<_{\Omega^{\prime}}$ built in $\Omega^{\prime}$. Dually, it is a
right $\nu$-trace, if the list
$[y^{\delta}]=[y_{1}^{\delta},\cdots,y_{n}^{\delta}]$ is lexicographically
less than the list $[w^{\beta}]=[w_{1}^{\beta},\cdots,w_{n}^{\beta}]$ by the
strict order $<_{\Omega^{\prime}}$ built in $\Omega^{\prime}$

######  Proof 11.35.

This theorem is a corollary of Lemmas 11.36 and 11.38 proved in Appendix A.

######  Lemma 11.36.

Consider a path $\mathbb{P}$ in the (infinite) typing derivation of a program
$\mathcal{Q}=\langle V,S\rangle$ defined on a signature $\Sigma$,

${z^{\alpha}:\omega\vdash_{\Omega}P::(w^{\beta}:C)\vdots{x^{\gamma}:\omega^{\prime}\vdash_{\Omega^{\prime}}P^{\prime}::(y^{\delta}:C^{\prime})}}$

with $n$ the maximum priority in $\Sigma$.

  1. (a)

For every $i\in\mathtt{c}(\omega^{\prime})$ with $\epsilon(i)=\mu$, if
$x^{\gamma}_{i}\leq_{\Omega^{\prime}}z^{\alpha}_{i}$ then $x=z$ and
$i\in\mathtt{c}(\omega)$.

  2. (b)

For every $i<n$, if $x^{\gamma}_{i}<_{\Omega^{\prime}}z^{\alpha}_{i}$, then
$i\in\mathtt{c}(\omega)$ and a $\mu L$ rule with priority $i$ is applied on
$\mathbb{P}$.

  3. (c)

For every $c\leq n$ with $\epsilon(c)=\nu$, if
$x^{\gamma}_{c}\leq_{\Omega^{\prime}}z^{\alpha}_{c}$ , then no $\nu L$ rule
with priority $c$ is applied on $\mathbb{P}$.

######  Proof 11.37.

The complete proof by induction on the structure of $\mathbb{P}$ is given in
Appendix A.

######  Lemma 11.38.

Consider a path $\mathbb{P}$ in the (infinite) typing derivation of a program
$\mathcal{Q}=\langle V,S\rangle$ defined on a Signature $\Sigma$,

${\bar{z}^{\alpha}:\omega\vdash_{\Omega}P::(w^{\beta}:C)\vdots{\bar{x}^{\gamma}:\omega^{\prime}\vdash_{\Omega^{\prime}}P^{\prime}::(y^{\delta}:C^{\prime})}}$

with $n$ the maximum priority in $\Sigma$.

  1. (a)

For every $i\in\mathtt{c}(\omega^{\prime})$ with $\epsilon(i)=\nu$, if
$y^{\delta}_{i}\leq_{\Omega^{\prime}}w^{\beta}_{i}$, then $y=w$ and
$i\in\mathtt{c}(\omega)$.

  2. (b)

If $y^{\delta}_{i}<_{\Omega^{\prime}}w_{i}^{\beta}$, then
$i\in\mathtt{c}(\omega)$ and a $\nu L$ rule with priority $i$ is applied on
$\mathbb{P}$ .

  3. (c)

For every $c\leq n$ with $\epsilon(c)=\mu$, if
$y^{\delta}_{c}\leq_{\Omega^{\prime}}w^{\beta}_{c}$, then no $\mu R$ rule with
priority $c$ is applied on $\mathbb{P}$ .

######  Proof 11.39.

Dual to the proof of Lemma 11.36 given in Appendix A.

We provide a few additional examples to elaborate Theorem 11.34 further.
Define a program
$\mathcal{P}_{9}:=\langle\\{\mathtt{Succ},\mathtt{Copy},\mathtt{SuccCopy}\\},\mathtt{SuccCopy}\rangle$,
over the signature $\Sigma_{1}$, using the process $\
w:\mathsf{nat}\vdash\mathtt{Copy}::(y:\mathsf{nat})$ and two other processs:
$x:\mathsf{nat}\vdash\mathtt{Succ}::(w:\mathsf{nat})$ and $\
x:\mathsf{nat}\vdash\mathtt{SuccCopy}::(y:\mathsf{nat})$. The processes are
defined as

$\displaystyle w\leftarrow\mathtt{Succ}\leftarrow
x=Rw.\mu_{nat};Rw.s;w\leftarrow x$ $\displaystyle
y\leftarrow\mathtt{Copy}\leftarrow w=\mathbf{case}\,Lw\
(\mu_{nat}\Rightarrow\mathbf{case}\,Lw\ $ $\displaystyle(\
\mathit{s}\Rightarrow
Ry.\mu_{nat};Ry.\mathit{s};y\leftarrow\mathtt{Copy}\leftarrow w$
$\displaystyle\mid\mathit{z}\Rightarrow
Ry.\mu_{nat};Ry.\mathit{z};\mathbf{wait}\,Lw;\mathbf{close}\,Ry))$
$\displaystyle y\leftarrow\mathtt{SuccCopy}\leftarrow
x=w\leftarrow\mathtt{Succ}\leftarrow x;y\leftarrow\mathtt{Copy}\leftarrow w,$

Process $\mathtt{SuccCopy}$ spawns a new process $\mathtt{Succ}$ and continues
as $\mathtt{Copy}$. The $\mathtt{Succ}$ process prepends an $\mathit{s}$ label
to the beginning of the finite string representing a natural number on its
left hand side and then forwards the string as a whole to the right.
$\mathtt{Copy}$ receives this finite string representing a natural number, and
_forwards_ it to the right label by label.

The only recursive process in this program is $\mathtt{Copy}$. So program
$\mathcal{P}_{9}$, itself, does not have a further interesting point to