# A Linear Algebra Approach to Linear Metatheory

James Wood James Wood is supported by an EPSRC Studentship.University of
Strathclyde
Glasgow, United Kingdom<EMAIL_ADDRESS>University of Strathclyde
Glasgow, United Kingdom Robert Atkey University of Strathclyde
Glasgow, United Kingdom<EMAIL_ADDRESS>
###### Abstract

Linear typed $\lambda$-calculi are more delicate than their simply typed
siblings when it comes to metatheoretic results like preservation of typing
under renaming and substitution. Tracking the usage of variables in contexts
places more constraints on how variables may be renamed or substituted. We
present a methodology based on linear algebra over semirings, extending
McBride’s _kits and traversals_ approach for the metatheory of syntax with
binding to linear usage-annotated terms. Our approach is readily formalisable,
and we have done so in Agda.

##  1 Introduction

The basic metatheoretic results for typed $\lambda$-calculi, such as
preservation of typing under renaming, weakening, substitution and so on, are
crucial but quite boring to prove. In calculi with substructural typing
disciplines and modalities, it can also be quite easy to break these
properties [Wad92, BBPH93]. It is desirable therefore to use a proof assistant
to prove these properties. This has the double benefit of both confidence in
the results and in focusing on the essential properties required to obtain
them.

Mechanisation of the metatheory of substructural $\lambda$-calculi has not
received the same level of attention as intuitionistic typing.
“Straightforward” translations from paper presentations to formal
presentations make metatheory difficult, due to incompatibilies between the
standard de Bruijn representation of binding and the splitting of contexts.
For formalisations of linear sequent calculi, sticking to the paper
presentation using lists and permutations is common [PW99, XORN17, Lau18], but
explicit permutations make the resulting encodings difficult to use. Multisets
for contexts are more convenient [CLR19], but do not work well for Curry-
Howard uses, as noted by Laurent. For natural deduction, Allais [All18] uses
an I/O model to track usage of variables, Rouvoet et al. [RBPKV20] use a co-de
Bruijn representation to distribute variables between subterms, and Crary uses
mutually defined typing and linearity judgements with HOAS [Cra10].

In this paper, we adapt the generic _kits and traversals_ technique for
proving admissibility of renaming and substitution due to McBride [McB05] to a
linear typed $\lambda$-calculus where variables are annotated with values from
a skew semiring denoting those variables’ _usage_ by terms. Our calculus,
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$,
is a prototypical example of a linear “quantitative” or “coeffect” calculus in
the style of [RP10, BGMZ14, GS14, POM14, OLE19]. The key advantages of
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
over the formalisations listed above are that the shape of typing contexts is
maintained, so de Bruijn indices behave the same as in non-substructural
calculi, and by selecting different semirings, we obtain from
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
well known systems, including Barber’s Dual Intuitionistic Linear Logic
[Bar96] and Pfenning and Davies’ S4 modal type theory [PD99].

McBride’s kits and traversals technique isolates properties required to form
binding-respecting traversals of simply typed $\lambda$-terms, so that
renaming and substitution arise as specific instantiations. Benton, Hur,
Kennedy, and McBride [BHKM12] implement the technique in Coq and extend it to
polymorphic terms. Allais _et al._ [AAC+20] generalise to a wider class of
syntax with binding and show that more general notions of _semantics_ can be
handled. Using methods like these can reduce the effort required to develop a
new calculus and its metatheory.

To adapt kits and traversals to linear usage-annotated terms requires us to
not only respect the binding structure, but to also respect the usage
annotations. For instance, the usages associated with a term being substituted
in must be correctly distributed across all the occurrences of that term in
the result. To aid us in tracking usages, we employ the linear algebra of
vectors and matrices induced by the skew semiring we are using. Usage
annotations on contexts are vectors, usage-preserving maps of contexts are
matrices, and the linearity properties of the maps induced by matrices are
exactly the lemmas we need for showing that traversals (and hence renaming,
subusaging, and substitution) preserve typing and usages.

The paper proceeds as follows:

  * •

In Section 2, we specify our requirements on the set of annotations that will
track usage of variables. A consequence of our formalisation is that we learn
that we only need _skew_ semirings, a weaker structure than the partially
ordered semirings usually used.

  * •

In Section 3, we use these annotations to define the system
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
in an intrinsically typed style.

  * •

In Section 4, we show some characteristics of
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
under certain general conditions on the skew semiring of usage annotations.

  * •

In Section 5, we show that, via choice of semiring, we can embed Barber’s Dual
Intuitionistic Linear Logic [Bar96] and Pfenning and Davies’ modal calculus
[PD99].

  * •

In Section 6, we prove that
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
admits renaming, subusaging, and substitution by our extension of McBride’s
kits and traversals technique.

  * •

We conclude in Section 7 with some directions for future work.

Section 4 and Section 5 can be read as extended examples of the
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
syntax. Those two sections logically come after Section 6, but we think it
helpful for readers unfamiliar with semiring-annotated calculi to read them
before proceeding to Section 6. Conversely, a reader familiar with semiring-
annotated calculi who is primarily interested in our metatheoretic methods may
skip Section 4 and Section 5 without issue.

The Agda formalisation of this work can be found at
https://github.com/laMudri/generic-lr/tree/lin/tlla-submission/src/Specific.
It contains our formalisation of vectors and matrices (approx. 790 lines) and
the definition of
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
and proofs of renaming and substitution (approx. 530 lines).

##  2 Skew semirings

We shall use skew semirings where other authors have previously used partially
ordered semirings (see, for example, the Granule definition of a _resource
algebra_ [OLE19]). Elements of a skew semiring are used as _usage annotations_
, and describe _how_ values are used in a program. In the syntax for
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$,
each assumption will have a usage annotation, describing how that assumption
can be used in the derivation. Addition describes how to combine multiple
usages of an assumption, and multiplication describes the action our graded
$\oc$-modality can have. The ordering describes the specificness of
annotations. If $p\trianglelefteq q$, $p$ can be the annotation for a variable
wherever $q$ can be. We can read this relation as
“$\textrm{supply}\trianglelefteq\textrm{demand}$” — given a variable annotated
$p$, we can coerce to treat it as if it has the desired annotation $q$.

Skew semirings are a generalisation of partially ordered semirings, which are
in turn a generalisation of commutative semirings. As such, readers unfamiliar
with the more general structures may wish to think in terms of the more
specific structures. Our formalisation was essential for noticing and sticking
to this level of generality.

######  Definition 2.1.

A _(left) skew monoid_ is a structure $(\mathbf{R},\trianglelefteq,1,*)$ such
that $(\mathbf{R},\trianglelefteq)$ forms a partial order, $*$ is monotonic
with respect to $\trianglelefteq$, and the following laws hold (with $x*y$
henceforth being written as $xy$). 1x ⊴x x ⊴x1 (xy)z ⊴x(yz)

######  Remark 2.2.

A commutative skew monoid is just a partially ordered commutative monoid.

Skew-monoidal categories are due to Szlachányi [Szl12], and the notion
introduced here of a skew monoid is a decategorification of the notion of
skew-monoidal category.

######  Definition 2.3.

A _(left) skew semiring_ is a structure $(\mathbf{R},\trianglelefteq,0,+,1,*)$
such that $(\mathbf{R},\trianglelefteq)$ forms a partial order, $+$ and $*$
are monotonic with respect to $\trianglelefteq$, $(\mathbf{R},0,+)$ forms a
commutative monoid, $(\mathbf{R},\trianglelefteq,1,*)$ forms a skew monoid,
and we have the following distributivity laws. 0z ⊴0 (x + y)z ⊴xz + yz 0 ⊴x0
xy + xz ⊴x(y + z)

######  Example 2.4.

In light of the above remark, most “skew” semirings are actually just
partially ordered semirings. An example that yields a system equivalent to
Barber’s DILL is the
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}\triangleright{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}\triangleleft{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$
semiring of “unused”, “unrestricted”, and “linear”, respectively. See [OLE19]
for more examples.

We will only speak of _left_ skew semirings, and thus generally omit the word
“left”. A mnemonic for (left) skew semirings is “multiplication respects
operators on the left from left to right, and respects operators on the right
from right to left”. One may also describe multiplication as “respecting” and
“corespecting” operators on the left and right, respectively.

From a skew semiring $\mathbf{R}$, we form finite vectors, which we notate as
$\mathbf{R}^{n}$, and matrices, which we notate as $\mathbf{R}^{m\times n}$.
In Agda, we represent vectors in $\mathbf{R}^{n}$ as functions
$\operatorname{Idx}n\to\mathbf{R}$, where $\operatorname{Idx}n$ is the type of
valid indexes in an $n$-tuple, and matrices in $\mathbf{R}^{m\times n}$ as
functions $\operatorname{Idx}m\to\operatorname{Idx}n\to\mathbf{R}$. Whereas
elements of $\mathbf{R}$ describe how individual _variables_ are used,
elements of $\mathbf{R}^{n}$ describe how all of the variables in an
$n$-length _context_ are used. We call such vectors _usage contexts_ , and
take them to be row vectors. Matrices in $\mathbf{R}^{m\times n}$ will be used
to describe how usage contexts are transformed by renaming and substitution in
Section 6. We define $\trianglelefteq$, $0$ and $+$ on vectors and matrices
pointwise. Basis vectors $\langle i\rvert$ (used to represent usage contexts
for individual variables), identity matrices $\mathbf{I}$, matrix
multiplication $*$, and matrix reindexing ${-}_{\\_}{{-}\times{-}}$ are
defined as follows: ⟨- |: Idxn →Rn⟨i |j := {1, if i = j0, otherwise I : Rm
×mIij := ⟨i |j * : Rm ×n×Rn ×o→Rm ×o(MN)ik := ∑j MijNjk –×- : Rm’ ×n’×(Idxm
→Idxm’) ×(Idxn →Idxn’) →Rm ×n(Mf ×g)i,j := Mf i,g j

We define vector-matrix multiplication by treating vectors as $1$-height
matrices. If $i:\operatorname{Idx}m$ and $j:\operatorname{Idx}n$, then
$\operatorname{inl}i$ and $\operatorname{inr}j$ are both of type
$\operatorname{Idx}(m+n)$. In prose, there will always be canonical choices
for $m$ and $n$, whereas in the mechanisation, we work with the free pointed
magma over the $1$-element set as opposed to the free monoid over the
$1$-element set (i.e., the natural numbers), so it is unambiguous where there
is a sum of dimensionalities.

##  3 Syntax

Figure 1: Typing rules of
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$

*[right=var] x : RΓ ⊐-A x : RΓ ⊢A *[right=$\multimap$-E] M : PΓ ⊢A ⊸B
N : QΓ ⊢A
R ⊴P \+ Q M N : RΓ ⊢B *[right=$\multimap$-I] M : RΓ, 1A ⊢B λM : RΓ ⊢A ⊸B

*[right=$1$-E] M : PΓ ⊢1
N : QΓ ⊢C
R ⊴P \+ Q let (_⊗)= M in N : RΓ ⊢C *[right=$1$-I] R ⊴0 (_⊗) : RΓ ⊢1
*[right=$\otimes$-E] M : PΓ ⊢A ⊗B
N : QΓ, 1A, 1B ⊢C
R ⊴P \+ Q let (- _⊗ -) = M in N : RΓ ⊢C *[right=$\otimes$-I] M : PΓ ⊢A
N : QΓ ⊢B
R ⊴P \+ Q (M _⊗ N) : RΓ ⊢A ⊗B

*[right=$0$-E] M : PΓ ⊢0
R ⊴P \+ Q ex-falso M : RΓ ⊢C *[right=$\oplus$-E] M : PΓ ⊢A ⊕B
N : QΓ, 1A ⊢C
O : QΓ, 1B ⊢C
R ⊴P \+ Q case M of inj_L - ↦N ; inj_R - ↦O : RΓ ⊢C *[right=$\oplus$-Il] M :
RΓ ⊢A inj_L M : RΓ ⊢A ⊕B *[right=$\oplus$-Ir] M : RΓ ⊢B inj_R M : RΓ ⊢A ⊕B

*[right=$\top$-I] (_) : RΓ ⊢⊤ *[right=$\with$-El] M : RΓ ⊢A B proj_L M : RΓ ⊢A *[right=$\with$-Er] M : RΓ ⊢A B proj_R M : RΓ ⊢B *[right=$\with$-I] M : RΓ ⊢A
N : RΓ ⊢B (M _ N) : RΓ ⊢A B

*[right=$\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}}$-E] M : PΓ ⊢_r A
N : QΓ, rA ⊢C
R ⊴P \+ Q let [-] = M in N : RΓ ⊢C
*[right=$\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}}$-I]
M : PΓ ⊢A
R ⊴rP [M] : RΓ ⊢_r A

We present the syntax of
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
as an _intrinsically_ typed syntax, as it is in our Agda formalisation.
Intrinisic typing means that we define well typed terms as inhabitants of an
inductive family
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\Gamma\vdash
A$ indexed by typing contexts $\Gamma$, usage contexts
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$,
and types $A$. Typing contexts are lists of types. Usage contexts
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
are vectors of elements of some fixed skew semiring $\mathbf{R}$, with the
same number of elements as the typing context they are paired with. To
highlight how usage annotations are used in the syntax, we write all elements
of $\mathbf{R}$, and vectors and matrices thereof, in green.

The types of
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
are given by the grammar: $A,B,C::=\iota\mid A\multimap B\mid 1\mid A\otimes
B\mid 0\mid A\oplus B\mid\top\mid A\with
B\mid\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}}A$.
We have a base type $\iota$, function types $A\multimap B$, tensor product
types $A\otimes B$ with unit $1$, sum types $A\oplus B$ with unit $0$, “with”
product types $A\with B$ with unit $\top$, and an exponential
$\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}}A$
indexed by a usage
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}$.

We distinguish between _plain_ variables, values of type $\Gamma\ni A$, which
are indices into a context with a specified type, and _usage-checked_
variables, values of type
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\Gamma\mathrel{\mathrlap{\sqsupset}{\mathord{-}}}A$
which are pairs of a plain variable $i:\Gamma\ni A$ and proof that
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\trianglelefteq\langle
i\rvert$. The force of the latter condition is that the selected variable $i$
must have a usage annotation
$\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$
in
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$,
and all other variables must have a usage annotation
$\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$.
We will sometimes silently cast between the types $\operatorname{Idx}m$ and
$\Gamma\ni A$, particularly when using the reindexing operation
${-}_{\\_}{{-}\times{-}}$.

The constructors for our intrinsically typed terms are presented in Figure 1.
In keeping with our intrinsic typing methodology, terms of
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
are presented as constructors of the inductive family
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\Gamma\vdash
A$, hence the notation
$M:{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\Gamma\vdash
A$ instead of the more usual
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\Gamma\vdash
M:A$. Our Agda formalisation uses de Bruijn indices to represent variables,
but we have annotated the rules with variable names for ease of reading.
Ignoring the usages, the typing rules all look like their simply typed
counterparts; the only difference between the $\otimes$ and $\with$ products
being their presentation in terms of pattern matching and projections,
respectively. Thus the addition of usage contexts and constraints on them
refines the usual simple typing to be usage constrained. For instance, in the
$\otimes$-I rule, the usage context
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
on the conclusion is constrained to be able to supply the sum
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}+{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}$
of the usage contexts of the premises. If we instantiate $\mathbf{R}$ to be
the
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}\triangleright{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}\triangleleft{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$
semiring, then we obtain a system that is equivalent to Barber’s DILL [Bar96].

For the sake of Section 6, the precise rules chosen here are not too
important. The salient point is that contexts can only be manipulated in
specific ways. Typing contexts can only be modified by context extensions,
i.e., binding new variables. Usage contexts can correspondingly be extended,
but also can be _linearly split_. A usage context
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
can be split into zero pieces via constraint
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathbf{0}}$,
into two pieces,
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}$
and
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}$,
via constraint
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}+{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}$,
and an
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}$-scaled
down piece
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}$
via constraint
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}$.

However, the rules chosen are important in Section 5, as they correspond
closely to the rules of Dual Intuitionistic Linear Logic and the modal
calculus of Pfenning and Davies [Bar96, PD99]. In fact, there are several
similar calculi in the literature which do not embed intuitionistic linear
logic, and thus do not translate in the same way as
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$.
For example, the system of Abel and Bernardy [AB20] essentially replaces
$\otimes$-E with the following stronger rule (in our notation, modified to
include subusaging). This eliminator allows one to derive
$\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}}(A\otimes
B)\multimap\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}}A\otimes\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}}B$
for any
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}$,
$A$, and $B$, whereas linear logic has no such tautology.

$\inferrule*[right=\otimes-E^{\prime}]{M:{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\vdash
A\otimes B\\\
{N}:{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Gamma,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}q}A,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}q}B\vdash
C\\\
{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}q}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}+{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}}{\mathrm{let}~{}(-\mathbin{{}_{\otimes}}-)={\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}q}M~{}\mathrm{in}~{}{N}:{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\Gamma\vdash
C}$

In Section 6, we will show the admissibility of, amongst others, the rules
shown in Section 3. The rules in Section 3 will be required for the proofs in
Section 4 and Section 5. Using these rules, we can also derive the following
fact, which demonstrates a linear form of _cut_.

######  Lemma 3.1.

If we can derive
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}A\vdash
B$, then we also know that from
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\Gamma\vdash
A$ we can derive
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\Gamma\vdash
B$.

###### Proof.

Assuming the two hypotheses, we can make the following derivation.

$\inferrule*[right=SingleSubst]{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\Gamma\vdash
A\\\
\inferrule*[right=Weak]{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}A\vdash
B}{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{0}}}\Gamma,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}A\vdash
B}\\\
\inferrule*{}{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}+\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}}}{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\Gamma\vdash
B}$

∎

*[right=SingleSubst] M : PΓ ⊢A
N : QΓ, rA ⊢B
R ⊴r P \+ Q N{M} : RΓ ⊢B *[right=Subuse] M : QΓ ⊢A
P ⊴Q M : PΓ ⊢A *[right=Weak] PΓ ⊢A PΓ, 0Δ ⊢A

##  4 Intuitionistic and modal instantiations

As we will show in subsection 5.1,
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
can be instantiated with a semiring which makes it capture linearity. However,
with different choices of semiring,
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
can become a calculus satisfying more structural rules.

######  Lemma 4.1.

When instantiated with the 1-element (skew) semiring
$\\{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\bullet}\\}$,
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
becomes a variant of intuitionistic simply typed $\lambda$-calculus.

###### Proof.

With only one possible usage annotation, usage contexts do not contain any
information. Because
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\bullet}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\bullet}$,
all $\trianglelefteq$-constraints are satisfied. ∎

An important class of skew semirings is those for which $0$ is the top element
of the $\trianglelefteq$-order and $+$ acts as a meet (minimum). While
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
instantiated this way admits full weakening and contraction, the usage
annotations can still play a part via the
$\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}}$
modality. We will see an example of such an instantiation in subsection 5.2.

######  Lemma 4.2.

If
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
is instantiated at a skew semiring such that $0$ is top and $+$ is meet (with
respect to the subusaging order), then $\top$ and $1$ are interderivable, and
$A\with B$ and $A\otimes B$ are interderivable.

###### Proof.

By 3.1, following derivations suffice. *[right=$\top$-I] 11 ⊢⊤

*[right=$1$-I] * 1 ⊴0 1⊤ ⊢1

*[right=$\otimes$-E] *[right=var] * (1) ⊴(1) 1(A ⊗B) ⊢A ⊗B
*[right=$\with$-I] *[right=var] * (0, 1, 1) ⊴(0, 1, 0) 0(A ⊗B), 1A, 1B ⊢A
*[right=var] * (0, 1, 1) ⊴(0, 0, 1) 0(A ⊗B), 1A, 1B ⊢B 0(A ⊗B), 1A, 1B ⊢A B
* (1) + (0) ⊴(1) 1(A ⊗B) ⊢A B

*[right=$\otimes$-I] *[right=$\with$-El] *[right=var] * (1) ⊴(1) 1(A B) ⊢A B 1(A B) ⊢A
*[right=$\with$-Er] *[right=var] * (1) ⊴(1) 1(A B) ⊢A B 1(A B) ⊢B
* (1) ⊴(1) + (1) 1(A B) ⊢A ⊗B  ∎

##  5 Translation to and from existing systems

A motivating reason to consider the system presented in this paper is that
instances of it correspond to previously studied systems. In this section, we
present translations from
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
to Dual Intuitionistic Linear Logic [Bar96] and the modal system of Pfenning
and Davies [PD99], and vice versa. These translations are not mechanised, as
part of the reason for developing
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
was to avoid mechanising these systems directly. We cannot prove that the
translations form an equivalence, because we have not written down an
equational theory for
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$,
but we expect this to be easy enough to do.

###  5.1 Dual Intuitionistic Linear Logic

Dual Intuitionistic Linear Logic is a particular formulation of intuitionistic
linear logic [Bar96]. Its key feature, which simplifies the metatheory of
linear logic, is the use of separate contexts for linear and intuitionistic
free variables. Here we show that DILL is a fragment of the instantiation of
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
at the linearity semiring
$\\{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0},{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1},{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}\\}$.

The types of DILL are the same as the types of
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$,
except for the restriction of
$\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}}$
to just
$\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}}}$.
We will write the latter simply as $\oc$ when it appears in DILL. We add sums
and with-products to the calculus of [Bar96], with the obvious rules (stated
fully in Figure 2). These additive type formers present no additional
difficulty to the translation.

*[right=Int-Ax] Γ, A; ⋅⊢A *[right=Lin-Ax] Γ; A ⊢A *[right=$I$-I] Γ; ⋅⊢I *[right=$I$-E] Γ; Δ1 ⊢I
Γ; Δ2 ⊢A Γ; Δ1, Δ2 ⊢A *[right=$\otimes$-I] Γ; Δ1 ⊢A
Γ, Δ2 ⊢B Γ; Δ1, Δ2 ⊢A ⊗B *[right=$\otimes$-E] Γ; Δ1 ⊢A ⊗B
Γ; Δ2, A, B ⊢C Γ; Δ1, Δ2 ⊢C *[right=$\multimap$-I] Γ; Δ, A ⊢B Γ; Δ⊢A ⊸B
*[right=$\multimap$-E] Γ; Δ1 ⊢A ⊸B
Γ; Δ2 ⊢A Γ; Δ1, Δ2 ⊢B *[right=$\oc$-I] Γ; ⋅⊢A Γ; ⋅⊢A *[right=$\oc$-E] Γ; Δ1 ⊢A
Γ, A; Δ2 ⊢B Γ; Δ1, Δ2 ⊢B *[right=$\top$-I] Γ; Δ⊢⊤ *[right=$\with$-I] Γ; Δ⊢A
Γ, Δ⊢B Γ; Δ⊢A B *[right=$\with$-E${}_{\\_}i$] Γ; Δ⊢A0 A1 Γ; Δ⊢Ai
*[right=$0$-E] Γ; Δ1 ⊢0 Γ; Δ1, Δ2 ⊢A *[right=$\oplus$-I${}_{\\_}i$] Γ; Δ⊢Ai Γ;
Δ⊢A0 ⊕A1 *[right=$\oplus$-E] Γ; Δ1 ⊢A ⊕B
Γ; Δ2, A ⊢C
Γ; Δ2, B ⊢C Γ; Δ1, Δ2 ⊢C

Figure 2: The rules of DILL, extended with additive connectives

DILL↪$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$01ωY↦ιYI↦1A
⊗B↦A ⊗BA ⊸B↦A
⊸BA↦_${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}$
A0↦0A ⊕B↦A ⊕B⊤↦⊤A B↦A B

PD↪$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}01\square}$Y↦ιY⊤↦1A
∧B↦A BA ⊃B↦A
⊸B□A↦_${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}$
A⊥↦0A ∨B↦A ⊕B

Figure 3: Embedding of DILL and PD types into
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$

######  Proposition 5.1 (DILL $\to$
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$).

Given a DILL derivation of $\Gamma;\Delta\vdash A$, we can produce a
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}_{\\_}{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}01\omega}}$
derivation of
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}}}}\Gamma,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{1}}}\Delta\vdash
A$.

###### Proof.

By induction on the derivation. We have
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$,
which allows us to discard intuitionistic variables at the var rules, and both
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$
and
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$,
which allow us to use both linear and intuitionistic variables.

Weakening is used when splitting linear variables between two premises. For
example, $\otimes$-I in DILL is as follows.

$\inferrule*[right=\otimes-I]{\Gamma;\Delta_{\\_}t\vdash t:A\\\
\Gamma;\Delta_{\\_}u\vdash u:B}{\Gamma;\Delta_{\\_}t,\Delta_{\\_}u\vdash
t\otimes u:A\otimes B}$

From this, our new derivation is as follows.

$\inferrule*[right=\otimes-I]{\inferrule*[right=Weak]{\mathit{ih}_{\\_}t\\\
\\\
{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}}}}\Gamma,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}}}}\Delta_{\\_}t\vdash
M_{\\_}t:A}{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}}}}\Gamma,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}}}}\Delta_{\\_}t,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}}}}\Delta_{\\_}u\vdash
M_{\\_}t:A}\\\ \inferrule*[right=Weak]{\mathit{ih}_{\\_}u\\\ \\\
{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}}}}\Gamma,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}}}}\Delta_{\\_}u\vdash
M_{\\_}u:A}{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}}}}\Gamma,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}}}}\Delta_{\\_}t,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}}}}\Delta_{\\_}u\vdash
M_{\\_}u:A}}{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}}}}\Gamma,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}}}}\Delta_{\\_}t,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}}}}\Delta_{\\_}u\vdash(M_{\\_}t\mathbin{{}_{\otimes}}M_{\\_}u):A\otimes
B}$

∎

When translating from
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
to DILL, we first coerce the
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
derivation to be in a form easily amenable to translation into DILL. An
example of a
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
derivation with no direct translation into DILL is the following. In DILL
terms, the intuitionistic variable of the conclusion becomes a linear variable
in the premises. Such a move is admissible in DILL, but does not come
naturally.

$\inferrule*[right=\otimes-I]{\inferrule*[right=var]{}{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}}A\vdash
A}\\\
\inferrule*[right=var]{}{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}}A\vdash
A}\\\
{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}+{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}}{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}}A\vdash
A\otimes A}$

To avoid such situations, and therefore manipulations on DILL derivations, we
show that all
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}_{\\_}{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}01\omega}}$
derivations can be made in _bottom-up_ style. In bottom-up style, the
algebraic facts we make use of are dictated by making most general choices
based on the conclusions of rules. Bottom-up style corresponds to a (non-
deterministic) form of _usage checking_ , and the following lemma can be
understood as saying that that form of usage checking is sufficiently general.

######  Definition 5.2.

A derivation is said to be
_${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}01\omega}$
-bottom-up_ if only the following facts about addition and multiplication are
used, and all proofs of inequalities not at leaves are by reflexivity (i.e,
not using the facts that
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$
and
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$).

$+$ ${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$ -
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$ - -
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}$
- -
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}$
$*$ ${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$ - -
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$ -
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}$

Bottom-up style enforces that whenever we split a context into two (for
example, in the rule $\otimes$-I) all unused variables in the conclusion stay
unused in the premises, intuitionistic variables stay intuitionistic, and
linear variables go either left or right. Multiplication is only used in the
rule
$\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}}$-I,
at which point both the result and left argument are available. Here, the
bottom-up style enforces that linear variables never appear in the premise of
$\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}}}$-I.

######  Lemma 5.3.

Every
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}_{\\_}{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}01\omega}}$
derivation can be translated into a bottom-up
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}_{\\_}{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}01\omega}}$
derivation.

###### Proof.

By induction on the shape of the derivation. When we come across a non-bottom-
up use of addition, it must be that the corresponding variable in the
conclusion has annotation
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}$.
By subusaging, we can give this variable annotation
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}$
in the premises too, before translating the subderivations to bottom-up style.
A similar argument applies to uses of multiplication, remembering that both
the left argument and result are fixed. ∎

######  Proposition 5.4
($\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
$\to$ DILL).

Given a
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}_{\\_}{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}01\omega}}$
derivation of
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}}}}\Gamma,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}}}}\Delta,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}}}}\Theta\vdash
A$ which contains only types expressible in DILL, we can produce a DILL
derivation of $\Gamma;\Delta\vdash A$.

###### Proof.

By induction on the derivation having been translated to bottom-up form.

In the case of var, all of the unused variables have annotation greater than
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$,
i.e.,
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$ or
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}$.
Those annotated
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$ are
absent from the DILL derivation, and those annotated
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}$
are in the intuitionistic context. The used variable is annotated either
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$ or
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}$.
In the first case, we use Lin-Ax, and in the second case, Int-Ax.

All binding of variables in
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
maps directly onto DILL.

Because we translated to bottom-up form, additions, as seen in, for example,
the $\otimes$-I rule, can be handled straightforwardly. Any intuitionistic
variables in the conclusion correspond to intuitionistic variables in both
premises. Any linear variables in the conclusion correspond to a linear
variable in exactly one of the premises, and is absent in the other premise.

The only remaining rule is
$\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}}$-I,
of which we only cover
$\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}}}$-I
(the other two targeting types not found in DILL). In this case, we know that
every variable in the conclusion is annotated either
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$ or
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\omega}$,
and every variable in the premise is annotated the same way. This corresponds
exactly to the restrictions of DILL’s $\oc$-I. ∎

###  5.2 Pfenning Davies

The translation to and from the modal system of Pfenning and Davies [PD99]
(henceforth _PD_) is similar to the translation to and from DILL. We present
our variant of PD, again adding some common connectives, in Figure 4 The main
difference is the algebra at which
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
is instantiated.

*[right=hyp] Γ; Δ, A true ⊢A true *[right=hyp*] Γ, A valid; Δ⊢A true *[right=$\supset$I] Γ; Δ, A true ⊢B true Γ; Δ⊢A ⊃B true *[right=$\supset$E] Γ; Δ⊢A ⊃B true
Γ; Δ⊢A true Γ; Δ⊢B true *[right=$\Box$I] Γ; ⋅⊢A true Γ; Δ⊢□A true
*[right=$\Box$-E] Γ; Δ⊢□A true
Γ, A valid; Δ⊢B true Γ; Δ⊢B true *[right=$\top$-I] Γ; Δ⊢⊤ true
*[right=$\wedge$-I] Γ; Δ⊢A true
Γ, Δ⊢B true Γ; Δ⊢A ∧B true *[right=$\wedge$-E${}_{\\_}i$] Γ; Δ⊢A0 ∧A1 true Γ;
Δ⊢Ai true *[right=$\bot$-E] Γ; Δ⊢⊥ true Γ; Δ⊢A true
*[right=$\vee$-I${}_{\\_}i$] Γ; Δ⊢Ai true Γ; Δ⊢A0 ∨A1 true *[right=$\vee$-E]
Γ; Δ⊢A ∨B true
Γ; Δ, A ⊢C true
Γ; Δ, B ⊢C true Γ; Δ⊢C true

Figure 4: The rules of PD, extended with several standard connectives

######  Definition 5.5.

Let
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}01\square}$
denote the following semiring on the partially ordered set
$\\{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}\triangleleft{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}\triangleleft{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}\\}$.

  * •

$0:={\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$.

  * •

$+$ is the meet ($\wedge$) according to the subusaging order.

  * •

$1:={\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$.

  * •

$*$ | ${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$ | ${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$ | ${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}$
---|---|---|---
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$ | ${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$ | ${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$ | ${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$ | ${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$ | ${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$ | ${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}$ | ${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$ | ${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}$ | ${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}$

The ${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$
annotation plays only a formal role in this example. Meanwhile,
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$ and
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}$
correspond to the judgement forms $\mathit{true}$ and $\mathit{valid}$ from
PD. Addition being the meet makes it idempotent. Furthermore, it gives us that
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}+{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}={\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}$
— if somewhere we require an assumption to be true, and elsewhere require it
to be valid, then ultimately it must be valid (from which we can deduce that
it is true). Multiplication is designed to make
$\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}}}$
act like PD’s $\Box$. In particular,
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}*{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}={\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}$
says that the valid assumptions are available before and after
$\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}}}$-I,
whereas
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}*{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}={\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}$
says that valid assumptions in the conclusion can be weakened to true
assumptions in the premise. The latter fact does not appear in PD, and will be
excluded from _bottom-up_ derivations.

To keep our notation consistent with that of DILL, we swap the roles of
$\Gamma$ and $\Delta$ in PD compared to what they were in the original paper.
Thus, our PD judgements are of the form $\Gamma;\Delta\vdash
A~{}\mathit{true}$, where $\Gamma$ contains valid assumptions and $\Delta$
contains true assumptions.

######  Proposition 5.6 (PD $\to$
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$).

Given a PD derivation of $\Gamma;\Delta\vdash t:A~{}\mathit{true}$, we can
produce a
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}_{\\_}{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}01\square}}$
derivation of
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}}}}\Gamma,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}}}}\Delta\vdash
A$.

###### Proof.

By induction on the PD derivation. Most PD rules have direct
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
counterparts, noting that variables of any annotation can be discarded and
duplicated because we have both
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$
and
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}+{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}$
for all
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}$.

Care must be taken with the $\Box$I rule. We have, from the induction
hypothesis, a
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
derivation of
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{\Box}}}\Gamma\vdash
A$. By
$\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}}}$-I,
we have
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{\Box}}}\Gamma\vdash\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}}}A$.
To get the desired conclusion, we must use Weak to get
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{\Box}}}\Gamma,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}}}}\Delta\vdash\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}}}A$,
and then Subuse on the variables we just introduced (noting that
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$)
to get
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{\Box}}}\Gamma,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}}}}\Delta\vdash\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}}}A$.
∎

For translating from
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}_{\\_}{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}01\square}}$
to PD, we introduce a similar notion of _bottom-up_ derivations as we did for
DILL. Every
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}_{\\_}{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}01\square}}$
derivation can be translated into bottom-up style, and then be directly
translated into PD.

######  Definition 5.7.

A derivation is said to be
_${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}01\square}$
-bottom-up_ if only the following facts about addition and multiplication are
used, and all proofs of inequalities not at leaves are by reflexivity.

$+$ ${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$ - -
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$ -
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$ -
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}$
- -
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}$
$*$ ${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$ - -
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}$
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$ -
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}$

######  Lemma 5.8.

Every
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}_{\\_}{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}01\square}}$
derivation can be translated into a bottom-up
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}_{\\_}{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}01\square}}$
derivation.

###### Proof.

By induction on the shape of the derivation. Given that addition is a meet, it
is clear that any non-bottom-up uses of addition come from one of the
arguments being greater than the result. Therefore, it is safe to make this
argument smaller in the corresponding premise (via subusaging), before
translating that subderivation. For multiplication, again, there is always a
lesser value of the right argument that will take us from a non-bottom-up fact
to a bottom-up fact with the same left argument and result. ∎

######  Proposition 5.9
($\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
$\to$ PD).

Given a
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}_{\\_}{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}01\square}}$
derivation of
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\square}}}}\Gamma,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}}}}\Delta,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}}}}\Theta\vdash
M:A$ which does not contain types using
$\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}}}$
or
$\oc_{{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}1}}}$,
we can produce a PD derivation of $\Gamma;\Delta\vdash A~{}\mathit{true}$.

###### Proof.

We translate away tensor products and tensor units using 4.2, and translate
the resulting derivation to bottom-up form. The proof proceeds by induction on
the resulting derivation in the obvious way. ∎

For similar reasons as explained at the end of Section 3, the system of Abel
and Bernardy [AB20] is unable to embed PD in this way, as it would prove
$\Box(A\wedge B)\to\Box A\wedge\Box B$, where PD and
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
do not. In fact, this example shows that, even when weakening and contraction
are admissible, with- and tensor-products are distinct in their system in the
presence of modalities.

##  6 Metatheory

The motivating result of the following section is the admissibility of the
single substitution principle. We derive single substitution from simultaneous
substitution (6.10), which we in turn derive from a generic traversal of
syntax (6.9). Our statement of single substitution is somewhat standard, easy
to intuit, and exactly what is called for to show preservation of typing by
$\beta$ rules, whereas our statement of simultaneous substitution is novel and
more abstract, but easier to work with.

*[right=SingleSubst] M : PΓ ⊢A
N : QΓ, rA ⊢B
R ⊴r P \+ Q N{M} : RΓ ⊢B *[right=Subst] ρ: PΓ 0359⊢QΔ
N : QΔ ⊢A N{ρ} : PΓ ⊢A

The notation
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\ext@arrow
0359\Rightarrowfill@{}{\vdash}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Delta$,
which can be thought of as the type of linear assignments from variables in
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Delta$
to terms in
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma$,
will be defined in the following section, and this definition can be seen as a
key contribution of this paper. The overloaded notations $N\\{M\\}$ and
$N\\{\rho\\}$ are hereby defined as operations on intrinsically typed and
usage-checked syntax. Specifically, $N\\{M\\}$ denotes the term $N$ but with
$M$ substituted in for the most recently bound variable, whereas $N\\{\rho\\}$
denotes the result of a generic traversal of $N$ in which its free variables
have been replaced according to the environment $\rho$.

McBride defines _kits_ [McB05, BHKM12], which provide a general method for
giving admissible rules that are usually proven by induction on the
derivation. To produce a kit, we give an indexed family
$\mathbin{\blacklozenge}:\mathrm{Ctx}\times\mathrm{Ty}\to\mathrm{Set}$ and
explain how to inject variables, extract terms, and weaken by new variables
coming from binders. In return, given a type-preserving map from variables in
one context to $\mathbin{\blacklozenge}$-stuff in another (an _environment_),
we get a type-preserving function between terms in these contexts. Such a
function is the intrinsic typing equivalent of an admissible rule.

To make the kit-based approach work in our usage-constrained setting, we make
modifications to both kits and environments. Kits need not support arbitrary
weakening, but only weakening by the introduction of
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$-use
variables. The family $\mathbin{\blacklozenge}$ must also respect
$\trianglelefteq$ of usage contexts. Environments are equipped with a matrix
mapping input usages to output usages.

We prove simultaneous substitution using renaming. We take both renaming and
substitution as corollaries of the _traversal_ principle (Theorem 6.3) yielded
from kits and environments.

Definition of _kit_ s, _environment_ s and traversal are in the module
Specific.Syntax.Traversal.

###  6.1 Kits, Environments, and Traversal

#### Kits

A kit is a structure on $\vdash$-like relations $\mathbin{\blacklozenge}$,
intuitively giving a way in which $\mathbin{\blacklozenge}$ lives between the
usage-checked variable judgement $\mathrel{\mathrlap{\sqsupset}{\mathord{-}}}$
and the typing judgement $\vdash$. The components $\mathit{vr}$ and
$\mathit{tm}$ are basically unchanged from McBride’s original kits. The
component $\mathit{wk}$ only differs in that new variables are given
annotation
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$,
which intuitively marks them as weakenable. The requirement $\mathit{psh}$ is
new, and allows us to fix up usage contexts via skew algebraic reasoning.

######  Definition 6.1 (Kit).

For any
$\mathbin{\blacklozenge}:\mathrm{Ctx}\times\mathrm{Ty}\to\mathrm{Set}$, let
$\operatorname{Kit}(\mathbin{\blacklozenge})$ denote the type of _kits_. A kit
comprises the following functions for all
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}$,
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}$,
$\Gamma$, $\Delta$, and $A$. psh : P ⊴Q →QΓ ◆A →PΓ ◆A vr : PΓ ⊐-A →PΓ ◆A
tm : PΓ ◆A →PΓ ⊢A wk : PΓ ◆A →PΓ, 0Δ ◆A

An inhabitant of
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\mathbin{\blacklozenge}A$
is described as _stuff in
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma$
of type $A$_. In a traversal (for example, simultaneous renaming and
simultaneous substitution), we use $\mathit{tm}$ in var cases to convert stuff
that has come from the environment into terms that replace variables. We use
$\mathit{vr}$ and $\mathit{wk}$ when binding new variables: $\mathit{vr}$
tells us what to add to the environment when it is being extended by a bound
variable, and $\mathit{wk}$ allows us to weaken all the other stuff in the
environment by such newly bound variables.

#### Environments

In simple intuitionistic type theory, an environment is a type-preserving
function from variables in the old context $\Delta$ to stuff in the new
context $\Gamma$: an inhabitant of $\Delta\ni
A\to\Gamma\mathbin{\blacklozenge}A$. The traversal function turns such an
environment into a map between terms, $\Delta\vdash A\to\Gamma\vdash A$.

For
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$,
we want maps of usaged terms
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Delta\vdash
A\to{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\vdash
A$. We can see that an environment of type
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Delta\mathrel{\mathrlap{\sqsupset}{\mathord{-}}}A\to{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\mathbin{\blacklozenge}A$
would be insufficient —
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Delta\mathrel{\mathrlap{\sqsupset}{\mathord{-}}}A$
can only be inhabited when
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}$
is compatible with a basis vector, so our environment would be trivial in more
general cases. Instead, we care about non-usage-checked variables $\Delta\ni
A$.

Our understanding of an environment is that it should simultaneously map all
of the usage-checked variables in
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Delta$
to stuff in
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma$
in a way that preserves usage. As such, we want to map each variable
$j:\Delta\ni A$ not to $A$-stuff in
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma$,
but rather $A$-stuff in
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}_{\\_}j\Gamma$,
where
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}_{\\_}j$
is some fragment of
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}$.
Precisely, when weighted by
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\lvert
j\rangle$, we want these
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}_{\\_}j$
to sum to
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}$,
so as to provide “enough” usage to cover all of the variables $j$. When we
collect all of the
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}_{\\_}j$
into a matrix
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi}$,
we notice that the condition just described is stated succinctly via a vector-
matrix multiplication
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi}$.
This culminates to give us the following:

######  Definition 6.2 (Env).

For any $\mathbin{\blacklozenge}$,
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}$,
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}$,
$\Gamma$, and $\Delta$, where $\Gamma$ and $\Delta$ have lengths $m$ and $n$
respectively, let
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\ext@arrow
0359\Rightarrowfill@{}{\mathbin{\blacklozenge}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Delta$
denote the type of _environments_. An environment comprises a pair of a matrix
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi}:\mathbf{R}^{n\times
m}$ and a mapping of variables $\mathit{act}:(j:(\Delta\ni A))\to(\langle
j\rvert{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi})\Gamma\mathbin{\blacklozenge}A$,
such that
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi}$.

Our main result is the following, which we will instantiate to prove
admissibility of renaming (6.6), subusaging (6.7), and substitution (6.9). The
proof is in subsection 6.5.

######  Theorem 6.3 (traversal, trav).

Given a kit on $\mathbin{\blacklozenge}$ and an environment
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\ext@arrow
0359\Rightarrowfill@{}{\mathbin{\blacklozenge}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Delta$,
we get a function
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Delta\vdash
A\to{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\vdash
A$.

###  6.2 Renaming

We now show how to use traversals to prove that renaming (including weakening)
and subusaging are admissible. This subsection corresponds to the Agda module
Specific.Syntax.Renaming.

######  Definition 6.4 (LVar-kit).

Let
$\mathrel{\mathrlap{\sqsupset}{\mathord{-}}}\textrm{-kit}:\operatorname{Kit}(\mathrel{\mathrlap{\sqsupset}{\mathord{-}}})$
be defined with the following fields.

$\mathit{psh}~{}(\mathit{PQ}:{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}):{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Gamma\mathrel{\mathrlap{\sqsupset}{\mathord{-}}}A\to{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\mathrel{\mathrlap{\sqsupset}{\mathord{-}}}A$:

The only occurrence of the usage context
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}$
in the definition of $\mathrel{\mathrlap{\sqsupset}{\mathord{-}}}$ is to the
left of a $\trianglelefteq$. Applying transitivity in this place gets us the
required term.

$\mathit{vr}:{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\mathrel{\mathrlap{\sqsupset}{\mathord{-}}}A\to{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\mathrel{\mathrlap{\sqsupset}{\mathord{-}}}A:=\mathrm{id}$

.

$\mathit{tm}:{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\mathrel{\mathrlap{\sqsupset}{\mathord{-}}}A\to{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\vdash
A:=\TirName{var}$

.

$\mathit{wk}:{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\mathrel{\mathrlap{\sqsupset}{\mathord{-}}}A\to{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{0}}}\Delta\mathrel{\mathrlap{\sqsupset}{\mathord{-}}}A$:

A basis vector extended by
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}$s is
still a basis vector: if that we have
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\trianglelefteq\langle
i\rvert$ for some $i$, we also have
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}},{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathbf{0}}\trianglelefteq\langle\operatorname{inl}i\rvert$.

Environments for renamings are special in that the matrix
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi}$
can be calculated from the action of the renaming on non-usage-checked
variables.

######  Lemma 6.5 (ren-env).

Given a type-preserving mapping of plain variables $f:\Delta\ni A\to\Gamma\ni
A$ such that
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}I}_{\\_}{f\times\operatorname{id}}$,
we can produce a $\mathrel{\mathrlap{\sqsupset}{\mathord{-}}}$-environment of
type
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\ext@arrow
0359\Rightarrowfill@{}{\mathrel{\mathrlap{\sqsupset}{\mathord{-}}}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Delta$.

###### Proof.

The environment has
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi}:={\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}I}_{\\_}{f\times\operatorname{id}}$,
so the usage condition holds by assumption. Now, $\mathit{act}$ is required to
have type $(j:\Delta\ni A)\to(\langle
j\rvert{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi})\Gamma\mathrel{\mathrlap{\sqsupset}{\mathord{-}}}A$.
Take arbitrary $j:\Delta\ni A$. Then, we have $f~{}j:\Gamma\ni A$, so all that
is left is to show that $f~{}j$ forms a usage-checked variable of type
$(\langle
j\rvert{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi})\Gamma\mathrel{\mathrlap{\sqsupset}{\mathord{-}}}A$.
This amounts to proving $\langle
j\rvert{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi}\trianglelefteq\langle
f~{}j\rvert$. Let $i:\Gamma\ni A$, then we have $(\langle
j\rvert{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi})_{\\_}i\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi}_{\\_}{j,i}={\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}I}_{\\_}{f\,j,i}=\langle
f~{}j\rvert_{\\_}i$. ∎

######  Corollary 6.6 (renaming, ren).

Given a type-preserving mapping of plain variables $f:\Delta\ni A\to\Gamma\ni
A$ such that
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}I}_{\\_}{f\times\operatorname{id}}$,
we can produce a function of type
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Delta\vdash
A\to{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\vdash
A$.

######  Corollary 6.7 (subusaging, subuse).

Given
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}$,
then we have a function
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Gamma\vdash
A\to{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\vdash
A$.

###  6.3 Substitution

Now that we have renaming, we can use it with traversals to prove that
simultaneous well usaged substitution is admissible. This subsection
corresponds to the Agda module Specific.Syntax.Substitution.

######  Definition 6.8 (Tm-kit).

Let $\vdash\textrm{-kit}:\operatorname{Kit}(\vdash)$ be defined with the
following fields.

$\mathit{psh}~{}(\mathit{PQ}:{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}):{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Gamma\vdash
A\to{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\vdash
A$:

This is Corollary 6.7 (subusaging).

$\mathit{vr}:{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\mathrel{\mathrlap{\sqsupset}{\mathord{-}}}A\to{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\vdash
A:=\TirName{var}$

.

$\mathit{tm}:{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\vdash
A\to{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\vdash
A:=\mathrm{id}$

.

$\mathit{wk}:{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\vdash
A\to{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{\mathbf{0}}}\Delta\vdash
A$:

We use Corollary 6.6 (renaming), with $f:\Gamma\ni A\to\Gamma,\Delta\ni A$
being the embedding $\operatorname{inl}$. It remains to check that
$({\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}},{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathbf{0}})\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}I}_{\\_}{\operatorname{inl}\times\operatorname{id}}$.
We prove this pointwise. Let $i:\Gamma,\Delta\ni A$, and take cases on whether
$i$ is from $\Gamma$ or from $\Delta$. If $i=\operatorname{inl}i^{\prime}$ for
an $i^{\prime}:\Gamma\ni A$, we must show that
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}_{\\_}{i^{\prime}}\trianglelefteq({\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}I}_{\\_}{\operatorname{inl}\times\operatorname{id}})_{\\_}{\operatorname{inl}i^{\prime}}$.
But we have the following.

${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}_{\\_}{i^{\prime}}\trianglelefteq({\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}I})_{\\_}{i^{\prime}}=\sum_{\\_}{j:\Gamma\ni
A}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}_{\\_}j{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}I}_{\\_}{j,i^{\prime}}=\sum_{\\_}{j:\Gamma\ni
A}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}_{\\_}j{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}I}_{\\_}{\operatorname{inl}j,\operatorname{inl}i^{\prime}}=({\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}I}_{\\_}{\operatorname{inl}\times\operatorname{id}})_{\\_}{\operatorname{inl}i^{\prime}}.$

If $i=\operatorname{inr}i^{\prime}$ for an $i^{\prime}:\Delta\ni A$, we must
show that
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}\trianglelefteq({\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}I}_{\\_}{\operatorname{inl}\times\operatorname{id}})_{\\_}{\operatorname{inr}i^{\prime}}$.
But we have the following.

${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}0}\trianglelefteq({\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathbf{0}})_{\\_}{i^{\prime}}=\sum_{\\_}{j:\Gamma\ni
A}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}_{\\_}j{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathbf{0}}_{\\_}{j,i^{\prime}}=\sum_{\\_}{j:\Gamma\ni
A}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}_{\\_}j{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}I}_{\\_}{\operatorname{inl}j,\operatorname{inr}i^{\prime}}=({\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}I}_{\\_}{\operatorname{inl}\times\operatorname{id}})_{\\_}{\operatorname{inr}i^{\prime}}.$

We define a simultaneous substitution as an environment of terms. Expanding
definitions, this means that a simultaneous substitution from
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma$
to
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Delta$
is a matrix
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi}$
such that
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi}$,
and for each variable $j$ of type $A$ in $\Delta$, a term $(\langle
j\rvert{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi})\Gamma\vdash
A$.

######  Corollary 6.9 (substitution, sub).

Given an environment of type
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\ext@arrow
0359\Rightarrowfill@{}{\vdash}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Delta$
(i.e., a well usaged simultaneous substitution), we get a function of type
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Delta\vdash
A\to{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\vdash
A$.

###  6.4 Single substitution

######  Corollary 6.10 (single substitution).

Given
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}+{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}$
and terms
$M:{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\vdash
A$ and
$N:{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Gamma,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}A\vdash
B$, we can produce a term deriving
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\Gamma\vdash
B$.

###### Proof.

By traversal (specifically, simultaneous substitution, 6.9) on $N$. We must
produce an environment of type
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\Gamma\ext@arrow
0359\Rightarrowfill@{}{\vdash}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Gamma,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}A$.
Let
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi}:=\left(\begin{array}[]{c}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathbf{I}}\\\
\hline\cr{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\end{array}\right)$
and notice that
$({\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}},{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}){\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi}={\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}+{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}r}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}$,
so our inequality assumption is enough to prove the inequality requirement of
environments. For the terms to substitute in, we choose the first
$\lvert\Gamma\rvert$ terms to be their respective variables, and the last term
to be $M$. ∎

###  6.5 Proof of traversal

The proof of the traversal theorem follows the same structure as in McBride’s
article, extended with proof obligations to show that we are correctly
respecting the usage annotations. We must first prove a lemma that shows that
environments can be pushed under binders.

######  Lemma 6.11 (bind, bind).

Given a kit on $\mathbin{\blacklozenge}$, we can extend an environment of type
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\ext@arrow
0359\Rightarrowfill@{}{\mathbin{\blacklozenge}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Delta$,
to an environment of type
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\Theta\ext@arrow
0359\Rightarrowfill@{}{\mathbin{\blacklozenge}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Delta,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\Theta$.

###### Proof.

Let the environment we are given be
$({\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi}:\mathbf{R}^{n\times
m},\mathit{act}:(j:\Delta\ni A)\to(\langle
j\rvert{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi})\Gamma\mathbin{\blacklozenge}A)$,
with
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi}$.
We are trying to construct
$({\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi^{\prime}}:\mathbf{R}^{(n+o)\times(m+o)},\mathit{act^{\prime}}:(j:\Delta,\Theta\ni
A)\to(\langle
j\rvert{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi^{\prime}})(\Gamma,\Theta)\mathbin{\blacklozenge}A)$,
with
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}},{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\trianglelefteq({\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}},{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}){\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi^{\prime}}$.
Let
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi^{\prime}}:=\left(\begin{array}[]{c|c}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi}&{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathbf{0}}\\\
\hline\cr{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathbf{0}}&{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathbf{I}}\end{array}\right).$
With this definition, our required condition splits into the easily checked
conditions
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi}+{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathbf{0}}$
and
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathbf{0}}+{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathbf{I}}$.
For $\mathit{act^{\prime}}$, we take cases on whether $j$ is from $\Delta$ or
from $\Theta$. In the $\Delta$ case, $\mathit{act}$ gets us an inhabitant of
$(\langle
j\rvert{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi})\Gamma\mathbin{\blacklozenge}A$.
Notice that $\langle
j\rvert{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi^{\prime}}=\langle
j\rvert{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi},{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathbf{0}}$,
so we want to get from $(\langle
j\rvert{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi})\Gamma\mathbin{\blacklozenge}A$
to $(\langle
j\rvert{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi})\Gamma,{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathbf{0}}\Theta\mathbin{\blacklozenge}A$.
We can get this using $\mathit{wk}$ from our kit. In the $\Theta$ case, notice
that $\langle
j\rvert{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi^{\prime}}={\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathbf{0}},\langle
j\rvert$. In other words, $\langle
j\rvert{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi^{\prime}}$
is a basis vector, so we actually have usage-checked $(\langle
j\rvert{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi^{\prime}})(\Gamma,\Theta)\mathrel{\mathrlap{\sqsupset}{\mathord{-}}}A$.
Thus, we can use $\mathit{vr}$ from our kit to get $(\langle
j\rvert{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi^{\prime}})(\Gamma,\Theta)\mathbin{\blacklozenge}A$,
as required. ∎

######  Theorem 6.3 (traversal, trav).

Given a kit on $\mathbin{\blacklozenge}$ and an environment
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\ext@arrow
0359\Rightarrowfill@{}{\mathbin{\blacklozenge}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Delta$,
we get a function
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Delta\vdash
A\to{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\vdash
A$.

###### Proof.

By induction on the syntax of $M$. In the var $x$ case, where
$x:{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\Delta\mathrel{\mathrlap{\sqsupset}{\mathord{-}}}A$:
By definition of $\mathrel{\mathrlap{\sqsupset}{\mathord{-}}}$, we have that
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}\trianglelefteq\langle
j\rvert$ for some $j$. Applying the action of the environment, we have
$(\langle
j\rvert{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi})\Gamma\mathbin{\blacklozenge}A$.
We then have
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\trianglelefteq{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi}\trianglelefteq\langle
j\rvert{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi}$,
so using the fact that stuff appropriately respects subusaging
($\mathit{psh}$), we have
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\mathbin{\blacklozenge}A$.
Finally, using $\mathit{tm}$, we get a term
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}\Gamma\vdash
A$, as required.

Non-var cases are generally handled in the following way. If the input usage
context
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}$
is split up into a linear combination of zero or more usage contexts
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}_{\\_}{i}$,
obtain a similar splitting of
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}$
by setting
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}_{\\_}{i}:={\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}_{\\_}{i}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\Psi}$.
This works out because of the linearity of matrix multiplication (in
particular, multiplication respects operations on the left). This yields
environments of type
${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{P}}_{\\_}{i}\Gamma\ext@arrow
0359\Rightarrowfill@{}{\mathbin{\blacklozenge}}{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{Q}}_{\\_}{i}\Delta$
for the subterms to use with the inductive hypothesis. If any subterms bind
variables, apply 6.11 as appropriate. ∎

##  7 Conclusion

We have extended McBride’s method of kits and traversals to proving
admissibility of renaming, subusaging, and substitution for the usage-
annotated calculus
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$.
In doing so, we have discovered that only skew semirings are required, and the
importance of linear algebra for stating and proving these results. We have
shown that
$\lambda{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}\mathcal{R}}$
is capable of representing several well known linear and modal type theories
by instantiation to different semirings.

Our work is similar in spirit to the work of Licata, Shulman, and Riley
[LSR17], which gives a proof of cut elimination for a large class of
substructural single-conclusion sequent calculi. The class of natural
deduction systems we consider here is likely less general, but is not directly
comparable. In particular, we assume contexts form a commutative monoid up to
admissible derivations, whereas Licata, Shulman, and Riley allow contexts to
be composed of arbitrary finitiary operators. Our results are also different —
our simultaneous substitution as opposed to their cut elimination. We leave a
complete comparison to future work. They have not mechanised their work.

We are currently building on this work to generalise the framework of Allais
_et al._ [AAC+20] to include usage annotations, allowing generic metatheory
and semantics for an even wider class of substructural calculi.

#### Acknowledgements

We are thankful for comments from Guillaume Allais and Michael Arntzenius.

## References

  * [1]
  * [AAC+20] Guillaume Allais, Robert Atkey, James Chapman, Conor McBride & James McKinna (2020): _A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs_.  Accepted for JFP.
  * [AB20] Andreas Abel & Jean-Philippe Bernardy (2020): _A Unified View of Modalities in Type Systems_.  Proc. ACM Program. Lang. 4(ICFP), 10.1145/3408972.  Available at https://doi.org/10.1145/3408972.
  * [All18] Guillaume Allais (2018): _Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic_.  In: TYPES 2017, pp. 1:1–1:22, 10.4230/LIPIcs.TYPES.2017.1.
  * [Bar96] Andrew Barber (1996): _Dual Intuitionistic Linear Logic_.  Technical Report, University of Edinburgh.
  * [BBPH93] P. N. Benton, Gavin M. Bierman, Valeria de Paiva & Martin Hyland (1993): _A Term Calculus for Intuitionistic Linear Logic_.  In: Typed Lambda Calculi and Applications, LNCS 664, Springer, pp. 75–90, 10.1007/BFb0037099.
  * [BGMZ14] A. Brunel, M. Gaboardi, D. Mazza & S. Zdancewic (2014): _A Core Quantitative Coeffect Calculus_.  In: ESOP 2014, pp. 351–370.
  * [BHKM12] Nick Benton, Chung-Kil Hur, Andrew Kennedy & Conor McBride (2012): _Strongly typed term representations in Coq_.  J. of Autom Reasoning 49(2), 10.1007/s10817-011-9219-0.
  * [CLR19] Kaustuv Chaudhuri, Leonardo Lima & Giselle Reis (2019): _Formalized meta-theory of sequent calculi for linear logics_.  Theor. Comput. Sci. 781, pp. 24–38, 10.1016/j.tcs.2019.02.023.
  * [Cra10] Karl Crary (2010): _Higher-Order Representation of Substructural Logics_.  SIGPLAN Not. 45(9), p. 131–142, 10.1145/1932681.1863565.
  * [GS14] Dan R. Ghica & Alex I. Smith (2014): _Bounded Linear Types in a Resource Semiring_.  In: ESOP 2014, pp. 331–350.
  * [Lau18] Olivier Laurent (2018): _Preliminary Report on the Yalla Library_.  Available at https://perso.ens-lyon.fr/olivier.laurent/yalla/.  Coq Workshop.
  * [LSR17] Daniel R. Licata, Michael Shulman & Mitchell Riley (2017): _A Fibrational Framework for Substructural and Modal Logics_.  In: FSCD 2017, pp. 25:1–25:22, 10.4230/LIPIcs.FSCD.2017.25.
  * [McB05] Conor McBride (2005): _Type-preserving renaming and substitution_.  Available at http://www.strictlypositive.org/ren-sub.pdf.
  * [OLE19] Dominic A. Orchard, Vilem Liepelt & Harley Eades (2019): _Quantitative program reasoning with graded modal types_.  Proceedings of the ACM on Programming Languages 3\.
  * [PD99] Frank Pfenning & Rowan Davies (1999): _A Judgmental Reconstruction of Modal Logic_.  In: Mathematical Structures in Computer Science, p. 2001.
  * [POM14] Tomas Petricek, Dominic A. Orchard & Alan Mycroft (2014): _Coeffects: a calculus of context-dependent computation_.  In: ICFP 2014, pp. 123–135.
  * [PW99] James Power & Caroline Webster (1999): _Working with Linear Logic in Coq_.  12th International Conference on Theorem Proving in Higher Order Logics (Work-in-progress paper).
  * [RBPKV20] Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers & Eelco Visser (2020): _Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages_.  In: CPP 2020, pp. 284–298, 10.1145/3372885.3373818.
  * [RP10] J. Reed & B. C. Pierce (2010): _Distance Makes the Types Grow Stronger_.  In P. Hudak & S. Weirich, editors: ICFP 2010, pp. 157–168.
  * [Szl12] Kornél Szlachányi (2012): _Skew-monoidal categories and bialgebroids_.  Advances in Mathematics 231(3-4), pp. 1694–1730, 10.1016/j.aim.2012.06.027.
  * [Wad92] Philip Wadler (1992): _There’s no substitute for linear logic_.  In: 8th International Workshop on the Mathematical Foundations of Programming Semantics.
  * [XORN17] Bruno Xavier, Carlos Olarte, Giselle Reis & Vivek Nigam (2017): _Mechanizing Focused Linear Logic in Coq_.  In: 12th Workshop on Logical and Semantic Frameworks, with Applications, ENTCS 338, Elsevier, pp. 219–236, 10.1016/j.entcs.2018.10.014.