$[w/x]\mathcal{L}_{u}$ of $\mathsf{lin}(u,\ [w/x]\varepsilon(P))$ for each
$u\in\operatorname{dom}(\Delta,w:A)$ (lemma A.4 and (3))

  10. (10)

$[w/x]\mathcal{L}^{\prime}_{u}$ of $\mathsf{lin}(u,\ [w/x]\varepsilon(Q))$ for
each $u\in\operatorname{dom}(\Delta,w:B)$ (lemma A.4 and (4))

Let $\varepsilon(\mathcal{D})$ be given by

$\mathtt{case}\ x\ (w.[w/x]\varepsilon(P),\
w.[w/x]\varepsilon(Q))\lx@proof@logical@and[w/x]\varepsilon(P)\Vdash\Delta,x:A\oplus
B,w:A\mathcal{W}_{1}[w/x]\varepsilon(Q)\Vdash\Delta,x:A\oplus
B,w:B\mathcal{W}_{2}$

This derivation has the correct conclusion by $\alpha$-equivalence.

Linearity $\mathsf{lin}(u,\ \mathtt{case}\ x\ (w.[w/x]\varepsilon(P),\
w.[w/x]\varepsilon(Q)))$ for $u\in\operatorname{dom}(\Delta,x:A\with B)$ is
given by case analysis on $u$:

$u=x$

We are done by $[w/x]\mathcal{L}_{x}$, $[w/x]\mathcal{L}^{\prime}_{x}$, and
$L_{\mathtt{case}}$.

$u\in\operatorname{dom}(\Delta)$

We are done by $[w/x]\mathcal{L}_{x}$, $[w/x]\mathcal{L}^{\prime}_{x}$, and
$L_{\mathtt{case2}}$.

($1$)

Assume $\mathcal{D}$ is given by

$\mathsf{close}\;x\vdash x:1$

Let $\varepsilon(\mathcal{D})$ be given by [$1$]. Linearity $\mathsf{lin}(x,\
\varepsilon(\mathtt{close}\ x))$ is given by $L_{\mathtt{close}}$.

($\bot$)

Assume $\mathcal{D}$ is given by

$\mathsf{wait}\;x;P\vdash\Delta,x:\bot P\vdash\Delta\mathcal{D}_{1}$

There exist derivations

  1. (1)

$\varepsilon(\mathcal{D}_{1})$ of $\varepsilon(P)\Vdash\Delta$ (induction
hypothesis)

  2. (2)

$\mathcal{L}_{u}$ of $\mathsf{lin}(u,\ \varepsilon(P))$ for each
$u\in\operatorname{dom}(\Delta)$ (induction hypothesis)

Let $\varepsilon(\mathcal{D})$ be given by

$\mathtt{wait}\ x;\
\varepsilon(P)\Vdash\Delta,x:\bot\varepsilon(P)\Vdash\Delta\varepsilon(\mathcal{D}_{1})$

Linearity $\mathsf{lin}(u,\ \mathtt{wait}\ x;\ \varepsilon(P))$ for
$u\in\operatorname{dom}(\Delta,x:\bot)$ is given by $L_{\mathtt{wait}}$ if
$u=x$, and by $L_{\mathtt{wait2}}$ and $\mathcal{L}_{u}$ otherwise.

We now show the converse, namely, that if $\mathcal{D}$ is a derivation of
$\mathtt{P}\Vdash\Gamma,\Delta$ where
$\operatorname{fn}(\mathtt{P})=\operatorname{dom}(\Delta)$ and
$\mathsf{lin}(\Delta,\ \mathtt{P})$, then there exists a derivation
$\delta(\mathcal{D})$ of $\delta(\mathtt{P})\vdash\Delta$ and
$\varepsilon(\delta(\mathtt{P}))=\mathtt{P}$. We will repeatedly use the
following fact: if $\mathtt{P}\Vdash\Gamma$, then by lemma A.3 there exists a
$\Delta\subseteq\Gamma$ such that
$\operatorname{dom}(\Delta)=\operatorname{fn}(\mathtt{P})$ We proceed by
induction on the derivation $\mathcal{D}$ of $\mathtt{P}\Vdash\Gamma,\Delta$.

[Id]

Assume $\mathcal{D}$ is given by

$\mathtt{fwd}\ x\ y\Vdash\Gamma,x:A,y:A^{\bot}$

Then $\Delta=x:A,y:A^{\bot}$. Let $\delta(\mathcal{D})$ be given by

$\mathsf{fwd}\;x\,y\vdash x:A,y:A^{\bot}$

It is clear that $\varepsilon(\delta(\mathtt{fwd}\ x\ y))=\mathtt{fwd}\ x\ y$.

[Cut]

Assume $\mathcal{D}$ is given by

$\nu
x{:}A.(\mathtt{P}\mathbin{\|}\mathtt{Q})\Vdash\Gamma\lx@proof@logical@and\mathtt{P}\Vdash\Gamma,x:A\mathcal{D}_{1}\mathsf{lin}(x,\
\mathtt{P})\mathcal{L}_{1}\mathtt{Q}\Vdash\Gamma,x:A^{\bot}\mathcal{D}_{2}\mathsf{lin}(x,\
\mathtt{Q})\mathcal{L}_{2}$

We start by showing that $\mathsf{lin}(\mathtt{P})$. Observe that
$x\in\operatorname{fn}(\mathtt{P})$ by lemma A.7 and $\mathsf{lin}(x,\
\mathtt{P})$. Let $\Delta_{1}\subseteq\Gamma$ be such that
$\operatorname{dom}(\Delta_{1},x:A)=\operatorname{fn}(\mathtt{P})$. Showing
$\mathsf{lin}(\mathtt{P})$ thus requires showing
$\mathsf{lin}(\Delta_{1},x:A,\ \mathtt{P})$. By inversion on $L_{\nu 1}$, it
follows that $\mathsf{lin}(z,\ \mathtt{P})$ for all
$z\in\operatorname{dom}(\Delta_{1})$. We have $\mathsf{lin}(x,\ \mathtt{P})$
by assumption. This gives $\mathsf{lin}(\mathtt{P})$ as desired. By the
induction hypothesis, there exists a derivation $\delta(\mathcal{D}_{1})$ of
$\mathtt{P}\vdash\Delta_{1},x:A$. An identical argument produces a derivation
$\delta(\mathcal{D}_{2})$ of $\mathtt{Q}\vdash\Delta_{2},x:A^{\bot}$.

Let $\delta(\mathcal{D})$ be given by

$\nu
x{:}A.(\delta(\mathtt{P})\mathbin{\|}\delta(\mathtt{Q}))\vdash\Delta_{1},\Delta_{2}\lx@proof@logical@and\delta(\mathtt{P})\vdash\Delta_{1},x:A\delta(\mathcal{D}_{1})\delta(\mathtt{Q})\vdash\Delta_{2},x:A^{\bot}\delta(\mathcal{D}_{2})$

Finally, we show that $\varepsilon(\delta(\nu
x{:}A.(\delta(\mathtt{P})\mathbin{\|}\delta(\mathtt{Q}))))=\nu
x{:}A.(\mathtt{P}\mathbin{\|}\mathtt{Q})$. By the induction hypothesis,
${\varepsilon(\delta(\mathtt{P}))=\mathtt{P}}$ and analogously for
$\mathtt{Q}$. Using this, we compute:

$\displaystyle\varepsilon(\delta(\nu
x{:}A.(\delta(\mathtt{P})\mathbin{\|}\delta(\mathtt{Q}))))$
$\displaystyle=\varepsilon(\nu
x{:}A.(\delta(\mathtt{P})\mathbin{\|}\delta(\mathtt{Q})))$ $\displaystyle=\nu
x{:}A.(\varepsilon(\delta(\mathtt{P}))\mathbin{\|}\varepsilon(\delta(Q)))$
$\displaystyle=\nu x{:}A.(\mathtt{P}\mathbin{\|}\mathtt{Q}).$

[$\otimes$]

Assume $\mathcal{D}$ is given by

$\mathtt{out}\ x;\
(y.\mathtt{P}\mathbin{\|}w.\mathtt{Q})\Vdash\Gamma,x:A\otimes
B\lx@proof@logical@and\mathtt{P}\Vdash\Gamma,x:A\otimes
B,y:A\mathcal{D}_{1}\mathsf{lin}(y,\
\mathtt{P})\mathcal{L}\mathtt{Q}\Vdash\Gamma,x:A\otimes B,w:B\mathcal{D}_{2}$

We follow a similar approach as in the case [Cut].

We first show $\mathsf{lin}(\mathtt{P})$, which requires checking the
linearity of each free name in $\mathtt{P}$. By lemma A.3,
$\operatorname{fn}(\mathtt{P})\subseteq\operatorname{dom}(\Gamma,x:A\otimes
B,y:A)$. We claim that
$\operatorname{fn}(\mathtt{P})=\operatorname{dom}(\Delta_{1},y:A)$ for some
$\Delta_{1}\subseteq\Gamma$:

  * •

$y\in\operatorname{fn}(\mathtt{P})$ by $\mathsf{lin}(y,\ \mathtt{P})$ and
lemma A.7;

  * •

$x\notin\operatorname{fn}(\mathtt{P})$ by inversion on $\mathsf{lin}(x,\
\mathtt{out}\ x;\ (y.\mathtt{P}\mathbin{\|}w.\mathtt{Q}))$ and
$L_{\mathtt{out}}$;

This establishes that
$\operatorname{fn}(\mathtt{P})=\operatorname{dom}(\Delta_{1},y:A)$ for some
$\Delta_{1}\subseteq\Gamma$.

Having established the set of free names that must be linear, we check
$\mathsf{lin}(P)$. To do so, we rely on the fact that the sets
$\operatorname{fn}(\mathtt{P})$ and $\operatorname{fn}(\mathtt{Q})$ are
disjoint by inversion on $L_{\mathtt{out}}$, $L_{\mathtt{out2}}$,
$L_{\mathtt{out3}}$ using $\mathsf{lin}(\Gamma,x:A\otimes B,\ \mathtt{out}\
x;\ (y.\mathtt{P}\mathbin{\|}w.\mathtt{Q}))$.

  * •

$\mathsf{lin}(y,\ \mathtt{P})$ by assumption;

  * •

$\mathsf{lin}(z,\ \mathtt{P})$ for all $z\in\operatorname{dom}(\Delta_{1})$ by
inversion on $L_{\mathtt{out2}}$ and linearity of $\mathtt{out}\ x;\
(y.\mathtt{P}\mathbin{\|}w.\mathtt{Q})$. Indeed, $L_{\mathtt{out2}}$ is the
only rule that could have been applied for
$z\in\operatorname{dom}(\Delta_{1})$ because $\mathtt{P}$ and $\mathtt{Q}$
have disjoint sets of free names.

We conclude $\mathsf{lin}(P)$. It follows by the induction hypothesis that
there then exists a derivation $\delta(\mathcal{D}_{1})$ of
$\delta(\mathtt{P})\vdash\Delta_{1},y:A$.

A similar argument implies that $\mathsf{lin}(\mathtt{Q})$. The induction
hypothesis produces a derivation $\delta(\mathcal{D}_{2})$ of
$\delta(\mathtt{Q})\vdash\Delta_{2},w:B$. By genericity, it follows that there
exists a derivation $[x/w]\delta(\mathcal{D}_{2})$ of
$[x/w]\delta(\mathtt{Q})\vdash\Delta_{2},x:B$.

Let the derivation $\delta(\mathcal{D})$ be given by

$\mathsf{out}\;x\,y;(\delta(\mathtt{P})\mathbin{\|}[x/w]\delta(Q))\vdash\Delta_{1},\Delta_{2},x:A\otimes
B\lx@proof@logical@and\delta(\mathtt{P})\vdash\Delta_{1},y:A\delta(\mathcal{D}_{1})[x/w]\delta(\mathtt{Q})\vdash\Delta_{2},x:B[x/w]\delta(\mathcal{D}_{2})$

It remains to show that $\varepsilon(\delta(\mathtt{out}\ x;\
(y.\mathtt{P}\mathbin{\|}w.\mathtt{Q})))=\mathtt{out}\ x;\
(y.\mathtt{P}\mathbin{\|}w.\mathtt{Q})$. Because
$x\notin\operatorname{fn}(\mathtt{Q})$, it follows that

$\mathtt{out}\ x;\
(y.\mathtt{P}\mathbin{\|}w.\mathtt{Q})\equiv_{\alpha}\mathtt{out}\ x;\
(y.\mathtt{P}\mathbin{\|}x.[x/w]\mathtt{Q})$

are $\alpha$-equivalent processes. By the induction hypothesis, we know that
$\varepsilon(\delta(\mathtt{P}))=\mathtt{P}$ and
$\varepsilon(\delta(\mathtt{Q}))=\mathtt{Q}$. We compute:

$\displaystyle\varepsilon(\delta(\mathtt{out}\ x;\
(y.\mathtt{P}\mathbin{\|}w.\mathtt{Q})))$
$\displaystyle=\varepsilon(\delta(\mathtt{out}\ x;\
(y.\mathtt{P}\mathbin{\|}x.[x/w]\mathtt{Q})))$
$\displaystyle=\varepsilon(\mathsf{out}\;x\,y;(\delta(\mathtt{P})\mathbin{\|}[x/x]\delta([x/w]\mathtt{Q})))$
$\displaystyle=\varepsilon(\mathsf{out}\;x\,y;(\delta(\mathtt{P})\mathbin{\|}\delta([x/w]\mathtt{Q})))$
$\displaystyle=\mathtt{out}\ x;\
(y.\varepsilon(\delta(\mathtt{P}))\mathbin{\|}x.\varepsilon(\delta([x/w]\mathtt{Q})))$
which by applying lemmas A.6 and A.4 to $\mathsf{lin}(\mathtt{Q})$,
$\displaystyle=\mathtt{out}\ x;\
(y.\varepsilon(\delta(\mathtt{P}))\mathbin{\|}x.\varepsilon([x/w](\delta(\mathtt{Q}))))$
which by applying lemma A.5 to $[x/w]\delta(\mathtt{Q})\vdash\Delta_{2},x:B$
$\displaystyle=\mathtt{out}\ x;\
(y.\varepsilon(\delta(\mathtt{P}))\mathbin{\|}x.[x/w](\varepsilon(\delta(\mathtt{Q}))))$
$\displaystyle=\mathtt{out}\ x;\
(y.\varepsilon(\delta(\mathtt{P}))\mathbin{\|}w.\varepsilon(\delta(\mathtt{Q}))))$
$\displaystyle=\mathtt{out}\ x;\ (y.\mathtt{P}\mathbin{\|}w.\mathtt{Q})$

This completes the case.

[$\invamp$]

Assume $\mathcal{D}$ is given by

$\mathtt{inp}\ x\ (w.y.\mathtt{P})\Vdash\Gamma,x:A\invamp
B\lx@proof@logical@and\mathtt{P}\Vdash\Gamma,x:A\invamp
B,w:B,y:A\mathcal{D}_{1}\mathsf{lin}(y,\ \mathtt{P})\mathcal{L}_{y}$

We show that $\mathsf{lin}(\mathtt{P})$. We start by showing that
$\operatorname{fn}{\mathtt{P}}=\operatorname{dom}(\Delta,w:B,y:A)$ for some
$\Delta\subseteq\Gamma$. By inversion on $\mathtt{P}\Vdash\Gamma,x:A\invamp
B,w:B,y:A$ with $L_{\mathtt{inp}}$ and $L_{\mathtt{inp2}}$, we deduce
$\mathsf{lin}(u,\ \mathtt{P})$ for all $u\in\operatorname{dom}(\Delta,w:B)$.
We know $\mathsf{lin}(y,\ \mathtt{P})$ by hypothesis. We deduce
$\mathsf{lin}(\mathtt{P})$. By the induction hypothesis, there exists a
derivation $\delta(\mathcal{D}_{1})$ of
$\delta(\mathtt{P})\vdash\Delta,w:B,y:A$. By genericity, there exists a
derivation $[x/w]\delta(\mathcal{D}_{1})$ of
$[x/w]\delta(\mathtt{P})\vdash\Delta,x:B,y:A$.

Let the derivation $\delta(\mathcal{D})$ be given by:

$\mathsf{inp}\;x\,y;[x/w]\delta(\mathtt{P})\vdash\Delta,x:A\invamp
B[x/w](\delta(\mathtt{P}))\vdash\Delta,x:B,y:A[x/w]\delta(\mathcal{D}_{1})$

It remains to show that $\varepsilon(\delta(\mathtt{inp}\ x\
(w.y.\mathtt{P})))=\mathtt{inp}\ x\ (w.y.\mathtt{P})$. We compute:

$\displaystyle\varepsilon(\delta(\mathtt{inp}\ x\ (w.y.\mathtt{P})))$
$\displaystyle=\varepsilon(\mathsf{inp}\;x\,y;[x/w]\delta(\mathtt{P}))$ which
by lemma A.5 $\displaystyle=\mathtt{inp}\ x\
(x.y.\varepsilon([x/w]\delta(\mathtt{P})))$ $\displaystyle=\mathtt{inp}\ x\
(x.y.[x/w](\varepsilon(\delta(\mathtt{P}))))$ which by the induction
hypothesis $\displaystyle=\mathtt{inp}\ x\ (x.y.[x/w]\mathtt{P})$
$\displaystyle=\mathtt{inp}\ x\ (w.y.\mathtt{P})$

[$\oplus_{1}$]

Assume $\mathcal{D}$ is given by

$\mathtt{inl}\ x;\ w.\mathtt{P}\Vdash\Gamma,x:A\oplus
B\mathtt{P}\Vdash\Gamma,x:A\oplus B,w:A\mathcal{D}_{1}$

We show that $\mathsf{lin}(\mathtt{P})$ to be able to apply the induction
hypothesis. By inversion on the assumption $\mathsf{lin}(\mathtt{inl}\ x;\
w.\mathtt{P})$ with $L_{\mathtt{inl}}$, we know that
$x\notin\operatorname{fn}(\mathtt{P})$ and
$w\in\operatorname{fn}(\mathtt{P})$. Let $\Delta\subseteq\Gamma$ be such that
$\operatorname{fn}(\mathtt{P})=\operatorname{dom}(\Delta,w:A)$. Then by the
induction hypothesis, there exists a derivation $\delta(\mathcal{D}_{1})$ of
$\delta(\mathtt{P})\vdash\Delta,w:A$. By genericity, there exists a derivation
$[x/w]\delta(\mathcal{D}_{1})$ of $[x/w]\delta(\mathtt{P})\vdash\Delta,x:A$.

Let the derivation $x{[\mathsf{inl}]};P\Vdash\Delta,x:A\oplus B$ be given by

$x{[\mathsf{inl}]};P\vdash\Delta,x:A\oplus
B[x/w]\delta(\mathtt{P})\vdash\Delta,x:A[x/w]\delta(\mathcal{D}_{1})$

It remains to show that $\varepsilon(\delta(\mathtt{inl}\ x;\
w.\mathtt{P}))=\mathtt{inl}\ x;\ w.\mathtt{P}$. We compute:

$\displaystyle\varepsilon(\delta(\mathtt{inl}\ x;\ w.\mathtt{P}))$
$\displaystyle=\varepsilon(x{[\mathsf{inl}]};[x/w]\delta(\mathtt{P}))$
$\displaystyle=\mathtt{inl}\ x;\ x.\varepsilon([x/w]\delta(\mathtt{P}))$ which
by lemma A.5 $\displaystyle=\mathtt{inl}\ x;\
x.[x/w](\varepsilon(\delta(\mathtt{P})))$ which by the induction hypothesis
$\displaystyle=\mathtt{inl}\ x;\ x.[x/w]\mathtt{P}$
$\displaystyle=\mathtt{inl}\ x;\ w.\mathtt{P}$

[$\oplus_{2}$]

This case in analogous to the case [$\oplus_{1}$].

[$\with$]

Assume $\mathcal{D}$ is given by

$\mathtt{case}\ x\ (w.\mathtt{P},\ w.\mathtt{Q})\Vdash\Gamma,x:A\with
B\lx@proof@logical@and\mathtt{P}\Vdash\Gamma,x:A\with
B,w:A\mathcal{D}_{1}\mathtt{Q}\Vdash\Gamma,x:A\with B,w:B\mathcal{D}_{2}$

We show $\mathsf{lin}(\mathtt{P})$. By inversion on
$\mathsf{lin}(\mathtt{case}\ x\ (w.\mathtt{P},\ w.\mathtt{Q}))$ with
$L_{\mathtt{case}}$ and $L_{\mathtt{case2}}$, we deduce $x\notin\mathtt{P}$
and $w\in\mathtt{P}$. Let $\Delta\subseteq\Gamma$ be such that
$\operatorname{dom}(\Delta,w:A)=\operatorname{fn}(\mathtt{P})$. By the
induction hypothesis, there exists a derivation $\delta(\mathcal{D}_{1})$ of
$\delta(\mathtt{P})\vdash\Delta,w:A$. By genericity, there exists a derivation
$[x/w]\delta(\mathcal{D}_{1})$ of $[x/w]\mathtt{P}\vdash\Delta,x:A$.

An analogous argument gives $\mathsf{lin}(\mathtt{Q})$ and a derivation a
derivation $[x/w]\delta(\mathcal{D}_{2})$ of
$[x/w]\mathtt{Q}\vdash\Delta,x:B$.

Let $\delta(\mathcal{D})$ be given by

$\mathsf{case}\;x\ (P,\,Q)\vdash\Delta,x:A\with
B\lx@proof@logical@and[x/w]\mathtt{P}\vdash\Delta,x:A[x/w]\delta(\mathcal{D}_{1})[x/w]\mathtt{Q}\vdash\Delta,x:B[x/w]\delta(\mathcal{D}_{2})$

The induction hypothesis and lemma A.5 imply
$\varepsilon(\delta(\mathtt{case}\ x\ (w.\mathtt{P},\
w.\mathtt{Q})))=\mathtt{case}\ x\ (w.\mathtt{P},\ w.\mathtt{Q})$.

[$1$]

Assume $\mathcal{D}$ is given by

$\mathsf{close}\;x\Vdash\Gamma,x:1$

Let $\delta(\mathcal{D})$ be given by

$\mathsf{close}\;x\vdash x:1$

It is clear that $\varepsilon(\delta(\mathtt{close}\ x))=\mathtt{close}\ x$.

[$\bot$]

Assume $\mathcal{D}$ is given by

$\mathsf{wait}\;x;\mathtt{P}\Vdash\Gamma,x:\bot\mathtt{P}\Vdash\Gamma\mathcal{D}_{1}$

By inversion on $\mathsf{lin}(\mathtt{wait}\ x;\ \mathtt{P})$ and
$L_{\mathtt{wait}}$, $x\notin\operatorname{fn}(\mathtt{P})$. Let
$\Delta\subseteq\Gamma$ be such that
$\operatorname{fn}(\mathtt{P})=\operatorname{dom}(\Delta)$. By the induction
hypothesis, there exists a derivation $\delta(\mathcal{D})$ of
$\delta(\mathtt{P})\vdash\Delta$.

Let the derivation $\delta(\mathcal{D})$ be given by

$\mathsf{wait}\;x;P\vdash\Delta,x:\bot P\vdash\Delta\delta(\mathcal{D})$

It is easy to check using the induction hypothesis that
$\varepsilon(\delta(\mathtt{wait}\ x;\ \mathtt{P}))=\mathtt{wait}\ x;\
\mathtt{P}$.

Finally, we show the desired identities for compositions of $\varepsilon$ and
$\delta$ on derivations. When $\mathcal{D}$ is a CP typing derivation, lemma
A.8 implies that $\delta(\varepsilon(\mathcal{D}))=\mathcal{D}$. Indeed, if
$\mathcal{D}$ is a derivation of $P\vdash\Delta$, then so is
$\delta(\varepsilon(\mathcal{D}))$ by the above. But there exists at most one
derivation of $P\vdash\Delta$, so we conclude
$\mathcal{D}=\delta(\varepsilon(\mathcal{D}))$.

If $\mathcal{D}$ is a derivation of $\mathtt{P}\Vdash\Gamma,\Delta$ where
$\operatorname{dom}(\Delta)=\operatorname{fn}(\mathtt{P})$ and
$\mathsf{lin}(\mathtt{P})$, then $\varepsilon(\delta(\mathcal{D}))$ is a
derivation of $\mathtt{P}\Vdash\Delta$. Weakening this derivation by $\Gamma$
gives a derivation $\mathcal{W}$ of $\mathtt{P}\Vdash\Gamma,\Delta$. But lemma
A.8 then implies that $\mathcal{W}=\mathcal{D}$. This is what we wanted to
show. ∎

##  Appendix B Adequacy proof of the LF encoding of SCP

###  B.1. Proof of Lemma 5.1

###### Lemma B.1 (Adequacy of tp).

There exists a bijection between the set of session types and canonical LF
terms $M$ such that
$\vdash_{LF}{M}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{tp}}$.

###### Proof.

We define the encoding ${}^{\ulcorner}{{-}^{\urcorner}}$ and decoding
$\left\lfloor-\right\rfloor$ of types in SCP as follows:

$\displaystyle{}^{\ulcorner}{{1}^{\urcorner}}$ $\displaystyle=1$
$\displaystyle{}^{\ulcorner}{{\bot}^{\urcorner}}$ $\displaystyle=\bot$
$\displaystyle{}^{\ulcorner}{{A\otimes B}^{\urcorner}}$
$\displaystyle={}^{\ulcorner}{{A}^{\urcorner}}\otimes{}^{\ulcorner}{{B}^{\urcorner}}$
$\displaystyle{}^{\ulcorner}{{A\invamp B}^{\urcorner}}$
$\displaystyle={}^{\ulcorner}{{A}^{\urcorner}}\invamp{}^{\ulcorner}{{B}^{\urcorner}}$
$\displaystyle{}^{\ulcorner}{{A\oplus B}^{\urcorner}}$
$\displaystyle={}^{\ulcorner}{{A}^{\urcorner}}\oplus{}^{\ulcorner}{{B}^{\urcorner}}$
$\displaystyle{}^{\ulcorner}{{A\with B}^{\urcorner}}$
$\displaystyle={}^{\ulcorner}{{A}^{\urcorner}}\with{}^{\ulcorner}{{B}^{\urcorner}}$
$\displaystyle\left\lfloor 1\right\rfloor$ $\displaystyle=1$
$\displaystyle\left\lfloor\bot\right\rfloor$ $\displaystyle=\bot$
$\displaystyle\left\lfloor A\otimes B\right\rfloor$
$\displaystyle=\left\lfloor A\right\rfloor\otimes\left\lfloor B\right\rfloor$
$\displaystyle\left\lfloor A\invamp B\right\rfloor$
$\displaystyle=\left\lfloor A\right\rfloor\invamp\left\lfloor B\right\rfloor$
$\displaystyle\left\lfloor A\oplus B\right\rfloor$ $\displaystyle=\left\lfloor
A\right\rfloor\oplus\left\lfloor B\right\rfloor$ $\displaystyle\left\lfloor
A\with B\right\rfloor$ $\displaystyle=\left\lfloor
A\right\rfloor\with\left\lfloor B\right\rfloor$

${}^{\ulcorner}{{-}^{\urcorner}}$ and $\left\lfloor-\right\rfloor$ are clearly
inverses of each other and satisfies adequacy. ∎

###  B.2. Proof of Lemma 5.2

###### Lemma B.2 (Adequacy of dual).

  1. (1)

For any session type $A$, there exists a unique LF canonical form $D$ such
that
$\vdash_{LF}{D}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{dual}}\;{{}^{\ulcorner}{{A}^{\urcorner}}}\;{{}^{\ulcorner}{{A^{\bot}}^{\urcorner}}}$

  2. (2)

For any LF canonical form $D$ such that
$\vdash_{LF}{D}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{dual}}\;{{}^{\ulcorner}{{A}^{\urcorner}}}\;{{}^{\ulcorner}{{A^{\prime}}^{\urcorner}}}$,
$\;A^{\prime}=A^{\bot}$.

###### Proof.

We show some cases for both parts. For (1), by induction on $A$.

######  Case 1.

$A=1$, then $A^{\bot}=\bot$, and therefore ${}^{\ulcorner}{{A}^{\urcorner}}=1$
and ${}^{\ulcorner}{{A^{\bot}}^{\urcorner}}=\bot$. So we can use the LF
constructor D1 : dual 1 $\bot$. Uniqueness follows by inspecting other
constructors.

######  Case 2.

$A=B\otimes C$, then $A^{\bot}=B^{\bot}\invamp C^{\bot}$, and therefore
${}^{\ulcorner}{{A}^{\urcorner}}={}^{\ulcorner}{{B}^{\urcorner}}\otimes{}^{\ulcorner}{{C}^{\urcorner}}$
and
${}^{\ulcorner}{{A^{\bot}}^{\urcorner}}={}^{\ulcorner}{{B^{\bot}}^{\urcorner}}\invamp{}^{\ulcorner}{{C^{\bot}}^{\urcorner}}$.
Then by induction hypothesis there exist unique LF derivations $D$ and $E$
such that
${\vdash_{LF}{D}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{dual}}\;{{}^{\ulcorner}{{B}^{\urcorner}}}\;{{}^{\ulcorner}{{B^{\bot}}^{\urcorner}}}}$
and
${\vdash_{LF}{E}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{dual}}\;{{}^{\ulcorner}{{C}^{\urcorner}}}\;{{}^{\ulcorner}{{C}^{\urcorner}}}}$.
We now use the constructor D$\otimes$ , and uniqueness follows by inspecting
other constructors.

For (2), by induction on the dervation of $D$ such that
${\vdash_{LF}{D}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{dual}}\;{{}^{\ulcorner}{{A}^{\urcorner}}}\;{{}^{\ulcorner}{{A^{\prime}}^{\urcorner}}}}$.

######  Case 1.

D1, then ${}^{\ulcorner}{{A}^{\urcorner}}=1$ and
${}^{\ulcorner}{{A^{\prime}}^{\urcorner}}=\bot$, so $A=1$ and
$A^{\prime}=\bot=A^{\bot}$.

######  Case 2.

D$\otimes$ , then
${}^{\ulcorner}{{A}^{\urcorner}}={}^{\ulcorner}{{B}^{\urcorner}}\otimes{}^{\ulcorner}{{C}^{\urcorner}}$
and
${}^{\ulcorner}{{A^{\prime}}^{\urcorner}}={}^{\ulcorner}{{B^{\prime}}^{\urcorner}}\otimes{}^{\ulcorner}{{C^{\prime}}^{\urcorner}}$
for some $B,B^{\prime},C,C^{\prime}$ and there are LF forms $D$ and $E$ such
that
${\vdash_{LF}{D}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{dual}}\;{{}^{\ulcorner}{{B}^{\urcorner}}}\;{{}^{\ulcorner}{{B^{\prime}}^{\urcorner}}}}$
and
${\vdash_{LF}{E}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{dual}}\;{{}^{\ulcorner}{{C}^{\urcorner}}}\;{{}^{\ulcorner}{{C^{\prime}}^{\urcorner}}}}$.
By induction hypothesis, $B^{\prime}=B^{\bot}$ and $C^{\prime}=C^{\bot}$, so
${}^{\ulcorner}{{A}^{\urcorner}}={}^{\ulcorner}{{A^{\bot}}^{\urcorner}}$.

∎

###  B.3. Proof of Lemma 5.4

We first define the encoding ${}^{\ulcorner}{{-}^{\urcorner}}$ and decoding
$\left\lfloor-\right\rfloor$ of processes in SCP as follows. For the encoding,
the idea is to represent all bindings as intuitionistic functions. For the
decoding, the idea is to perform function application on relevant
substructures with freshly bound channels.

$\displaystyle{}^{\ulcorner}{{\mathtt{fwd}\ x\ y}^{\urcorner}}$
$\displaystyle={\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{fwd}}\
x\ y$ $\displaystyle{}^{\ulcorner}{{\nu
x{:}A.(\mathtt{P}\mathbin{\|}\mathtt{Q})}^{\urcorner}}$
$\displaystyle={\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{pcomp}}\
{}^{\ulcorner}{{A}^{\urcorner}}\ (\lambda
x.{}^{\ulcorner}{{\mathtt{P}}^{\urcorner}})(\lambda
x.{}^{\ulcorner}{{\mathtt{Q}}^{\urcorner}})$
$\displaystyle{}^{\ulcorner}{{\mathtt{close}\ x}^{\urcorner}}$
$\displaystyle={\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{close}}\
x$ $\displaystyle{}^{\ulcorner}{{\mathtt{wait}\ x;\ \mathtt{P}}^{\urcorner}}$
$\displaystyle={\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{wait}}\
x\ {}^{\ulcorner}{{\mathtt{P}}^{\urcorner}}$
$\displaystyle{}^{\ulcorner}{{\mathtt{out}\ x;\
(y.\mathtt{P}\mathbin{\|}w.\mathtt{Q})}^{\urcorner}}$
$\displaystyle={\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{out}}\
x\ (\lambda y.{}^{\ulcorner}{{\mathtt{P}}^{\urcorner}})\ (\lambda
w.{}^{\ulcorner}{{\mathtt{Q}}^{\urcorner}})$
$\displaystyle{}^{\ulcorner}{{\mathtt{inp}\ x\ (w.y.\mathtt{P})}^{\urcorner}}$
$\displaystyle={\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{inp}}\
x\ (\lambda w.\lambda y.{}^{\ulcorner}{{\mathtt{P}}^{\urcorner}})$
$\displaystyle{}^{\ulcorner}{{\mathtt{inl}\ x;\ w.\mathtt{P}}^{\urcorner}}$
$\displaystyle={\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{inl}}\
x\ (\lambda w.{}^{\ulcorner}{{\mathtt{P}}^{\urcorner}})$
$\displaystyle{}^{\ulcorner}{{\mathtt{inr}\ x;\ w.\mathtt{P}}^{\urcorner}}$
$\displaystyle={\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{inr}}\
x\ (\lambda w.{}^{\ulcorner}{{\mathtt{P}}^{\urcorner}})$
$\displaystyle{}^{\ulcorner}{{\mathtt{case}\ x\ (w.\mathtt{P},\
w.\mathtt{Q})}^{\urcorner}}$
$\displaystyle={\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{choice}}\
x\ (\lambda w.{}^{\ulcorner}{{\mathtt{P}}^{\urcorner}})\ (\lambda
w.{}^{\ulcorner}{{\mathtt{Q}}^{\urcorner}})$
$\displaystyle\left\lfloor{\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{fwd}}\
x\ y\right\rfloor$ $\displaystyle=\mathtt{fwd}\ x\ y$
$\displaystyle\left\lfloor{\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{pcomp}}\
T\ M\ N\right\rfloor$ $\displaystyle=\nu x{:}\left\lfloor
T\right\rfloor.(\left\lfloor M\;x\right\rfloor\mathbin{\|}\left\lfloor
N\;x\right\rfloor)$
$\displaystyle\left\lfloor{\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{close}}\
x\right\rfloor$ $\displaystyle=\mathtt{close}\ x$
$\displaystyle\left\lfloor{\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{wait}}\
x\ M\right\rfloor$ $\displaystyle=\mathtt{wait}\ x;\ \left\lfloor
M\right\rfloor$
$\displaystyle\left\lfloor{\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{out}}\
x\ M\ N\right\rfloor$ $\displaystyle=\mathtt{out}\ x;\ (y.\left\lfloor
M\;y\right\rfloor\mathbin{\|}w.\left\lfloor N\;w\right\rfloor)$
$\displaystyle\left\lfloor{\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{inp}}\
x\ M\right\rfloor$ $\displaystyle=\mathtt{inp}\ x\ (w.y.\left\lfloor
M\;w\;y\right\rfloor)$
$\displaystyle\left\lfloor{\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{inl}}\
x\ M\right\rfloor$ $\displaystyle=\mathtt{inl}\ x;\ w.\left\lfloor
M\;w\right\rfloor$
$\displaystyle\left\lfloor{\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{inr}}\
x\ M\right\rfloor$ $\displaystyle=\mathtt{inr}\ x;\ w.\left\lfloor
M\;w\right\rfloor$
$\displaystyle\left\lfloor{\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{choice}}\
x\ M\ N\right\rfloor$ $\displaystyle=\mathtt{case}\ x\ (w.\left\lfloor
M\;w\right\rfloor,\ w.\left\lfloor N\;w\right\rfloor)$

###### Lemma B.3 (Adequacy of proc).

For each SCP processes $\mathtt{P}$, there exists a unique canonical LF
derivation
${}^{\ulcorner}{{\operatorname{fn}(\mathtt{P})}^{\urcorner}}\vdash_{LF}{{}^{\ulcorner}{{\mathtt{P}}^{\urcorner}}}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{proc}}$
and
$\left\lfloor{}^{\ulcorner}{{\mathtt{P}}^{\urcorner}}\right\rfloor=\mathtt{P}$.
Conversely, if
$\Gamma\vdash_{LF}{M}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{proc}}$
is a canonical LF derivation, then $\left\lfloor M\right\rfloor$ is an SCP
process, ${}^{\ulcorner}{{\left\lfloor M\right\rfloor}^{\urcorner}}=M$, and
${}^{\ulcorner}{{\operatorname{fn}(\left\lfloor
M\right\rfloor)}^{\urcorner}}\subseteq\Gamma$.

###### Proof.

For the forward direction, by induction on $\mathtt{P}$. We show two cases.
For all cases, uniqueness follows from inspecting constructors to observe that
every process construct in SCP has a corresponding constructor in our
encoding. Left invertibility of ${}^{\ulcorner}{{-}^{\urcorner}}$ follows from
simple computation of each case.

######  Case 1.

$\mathtt{P}=\mathtt{fwd}\ x\ y$
Then $\operatorname{fn}(\mathtt{P})=\\{x,y\\}$, and indeed,
${x}{:}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{name}},{y}{:}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{name}}\vdash_{LF}{{\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{fwd}}\
x\
y}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{proc}}$.

######  Case 2.

$\mathtt{P}=\mathtt{inl}\ x;\ w.\mathtt{P^{\prime}}$
Then
${}^{\ulcorner}{{\mathtt{P}}^{\urcorner}}={\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{inl}}\
x\ (\lambda w.{}^{\ulcorner}{{\mathtt{P^{\prime}}}^{\urcorner}})$. Therefore
${}^{\ulcorner}{{\operatorname{fn}(\mathtt{P^{\prime}})}^{\urcorner}}\vdash_{LF}{{}^{\ulcorner}{{\mathtt{P^{\prime}}}^{\urcorner}}}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{proc}}$
by induction hypothesis. Since
$\operatorname{fn}(\mathtt{P})=(\operatorname{fn}(\mathtt{P^{\prime}})\setminus{w})\cup\\{x\\}$,
we have
${}^{\ulcorner}{{\operatorname{fn}(\mathtt{P})}^{\urcorner}}\vdash_{LF}{{}^{\ulcorner}{{\mathtt{P}}^{\urcorner}}}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{proc}}$
by the LF constructor inl.

For the reverse direction, by induction on the derivation
$\Gamma\vdash_{LF}{M}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{proc}}$.

######  Case 1.

$\Gamma\vdash_{LF}{{\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{fwd}}\
x\
y}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{proc}}$
Then $\left\lfloor M\right\rfloor=\mathtt{fwd}\ x\ y$ and invertibility is
obvious. Moreover,
${x}{:}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{name}}$
and
${y}{:}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{name}}$
must appear in $\Gamma$ since there are no constructors of the LF type name.
Indeed, $\operatorname{fn}(\mathtt{fwd}\ x\
y)=\\{{x}{:}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{name}},{y}{:}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{name}}\\}$
which is a subset of $\Gamma$.

######  Case 2.

$\Gamma\vdash_{LF}{{\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{inl}}\
x\
M^{\prime}}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{proc}}$
Then $\left\lfloor M\right\rfloor=\mathtt{inl}\ x;\ w.\left\lfloor
M^{\prime}\;w\right\rfloor$. For invertibility, we have

$\displaystyle{}^{\ulcorner}{{\left\lfloor{\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{inl}}\
x\ M^{\prime}\right\rfloor}^{\urcorner}}$
$\displaystyle={}^{\ulcorner}{{\mathtt{inl}\ x;\ w.\left\lfloor
M^{\prime}\;w\right\rfloor}^{\urcorner}}$
$\displaystyle={\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{inl}}\
x\ (\lambda w.{}^{\ulcorner}{{\left\lfloor
M^{\prime}\;w\right\rfloor}^{\urcorner}})$
$\displaystyle={\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{inl}}\
x\ (\lambda w.M^{\prime}\;w)$
$\displaystyle={\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{inl}}\
x\ M^{\prime}$

For the context condition, we have
${}^{\ulcorner}{{\operatorname{fn}(\left\lfloor M^{\prime}\
w\right\rfloor)}^{\urcorner}}\subseteq\Gamma,{w}{:}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{name}}$
by induction hypothesis using some fresh
${w}{:}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{name}}$.
Since $\operatorname{fn}(\left\lfloor
M\right\rfloor)=(\operatorname{fn}(\left\lfloor M^{\prime}\
w\right\rfloor)\setminus w)\cup\\{x\\}$, we obtain

${}^{\ulcorner}{{\operatorname{fn}(\left\lfloor
M\right\rfloor}^{\urcorner}}\subseteq\Gamma$

since
${x}{:}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{name}}\in\Gamma$
due to it being used in
${\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{inl}}\
x\ M^{\prime}$.

∎

###  B.4. Proof of Lemma 5.5

###### Lemma B.4 (Adequacy of linear).

For each derivation $\mathcal{D}$ of $\mathsf{lin}(x,\ \mathtt{P})$, there
exists a unique canonical LF derivation
$L={}^{\ulcorner}{{\mathcal{D}}^{\urcorner}}$ such that
${}^{\ulcorner}{{\operatorname{fn}(\mathtt{P})\setminus
x}^{\urcorner}}\vdash_{LF}L:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{linear}}\;\lambda
x.{}^{\ulcorner}{{\mathtt{P}}^{\urcorner}}$ and $\left\lfloor
L\right\rfloor=\mathcal{D}$. Conversely, if
$\Gamma\vdash_{LF}L:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{linear}}\;M$
is a canonical LF derivation, then $\left\lfloor L\right\rfloor$ is a
derivation of $\mathsf{lin}(x,\ \left\lfloor M\ x\right\rfloor)$ and
${}^{\ulcorner}{{\operatorname{fn}(\left\lfloor M\ x\right\rfloor)\setminus
x}^{\urcorner}}\vdash_{LF}{}^{\ulcorner}{{\left\lfloor
L\right\rfloor}^{\urcorner}}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{linear}}\;M$
where ${}^{\ulcorner}{{\operatorname{fn}(\left\lfloor M\
x\right\rfloor)}^{\urcorner}}\subseteq\Gamma$.

###### Proof.

Since there is an exact correspondence between inference rules for the
linearity predicate in SCP and the constructors for the LF type family linear,
we informally case on a few inference rules and prove both directions. The
encodings and decodings are modular, so we present the result of encoding and
decoding as needed in the proof. We omit the verification of the invertibility
statements since they are obvious.

######  Case 1 ($L_{\mathtt{fwd}1}$).

We start with the forward direction. Suppose $\mathcal{D}$ is

$\mathsf{lin}(x,\ \mathtt{fwd}\ x\ y)$

Where
${}^{\ulcorner}{{\mathcal{D}}^{\urcorner}}={\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{l\\_fwd1}}$.
Then indeed,

${}^{\ulcorner}{{\operatorname{fn}(\mathtt{fwd}\ x\ y)\setminus
x}^{\urcorner}}\vdash_{LF}{\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{l\\_fwd1}}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{linear}}\;\lambda
x.{}^{\ulcorner}{{\mathtt{fwd}\ x\ y}^{\urcorner}}$

because ${}^{\ulcorner}{{\mathtt{fwd}\ x\
y}^{\urcorner}}={\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{fwd}}\
x\ y$ and ${}^{\ulcorner}{{\operatorname{fn}(\mathtt{fwd}\ x\ y)\setminus
x}^{\urcorner}}={y}{:}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{name}}$.
The reverse direction uses a similar argument.

######  Case 2 ($L_{\mathtt{inl}}$).

Starting with the forward direction, where $\mathcal{D}$ is

$\mathsf{lin}(x,\ \mathtt{inl}\ x;\ w.\mathtt{P})\mathsf{lin}(w,\
\mathtt{P})&x\notin\operatorname{fn}(\mathtt{P})$

Then
${}^{\ulcorner}{{\mathcal{D}}^{\urcorner}}={\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{l\\_inl}}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{linear}}\
(\lambda
w.{}^{\ulcorner}{{\mathtt{P}}^{\urcorner}})\to{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{linear}}\
(\lambda
x.({\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{inl}}\
x\ \lambda w.{}^{\ulcorner}{{\mathtt{P}}^{\urcorner}})$.
First, we have ${}^{\ulcorner}{{\operatorname{fn}(\mathtt{P})\setminus
w}^{\urcorner}}\vdash_{LF}L:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{linear}}\;\lambda
w.{}^{\ulcorner}{{\mathtt{P}}^{\urcorner}}$ by induction hypothesis, so it
suffices to show

${}^{\ulcorner}{{\operatorname{fn}(\mathtt{inl}\ x;\ w.\mathtt{P})\setminus
x}^{\urcorner}}\vdash_{LF}({\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{l\\_inl}}\
L):{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{linear}}\;\lambda
x.{}^{\ulcorner}{{\mathtt{inl}\ x;\ w.\mathtt{P}}^{\urcorner}}$

First, we observe that ${}^{\ulcorner}{{\mathtt{inl}\ x;\
w.\mathtt{P}}^{\urcorner}}={\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{inl}}\
x\ \lambda w.{}^{\ulcorner}{{\mathtt{P}}^{\urcorner}}$ by definition of
${}^{\ulcorner}{{-}^{\urcorner}}$, so the typing matches. Next, to show that
the context matches, we must show
${}^{\ulcorner}{{\operatorname{fn}(\mathtt{P})\setminus
w}^{\urcorner}}={}^{\ulcorner}{{\operatorname{fn}(\mathtt{inl}\ x;\
w.\mathtt{P})\setminus x}^{\urcorner}}$, which follows from the side condition
$x\notin\operatorname{fn}(\mathtt{P})$.

Consider the converse next where we have an LF derivation of form

$\Gamma\vdash_{LF}({\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{l\\_inl}}\
L):{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{linear}}\
(\lambda
x.({\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{inl}}\
x\ M)$

such that
$\Gamma\vdash_{LF}L:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{linear}}\
M$.
Then by induction hypothesis, we have $\left\lfloor L\right\rfloor$ is a
derivation of $\mathsf{lin}(w,\ \left\lfloor M\ w\right\rfloor)$. Furthermore,
$M$ cannot depend on $x$ since it is a metavariable and therefore must be
independent of the internally bound $x$. Therefore,
$x\notin\operatorname{fn}(\left\lfloor M\ w\right\rfloor)$. And therefore, we
can apply $L_{\mathtt{inl}}$.

∎

###  B.5. Proof of Lemma 5.7

###### Lemma B.5 (Adequacy of wtp).

There exists a bijection between typing derivations in SCP of form
$\mathtt{P}\Vdash\Gamma$ and LF canonical forms $D$ such that
${}^{\ulcorner}{{\Gamma}^{\urcorner}}\vdash_{LF}{D}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{wtp}}\;{}^{\ulcorner}{{\mathtt{P}}^{\urcorner}}$

###### Proof.

Just like in the proof sketch for adequacy on linearity, we informally case on
a few typing rules and prove both directions since there is an exact
correspondence between typing rules in SCP and the constructors for the LF
type family wtp. The encodings and decodings are modular, so we informally
present the result of encoding and decoding as needed in the proof. We omit
verifying invertibility statements since they are obvious.

######  Case 1 ([Id]).

$\mathtt{fwd}\ x\ y\Vdash\Gamma,x:A,y:A^{\bot}$

This rule corresponds to
wtp_fwd : dual T T’ $\rightarrow$ {X:name}hyp X T $\rightarrow$ {Y:name}hyp Y
T’ $\rightarrow$ wtp (fwd X Y).
By Lemma 5.2, we have a unique derivation
$\vdash_{LF}{D}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{dual}}\;{{}^{\ulcorner}{{A}^{\urcorner}}}\;{{}^{\ulcorner}{{A^{\bot}}^{\urcorner}}}$,
so we set $A=T$ and $A^{\bot}=T^{\prime}$. By expanding the context encoding,
${}^{\ulcorner}{{\Gamma,x{:}A,y{:}A^{\bot}}^{\urcorner}}={}^{\ulcorner}{{\Gamma}^{\urcorner}},{x}{:}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{name}},{hx}{:}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{hyp}}\
{x}\
{}^{\ulcorner}{{A}^{\urcorner}},{y}{:}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{name}},{hy}{:}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{hyp}}\
{y}\ {}^{\ulcorner}{{A^{\bot}}^{\urcorner}}$, allowing usage of wtp_fwd.
We use a similar argument for the reverse direction, in particular, we apply
Lemma 5.2 to infer $A^{\prime}=A^{\bot}$ from
$\vdash_{LF}{D}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{dual}}\;{{}^{\ulcorner}{{A}^{\urcorner}}}\;{{}^{\ulcorner}{{A^{\prime}}^{\urcorner}}}$.
We then prove that the decoding of the LF context yields a context of form
$\Gamma,x{:}A,y{:}A^{\prime}$ with $A^{\prime}=A^{\bot}$.

######  Case 2 ([Cut]).

$\nu
x{:}A.(\mathtt{P}\mathbin{\|}\mathtt{Q})\Vdash\Gamma\mathtt{P}\Vdash\Gamma,x:A&\mathsf{lin}(x,\
\mathtt{P})\mathtt{Q}\Vdash\Gamma,x:A^{\bot}\mathsf{lin}(x,\ \mathtt{Q})$

This rule corresponds to

⬇

wtp_pcomp : dual T T’ $\rightarrow$ ({x:name} hyp x T $\rightarrow$ wtp (M x))
$\rightarrow$ ({x:name} hyp x T’ $\rightarrow$ wtp (N x))

$\rightarrow$ linear M $\rightarrow$ linear N

$\rightarrow$ wtp (pcomp T M N)

First, ${}^{\ulcorner}{{A}^{\urcorner}}=T$ and
${}^{\ulcorner}{{A^{\bot}}^{\urcorner}}=T^{\prime}$ by Lemma 5.2. By induction
hypothesis, we have unique derivations
${}^{\ulcorner}{{\Gamma,x{:}A}^{\urcorner}}\vdash_{LF}{\mathcal{D}_{1}}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{wtp}}\;{}^{\ulcorner}{{\mathtt{P}}^{\urcorner}}$
and
${}^{\ulcorner}{{\Gamma,x{:}A^{\bot}}^{\urcorner}}\vdash_{LF}{\mathcal{D}_{2}}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{wtp}}\;{}^{\ulcorner}{{\mathtt{Q}}^{\urcorner}}$.
The linearity predicates follow from Lemma 5.5. For example, we can encode the
derivation of the predicate $\mathsf{lin}(x,\ \mathtt{P})$ to some $L$ such
that ${}^{\ulcorner}{{\operatorname{fn}(\mathtt{P})\setminus
x}^{\urcorner}}\vdash_{LF}L:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{linear}}\;\lambda
x.{}^{\ulcorner}{{\mathtt{P}}^{\urcorner}}$. Moreover,
${}^{\ulcorner}{{\operatorname{fn}(\mathtt{P})}^{\urcorner}}\subseteq{}^{\ulcorner}{{\Gamma}^{\urcorner}}$,
so by weakening, we have
${{}^{\ulcorner}{{\Gamma}^{\urcorner}}\vdash_{LF}L:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{linear}}\;\lambda
x.{}^{\ulcorner}{{\mathtt{P}}^{\urcorner}}}$. We apply the same reasoning to
obtain the corresponding derivation to $\mathsf{lin}(x,\ \mathtt{Q})$, thereby
enabling use of wtp_pcomp as desired.
For the reverse direction, we have a derivation

$\Gamma\vdash_{LF}{{\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{wtp\\_pcomp}}\
D\ \mathcal{D}_{1}\ \mathcal{D}_{2}\ \mathcal{L}_{1}\
\mathcal{L}_{2}}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{wtp}}\;{\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{pcomp}}\
T\ M\ N$

where:

$\displaystyle\vdash_{LF}{D}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{dual}}\;{T}\;{T^{\prime}}$
$\displaystyle\Gamma\vdash_{LF}{\mathcal{D}_{1}}:(\\{{x}{:}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{name}}\\}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{hyp}}\
{x}\
{T}\to{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{wtp}}\;M\
x)$
$\displaystyle\Gamma\vdash_{LF}{\mathcal{D}_{2}}:(\\{{x}{:}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{name}}\\}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{hyp}}\
{x}\
{T^{\prime}}\to{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{wtp}}\;N\
x)$
$\displaystyle\Gamma\vdash_{LF}\mathcal{L}_{1}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{linear}}\;M$
$\displaystyle\Gamma\vdash_{LF}\mathcal{L}_{2}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{linear}}\;N$

First, we let $A=\left\lfloor T\right\rfloor$, or
${}^{\ulcorner}{{A}^{\urcorner}}=T$, and by Lemma 5.2,
${}^{\ulcorner}{{A^{\bot}}^{\urcorner}}=T^{\prime}$. We also obtain two
derivations of wtp by extending the context on $\mathcal{D}_{1}$ and
$\mathcal{D}_{2}$:

$\displaystyle\Gamma,{x}{:}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{name}},{h}{:}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{hyp}}\
{x}\ {}^{\ulcorner}{{A}^{\urcorner}}\vdash_{LF}{(\mathcal{D}_{1}\ x\
h)}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{wtp}}\;M\
x$
$\displaystyle\Gamma,{x}{:}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{name}},{h}{:}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathtt{hyp}}\
{x}\ {}^{\ulcorner}{{A^{\bot}}^{\urcorner}}\vdash_{LF}{(\mathcal{D}_{2}\ x\
h)}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{wtp}}\;N\
x$

By induction hypotheses on $(\mathcal{D}_{1}\ x\ h)$ and $(\mathcal{D}_{2}\ x\
h)$, we obtain two SCP type derivations.

$\left\lfloor M\ x\right\rfloor\Vdash\Delta,x{:}A\quad\left\lfloor N\
x\right\rfloor\Vdash\Delta,x{:}A^{\bot}$

where $\Delta$ is an SCP typing context such that
${}^{\ulcorner}{{\Delta}^{\urcorner}}=\Gamma$.

Next, by Lemma 5.5 on $\mathcal{L}_{1}$ and $\mathcal{L}_{2}$, we obtain two
SCP linear predicates:

$\mathsf{lin}(x,\ \left\lfloor M\ x\right\rfloor)\quad\mathsf{lin}(x,\
\left\lfloor N\ x\right\rfloor)$

And finally, we apply [Cut]:

$\nu x{:}A.(\left\lfloor M\ x\right\rfloor\mathbin{\|}\left\lfloor N\
x\right\rfloor)\Vdash\Gamma\lx@proof@logical@and\left\lfloor M\
x\right\rfloor\Vdash\Gamma,x{:}A\mathsf{lin}(x,\ \left\lfloor M\
x\right\rfloor)\left\lfloor N\
x\right\rfloor\Vdash\Gamma,x{:}A^{\bot}\mathsf{lin}(x,\ \left\lfloor N\
x\right\rfloor)$

Finally, we verify that
${}^{\ulcorner}{{{\color[rgb]{0.775,0.1,0.325}\definecolor[named]{pgfstrokecolor}{rgb}{0.775,0.1,0.325}\mathtt{pcomp}}\
T\ M\ N}^{\urcorner}}=\nu x{:}A.(\left\lfloor M\
x\right\rfloor\mathbin{\|}\left\lfloor N\ x\right\rfloor)$.

∎

###  B.6. Proof of Lemma 5.8 and Lemma 5.9

###### Lemma B.6 (Adequacy of step).

For each SCP reduction $S$ of $\mathtt{P}\Rightarrow_{SCP}\mathtt{Q}$, there
exists a unique canonical LF derivation
${}^{\ulcorner}{{\operatorname{fn}(\mathtt{P})}^{\urcorner}}\vdash_{LF}{D}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{step}}\;{}^{\ulcorner}{{\mathtt{P}}^{\urcorner}}\;{}^{\ulcorner}{{\mathtt{Q}}^{\urcorner}}$
and $\left\lfloor{}^{\ulcorner}{{S}^{\urcorner}}\right\rfloor=S$. Conversely,
if
$\Gamma\vdash_{LF}{D}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{step}}\;M\;N$
is a canonical LF derivation, then $\left\lfloor D\right\rfloor$ is a
derivation of a reduction $\left\lfloor
M\right\rfloor\Rightarrow_{SCP}\left\lfloor N\right\rfloor$,
${}^{\ulcorner}{{\left\lfloor D\right\rfloor}^{\urcorner}}=D$, and
${}^{\ulcorner}{{\operatorname{fn}(\left\lfloor
M\right\rfloor)}^{\urcorner}}\subseteq\Gamma$.

###### Lemma B.7 (Adequacy of equiv).

For each SCP structural equivalence $S$ of $\mathtt{P}\equiv\mathtt{Q}$, there
exists a unique canonical LF derivation
${}^{\ulcorner}{{\operatorname{fn}(\mathtt{P})}^{\urcorner}}\vdash_{LF}{D}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{equiv}}\;{}^{\ulcorner}{{\mathtt{P}}^{\urcorner}}\;{}^{\ulcorner}{{\mathtt{Q}}^{\urcorner}}$
and $\left\lfloor{}^{\ulcorner}{{S}^{\urcorner}}\right\rfloor=S$. Conversely,
if
$\Gamma\vdash_{LF}{D}:{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\mathrm{equiv}}\;M\;N$
is a canonical LF derivation, then $\left\lfloor D\right\rfloor$ is a
derivation of a reduction $\left\lfloor M\right\rfloor\equiv\left\lfloor
N\right\rfloor$, ${}^{\ulcorner}{{\left\lfloor
D\right\rfloor}^{\urcorner}}=D$, and
${}^{\ulcorner}{{\operatorname{fn}(\left\lfloor
M\right\rfloor)}^{\urcorner}}\subseteq\Gamma$.

###### Proof.

Both are easy to prove. For both directions, all axiom cases can be shown by
appealing to Lemma 5.4 on both $\mathtt{P}$ and $\mathtt{Q}$ (or $M$ and $N$
for the reverse direction). The two congruence cases in step for pcomp is a
straightforward application of the induction hypothesis. ∎


# MRxaI: Black-Box Explainability for Image Classifiers
in a Medical Setting

Nathan Blake, Hana Chockler, David A. Kelly,
Santiago Calderón Peña, Akchunya Chanchal
Department of Informatics,
King’s College London
nathan.blake, hana.chockler, david.a.kelly,
santiago.calderon, akchunya.chanchal AT kcl.ac.uk

###### Abstract

Existing tools for explaining the output of image classifiers can be divided
into white-box, which rely on access to the model internals, and black-box,
agnostic to the model. As the usage of AI in the medical domain grows, so too
does the usage of explainability tools. Existing work on medical image
explanations focuses on white-box tools, such as grad-cam. However, there are
clear advantages to switching to a black-box tool, including the ability to
use it with any classifier and the wide selection of black-box tools
available. On standard images, black-box tools are as precise as white-box. In
this paper we compare the performance of several black-box methods against
grad-cam on a brain cancer MRI dataset. We demonstrate that most black-box
tools are not suitable for explaining medical image classifications and
present a detailed analysis of the reasons for their shortcomings. We also
show that one black-box tool, a causal explainability-based rex, performs as
well as grad-cam.

##  1 Introduction

Machine learning (ML) for classification in the medical domain is facing what
has been described as a “reproducibility crisis”. It is characterized by a
model’s published performance failing to generalize to the clinical setting,
even when deployed in ostensibly the same setting [20, 23, 40]. Hence,
reported state-of-the-art performance is often not reproducible. For instance,
a recent systematic review of ML applied to diagnosing COVID with radiographs
found that out of $62$ studies, none were clinically relevant [30]. Even in
more established diagnostic pathways, such as neuroimaging for intracranial
hemorrhage, very few clinically relevant models exist out of thousands of
developed models [2].

There are several factors contributing to this phenomenon. Exceptional
performance is often achieved on highly curated benchmark datasets. While
these have utility for model development, they are rarely representative of
data from real clinical environments [39]. Such benchmark datasets are often
small, relative to the large datasets used in deep learning (DL), typically of
the order of hundreds of patients. This is compounded by the fact that medical
data is complex and hierarchically structured. For instance, MRI images taken
with a single MRI machine may learn to distinguish instrumental rather than
clinical features [27]. Even when trained upon numerous MRI machines, the
imaging protocol can influence downstream learning [10]. Even racial
structures in datasets have been observed to contribute to a lack of
generalizability in various disease classification tasks [28].

If such factors are not carefully considered, the resultant models fail to
learn the relevant features and do not generalize. This ’dataset’ or
’distributional’ shift can result in models with high published evaluation
metrics which fail to apply to the clinical setting. To counter this potential
misuse of ML, the use of counterfactual reasoning to distinguish correlation
from causation is growing in popularity [40].

Interest in explainability tools for medical applications has rapidly grown
recently [6] as clinicians seek trustworthy models to assist with various
medical tasks, notably including imaging tasks. To this end, there are calls
for explainable AI (XAI) to check the fidelity of medical classifiers [28,
27]. By highlighting which features a classifier has learnt to utilize, the
XAI algorithm could assess whether the classifier has been over-fit to learn
spurious features. This would provide a post-processing quality control step
to check that the classifier is indeed highlighting clinically relevant
features.

We assessed several popular XAI tools applied to a model developed to detect
the presence of brain tumor in MRI images. This is the first paper to
explicitly compare a suite of black-box XAI tools in a strictly medical
imaging context, comparing performance to a white-box standard, grad-cam.

Detailed experimental results, including the datasets and evaluation, are
submitted as a part of the supplementary material.

##  2 Background

The most commonly used XAI tools in medical diagnostic imaging are Gradient-
weighted Class Activation Mapping (grad-cam) [33], Local Interpretable Model-
agnostic Explanations (lime) [29] and SHapley Additive exPlanations (shap)
[22]. Randomized Input Sampling for Explanation (rise) is less popular in the
medical literature but has attractive features, discussed below, making it
worth considering.

grad-cam works in CNNs by using the gradients of a target class (e.g. a
disease type) flowing into the final convolutional layer to produce a salience
map of important regions. grad-cam is the most commonly used XAI tool for
medical imaging applications [17, 38, 6]. However, it has been shown to be
fragile in the sense that two imperceptibly different images with the same
label can give very different explanations [15]. It has also been found
unsuitable for medical applications using certain DL architectures. For
instance, in a brain MRI task the final convolutional layer of a DenseNet
model was too small ($3\times 3\times 3$) to be clinically useful when
upscaled to the full image size ($120\times 120\times 120$) [41].

A large disadvantage of any white-box method is the necessity of having access
to the internals of the model. This may not be available depending upon the
nature of various healthcare and commercial collaborations, and even between
purely academic teams there may be a reluctance to share. This would only
exacerbate the reproducibility crisis, where the explanations for a given
model are not amenable to verification. Thus black-box XAI tools have a
critical role in the verification of medical models. The following XAI tools
are all model-agnostic.

lime, in the context of images, works by perturbing images from which
predictions are obtained. These are then used to train a simpler model (often
linear), from which the feature weights are extracted to build a map of their
importance. The default perturbation used in lime is to replace a pixel with
the mean segment pixel intensity. Several medical researchers have used lime
for explaining DL models [29].

shap uses Shapley values, from game theory, to determine the marginal
contribution of every feature (superpixels) to the model output [22]. Although
generally popular, it is less commonly used for medical image explanations,
perhaps due to its computational cost [38]. To calculate the exact Shapley
values would require $2^{F}$ mutants, where $F$ is the total number of pixels.
To find solutions in polynomial time, it leverages Owen values, trading
accuracy for speed.

rise computes the importance of each pixel by applying binary masks over an
image [26]. These masks are then upsampled using bi-linear interpolation,
which seeks to avoid sharp edges for a smooth saliency map. During
interpolation these upsampled masks do not remain binary but take values in
$[0,1]$. The resulting mask is applied to the model to obtain a confidence
score. Thus, the importance of each pixel is quantified based on the expected
confidence score over all possible masks in which the pixel is observed.

The XAI tools described above, and indeed many similar tools, occlude, or
otherwise perturb, various pixels in an input image to determine the
difference such perturbations make on its classification. The nature of the
perturbations might include setting pixel values to zero or the mean pixel
value, with or without blurring at the edges. The strategy by which perturbed
pixels are selected may impact explanations, and can, for instance, manifest
in particularly rectilinear, and quite unnatural, explanations. Some of these
will be impacted by the selection of tool parameters while others will be
implicit in the nature of the XAI tool itself. These considerations are likely
exacerbated by the relative homogeneity of medical images compared to normal
image classification: the difference between a sub-species of dogs is larger
than between sub-types of cancer, and so the latter may be more sensitive to
the nature of XAI tool perturbations (and their associated parameters). Most
XAI tools have a number of parameters, whether implicit or explicitly
declared. Though default settings exist, these are rarely optimised for use in
medical images, and their selection is non-trivial, especially for clinical
end-users. Hence it is desirable for an XAI tool to have few, if any,
parameters which require fine-tuning, or to default those parameters to domain
specific values [38].

A desirable trait for an XAI tool is to move beyond correlation and provide
explanations that incorporate causal relationships [37]. Tools, which account
for such relationships, allow insights into potential biases which can then be
removed [35]. Causal Responsibility eXplanations (rex) [9] is an XAI tool
based on causal reasoning [18].

rex constructs an approximation of a causal explanation [19, 18] by first
ranking the pixels of a given image according to their importance for the
classification, and then constructing an explanation greedily from the
saliency landscape of the pixels. The ranking is an approximate degree of
responsibility [8], computed on the coarsely partitioned image, and updated by
refining the areas of the input with high responsibility, until a sufficiently
fine partition is reached. To compute the degree of responsibility, rex
generates mutants (images with some parts masked) and queries the classifier
on these mutants. If a non-masked area is sufficient to get the same
classification as the original image, it is a cause for the classification,
with the degree of responsibility of each part based on the number of parts in
the area.

##  3 Models, Methods and Measures

We investigated the performance of several image-based XAI tools on low
diversity medical data. XAI tools are frequently trained on standard datasets,
such as ImageNet [31]. These images exhibit a relatively high degree of
diversity, so that a dog, for example, may appear against many different
backgrounds, in different sections of the image. MRI images almost completely
lack this diversity, with brains at consistent locations, sizes and pixel
densities. Occlusion techniques and defaults developed for models trained on
diverse data may be inappropriate for models trained on low diversity data.
The model may be overly sensitive to occlusions, or fail entirely.

###  3.1 Model and dataset

The model is a pre-trained CNN based on the ResNet 50 architecture [21]. Brain
magnetic resonance imaging (MRI) data was obtained from The Cancer Imaging
Archive, as published by Buda et al. [5], and made publicly available on
kaggle [4]. This curated dataset of $110$ pre-operative patients with low
grade gliomas (LGG) was gathered from five US institutions. All of the images
are axial slices of the brain and include fluid-attenuated-inversion recovery
(FLAIR) sequence, while $101$ also have pre-contrast sequence and $104$ have
post-contrast sequence patient images. Each patient had between $20$ and $88$
slices taken, with a total of $3,929$ images. Each image contains $3$
channels, one for each of the three sequences. All images are $256\times
256\times 3$. A radiologist annotate the FLAIR images into binary masks of
“tumor” or “no tumor”. This provides a measure of the ground truth, or Human-
Provided Explanation (_HPE_), by which to quantify the performance of the XAI
tools.

As there is no clear definition of an explanation of a negative
classification, we have retained only the positive (diseased) images for
assessment, leaving $1370$ images. Of these $1370$, $118$, $\approx 9\%$ of
the data, are false negatives, where the model reports no tumor, even though
the _HPE_ indicates tumor. As the goal is to explain positive classifications,
we also exclude the false negatives. The failure modes of each tool are
interesting in and of themselves and merit further study.

This is not a clinically motivated task, but one designed to establish the
validity of XAI tools in a medical imaging context, based on the assumption
that diagnostically significant features coincide with the _HPE_. This may not
be strictly true, as, for instance, tumors present in a brain may distort the
ventricles distal to a tumor and so even though a tumor may not be present in
a given MRI slice, clinical features may still be present. However, as the CNN
was trained on MRI slices as opposed to whole 3D images, the classifier was
forced to ignore such features and focus on what distinguishes the slices: the
increased signal intensity of pixels containing tumor.

###  3.2 Quantifying explainability performance

Very few studies of XAI tools in the medical domain have been subject to
clinical scrutiny [17]. In part this is due to success criteria for
explanations being more subjective than standard measures of classifier
performance such as ROC analysis [38]. Ultimately, the ’best’ measure of XAI
performance is task specific. One method is to allow clinicians to assess XAI
outputs, judging their usefulness on whatever criteria they deem most
appropriate. However, this is not without its own limitations, as humans are
prone to biases, such as using XAI to confirm existing beliefs and decreased
vigilance of AI systems [13]. In addition, this method requires copious
amounts of clinician input, which is a scarce resource. Therefore we utilise a
clinically annotated segmentation (_HPE_) as a baseline for XAI performance.

All XAI tools tested provide explanations in the sense that the pixels
indicated by the tool are sufficient to generate a positive classification by
the model. It is categorically not the case, however, that each explanation is
equally good. We assess tool output against human expectation via comparison
with the _HPE_. Our measure, detailed in Sec. 3.2.1, allows us to grade tool
explanations against the _HPE_ and therefore provide a ranking of tools by
human explanation fidelity. The underlying assumption of this procedure is
that a better explanation is one that better coincides with an explanation
provided by a clinician.

####  3.2.1 Penalised Dice Coefficient (PDC)

Even with a clinical _HPE_ against which to compare XAI outputs, there are
many ways to construct a measure of performance. The Sørensen–Dice coefficient
(_DC_) is one such statistic, used to gauge the similarity of any two samples
[11, 34]. It is a common metric to assess the similarity of medical images in
segmentation tasks, where one image is the result of a segmentation model and
the other is a ‘ground-truth’ mask, such as a _HPE_. Given two sets of pixels
$X$ and $Y$, we have

$DC=\frac{2\mid X\cap Y\mid}{\mid X\mid+\mid Y\mid.}$ (1)

Unfortunately _DC_ does not account for the distance between an explanation
and the _HPE_ , nor the size or the number of explanation segments. These are
important as the farther an explanation is from the _HPE_ , the less
clinically useful it is. Similarly, an explanation that is too large can
distract attention, and one too small can lead to missing clinical
information. An explanation erroneously consisting of multiple non-contiguous
areas is also distracting. We therefore define a new measure, the _Penalized
Dice Coefficient (_PDC_)_. It captures the difference between the _HPE_ and a
given explanation, $exp$, taking the comparative areas, the distance between
the areas, and the number of areas as follows. The function $E$ is the
standard euclidean distance, measured between the centers of the _HPE_ and
$exp$, normalized against the maximum possible distance from the center of the
_HPE_ ($E_{max}$), captured as $d=1-E/E_{max}$; $d=0$ means that the centers
are in the same location, and $d=1$ that the centers are maximally far from
each other.

We also calculate the ratio between the _HPE_ area and $exp$ area. As we
require the _PDC_ to always be in the range $(0,1)$ for easy comparison, we
define the ratio $r$ as:

$r=\begin{cases}s\frac{exp_{\text{size}}}{\emph{HPE}_{\text{size}}}&\text{if
}exp_{\text{size}}<\emph{HPE}_{\text{size}}\\\
b\frac{\emph{HPE}_{\text{size}}}{exp_{\text{size}}}&\text{if
}\emph{HPE}_{\text{size}}<exp_{\text{size}}\\\ 1&\text{if
}exp_{\text{size}}=\emph{HPE}_{\text{size}}\end{cases}$ (2)

where $s$ and $b$ are parameters, between $(0,1)$, which allow users to define
how much they wish to penalise against explanations that are too small or too
big, respectively. The ratio $r$ is thus bounded in the range $(0,1)$.

We combine the distance and area ratio with the _DC_ (the latter ensuring that
explanations which overlap with the _HPE_ score higher than non-overlapping
explanations) to form the summary statistic of the _PDC_ :

$\emph{PDC}=\frac{d+r+DC}{3}$ (3)

As each component $d$, $r$ and _DC_ is in $[0,1]$, the _PDC_ is also in this
range. 1 indicates a perfect alignment of the _HPE_ and explanation area and 0
indicates an empty explanation. Unlike the _DC_ , which simply returns $0$ if
two masks do not overlap to any degree, the _PDC_ is always a strictly
positive number, unless no explanation is provided at all, but approaches $0$
as the different penalties for size and location come into effect.

In many cases XAI tools give an explanation with multiple non-contiguous
areas. In this case the _PDC_ for a single explanation mask is given as the
mean of all non-contiguous areas. We also report the number of non-contiguous
areas found in the explanations.

###  3.3 Comparing tools output

Unfortunately, the different XAI tools do not produce outputs which are
directly comparable or immediately amenable to the _DC_ or _PDC_. Both lime
and rex provide boolean-valued masks in addition to heatmaps. Comparing these
masks is much easier than comparing heatmaps. We use these masks directly when
comparing against _HPE_.

shap, rise and grad-cam do not provide these masks directly, so we need to
extract them from the heatmaps. We do this via a method similar to that used
by rex to produce its minimal passing explanations. We choose those pixels
which are most highly ranking in the heatmap and query the model on these
pixels only. If this satisfies the classification requirement, we quit there,
otherwise we add in the next set of pixels and so on until we have the
necessary classification. This gives us a direct assessment over the quality
of the heatmap.

We then extract the _DC_ , _PDC_ and number of non-contiguous areas (count) of
every positively labelled image, using each XAI tool.

grad-cam is unique amongst the XAI tools under consideration in this paper in
that it is the only white-box method. Having direct access to the model
weights should theoretically confer it a significant advantage, given that the
setting is not adversarial. Hence, it serves as the gold-standard by which to
compare the black-box XAI tools.

##  4 Results

We evaluated the XAI tools against the _HPE_ (Human-Provided Explanation)
using our _PDC_. We also inspected tool performance in order to understand why
they succeed or fail. None of the XAI tools have been optimized for this
particular task. Such an optimization for every tool would be impractical.
Moreover, parameter fine-tuning suggests prior knowledge on the part of the
user as to appropriate values. We wished to determine the effectiveness of a
tool without such knowledge. We proceeded with the most parsimonious case of
using each tool’s default parameters, except for the number of mutants
generated which was set at 2000. In the case of rex, there is no default
distribution to decide partitioning, so we default to uniform as the least
informative.

Given size penalization parameters $b=s=1.0$ (not additionally penalizing
explanations that are too large or too small) we present the relative
performance of each tool in Tab. 1 and Fig. 1 and 2.

Tool | Count | _DC_ | _PDC_
---|---|---|---
lime | 2.41 ± 1.95 | 0.16 ± 0.16 | 0.28 ± 0.17
rise | 2.64 ± 3.43 | 0.10 ± 0.12 | 0.33 ± 0.13
shap | 11.96 ± 13.21 | 0.27 ± 0.14 | 0.33 ± 0.08
grad-cam | 9.08 ± 13.37 | 0.33 ± 0.22 | 0.41 ± 0.2
rex | 1.45 ± 1.01 | 0.42 ± 0.2 | 0.55 ± 0.16
Table 1: Mean performance ± 1 standard deviation for all five XAI tools
assessed by three measures. Count refers to the number of non-contiguous areas
returned by a tool. Best performance per measure in bold. The best value for
all parameters would be $1$.

Across all three measures of performance, rex is the best performing tool,
exceeding even grad-cam, which is generally the next best performing tool. The
remaining XAI tools have comparable performance as measured by _PDC_ , though
differences manifest in the $DC$ and count, with rise performing particularly
poorly as measured by $DC$ and shap as measured by count.

For the purposes of visualization we show four rows of results corresponding
to the worst, median, mean and best rex _PDC_ respectively in Fig. 3.

Figure 1: Box and whisker plots for the XAI tools as assessed by _PDC_ (left
panel) and $DC$ (right). Each box delineates the interquartile range (IQR),
with the top and bottom edges representing the 75th (Q3) and 25th (Q1)
percentiles, respectively. The horizontal line inside the box indicates the
median. Whiskers extend to the most extreme data point which is no more than
1.5 times the IQR away from the box. Points outside the whiskers are
considered outliers and are represented as circles. Figure 2: Box and whisker
plot of the count of non-contiguous regions given by each XAI tool Figure 3: A
selection of XAI outputs for images representing, from top row to bottom row,
the worst, median, mean, and best performing rex results as measured by _PDC_.
All tools give differently formatted outputs, these have been homogenized for
ease of comparison. Gray background shows the underlying MRI, pink patches
show the tumor as defined by _HPE_ and the blue regions are the tools’
respective explanations.

###  4.1 Tool analysis

In this section we inspect the explanations provided by the XAI tools, and
investigate their performance and their failures modes.

grad-cam is the only white-box XAI tool we investigated, grad-cam is the
second best performing tool except by count, in which it performs poorly. This
divergence is explained by the fact that although grad-cam can localise well
to the tumor, it also often includes unassociated regions of the head (though
it seldom shows areas outside of the head, which helps imbue trust with
clinicians), as demonstrated in Fig. 4(a). These partitionings tend to
separate the brain and the skull (called the subarachnoid space), sometimes
containing multiple small ’islands’, which increases the count of non-
contiguous areas. This separation is perhaps related to a similar phenomenon
observed in brain imaging of explanations localising to eyeballs – the sharp
gradients of such anatomical features confuse the model as sharp gradients are
also a common feature of tumors.

From a qualitative perspective, even though grad-cam has a tendency to return
multiple areas of explanation, these areas are often contained within a
region. This would draw a clinicians eye to a single region (see top row of
Fig. 3), thus the grad-cam count score is not as bad as first appears.

As grad-cam does not iteratively query the model, unlike black box XAI tools,
it is comparatively fast. Speed has been cited as a critical for clinical
applications [6]. However, the necessity for speed varies greatly by the
nature of the clinical task. In intra-operative applications every second
waiting for results could extend the length of surgery. For screening and
triaging tasks, results could be expected to take hours, days and even weeks.
Hence, slower methods could have utility, especially if they demonstrate
superiority.

rise creates random rectangular masks which it overlays on an image. The
number and size are controlled by parameters. We generate $2,000$ mutants, in
keeping with the average amount of work performed by rex. We set the other
parameters to their default values. It is the least complex of the black-box
tools we investigated, and is the median performer in terms of _PDC_ and
count. However, the _DC_ values for rise are the worst. The tool has a
tendency of returning explanations at the front of the brain or explanations
that fill the majority of the image ( Fig. 4(b)). To examine this, we
calculated the average dice coefficient of the random masks produced by rise
against a mask containing the front region of the head. As we used the same
seed for all experiments, the mask production is the same for all images. The
average _DC_ of $0.002$ indicates that occlusions almost never covered these
areas, hence their over-representation in passing mutants.

There were no duplicates in the mutants produced by rise with our chosen seed.
The area a mutant covers with our parameters is approximately $10\%$ of the
image. As the model is overly generous in what it accepts, the mutants that
rise produces do not cover enough of the image to force failing cases. Passing
cases constitute $77\%$ of the mutants on our dataset. It has been long known
in the testing community that a balance of passing and failing cases in
required for a good-quality output [1] and it is also the reason for
outputting wrong regions of the image as the explanation here. The result is a
heatmap which is too hot in general. The concentration of explanations towards
the front of the head is due to the particular set of mutants generated. This
would likely change given a different random seed.

lime is unique amongst the XAI tools we tested in that it uses a segmentation
algorithm, rather than rectilinear partitioning, to generate occluded mutants
(Fig. 4(c)). The resulting segments are generally larger than pertinent to
neuro-anatomical features. Nor are they anatomically meaningful, though this
could be achieved by segmentation algorithms dedicated to brain images [14].
In our dataset, there was an average of $40$ segments per image. The
probability of mutants sharing at least one segment approaches $1$ after just
$19$ mutants. As lime with default parameters generates $1,000$ mutants, the
best case scenario is that there exists a subset of $\approx 25$ mutants that
share a segment. In practice, this is likely to be much higher.

Further, the default use of the mean segment value to generate mutants is not
clinically meaningful. These result in mutants which are not diverse, likely a
consequence of the relative homogeneity of MRI images compared to standard
images for which lime was developed. Additionally, as has been noted in the
context of histopathological images [16], lime is non-deterministic: given the
same image and random seed it can produce different explanations. This is an
undesirable trait, especially in a medical context in which consistency is
paramount.

shap is computationally expensive to run. It is the lowest performing in terms
of count, on average returning $12$ non-contiguous regions. As seen in Fig.
4(d) these areas tend to be distant from each other and from the _HPE_. This
is ameliorated by the fact that amongst these many areas is the tumor, hence
its _DC_ and _PDC_ are commensurate with the other tools. However, from a
clinical perspective having so many disparate areas in an explanation is
highly undesirable, as each area requires clinical scrutiny for confirmation.

The computation of Shapley values requires considering all possible mutants to
quantify the contribution of each pixel. To avoid this computational overhead,
shap relies on Owen values to estimate the contribution of a collection of
pixels, which is a valid approximation of Shapley values [24]. As a
consequence, the granularity of the explanations is constrained by the minimal
grouping of pixels utilized.

Additionally, prior research has demonstrated that reliance on a single
iteration can introduce bias into the explanations [7]. In the context of this
experiment, this bias manifests in the form of certain images consistently
yielding explanations that are invariably 0 throughout the whole image, where
no mutant was able to induce a change in the image’s classification. shap
requires the specification of a blur window in order to generate mutants of
images. A small scale investigation suggested to us that there was no one
ideal value for this setting. We utilized a $64\times 64$ window in our final
experiments, noting that different window sizes can produce different,
including empty, results.

rex is the best performing XAI tool by all measures. It is comparatively fast,
in the order of seconds, due to its dynamic mutant generation which stops when
no new mutants increase the measure of causal responsibility. Its explanations
usually coincide with the tumor to at least some extent, thus producing a
higher _DC_ and _PDC_ relative to the other tools. Additionally, it seldom
returns spurious explanations with multiple areas, resulting in a low count.
However, as with other tools, it is not immune to the effect of the model
treating eyeballs as signs of cancer.

It is perhaps surprising that rex outperforms grad-cam, but on this particular
task it is highly likely that the model is suboptimal, despite a high test
accuracy ($\approx 91\%$). This is a very common feature of deep learning
models in a medical context [20, 23, 40]. As grad-cam is a white-box method,
it is more sensitive to over-fitting accrued in the training process [15], and
is likely to improve significantly on a thoroughly curated and validated
dataset and model.

We occasionally see straight edges in rex explanations (Fig. 4(e)). Straight
edges are extremely unlikely in any natural phenomenon, including tumors.
Their presence is explained by the effect of the spatial search algorithm.
This places a square box centered over the region of highest responsibility.
This square may grow, contract or move until an explanation is found. As this
square is initially placed over the pixels of highest responsibility, this
procedure does not, in general, take very long. However, in some cases, a box
grabs enough of the tumor to satisfy the model, even though a better
explanation (_i.e_. one with a higher _PDC_) may exist. Straight lines in the
explanation may point to the presence of a better explanation in the direction
of those straight lines.

(a) grad-cam

(b) rise

(c) lime

(d) shap

(e) rex

Figure 4: A selection of strange results from XAI tools (not on the same
image). 4(a) shows the grad-cam binary mask. Note the separation of brain and
skull and the islands contained therein. 4(b) shows the output of rise. rise
often localizes the front of the skull, even when eyes are not present. 4(c)
shows the segmentation map produced by lime (not lime’s final output). As this
map shows, lime often produces anatomically meaningless segments. 4(d) shows
the shap binary map. As well as the tumor, numerous other regions of the brain
are also erroneously given as parts of the explanation. 4(e) shows rex hybrid
mask. Note the sharp line of the explanation that has no anatomical
justification and cuts out the remainder of the tumor.

###  4.2 Limitations

All of the XAI tools were used in their default settings, with the exception
of mutant budget. This was set to 2000 where applicable. It is likely that
each could be optimized for clinical applications to improve the performances
reported here. However, it would be impractical to exhaustively search the
entire parameter space for each tool. Even if possible, great care would be
required to avoid over-fitting the tool parameters to perform well on a
particular model and dataset, but being unable to generalize to new datasets.
Therefore assessing each tool with its default settings provides the most
parsimonious comparison.

Although the _PDC_ has prima facie validity in that it rewards explanations
closer, and of a similar size, to the _HPE_ , it requires validation in the
clinical setting. To this end we plan to correlate _PDC_ with clinicians’
assessments to develop the first clinically validated measure of XAI tools.
These results are based upon a single clinical dataset and would need to be
repeated on several such datasets in order to confirm the generalisability of
our findings.

##  5 Related Work

Much of the focus of XAI in the medical domain is on the need for it and its
required characteristics, how it should be incorporated into medical workflows
and how to evaluate its outputs. There are also many studies which employ XAI
in a medical context. Far fewer publications have focused on directly
comparing XAI tools as we have here.

In one study comparing several white-box XAI tools for chest x-ray images,
grad-cam was found to be the best performing, supporting our decision to use
it as a gold-standard comparator [32]. This study also used _HPE_ to compare
XAI tool outputs, but additionally had blinded clinicians again annotate the
images in order to create a comparator. By doing so they found that grad-cam
struggled with pathologies that were small or irregular in shape. We have also
noted that all the XAI tools struggle to match the contours of irregular
shaped tumors. The very occasional exception to this is lime, which at times
provided at least partial tracing of complex shapes. This is likely due to its
segmentation step sometimes successfully delineating the complex contours of a
tumour.

Arun et al. similarly compared a number of white-box XAI tools and found that
none performed as well as dedicated segmentation DNNs [3]. They stress that
the tools failed on a number of clinical benchmarks, highlighting the
performance level required of clinically orientated XAI tools over and above
normal imaging standards.

That different XAI tools will give different explanations with the same model
and dataset has been noted in various medical contexts including;
histopathology (CAM variants vs lime variants) [16], blood test results
(interpretable models vs shap) [25] and electronic healthcare records (shap vs
lime) [12]. We have similarly noted that the XAI tools often give conflicting
information to one another. As they are evaluating the same model, this can
only be an artefact of the XAI tools themselves.

Although several papers have compared various XAI tools, as far as we can
discern this is the first paper comparing a suite of black box XAI tools
against the presumed gold-standard grad-cam on MRI data.

##  6 Conclusions

The XAI tools considered in this paper all have their limitations when applied
to tumor detection in MRIs. rex performs the best across all measures of
performance, outperforming the gold-standard grad-cam which is significant
given that the latter is a white box method.

If XAI tools are to find a place in nascent clinical AI workflows, then their
performance must be demonstrable to a degree commensurate to the task. rex is
under active development and assessment. Discussions with consultant
neuroradiologists and neuroimaging professors will guide the tool’s
development in the clinical setting. Future work will include assessing the
tool with clinically validated deep learning models, trained on large, multi-
site datasets with annotations performed by leading cancer imaging experts.

In addition to this, future work will also focus upon including a segmentation
process for the partitioning of images, similar to lime but tested upon
medical images to ensure more clinically relevant partitions. The nature of
the occlusions themselves will also be explored, as replacing image pixels
with zero, or mean/median values is not clinically meaningful. It may be
possible to use variational autoencoders to replace occluded areas with
essentially simulated data allowing, for instance, tumorous regions to be
replaced with healthy looking pixel data. This has been demonstrated on 2D
electrocardiogram data [36].

Although rex outperformed its competitors here, it is possible that the other
XAI tools could be improved to make them more amenable to clinical tasks. We
will explore several modifications that might make these general XAI tools
more suitable to medical images.

## References

  * Abreu et al. [2007] Rui Abreu, Peter Zoeteweij, and Arjan JC Van Gemund.  On the accuracy of spectrum-based fault localization.  In _Testing: Academic and Industrial Conference Practice and Research Techniques-MUTATION (TAICPART-MUTATION 2007)_ , pages 89–98. IEEE, 2007\.
  * Agarwal et al. [2023] Siddharth Agarwal, David Wood, Mariusz Grzeda, Chandhini Suresh, Munaib Din, James Cole, Marc Modat, and Thomas C Booth.  Systematic review of artificial intelligence for abnormality detection in high-volume neuroimaging and subgroup meta-analysis for intracranial hemorrhage detection.  _Clinical Neuroradiology_ , pages 1–14, 2023.
  * Arun et al. [2021] Nishanth Arun, Nathan Gaw, Praveer Singh, Ken Chang, Mehak Aggarwal, Bryan Chen, Katharina Hoebel, Sharut Gupta, Jay Patel, Mishka Gidwani, et al.  Assessing the trustworthiness of saliency maps for localizing abnormalities in medical imaging.  _Radiology: Artificial Intelligence_ , 3(6):e200267, 2021.
  * Buda [2017] Mateusz Buda.  Brain mri segmentation, 2017.  https://www.kaggle.com/datasets/mateuszbuda/lgg-mri-segmentation.
  * Buda et al. [2019] Mateusz Buda, Ashirbani Saha, and Maciej A Mazurowski.  Association of genomic subtypes of lower-grade gliomas with shape features automatically extracted by a deep learning algorithm.  _Computers in biology and medicine_ , 109:218–225, 2019\.
  * Chaddad et al. [2023] Ahmad Chaddad, Jihao Peng, Jian Xu, and Ahmed Bouridane.  Survey of explainable ai techniques in healthcare.  _Sensors_ , 23(2):634, 2023.
  * Chen et al. [2022] Hugh Chen, Scott M. Lundberg, and Su In Lee.  Explaining a series of models by propagating Shapley values.  _Nature Communications_ , 13(1), 2022.
  * Chockler and Halpern [2004] Hana Chockler and Joseph Y. Halpern.  Responsibility and blame: A structural-model approach.  _J. Artif. Intell. Res._ , 22:93–115, 2004.
  * Chockler et al. [2021] Hana Chockler, Daniel Kroening, and Youcheng Sun.  Explanations for occluded images.  In _Proceedings of the IEEE/CVF International Conference on Computer Vision_ , pages 1234–1243, 2021.
  * Dewey et al. [2019] Blake E Dewey, Can Zhao, Jacob C Reinhold, Aaron Carass, Kathryn C Fitzgerald, Elias S Sotirchos, Shiv Saidha, Jiwon Oh, Dzung L Pham, Peter A Calabresi, et al.  Deepharmony: A deep learning approach to contrast harmonization across scanner changes.  _Magnetic resonance imaging_ , 64:160–170, 2019.
  * Dice [1945] Lee Raymond Dice.  Measures of the amount of ecologic association between species.  _Ecology_ , 26:297–302, 1945.
  * Duell et al. [2021] Jamie Duell, Xiuyi Fan, Bruce Burnett, Gert Aarts, and Shang-Ming Zhou.  A comparison of explanations given by explainable artificial intelligence methods on analysing electronic health records.  In _2021 IEEE EMBS International Conference on Biomedical and Health Informatics (BHI)_ , pages 1–4. IEEE, 2021.
  * Ghassemi et al. [2021] Marzyeh Ghassemi, Luke Oakden-Rayner, and Andrew L Beam.  The false hope of current approaches to explainable artificial intelligence in health care.  _The Lancet Digital Health_ , 3(11):e745–e750, 2021.
  * Ghazi and Nielsen [2022] Mostafa Mehdipour Ghazi and Mads Nielsen.  Fast-aid brain: Fast and accurate segmentation tool using artificial intelligence developed for brain.  _arXiv preprint arXiv:2208.14360_ , 2022.
  * Ghorbani et al. [2019] Amirata Ghorbani, Abubakar Abid, and James Zou.  Interpretation of neural networks is fragile.  In _Proceedings of the AAAI conference on artificial intelligence_ , pages 3681–3688, 2019.
  * Graziani et al. [2021] Mara Graziani, Thomas Lompech, Henning Müller, and Vincent Andrearczyk.  Evaluation and comparison of cnn visual explanations for histopathology.  In _Proceedings of the AAAI Conference on Artificial Intelligence Workshops (XAI-AAAI-21), Virtual Event_ , pages 8–9, 2021.
  * Gulum et al. [2021] Mehmet A Gulum, Christopher M Trombley, and Mehmed Kantardzic.  A review of explainable deep learning cancer detection models in medical imaging.  _Applied Sciences_ , 11(10):4573, 2021.
  * Halpern [2016] J. Y. Halpern.  _Actual Causality_.  MIT Press, Cambridge, MA, 2016.
  * Halpern and Pearl [2005] Joseph Y. Halpern and Judea Pearl.  Causes and explanations: a structural-model approach. Part II: Explanations.  _British Journal for the Philosophy of Science_ , 56(4), 2005.
  * Hutson [2018] Matthew Hutson.  Artificial intelligence faces reproducibility crisis, 2018.
  * Legastelois et al. [2023] Benedicte Legastelois, Amy Rafferty, Paul Brennan, Hana Chockler, Ajitha Rajan, and Vaishak Belle.  Challenges in explaining brain tumor detection.  In _Proceedings of the First International Symposium on Trustworthy Autonomous Systems_ , pages 1–8, 2023.
  * Lundberg and Lee [2017] Scott M Lundberg and Su-In Lee.  A unified approach to interpreting model predictions.  In _Advances in Neural Information Processing Systems_ , pages 4765–4774, 2017.
  * McDermott et al. [2021] Matthew BA McDermott, Shirly Wang, Nikki Marinsek, Rajesh Ranganath, Luca Foschini, and Marzyeh Ghassemi.  Reproducibility in machine learning for health research: Still a ways to go.  _Science Translational Medicine_ , 13(586):eabb1655, 2021.
  * Okhrati and Lipani [2021] R Okhrati and A Lipani.  A Multilinear Sampling Algorithm to Estimate Shapley Values.  In _2020 25th International Conference on Pattern Recognition (ICPR)_ , pages 7992–7999, Los Alamitos, CA, USA, 2021. IEEE Computer Society.
  * Onari et al. [2022] Mohsen Abbaspour Onari, Marco S Nobile, Isel Grau, Caro Fuchs, Yingqian Zhang, Arjen-Kars Boer, and Volkher Scharnhorst.  Comparing interpretable ai approaches for the clinical environment: an application to covid-19.  In _2022 IEEE Conference on Computational Intelligence in Bioinformatics and Computational Biology (CIBCB)_ , pages 1–8. IEEE, 2022.
  * Petsiuk et al. [2018] Vitali Petsiuk, Abir Das, and Kate Saenko.  RISE: randomized input sampling for explanation of black-box models.  In _British Machine Vision Conference (BMVC)_. BMVA Press, 2018\.
  * Rajpurkar and Lungren [2023] Pranav Rajpurkar and Matthew P Lungren.  The current and future state of ai interpretation of medical images.  _New England Journal of Medicine_ , 388(21):1981–1990, 2023.
  * Rajpurkar et al. [2022] Pranav Rajpurkar, Emma Chen, Oishi Banerjee, and Eric J Topol.  Ai in health and medicine.  _Nature medicine_ , 28(1):31–38, 2022.
  * Ribeiro et al. [2016] Marco Tulio Ribeiro, Sameer Singh, and Carlos Guestrin.  “Why should I trust you?” Explaining the predictions of any classifier.  In _Knowledge Discovery and Data Mining (KDD)_ , pages 1135–1144. ACM, 2016.
  * Roberts et al. [2021] Michael Roberts, Derek Driggs, Matthew Thorpe, Julian Gilbey, Michael Yeung, Stephan Ursprung, Angelica I Aviles-Rivero, Christian Etmann, Cathal McCague, Lucian Beer, et al.  Common pitfalls and recommendations for using machine learning to detect and prognosticate for covid-19 using chest radiographs and ct scans.  _Nature Machine Intelligence_ , 3(3):199–217, 2021.
  * Russakovsky et al. [2015] Olga Russakovsky, Jia Deng, Hao Su, Jonathan Krause, Sanjeev Satheesh, Sean Ma, Zhiheng Huang, Andrej Karpathy, Aditya Khosla, Michael Bernstein, Alexander C. Berg, and Li Fei-Fei.  ImageNet Large Scale Visual Recognition Challenge.  _International Journal of Computer Vision (IJCV)_ , 115(3):211–252, 2015.
  * Saporta et al. [2022] Adriel Saporta, Xiaotong Gui, Ashwin Agrawal, Anuj Pareek, Steven QH Truong, Chanh DT Nguyen, Van-Doan Ngo, Jayne Seekins, Francis G Blankenberg, Andrew Y Ng, et al.  Benchmarking saliency methods for chest x-ray interpretation.  _Nature Machine Intelligence_ , 4(10):867–878, 2022.
  * Selvaraju et al. [2017] Ramprasaath R Selvaraju, Michael Cogswell, Abhishek Das, Ramakrishna Vedantam, Devi Parikh, and Dhruv Batra.  Grad-CAM: Visual explanations from deep networks via gradient-based localization.  In _International Conference on Computer Vision (ICCV)_ , pages 618–626. IEEE, 2017.
  * Sørensen [1948] Thorvald Sørensen.  A method of establishing groups of equal amplitude in plant sociology based on similarity of species and its application to analyses of the vegetation on danish commons.  _Kongelige Danske Videnskabernes Selskab._ , 5:1–34, 1948\.
  * van Amsterdam et al. [2019] WAC van Amsterdam, JJC Verhoeff, PA de Jong, T Leiner, and MJC Eijkemans.  Eliminating biasing signals in lung cancer images for prognosis predictions with deep learning.  _NPJ digital medicine_ , 2(1):122, 2019.
  * van de Leur et al. [2022] Rutger R van de Leur, Max N Bos, Karim Taha, Arjan Sammani, Ming Wai Yeung, Stefan van Duijvenboden, Pier D Lambiase, Rutger J Hassink, Pim van der Harst, Pieter A Doevendans, et al.  Improving explainability of deep neural network-based electrocardiogram interpretation using variational auto-encoders.  _European Heart Journal-Digital Health_ , 3(3):390–404, 2022.
  * van der Velden [2023] Bas HM van der Velden.  Explainable ai: current status and future potential.  _European Radiology_ , pages 1–3, 2023.
  * Van der Velden et al. [2022] Bas HM Van der Velden, Hugo J Kuijf, Kenneth GA Gilhuijs, and Max A Viergever.  Explainable artificial intelligence (xai) in deep learning-based medical image analysis.  _Medical Image Analysis_ , 79:102470, 2022.
  * Varoquaux and Cheplygina [2022] Gaël Varoquaux and Veronika Cheplygina.  Machine learning for medical imaging: methodological failures and recommendations for the future.  _NPJ digital medicine_ , 5(1):48, 2022.
  * Volovici et al. [2022] Victor Volovici, Nicholas L Syn, Ari Ercole, Joseph J Zhao, and Nan Liu.  Steps to avoid overuse and misuse of machine learning in clinical research.  _Nature Medicine_ , 28(10):1996–1999, 2022.
  * Wood et al. [2022] David A Wood, Sina Kafiabadi, Ayisha Al Busaidi, Emily Guilhem, Antanas Montvila, Jeremy Lynch, Matthew Townend, Siddharth Agarwal, Asif Mazumder, Gareth J Barker, et al.  Deep learning models for triaging hospital head mri examinations.  _Medical Image Analysis_ , 78:102391, 2022.