11institutetext: [24]7.ai

# On the Fragility of Active Learners

Abhishek Ghose 11 Emma Nguyen 11

###### Abstract

Active learning (AL) techniques aim to maximally utilize a labeling budget by
iteratively selecting instances that are most likely to improve prediction
accuracy. However, their benefit compared to random sampling has not been
consistent across various setups, e.g., different datasets, classifiers. In
this empirical study, we examine how a combination of different factors might
obscure any gains from an AL technique.

Focusing on text classification, we rigorously evaluate AL techniques over
around $1000$ experiments that vary wrt the dataset, batch size, text
representation and the classifier. We show that AL is only effective in a
narrow set of circumstances. We also address the problem of using metrics that
are better aligned with real world expectations.

The impact of this study is in its insights for a practitioner: (a) the choice
of text representation and classifier is as important as that of an AL
technique, (b) choice of the right metric is critical in assessment of the
latter, and, finally, (c) reported AL results must be holistically
interpreted, accounting for variables other than just the query strategy.

###### Keywords:

First keyword Second keyword Another keyword.

##  1 Introduction

Within a supervised learning setup, Active Learning (AL) techniques use a
_Query Strategy (QS)_ to identify an unlabeled set of instances which is
optimal in the following sense: if labelled and added to the training data,
they lead to the greatest improvement in model accuracy, relative to any other
same-sized set. In cases where labelling is expensive, using AL is cost-
efficient compared to _random sampling_ , because the model reaches greater
accuracy with a smaller number of labelled instances. AL techniques can be
both domain-agnostic, e.g., _uncertainty-based sampling_ [16], or domain
specific, e.g., _Contrastive Active Learning_ [21] for Natural Language
Processing (NLP).

Our focus here is AL for text classification. Today, a practitioner has easy
access to a variety of powerful classifiers via packages such as _scikit-
learn_ [25] and _Hugging Face_ [34], and text representations, such as
_Universal Sentence Encoding (USE)_ [3] and _MPNet_ [31]. Within that context,
we ask these questions: is the choice of AL algorithm still as important? Do
AL techniques exhibit strong performance over random sampling with any
combination of text representation and a classifier?

In this empirical work, we answer this question in the _negative_ : AL
techniques can be _fragile_ , i.e., they are heavily influenced by other
variables. This study is valuable for the following reasons:

  1. 1.

In practice, where data labeling is costly, should one just spend time seeking
a good AL algorithm? Or should they cast their net of design choices wider to
take into account the classifier and representation as well?

  2. 2.

An important part of assessing a technique is _how_ we measure, i.e., metrics
used. We discuss this aspect too, e.g., rank-based metrics such as the
_Wilcoxon test_ or _Mean Rank_ ignore how large is the accuracy gap wrt random
sampling.

The practical implication of this is that a small gap might not justify the
cost of an AL workflow, given that random sampling is trivial to use in most
programming languages.

  3. 3.

Finally, this cautions us as consumers of research that an AL technique is not
just the QS; reported results must be carefully understood to be situated
within, and affected by, other significant experiment variables such as the
classifier, representation, batch size, etc.

To our knowledge, this is the first such comprehensive study of AL algorithms
for the task of text classification. The rest of the paper is organized as
follows:

##  2 Previous Work

The field of AL has seen a steady stream of novel contributions over the
years, e.g., [16, 12, 29, 7]. Being a hard problem - identifying important
instances having only seen a few examples from the instance-label distribution
- it also seems to suffer from real-world challenges, e.g., wrt variations in
dataset, batch sizes, classifier used, which has been pointed out in the
literature [1, 35, 18, 20].

In the domain of NLP, the problem is compounded by the fact that text
representations may vary widely. This is pertinent since a lot of rich
representations have been proposed in the past few years, e.g., _word2vec_
[22], _Universal Sentence Encodings (USE)_ [3], _Backpacks_ [14], _BERT_ [10],
_MiniLM_ [33], _MPNet_ [31]. We are not aware of any work that studies AL’s
effectiveness in context of these relatively modern representations. Hence,
this work constitutes a useful addition to the line of work that draws
attention to challenges of AL deployment.

##  3 Batch Active Learning - Overview

In this work, we study AL techniques for the task of _text classification_ ,
in the _batch_ AL setting. To ensure no ambiguity, we provide pseudo-code for
this AL setting in Algorithm 1.

Input: Unlabeled data $X_{U}$, test data $(X_{test},Y_{test})$, query strategy
$\mathcal{Q}$, seed set selection strategy $\mathcal{A}$, search space
$\Theta$ for model $\mathcal{M}$, seed size $s$, batch size $b$, number of
iterations $T$, metric $\mathcal{V}$

Result: Scores on test set at various iterations
$\\{(\mathcal{V}_{0},0),(\mathcal{V}_{1},1),...,(\mathcal{V}_{T},T)\\}$

$result\leftarrow\\{\\}$ // to be returned

1 $X_{L,0},X_{U,0}\leftarrow\mathcal{A}(X_{U},s)$

2 $(X_{L,0},Y_{L,0})\leftarrow\text{obtain labels for }X_{L,0}$

$M_{0}\leftarrow\operatorname*{arg\,max}_{\theta\in\Theta}M_{\theta}((X_{L,0},Y_{L,0}))$
// both model selection and calibration are performed

3 $\mathcal{V}_{0}\leftarrow\mathcal{V}(M_{0}(X_{test}),Y_{test})$

4 $result\leftarrow result\cup\\{(\mathcal{V}_{0},0)\\}$

5 for  _$t\leftarrow 1$ to $T$_ do

6
$X_{L,t}^{new},X_{U,t}\leftarrow\mathcal{Q}(M_{t-1},X_{U,t-1},(X_{L,t-1},Y_{L,t-1}),b)$

7 $(X_{L,t}^{new},Y_{L,t}^{new})\leftarrow\text{obtain labels for
}X_{L,t}^{new}$

8 $(X_{L,t},Y_{L,t})\leftarrow\text{add }(X_{L,t}^{new},Y_{L,t}^{new})\text{
to previous labeled pool }(X_{L,t-1},y_{L,t-1})$

$M_{t}\leftarrow\operatorname*{arg\,max}_{\theta\in\Theta}M_{\theta}((X_{L,t},Y_{L,t}))$
// both model selection and calibration are performed

9 $\mathcal{V}_{t}\leftarrow\mathcal{V}(M_{t}(X_{test}),Y_{test})$

10 $result\leftarrow result\cup\\{(\mathcal{V}_{t},t)\\}$

11

12 end for

return $result$

Algorithm 1 Batch Active Learning.

At a high-level, at every AL iteration $1\leq t\leq T$, we use a query
strategy $\mathcal{Q}$ to select a $b$-sized batch of instances from the
unlabeled pool of data (line 8). We obtain labels for this set (line 9) and
add it to the existing pool of labeled data (line 10). We then train a model
$M_{t}$ over this data (line 11). We emphasize that:

  1. 1.

The model $M_{t}$ is obtained after performing _model selection_ over its
hyperparameter space $\Theta$, using _grid-search_ against a _validation set_.
The validation set is a label-stratified subset (a $20\%$ split) of the
current labeled set; the rest is used for training.

  2. 2.

The model is also _calibrated_ 111A notable exception is in our use of the
_RoBERTa_ model, which already is well calibrated [9].. This is critical since
query strategies $\mathcal{Q}$ often use the predicted class probabilities
from $M_{t}$. We use _Platt scaling_ [26, 24].

The process is initialized by selecting a seed set of size $s$ from the
unlabeled data pool, using a strategy $\mathcal{A}$ (line 2). We use random
selection for this step.

We also note that a “model” here might mean a combination of a text
representation, e.g., _word vectors_ , and a classifier, e.g., _Random Forest_
; further detailed in Section 4.

It might seem unusual that we explicitly mention model selection and
calibration, which should be part of the standard practice for building
probabilistic classifiers. Unfortunately, in our experience multiple
implementations/studies miss one or both of these steps.

##  4 Comparison Methodology

In our experiments, we vary _classifiers_ , _text representations_ (we often
jointly refer to them as a _prediction pipeline_), _batch size_ , _seed size_
and, of course, _query strategies_. These combinations are listed below:

  1. 1.

Prediction pipeline: There are two categories of pipelines we use:

    1. (a)

Separate representation and classifier: The representations used are _USE_
[3], _MPNet_ [31] and _word vectors_ (we use the models provided by the
_spaCy_ library [15]). While USE and MPNet directly convert sentences into
vectors, in the case of word vectors, we compute the average of the vectors of
all words in a text to obtain its representation. For classification, we use
_Random Forests (RF)_ [2] and _Support Vector Machines_ [6] with a _linear
kernel_ \- we’ll term the latter as “ _LinearSVC_ ”.

We use off-the-shelf representations and they are _not_ fine-tuned on our
data. Only the classifiers are trained on our data.

    2. (b)

End-to-end classifier: This does not require a separate representation model.
We use _RoBERTa_ [17] (a variant of _BERT_). This is fine-tuned on the labeled
data at each AL iteration.

Hyperparameter search spaces are detailed in Section 0.A.4.2 of the Appendix.
As noted in Section 3, model selection and calibration are performed during
training of a prediction pipeline. The only exception is _RoBERTa_ , which has
been shown to be well-calibrated out of the box [9].

The first category gives us $2\times 3=6$ combinations. Counting _RoBERTa_ ,
we have $\boldsymbol{7}$ prediction pipelines in our study.

  2. 2.

Query Strategy: we list these below, with the year of publication mentioned,
to show our focus on contemporary techniques:

    1. (a)

_Random_ : the batch is selected uniformly at random. This forms our baseline.

    2. (b)

_Margin_ 222Also referred to as _Smallest Margin_ or _Breaking Ties_. [27]
(2001): this selects instances with the smallest differences between the
confidence of the most likely and the second-most likely predicted (by the
current classifier333Note that in reference to Algorithm 1, at iteration $t$,
the query strategy $\mathcal{Q}$ uses model $M_{t-1}$.) classes. Despite being
a relatively old technique, it continues to be competitive [28].

    3. (c)

_Contrastive Active Learning (CAL)_ [21] (2021): chooses instances whose
predicted class-probability distribution is the most different (based on _KL
divergence_) from those of their $k$-nearest neighbors. This is similar to
another work [23], where such conflicts are detected using the _explanation
space_ produced by XAI techniques.

    4. (d)

_Discriminative Active Learning (DAL)_ [13, 11] (2019): a binary classifier (a
feedforward neural network) is constructed to discriminate between labeled and
unlabeled data, and then selects unlabeled instances with the greatest
predicted probability of being unlabeled. This picks examples that are most
different from the labeled instances in this classifier’s representation
space. While the original work [13] only considers image datasets, a separate
study shows its efficacy on text [11].

    5. (e)

_Representative Errors for Active Learning (REAL)_ [5] (2023): identifies
clusters in the unlabeled pool and assigns the majority predicted label as a
“pseudo-label” to all points in it. Instances are then sampled whose
predictions differ from the pseudo-label. The extent of disagreement and
cluster size are factored into the sampling step

We use a total of $\boldsymbol{5}$ query strategies.

  3. 3.

Datasets: we use $\boldsymbol{5}$ standard datasets: _agnews_ , _sst-2_ ,
_imdb_ , _pubmed_ and _dbpedia-5_ (a $5$-label version of the standard
_dbpedia_ dataset that we created). These are detailed in Table 2 in the
Appendix.

  4. 4.

Batch and Seed sizes: We use batch and seed size combinations of $(200,200)$
and $(500,500)$. This is a total of $\boldsymbol{2}$ combinations.

  5. 5.

Trials: For statistical significance, we run $\boldsymbol{3}$ trials for each
combination of the above settings.

Other settings: The accuracy metric we use is the F1 (macro) score, since it
prevents performance on a dominant class from overwhelming results. The size
of the unlabeled pool is $20000$ at the start of each experiment. If the
original dataset has more than than $20000$ instances, we extract a label-
stratified sample, to retain the original class distribution. The size of the
test set is $5000$ \- also a label-stratified sample from the corresponding
test set of the original dataset.

We run an experiment till the size of the labeled set has grown to $5000$
instances. This which implies $T=(5000-200)/200=24$ iterations for the
batch/seed size setting of $(200,200)$, and similarly $9$ iterations for the
$(500,500)$ setting.

Total # experiments444Our code is available here:
https://anonymous.4open.science/r/On_the_Fragility_of_Active_Learners/README.md.:
Accounting for the above settings, we have $7\times 5\times 5\times 2=350$
unique configurations. Accounting for the trials, we have a total of
$350\times 3=\boldsymbol{1050}$ experiments. Reiterating something we had
mentioned earlier: _we follow the due process of performing model selection
and calibration (excepting RoBERTa) in each AL iteration of each of these
experiments_.

##  5 Reproducibility of Benchmarked Techniques

Before we analyze our results, we would like to stress that our intention is
_not_ to suggest that the techniques we evaluate, e.g., REAL, CAL, DAL, don’t
work. In the specific settings discussed in their respective papers, they most
likely perform as reported. In the interest of fairness, we have conducted
limited independent tests that confirm this - see Section 0.A.3 in the
Appendix.

##  6 Results

We present our observations in this section. We begin with visualizing a
cross-section of our experiments: Figure 1 shows results for the dataset
_agnews_ and batch/seed size of $(200,200)$.

Figure 1: F1 macro scores on the test set at each iteration, for the dataset
_agnews_ and batch size of $200$. The $x$-axes show size of the labeled data,
the $y$-axes show the F1-macro scores on the test data. The corresponding plot
for batch size = $500$ is shown as Figure 8 in the Appendix.

We introduce some notation to aid in the interpretation of our results. We
think of the _F1-macro_ score to be provided by this function:

$f(g,\mathcal{Q},\mathcal{D},b,s,N)$ (1)

Here,

  * •

$g$ denotes a prediction pipeline.

  * •

$\mathcal{Q}\in\\{cal,dal,real,margin,random\\}$ is a query strategy.

  * •

$\mathcal{D}\in\\{imdb,agnews,dbpedia-5,pubmed,sst-2\\}$ is a query strategy.

  * •

$b\in\\{200,500\\}$ is the batch size.

  * •

$s\in\\{200,500\\}$ is the seed size.

  * •

$N$ is the size of the labeled data. Here $N\leq 5000$.

Each of $g,\mathcal{Q},\mathcal{D},b,s,N$ may be thought of as a _random
variable_ , which takes on specific values in our experiments, e.g.,
$g=\text{\emph{LinearSVC-MPNet}}$, with uniform probability. $f$ is non-
deterministic because different trials with the same settings produce slightly
different results.

We now try to answer some interesting questions based on our results. In most
cases, we will average over various factors, especially datasets, since most
AL techniques assume their query strategy may be used without any prior
knowledge.

###  6.1 In what data regimes do query strategies most differ?

We immediately note in Figure 1 that learning curves vary quite a bit based on
the prediction pipeline.

What broad trend(s) might we expect? _F1-macro_ scores from different query
strategies (for a given pipeline and dataset) should converge as we see more
data due to at least two reasons: (a) the concept space would be eventually
covered, (b) at later iterations, there is less of the unlabeled pool to
choose from. Indeed, Figure 2 confirms this. We first compute variances in
_F1-macro_ scores for different pipeline/dataset combinations555This step
comes first since the accuracies obtained by a _LinearSVC_ would be very
different from those by _RoBERTa_. In this case, the inner quantity is
conditioned over the dataset first, because we wanted to validate a specific
property. In subsequent analyses, we will average over datasets, so as to
mimic real-life use of AL, where no prior knowledge is assumed., and then plot
their averages. In other words, a point $(x,y)$ for the batch/seed size
$(200,200)$ curve denotes:

$y=\mathbb{E}_{g,\mathcal{D}}[Var[f|g=g^{\prime},\mathcal{D}=d^{\prime},N=x,b=200,s=200]]$
(2)

where $g^{\prime}$ and $d^{\prime}$ are a specific pipeline and dataset
respectively.

Figure 2: Expectation over variance of _F1-macro_ given a pipeline and
dataset, plotted size of labeled data. See Section 6.1 for details. Note that
the batch size doesn’t strongly affect trends.

###  6.2 Measuring effectiveness

A key reason to use AL is its effectiveness over random sampling. A common way
to assess this is to use the _Wilcoxon signed-rank test_ , e.g., [11], by
comparing accuracy scores from these strategies, at various labeled data
sizes. Unfortunately, this entirely ignores the _magnitude_ of the difference
in scores. This is a limitation of rank based metrics in general666Another
example is _Mean Rank_ over AUC values of the learning curves.. See Figure 3,
which shows learning curves for the _random_ strategy, and query strategies
$QS1$ and $QS2$. The latter two strategies have identical _p-values_ of
$9.77\times 10^{-4}$ for the Wilcoxon test (compared to random).

Figure 3: Hypothetical query strategies $QS1$ and $QS2$ shown against random.
Note that _p-value_ from the Wilcoxon test is identical for both. Discussed in
Section 6.2.

In practice, one would clearly prefer $QS2$ over $QS1$, since it reaches
higher accuracies earlier. In fact, considering the possibly non-zero cost of
setting up an AL-based tagging system, a query strategy needs to be
significantly better for it to be useful.

We recommend assessing the magnitude (relative to the _random_ strategy) using
_Root Mean Square Error (RMSE)_ or the _Area Under the (Learning) Curve
(AUC)_.

RMSE vs AUC: the choice between them comes down to these factors: (a) _RMSE_
doesn’t provide a direction of change (while _AUC_ does), which may be
addressed by pairing it with the Wilcoxon test, (b) _AUC_ monotonically
increases from left-to-right on the $x$-axis (unlike _RMSE_ which is a
_mean_), and so it must be carefully interpreted. Direct comparisons of _AUC_
are most convenient over identical spans of the $x$-axis.

We apply these metrics to our results to obtain Figure 4, where we show both
average _p-values_ from the Wilcoxon test (on the left) and average RMSE
scores (right subplot). Mathematically, for a given value on the $x$-axis, we
compare the _sequences_ :

$\displaystyle(\mathbb{E}_{g,\mathcal{D}}[f|\mathcal{Q}\in
S_{qs},N=n,b=200,s=200])_{n\leq x}\text{ and}$
$\displaystyle(\mathbb{E}_{g,\mathcal{D}}[f|\mathcal{Q}=random,N=n,b=200,s=200])_{n\leq
x}$ (3)

where $S_{qs}=\\{cal,dal,real,margin\\}$. Note that the $y$ values are
_cumulative_ , i.e., all sizes $n\leq x$ are considered. We prefer the _RMSE_
here to normalize for the $x$-axis span.

For the Wilcoxon test, we have set the minimal sample size at $3$ points,
which is why we see different starting points on the $x$-axes in Figure 4.
This test is also performed to assess if the _alternative_ , i.e., a non-
random strategy, produces higher values than the random strategy.

Figure 4: The left plot shows averaged _p-values_ from a Wilcoxon test, while
the right plot shows averaged _RMSE_ values. A consistently good query
strategy should have a low _p-value_ and high _RMSE_ ; none of the evaluate
strategies fall in that category. Discussed in Section 6.2.

An ideal query strategy should have a low _p-value_ and high _RMSE_.
Unfortunately, no query strategy fulfills this criteria: while _cal_ and _dal_
have high _RMSE_ values, they have poor _p-values_ (the _dal_ curve eclipses
_cal_ in the plot). And while _real_ and _margin_ have _p-values_ that improve
with labeled data, they exhibit small _RMSE_ scores. Some things of note:

  1. 1.

The fact the _p-value_ scores of _real_ and _margin_ improve with size, is
something we will encounter again (Figure 5).

  2. 2.

The _RMSE_ plot reinforces trends of the variance plot in Figure 2: we see
higher _RMSEs_ in the low data regime.

  3. 3.

The batch/seed settings preserve the general trend.

###  6.3 Gain over random and margin strategies

We now ask if we actually do better than random sampling. We define the
relative improvement $\delta$ between two scores as:

$\delta(treatment,control)=100\times\frac{(treatment-control)}{control}$ (4)

For a labeled dataset of size $(n_{1},n_{2}]$, batch/seed size
$(b^{\prime},s^{\prime})$ and
$q^{\prime}\in\\{cal,dal,real,margin\\}$, we compute:

$\mathbb{E}_{g,\mathcal{D}}[\delta((f|\mathcal{Q}=q^{\prime},b=b^{\prime},s=s^{\prime},n_{1}<N\leq
n_{2}]),\\\ (f|\mathcal{Q}=random,b=b^{\prime},s=s^{\prime},n_{1}<N\leq
n_{2}))]$ (5)

This is shown in Figure 5, where the labeled data size is broken up into
multiple bins to distinguish patterns at different size regimes. We also
separate the batch sizes (see legend). Given the negative scores, it seems
that in general, _random is either competitive or better_!

At relatively higher data sizes, _margin_ and _real_ start to surpass _random_
: which seems to suggest that (a) at low size regimes, where we expect the
greatest impact from AL, their performance is actually poor, and (b) after
gathering some data, these strategies are able to better exploit structure in
the data (and _margin_ seems surprisingly competitive in this regime). Also,
recall that we had seen this behaviour of _margin_ and _real_ in the _RMSE_
subplot of Figure 4.

Since behaviour across the two batch/seed size settings don’t seem to
appreciably differ (we note this in Figures 2, 4 and 5), we will average over
them in the next few plots.

Figure 5: Average relative improvement in _F1-macro_ score over random, for
different query strategies. Corresponds to Equation 5.

We can repeat the above exercise, to assess the effect of pipelines now, i.e.,
for a given data size bin $(n_{1},n_{2}]$ and prediction pipeline
$g^{\prime}$, we now compute:

$\mathbb{E}_{\mathcal{Q}\in
S_{qs},\mathcal{D},b,s}[\delta((f|g=g^{\prime},n_{1}<N\leq n_{2}]),\\\
(f|g=g^{\prime},\mathcal{Q}=random,n_{1}<N\leq n_{2}))]$ (6)

where $S_{qs}=\\{cal,dal,real,margin\\}$. This is plotted in Figure 6. Here we
note that, using _RoBERTa_ gives us a better average performance over _random_
at any size regime.

Figure 6: Average relative improvement in _F1-macro_ score over random, for
different pipelines. This corresponds to Equation 6.

We might want to know if for the promising case of _RoBERTa_ relatively new
techniques like _dal_ , _real_ and _cal_ outperform _margin_. This is easy to
plot with minor changes to the quantity in Equation 6:

$\mathbb{E}_{\mathcal{Q}\in
S_{qs},\mathcal{D},b,s}[\delta((f|g=RoBERTa,n_{1}<N\leq n_{2}]),\\\
(f|g=RoBERTa,\mathcal{Q}=margin,n_{1}<N\leq n_{2}))]$ (7)

where $S_{qs}=\\{cal,dal,real\\}$. The corresponding plot is shown in Figure
7. We see that aside from one data regime, $(1250-2500]$ _margin_ remains
quite competitive.

Figure 7: Average relative improvement in _F1-macro_ score over _margin_ for
_RoBERTa_. This corresponds to Equation 7.

###  6.4 The best combinations

Finally, we ask what are the best combinations of pipelines and query
strategies, at different size regimes? We measure this by the _AUC_ per
regime. Given a pipeline $g^{\prime}$, strategy $q^{\prime}$, and data sizes
$n_{i}$ within a bin, the _AUC_ 777Using _AUC_ is reasonable since the
$x$-axis is broken up into bins of roughly equal size (see discussion in
Section 6.2), and we are not looking for comparison to the _random_ strategy.
is computed for the following _sequence_ :

$(\mathbb{E}_{\mathcal{D},b,s}[f|g=g^{\prime},\mathcal{Q}=q^{\prime},N=n_{i}])_{n_{i}}$
(8)

Table 1 shows the top-$10$ combinations of pipelines and query strategies for
different regimes. Not surprisingly, wrt pipelines, _RoBERTa_ shows the
strongest performance. Somewhat surprisingly, the next best pipeline is
_LinearSVC-MPNet_ (shortened to _LinSVC_MPNet_) and not a _RF_ -based
pipeline. Our guess as to why this is the case is that _RF_ ’s
hyperparamṡearch space (detailed in Section 0.A.4.2) was not comprehensive
enough, while _MPNet_ transformed the data to be nearly linearly separable,
which enabled the high-bias _LinearSVC_ to quickly find a good optima. Sadly,
no single query strategy dominates the _QS_ column, and thus we are offered no
insight as to what strategy pairs best with a pipeline. Somewhat noteworthy is
the fact that the _random_ strategy is quite competitive for the _LinearSVC-
MPNet_ pipeline, but not for _RoBERTa_.

Table 1: The top-$10$ combinations of pipelines and query strategies are shown (in two columns) for different labeled data size regimes. We show the _AUC_ score for a combinations in size regime. See Section 6.4 for details. train size | pipeline | QS | AUC | pipeline | QS | AUC
---|---|---|---|---|---|---
(0-1250] | 1\. RoBERTa | dal | 875.46 | 6\. LinSVC_MPNet | random | 807.04
(0-1250] | 2\. RoBERTa | real | 873.64 | 7\. LinSVC_MPNet | real | 794.69
(0-1250] | 3\. RoBERTa | margin | 873.36 | 8\. LinSVC_MPNet | margin | 793.08
(0-1250] | 4\. RoBERTa | cal | 871.92 | 9\. LinSVC_MPNet | cal | 790.42
(0-1250] | 5\. RoBERTa | random | 862.99 | 10\. LinSVC_MPNet | dal | 789.60
(1250-2500] | 1\. RoBERTa | cal | 986.22 | 6\. LinSVC_MPNet | random | 913.76
(1250-2500] | 2\. RoBERTa | dal | 984.40 | 7\. LinSVC_MPNet | real | 907.98
(1250-2500] | 3\. RoBERTa | real | 981.07 | 8\. LinSVC_MPNet | margin | 907.39
(1250-2500] | 4\. RoBERTa | margin | 976.07 | 9\. LinSVC_MPNet | dal | 900.13
(1250-2500] | 5\. RoBERTa | random | 974.04 | 10\. LinSVC_MPNet | cal | 899.12
(2500-3750] | 1\. RoBERTa | margin | 903.60 | 6\. LinSVC_MPNet | random | 837.91
(2500-3750] | 2\. RoBERTa | dal | 900.93 | 7\. LinSVC_MPNet | margin | 836.57
(2500-3750] | 3\. RoBERTa | real | 900.83 | 8\. LinSVC_MPNet | real | 833.95
(2500-3750] | 4\. RoBERTa | cal | 897.16 | 9\. LinSVC_MPNet | dal | 828.73
(2500-3750] | 5\. RoBERTa | random | 891.58 | 10\. LinSVC_MPNet | cal | 827.24
(3750-5000] | 1\. RoBERTa | real | 1087.92 | 6\. LinSVC_MPNet | margin | 1016.94
(3750-5000] | 2\. RoBERTa | margin | 1087.37 | 7\. LinSVC_MPNet | random | 1010.88
(3750-5000] | 3\. RoBERTa | dal | 1085.06 | 8\. LinSVC_MPNet | real | 1008.67
(3750-5000] | 4\. RoBERTa | cal | 1076.79 | 9\. LinSVC_MPNet | dal | 1004.44
(3750-5000] | 5\. RoBERTa | random | 1075.20 | 10\. LinSVC_MPNet | cal | 999.97

##  7 Summary and Conclusion

We first summarize our observations:

  1. 1.

We noted in the dataset cross-section (Figure 1) of our experiments that the
behavior of query strategies vary widely wrt pipelines. However, we observe
the larger expected trend of reduction in the variance of accuracies produced
by different strategies, with increase in the size of labeled data (Figure 2
in Section 2).

  2. 2.

Wrt assessing the value of a query strategy, we noted that the Wilcoxon test
only provides a partial picture by ignoring magnitudes (Figure 3 in Section
6.2). We might use the _RMSE_ score to measure differences wrt the _random_
strategy. Applied to our results, it shows that no query strategy exhibits the
favorable properties of having both a low _p-value_ and high _RMSE_ score
(Figure 4 in Section 6.2).

  3. 3.

Our batch/seed size settings of $(200,200)$ and $(500,500)$ only seem to
influence slight change in behaviors. We noted this in Figure 2, Figure 4 and
Figure 5.

  4. 4.

Most query strategies exhibit no significant gain over the _random_ strategy
(Figure 5), although at relatively higher data regimes we noted _real_ and
_margin_ surpass _random_.

  5. 5.

Among pipelines, _RoBERTa_ exhibits the strongest performance (Figure 6)
relative to _random_ , but not wrt _margin_ (Figure 7).

  6. 6.

When we list the top-$10$ best performing combinations per data size regime
(Table 1), we note that _RoBERTa_ and _LinearSVC-MPNet_ consistently do well,
but unfortunately, their best performances are paired with different query
strategies. The only (broad) takeaways are that while _LinearSVC-MPNet_ works
well with the _random_ strategy, _RoBERTa_ performs well with non-random
strategies, but its not clear which specific one.

After extensive evaluation of different AL algorithms, we are forced to
conclude that AL doesn’t reliably work across datasets, prediction pipelines
and text representations. This study may be considered “limited” relative to
real-world variances, e.g., many more choices of classifiers, datasets, which
leads us to suspect that the true picture is probably more dismal. Of course,
we see some associations in isolated pockets, such as _RoBERTa_ consistently
performs well, that are promising, but not enough (with what query strategy?)
to derive a useful prescription. It’s known that query strategies require a
“warm-start” labeled set, and this is probably why we observe the deferred
performance of _real_ and _margin_ in Figure 5, but again, this does not
translate to practical advice unless we can precisely identify a settings-
specific warm-start size. It’d seem the only way to know if an AL technique
would work in a setting is to find results reported for similar settings, and
even this advice leaves open the question of inferring similarity between
datasets. And if one can’t find such results, the only other way to know is by
trying out multiple techniques - which of course is a chicken-and-egg problem
when data-labeling is expensive!

How do we encourage the field of AL to be more utility-driven? We believe
there are at least two ways: (a) embrace a broader discourse where the success
of a technique needs to be tied to fundamental properties of datasets (e.g.,
_topological_ features [4]) and predictors (e.g., _VC dimension_ [32]), that
are identifiable in an _unsupervised_ manner in novel settings, and (b) on the
empirical front, reported results need to account for an array of settings
much more diverse than is customary today.

## References

  * [1] Attenberg, J., Provost, F.: Inactive learning? difficulties employing active learning in practice. SIGKDD Explor. Newsl. 12(2), 36–41 (mar 2011)
  * [2] Breiman, L.: Random forests. Machine Learning 45(1), 5–32 (Oct 2001)
  * [3] Cer, D., Yang, Y., Kong, S.y., Hua, N., Limtiaco, N., St. John, R., Constant, N., Guajardo-Cespedes, M., Yuan, S., Tar, C., Strope, B., Kurzweil, R.: Universal sentence encoder for English. In: Blanco, E., Lu, W. (eds.) Proceedings of the 2018 Conference on Empirical Methods in Natural Language Processing: System Demonstrations. pp. 169–174 (Nov 2018)
  * [4] Chazal, F., Michel, B.: An introduction to topological data analysis: Fundamental and practical aspects for data scientists. vol. 4 (2021). https://doi.org/10.3389/frai.2021.667963, https://www.frontiersin.org/articles/10.3389/frai.2021.667963
  * [5] Chen, C., Wang, Y., Liao, L., Chen, Y., Du, X.: Real: A representative error-driven approach for active learning. In: Machine Learning and Knowledge Discovery in Databases: Research Track: European Conference, ECML PKDD 2023, Turin, Italy, September 18–22, 2023, Proceedings, Part I. p. 20–37 (2023)
  * [6] Cortes, C., Vapnik, V.: Support-vector networks. Machine Learning 20(3), 273–297 (Sep 1995)
  * [7] Dasgupta, S.: Two faces of active learning. Theoretical Computer Science 412(19), 1767–1781 (2011), algorithmic Learning Theory (ALT 2009)
  * [8] Dernoncourt, F., Lee, J.Y.: PubMed 200k RCT: a dataset for sequential sentence classification in medical abstracts. In: Kondrak, G., Watanabe, T. (eds.) Proceedings of the Eighth International Joint Conference on Natural Language Processing (Volume 2: Short Papers). pp. 308–313 (Nov 2017)
  * [9] Desai, S., Durrett, G.: Calibration of pre-trained transformers. In: Webber, B., Cohn, T., He, Y., Liu, Y. (eds.) Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP). pp. 295–302 (Nov 2020)
  * [10] Devlin, J., Chang, M.W., Lee, K., Toutanova, K.: BERT: Pre-training of deep bidirectional transformers for language understanding. In: Burstein, J., Doran, C., Solorio, T. (eds.) Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume 1 (Long and Short Papers). pp. 4171–4186 (Jun 2019)
  * [11] Ein-Dor, L., Halfon, A., Gera, A., Shnarch, E., Dankin, L., Choshen, L., Danilevsky, M., Aharonov, R., Katz, Y., Slonim, N.: Active Learning for BERT: An Empirical Study. In: Webber, B., Cohn, T., He, Y., Liu, Y. (eds.) Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP). pp. 7949–7962 (Nov 2020)
  * [12] Gal, Y., Islam, R., Ghahramani, Z.: Deep Bayesian active learning with image data. In: Precup, D., Teh, Y.W. (eds.) Proceedings of the 34th International Conference on Machine Learning. Proceedings of Machine Learning Research, vol. 70, pp. 1183–1192 (06–11 Aug 2017)
  * [13] Gissin, D., Shalev-Shwartz, S.: Discriminative active learning. CoRR abs/1907.06347 (2019), http://arxiv.org/abs/1907.06347
  * [14] Hewitt, J., Thickstun, J., Manning, C., Liang, P.: Backpack language models. In: Rogers, A., Boyd-Graber, J., Okazaki, N. (eds.) Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). pp. 9103–9125 (Jul 2023)
  * [15] Honnibal, M., Montani, I., Landeghem, S.V., Boyd, A.: "spacy: Industrial-strength natural language processing in python" (2020), https://spacy.io/
  * [16] Lewis, D.D., Gale, W.A.: A sequential algorithm for training text classifiers. In: Proceedings of the 17th Annual International ACM SIGIR Conference on Research and Development in Information Retrieval. pp. 3–12. SIGIR ’94 (1994)
  * [17] Liu, Y., Ott, M., Goyal, N., Du, J., Joshi, M., Chen, D., Levy, O., Lewis, M., Zettlemoyer, L., Stoyanov, V.: Roberta: A robustly optimized bert pretraining approach. arXiv preprint arXiv:1907.11692 (2019)
  * [18] Lüth, C.T., Bungert, T.J., Klein, L., Jaeger, P.F.: Navigating the pitfalls of active learning evaluation: A systematic framework for meaningful performance assessment. In: Thirty-seventh Conference on Neural Information Processing Systems (2023), https://openreview.net/forum?id=Dqn715Txgl
  * [19] Maas, A.L., Daly, R.E., Pham, P.T., Huang, D., Ng, A.Y., Potts, C.: Learning word vectors for sentiment analysis. In: Proceedings of the 49th Annual Meeting of the Association for Computational Linguistics: Human Language Technologies. pp. 142–150 (June 2011), http://www.aclweb.org/anthology/P11-1015
  * [20] Margatina, K., Aletras, N.: On the limitations of simulating active learning. In: Rogers, A., Boyd-Graber, J., Okazaki, N. (eds.) Findings of the Association for Computational Linguistics: ACL 2023. pp. 4402–4419 (Jul 2023)
  * [21] Margatina, K., Vernikos, G., Barrault, L., Aletras, N.: Active learning by acquiring contrastive examples. In: Moens, M.F., Huang, X., Specia, L., Yih, S.W.t. (eds.) Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing. pp. 650–663 (Nov 2021)
  * [22] Mikolov, T., Chen, K., Corrado, G., Dean, J.: Efficient estimation of word representations in vector space. In: "International Conference on Learning Representations", ICLR (2013)
  * [23] Nguyen, E.T., Ghose, A.: Are good explainers secretly human-in-the-loop active learners? In: "AI&HCI workshop at the 40th International Conference on Machine Learning", ICML (2023), https://arxiv.org/abs/2306.13935
  * [24] Niculescu-Mizil, A., Caruana, R.: Predicting good probabilities with supervised learning. In: Proceedings of the 22nd International Conference on Machine Learning. p. 625–632. ICML ’05 (2005)
  * [25] Pedregosa, F., Varoquaux, G., Gramfort, A., Michel, V., Thirion, B., Grisel, O., Blondel, M., Prettenhofer, P., Weiss, R., Dubourg, V., Vanderplas, J., Passos, A., Cournapeau, D., Brucher, M., Perrot, M., Duchesnay, E.: Scikit-learn: Machine learning in Python. Journal of Machine Learning Research 12, 2825–2830 (2011)
  * [26] Platt, J.: Probabilistic outputs for support vector machines and comparisons to regularized likelihood methods. Adv. Large Margin Classif. 10 (06 2000)
  * [27] Scheffer, T., Decomain, C., Wrobel, S.: Active hidden markov models for information extraction. In: Hoffmann, F., Hand, D.J., Adams, N., Fisher, D., Guimaraes, G. (eds.) Advances in Intelligent Data Analysis. pp. 309–318 (2001)
  * [28] Schröder, C., Niekler, A., Potthast, M.: Revisiting uncertainty-based query strategies for active learning with transformers. In: Findings of the Association for Computational Linguistics: ACL 2022. pp. 2194–2203 (May 2022)
  * [29] Settles, B.: Active learning literature survey. Computer Sciences Technical Report 1648, University of Wisconsin–Madison (2009)
  * [30] Socher, R., Perelygin, A., Wu, J., Chuang, J., Manning, C.D., Ng, A., Potts, C.: Recursive deep models for semantic compositionality over a sentiment treebank. In: Proceedings of the 2013 Conference on Empirical Methods in Natural Language Processing. pp. 1631–1642 (Oct 2013)
  * [31] Song, K., Tan, X., Qin, T., Lu, J., Liu, T.Y.: Mpnet: Masked and permuted pre-training for language understanding. In: Larochelle, H., Ranzato, M., Hadsell, R., Balcan, M., Lin, H. (eds.) Advances in Neural Information Processing Systems. vol. 33, pp. 16857–16867 (2020)
  * [32] Vapnik, V.N.: Constructing Learning Algorithms. Springer New York (1995). https://doi.org/10.1007/978-1-4757-2440-0_6
  * [33] Wang, W., Wei, F., Dong, L., Bao, H., Yang, N., Zhou, M.: MiniLM: Deep self-attention distillation for task-agnostic compression of pre-trained transformers. In: Proceedings of the 34th International Conference on Neural Information Processing Systems. NIPS’20 (2020)
  * [34] Wolf, T., Debut, L., Sanh, V., Chaumond, J., Delangue, C., Moi, A., Cistac, P., Rault, T., Louf, R., Funtowicz, M., Davison, J., Shleifer, S., von Platen, P., Ma, C., Jernite, Y., Plu, J., Xu, C., Le Scao, T., Gugger, S., Drame, M., Lhoest, Q., Rush, A.: Transformers: State-of-the-art natural language processing. In: Liu, Q., Schlangen, D. (eds.) Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing: System Demonstrations. pp. 38–45 (Oct 2020)
  * [35] Zhan, X., Liu, H., Li, Q., Chan, A.B.: A comparative survey: Benchmarking for pool-based active learning. In: Zhou, Z.H. (ed.) Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21. pp. 4679–4686 (8 2021), survey Track
  * [36] Zhang, X., Zhao, J., LeCun, Y.: Character-level convolutional networks for text classification. In: Cortes, C., Lawrence, N., Lee, D., Sugiyama, M., Garnett, R. (eds.) Advances in Neural Information Processing Systems. vol. 28 (2015)

##  Appendix 0.A Appendix

###  0.A.1 Datasets

As an addendum to the methodology discussion in Section 4, we provide details
of the datasets used in Table 2.

Table 2: Datasets used. Dataset |  # classes |  Description
---|---|---
sst-2 |  2 |  Single sentences extracted from movie reviews with their sentiment label [30].
imdb |  2 |  Movie reviews with corresponding sentiment label [19].
agnews |  4 |  News articles with their topic category [36].
pubmed |  4 |  Sentences in medical articles’ abstracts which are labeled with their role on the abstract [8].
dbpedia-5 |  5 |  A subset of _dbpedia_ [36] which contains Wikipedia articles accompanied by a topic label. The original dataset’s instances are evenly distributed across $14$ classes. To form _dbpedia-5_ , we use only the first $5$ classes: _Company, EducationalInstitution, Artist, Athlete, OfficeHolder_. This was done to reduce the training time of one-vs-all classifiers, e.g., _LinearSVC_.

###  0.A.2 Learning curves for _agnews_

This is the plot for the batch/seed size setting of $(500,500)$, for the
dataset _agnews_. This is a companion to the plot shown in Figure 1 of Section
6.

Figure 8: F1 macro scores on the test set at each iteration, for the dataset
_agnews_ and batch size of $500$. The $x$-axes show size of the labeled data,
the $y$-axes show the F1-macro scores on the test data.

###  0.A.3 Reproducibility Experiments

In all cases, we have attempted to replicate the original settings, e.g. same
train/development/test data split, model type, seed/batch sizes, number of AL
iterations as shown in Table 3. For CAL, REAL, we report the F1-macro scores
on _agnews_ , in which classes are evenly distributed, instead of the accuracy
provided in the original papers. For DAL, we use the dataset _cola_
888https://nyu-mll.github.io/CoLA/ and utilise the _Hugging Face_ library to
finetune BERT (while the original work employs _TensorFlow_
999https://www.tensorflow.org/, but we use equivalent settings). Figure 9
shows a comparison between our results and the reported ones in these papers.
Despite some minor differences in the setups, we observe that these AL methods
work as described in their respective papers in these settings.

One significant difference between these settings compared to our methodology
is the use of a predetermined _labeled_ development set for all BERT/RoBERTa
model finetuning. This set is relatively larger than the AL batch or seed size
and is not part the labeled data available at each AL iteration. This is
impractical in scenarios where AL is typically used: labeling is expensive.
Moreover, in some cases, there is no model selection performed, which we
remedy in our experiments (Section 3).

Figure 9: Comparison between published results and ours with the same settings for CAL, REAL, DAL. Table 3: Settings for reproducibility experiments. AL |  Dataset |  AL loop |  Classifier & text representation |  QS parameters |  Metric
---|---|---|---|---|---
CAL |  _agnews_ |  b=2280
s=1140
T = 7 |  BERT (bert-base-cased)
[CLS] at the last hidden layer
learning rate = 2e-5
train batch size = 16
# epochs = 3
sequence length = 128
warmup ratio = 0.1
# evaluations per epoch = 5 |  # neighbors=10 |  F1-macro
DAL |  _cola_ |  b=50
s=100
T = 5 |  BERT (bert-base-uncased)
[CLS] at the pooled layer
learning rate = 5e-5
train batch size = 50
# epochs = 5
sequence length = 50
warmup ratio = 0
# evaluations per epoch = 1 |  - |  Accuracy
REAL |  _agnews_ |  b=150
s=100
T = 8 |  RoBERTa (roberta-base)
[CLS] at the last hidden layer
learning rate = 2e-5
train batch size = 8
# epochs = 4
sequence length = 96
warmup ratio = 0.1
# evaluations per epoch = 4 |  # clusters=25 |  F1-macro

###  0.A.4 Hyperparameters

####  0.A.4.1 Query Strategy (QS) hyperparameters

For each QS’s hypeparameters, we use the values recommended by the authors in
corresponding papers. This means setting number of nearest neighbors in CAL to
10, number of clusters in DAL to 25, and keeping the same discriminative model
in REAL.

####  0.A.4.2 Hyperparameters search for prediction pipelines

Table 4 shows the search space for hyperparameters we use for each classifier.

Table 4: Hyperparameters for each classifier in the prediction pipelines. Classifier |  Hyperparameters
---|---
RoBERTa |  roberta-base
[CLS] at the last hidden layer
learning rate = {3e-5, 5e-5}
train batch size = 16
# epochs = {5, 10}
sequence length = 128
warmup ratio = 0.1
# evaluations per epoch = 5
LinearSVC |  C = {0.001, 0.01, 0.1, 1, 10, 100, 1000}
class weight = balanced
RF |  min samples leaf = {1, 5, 9}
# estimators = {5, 10, 20, 30, 40, 50}
max depth = {5, 10, 15, 20, 25, 30}
class weight = balanced
max features = sqrt


As we can see, in $M_{2}$ the cursor ^^ of the Buyer monitor has been moved
into the choice. Moreover. the process stack of Buyer is updated in order to
register the discarded branch of the choice (i.e., the branch involving label
quit). From $M_{2}$, Seller can consume the message on top of the queue (which
details the choice by $\mathtt{B}$), or the Buyer can revert its choice. In
the first case we have the following, using Rule (Bra):

$\displaystyle M_{2}{\color[rgb]{0,0,1}\,\twoheadrightarrow\,}$
$\displaystyle(\nu\,s)(\,\ell_{1}[\mathtt{S}]:\lbag\mathbf{0},s[\mathtt{S}]\triangleright\\{\mathbf{quit}:\mathbf{0}\\}\;{\color[rgb]{1,0,1}\textbf{;}}\;s[\mathtt{S}]?(addr).s[\mathtt{S}]!\langle
date\rangle.\mathbf{0}\rbag\;|\;$
$\displaystyle{s_{\mathtt{S}}\left\lfloor{\color[rgb]{0,0,0}\mathbb{T_{\text{1}}}[\mathtt{B}\&\\{\mathbf{ok}:\,{\color[rgb]{1,0,1}\text{{\textasciicircum\\!\\!\textasciicircum}}}\mathtt{B}?\langle\mathsf{addr}\rangle.\mathtt{B}!\langle\mathsf{date}\rangle.\mathsf{end}\,;\,\mathbf{quit}:\mathsf{end}\\}]}\cdot
x_{1}\cdot\sigma_{1}\right\rfloor^{\lozenge}}\;|\;$
$\displaystyle\ell_{2}[\mathtt{B}]:\lbag\mathbf{0},s[\mathtt{B}]\triangleleft\\{\mathbf{quit}:\mathbf{0}\\}\;{\color[rgb]{1,0,1}\textbf{;}}\;s[\mathtt{B}]?(addr).s[\mathtt{B}]!\langle
date\rangle.\mathbf{0}\rbag\;|\;$
$\displaystyle{s_{\mathtt{B}}\left\lfloor{\color[rgb]{0,0,0}\mathbb{S_{\text{1}}}[\mathtt{S}\oplus\\{\mathbf{ok}:\,{\color[rgb]{1,0,1}\text{{\textasciicircum\\!\\!\textasciicircum}}}\mathtt{S}!\langle\mathsf{addr}\rangle.\mathtt{S}?\langle\mathsf{date}\rangle.\mathsf{end}\,;\,\mathbf{quit}:\mathsf{end}\\}]}\cdot
x_{2}\cdot\sigma_{2}\right\rfloor^{\lozenge}}\;|\;$ $\displaystyle
s:(h_{1}\circ(\mathtt{B}\,,\,\mathtt{S}\,,\,\mathbf{ok})\,{\color[rgb]{1,0,1}\mathbf{\star}}\,\epsilon)\\!~{})=M_{3}$

In the second case, we can revert the labeled choice by using Rule (RollC)
from $M_{3}$ first, and then using Rules (RBra) and (RSel) in a decoupled
fashion.

##  Appendix B Omitted Proofs

###  B.1 Proof of Theorem 4.2

We repeat the statement in Page 4.2:

######  Theorem 4.2.

For any atomic reachable configuration $M$, we have that
$M\stackrel{{\scriptstyle\cdot}}{{\approx}}M$.

###### Proof.

First, notice that showing $\mathbb{C}[M]\approx\mathbb{C}[M]$ is similar to
show $M_{1}\approx M_{1}$ with $M_{1}=\mathbb{C}[M]$. This allows us to just
focus on the “hole” of the context. It is then sufficient to show that the
following relation is a bf weak bisimulation.

$\displaystyle\Re=\\{(M,N)\,|\,M{\color[rgb]{0,0,1}\,\twoheadrightarrow\,}^{*}N\text{
via Rules~{}{Out} or {Sel}}\wedge$ $\displaystyle
M{\color[rgb]{1,0,0}\,\rightsquigarrow\,}^{*}N\text{ via Rules~{}{ROut} or
{RSel}}\\}$

Clearly, $(M,M)\in\Re$. We consider the requirements in Def. 4.4.

Let us first consider barbs. Suppose that $M$ challenges $N$ with a barb, we
distinguish two cases: $N$ is stable or not. If $\mathtt{sb}(N)$ then $N$ has
the same barb. Otherwise, if $\lnot\mathtt{sb}(N)$, by Corollary 4.1 there
exists an $N_{1}$ such that $N\longrightarrow^{*}N_{1}$ and
$\mathtt{sb}(N_{1})$. Since $M\longrightarrow^{*}N$ we may derive
$M\longrightarrow^{*}N_{1}$ with both stable configurations. By applying
Theorem 4.1 on $M\longrightarrow^{*}N_{1}$ we infer
$M\rightarrowtail^{*}N_{1}$; then, by applying the Loop Lemma (Lemma 4.2) we
further infer $N_{1}\rightarrowtail^{*}M$. Using again Theorem 4.1 we infer
that $N_{1}\longrightarrow^{*}M$; since we have deduced that
$N\longrightarrow^{*}N^{\prime}\longrightarrow^{*}M$, we know that $N$ weakly
matches all the barbs of $M$, as desired. Suppose now that $N$ challenges $M$
with a barb. We proceed similarly as above: if $\mathtt{sb}(M)$ then $M$ has
the same barb; otherwise, if $\lnot\mathtt{sb}(M)$, since
$M\longrightarrow^{*}N$, by Corollary 4.1 we have that
$M\longrightarrow^{*}N\longrightarrow^{*}N_{1}$, with $\mathtt{sb}(N_{1})$.
Let us note that the reductions in $N\longrightarrow^{*}N_{1}$ do not add
barbs to $N_{1}$: they only finalize ongoing synchronizations; by definition
of barbs (Def. 4.3) parties involved in ongoing rollbacks do not contribute to
barbs. We can conclude by applying Theorem 4.1 and deriving
$M\rightarrowtail^{*}N_{1}$, which has the same barbs of $N$, as desired.

Let us now consider reductions. We will just focus on synchronizations due to
input/output and branching/selection reduction steps, since these are the
cases in which $\longrightarrow$ and $\rightarrowtail$ differ; indeed,
reductions due to Rules Spawn and Beta can be trivially matched. There are two
cases: $M{\color[rgb]{0,0,1}\Rrightarrow}M_{1}$ and
$M{\color[rgb]{1,0,0}\Lleftarrow}M_{1}$. In the first case, as we distinguish
two sub-cases: either $N$ has already started the synchronization or not. In
the first case, $N$ can conclude the step:
$N{\color[rgb]{0,0,1}\,\twoheadrightarrow\,}N^{\prime}$. Now we have that
$M{{\color[rgb]{0,0,1}\,\twoheadrightarrow^{*}\,}}N{\color[rgb]{0,0,1}\,\twoheadrightarrow\,}N^{\prime}$.
Thanks to Lemma 4.3 we can rearrange such a reduction sequence as follows:
$M{\color[rgb]{0,0,1}\,\twoheadrightarrow\,}{\color[rgb]{0,0,1}\,\twoheadrightarrow\,}M_{1}{{\color[rgb]{0,0,1}\,\twoheadrightarrow^{*}\,}}N^{\prime}$.
We then have that the pair $(M_{1},N^{\prime})\in\Re$, as desired. In the
second case, $N$ can match the step with 2 reductions:
$N{\color[rgb]{0,0,1}\,\twoheadrightarrow\,}{\color[rgb]{0,0,1}\,\twoheadrightarrow\,}N^{\prime}$.
Also in this case we can rearrange the reduction sequence so as to obtain
$M{\color[rgb]{0,0,1}\,\twoheadrightarrow\,}{\color[rgb]{0,0,1}\,\twoheadrightarrow\,}M_{1}{\color[rgb]{0,0,1}\,\twoheadrightarrow\,}^{*}N^{\prime}$,
with $(M_{1},N^{\prime})\in\Re$, as desired. The second case is when
$M{\color[rgb]{1,0,0}\Lleftarrow}M_{1}$ (i.e., the challenge is a backward
move) and is handled similarly.

We now consider challenges from $N$, focusing only on synchronizations, just
as before. If $N{\color[rgb]{0,0,1}\,\twoheadrightarrow\,}N^{\prime}$, we
distinguish two cases: whether the reduction finalizes ends an ongoing
input/output and branching/selection, or it opens a new one. In the second
case $M$ matches the move with an idle move, i.e., $(M,N^{\prime})\in\Re$. In
the other case we can rearrange the reduction
$M{{\color[rgb]{0,0,1}\,\twoheadrightarrow^{*}\,}}N{\color[rgb]{0,0,1}\,\twoheadrightarrow\,}N^{\prime}$
into a similar reduction sequence
$M\longrightarrow^{*}N_{1}{{\color[rgb]{0,0,1}\,\twoheadrightarrow^{*}\,}}N^{\prime}$
with $\mathtt{sb}(N_{1})$, and all reductions in
$N_{1}{\color[rgb]{0,0,1}\,\twoheadrightarrow^{*}\,}N^{\prime}$ just start new
synchronizations. Thanks to Theorem 4.1, $M$ can mimick the same reduction to
$N_{1}$, i.e., $M{\color[rgb]{0,0,1}\Rrightarrow}^{*}N_{1}$, and we have that
$(N_{1},N^{\prime})\in\Re$, as desired. The case in which
$N{\color[rgb]{1,0,0}\,\rightsquigarrow\,}N^{\prime}$ (i.e., the challenge is
a backward move) is similar. This concludes the proof. ∎

###  B.2 Appendix to § 4.3

##### Well-formed Process Implementations of a Local Type

The results in § 4.3 rely on _well-formedness_ of a process $P$ with respect
to a local type $T$. Figure 9 reports a very simple system for decreeing well-
formedness. It is inspired by the type system for processes defined in [4];
clearly, more sophisticated systems, such as variants of those in [19, 13],
can be considered. We rely on two judgments:

  * •

$\vdash V::U$ says that $V$ is a well-formed (i.e. valid) value of type $V$.

  * •

$\Gamma\vdash P::x:T$ says that $P$ implements a single session with local
type $T$ along variable $x$, relying on type assignments for name variables
and recursive variables declared in $\Gamma$.

We will write $P\bowtie_{\,x}T$ if and only iff $\emptyset\vdash P::x:T$. This
notion of well-formedness can be extended to relate configurations and local
types with history; see Figure 10.

###  B.3 Proof of Theorem 4.4

We write $\mathtt{\mathtt{pa}}(\mathsf{H})$ to denote the set of participants
in a global type with history $\mathsf{H}$. The following proposition details
the shape of configurations that are reachable from a configuration that
initially implements a global type with history. In particular, monitor tags
can be full ${\color[rgb]{1,0,0}\blacklozenge}$ or empty $\lozenge$, and so if
$M\bowtie\mathsf{H}$ then $M$ may not be stable:

######  Proposition B.1.

Let $M\bowtie\mathsf{H}$ with
$\mathtt{\mathtt{pa}}(\mathsf{H})=\\{\mathtt{p}_{1},\cdots,\mathtt{p}_{n}\\}$.
Then we have

$\displaystyle
M\equiv(\nu\,s,\widetilde{n})\Big{(}\,\prod_{i\in\\{1,\cdots,n\\}}\ell_{i}[\mathtt{p}_{i}]:\lbag\mathtt{C}_{i}\;{\color[rgb]{1,0,1}\textbf{;}}\;Q_{i}\rbag\;|\;$
$\displaystyle{s_{\mathtt{p}_{i}}\left\lfloor{\color[rgb]{0,0,0}{\mathbb{T}_{i}\left[{\color[rgb]{0,0,0}\,{\color[rgb]{1,0,1}\text{{\textasciicircum\\!\\!\textasciicircum}}}S_{i}}\right]}}\cdot\widetilde{x_{i}}\cdot\sigma_{i}\right\rfloor^{\spadesuit}}\;|\;s:(h_{1}^{i}\,{\color[rgb]{1,0,1}\mathbf{\star}}\,h_{2}^{i})\\!\Big{)}$

with
${\lbag\mathtt{C}_{i}\;{\color[rgb]{1,0,1}\textbf{;}}\;Q_{i}\rbag}\bowtie_{\,s[\mathtt{p}_{i}]}{\mathbb{T}_{i}\left[{\color[rgb]{0,0,0}\,{\color[rgb]{1,0,1}\text{{\textasciicircum\\!\\!\textasciicircum}}}S_{i}}\right]}$
(cf. Figure 10), for all $i\in\\{1,\\!\cdots\\!,n\\}$, for some stores
$\sigma_{1},\ldots,\sigma_{n}$, process stacks
$\mathtt{C}_{1},\ldots,\mathtt{C}_{n}$. type contexts
$\mathbb{T}_{1},\ldots,\mathbb{T}_{n}$, local types $S_{1},\ldots,S_{n}$,
variables $\widetilde{x_{1}},\ldots,\widetilde{x_{n}}$, and queues
$h_{1}^{1},h_{2}^{1},\ldots,h_{1}^{n},h_{2}^{n}$.

###### Proof.

Immediate from Definition 4.1 (reachable configuration), Definition 4.9
(“initially implements”), and the reduction semantics $\longrightarrow$. ∎

The following congruence allows us to (silently) modify the order of the
messages in the queue in a consistent way:

######  Definition B.1 (Equivalence on message queues).

We define the structural equivalence on queues, denoted $\equiv_{\mathsf{q}}$,
as follows:

$\displaystyle
h\circ(\mathtt{p}_{1}\,,\,\mathtt{q}_{1}\,,\,m_{1})\circ(\mathtt{p}_{2}\,,\,\mathtt{q}_{2}\,,\,m_{2})\circ
h^{\prime}\equiv_{\mathsf{q}}\qquad\qquad\qquad$
$\displaystyle\qquad\qquad\qquad
h\circ(\mathtt{p}_{2}\,,\,\mathtt{q}_{2}\,,\,m_{2})\circ(\mathtt{p}_{1}\,,\,\mathtt{q}_{1}\,,\,m_{1})\circ
h^{\prime}$

whenever
$\mathtt{p}_{1}\neq\mathtt{p}_{2}\land\mathtt{q}_{1}\neq\mathtt{q}_{2}$.
Equivalence $\equiv_{\mathsf{q}}$ extends to configurations as expected.

We may now have:

###### Proof of Theorem 4.4 (Sketch).

The proof of Part (a) proceeds by induction on the transitions
$\mathsf{H}{\color[rgb]{0,0,1}\,\hookrightarrow\,}\mathsf{H}^{\prime}$ and
$\mathsf{H}{\color[rgb]{1,0,0}\,\rightharpoonup\,}\mathsf{H}^{\prime}$, with a
case analysis on the last applied rule. For the forward case we have a one-to-
one correspondence; there are four possible transitions at the level of global
types: a transition derived using Rule (FVal1) is matched by $M$ using Rule
(Out); a transition derived using Rule (FVal2) is matched by $M$ using Rule
(In); a transition derived using Rule (FCho1) is matched by $M$ using Rule
(Sel); a transition derived using Rule (FCho2) is matched by $M$ using Rule
(Bra). The analysis for the backward case is similar, but before matching the
transition
$\mathsf{H}{\color[rgb]{1,0,0}\,\rightharpoonup\,}\mathsf{H}^{\prime}$, we may
require an additional reduction step from $M$, depending on the tag of the
corresponding monitor. We use Prop. B.1 to determine this tag. If the tag is
$\lozenge$, then a reduction (using Rule (RollS) or (RollC)) is required in
order to have a full tag $\blacklozenge$, as needed by all relevant backward
reduction rules ($j=2$). Otherwise, if the tag is already $\blacklozenge$ from
a previous reduction then no additional step is needed ($j=1$). Once the tag
is full, the transition is matched as follows: a transition derived using Rule
(BVal1) is matched by $M$ using Rule (ROut); a transition derived using Rule
(BVal2) is matched by $M$ using Rule (RIn); a transition derived using Rule
(BCho1) is matched by $M$ using Rule (RSel); a transition derived using Rule
(BCho2) is matched by $M$ using Rule (RBra).

The proof of Part (b) proceeds by induction on transitions
$M{\color[rgb]{0,0,1}\,\twoheadrightarrow\,}N$ and
$M{\color[rgb]{1,0,0}\,\rightsquigarrow\,}N$, with a case analysis on the last
applied rule, following similar lines. There are two main cases:

  1. (i)

There is exactly one reduction from $M$ involving the participants that appear
at the top-level in $\mathsf{H}$ and can evolve.

  2. (ii)

There are one or more reductions from $M$ to $N_{i}$ whose involved
participants cannot be found at the top-level in $\mathsf{H}$.

While in case (i) the proof follows the analysis for Part (a), in case (ii) we
use $\approx_{\mathtt{sw}}$ on $\mathsf{H}$ to obtain behavior-preserving
transformations $\mathsf{H}_{i}$ of $\mathsf{H}$ in which the participants
involved in the reductions ($M{\color[rgb]{0,0,1}\,\twoheadrightarrow\,}N_{i}$
or $M{\color[rgb]{1,0,0}\,\rightsquigarrow\,}N_{i}$) appear at the top-level.
Such transformations exist, because of assumption $M\bowtie\mathsf{H}$. This
way, reductions from $M$ can be matched by $\mathsf{H}$ up to swapping; after
all the independent communication actions have been performed and matched
(there are finitely many of them), one obtains $M^{\prime}$, $\mathsf{H}$ such
that $M^{\prime}\bowtie\mathsf{H}^{\prime\prime}$.

In both (i) and (ii), the analysis of a backwards reduction from $M$ relies on
Prop. B.1 to determine the relevant tag involved. If the tag in $M$ is
$\blacklozenge$ then a reduction
$M{\color[rgb]{1,0,0}\,\rightsquigarrow\,}N^{\prime}$ was derived using Rules
(ROut), (RIn), (RSel), or (RBra) and it is easy to show that it corresponds
directly to one transition from $\mathsf{H}$ ($j=0$). When the reduction is
derived using Rules (RollS) or (RollC) (because the corresponding tag in $M$
is $\lozenge$), there is no corresponding transition from $\mathsf{H}$ and an
extra reduction (using Rules (ROut), (RIn), (RSel), or (RBra), which become
enabled thanks to Rules (RollS) and (RollC)) is required to actually match the
transition ($j=1$). It is worth noticing that due to the simplicity of our
well-formed processes/configurations (and our focus on first-order global
types), reduction $M{\color[rgb]{0,0,1}\,\twoheadrightarrow\,}N$ does not
involve Rule (Spawn) (for well-formed processes are single-threaded) nor Rule
(Beta) (for ($V\,{w})$ is a well-formed value but not a well-formed process).
Similarly, $M{\color[rgb]{1,0,0}\,\rightsquigarrow\,}N$ does not involve Rules
(RSpawn) and (RBeta). ∎

$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
24.88441pt\vbox{\vbox{}\hbox{\hskip-24.8844pt\hbox{\hbox{$\displaystyle\displaystyle{\Gamma\vdash\mathbf{0}::x:\mathsf{end}}$}}}}}}$
$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
39.30626pt\vbox{\vbox{}\hbox{\hskip-39.30626pt\hbox{\hbox{$\displaystyle\displaystyle{\Gamma,X:T\vdash
X::x:T}$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
38.73907pt\vbox{\hbox{\hskip-38.73907pt\hbox{\hbox{$\displaystyle\displaystyle{\Gamma,X:T\vdash
P::x:T}$}}}\vbox{}}}\over\hbox{\hskip
34.69586pt\vbox{\vbox{}\hbox{\hskip-34.69585pt\hbox{\hbox{$\displaystyle\displaystyle{\Gamma\vdash\mu
X.P::x:T}$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
48.09126pt\vbox{\hbox{\hskip-48.09125pt\hbox{\hbox{$\displaystyle\displaystyle{\Gamma\vdash
P::x:T\quad\vdash V::U}$}}}\vbox{}}}\over\hbox{\hskip
51.44093pt\vbox{\vbox{}\hbox{\hskip-51.44093pt\hbox{\hbox{$\displaystyle\displaystyle{\Gamma\vdash
x!\langle V\rangle.{P}::x:\mathtt{p}!\langle U\rangle.T}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
37.33397pt\vbox{\hbox{\hskip-37.33397pt\hbox{\hbox{$\displaystyle\displaystyle{\Gamma,y:U\vdash
P::x:T}$}}}\vbox{}}}\over\hbox{\hskip
51.15587pt\vbox{\vbox{}\hbox{\hskip-51.15587pt\hbox{\hbox{$\displaystyle\displaystyle{\Gamma\vdash
x?(y).{P}::x:\mathtt{p}?(U).T}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
57.76588pt\vbox{\hbox{\hskip-57.76588pt\hbox{\hbox{$\displaystyle\displaystyle{\forall
i\in\\{1,\ldots,n\\}.(\Gamma\vdash
P_{i}::x:T_{i})}$}}}\vbox{}}}\over\hbox{\hskip
81.90681pt\vbox{\vbox{}\hbox{\hskip-81.9068pt\hbox{\hbox{$\displaystyle\displaystyle{\Gamma\vdash
x\triangleleft\\{l_{i}.P_{i}\\}_{i\in\\{1,\ldots,n\\}}::x:\mathtt{\mathtt{q}}\\!\oplus\\!\\{l_{i}:T_{i}\\}_{i\in\\{1,\ldots,n\\}}}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
57.76588pt\vbox{\hbox{\hskip-57.76588pt\hbox{\hbox{$\displaystyle\displaystyle{\forall
i\in\\{1,\ldots,n\\}.(\Gamma\vdash
P_{i}::x:T_{i})}$}}}\vbox{}}}\over\hbox{\hskip
82.2957pt\vbox{\vbox{}\hbox{\hskip-82.2957pt\hbox{\hbox{$\displaystyle\displaystyle{\Gamma\vdash
x\triangleright\\{l_{i}:P_{i}\\}_{i\in\\{1,\ldots,n\\}}::x:\mathtt{\mathtt{q}}\&\\{l_{i}:T_{i}\\}_{i\in\\{1,\ldots,n\\}}}$}}}}}}$
Figure 9: Well-formed processes with respect to a local type.
$\displaystyle\displaystyle{\hbox{\hskip
13.434pt\vbox{\hbox{\hskip-13.43399pt\hbox{\hbox{$\displaystyle\displaystyle{P\bowtie_{\,x}T}$}}}\vbox{}}}\over\hbox{\hskip
29.93402pt\vbox{\vbox{}\hbox{\hskip-29.93402pt\hbox{\hbox{$\displaystyle\displaystyle{\lbag\mathbf{0}\;{\color[rgb]{1,0,1}\textbf{;}}\;P\rbag\bowtie_{\,x}\,{\color[rgb]{1,0,1}\text{{\textasciicircum\\!\\!\textasciicircum}}}T}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
62.86087pt\vbox{\hbox{\hskip-62.86087pt\hbox{\hbox{$\displaystyle\displaystyle{\lbag\mathtt{C}\;{\color[rgb]{1,0,1}\textbf{;}}\;x!\langle
V\rangle.{P}\rbag\bowtie_{\,x}{\mathbb{T}\left[{\color[rgb]{0,0,0}\,{\color[rgb]{1,0,1}\text{{\textasciicircum\\!\\!\textasciicircum}}}\mathtt{\mathtt{q}}!\langle
U\rangle.S}\right]}}$}}}\vbox{}}}\over\hbox{\hskip
49.5251pt\vbox{\vbox{}\hbox{\hskip-49.52509pt\hbox{\hbox{$\displaystyle\displaystyle{\lbag\mathtt{C}\;{\color[rgb]{1,0,1}\textbf{;}}\;{P}\rbag\bowtie_{\,x}{\mathbb{T}\left[{\color[rgb]{0,0,0}\mathtt{\mathtt{q}}!\langle
U\rangle.\,{\color[rgb]{1,0,1}\text{{\textasciicircum\\!\\!\textasciicircum}}}S}\right]}}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
62.9647pt\vbox{\hbox{\hskip-62.9647pt\hbox{\hbox{$\displaystyle\displaystyle{\lbag\mathtt{C}\;{\color[rgb]{1,0,1}\textbf{;}}\;x?(y).{P}\rbag\bowtie_{\,x}{\mathbb{T}\left[{\color[rgb]{0,0,0}\,{\color[rgb]{1,0,1}\text{{\textasciicircum\\!\\!\textasciicircum}}}\mathtt{\mathtt{q}}?\langle
U\rangle.S}\right]}}$}}}\vbox{}}}\over\hbox{\hskip
50.4001pt\vbox{\vbox{}\hbox{\hskip-50.4001pt\hbox{\hbox{$\displaystyle\displaystyle{\lbag\mathtt{C}\;{\color[rgb]{1,0,1}\textbf{;}}\;{P}\rbag\bowtie_{\,x}{\mathbb{T}\left[{\color[rgb]{0,0,0}\mathtt{\mathtt{q}}?\langle
U\rangle.\,{\color[rgb]{1,0,1}\text{{\textasciicircum\\!\\!\textasciicircum}}}S}\right]}}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
99.06535pt\vbox{\hbox{\hskip-99.06535pt\hbox{\hbox{$\displaystyle\displaystyle{\lbag\mathtt{C}\;{\color[rgb]{1,0,1}\textbf{;}}\;x\triangleleft\\{l_{i}.P_{i}\\}_{i\in
I}\rbag\bowtie_{\,x}{\mathbb{T}\left[{\color[rgb]{0,0,0}\,{\color[rgb]{1,0,1}\text{{\textasciicircum\\!\\!\textasciicircum}}}\mathtt{\mathtt{q}}\\!\oplus\\!\\{l_{j}:S_{j}\\}_{j\in
J}}\right]}\quad w\in I,J}$}}}\vbox{}}}\over\hbox{\hskip
107.5069pt\vbox{\vbox{}\hbox{\hskip-107.5069pt\hbox{\hbox{$\displaystyle\displaystyle{\lbag\mathtt{C},x\triangleleft\\{l_{l}.P_{l}\\}_{l\in
I\setminus
w}\;{\color[rgb]{1,0,1}\textbf{;}}\;P_{w}\rbag\bowtie_{\,x}{\mathbb{T}\left[{\color[rgb]{0,0,0}\mathtt{\mathtt{q}}\\!\oplus\\!\\{l_{j}:S_{j}\,,\,l_{w}:\,{\color[rgb]{1,0,1}\text{{\textasciicircum\\!\\!\textasciicircum}}}S_{w}\\}_{j\in
J\setminus w}}\right]}}$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
98.95425pt\vbox{\hbox{\hskip-98.95424pt\hbox{\hbox{$\displaystyle\displaystyle{\lbag\mathtt{C}\;{\color[rgb]{1,0,1}\textbf{;}}\;x\triangleright\\{l_{i}.P_{i}\\}_{i\in
I}\rbag\bowtie_{\,x}{\mathbb{T}\left[{\color[rgb]{0,0,0}\,{\color[rgb]{1,0,1}\text{{\textasciicircum\\!\\!\textasciicircum}}}\mathtt{\mathtt{q}}\&\\{l_{j}:S_{j}\\}_{j\in
J}}\right]}\quad w\in I,J}$}}}\vbox{}}}\over\hbox{\hskip
107.3958pt\vbox{\vbox{}\hbox{\hskip-107.39578pt\hbox{\hbox{$\displaystyle\displaystyle{\lbag\mathtt{C},x\triangleright\\{l_{l}.P_{l}\\}_{l\in
I\setminus
w}\;{\color[rgb]{1,0,1}\textbf{;}}\;P_{w}\rbag\bowtie_{\,x}{\mathbb{T}\left[{\color[rgb]{0,0,0}\mathtt{\mathtt{q}}\&\\{l_{j}:S_{j}\,,\,l_{w}:\,{\color[rgb]{1,0,1}\text{{\textasciicircum\\!\\!\textasciicircum}}}S_{w}\\}_{j\in
J\setminus w}}\right]}}$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
71.46321pt\vbox{\hbox{\hskip-71.46321pt\hbox{\hbox{$\displaystyle\displaystyle{\lbag\mathtt{C}\;{\color[rgb]{1,0,1}\textbf{;}}\;{P}\rbag\bowtie_{\,x}{\mathbb{T}\left[{\color[rgb]{0,0,0}\mathtt{\mathtt{q}}!\langle
U\rangle.\,{\color[rgb]{1,0,1}\text{{\textasciicircum\\!\\!\textasciicircum}}}S}\right]}\quad\vdash
V::U}$}}}\vbox{}}}\over\hbox{\hskip
62.86087pt\vbox{\vbox{}\hbox{\hskip-62.86087pt\hbox{\hbox{$\displaystyle\displaystyle{\lbag\mathtt{C}\;{\color[rgb]{1,0,1}\textbf{;}}\;x!\langle
V\rangle.{P}\rbag\bowtie_{\,x}{\mathbb{T}\left[{\color[rgb]{0,0,0}\,{\color[rgb]{1,0,1}\text{{\textasciicircum\\!\\!\textasciicircum}}}\mathtt{\mathtt{q}}!\langle
U\rangle.S}\right]}}$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
81.36375pt\vbox{\hbox{\hskip-81.36374pt\hbox{\hbox{$\displaystyle\displaystyle{\lbag\mathtt{C}\;{\color[rgb]{1,0,1}\textbf{;}}\;{P}\rbag\bowtie_{\,x}{\mathbb{T}\left[{\color[rgb]{0,0,0}\mathtt{\mathtt{q}}?\langle
U\rangle.\,{\color[rgb]{1,0,1}\text{{\textasciicircum\\!\\!\textasciicircum}}}S}\right]}\quad
y:U\vdash P::S}$}}}\vbox{}}}\over\hbox{\hskip
62.9647pt\vbox{\vbox{}\hbox{\hskip-62.9647pt\hbox{\hbox{$\displaystyle\displaystyle{\lbag\mathtt{C}\;{\color[rgb]{1,0,1}\textbf{;}}\;x?(y).{P}\rbag\bowtie_{\,x}{\mathbb{T}\left[{\color[rgb]{0,0,0}\,{\color[rgb]{1,0,1}\text{{\textasciicircum\\!\\!\textasciicircum}}}\mathtt{\mathtt{q}}?\langle
U\rangle.S}\right]}}$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
99.84306pt\vbox{\hbox{\hskip-99.84306pt\hbox{\hbox{$\displaystyle\displaystyle{\lbag\mathtt{C},x\triangleleft\\{l_{l}.P_{l}\\}_{l\in
I}\;{\color[rgb]{1,0,1}\textbf{;}}\;P_{w}\rbag\bowtie_{\,x}{\mathbb{T}\left[{\color[rgb]{0,0,0}\mathtt{\mathtt{q}}\\!\oplus\\!\\{l_{j}:S_{j}\,,\,l_{w}:\,{\color[rgb]{1,0,1}\text{{\textasciicircum\\!\\!\textasciicircum}}}S_{w}\\}_{j\in
J}}\right]}}$}}}\vbox{}}}\over\hbox{\hskip
85.56711pt\vbox{\vbox{}\hbox{\hskip-85.56711pt\hbox{\hbox{$\displaystyle\displaystyle{\lbag\mathtt{C}\;{\color[rgb]{1,0,1}\textbf{;}}\;x\triangleleft\\{l_{i}.P_{i}\\}_{i\in
I\cup
w}\rbag\bowtie_{\,x}{\mathbb{T}\left[{\color[rgb]{0,0,0}\,{\color[rgb]{1,0,1}\text{{\textasciicircum\\!\\!\textasciicircum}}}\mathtt{\mathtt{q}}\\!\oplus\\!\\{l_{j}:S_{j}\\}_{j\in
J\cup w}}\right]}}$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
99.73196pt\vbox{\hbox{\hskip-99.73195pt\hbox{\hbox{$\displaystyle\displaystyle{\lbag\mathtt{C},x\triangleright\\{l_{l}.P_{l}\\}_{l\in
I}\;{\color[rgb]{1,0,1}\textbf{;}}\;P_{w}\rbag\bowtie_{\,x}{\mathbb{T}\left[{\color[rgb]{0,0,0}\mathtt{\mathtt{q}}\&\\{l_{j}:S_{j}\,,\,l_{w}:\,{\color[rgb]{1,0,1}\text{{\textasciicircum\\!\\!\textasciicircum}}}S_{w}\\}_{j\in
J}}\right]}}$}}}\vbox{}}}\over\hbox{\hskip
85.45601pt\vbox{\vbox{}\hbox{\hskip-85.456pt\hbox{\hbox{$\displaystyle\displaystyle{\lbag\mathtt{C}\;{\color[rgb]{1,0,1}\textbf{;}}\;x\triangleright\\{l_{i}.P_{i}\\}_{i\in
I\cup
w}\rbag\bowtie_{\,x}{\mathbb{T}\left[{\color[rgb]{0,0,0}\,{\color[rgb]{1,0,1}\text{{\textasciicircum\\!\\!\textasciicircum}}}\mathtt{\mathtt{q}}\&\\{l_{j}:S_{j}\\}_{j\in
J\cup w}}\right]}}$}}}}}}$ Figure 10: Well-formed configurations with respect
to a local type with history.