by first strengthening the domain of the first component before distributing
the product over the functions. This explains the remaining complication in
the actual condition of Figure 11.

##### Top Cases

Finally, the last case summarizes all combinations of $\top$ with itself and
with $\mathsf{Nat}$, where all values are trivially related.

##### Terms

Figure 11 also contains the definition of the logical relation for terms,
whose form is fairly standard for strongly normalising languages. The one
extension is that we also normalise the original-term indices and not just the
terms in the relation.

##  Appendix G Termination of Algorithmic Subtyping

RstartL AR-and
AR-arr AR-nat AL-and1, AL-and2, AL-arr, AL-mp AL-arr, AL-mp

Figure 12. Dependency graph of algorithmic subtyping

In this section, we prove that with the use of a loop detection mechanism, the
subtyping algorithm presented in Figure 9 of Section 5 terminates for any
input types, $\mathit{A}$ and $\mathit{B}$.

The proof is partly mechanized in Coq and partly written in LaTeX. The
mechanized part is presented here in the form of lemmas, while the written
part is contained in the text and the remarks of this section. A table at the
end of this section links the lemmas presented here with their mechanized
counterparts.

###  G.1. The proof

The subtyping algorithm uses a left and a right focusing mode. Figure 12 shows
the dependency graph of the two modes. (L) and (R) stand for left- and right-
focusing, respectively, and the gray edges of the graph are those that switch
between modes. The algorithm always starts with right-focusing, which
decomposes $\mathit{B}$ in
${\mathcal{L}}\mathrel{\vdash_{\text{R}}}{\mathit{A}}\prec:{\mathit{B}}$, and
eventually enters the left-focusing phase which works by decomposing
$\mathit{A}$. In left focusing mode, rules AL-arr and AL-mp recursively
continue in this mode, while at the same time triggering back the right-
focusing mode.

In an effort to detect potential diverging behavior, we can start by examining
a variation of the algorithm where the interdependencies of the focusing modes
are removed, as shown in the black-colored part of Figure 12, thus isolating
the two modes of the algorithm161616In this variation, the right-focusing
premises in the left-focusing rules AL-mp and AL-arr, and the left-focusing
premise of the right-focusing rule AR-nat are stripped away. This makes the
algorithm incomplete w.r.t. the declarative version, but this is not a concern
here.. Since both modes follow the structure of their corresponding focal
type, they are both terminating when considered in isolation. Adding back the
left-focusing dependency in rule AR-nat still retains termination, because
left-focusing (which still ignores the right-focusing calls) terminates. To
conclude, the only diverging loops that could possibly occur involve mutual
recursion between both focusing modes, through the rules AL-arr and AL-mp.

${[]}\mathrel{\vdash_{\text{R}}}{\mathit{A}}\prec:{\mathit{B}}$AR-andAR-natAL-
mpAR-natAL-arrAL-mpAL-arrAL-arr A sequence of right-focusing rules A sequence
of left-focusing rules Arrow-loop endpoint Mp-loop endpoint pt Backtracking
point Figure 13. Visualization of the $\hookrightarrow$ relation

Figure 13 offers a visual aid to closely examine the shape of these loops. It
shows part of an arbitrary computation tree of the algorithmic subtyping
process, including backtracking branches. The algorithm starts by applying a
number of right-focusing rules (represented by a dotted pink path) until it
reaches an AR-nat rule application. Now it continues in left-focusing mode
(represented by a dashed purple path), sometimes igniting a new right-focusing
branch through rules AL-arr and AL-mp, as shown in the rightmost left-focusing
path of Figure 13. In the computation tree, a path that has an initial part in
right-focusing mode, its remainder in left-focusing mode and ends on a AL-arr
or AL-mp application, represents what we call a _single loop_ of mutual
recursion between the two focusing modes. Informally, it is a computation path
of the form
${\color[rgb]{0.88,0.07,0.37}\definecolor[named]{pgfstrokecolor}{rgb}{0.88,0.07,0.37}\mathrel{\vdash_{\text{R}}}\,\to\cdots\to\,\mathrel{\vdash_{\text{R}}}\,\to}\,{\color[rgb]{0.47,0.32,0.66}\definecolor[named]{pgfstrokecolor}{rgb}{0.47,0.32,0.66}\mathrel{\vdash_{\text{L}}}\,\to\cdots\to\,\mathrel{\vdash_{\text{L}}}\,\to}\,{\color[rgb]{0.88,0.07,0.37}\definecolor[named]{pgfstrokecolor}{rgb}{0.88,0.07,0.37}\mathrel{\vdash_{\text{R}}}}$,
where the last node is the right-focusing premise of an AL-arr or an AL-mp
rule. If it ends with an AL-arr rule application, we call it an _arrow-loop_ ,
and otherwise an _mp-loop_. For instance, in Figure 13 all the paths that
start at the root and end on an outlined AL-arr or AL-mp rule are single
loops.

It is now clearer that every right-focusing judgment to be resolved, signifies
the start of a number (possibly zero) of sequences (possibly empty) of single
loops. Therefore, a single loop, itself ending in a right-focusing judgment to
be resolved, can be considered as the first loop in a number of sequences of
single loops of the same kind (arrow- or mp-loops). Our termination proof
examines the finiteness of the number of single loop sequences that the
algorithm might go though, as well as the finiteness of the size of each of
those sequences.

We will show that a) arrow-loops are not a source of non-termination, and b) a
loop-detection mechanism that tracks previously tried mp-loops makes the
algorithm terminating. For that, we define two relations, one for arrow-loops
and one for mp-loops, each capturing the ways in which left-focusing triggers
the right-focusing mode through an application of the AL-arr or the AL-mp
rule, respectively.

$A\in_{\scriptstyle\&}B$ Intersection membership

$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
15.33334pt\vbox{\vbox{}\hbox{\hskip-15.33333pt\hbox{\hbox{$\displaystyle\displaystyle
A\in_{\scriptstyle\&}A$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
16.52501pt\vbox{\hbox{\hskip-16.52501pt\hbox{\hbox{$\displaystyle\displaystyle
A\in_{\scriptstyle\&}\mathit{B_{{\mathrm{1}}}}$}}}\vbox{}}}\over\hbox{\hskip
27.02222pt\vbox{\vbox{}\hbox{\hskip-27.02222pt\hbox{\hbox{$\displaystyle\displaystyle
A\in_{\scriptstyle\&}\mathit{B_{{\mathrm{1}}}}\,\&\,\mathit{B_{{\mathrm{2}}}}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
16.52501pt\vbox{\hbox{\hskip-16.52501pt\hbox{\hbox{$\displaystyle\displaystyle
A\in_{\scriptstyle\&}\mathit{B_{{\mathrm{2}}}}$}}}\vbox{}}}\over\hbox{\hskip
27.02222pt\vbox{\vbox{}\hbox{\hskip-27.02222pt\hbox{\hbox{$\displaystyle\displaystyle
A\in_{\scriptstyle\&}\mathit{B_{{\mathrm{1}}}}\,\&\,\mathit{B_{{\mathrm{2}}}}$}}}}}}$

Figure 14. Definition of intersection membership

Their definition uses an auxiliary intersection-membership relation, written
as $\mathit{A}\in_{\scriptstyle\&}\mathit{B}$ and defined in Figure 14. The
formula $\mathit{A}\in_{\scriptstyle\&}\mathit{B}$ expresses that $\mathit{B}$
is the type $\mathit{A}$ possibly intersected with more types.

$\mathit{B}=(\ldots\&(\mathit{A}\&\ldots))\&\ldots$

We say that type $\mathit{A}$ is a component of type $\mathit{B}$.

The following results on intersection membership are useful for the rest of
the proof. The definition of the left-arrow depth function $||\cdot||$, here
referred to as our _norm_ , is given in Section 5.2 of the paper.

###### Lemma G.1 (Intersection membership decreases the norm).

If $\mathit{A}\in_{\scriptstyle\&}\mathit{B}$, then $||\mathit{A}||\leq||B||$.

###### Remark 1.

Every type has a finite number of components. Formally, for a given type
$\mathit{B}$, the set
$\\{\mathit{A}\mid\mathit{A}\in_{\scriptstyle\&}\mathit{B}\\}$ is finite. We
also say that, given type $\mathit{B}$, the intersection membership relation
produces a finite number of elements (that belong to that relation).

###  G.2. Arrow-loops are not a source of non-termination

$(\mathit{A}\prec:\mathit{B})\hookrightarrow(\mathit{B^{\prime}}\prec:\mathit{A^{\prime}})$
Single arrow-loops

LA-base $\displaystyle\displaystyle{\hbox{\hskip
22.36952pt\vbox{\hbox{\hskip-22.3695pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B_{{\mathrm{1}}}}\rightarrow\mathit{B_{{\mathrm{2}}}}\in_{\scriptstyle\&}\mathit{B}$}}}\vbox{}}}\over\hbox{\hskip
51.2945pt\vbox{\vbox{}\hbox{\hskip-51.2945pt\hbox{\hbox{$\displaystyle\displaystyle(\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}\prec:\mathit{B})\hookrightarrow(\mathit{B_{{\mathrm{1}}}}\prec:\mathit{A_{{\mathrm{1}}}})$}}}}}}$
LA-mp $\displaystyle\displaystyle{\hbox{\hskip
42.38448pt\vbox{\hbox{\hskip-42.38446pt\hbox{\hbox{$\displaystyle\displaystyle(\mathit{A_{{\mathrm{2}}}}\prec:\mathit{B})\hookrightarrow(\mathit{B^{\prime}}\prec:\mathit{A^{\prime}})$}}}\vbox{}}}\over\hbox{\hskip
50.03448pt\vbox{\vbox{}\hbox{\hskip-50.03448pt\hbox{\hbox{$\displaystyle\displaystyle(\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}\prec:\mathit{B})\hookrightarrow(\mathit{B^{\prime}}\prec:\mathit{A^{\prime}})$}}}}}}$
LA-arr $\displaystyle\displaystyle{\hbox{\hskip
76.154pt\vbox{\hbox{\hskip-76.15399pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B_{{\mathrm{1}}}}\rightarrow\mathit{B_{{\mathrm{2}}}}\in_{\scriptstyle\&}\mathit{B}\qquad(\mathit{A_{{\mathrm{2}}}}\prec:\mathit{B_{{\mathrm{2}}}})\hookrightarrow(\mathit{B^{\prime}}\prec:\mathit{A^{\prime}})$}}}\vbox{}}}\over\hbox{\hskip
50.03448pt\vbox{\vbox{}\hbox{\hskip-50.03448pt\hbox{\hbox{$\displaystyle\displaystyle(\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}\prec:\mathit{B})\hookrightarrow(\mathit{B^{\prime}}\prec:\mathit{A^{\prime}})$}}}}}}$
LA-andL $\displaystyle\displaystyle{\hbox{\hskip
42.38448pt\vbox{\hbox{\hskip-42.38446pt\hbox{\hbox{$\displaystyle\displaystyle(\mathit{A_{{\mathrm{1}}}}\prec:\mathit{B})\hookrightarrow(\mathit{B^{\prime}}\prec:\mathit{A^{\prime}})$}}}\vbox{}}}\over\hbox{\hskip
53.09001pt\vbox{\vbox{}\hbox{\hskip-53.09pt\hbox{\hbox{$\displaystyle\displaystyle(\mathit{A_{{\mathrm{1}}}}\,\&\,\mathit{A_{{\mathrm{2}}}}\prec:\mathit{B})\hookrightarrow(\mathit{B^{\prime}}\prec:\mathit{A^{\prime}})$}}}}}}$
LA-andR $\displaystyle\displaystyle{\hbox{\hskip
42.38448pt\vbox{\hbox{\hskip-42.38446pt\hbox{\hbox{$\displaystyle\displaystyle(\mathit{A_{{\mathrm{2}}}}\prec:\mathit{B})\hookrightarrow(\mathit{B^{\prime}}\prec:\mathit{A^{\prime}})$}}}\vbox{}}}\over\hbox{\hskip
53.09001pt\vbox{\vbox{}\hbox{\hskip-53.09pt\hbox{\hbox{$\displaystyle\displaystyle(\mathit{A_{{\mathrm{1}}}}\,\&\,\mathit{A_{{\mathrm{2}}}}\prec:\mathit{B})\hookrightarrow(\mathit{B^{\prime}}\prec:\mathit{A^{\prime}})$}}}}}}$

Figure 15. Single arrow-loops, formalized

The arrow-loop relation, $\hookrightarrow$, between right-focusing subtyping
judgments, shown in Figure 15, captures single cycles of mutual recursion
through an AL-arr rule application. Informally,
$(\mathit{A}\prec:\mathit{B})\hookrightarrow(\mathit{B^{\prime}}\prec:\mathit{A^{\prime}})$
expresses that resolving
${[]}\mathrel{\vdash_{\text{R}}}{\mathit{A}}\prec:{\mathit{B}}$, will trigger
resolving
${[]}\mathrel{\vdash_{\text{R}}}{\mathit{B^{\prime}}}\prec:{\mathit{A^{\prime}}}$
through a single arrow loop.

There are many ways in which AL-arr can be reached starting from the right-
focusing mode. The most immediate case is when resolving
${[]}\mathrel{\vdash_{\text{R}}}{\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}}\prec:{\mathit{B_{{\mathrm{1}}}}\rightarrow\mathit{B_{{\mathrm{2}}}}}$,
which triggers
${[]}\mathrel{\vdash_{\text{R}}}{\mathit{B_{{\mathrm{1}}}}}\prec:{\mathit{A_{{\mathrm{1}}}}}$.
We can generalize this to account for intersections of arrow types in the
right hand side of the initial subtyping judgment. Thus, trying to resolve
${[]}\mathrel{\vdash_{\text{R}}}{\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}}\prec:{\mathit{B}}$
will ignite a right-focusing call to resolve
${[]}\mathrel{\vdash_{\text{R}}}{\mathit{B_{{\mathrm{1}}}}}\prec:{\mathit{A_{{\mathrm{1}}}}}$,
for every arrow type component
$\mathit{B_{{\mathrm{1}}}}\rightarrow\mathit{B_{{\mathrm{2}}}}$ of
$\mathit{B}$ (LA-base). In addition, for every arrow type component
$\mathit{B_{{\mathrm{1}}}}\rightarrow\mathit{B_{{\mathrm{2}}}}\in_{\scriptstyle\&}\mathit{B}$,
if starting from
${[]}\mathrel{\vdash_{\text{R}}}{\mathit{A_{{\mathrm{2}}}}}\prec:{\mathit{B_{{\mathrm{2}}}}}$
triggers an arrow-loop on
${[]}\mathrel{\vdash_{\text{R}}}{\mathit{B^{\prime}}}\prec:{\mathit{A^{\prime}}}$,
then that loop is reached also starting from
${[]}\mathrel{\vdash_{\text{R}}}{\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}}\prec:{\mathit{B}}$.
These are arrow-loops that occur under the left-focusing subderivation of an
AL-arr rule (LA-arr). Similarly, rules LA-andL, LA-andR and LA-mp encode the
arrow-loops that occur under an application of AL-and1 or AL-and2 or the left-
focusing subderivation of AL-mp, respectively.

In Figure 13, $\hookrightarrow$ relates the right-focusing judgment at the
root of the tree with the right-focusing premise of every AL-arr application
that is outlined with green borders. The innermost AL-arr application is not
outlined because, starting from the root, it takes more than one (in
particular, it takes two) single mutual recursion cycles to reach it. Such
arrow-loops, nested in the right-focusing subderivation of a previously
applied AL-arr, are encoded in the transitive closure of $\hookrightarrow$.

###### Remark 2.

Given types $\mathit{A}$ and $\mathit{B}$, because of Remark 1, rule LA-base
produces a finite number of elements (possibly zero) in the
$\hookrightarrow$-relation. Since the rest of the rules in Figure 15 are
structurally decreasing on argument $\mathit{A}$, it follows that given types
$\mathit{A}$ and $\mathit{B}$, the set
$\\{(\mathit{B^{\prime}},\mathit{A^{\prime}})\mid(\mathit{A}\prec:\mathit{B})\hookrightarrow(\mathit{B^{\prime}}\prec:\mathit{A^{\prime}})\\})\\}$
is finite. Note that the left premise of rule LA-arr contributes by a finite
factor in the number of elements that this rule can produce.

###### Lemma G.2 (Arrow-loops strictly decrease the norm).

If
$(\mathit{A}\prec:\mathit{B})\hookrightarrow(\mathit{B^{\prime}}\prec:\mathit{A^{\prime}})$,
then
$||{[]}\mathrel{\vdash_{\text{R}}}{\mathit{A}}\prec:{\mathit{B}}||<||{[]}\mathrel{\vdash_{\text{R}}}{\mathit{B^{\prime}}}\prec:{\mathit{A^{\prime}}}||$.

It follows from the above remark and from Lemma G.2 that whenever the
algorithm is in right-focusing mode, it re-enters that mode through AL-arr a
finite number of times and with a right-focusing judgment that is strictly
smaller than the previous (w.r.t. our norm). This ensures that arrow-loops are
not a source of non-termination.

###  G.3. Loop detection for termination of MP-loops

$\mathit{B}\mathrel{\looparrowright^{\raisebox{2.0pt}{{$\scriptstyle\mathit{A}$}}}}\mathit{B^{\prime}}$
Single mp-loops

LM-base $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
18.73169pt\vbox{\vbox{}\hbox{\hskip-18.73169pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B}\mathrel{\looparrowright^{\raisebox{2.0pt}{{$\displaystyle\scriptstyle\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}$}}}}\mathit{A_{{\mathrm{1}}}}$}}}}}}$
LM-mp $\displaystyle\displaystyle{\hbox{\hskip
14.88336pt\vbox{\hbox{\hskip-14.88336pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B}\mathrel{\looparrowright^{\raisebox{2.0pt}{{$\displaystyle\scriptstyle\mathit{A_{{\mathrm{2}}}}$}}}}\mathit{B^{\prime}}$}}}\vbox{}}}\over\hbox{\hskip
17.89336pt\vbox{\vbox{}\hbox{\hskip-17.89336pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B}\mathrel{\looparrowright^{\raisebox{2.0pt}{{$\displaystyle\scriptstyle\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}$}}}}\mathit{B^{\prime}}$}}}}}}$
LM-arr $\displaystyle\displaystyle{\hbox{\hskip
48.6529pt\vbox{\hbox{\hskip-48.6529pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B_{{\mathrm{1}}}}\rightarrow\mathit{B_{{\mathrm{2}}}}\in_{\scriptstyle\&}\mathit{B}\qquad\mathit{B_{{\mathrm{2}}}}\mathrel{\looparrowright^{\raisebox{2.0pt}{{$\displaystyle\scriptstyle\mathit{A_{{\mathrm{2}}}}$}}}}\mathit{B^{\prime}}$}}}\vbox{}}}\over\hbox{\hskip
25.33505pt\vbox{\vbox{}\hbox{\hskip-25.33504pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B}\mathrel{\looparrowright^{\raisebox{2.0pt}{{$\displaystyle\scriptstyle\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}$}}}}\mathit{B_{{\mathrm{1}}}}\rightarrow\mathit{B^{\prime}}$}}}}}}$
LM-andL $\displaystyle\displaystyle{\hbox{\hskip
14.88336pt\vbox{\hbox{\hskip-14.88336pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B}\mathrel{\looparrowright^{\raisebox{2.0pt}{{$\displaystyle\scriptstyle\mathit{A_{{\mathrm{1}}}}$}}}}\mathit{B^{\prime}}$}}}\vbox{}}}\over\hbox{\hskip
21.35779pt\vbox{\vbox{}\hbox{\hskip-21.35777pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B}\mathrel{\looparrowright^{\raisebox{2.0pt}{{$\displaystyle\scriptstyle\mathit{A_{{\mathrm{1}}}}\,\&\,\mathit{A_{{\mathrm{2}}}}$}}}}\mathit{B^{\prime}}$}}}}}}$
LM-andR $\displaystyle\displaystyle{\hbox{\hskip
14.88336pt\vbox{\hbox{\hskip-14.88336pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B}\mathrel{\looparrowright^{\raisebox{2.0pt}{{$\displaystyle\scriptstyle\mathit{A_{{\mathrm{2}}}}$}}}}\mathit{B^{\prime}}$}}}\vbox{}}}\over\hbox{\hskip
21.35779pt\vbox{\vbox{}\hbox{\hskip-21.35777pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B}\mathrel{\looparrowright^{\raisebox{2.0pt}{{$\displaystyle\scriptstyle\mathit{A_{{\mathrm{1}}}}\,\&\,\mathit{A_{{\mathrm{2}}}}$}}}}\mathit{B^{\prime}}$}}}}}}$

Figure 16. Single mp-loops, formalized

Figure 16 shows the definition of the mp-loop family of relations, which,
similarly to the arrow-loop relation, encodes single cycles of mutual
recursion through AL-mp rule applications. Informally,
$\mathit{B}\mathrel{\looparrowright^{\raisebox{2.0pt}{{$\scriptstyle\mathit{A}$}}}}\mathit{B^{\prime}}$
expresses that resolving the judgment
${[]}\mathrel{\vdash_{\text{R}}}{\mathit{A}}\prec:{\mathit{B}}$, generates the
call ${[]}\mathrel{\vdash_{\text{R}}}{\mathit{A}}\prec:{\mathit{B^{\prime}}}$
through a single mp-loop.

A single right-focusing judgment may generate several mp-loops. The most
immediate case, encoded by rule LM-base, is when resolving
${[]}\mathrel{\vdash_{\text{R}}}{\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}}\prec:{\mathit{B}}$,
which triggers the resolution of
${[]}\mathrel{\vdash_{\text{R}}}{\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}}\prec:{\mathit{A_{{\mathrm{1}}}}}$.
Subsequent applications of the AL-mp rule that occur under the left-focusing
branch of a previous AL-mp rule application are encoded by rule LM-mp.
Similarly, rule LM-arr encodes applications of the AL-mp rule under the left-
focusing branch of a previously applied AL-arr rule. Lastly, rules LM-andL and
LM-andR encode mp-loops that occur under an application of AL-and1 and AL-
and2, respectively.

Note that for a type $\mathit{A}$,
$\mathrel{\looparrowright^{\raisebox{2.0pt}{{$\scriptstyle\mathit{A}$}}}}$ is
a set (not a multiset) and, thus, contains unique pairs of related right-
focusing judgments. Put differently, starting resolution on
${[]}\mathrel{\vdash_{\text{R}}}{\mathit{A}}\prec:{\mathit{B}}$, the judgment
does not distinguish between distinct applications of the AL-mp rule that
generate the same right-focusing call
${[]}\mathrel{\vdash_{\text{R}}}{\mathit{A}}\prec:{\mathit{B^{\prime}}}$. For
example, starting with
${[]}\mathrel{\vdash_{\text{R}}}{\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}}\prec:{\mathsf{Nat}\,\&\,\mathsf{Bool}\rightarrow\mathsf{Nat}}$,
the algorithm branches by rule AR-and and tries to apply the AL-mp rule within
both branches. Both applications generate the same right-focusing call,
${[]}\mathrel{\vdash_{\text{R}}}{\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}}\prec:{\mathit{A_{{\mathrm{1}}}}}$,
but are encoded as one mp-loop through rule LM-base. This justifies the use of
an arbitrary type $\mathit{B}$ in the left component of the relation
$\mathrel{\looparrowright^{\raisebox{2.0pt}{{$\scriptstyle\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}$}}}}$,
in the conclusion of the rules LM-base and LM-arr of Figure 16.

###### Remark 3.

The rules of the mp-loop relation family are structurally decreasing on the
index type $\mathit{A}$. Therefore, taking into consideration Remark 1 to
account for rule LM-arr, it follows that for given types $\mathit{A}$ and
$\mathit{B}$, the set
$\\{B^{\prime}\mid\mathit{B}\mathrel{\looparrowright^{\raisebox{2.0pt}{{$\scriptstyle\mathit{A}$}}}}\mathit{B^{\prime}}\\}$
is finite.

###### Lemma G.3 (Mp-loops non-strictly decrease the norm).

If
$\mathit{B}\mathrel{\looparrowright^{\raisebox{2.0pt}{{$\scriptstyle\mathit{A}$}}}}\mathit{B^{\prime}}$,
then
$||{[]}\mathrel{\vdash_{\text{R}}}{\mathit{A}}\prec:{\mathit{B}}||\leq||{[]}\mathrel{\vdash_{\text{R}}}{\mathit{A}}\prec:{\mathit{B^{\prime}}}||$.

Because a mp-loop signifies the start of a number of sequences of mp-loops to
follow, Remark 3 essentially means that when the algorithm is in right-
focusing mode it will generate a finite number of mp-loop sequences. However,
Lemma G.3 does not guarantee that the right-focusing judgment triggered by a
mp-loop is strictly smaller than the initial right-focusing judgment. As a
result, although the _number_ of mp-loop sequences is finite, not all
sequences are necessarily finite. Some of them might be infinite, with each
mp-loop triggering a right-focusing call on a judgment of equal norm.

In the following subsection, we show that the algorithm’s search space,
consisting of all possible recursive calls that the algorithm may trigger
given an initial subtyping judgment to resolve, is finite. As a direct result,
the algorithm has a finite number of possible mp-loops to follow. Then, by the
pigeon hole principle and the algorithm’s determinism, we can conclude that
for an mp-loop sequence to be infinite, it must contain an infinite repetition
of a finite number of finite mp-loop subsequences. Thus, a mechanism that
detects repetitions of mp-loops is sufficient to salvage the algorithm from
non-termination.

###  G.4. The search space is finite

To establish the finiteness of the algorithm’s search space, we only need to
consider the subspace generated by rule AL-mp, since it is the only rule that
threatens the algorithm’s termination. For that, we devise the _type
generator_ relation family, shown at the top of Figure 17, which uses two
auxiliary definitions, $\mathit{B}\underset{\scriptstyle
n}{\overset{\mathit{A}}{\bowtie}}\mathit{B^{\prime}}$ and
$\mathit{A}\underset{\scriptstyle n}{\bowtie}\mathit{B}$.

Although an understanding of the two auxiliary definitions is necessary to
understand what the type generator family relates, for the purposes of this
proof we only need to realize two properties it satisfies. First, the type
generator relation family is an over-approximation of all possible mp-loop
sequences, given an initial right-focusing subtyping judgment to resolve, and
second, we need a finiteness property similar to that in Remarks 1, 2 and 3.
The first property establishes that the type generator family contains an
encoding of the algorithm’s subspace that is generated by the Al-mp rule (or,
equivalently, by mp-loops). Then, the finiteness property allows us to
conclude that the algorithm’s subspace generated by mp-loops is finite.

$\mathit{B}\overset{\mathit{A}}{\bowtie}\mathit{B^{\prime}}$ Type generator
relation family

SB-main $\displaystyle\displaystyle{\hbox{\hskip
13.57085pt\vbox{\hbox{\hskip-13.57085pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B}\underset{\scriptstyle
0}{\overset{\mathit{A}}{\bowtie}}\mathit{B^{\prime}}$}}}\vbox{}}}\over\hbox{\hskip
15.35336pt\vbox{\vbox{}\hbox{\hskip-15.35336pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B}\overset{\mathit{A}}{\bowtie}\mathit{B^{\prime}}$}}}}}}$

$\mathit{B}\underset{\scriptstyle
n}{\overset{\mathit{A}}{\bowtie}}\mathit{B^{\prime}}$ Auxiliary type generator
relation family

SBx-done $\displaystyle\displaystyle{\hbox{\hskip
13.03969pt\vbox{\hbox{\hskip-13.03967pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A}\underset{\scriptstyle
n}{\bowtie}\mathit{A^{\prime}}$}}}\vbox{}}}\over\hbox{\hskip
14.0675pt\vbox{\vbox{}\hbox{\hskip-14.06749pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B}\underset{\scriptstyle
n}{\overset{\mathit{A}}{\bowtie}}\mathit{A^{\prime}}$}}}}}}$ SBx-more1
$\displaystyle\displaystyle{\hbox{\hskip
38.41693pt\vbox{\hbox{\hskip-38.41692pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A}\underset{\scriptstyle
n}{\bowtie}\mathit{A_{{\mathrm{1}}}}\qquad\mathit{B}\underset{\scriptstyle
n+1}{\overset{\mathit{A}}{\bowtie}}\mathit{A_{{\mathrm{2}}}}$}}}\vbox{}}}\over\hbox{\hskip
19.8925pt\vbox{\vbox{}\hbox{\hskip-19.8925pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B}\underset{\scriptstyle
n}{\overset{\mathit{A}}{\bowtie}}\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}$}}}}}}$
SBx-more2 $\displaystyle\displaystyle{\hbox{\hskip
37.91695pt\vbox{\hbox{\hskip-37.91693pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B}\underset{\scriptstyle
n}{\bowtie}\mathit{B_{{\mathrm{1}}}}\qquad\mathit{B}\underset{\scriptstyle
n+1}{\overset{\mathit{A}}{\bowtie}}\mathit{B_{{\mathrm{2}}}}$}}}\vbox{}}}\over\hbox{\hskip
19.60085pt\vbox{\vbox{}\hbox{\hskip-19.60085pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B}\underset{\scriptstyle
n}{\overset{\mathit{A}}{\bowtie}}\mathit{B_{{\mathrm{1}}}}\rightarrow\mathit{B_{{\mathrm{2}}}}$}}}}}}$

$\mathit{A}\underset{\scriptstyle n}{\bowtie}\mathit{B}$ Look-up relation
family

LU-here $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
22.18889pt\vbox{\vbox{}\hbox{\hskip-22.18887pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}\underset{\scriptstyle
0}{\bowtie}\mathit{A_{{\mathrm{1}}}}$}}}}}}$ LU-there
$\displaystyle\displaystyle{\hbox{\hskip
13.74387pt\vbox{\hbox{\hskip-13.74385pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A_{{\mathrm{2}}}}\underset{\scriptstyle
n}{\bowtie}\mathit{B}$}}}\vbox{}}}\over\hbox{\hskip
29.2341pt\vbox{\vbox{}\hbox{\hskip-29.2341pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}\underset{\scriptstyle
n+1}{\bowtie}\mathit{A_{{\mathrm{1}}}}$}}}}}}$ LU-skip
$\displaystyle\displaystyle{\hbox{\hskip
13.74387pt\vbox{\hbox{\hskip-13.74385pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A_{{\mathrm{2}}}}\underset{\scriptstyle
n}{\bowtie}\mathit{B}$}}}\vbox{}}}\over\hbox{\hskip
21.39388pt\vbox{\vbox{}\hbox{\hskip-21.39388pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}\underset{\scriptstyle
n}{\bowtie}\mathit{B}$}}}}}}$ LU-down $\displaystyle\displaystyle{\hbox{\hskip
13.74387pt\vbox{\hbox{\hskip-13.74385pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A_{{\mathrm{1}}}}\underset{\scriptstyle
n}{\bowtie}\mathit{B}$}}}\vbox{}}}\over\hbox{\hskip
21.39388pt\vbox{\vbox{}\hbox{\hskip-21.39388pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}\underset{\scriptstyle
n}{\bowtie}\mathit{B}$}}}}}}$ LU-left $\displaystyle\displaystyle{\hbox{\hskip
13.74387pt\vbox{\hbox{\hskip-13.74385pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A_{{\mathrm{1}}}}\underset{\scriptstyle
n}{\bowtie}\mathit{B}$}}}\vbox{}}}\over\hbox{\hskip
24.4494pt\vbox{\vbox{}\hbox{\hskip-24.44939pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A_{{\mathrm{1}}}}\,\&\,\mathit{A_{{\mathrm{2}}}}\underset{\scriptstyle
n}{\bowtie}\mathit{B}$}}}}}}$ LU-right
$\displaystyle\displaystyle{\hbox{\hskip
13.74387pt\vbox{\hbox{\hskip-13.74385pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A_{{\mathrm{2}}}}\underset{\scriptstyle
n}{\bowtie}\mathit{B}$}}}\vbox{}}}\over\hbox{\hskip
24.4494pt\vbox{\vbox{}\hbox{\hskip-24.44939pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A_{{\mathrm{1}}}}\,\&\,\mathit{A_{{\mathrm{2}}}}\underset{\scriptstyle
n}{\bowtie}\mathit{B}$}}}}}}$

Figure 17. An over-approximation of mp-loop sequences

####  G.4.1. An over-approximation of mp-loop sequences

Before we proceed, we formalize the notion of a sequence of mp-loops.
Naturally, sequences of mp-loops are modeled by the transitive closure of the
mp-loops relation family, as shown in Figure 18. A member
$\mathit{B}\,\looparrowright\looparrowright^{\raisebox{2.0pt}{{$\scriptstyle\mathit{A}$}}}\mathit{B^{\prime\prime}}$
of the
$\,\looparrowright\looparrowright^{\raisebox{2.0pt}{{$\scriptstyle\mathit{A}$}}}$-relation
models a sequence of mp-loops that starts with a
${[]}\mathrel{\vdash_{\text{R}}}{\mathit{A}}\prec:{\mathit{B}}$ and ends with
a
${[]}\mathrel{\vdash_{\text{R}}}{\mathit{A}}\prec:{\mathit{B^{\prime\prime}}}$
right-focusing judgment, after possibly going through intermediate mp-loops of
the form
${[]}\mathrel{\vdash_{\text{R}}}{\mathit{A}}\prec:{\mathit{B^{\prime}}}$.

$\mathit{B}\,\looparrowright\looparrowright^{\raisebox{2.0pt}{{$\scriptstyle\mathit{A}$}}}\mathit{B^{\prime}}$
Sequences of mp-loops

LMT-base $\displaystyle\displaystyle{\hbox{\hskip
14.32336pt\vbox{\hbox{\hskip-14.32336pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B}\mathrel{\looparrowright^{\raisebox{2.0pt}{{$\displaystyle\scriptstyle\mathit{A}$}}}}\mathit{B^{\prime}}$}}}\vbox{}}}\over\hbox{\hskip
21.54555pt\vbox{\vbox{}\hbox{\hskip-21.54553pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B}\,\looparrowright\looparrowright^{\raisebox{2.0pt}{{$\displaystyle\scriptstyle\mathit{A}$}}}\mathit{B^{\prime}}$}}}}}}$
LMT-cons $\displaystyle\displaystyle{\hbox{\hskip
48.52893pt\vbox{\hbox{\hskip-48.52893pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B}\mathrel{\looparrowright^{\raisebox{2.0pt}{{$\displaystyle\scriptstyle\mathit{A}$}}}}\mathit{B_{{\mathrm{1}}}}\qquad\mathit{B_{{\mathrm{1}}}}\,\looparrowright\looparrowright^{\raisebox{2.0pt}{{$\displaystyle\scriptstyle\mathit{A}$}}}\mathit{B_{{\mathrm{2}}}}$}}}\vbox{}}}\over\hbox{\hskip
22.17555pt\vbox{\vbox{}\hbox{\hskip-22.17554pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B}\,\looparrowright\looparrowright^{\raisebox{2.0pt}{{$\displaystyle\scriptstyle\mathit{A}$}}}\mathit{B_{{\mathrm{2}}}}$}}}}}}$

Figure 18. Sequences of mp-loops, formalized

Lemma G.4 justifies that the type generator family is an over-approximation of
all possible mp-loop sequences.

###### Lemma G.4.

If
$\mathit{B}\,\looparrowright\looparrowright^{\raisebox{2.0pt}{{$\scriptstyle\mathit{A}$}}}\mathit{B^{\prime}}$,
then $\mathit{B}\overset{\mathit{A}}{\bowtie}\mathit{B^{\prime}}$.

####  G.4.2. A finiteness property for the over-approximation

First, we examine the look-up relation family, on which the definition of the
type generator family depends.

###### Remark 4.

Consider a member $\mathit{A}\underset{\scriptstyle
n}{\bowtie}\mathit{A^{\prime}}$ of the look-up relation family. The inductive
rules of this definition are decreasing on the lexicographic order of the pair
$(n,\mathit{A})$. Therefore, given a natural number $n$ and a type
$\mathit{A}$, the set
$\\{\mathit{A^{\prime}}\mid\mathit{A}\underset{\scriptstyle
n}{\bowtie}\mathit{A^{\prime}}\\}$ is finite.

Next, we examine the auxiliary type generator family. Consider an element
$\mathit{B}\underset{\scriptstyle
n}{\overset{\mathit{A}}{\bowtie}}\mathit{B^{\prime}}$. From Remark 4, it
follows that given $n$, $A$ and $B$, rule SBx-done produces a finite number of
elements in the auxiliary type generator family. Similarly, given $n$, $A$ and
$B$, the left premise of the two remaining rules contributes by a finite
factor on the number of elements that each of those rules can produce. In
particular, the $\mathit{A_{{\mathrm{1}}}}$ and $\mathit{B_{{\mathrm{1}}}}$
types in the conclusion of rules SBx-more1 and SBx-more2, respectively, are
produced by the look-up relation family (on the left premise of the
corresponding rule) and thus they can only be finite in number. Yet, we are
left with the possibility to choose arrow types of unconstrained size for the
$\mathit{A_{{\mathrm{2}}}}$’s and $\mathit{B_{{\mathrm{2}}}}$’s of those two
rules. At first sight, we can have countably infinite choices for the right
hand side component of this family relation.

$\displaystyle\llparenthesis\mathsf{Nat}\rrparenthesis$
$\displaystyle=\llparenthesis\mathsf{top}\rrparenthesis=0$
$\displaystyle\llparenthesis\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}\rrparenthesis$
$\displaystyle=\max(\llparenthesis\mathit{A_{{\mathrm{1}}}}\rrparenthesis,\llparenthesis\mathit{A_{{\mathrm{2}}}}\rrparenthesis+1)$
$\displaystyle\llparenthesis\mathit{A_{{\mathrm{1}}}}\,\&\,\mathit{A_{{\mathrm{2}}}}\rrparenthesis$
$\displaystyle=\max(\llparenthesis\mathit{A_{{\mathrm{1}}}}\rrparenthesis,\llparenthesis\mathit{A_{{\mathrm{2}}}}\rrparenthesis)$
Figure 19. The range of a type

$\displaystyle\displaystyle{\hbox{\hskip
60.93344pt\vbox{\hbox{\hskip-60.93343pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A}\underset{\scriptstyle
n}{\bowtie}\mathit{A_{{\mathrm{1}}}}\qquad\raise
8.99443pt\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
39.27707pt\vbox{\hbox{\hskip-39.27705pt\hbox{\hbox{$\displaystyle\displaystyle{\mathit{A}\underset{\scriptstyle
n+1}{\bowtie}\mathit{A_{{\mathrm{2}}}}}\qquad\raise
14.22636pt\hbox{$\displaystyle{\hbox{$\displaystyle\vbox{\hbox{\hskip
16.9815pt\vbox{\vbox{}\hbox{\hskip-16.9815pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B}\underset{\scriptstyle
n+k}{\overset{\mathit{A}}{\bowtie}}B_{k+1}^{\prime}$}}}}}}$}}\hbox{}\atop\vbox
to28.45274pt{\leaders\hbox{$\displaystyle\cdot$} \vfil}$
}$}}}\vbox{}}}\over\hbox{\hskip
26.17845pt\vbox{\vbox{}\hbox{\hskip-26.17845pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B}\underset{\scriptstyle
n+1}{\overset{\mathit{A}}{\bowtie}}\mathit{B^{\prime}_{{\mathrm{2}}}}\to\cdots\to
B_{k+1}^{\prime}$}}}}}}$}}\hbox{}$ }$}}}\vbox{}}}\over\hbox{\hskip
30.70334pt\vbox{\vbox{}\hbox{\hskip-30.70332pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B}\underset{\scriptstyle
n}{\overset{\mathit{A}}{\bowtie}}\mathit{B^{\prime}_{{\mathrm{1}}}}\to\cdots\to
B_{k+1}^{\prime}$}}}}}}$
Figure 20. Example derivation

Fortunately, the following lemma limits the size of the arrow types that can
be chosen. It expresses that given a natural number index $n$ and types
$\mathit{A}$ and $\mathit{B}$, if $n$ is greater than the range of both types,
then there is no type $\mathit{B^{\prime}}$ such that
$\mathit{B}\underset{\scriptstyle
n}{\overset{\mathit{A}}{\bowtie}}\mathit{B^{\prime}}$. The range
$\llparenthesis\mathit{A}\rrparenthesis$ of a type $\mathit{A}$, defined in
Figure 20 is a function in the role of a norm for types.

###### Lemma G.5.

If
$max(\llparenthesis\mathit{A}\rrparenthesis,\llparenthesis\mathit{B}\rrparenthesis)<n$,
then $\mathit{B}\underset{\scriptstyle
n}{\overset{\mathit{A}}{\bowtie}}\mathit{B^{\prime}}$ does not hold for any
type $\mathit{B^{\prime}}$.

This lemma does not directly limit the choices for $\mathit{B^{\prime}}$ to a
finite number, because it does not impose any constraint on the
$\mathit{B^{\prime}}$ component of the auxiliary type generator family.
Rather, it constrains $n$ to be necessarily less than or equal to the range of
at least one of the two given types.

However, specializing $\mathit{B^{\prime}}$ to be an arrow type, since we are
interested in applications of rules SBx-more1 and SBx-more2, note that these
two rules increase the natural number index of the auxiliary type generator
relation in their right premise. As exemplified by the derivation in Figure
20, the size of the arrow type $\mathit{B^{\prime}}$ is limited so that if its
derivation contains a branch with $k$ applications of those two rules, then
$n+k\leq\max(\llparenthesis\mathit{A}\rrparenthesis,\llparenthesis\mathit{B}\rrparenthesis)$.

With this, we can conclude that given $n$, $A$ and $B$, rules SBx-more1 and
SBx-more2 generate a finite number of elements in the auxiliary type generator
relation. Altogether, given $n$, $\mathit{A}$ and $\mathit{B}$, the set
$\\{B^{\prime}\mid\mathit{B}\underset{\scriptstyle
n}{\overset{\mathit{A}}{\bowtie}}\mathit{B^{\prime}}\\}$ is finite.

Finally, the finiteness result about the type generator family, or to say,
about the over-approximation of the algorithm’s possible mp-loop sequences,
follows directly: given types $\mathit{A}$ and $\mathit{B}$, the set
$\\{B^{\prime}\mid\mathit{B}\overset{\mathit{A}}{\bowtie}\mathit{B^{\prime}}\\}$
is finite. ∎


11institutetext: Computer Aided Medical Procedures (CAMP), Technical
University of Munich, Munich, DE-85748, Germany 22institutetext: Research in
Orthopedic Computer Science (ROCS), University Hospital Balgrist, University
of Zurich, Zurich, CH-8008, Switzerland 33institutetext: Balgrist University
Hospital, Zurich, CH-8008, Switzerland
equally contributing last authors

# Conditional Generative Data Augmentation for Clinical Audio Datasets

Matthias Seibold 1122 Armando Hoch 33 Mazda Farshad 33 *Nassir Navab 11
*Philipp Fürnstahl 2233

###### Abstract

In this work, we propose a novel data augmentation method for clinical audio
datasets based on a conditional Wasserstein Generative Adversarial Network
with Gradient Penalty (cWGAN-GP), operating on log-mel spectrograms. To
validate our method, we created a clinical audio dataset which was recorded in
a real-world operating room during Total Hip Arthroplasty (THA) procedures and
contains typical sounds which resemble the different phases of the
intervention. We demonstrate the capability of the proposed method to generate
realistic class-conditioned samples from the dataset distribution and show
that training with the generated augmented samples outperforms classical audio
augmentation methods in terms of classification performance. The performance
was evaluated using a ResNet-18 classifier which shows a mean Macro F1-score
improvement of $1.70\%$ in a 5-fold cross validation experiment using the
proposed augmentation method. Because clinical data is often expensive to
acquire, the development of realistic and high-quality data augmentation
methods is crucial to improve the robustness and generalization capabilities
of learning-based algorithms which is especially important for safety-critical
medical applications. Therefore, the proposed data augmentation method is an
important step towards improving the data bottleneck for clinical audio-based
machine learning systems.

###### Keywords:

Deep Learning Data Augmentation Acoustic Sensing Total Hip Arthroplasty
Generative Adversarial Networks

##  1 Introduction

Acoustic signals are easy and low-cost to acquire, can be captured using air-
borne or contact microphones and show great potentials in medical applications
for interventional guidance and support systems. Successful applications are
intra-operative tissue characterization during needle insertion [9] and tissue
coagulation [16], the identification of the insertion endpoint in THA
procedures [3, 20], error prevention in surgical drilling during orthopedic
procedures [21] or guidance in orthopedic arthroscopy procedures [23].

Furthermore, acoustic signals have successfully been employed for diagnostic
medical applications. Exemplary applications include the assessment of
cartilage degeneration by measuring structure borne noise in the human knee
during movement [11], the development of a prototype for the detection of
implant loosening through an acoustic sensor system [2], a system for
monitoring the acoustic emissions of THA implants [19], or the automated
analysis of lung sounds captured with a digital stethoscope which allows non-
specialists to screen for pulmonary fibrosis [14].

Through recent advances in machine learning research, learning-based methods
have replaced and outperformed classical acoustic signal processing-based
approaches, as well as classical handcrafted feature-based learning approaches
for many acoustic audio signal processing tasks [18]. However, state-of-the-
art deep learning methods require large amounts of training data to achieve
superior performance and generalize well to unseen data, which are often
difficult or infeasible to acquire in a clinical setting. To tackle this
issue, the usage of augmentation techniques is a standard approach to increase
the diversity and size of training datasets. Hereby, new samples can be
synthesized by applying transformations to the existing data, e.g. rotation
and cropping for images, replacing words with synonyms for text, and applying
noise, pitch shifting, and time stretching to audio samples [28]. Even though
these data augmentation methods improve the performance of target
applications, they do not necessarily generate realistic samples which is
especially crucial in the medical domain where reliability is a key factor.
One solution to this problem is for example to exploit the underlying physics
for augmentation, e.g. for ultrasound image augmentation [26] which is,
however, not applicable for clinical audio data. In the presented work, we
will focus on realistic data augmentation of audio datasets for medical
applications.

Recently, deep generative models, a family of deep learning models, which are
able to synthesize realistic samples from a learned distribution, have been
applied for data augmentation of various data modalities outside of the
medical domain. For the augmentation of audio data, different generative
approaches have been introduced, of which related work to the proposed method
is described in the following section. Hu et al. utilized a GAN to synthesize
samples of logarithmic Mel-filter bank coefficients (FBANK) from a learned
distribution of a speech dataset and subsequently generated soft labels using
a pretrained classifier [8]. Madhu et al. trained separate GANs on mel-
spectrograms for each class of a dataset to generate augmentation data [12].
Chatziagapi et al. used the Balancing GAN (BAGAN) framework [13] to augment an
imbalanced speech dataset [1]. A conditional GAN was employed for data
augmentation of speech using FBANK features by Sheng et al. [22] and for
respiratory audio signals based on raw waveform augmentation by Jayalakshmy et
al. [10].

In this work, we introduce a novel augmentation technique for audio data based
on a conditional Wasserstein GAN model with Gradient Penalty (cWGAN-GP) which
produces higher-quality samples and is easier to train than standard GANs [5].
The proposed model operates on log-mel spectrograms which have been shown to
outperform other feature representations and achieves state-of-the-art
performance in audio classification tasks [18]. The proposed model is able to
generate realistic and high-quality log-mel spectrograms from the learned
dataset distribution. We show that our model can be used for two augmentation
strategies, doubling the number of samples and balancing the dataset. While
classical audio augmentation techniques might improve the performance of the
classifier, they do not generate samples that can be captured in a real
environment and might therefore be inconsistent with the real variability of
captured real-world acoustic signals. In contrast, the proposed model is able
to generate realistic samples from the learned distribution of the original
data.

To evaluate the proposed framework on realistic clinical data, we introduce a
novel audio dataset containing sounds of surgical actions recorded from five
real THA procedures which resemble the different phases of the intervention.
We thoroughly evaluate the proposed method on the proposed dataset in terms of
classification performance improvement of a ResNet-18 classifier with and
without data augmentation using 5-fold cross validation and compare the
results with classical audio augmentation techniques.

##  2 Materials and Method

###  2.1 Novel Surgical Audio Dataset

Figure 1: The classes of the novel clinical dataset resemble the phases of a
THA procedure. Occurrences with drawn through lines indicate intensive usage
of the respective surgical action, dashed lines correspond to sporadic usage.

Figure 1 illustrates the occurrence of the six classes $C:=$ {Suction,
Coagulation, Sawing, Reaming, Insertion, Adjustment} present in the dataset
over the course of a THA procedure. Please note that ”Insertion Cup” and
”Broaching and Insertion Femoral Stem” were joined into a single class
(”Insertion”) because of the similar acoustic signature generated by hammering
onto the metal structure of the insertion tools for the acetabular cup,
femoral broach and femoral stem implant, respectively. The ”Adjustment” class
also contains hammering signals that are, however, performed with a
screwdriver-like tool which is used to adjust the orientation of the
acetabular cup and generates a slightly different sound. During opening the
access to the area of operation in the beginning of the procedure, suction and
coagulation is employed intensively, whereas in the rest of the procedure both
surgical actions are performed sporadically and on demand (indicated through
dashed outlines in Figure 1). All samples were manually cut from recordings of
five THA interventions conducted at our university hospital for which we
captured audio with a framerate of $44.1\text{\,}\mathrm{kHz}$ using a air-
borne shotgun microphone (Røde NTG2) pointed towards the area of operation and
video captured from the OR light camera (Trumpf TruVidia). The captured video
was used to facilitate the labelling process. We labelled the dataset in a way
that audio samples do not contain overlapping classes and no staff
conversations. An ethical approval has been obtained prior to recording the
data in the operating room. The resulting dataset contains 568 recordings with
a length of $1\text{\,}\mathrm{s}31\text{\,}\mathrm{s}$ and the following
distribution: $n_{raw,Adjustment}=68$, $n_{raw,Coagulation}=117$,
$n_{raw,Insertion}=76$, $n_{raw,Reaming}=64$, $n_{raw,Sawing}=21$, and
$n_{raw,Suction}=222$. The dataset can be accessed under
https://rocs.balgrist.ch/en/open-access/.

###  2.2 Data Preprocessing and Baseline Augmentations

Log-mel spectrograms are a two-dimensional representation of an audio signal,
mapping frequency components of a signal to the ordinate and time to the
abscissa. They offer a dense representation of the signal, reduce the
dimensionality of the samples, and have been shown to yield superior
classification performance for a wide variety of acoustic sensing tasks [18].
We compute log-mel spectrograms of size $64\times 64$ from the dataset samples
by applying a sliding window technique with non-overlapping windows of length
$L=16380$ samples, a Short Time Fourier Transform (STFT) hop length of $H=256$
samples and $n_{mels}=64$ mel bins using the Python library librosa 0.8.1
[15]. We compute a total number of 3597 individual spectrograms from the raw
waveform dataset. The resulting number of spectrograms per-class is:
$n_{spec,Adjustment}=494$, $n_{spec,Coagulation}=608$,
$n_{spec,Insertion}=967$, $n_{spec,Reaming}=469$, $n_{spec,Sawing}=160$, and
$n_{spec,Suction}=899$. For the evaluation using 5-fold cross validation, we
randomly split the dataset into five folds on the raw waveform level over all
recordings, as the recording conditions are identical.

To compare the proposed augmentation method against classical signal
processing augmentation approaches, we implemented the following augmentation
strategies which are applied to the raw waveforms directly. We apply Gaussian
noise with $\mu=0$ and $\sigma=0.01$. We apply Pitch Shifting by 3 semitones
upwards. We apply time stretching with a factor of 1.5. Furthermore, we
compare our method with SpecAugment, a widely used approach for audio
augmentation in Automatic Speech Recognition (ASR) tasks which applies random
time-warping, frequency- and time-masking to the spectrograms directly [17].
For a fair comparison of all augmentations, we add 100% generated samples for
each augmentation strategy, respectively. We normalize the data by computing
$X_{norm,mel}={(X_{mel}-\mu)}/{\sigma}$, where ($\mu$) is the mean and
($\sigma$) is the standard deviation of the entire dataset.

###  2.3 Conditional Generative Data Augmentation Method

The architectural details of the proposed GAN are illustrated in Figure 2. To
stabilize the training process and improve the generated sample quality, we
apply the Wasserstein loss with Gradient Penalty (GP) as introduced by
Gulrajani et al. [5] which enforces a constraint such that the gradients of
the discriminator’s (critic) output w.r.t the inputs have unit norm. This
approach greatly improves the stability of the training and compensates for
problems such as mode collapse. We define the critic’s loss function as:

$L_{C}=\mathbb{E}_{\tilde{x}\sim\mathbb{P}_{g}}[D(\tilde{x},y)]-\mathbb{E}_{x\sim\mathbb{P}_{r}}[D(x,y)]+\lambda\;\mathbb{E}_{\hat{x}\sim\mathbb{P}_{\hat{x}}}[\|\Delta_{\hat{x}}D(\hat{x},y)\|_{2}-1)^{2}]$
(1)

where $\mathbb{P}_{r}$ is the real distribution, $\mathbb{P}_{g}$ is the
generated distribution, and $\mathbb{P}_{\hat{x}}$ is the interpolated
distribution. The interpolated samples $\hat{x}$ are uniformly sampled along a
straight line between real $x$ and generated $\tilde{x}$ samples by computing:

$\hat{x}=\epsilon x+(1-\epsilon)\tilde{x}$ (2)

We use the recommended GP weight of $\lambda=10$, a batch size of 64 and train
the discriminator five times for each generator iteration. In order to choose
the stopping point for training, we frequently compute the Fréchet Inception
Distance (FID) [7] which is calculated from features of a pretrained
classifier by:

$FID=\|\mu_{r}-\mu_{g}\|^{2}+\operatorname{Tr}(C_{r}+C_{g}-2*\sqrt{C_{r}*C_{g}})$
(3)

as a measure of the quality for the generated samples and stop the training at
epoch 580. Hereby, $\mu_{r}$ and $\mu_{g}$ represent the feature-wise mean of
the real and generated spectrograms, $C_{r}$ and $C_{g}$ the respective
covariance matrices. Because of the structural differences of images and
spectrograms, we cannot use an Inception v3 network pretrained on ImageNet to
compute the FID. Therefore, we employ a ResNet-18 [6] model pretrained on the
proposed dataset, extract the features from the last convolutional layer, and
use these features for FID calculation. The proposed model is implemented with
TensorFlow/Keras 2.6 and trained using the Adam optimizer ($LR=1e-4$,
$\beta_{1}=0.5$, $\beta_{2}=0.9$) in $\sim$6 hours on a NVidia RTX 2080 SUPER
GPU.

Figure 2: The architecture of the proposed model including output sizes of
each layer. The input for the generator is a noise vector of size 1x128 and a
class condition. The generator outputs a spectrogram which is fed to the
discriminator together with the class condition. The discriminator (critic)
outputs a scalar realness score.

A nonlinear activation function is omitted in the last convolutional layer of
the generator because the spectrogram samples are not normalized in the range
$[0,1]$. The mapping layer of the generator employs a dense layer, whereas in
the discriminator (critic) we use repeat and reshaping operations for
remapping. The generator and discriminator have a total number of 1,526,084
and 4,321,153 parameters, respectively. The implementation, pretrained models,
and dataset can be accessed under: https://rocs.balgrist.ch/en/open-access/.

###  2.4 Classification Model

To evaluate the augmentation performance of our model against classical audio
augmentation techniques, we analyze the effect of augmentation on the
classification performance in a 5-fold cross validation experiment using a
ResNet-18 [6] classifier, an architecture which has been successfully employed
for clinical audio classification tasks [20, 21]. We train the classifier from
scratch for 20 epochs using categorical crossentropy loss, the Adam optimizer
($LR=1e-4$, $\beta_{1}=0.9$, $\beta_{2}=0.999$) and a batch size of 32.

##  3 Results and Evaluation

In Figure 3, we show a comparison of randomly chosen ground truth and randomly
generated samples. The visual quality of the generated samples is comparable
to the original data and the model seems to be able to generate samples
conditioned on the queried class. By further visual inspection it can be
observed that the synthesized samples contain the characteristics of the
original dataset, e.g. the hammer strokes are clearly visible for the classes
”Adjustment” and ”Insertion”.

Figure 3: The top row shows log-mel spectrograms of random samples for each
class present in the acquired dataset, the bottom row shows log-mel
spectrograms generated by the proposed model for each class, respectively.

The quantitative evaluation of the classification performance using a
ResNet-18 classifier is given in Table 1. We report the mean Macro F1-Score in
the format $mean\pm std$. . We compare training without augmentations and
classical audio augmentation techniques (adding noise, pitch shifting, time
stretching, and SpecAugment [17]) with the proposed method. The cWGAN-GP-based
augmentations outperform all classical augmentation strategies when doubling
the samples ($+1.70\%$) and show similar performance ($+1.07\%$) as the best
performing classical augmentation strategy (Time Stretch) when balancing the
dataset.

Augmentation Technique |  Mean Macro
F1-Score |  Relative Improvement
---|---|---
No Augmentation |  $93.90\pm 2.48\%$ |
Add Noise |  $92.87\pm 0.99\%$ |  $-1.03\%$
Pitch Shift |  $94.73\pm 1.28\%$ |  $+0.83\%$
Time Stretch |  $95.00\pm 1.49\%$ |  $+1.10\%$
SpecAugment [17] |  $94.23\pm 1.14\%$ |  $+0.33\%$
cWGAN-GP (balanced) |  $94.97\pm 1.71\%$ |  $+1.07\%$
cWGAN-GP (doubled) |  $\mathbf{95.60\pm 1.26\%}$ |  $\mathbf{+1.70\%}$
Table 1: Results of the proposed model in comparison to classical audio
augmentation techniques.

##  4 Discussion

The proposed augmentation method is an important step towards improving the
data limitations by generating synthetic in-distribution augmentation data for
clinical applications for which it is often expensive or even impossible to
gather large amounts of training data. We showed that our augmentation
strategy outperforms classical signal processing approaches and has the
capability to balance imbalanced datasets to a certain extent. To balance
imbalanced datasets, any arbitrary number of samples can easily be generated
for each class with the proposed approach which is not possible using
classical signal processing techniques in the same way. However, for the given
dataset and configuration, doubling the number of samples using the proposed
augmentation method leads to the best final classification results.
Furthermore, we show that the proposed method outperforms SpecAugment [17], an
established audio augmentation method which applies time-warping, as well as
frequency and time masking to the spectrogram data directly.

In future work, we want to benchmark the proposed framework with other
generative augmentation models and model architectures, investigate the
performance of the proposed approach on more (balanced and imbalanced)
datasets and further optimize our model towards improved classification
performance. Furthermore, it should be investigated how combinations of
augmentation techniques influence the resulting classification performance and
if it is possible to maximize the impact of augmentations through an optimized
combination scheme.

The improved performance achieved by the proposed augmentation method comes at
the cost of increased demands on computational power and resources. While
signal processing augmentations are computed in the range of seconds to
minutes, our model requires an additional training step which takes $\sim$6
hours for the presented dataset and increases with larger datasets.

Because we created the proposed clinical dataset in a way that it resembles
the phases and surgical actions executed during a real THA procedure,
potential future clinical applications are the prediction of surgical actions
from captured audio signals in the operating room which could be used for
workflow recognition and surgical phase detection. Therefore, we consider the
proposed dataset as an important step towards automated audio-based clinical
workflow detection systems, a topic which has only been studied rudimentally
so far [24, 27]. The proposed approach is designed to work with spectrogram
based audio, which can be transformed back to the signal domain, e.g. using
the Griffin-Lim algorithm [4] or more recently introduced learning-based
transformation approaches, e.g. the work by Takamichi et al. [25]. We
reconstructed waveforms from a few generated spectrograms using the Griffin-
Lim algorithm and could, despite artifacts being present, recognize acoustic
similarities to the original samples for each class, respectively. In future
work, the proposed augmentation method could furthermore be transferred to
other medical and non-medical grid-like data domains.

##  5 Conclusion

In the presented work, we introduce a novel data augmentation method for
medical audio data and evaluate it on a clinical dataset which was recorded in
real-world Total Hip Arthroplasty (THA) surgeries. The proposed dataset
contains sound samples of six surgical actions which resemble the different
phases of a THA intervention. We show in quantitative evaluations that the
proposed method outperforms classical signal and spectrogram processing-based
augmentation techniques in terms of Mean Macro F1-Score, evaluated using a
ResNet-18 classifier in a 5-fold cross validation experiment. By generating
high-quality in-distribution samples for data augmentation, our method has the
potential to improve the data bottleneck for acoustic learning-based medical
support systems.

## Acknowledgment

This work is part of the SURGENT project under the umbrella of
Hochschulmedizin Zürich.

## References

  * [1] Chatziagapi, A., Paraskevopoulos, G., Sgouropoulos, D., Pantazopoulos, G., Nikandrou, M., Giannakopoulos, T., Katsamanis, A., Potamianos, A., Narayanan, S.: Data Augmentation Using GANs for Speech Emotion Recognition. In: Proc. Interspeech 2019. pp. 171–175 (2019)
  * [2] Ewald, H., Timm, U., Ruther, C., Mittelmeier, W., Bader, R., Kluess, D.: Acoustic sensor system for loosening detection of hip implants. In: 2011 Fifth International Conference on Sensing Technology. pp. 494–497 (2011)
  * [3] Goossens, Q., Pastrav, L., Roosen, J., Mulier, M., Desmet, W., Vander Sloten, J., Denis, K.: Acoustic analysis to monitor implant seating and early detect fractures in cementless tha: An in vivo study. Journal of Orthopedic Research (2020)
  * [4] Griffin, D., Lim, J.: Signal estimation from modified short-time fourier transform. IEEE Transactions on Acoustics, Speech, and Signal Processing 32(2), 236–243 (1984)
  * [5] Gulrajani, I., Ahmed, F., Arjovsky, M., Dumoulin, V., Courville, A.: Improved training of wasserstein gans. In: Proceedings of the 31st International Conference on Neural Information Processing Systems. pp. 5769––5779 (2017)
  * [6] He, K., Zhang, X., Ren, S., Sun, J.: Deep residual learning for image recognition. In: 2016 IEEE Conference on Computer Vision and Pattern Recognition (CVPR). pp. 770–778 (2016)
  * [7] Heusel, M., Ramsauer, H., Unterthiner, T., Nessler, B., Hochreiter, S.: Gans trained by a two time-scale update rule converge to a local nash equilibrium. In: Proceedings of the 31st International Conference on Neural Information Processing Systems. p. 6629–6640 (2017)
  * [8] Hu, H., Tan, T., Qian, Y.: Generative adversarial networks based data augmentation for noise robust speech recognition. In: 2018 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP). pp. 5044–5048 (2018)
  * [9] Illanes, A., Boese, A., Maldonado, I., Pashazadeh, A., Schaufler, A., Navab, N., Friebe, M.: Novel clinical device tracking and tissue event characterization using proximally placed audio signal acquisition and processing. Scientific Reports 8 (2018)
  * [10] Jayalakshmy, S., Sudha, G.F.: Conditional gan based augmentation for predictive modeling of respiratory signals. Computers in Biology and Medicine 138, 104930 (2021)
  * [11] Kim, K.S., Seo, J.H., Kang, J.U., Song, C.G.: An enhanced algorithm for knee joint sound classification using feature extraction based on time-frequency analysis. Computer Methods and Programs in Biomedicine 94(2), 198–206 (2009)
  * [12] Madhu, A., Kumaraswamy, S.: Data augmentation using generative adversarial network for environmental sound classification. In: 2019 27th European Signal Processing Conference (EUSIPCO) (2019)
  * [13] Mariani, G., Scheidegger, F., Istrate, R., Bekas, C., Malossi, A.C.I.: Bagan: Data augmentation with balancing gan. arXiv abs/1803.09655 (2018)
  * [14] Marshall, A., Boussakta, S.: Signal analysis of medical acoustic sounds with applications to chest medicine. Journal of the Franklin Institute 344(3), 230–242 (2007)
  * [15] McFee, B., Raffel, C., Liang, D., PW Ellis, D., McVicar, M., Battenberg, E., Nieto, O.: librosa: Audio and music signal analysis in python. In: 14th python in science conference. pp. 18–25 (2015)
  * [16] Ostler, D., Seibold, M., Fuchtmann, J., Samm, N., Feussner, H., Wilhelm, D., Navab, N.: Acoustic signal analysis of instrument–tissue interaction for minimally invasive interventions. International Journal of Computer Assisted Radiology and Surgery (2020)
  * [17] Park, D.S., Chan, W., Zhang, Y., Chiu, C.C., Zoph, B., Cubuk, E.D., Le, Q.V.: Specaugment: A simple data augmentation method for automatic speech recognition. Interspeech 2019 (Sep 2019)
  * [18] Purwins, H., Li, B., Virtanen, T., Schlüter, J., Chang, S.y., Sainath, T.: Deep learning for audio signal processing. IEEE Journal on Selected Topics in Signal Processing 14, 206–219 (2019)
  * [19] Rodgers, G.W., Young, J.L., Fields, A.V., Shearer, R.Z., Woodfield, T.B.F., Hooper, G.J., Chase, J.G.: Acoustic emission monitoring of total hip arthroplasty implants. IFAC Proceedings Volumes 47(3), 4796–4800 (2014), 19th IFAC World Congress
  * [20] Seibold, M., Hoch, A., Suter, D., Farshad, M., Zingg, P.O., Navab, N., Fürnstahl, P.: Acoustic-based spatio-temporal learning for press-fit evaluation of femoral stem implants. In: International Conference on Medical Image Computing and Computer-Assisted Intervention. pp. 447–456 (2021)
  * [21] Seibold, M., Maurer, S., Hoch, A., Zingg, P., Farshad, M., Navab, N., Fürnstahl, P.: Real-time acoustic sensing and artificial intelligence for error prevention in orthopedic surgery. Scientific Reports 11 (2021)
  * [22] Sheng, P., Yang, Z., Hu, H., Tan, T., Qian, Y.: Data augmentation using conditional generative adversarial networks for robust speech recognition. In: 2018 11th International Symposium on Chinese Spoken Language Processing (ISCSLP). pp. 121–125 (2018)
  * [23] Suehn, T., Pandey, A., Friebe, M., Illanes, A., Boese, A., Lohman, C.: Acoustic sensing of tissue-tool interactions – potential applications in arthroscopic surgery. Current Directions in Biomedical Engineering 6 (2020)
  * [24] Suzuki, T., Sakurai, Y., Yoshimitsu, K., Nambu, K., Muragaki, Y., Iseki, H.: Intraoperative multichannel audio-visual information recording and automatic surgical phase and incident detection. In: 2010 Annual International Conference of the IEEE Engineering in Medicine and Biology. pp. 1190–1193 (2010)
  * [25] Takamichi, S., Saito, Y., Takamune, N., Kitamura, D., Saruwatari, H.: Phase reconstruction from amplitude spectrograms based on directional-statistics deep neural networks. Signal Processing 169, 107368 (2020)
  * [26] Tirindelli, M., Eilers, C., Simson, W., Paschali, M., Azampour, M.F., Navab, N.: Rethinking ultrasound augmentation: A physics-inspired approach. In: Medical Image Computing and Computer Assisted Intervention. pp. 690–700 (2021)
  * [27] Weede, O., Dittrich, F., Wörn, H., Jensen, B., Knoll, A., Wilhelm, D., Kranzfelder, M., Schneider, A., Feussner, H.: Workflow analysis and surgical phase recognition in minimally invasive surgery. In: 2012 IEEE International Conference on Robotics and Biomimetics (ROBIO). pp. 1080–1074 (2012)
  * [28] Wei, S., Zou, S., Liao, F., Lang, W.: A comparison on data augmentation methods based on deep learning for audio classification. Journal of Physics: Conference Series 1453(1), 012085 (2020)