prove that $\elctxfp\tm= \lctxp{\cuta\val\var\var} \in \sn\toss$. By induction on $\tm \in \sn\toss$ we show that all the reducts of $\tmtwo$ are in $\sn\toss$. If $\elctxfp\tm \toss \tm$ by reducing the cut on $\var$,
then the reduct is $\tm$, which is in $\sn\toss$ by hypothesis. Otherwise, $\elctxfp\tm$ makes a step in $\val$, or in
$\lctx$, or involving both $\lctx$ and $\val$. The same step can be done on $\tm$, and thus by the reduct is in

* Let $\lctxp{\cuta\ctxhole\var\tm}\in \elctx$, so that $\elctxfp\vartwo = \lctxp{\cuta\vartwo\var\tm}$. If
$\elctxfp\vartwo \toss \lctxp{\cutsub\vartwo\var\tm}$ then the reduct is in $\sn\toss$ by the hypothesis on $\elctx$.
Otherwise, $\elctxfp\vartwo$ makes a step in $\tm$, or in $\lctx$, or involving both $\lctx$ and $\tm$. The same step
can be done on $\lctxp\tm$ (we rely on sn-renaming), and thus by the reduct is in $\sn\toss$.

If $\settone$ is a generator then $\settone^\bot$ is a candidate.

We first consider the case $\settone \subseteq \lltermsform$. Properties:

* Strong normalization: let  $\elctx = \lctxtwop{\cuta\ctxhole\var\tmtwo} \in
\settone^\bot$ and $\tm= \lctxp\val\in\settone \neq\emptyset$. By duality, $\elctxfp\tm \in\sn\toss$. By
sn-to-subtermsone, $\elctx\in\sn\toss$.

* Variables (which subsumes non-emptyness):  let $\tm = \lctxp\val\in \settone$ and $\cuta\ctxhole\var\var\in
\elvars_{\form}$. By $\settone \subseteq \sn\toss$ and sn-to-subtermstwo we obtain
$\lctxp{\cuta\val\var\var}\in\sn\toss$, that is, $\cuta\ctxhole\var\var \in \settone^{\bot}$.

* Bi-orthogonal: by the by-orthogonal property of duality (basic-prop-duality).

Now, the case $\settone\subseteq\elctxsform$.

* Strong normalization: let  $\tm= \lctxp\val \in
\settone^\bot$ and $\elctx = \lctxtwop{\cuta\ctxhole\var\tmtwo} \in\settone\neq\emptyset$. By duality, $\elctxfp\tm
\in\sn\toss$. By sn-to-subtermsone, $\tm\in\sn\toss$.

* Variables (which subsumes non-emptyness):  let $\elctx \in\settone$ and $\var\in \vars_{\form}$. By
$\settone \subseteq \sn\toss$ and sn-to-subtermsthree we obtain $\elctxfp\var\in\sn\toss$, that is, $\var
\in \settone^{\bot}$.

* Bi-orthogonal: by the by-orthogonal property of duality (basic-prop-duality).

We now associate to every formula $\form$ a set $\settone_{\redc\form}$ that we then prove to be a generator, so that
its bi-orthogonal is a candidate by generators-give-red-cands. A minor unusual point is that we define the set
$\settone_{\redc\aform}$ for the atomic formula is the set of multiplicative variables. The literature rather defines it
as $\lltermsp\aform\cap\sn{\toss}$, which is wacky, as this is actually what the method is meant to prove!

[Formulas candidates]
Set $\redc{\form} \defeq \settone_{\redc\form}^{\bot\bot}$, where
$\settone_{\redc\form}$ is defined by induction on $\form$:

* $\settone_{\redc\aform} \defeq \mvars$;

* $\settone_{\redc{\form\tens\formtwo}} \defeq \set{\pair\tm\tmtwo\ |\
\tm\in\redc{\form}, \tmtwo\in\redc{\formtwo}, \pair\tm\tmtwo \mbox{ is \proper}}$;

* $\settone_{\redc{\form\lolli\formtwo}} \defeq \left\{\la\var\tm\
\Bigg|\ \begin{array}{l}
\multiform, \var\hastype\form\vdash\tm\hastype\formtwo, \\
\lctxp{\cuta\val\var\tm} \in\redc{\formtwo}\, \forall\tmtwo =\lctxp\val\in\redc\form,
\mbox{ and }\\
\la\var\tm\mbox{ is \proper}
\end{array}\right\}$;

* $\settone_{\redc{\bang\form}} \defeq \set{\bang\tm\ |\ \tm\in\redc{\form},  \bang\tm\mbox{ is
\proper}}$.

The proof of that $\redc{\form}$ is a candidate for every formula $\form$ requires a lemma for the lolli case.

If $\redc\form\subseteq\sn\toss$ and $\vars_\formtwo \subset \redc\formtwo$ then $\settone_{\redc{\form\lolli\formtwo}} \neq \emptyset$.

We show that $\la\var\suba\mvar\var\vartwo\vartwo \in \settone_{\redc{\form\lolli\formtwo}}$. The idea is that the body $\suba\mvar\var\vartwo\vartwo$ of that abstraction is the smallest term $\tm$ verifying the typing requirement $\multiform, \var\hastype\form\vdash\tm\hastype\formtwo$ when $\form\neq\formtwo$. By definition, $\la\var\suba\mvar\var\vartwo\vartwo \in \settone_{\redc{\form\lolli\formtwo}}$ holds if $\lctxp{\cuta\val\var \suba\mvar\var\vartwo\vartwo} \in \redc{\formtwo}$ for every $\lctxp\val\in\redc\form$, that is,  $\elctxfp{\lctxp{\cuta\val\var \suba\mvar\var\vartwo\vartwo}} \in \sn\toss$ for every $\elctx\in\redc\formtwo^{\bot}$.
By hypothesis, $\vars_{\formtwo} \subseteq \redc\formtwo$, and duality gives $\elctxfp\vartwo \in \sn\toss$. By hypothesis, we also have $\lctxp\val \in \sn\toss$. The proof is in two steps:

* Proving $\tm \defeq \elctxfp{\lctxp{\suba\mvar\val\vartwo\vartwo}}\in \sn\toss$: note that the two components $\lctxp\val$ and $\elctxfp{\vartwo}$ cannot interact in any way, so that every step of $\tm$ comes from a step of either $\lctxp\val$ or $\elctxfp{\vartwo}$, as in the proof of the extension property. Formally, the proof is by induction on $(\lctxp\val \in \sn\toss, \elctxfp{\vartwo} \in \sn\toss)$.

* Proving $\tmtwo \defeq \elctxfp{\lctxp{\cuta\val\var\suba\mvar\var\vartwo\vartwo} } \in \sn\toss$: note that  $\tm = \elctxfp{\lctxp{\suba\mvar\val\vartwo\vartwo}} = \cutsub\val\var\elctxfp{\lctxp{\suba\mvar\var\vartwo\vartwo}}$, thus by root cut expansion we obtain $\cuta\val\var\elctxfp{\lctxp{\suba\mvar\var\vartwo\vartwo}} \in \sn\toss$. By structural stability, $\cuta\val\var\elctxfp{\lctxp{\suba\mvar\var\vartwo\vartwo}} \cuteq \tmtwo \in \sn\toss$.

Therefore, $\la\var\suba\mvar\var\vartwo\vartwo \in \settone_{\redc{\form\lolli\formtwo}} \neq \emptyset$.

The proof of the next proposition is simple and yet tricky: by induction on $\form$, it uses
generators-give-red-cands to prove 2 from 1, and 3 from 2, but it also needs 3 (on sub-formulas) to prove 1.

Let $\form$ be a  formula.

* Generators: $\settone_{\redc\form}$ is a generator.

* Dual candidates: $\redc{\form}^{\bot}$ is a  candidate.

* Candidates: $\redc{\form}$ is a candidate.

Reducibility and Adequacy. In the following notion of reducible derivations, the rigid structure of terms
forces an order between the assignments in the typing context $\multiform$, that is, it treats $\multiform$ as a
list rather than as a multi-set. The proof of adequacy then considers that the sequent calculus comes with an
exchange rule, treated by one of the cases.
[Reducible derivations]
Let $\tderiv\pof\multiForm \vdash \tm\hastype \form$ be a typing derivation, and  $\multiForm =
\var_{1}\hastype\formtwo_{1},\mydots,
\var_{k}\hastype\formtwo_{k} $. Then $\tderiv$ is reducible if
$\cuta{\val_{1}}{\var_{1}}\ldots \cuta{\val_{k}}{\var_{k}} \tm \in \redc\form$
for every value
$\val_{i}\in\settone_{\redc{\formtwo_{i}}}$ such that the introduced cuts are independent, that is,
$\fv{\val_{i}} \cap \dom\multiForm = \emptyset$.
To ease notations, we shorten $\cuta{\val_{1}}{\var_{1}}\ldots \cuta{\val_{k}}{\var_{k}} \tm$ to

Before proving adequacy, we provide an equivalent but slightly extended reformulation of the reducibility clause, in
which the variables $\var_i$ are cut with arbitrary terms, not necessarily with values. The variant is used in the below
proof of adequacy when dealing with: the left rules having $\lctxp\val$ as hypothesis (cut and subtraction) or the
rewriting rule of which has to split terms on-the-fly (par and dereliction), and in the lolli case, because split terms
are used in the definition of $\settone_{\redc{\form\lolli\formtwo}}$.
Notations: if $\tmtwo = \lctxp\val$, we use $\cuta{\ctxholep\tmtwo}\var\tm$ for $\lctxp{\cuta\val\var\tm}$, and
$\cuta{\ctxholep{\tmtwo_{i}}}{\var_{i}}_{\multiForm}\tm$ for $\cuta{\ctxholep{\tmtwo_{1}}}{\var_{1}}\ldots
\cuta{\ctxholep{\tmtwo_{k}}}{\var_{k}} \tm$.

Let $\tderiv\pof \multiForm \vdash \tm\hastype \form$ with $\multiForm = \var_{1}\hastype\formtwo_{1},\mydots,
\var_{k}\hastype\formtwo_{k} $  be a typed derivation. Then $\tderiv$ is reducible if and
only if $\cuta{\ctxholep{\tmtwo}}{\var_{i}}_{\multiForm}\tm \in \redc\form$ for every $\tmtwo\in \redc{\formtwo_{i}}$
such that the introduced cuts are independent.

Let $\tderiv \pof \multiForm \vdash \tm\hastype \form$ a type derivation. Then $\tderiv$ is reducible.

Let $\tm$ be a typable term. Then $\tm\in\sn\toss$ and $\tm\in\sn\toms$.

Since $\tm$ is typable, we have $\tderiv\pof\var_{1}\hastype\formtwo_{1},\ldots, \var_{k}\hastype\formtwo_{k} \vdash
\tm\hastype \form$, for some derivation $\tderiv$.  By adequacy (adequacy), $\tderiv$ is reducible. By
formulas-give-redc, $\var_{i} \in \redc{\formtwo_{i}}$
for $i\in\set{1,\ldots,k}$ and
$\cuta\ctxhole\vartwo\vartwo \in \redc\form^{\bot}$. Let $\tm = \lctxp\val$. By reducibility of $\tderiv$,
$\tmtwo\defeq\cuta{\var_{1}}{\var_{1}}\ldots\cuta{\var_{k}}{\var_{k}}\lctxp{\cuta{\val}\vartwo\vartwo} \in \sn\toss$.
Note that $\tmtwo \toss^* \tm$, thus $\tm\in\sn\toss$. By PSN (PSN), $\tm\in\sn\toms$.

§ CONCLUSIONS

This work lifts Accattoli and Kesner's linear substitution calculus to the sequent calculus for IMELL via 3 generalizations: adding explicit (non-)linearity, a simple form of pattern matching ($\tens$), and replacing applications with subtractions.

We provide 3 main contributions for the new exponential substitution calculus. Firstly, we show that IMELL untyped exponentials, in contrast to the classical case, are strongly normalizing. Secondly, we define the good evaluation strategy and show that it has the sub-term property, obtaining the first polynomial cost model for IMELL. Thirdly, we provide elegant proofs of confluence,  strong normalization, and preservation of strong normalization.

Methodologically, we provide an extensive study of linear logic cut elimination that is not based on proof nets.

The Next Step. In the $\l$-calculus, the number of (leftmost) $\beta$-steps is a polynomial cost model <cit.>. Since one $\beta$-steps is simulated in IMELL by one multilicative step (actually a $\tololli$ step) followed by possibly many exponential steps, it means that one can count only the number of multiplicative (or even $\tololli$) steps, that is, one can count $0$ for exponential steps. Such a surprising fact is enabled by a sophisticated technique called useful sharing <cit.>. Can useful sharing be generalized to the ESC as to turn the number of multiplicative/$\tololli$ good steps into a polynomial time cost model? For this, termination of untyped exponentials is mandatory, thus, the results of this paper suggest that it might be possible. Still, the question is far from obvious, as in the $\l$-calculus there is a strong, hardcoded correlation between multiplicatives and exponentials, not present in IMELL. In the standard call-by-name/value encodings of $\l$-calculus in IMELL, indeed, multiplicatives and exponentials connectives rigidly alternate, while IMELL enables consecutive exponentials, as in $\bang\bang\form$, allowing wilder exponential behavior.

Further Future Work Beyond refining the cost model, there are many possible directions for future work. Is the good strategy normalizing on untyped (clash-free) terms (that is, does it reach a cut-free reduct whenever there is one)? Good redexes are not stable by cut/left-equivalence: is there a generalization that is stable? Is it possible to measure good steps via relational semantics/multi types, refining the work of de Carvalho et al. <cit.>? Being a generalization of linear head reduction, does the good strategy have a similar connection to game semantics (see <cit.>)? Can the good strategy be exploited for implicit computational complexity? Can the left context/value splitting be given a logical status? What about a LSC/cost-aware approach for the additives?

§ ACKNOWLEDGMENTS

To Delia Kesner, for asking the question that triggered this work. To Giulio Guerrieri, Claudio Sacerdoti Coen, and Olivier Laurent for feedback.

§ APPENDIX OF SN (TYPED STRONG NORMALIZATION)

§ APPENDIX OF INTRO (INTRODUCTION)

Here we give an example fo size exploding family for least level reduction $\Rew{ll}$, as hinted at in the introduction.

Size Exploding Family For the time being, let's consider untyped proof nets. Consider the following net:

that in the ESC could be writen as $\bang\pair{\dera\evar\mvar\mvar} {\dera\evar\mvartwo\mvartwo}$ (but in the ESC there is no way to specify that the contraction is outside the box, which is important in this example). Now define the following two families of nets:

\rho_0 & \defeq & \pi
\\
\rho_{n+1} & \defeq & \input{figure-size-exploding-family}
\\
\\
\sigma_0 & \defeq & \pi
\\
\sigma_{n+1} & \defeq & \input{figure-size-exploding-result}
\end{array}$

It is easily seen that $\rho_n$ reduces by cut elimination at level 0 to $\sigma_n$ in a number of steps linear in $n$ if one always reduces the leftmost cut at level 0, and that the size of $\sigma_n$ is exponential in $n$. The net $\rho_n$ is typable, but with types of size exponential in $n$. By replacing the axioms in $\pi$ with $1$ for each of their right conclusions and $\bot\parr\bot$ for each of their left conclusions one obtains a proof net typable without constant size types.

§ APPENDIX OF TOWARDS (TOWARDS EXPONENTIAL AS SUBSTITUTION)

In this appendix we motivate some design choices behind the ESC, namely:

* Split syntax, that is, having split cuts and subtractions, that is, of restritcting the left subterm of cuts and subtractions to be a value. To distinguish the two approaches, we refer to the ESC as to the Split ESC and to the variant presented in this section as to the Plain ESC.

* Unusual cut elimination for exponential axioms: as we mentioned in the body of the paper there is a third difference between the ESC and more traditional cut eliminations for linear logic (beyond LSC-style duplications and the absence of the commutative rule for promotions), which concerns cut elimination for exponential axioms.

* The avoidance of a Curien-Herbelin syntax for the ESC.

§.§ The Split $vs$ the Plain ESC

The Plain ESC, where cuts and subtractions are not necessarily split, is given by (note the use of $\tmtwo$ rather than $\val$ in $\cuta\tmtwo\var\tm$ and $\suba\mvar\tmtwo\var \tm$):

\textsc{Multiplicative values}
& \mval & \grameq & \mvar \mid \pair\tm\tmtwo \mid \la\var\tm
\\
\textsc{Exponential values}
& \exval & \grameq & \evar \mid  \bang\tm
\\
\textsc{Terms}
& \tm,\tmtwo,\tmthree & \grameq & %\star &
\mval \mid \exval \mid
\cuta\tmtwo\var\tm \mid \para\mvar\var\vartwo \tm \mid \suba\mvar\tmtwo\var \tm \mid \dera\evar\var \tm
\end{array}$

The grammars for contexts are as expected and there is no need of value contexts anymore.

The typing rules for cut and subtraction are the following, natural ones (and all the other typing rules are as for the ESC):

$\multiForm   \vdash \tmtwo \hastype \form$
$\multiFormtwo, \var\hastype \form \vdash \tm\hastype\formtwo$
$  \multiForm, \multiFormtwo\vdash \cuta\tmtwo\var\tm \hastype\formtwo$

$  \multiForm \vdash \tmtwo\hastype\form$
$  \multiFormtwo, \var\hastype\formtwo \vdash \tm\hastype\formthree$
$ \lolliLeftRule $
$  \multiForm, \multiFormtwo, \mvar\hastype \form \lolli \formtwo \vdash \suba\mvar\tmtwo\var  \tm \hastype\formthree$

The rewriting rules now have to do an on-the-fly splitting of the left sub-term in the cut. On the other hand, they no longer have to split the content of tensor pairs, abstractions, and promotions to write the reduct, as in the Split ESC.

\multicolumn{3}{c}{\textsc{Top-level multiplicative rules}}
\\
\cuta{\lctxp\mval}\mvar\mctxfp\mvar & \rtoaxmone & \lctxp{\mctxfp\mval}
\\
\cuta{\lctxp\mvartwo}\mvar\tm & \rtoaxmtwo & \lctxp{\cutsub\mvartwo\mvar\tm}
\\
%& \Rew{1} &
\cuta{\lctxp{\pair\tmtwo\tmthree}}\mvar \mctxp{\para\mvar\vartwo\var \tm}
& \rtotens &
\lctxp{ \mctxp{\cuta\tmtwo\vartwo \cuta\tmthree\var\tm} }
\\
\cuta{\lctxp{\la\vartwo\tmthree}}\mvar \mctxp{\suba\mvar\tmtwo\var  \tm}
& \rtololli &
\lctxp{\mctxp{ \cuta\tmtwo\vartwo \cuta\tmthree\var \tm }}
\\
\\
\multicolumn{3}{c}{\textsc{Small-step top-level exponential rule}}
\\
\cuta{\lctxp\exval}\evar \tm & \rtoess & \lctxp{\cutsub\exval\evar\tm}
\\
\\
\multicolumn{3}{c}{\textsc{Micro-step top-level exponential rules}}
\\
\cuta{\lctxp{\exval}} \evar \ctxfp{\evar}
& \rtoaxeone &
\lctxp{\cuta{\exval}\evar\ctxfp{\exval}}
\\
\cuta{\lctxp{\evartwo}}\evar\ctxp{\dera\evar\var \tm}
& \rtoaxetwo &
\lctxp{\cuta{\evartwo}\evar\ctxp{\dera\evartwo\var \tm}}
\\
\cuta{\lctxp{\bang\tmtwo}}\evar\ctxp{\dera\evar\var \tm}
& \rtobder &
\lctxp{\cuta{\bang\tmtwo}\evar\ctxp{\cuta\tmtwo\var \tm}}
\\
\cuta{\lctxp{\exval}}\evar \tm
& \rtow &
\lctxp{\tm} \ \ \ \  \mbox{if }\evar\notin\fv\tm
\end{array}$

Reasons for Prefering the Split ESC to the Plain ESC At the inception of this work, we actually worked with the Plain ESC. There were however some unpleasant technical points that pushed us to turn towards the Split ESC. Some of them follows.

* Local confluence: the proof of confluence given in the paper adapts smoothly to the plain calculus, which is then confluent. A close inspection of the local confluence diagrams, however, reveals the following local diagram, where we assume that $\evar\notin\fv\tmtwo$ and that $\exval = \ctxfp\evartwo$ for some $\ctx$:

\[\begin{array}{cccccc}
\cuta{\cuta{\lctxtwop\exvaltwo}\evartwo\lctxp{\exval}}\evar \tmtwo
& \rtobw &
\cuta{\lctxtwop\exvaltwo}\evartwo\lctxp \tmtwo
\\
& &\downarrow_{\ems+}
\\
\downarrow_{!}&& \lctxtwop{\cutsub{\exvaltwo}\evartwo\lctxp\tmtwo}\\
& & \uparrow_{\ems+}
\\
\cuta{\lctxtwop{\cuta{\exvaltwo}\evartwo\lctxp{\exvalthree}}}\evar \tmtwo
& \rtow &
\lctxtwop{\cuta{\exvaltwo}\evartwo\lctxp\tmtwo}
\end{array}\]

What happens is that, if one substitutes $\exvaltwo$ for $\evartwo$ in $\exval$ before erasing the cut on $\evar$, the left context $\lctxtwo$ ends up out of the cut on $\evartwo$, when the cut on $\evar$ is erased. The diagram can be closed, but it requires to develop the whole cut on $\evartwo$, which is a small-step closure, while the diagram is generated by a micro-step span. In the Split ESC, this diagram is ruled out, simply because $\lctxtwo$ cannot be inside the cut for $\evartwo$ from the start. In fact, in the Split ESC local diagrams never require the small-step full development of a cut in order to be closed.

* Defining good and bad redexes: in the Plain ESC it is harder to define a meaningful good strategy. The good strategy is designed having as guiding principle that it should satisfy an untyped normalization theorem, that is, that the good strategy reaches the normal form from $\tm$ whenever $\tm$ is normalizable, even for untyped terms (one has to require clash-freeness). The good strategy does satisfy an untyped normalization theorem, the proof of which is non-trivial and omitted for lack of space (it will be the topic of a forthcoming paper). One of the key properties needed in order to prove untyped normalization is the isolation of bad steps, that is, the fact that bad redexes cannot create good redexes nor turn bad redexes into good ones. In the Plain ESC, the isolation of bad steps does not hold. Consider the bad Plain ESC step:

\[\tm = \cuta{\cuta{\tmthree}\evarthree\exval}\evar \cuta{\bang\evar}\evartwo\tmfour \ \ \toaxeone \cuta{\tmthree}\evarthree\cuta{\exval}\evar \cuta{\bang\exval}\evartwo\tmfour  = \tmtwo\]

If $\evarthree\notin\fv{\exval}$ then the cut $\cuta{\tmthree}\evarthree$ gives rise to a $\tow$ redex in both $\tm$ and $\tmtwo$, but in $\tm$ the $\tow$ redex is bad while in $\tmtwo$ it is good, that is, a good $\tow$ redex  turns into a bad one because of the reduction of a bad $\toaxeone$ redex. Of course, one might try to change the definitions of good and bad steps, but there are no obvious ones that seem to work (we tried repeatedly).

* Rules and diagrams: in the Plain ESC, the on-the-fly splitting of terms happens in order to identify the redex, while in the Split ESC it happens in order to write some of the reducts (to preserve the split shape). It seems an equivalent cost, but it is not: in the study of the many confluence diagrams for the calculus, one needs to check the superposition of two redexes, so having simpler redexes is more convenient. Moreover, in the Split ESC only some rules need the on-the-fly splitting, while in the Plain ESC all rules need it.

* Local termination: the proof of local termination (in local-termination) suggests to switch to the Split ESC. The proof uses a measure $\ltmeas{\tm}$ on terms (termination-meas, page def:termination-meas) that takes into account how many times the content of cuts is duplicated, depending on the number of occurrences of their variables. Now, given $\cuta\tmtwo\var\tm$ with $\tmtwo = \lctxp\val$ only $\val$ can be duplicated, so in the case of the Plain ESC (for which we first developed the proof of local termination) the measure for the left context $\lctx$, differently from $\val$, does not depend on the multiplicity of $\var$, at least not directly. It is then natural to define the measure on $\cuta\tmtwo\var\tm$ by splitting $\tmtwo$, that is, as follows:

\[ \ltmeas{\cuta{\lctxp\val}\var\tm} \ \ \defeq \ \  \ltmeas{\lctxp{\cuta\val\var\tm}} \]

and then having a further case for $\ltmeas{\cuta{\val}\var\tm}$ (which is as in termination-meas). Roughly, this means defining the measure via the Split ESC, and it was one of the reasons that motivated us to abandon the Plain ESC.

Once one decides to adopt a split approach, there still is a design space. We considered at least the following options.

* Adopting restricted typing rules: for cut and subtractions it becomes natural to adopt the following typing rules where there is no left context $\lctx$:

$\multiForm   \vdash \val \hastype \form$
$\multiFormtwo, \var\hastype \form \vdash \tm\hastype\formtwo$
$  \multiForm, \multiFormtwo\vdash \cuta\val\var\tm \hastype\formtwo$

$  \multiForm \vdash \val\hastype\form$
$  \multiFormtwo, \var\hastype\formtwo \vdash \tm\hastype\formthree$
$ \lolliLeftRule $
$  \multiForm, \multiFormtwo, \mvar\hastype \form \lolli \formtwo \vdash \suba\mvar\val\var  \tm \hastype\formthree$

Adopting these rules is obviously sound (because they are special cases of the ones of the ESC) but also complete, because left rules can always be permuted down, so adopting these restricted rules does not affect provability, it only forces a certain order among rules. Despite their completeness, we prefered to avoid the restricted rules because we did not want to give the impression that in order to reduce at a distance one needs to modify the deductive system. Another reason for avoiding the rules is that in the restricted rules the restriction is enforced by the proof term, which we believed is not nice.

* Splitting tensors: once cut and subtractions are split, one may wonder why not pushing splitting further, splitting also other constructs. Promotions and abstractions cannot be split, because they depend on the left side of the sequent, but tensors can very easily be split by adopting tensor pairs of the form $\pair\val\valtwo$ and a modified typing rule for $\tens$ such as:

\[\AxiomC{$  \multiForm\vdash \lctxp\val\hastype\form$}
\AxiomC{$  \multiFormtwo\vdash \lctxtwop\valtwo\hastype\formtwo$}
\AxiomC{$\multiForm\#\multiFormtwo$}
\RightLabel{$ \tensRightRule $}
\TrinaryInfC{$  \multiForm, \multiFormtwo\vdash \lctxp{\lctxtwop{\pair\val\valtwo}} \hastype\form\otimes \formtwo$}
\DisplayProof
\]

The change simplifies the cut elimination rule $\totens$, which no longer needs to use on-the-fly splitting to write the reduct, as it simply becomes:

\[ \cuta{\pair\val\valtwo}\mvar \mctxp{\para\mvar\var\vartwo\tm}
\ \ \rtotens \ \
\mctxp{\cuta\val\var \cuta\valtwo\vartwo \tm}  \]

The change however impacts on the proof of strong normalization in nasty ways. The problem is that the typing rule needs to fix an order between the left rules in $\lctx$ and $\lctxtwo$ in the conclusion which clashes with the definition of reducibility, candidates, and the proof of adequacy. Adopting restricted typing rules as in the previous point seem to solve all these problems, but then one is modifying the deductive system.

§.§ Unusual cut elimination for exponential axioms

In the proof nets literature, cut elimination of exponential axioms is identical to the one for multiplicative axioms (there is in fact no distinction between the two kinds of axioms) and simply amounts to the removal of the cut and the axiom, in both the small-step (la Regnier) and the micro-step (à la Girard) approaches. In the asymmetric intuitionistic setting, axioms have two rules, depending whether they are substituted, or substituted upon. Let's focus on the substitution of axioms. In our syntax, the traditional approach to cut elimination for exponential axioms would take the following form:

\[ \cuta\evartwo\evar\tm \ \  \to \ \ \cutsub\evartwo\evar\tm\]

When written with terms, one immediately notices that such a rule is small-step. If considered with micro-step rules (in particular our $\tobder$), it generates a closable but unpleasant local confluence diagram (similar in spirit to the unpleasant one for the Plain ESC given above):

\[\begin{array}{cccccccc}
\cuta{\bang\val}\evartwo \ctxp{\cuta\evartwo\evar \tm}
& \rtobder &
\cuta{\bang\val}\evartwo \ctxp{\cuta{\bang\val}\evar \tm}
\toems^+
\cuta{\bang\val}\evartwo \ctxp{\cutsub{\bang\val}\evar \tm}

\\
\downarrow & &&&\downarrow_{\ems+}

\\
\cuta{\bang\val}\evartwo \ctxp{\cutsub\evartwo\evar \tm}
& \toems^+ &
\cutsub{\bang\val}\evartwo \ctxp{\cutsub\evartwo\evar \tm}
& = &
\cutsub{\bang\val}\evartwo \ctxp{\cutsub{\bang\val}\evar \tm}
\end{array}\]

The point is that in order to close the local diagram one need to fully develop some exponential cuts, which is a small-step concept and not a micro-step one. This is why we instead adopted a LSC-duplication style also for exponential axioms/variables. Curiously, this is exactly the confluence issue that Accattoli <cit.> has with MELLP proof nets at a distance, the solution of which is now clear: it is enough to switch to LSC-duplication of exponential axioms rather than the usual approach. The moral of the story is that proof nets might be misleading in distinguishing between small-step and micro-step cut elimination rules.

§.§ The avoidance of a Curien-Herbelin syntax for the ESC

As we said in the introduction, one of the reasons for avoiding a Curien-Herbelin-style syntax for the ESC is that their syntaxes are not  decorations of usual sequent calculus rules, as they requires to have a distinguished formula on the left. One of our aims was to show that there is no need to modify the sequent calculus in order to reduce at a distance.

There is however another reason for avoiding a Curien-Herbelin-style syntax. Their approach has three syntactic categories: terms, co-terms, and commands (that are cuts between a term and a co-term). Micro-step cut elimination at a distance makes crucial use of contexts. As the reader might have noticed, the use of contexts is already quite heavy for the ESC as it is. Adoting Curien-Herbelin-style would have the dramatic drawback of multiplying the notions of contexts, as each notion of context needs to be instanciated on each syntactic category. We tried at some point to work with a Curien-Herbelin-style ESC, but we abandoned the attempt as it was syntactically too heavy without a clear gain.
Note that the ESC has only one syntactic category, terms, plus the sub-category of values. This aspect is quite essential in order to make the calculus manageable.

§ APPENDIX OF CALCULUS (THE EXPONENTIAL SUBSTITUTION CALCULUS)

Let $\ctxp\tm$ be a term. Then:

* $\tm$ is .

* If $\tmtwo$ is and such that $\mfv\tmtwo = \mfv\tm$ then $\ctxp\tmtwo$ is .

By induction on $\ctx$.

Let $\tm$ be a term and $\tm \toms \tmtwo$. Then $\tmtwo$ is .

Let $\tm = \ctxp\tmthree \toms \ctxp\tmfour = \tmtwo$. By proper-replacement, $\tmthree$ is , and to prove the statement it is enough to prove that if $\tmthree \toms \tmfour$ is a root step then $\tmfour$ is and that that $\mfv\tmfour = \mfv\tmthree$. Note that all the the root rewriting rules preserve the set of multiplicative variables, that is, $\mfv\tmfour = \mfv\tmthree$ holds. Proving that the root rules preserve being is a straightforward induction.

Preservation of properness by $\toess$ follows from full composition (ms-simulates-ss,  the proof of that proposition is just below).

§ APPENDIX OF BASIC-PROP (BASIC PROPERTIES)

Let $\tm$ be a term and $\tm \toss \tmtwo$. Then $\tmtwo$ is .

§ APPENDIX OF STRATEGY (THE GOOD STRATEGY)

We first need some definitions and technical tools to manage contexts, namely the outside-in order on contexts, contexts with two holes (called double contexts), and some of their properties, together with some properties of dominating free variables and good contexts.

[Outside-in context order]
We define the partial outside-in order $\outer$ over contexts:

$\ctxhole \outer \ctx$

$\ctx \outer\ctxtwo$
$\ctxthreep\ctx \outer \ctxthreep\ctxtwo$

And say that $\ctx$ is outer than $\ctxtwo$ if $\ctx\outer \ctxtwo$. If $\ctx\not\outer \ctxtwo$ and $\ctxtwo\not\outer \ctx$ we say that $\ctx$ and $\ctxtwo$ are disjoint, and write $\ctx\parallel \ctxtwo$.

Double Contexts. Double contexts have as base cases binary constructors (that is, tensor pairs, cuts, and subtractions) having contexts replacing their subterms, and as inductive cases they are simply closed by an ordinary context.
[Double contexts]
Double contexts $\cctx$ are defined by the following grammar.

\[\begin{array}{l@{\sep}llll}
\textsc{Double contexts} & \cctx& \defeq & \pair\ctx\ctxtwo \mid \suba\mvar\ctx\var\ctxtwo \mid \cuta\ctx\var\ctxtwo \mid \ctxp\cctx
\end{array}\]

We now discuss some easy facts about double contexts.

* Plugging: the plugging $\cctxp{\tm,\tmtwo}$ of two terms $\tm$ and $\tmtwo$ into a double context $\cctx$ is defined as expected and gives a term. The two ways of plugging one term $\cctxp{\tm,\ctxhole}$ and $\cctxp{\ctxhole,\tmtwo}$ into a double context give instead a context. We often use $\cctxp{\tm,\cdot}$ and $\cctxp{\cdot,\tmtwo}$ as compact notations for $\cctxp{\tm,\ctxhole}$ and $\cctxp{\ctxhole,\tmtwo}$.

* Pairs of disjoint positions and double contexts: every pair of positions $\ctxp\tm=\ctxtwop\tmtwo$ which are disjoint, that is, such that $\ctx \parallel\ctxtwo$, gives rise to a double context $\cctx_{\ctx,\ctxtwo}$ such that $\cctx_{\ctx,\ctxtwo}\ctxholep{\cdot,\tmtwo} = \ctx$ and $\cctx_{\ctx,\ctxtwo}\ctxholep{\tm,\cdot} = \ctxtwo$. Conversely, every double context $\cctx$ and every pair of terms $\tm$ and $\tmtwo$ gives rise to two context $\cctx_{l}^{\tm,\tmtwo} \defeq \cctxp{\ctxhole, \tmtwo}$ and $\ctx_{r}^{\tm,\tmtwo} \defeq \cctxp{\tm,\ctxhole}$. Note that the two constructions are inverse of each other, that is, given $\cctx$, we have $\cctx_{\cctx_{l}^{\tm,\tmtwo},\ctx_{r}^{\tm,\tmtwo} } = \cctx$, and, conversely, given $\ctxp\tm=\ctxtwop\tmtwo$ we have $(\cctx_{\ctx,\ctxtwo})_{l}^{\tm,\tmtwo} = \ctx$ and $(\cctx_{\ctx,\ctxtwo})_{r}^{\tm,\tmtwo} = \ctxtwo$.

Let $\cctx$ be a double context and $\tm$ and $\tmtwo$ be two terms. Then:

* $\cctxp{\cdot,\tm}$ is as capturing as $\cctxp{\cdot,\tmtwo}$;

* $\dfv{\cctxp{\cdot,\tm}} = \dfv{\cctxp{\cdot,\tmtwo}}$;

* $\cctxp{\cdot,\tm}$ is good if and only if $\cctxp{\cdot,\tmtwo}$ is good.

Note that the last point of double-ctx-repl could have be equivalently stated with respect to being bad.

By induction on $\cctx$. The base cases are straightforward, and the inductive cases follow from the The inductive case where it is worth spending two words is when $\cctx = \cuta\val\var\cctxtwo$, where the point about goodness uses the point about the preservation of dominating free variables.

$\ctxp{\cctxp{\tm,\cdot}} = \ctxp{\cctx}\ctxholep{\tm,\cdot}$ and $\ctxp{\cctxp{\cdot,\tm}} = \ctxp{\cctx}\ctxholep{\cdot,\tm}$.

By induction on $\ctx$.

Dominating Free Variables

Let $\var\in\dfv\ctx$.

* Then one of the following cases hold:

* $\ctx = \mctxp{\para\mvar\vartwo\varthree\ctxtwo}$ and $\var = \mvar$.

* $\ctx = \mctxp{\suba\mvar\val\vartwo\ctxtwo}$ and $\var = \mvar$.

* $\ctx = \mctxp{\suba\mvar\vctx\vartwo\tm}$ and $\var = \mvar$.

* $\ctx = \ctxtwop{\dera\evar\vartwo\ctxthree}$, $\var = \evar$, and $\evar \notin\dfv\ctxtwo$.

*  If $\ctx$ is a position in $\mctxp{\tm_{\mvar}}$ and $\mctx \not\outer \ctx$ then $\mvar \notin\dfv\ctx$.

* The first three points are simply the observation that if $\var=\mvar$ is multiplicative and $\mvar\in\dfv\ctx$ then

* $\mvar\in\fv\ctx$ and so the position of $\mvar$ has to be a multiplicative context $\mctx$;

* the occurrence has to be a par or subtraction occurrence by definition of $\dfv\ctx$ (that is, it cannot be a variable occurrence).

The fourth point is similar but it says something more so we need a bit more. It is by induction on $\ctx$. If $\var=\evar$  is exponential and $\evar\in\dfv\ctx$ then $\ctx = \ctxtwo'\ctxholep{\dera\evar\vartwo\ctxthree'}$. Now, if $\evar\notin\dfv{\ctxtwo'}$ the statement holds with $\ctxtwo \defeq \ctxtwo'$. Otherwise, by , $\ctxtwo' = \ctxtwo''\ctxholep{\dera\evar\varthree\ctxthree''}$ with $\evar\notin\dfv{\ctxtwo''}$. Then $\ctx =  \ctxtwo''\ctxholep{\dera\evar\varthree\ctxthree''\ctxholep{\dera\evar\vartwo\ctxthree'}}$, which satisfies the statement with respect to $\ctxtwo \defeq \ctxtwo''$.

* By induction on $\ctx$. Note that since $\mctx \not\outer \ctx$ then $\mctx \neq \ctxhole$. Cases:

* Empty, that is, $\ctx = \ctxhole$. Then $\mvar \notin \emptyset = \dfv\ctxhole$.

* Abstraction, dereliction, par: we do the par case $\ctx = \para\mvartwo\var\vartwo\ctxtwo$. Then $\mctx = \para\mvartwo\var\vartwo\mctxtwo$ with $\mctxtwo \not \outer \ctxtwo$ (otherwise $\mctx \outer \ctx$). By , $\mvar \notin \dfv\ctxtwo$ and so $\mvar \notin\dfv\ctx$.

* Bang case, that is, $\ctx = \bang\ctxtwo$. This is impossible, because then $\mctx$ should be empty.

* Left sub-term of cut, that is, $\ctx = \cuta\vctx\var\tmtwo$. If $\mctx = \cuta\vmctx\var\tmtwo$ then $\vmctx \not\outer \vctx$ (otherwise $\mctx \outer \ctx$), and the statement follows from the Otherwise, $\mctx = \cuta\tmthree\var\mctxtwo$ and by properness $\mvar \notin \tmthree$ and so $\mvar\notin \vctx$. Then $\mvar \notin \dfv\vctx = \dfv\ctx$.

* Right sub-term of cut, that is, $\ctx = \cuta\tmtwo\var \ctxtwo$. If $\mctx = \cuta\tmtwo\var\mctxtwo$ then $\mctxtwo \not\outer \ctxtwo$ (otherwise $\mctx \outer \ctx$), and the statement follows from the Otherwise, $\mctx = \cuta\vmctx\var\tmthree$ and by properness $\mvar \notin \tmthree$ and so $\mvar\notin \ctxtwo$. Then $\mvar \notin \dfv\ctxtwo = \dfv\ctx$.

* Subtraction and tensor: as for cut.

Good and Bad Contexts and Steps

By induction on $\ctx$. The empty context $\ctxhole$ is good and not bad. For all inductive cases but cut, it follows from the The cut cases:

* $\ctx = \cuta\vctx\var\tm$. Then $\ctx$ is bad and not good.

* $\ctx = \cuta\val\var\ctxtwo$. By , $\ctxtwo$ is either good or bad. If $\ctxtwo$ is bad then $\ctx$ is bad, and $\ctx$ is not good because $\ctxtwo$ is not good. If $\ctxtwo$ is good, consider whether $\var\in \dfv\ctxtwo$. If it does, then $\ctx$ is bad and not good. If instead  $\var\notin \dfv\ctxtwo$ then $\ctx$ is good and not bad.

Let $\ctxp\ctxtwo$ be a good context. Then $\ctx$ and $\ctxtwo$ are good contexts.

Let $\gctxp\tm= \bctxp\tmtwo$. Then $\bctx\not\outer\gctx$, that is, either $\gctx\outer\bctx$ or $\gctx \parallel \bctx$.

By induction on $\gctx$. Note that $\bctx$ cannot be empty, otherwise it would be good. Cases:

* $\gctx = \ctxhole$. Then $\tm = \bctxp\tmtwo$ and so $\bctx\not\outer \gctx$.

* $\gctx = \la\var\gctxtwo$. Then $\bctx = \la\var\bctxtwo$ and the statement follows from the
* The bang, par, and dereliction cases follows from the as the previous one.

* $\gctx = \pair\gctxthree\tmthree$. If $\bctx = \pair\bctxtwo\tmthree$ then it follows from the If instead $\bctx = \pair\tmfour\bctxtwo$ then $\bctx \not\outer \gctx$.

* The subtraction case is as the tensor case.

* $\gctx = \cuta\val\var\gctxtwo$. If $\bctx = \cuta\val\var\bctxtwo$ it follows from the If instead $\bctx = \cuta\bctxtwo\var\tmthree$ then $\bctx \not\outer \gctx$.

The next few lemmas are technical ones used in the proofs of the properties of the good strategies that follow.

* If $\ctxp{\cuta\val\var\ctxtwo}$ is good then $\ctxp{\ctxtwo}$ is good.

* If $\ctxp{\ctxtwo}$ is bad then $\ctxp{\cuta\val\var\ctxtwo}$ is bad.

Point 1 is by induction on $\ctx$. Since a context is either good or bad (good-bad-partition), Point 2 is simply the contrapositive of Point 1.

If $\gctx$ is good then $\cutsub\mvartwo\mvar\gctx$ is good. Moreover, if $\mvar\notin\dfv\gctx$ then $\dfv\gctx = \dfv{\cutsub\mvartwo\mvar\gctx}$.

By induction on $\gctx$.

Let $\mctxp{\para\mvar\var\vartwo \ctx}$ be good, with $\mctx$ not capturing $\mvar$ and $\mvar\notin\dfv{\mctxp{\para\mvar\var\vartwo \ctx}}$. Then $\mctxp{\ctxtwop\ctx}$ is good and $\dfv{\mctxp{\ctxtwop\ctx}}= \dfv{\mctxp{\para\mvar\var\vartwo \ctx}}$ for every context $\ctxtwo$ capturing no more than $\var$ and $\vartwo$ in $\ctx$.

Let $\mctxp{\suba\mvar\val\var \ctx}$ be good, with $\mctx$ not capturing $\mvar$ and $\mvar\notin\dfv{\mctxp{\suba\mvar\val\var \ctx}}$. Then $\mctxp{\ctxtwop\ctx}$ is good and $\dfv{\mctxp{\ctxtwop\ctx}}= \mctxp{\suba\mvar\val\var \ctx}$ for every context $\ctxtwo$ capturing no more than $\var$ in $\ctx$.

Let $\mctxp{\dera\evar\var \ctx}$ be good, with $\mctx$ not capturing $\evar$ and $\evar\notin\dfv{\dera\evar\var}$. Then $\mctxp{\ctxtwop\ctx}$ is good and $\dfv{\mctxp{\ctxtwop\ctx}}= \mctxp{\dera\evar\var \ctx}$ for every context $\ctxtwo$ capturing no more than $\var$ in $\ctx$.

By induction on $\mctx$.

Sub-Term Property

By induction on the length $k$ of the reduction $\tm \tog^{k} \tmtwo$. If $k=0$ then the statement obviously holds. If $k>0$ then we consider the last step $\tmthree \tog \tmtwo$ of the sequence. By the local sub-term property (local-sub-tm), the size of every bad value $\val$ of $\tmtwo$ is bound by the size of a bad value $\valtwo$ of $\tmthree$, which by satisfy the statement.

Good Diamond For proving the good diamond property, we need a set of deformation lemmas, collected together in aux-props-loc-confl-strong-comm, that essentially say what happens to a variable occurrence under the action of a rewriting step. The statements avoid using any form of residual of steps, sub-terms, or constructors but they often establish a sort of residual relationship by specifying the preservation modulo a parameter—for instance in the first point the context $\mctxtwo$ is meant to be the residual of $\mctx$ and this is obtained via the preservation of the step modulo $\mval$.

The deformation lemmas shall also be used in the proofs of confluence and root cut expansion in the following sections. The moreover part of each statement, however, is used only here for the good diamond, while the case of $\to = \toss$ shall be used in the proof of root cut expansion and only for some of the deformation lemmas.

We give all the (many!) details of the proof of the first deformation property. The proofs of the others are tedious minor variations.

Let $\to\in\set{\toss,\toms}$.

Let $\ctx: \tm = \mctxfp\mvar \Rew{a} \tmtwo$ and $\Rew{a}$ be a $\to$ step. Then:

either $\tmtwo = \mctxtwofp{\mvar}$ for some
$\mctxtwo$ such that $\mvar\notin\fv\mctxtwo$ and there is a step $\ctxtwo_{\mval}: \mctxfp\mval \Rew{a} \mctxtwofp\mval$ for every $\mval$,

* or $\mctx = \mctxtwop{\cuta\ctxhole\mvartwo\tmthree}$ for some
$\mctxtwo$ and $\ctx$ reduces the cut on $\mvartwo$.

Moreover, if $\to$ is $\toms$ and both $\ctx$ and $\mctx$ are good,  then case <ref> holds and both $\mctxtwo$ and $\ctxtwo_{\mval}$ are good and satisfy $\dfv\mctx = \dfv\mctxtwo$ and $\dfv\ctx = \dfv{\ctxtwo_{\mval}}$.

Let $\ctx: \tm = \mctxfp{\tm_\mvar} \Rew{a} \tmtwo$ where $\tm_\mvar$ is a par or a subtraction of conclusion $\mvar$, $\mctxtwo$ does not capture $\mvartwo$, and $\Rew{a}$ be a $\to$ step. Then  $\tmtwo = \mctxtwofp{\tmtwo_\mvar}$ where $\tmtwo_\mvar$ is an occurrence of $\mvar$ of the same kind of $\tm_\mvar$,
$\mctxtwo$ does not capture $\mvar$ and $\mvar\notin\fv\mctxtwo$, and there is a step $\ctxtwo_{\mvartwo}: \mctxfp{\cutsub\mvartwo\mvar \tm_\mvar} \Rew{a} \mctxtwofp{\cutsub\mvartwo\mvar \tmtwo_\mvar}$ for every fresh multiplicative variable $\mvartwo$.

Moreover, if $\to$ is $\toms$ and both $\ctx$ and $\mctx$ are good,  then  both $\mctxtwo$ and $\ctxtwo_{\mvartwo}$ are good and satisfy $\dfv\mctx = \dfv\mctxtwo$ and $\dfv\ctx = \dfv{\ctxtwo_{\mvartwo}}$.

*  If $\ctx: \mctxp{\para\mvar\var\vartwo \tm} \Rew{a} \tmtwo$ is a $\to$-step and $\mctx$ does not
capture $\mvar$ then $\tmtwo = \mctxtwop{\para\mvar\var\vartwo \tm'}$ with $\mctxtwo$ not capturing $\mvar$ and
such that there is a step $\ctxtwo_{\ctxthree}: \mctxp{\ctxthreep\tm} \Rew{a} \mctxtwop{\ctxthreep{\tm'}}$ for every context $\ctxthree$ capturing no more than $\var$ and $\vartwo$ in $\tm$ and such that $\mctx$ does not capture variables of $\ctxthree$.

Moreover, if $\to$ is $\toms$ and both $\ctx$ and $\mctx$ are good,  then  both $\mctxtwo$ and $\ctxtwo_{\ctxthree}$ are good and satisfy $\dfv\mctx = \dfv\mctxtwo$ and $\dfv\ctx = \dfv{\ctxtwo_{\ctxthree}}$.

*  If $\ctx: \mctxp{\suba\mvar\val\var \tmfour} \Rew{a} \tmtwo$ is a $\to$-step and $\mctx$ does not
capture $\mvar$ then either

* $\tmtwo = \mctxtwop{\suba\mvar\val\var \tmfour'}$ with
$\ctxtwo_{\ctxthree}:\mctxp{\ctxthreep\tmfour} \Rew{a}
\mctxtwop{\ctxthreep{\tmfour'}}$ for every context $\ctxthree$ capturing no more than $\var$ in $\tmfour$  and such that $\mctx$ does not capture in $\ctxthree$ more variables than those in $\fv\val$, or

* $\tmtwo = \mctxtwop{\suba\mvar\valtwo\var \tmfour}$ with $\ctxtwo_{\ctxthree}:\mctxp{\ctxthreep\val} \Rew{a}
\mctxtwop{\ctxthreep{\valtwo}}$ for every context $\ctxthree$ not capturing variables of $\val$ and such that $\mctx$ does not capture in $\ctxthree$ more variables than those in $\fv\tmfour \setminus\set{\var}$.

In both cases $\mctxtwo$ does not capture $\mvar$.

Moreover, if $\to$ is $\toms$ and both $\ctx$ and $\mctx$ are good,  then  both $\mctxtwo$ and $\ctxtwo_{\ctxthree}$ are good and satisfy $\dfv\mctx = \dfv\mctxtwo$ and $\dfv\ctx = \dfv{\ctxtwo_{\ctxthree}}$.

Let $\ctx: \tm = \ctxtwofp\evar \Rew{a} \tmtwo$ and $\Rew{a}$  be a $\toms$ step.  Then:

either $\tmtwo = \ctxtwo'\ctxholefp{\evar}$ for some
$\ctxthree$ such that there is a step $\ctx^\bullet_{\exval}:\ctxtwofp\exval \Rew{a} \ctxtwo'\ctxholefp\exval$ for every $\exval$,

* or $\ctxtwo = \ctxthreep{\cuta\ctxfour\evartwo\tmthree}$ for some
$\ctxthree$ and $\ctxfour$, and $\ctx$ reduces a redex where the  active cut is the one on $\evartwo$.

Moreover, if both $\ctx$ and $\ctxtwo$ are good  then case <ref> holds and both $\ctxthree$ and $\ctx^\bullet_{\exval}$ are good and satisfy $\dfv\ctxtwo = \dfv\ctxthree$ and $\dfv\ctx = \dfv{\ctx^\bullet_{\exval}}$.

Let $\ctx: \tm = \ctxtwop{\dera\evar\var\tmthree} \Rew{a} \tmtwo$ with $\ctxtwo$ not capturing $\evar$ and $\Rew{a}$  be a $\toms$ step.  Then:

either $\tmtwo = \ctxtwo'\ctxholep{\dera\evar\var\tmthree'}$ for some
$\ctxtwo'$ such that there is a step $\ctx^\bullet_{\ctxthree}:\ctxtwop{\ctxthreep{\tmthree}} \Rew{a} \ctxtwo'\ctxholep{\ctxthreep{\tmthree'}}$ for every $\ctxthree$ capturing no more than $\var$ in $\tmthree$ and $\tmthree'$,

* or $\ctxtwo = \ctxthreep{\cuta\ctxfour\evartwo\tmthree}$ for some $\ctxthree$ and
$\ctxfour$, and $\ctx$ reduces a redex given by the cut on $\evartwo$.

Moreover, if both $\ctx$ and $\ctxtwo$ are good  then case <ref> holds and both $\ctxthree$ and $\ctx^\bullet_{\exval}$ are good and satisfy $\dfv\ctxtwo = \dfv\ctxthree$ and $\dfv\ctx = \dfv{\ctx^\bullet_{\exval}}$.

Fullness We recall that an occurrence of $\var$ in $\tm$ is given by a position $\tm = \ctxp{\tm_{\var}}$  where $\tm_{\var}$ is a sub-term of $\tm$ of shape $\var$, $\para\var\vartwo\varthree\tmtwo$, $\suba\var\val\vartwo\tmtwo$, or $\dera\var\vartwo\tmtwo$. Note that the shapes of $\tm_{\var}$ are the kind of terms with which a cut on $\var$ can interact at a distance to form a redex.

[Outermost variable occurrence]
An occurrence $\tm = \ctxp{\tm_{\var}}$ of $\var$ in $\tm$ is outermost if $\ctxtwo \not\outer\ctx$ for all other occurrences $\tm = \ctxtwop{\tm'_{\var}}$ of $\var$.

Let $\tm = \ctxp{\tm_{\var}}$ be an outermost occurrence of $\var$ in $\tm$ with $\ctx$ not capturing $\var$. Then $\var \notin\dfv\ctx$.

By induction on the number $\sizep\ctx\var$ of free occurrences of $\var$ in $\ctx$. If $\sizep\ctx\var = 0$ then $\var\notin \fv\ctx \supset \dfv\ctx$. If $\sizep\ctx\var > 0$ consider another occurrence $\ctxtwop{\tm_{\var}'}$ of $\var$ in $\tm$ such that $\ctx\not\outer\ctxtwo$, which exists because $\sizep\ctx\var > 0$ (indeed if $\ctx\outer\ctxtwo$ then $\tm_{\var}'$ is a sub-term of $\tm_{\var}$ and does not contribute to $\sizep\ctx\var$). Since $\tm_{\var}$ is outermost, we have $\ctxtwo \parallel \ctx$. Now, consider the double context $\cctx_{\ctx,\ctxtwo}$ such that $\cctx_{\ctx,\ctxtwo}\ctxholep{\ctxhole, \tm_{\var}'}=\ctx$ and $\cctx_{\ctx,\ctxtwo}\ctxholep{\tm_{\var},\ctxhole}=\ctxtwo$. By double-ctx-repl, the context $\ctxthree \defeq \cctx_{\ctx,\ctxtwo}\ctxholep{\ctxhole, \la\mvar\mvar}$ verifies $\dfv\ctxthree = \dfv\ctx$ and $\sizep\ctxthree\var \leq \sizep\ctx\var -1$. Then by we have $\var\notin\dfv\ctxthree = \dfv\ctx$.

By typed strong normalization (sn), $\tog$ terminates on $\tm$, let $\tmtwo$ be its $\tog$ normal form. Since typable implies clash-freeness (clashfree-implies-cutfree), $\tm$ is clash-free, and thus so is $\tmtwo$. By fullness and $\tog$ normality, $\tmtwo$ is $\toms$-normal, which by clashfree-implies-cutfree means that it is cut-free.

Now, about the cost. Let $\tm = \tm_{0} \tog \tm_{1} \underbrace{ \tog\ldots \tog}_{k-1} \tm_{k} = \tmtwo$. All steps $\tm_{i} \tog \tm_{i+1}$ of the sequence that are multiplicative, as well as $\toaxetwo$ step, do only manipulation of a constant number of constructors of the term. Therefore, they can clearly be implemented in time polynomial in $\size{\tm_{i}}$, as searching for a redex and checking that its position is good are clearly polynomial problems, and there is at most a linear number of redexes in a term. By a straightforward induction using the sub-term property, one obtains that $\size{\tm_{i}} \leq i*\size{\tm_{0}}$, and so all those steps have  cost polynomial in $k$ and $\size{\tm_{0}}$. By the sub-term property, the cost of duplication/erasure of values in non-linear steps (namely, $\toaxeone$, $\tobder$, and $\tobw$ steps) is bound by $\tm_{0}$, so they have polynomial cost in $k$ and $\size{\tm_{0}}$ as well.

§ APPENDIX OF CONFLUENCE (UNTYPED CONFLUENCE)

Let $\to\in\set{\toss,\toms}$.

If $\ctx:\tm \Rew{a} \tmtwo$ then $\cutsub\vartwo\var\ctx:\cutsub\vartwo\var\tm \Rew{a} \cutsub\vartwo\var\tmtwo$.

If $\lctxp\val \Rew{a} \lctxtwop\valtwo$ is a $\to$-step then $\lctxp{\ctxp{\val}} \Rew{a} \lctxtwop{\ctxp\valtwo}$ for every context $\ctx$ not capturing variables of $\val$ and such that $\lctx$ does not capture the free variables of $\ctx$.

* Straightforward induction on the rewriting step.

* Straightforward induction on $\lctx$. In fact, it holds simply because the rules are at a distance or contextual, that is, they do not care what is in between the cut and the variable occurrence(s) interacting with it.

We deal with $\toms$, the reasoning for $\toess$ is identical. By Newman lemma, local confluence (loc-confluence) and local termination (local-termination) imply that $\tom$ and $\toess$ are confluent separately. By a result of Hindley <cit.>, strong commutation  (strong-commutation) and local termination imply that $\tom$ and $\toess$ commute. By Hindley-Rosen lemma, $\toms = \tom \cup \toems$ is confluent.

§ APPENDIX OF PSN (UNTYPED PRESERVATION OF SN)


# Differentially Private Neural Network Training under Hidden State Assumption

Ding Chen City University of Hong Kong, Hong Kong, China/ emails:
ding.chen<EMAIL_ADDRESS>Chen Liu11footnotemark: 1

###### Abstract

We present a novel approach called differentially private stochastic block
coordinate descent (DP-SBCD) for training neural networks with provable
guarantees of differential privacy under the hidden state assumption. Our
methodology incorporates Lipschitz neural networks and decomposes the training
process of the neural network into sub-problems, each corresponding to the
training of a specific layer. By doing so, we extend the analysis of
differential privacy under the hidden state assumption to encompass non-convex
problems and algorithms employing proximal gradient descent. Furthermore, in
contrast to existing methods, we adopt a novel approach by utilizing
calibrated noise sampled from adaptive distributions, yielding improved
empirical trade-offs between utility and privacy.

##  1 Introduction

Machine learning models, especially deep neural networks, have exhibited
remarkable progress in the last decade across diverse fields. Their
applications, such as face recognition [11] and large language models [20],
have been integrated into people’s daily lives. However, the increasing demand
for large amounts of training data in the training process has given rise to
growing concerns regarding the potential privacy vulnerabilities [14, 28]
associated with these models. For example, deep neural networks are shown to
memorize the training data [34] so that we can even reconstruct part of the
training data from the learned model parameters [19]. To address these issues,
differential privacy [10] has become the gold standard for making formal and
quantitative guarantees on model’s privacy and has been widely applied in
learning problems [1, 18].

The predominate approach to ensuring differential privacy in the context of
machine learning involves the incorporation of calibrated noise during each
update step in the training phase, which leads to a trade-off between utility
and privacy loss [2, 3]. Excessive noise often leads to a significant loss in
utility, while insufficient noise may result in privacy leakage. Moreover,
many privacy accountant methods, such as moment accountant [1], are typically
based on the composition properties of differential privacy. Specifically,
they usually assume that the calibrated noise in each training iteration
follows the same distribution and that the algorithm’s internal states, i.e.,
the model’s parameters in each training step, can be revealed to the
adversaries. As a result, the total privacy loss of the algorithm
significantly increases with the number of training iterations, because more
internal states will be revealed with more training iterations. Such
assumptions lead to a very loose privacy estimation of the algorithm, because,
in practice, most internal states are usually not even recorded during
training.

The gap between theory and practice motivates researchers to consider more
practical assumptions. Recently, the hidden state assumption was proposed to
narrow down this gap [9, 13, 32]. This assumption posits that the internal
states of the training phase are hidden, and that the adversaries only have
access to the last iterate. Under this assumption, Chourasia et al. [9], Ye
and Shokri [32] use Langevin diffusion to track the change rate of Rényi
Differential Privacy (RDP) in each epoch and bound the privacy loss for
Differential Privacy Gradient Descent (DP-GD) and Differential Privacy
Stochastic mini-batch Gradient Descent (DP-SGD) [1]. Recently, Asoodeh and
Diaz [4] also considered directly using hockey-stick divergence instead of
Rényi divergence. These works claim a converged and small privacy loss
(usually less than 1) under some strict assumption such as strongly convex
loss function and gradient Lipschitzness.

From a theoretical aspect, existing theorems indicate a valuable property that
privacy loss could converge under the hidden state assumption in learning
problems with strongly convex and $\beta$-smooth loss function. Otherwise, the
privacy loss will increase exponentially. Consequently, existing methods
cannot be directly applicable to training deep neural networks, whose loss
functions are non-convex and may exhibit non-smoothness when using activation
functions like ReLU [21].

To extend existing analyses of differential privacy under the hidden state
assumptions to deep learning problem, we introduce deep neural networks with a
Lipschitz constraint. To this end, we propose differentially private
stochastic block coordinate descent (DP-SBCD). In our proposed approach, we
formulate the task of training neural networks as a constrained optimization
problem and subsequently construct the associated Lagrangian function. The DP-
SBCD algorithm then considers each layer individually, decomposing the
original learning problem into multiple sub-problems. By observing that the
Lagrangian function exhibits convexity and smoothness concerning the model
parameters of each layer, our theoretical analyses yield the conclusion that
the DP-SBCD algorithm can yield models with guaranteed differential privacy
under the hidden state assumption. Besides, our algorithm’s privacy loss is
significantly smaller than that of composition theory.

In addition, this work investigates the connections between the calibrated
noise and the smoothness of the loss function in the context of differential
privacy. Intuitively speaking, we need noise of larger variance to achieve the
same level of differential privacy if the Lipschitz constant of the loss
gradient is bigger, but noise of large variance harms the utility when the
algorithm approaches the optimal solution. Due to this, we study the impact of
the variance of the calibrated noise on differential privacy and propose to
adaptively adjust it during training. We also explain why the privacy loss
will converge under the hidden state assumption. Empirically, our proposed
algorithm with adaptive calibrated noise achieves a better trade-off between
the model’s utility and privacy.

In summary, we highlight our contributions as follows:

  * •

We propose differentially private stochastic block coordinate descent (DP-
SBCD), which, to the best of our knowledge, is the first feasible method to
solve non-convex problems with differential privacy guarantees under the
hidden state assumption.

  * •

The algorithms and theorems in this work possess a generic nature, rendering
them compatible with proximal gradient descent and adaptive calibrated noise.

  * •

Empirically, the adaptive calibrated noise proposed in this work is able to
achieve better trade-offs between the model’s utility and privacy under the
hidden state assumption.

Terminology and Notation The privacy loss refers to the Rényi differential
privacy (RDP). When using the diffusion process to analyze the update scheme,
we use $t$ to represent the time in the process. We use $\|\cdot\|_{2}$ to
represent $l_{2}$ norm for vectors and the spectral norm for matrices. In
addition, $\|\cdot\|_{F}$ denotes Frobenius norm. Other notations are
explicitly defined before usage.

##  2 Related Works

Differential Privacy Differential Privacy (DP) [10] was initially introduced
to quantitatively ensure the privacy guarantees within the realm of databases.
Nevertheless, its rigorous mathematical foundations and nice properties, such
as composition theorem and post-processing immunity, have raised more and more
interest in its application in machine learning. Among the practical methods
for achieving DP-guaranteed models, DP-SGD [29] is the most popular one, which
involves the addition of calibrated noise to the clipped per-sample gradients
in each iterative update.

Besides the DP-guaranteed training algorithm, the proper accounting of privacy
loss is also critical. Most accountant methods rely on the composition theorem
of differential privacy. In this regard, Abadi et al. [1] introduces the
momentum accountant, Mironov [25] further proposes Rényi differential privacy
(RDP), which turns out a better tool to analyze the algorithm’s privacy loss.
Specifically, a randomized mechanism
${\mathcal{M}}:{\mathcal{D}}\rightarrow{\mathcal{R}}$ is said to have
$(\alpha,\varepsilon)$-RDP if for any adjacent datasets
$d,d^{\prime}\in{\mathcal{D}}$, it holds that
$D_{\alpha}({\mathcal{M}}(d)||{\mathcal{M}}(d^{\prime}))\leq\varepsilon$ where
$D_{\alpha}$ denotes the Rényi divergence of order $\alpha$.

Recently, the hidden state assumption has been explored in many works [9, 13,
32]. While the composition theory assumes that adversaries have access to the
intermediate states of the algorithm, which requires the summation of the
privacy loss across each training iteration [27], the hidden state assumption
posits that these intermediate states remain concealed. In real-life
applications, the intermediate states usually cannot be tracked, so the hidden
state assumption is more practical. It is first proposed in [13], which also
proves that a sequence of contractive maps can exhibit bounded
$(\alpha,\varepsilon)$-RDP. Subsequently, Chourasia et al. [9] consider the
update scheme as a Langevin diffusion process and analyze the privacy loss for
DP-GD using the log-Sobolev inequality [30]. Expanding upon this, Ye and
Shokri [32] analyze DP-SGD by leveraging the convergent analysis of unadjusted
Langevin algorithm proposed by Wibisono [31].

Block Coordinate Descent The block coordinate descent algorithm is designed to
decompose the original problem into several sub-problems which allow for
independent and efficient solutions. It not only helps prevent the vanishing
gradient problem [35] but also facilitates distributed or parallel
implementations [23]. In the era of deep learning, many works focus on
employing block coordinate descent to train neural networks [16, 33, 35].
Zhang and Brand [35] utilize a lifting trick to solve the learning problem of
deep neural networks with ReLU activation function, which is then extended by
Gu et al. [16], Mangold et al. [24]. Furthermore, Zeng et al. [33]
comprehensively analyzes two general types of optimization formulas: Two-
splitting and Three-splitting. They also investigate the loss function,
activation function, and architecture that these algorithms require.

Lipschitz Neural Networks The Lipschitz constant of a neural network holds
significant importance, especially in the context of robustness [12, 22] and
generalization [7, 26]. Recently, some works [8] remove the computationally
expensive per-sample gradient clipping in DP-SGD by controlling the Lipschitz
constants of neural networks. However, it is challenging to accurately enforce
the Lipschitz constant of neural networks. Gouk et al. [15] address this
challenge by using power iteration to approximate the layerwise Lipschitz
constant.

##  3 Solving Neural Network using Block Coordinate Descent

In this section, we train Lipschitz neural networks with block coordinate
descent and analyze the properties of the decomposed sub-problems.

###  3.1 Lipschitz Neural Network

We consider learning an $D$-layer neural network parameterized by
${\bm{\theta}}\overset{\text{\tiny def}}{=}\\{\theta_{d}\\}_{d=0}^{D}$:

$\min_{\bm{\theta}}{\mathcal{L}}({\bm{\theta}},{\bm{x}})\overset{\text{\tiny
def}}{=}{\mathcal{R}}(\theta_{D},{\bm{x}}_{D};y)\quad\text{s.t.}\quad{\bm{x}}_{d+1}=\sigma_{d}(\theta_{d}{\bm{x}}_{d})\quad
d=0,\ldots,D-1$ (1)

Here, ${\bm{x}}\overset{\text{\tiny def}}{=}{\bm{x}}_{0}$ is the input, and
$\\{{\bm{x}}_{d}\\}_{d=1}^{D}$ are vectors representing the intermediate
activations of each layer. ${\mathcal{R}}$ is the loss function, such as
softmax cross-entropy function, which is convex w.r.t. $\theta_{D}$. Moreover,
$\\{\sigma_{d}\\}_{d=0}^{D-1}$ are activation functions, such as ReLU
function, that are Lipschitz continuous. Finally, $\\{\theta_{d}\\}_{d=0}^{D}$
are matrices representing the weights of linear layers, including fully-
connected layers and convolutional layers. This formulation is generic and
consistent with practices.

As formulated in (1), the neural network is the composition of $D$ layers, so
the global Lipschitz constant is the product of the Lipschitz constant of each
layer [26]. We control the Lipschitz constant of each layer by normalizing the
weight parameters. Specifically, following the practice of Behrmann et al.
[6], we use power iteration [15] to approximate the spectral norm
$\widetilde{\lambda}_{d}$ of each layer and normalize the corresponding
parameter $\theta_{d}$ given the designated bound of the Lipschitz constant
$\rho_{d}$ by:

$\widetilde{\theta}_{d}=\theta_{d}\cdot\min(\rho_{d}/\widetilde{\lambda}_{d},1)$
(2)

###  3.2 Block Coordinate Descent Algorithm

In this work, we use Three-splitting scheme [33] to solve problem (1). First,
we introduce the variables $\\{{\mathbf{U}}_{d}\\}_{d=0}^{D-1}$ and rewrite
the problem as follows:

$\min_{{\bm{\theta}}}\mathcal{L}({\bm{\theta}},{\bm{x}}):={\mathcal{R}}(\theta_{D},{\bm{x}}_{D};y)\quad\text{s.t.}\quad{\bm{x}}_{d+1}=\sigma_{d}(\bm{U}_{d}),\
\bm{U}_{d}=\theta_{d}{\bm{x}}_{d}\quad d=0,\ldots,D-1$ (3)

We then consider the Lagrangian function of the problem (3) with a multiplier
co-efficient $\gamma$, which is set $1$ in this work.

${\mathcal{F}}({\bm{\theta}},{\bm{x}},{\mathbf{U}})={\mathcal{R}}(\theta_{D},{\bm{x}}_{D};y)+\frac{\gamma}{2}\sum_{d=0}^{D-1}(\|{\bm{x}}_{d+1}-\sigma_{d}({\mathbf{U}}_{d})\|_{2}^{2}+\|{\mathbf{U}}_{d}-\theta_{d}{\bm{x}}_{d}\|_{F}^{2})$
(4)

${\mathcal{F}}$ is a function of $\\{\theta_{d}\\}_{d=0}^{D}$,
$\\{{\bm{x}}_{d}\\}_{d=0}^{D}$ and $\\{{\mathbf{U}}_{d}\\}_{d=0}^{D-1}$. For
notation simplicity, we only explicitly highlight the parameter we consider
for ${\mathcal{F}}$ if there is no ambiguity. For example
${\mathcal{F}}(\theta^{\prime}_{d})$ means we update the parameter
$\theta_{d}$ in ${\mathcal{F}}$ while keeping the other parameters fixed. We
use block coordinate descent to update parameters of ${\mathcal{F}}$ where we
treat each layer as a sub-problem. The algorithm is summarized in Algorithm 1.
Considering the loss function ${\mathcal{R}}$ is a convex function w.r.t. both
$\theta_{D}$ and ${\bm{x}}_{D}$, we have $\forall d$,
${\mathcal{F}}(\theta_{d})$ is convex w.r.t. $\theta_{d}$, and $\forall d$,
${\mathcal{F}}({\bm{x}}_{d})$ is convex w.r.t. ${\bm{x}}_{d}$.

To update $\theta_{d}$, Algorithm 1 also considers the damping term
$\frac{1}{2\eta}\|\theta_{d}-\theta^{\prime}_{d}\|_{F}^{2}$ and the
regularization term $r_{d}(\theta^{\prime}_{d})$, which can be optimized by
the proximal gradient descent elaborated in the next section. To update
${\bm{x}}_{d}$, we have the analytical solution due to the convexity of
${\mathcal{F}}({\bm{x}}_{d})$.

${\bm{x}}_{d}\leftarrow\begin{cases}\left(\theta^{T}_{d}\theta_{d}+{\mathbf{I}}\right)^{-1}\left(\theta^{T}_{d}{\mathbf{U}}_{d}+\sigma({\mathbf{U}}_{d-1})\right)&\text{if}\
d=0,1,...,D-1.\\\
\mathrm{Prox}_{\frac{1}{\gamma},{\mathcal{R}}}(\sigma_{D-1}({\mathbf{U}}_{d-1})).&\text{if}\
d=D\end{cases}$ (5)

To update ${\mathbf{U}}_{d}$, we utilize Zeng et al. [33, Lemma 13] as follows
to obtain the analytical solution.

${\mathbf{U}}_{d}\leftarrow\begin{cases}\theta_{d}{\bm{x}}_{d}&\text{if}-{\bm{x}}_{d+1}\leq\theta_{d}{\bm{x}}_{d}\leq-(\sqrt{2}-1){\bm{x}}_{d+1}\leq
0.\\\ \min\\{0,\theta_{d}{\bm{x}}_{d}\\}&\text{if}\
\theta_{d}{\bm{x}}_{d}+{\bm{x}}_{d+1}\leq 0.\\\
\frac{1}{2}\left(\theta_{d}{\bm{x}}_{d}+{\bm{x}}_{d+1}\right)&\text{otherwise}.\end{cases}$
(6)

Algorithm 1 Stochastic Block Coordinate Descent For Lipschitz Neural Network

Input: training set, regularization schemes $\\{r_{d}\\}_{d=0}^{D}$, parameter
$\eta$, batch size $b$, Lipschitz constant $\rho$.

Initialization:
$\\{\theta_{d}\\}_{d=0}^{D},\\{{\bm{x}}_{d}\\}_{d=0}^{D},\\{{\bm{U}}_{d}\\}_{d=0}^{D-1}$.

for epoch $k=0,1,\ldots,K-1$ do

for each mini-batch of size $b$ do

for layer $d=0,1,\ldots,D$ do

Update $\theta_{d}$, ${\mathbf{U}}_{d}$, ${\bm{x}}_{d}$ simultaneously as
follows:

${\bm{x}}_{d}\leftarrow\operatorname*{arg\,min}_{{\bm{x}}^{\prime}_{d}}{\mathcal{F}}({\bm{x}}^{\prime}_{d})$

${\mathbf{U}}_{d}\leftarrow\operatorname*{arg\,min}_{{\mathbf{U}}^{\prime}_{d}}{\mathcal{F}}({\mathbf{U}}^{\prime}_{d})$

Normalize $\theta_{d}$ by (2) with coefficient $\rho$.

$\theta_{d}\leftarrow\operatorname*{arg\,min}_{\theta^{\prime}_{d}}{\mathcal{F}}(\theta^{\prime}_{d})+\frac{1}{2\eta}\|\theta_{d}-\theta^{\prime}_{d}\|_{F}^{2}+r_{d}(\theta^{\prime}_{d})$

end for

end for

end for

Algorithm 2 Differentially Private Stochastic Block Coordinate Descent For
Lipschitz Neural Network

Input: training set, regularization schemes $\\{r_{d}\\}_{d=0}^{D}$, step size
$\eta$, batch size $b$, noise control function $o(\eta,k,j)$, Lipschitz
constant $\rho$.

Initialization:
$\\{\theta_{d}\\}_{d=0}^{D},\\{{\bm{x}}_{d}\\}_{d=0}^{D},\\{{\bm{U}}_{d}\\}_{d=0}^{D-1}$.

for epoch $k=0,1,\ldots,K-1$ do

for each mini-batch of size $b$ do

for layer $d=0,1,\ldots,D$ do

Update $\theta_{d}$, ${\mathbf{U}}_{d}$, ${\bm{x}}_{d}$ simultaneously as
follows:

${\bm{x}}_{d}\leftarrow\operatorname*{arg\,min}_{{\bm{x}}^{\prime}_{d}}{\mathcal{F}}({\bm{x}}^{\prime}_{d})$

${\mathbf{U}}_{d}\leftarrow\operatorname*{arg\,min}_{{\mathbf{U}}^{\prime}_{d}}{\mathcal{F}}({\mathbf{U}}^{\prime}_{d})$

Normalize $\theta_{d}$ by (2) with coefficient $\rho$.

Update $\theta_{d}$ based on (8)

end for

end for

end for

Now, we assume the activations $\\{{\bm{x}}_{d}\\}_{d=0}^{D}$ are bounded.

###### Assumption 3.1

(Bounded layer input) $\forall d$, $\exists X_{d}<+\infty$ such that
${\bm{x}}_{d}$ always satisfies $\|{\bm{x}}_{d}\|_{2}^{2}\leq X_{d}$.

Bounded input assumption is common in the machine learning community. Since we
loosen $\\{{\bm{x}}_{d}\\}_{d=1}^{D}$ in Equation (4), we bound these
intermediate activations as well. This assumption is benign, because
${\bm{x}}_{0}$ is anchored as the input, and $\\{{\bm{x}}_{d}\\}_{d=1}^{D}$
are softly constrained by several quadratic terms in Equation (4) that we aim
to jointly minimize.

The following lemma confirms the smoothness of the function
${\mathcal{F}}(\theta_{d})$ as a function of $\theta_{d}$, the loss function
for layerwise parameters.

###### Lemma 3.2

If Assumption 3.1 is satisfied, and the activation function is ReLU, then the
function ${\mathcal{F}}(\theta_{d})$ for any layer $0\leq d\leq D$ is
$\beta_{d}$-smooth and the smoothness constant $\beta_{d}$ is $\gamma
X_{d}^{2}$.

We have to highlight that the $\mathcal{F}(\theta_{d})$ assumes that other
parameters except $\theta_{d}$ are fixed. In addition, Lemma 3.2 indicates
that the smoothness constant $\beta_{d}$ does not depend on other parameters.
Based on this, we can calculate the Hessian matrix of
${\mathcal{F}}(\theta_{d})$ as
$\nabla^{2}{\mathcal{F}}(\theta_{d})={\bm{x}}_{d}{\bm{x}}_{d}^{T}\geq 0$.
Therefore, ${\mathcal{F}}(\theta_{d})$ is convex w.r.t. $\theta_{d}$.

##  4 Differentially Private Stochastic Block Coordinate Descent

In this section, we propose Differentially Private Stochastic Block Coordinate
Descent (DP-SBCD), i.e., the differentially private version of Algorithm 1. We
then calculate the algorithm’s privacy loss under the hidden state assumption.
We discuss the privacy loss in a generic form, especially the case when using
adaptive calibrated noise.

###  4.1 Differentially Private Update Scheme

We first consider the update scheme for $\theta_{d}$ in Algorithm 1 and use
first order Taylor expansion of ${\mathcal{F}}(\theta^{\prime}_{d})$ to write
it in the proximal gradient descent format.

$\theta_{d}\leftarrow\operatorname*{arg\,min}_{\theta^{\prime}_{d}}\langle\nabla{\mathcal{F}}(\theta_{d}),\theta^{\prime}_{d}-\theta_{d}\rangle+\frac{1}{2\eta}\|\theta^{\prime}_{d}-\theta_{d}\|_{F}^{2}+r_{d}(\theta^{\prime}_{d})=\text{Prox}_{\eta,r_{d}}\left(\theta_{d}-\eta\nabla{\mathcal{F}}(\theta_{d})\right)$
(7)

Owing to the post-processing immunity of differential privacy, the privacy
guarantee is required for each sub-problem. Furthermore, as the algorithm
converges gradually, the gradient $\nabla{\mathcal{F}}(\theta_{d})$
diminishes, prompting the use of calibrated noise with an adaptive variance
instead of a fixed one. As a result, we propose the following update scheme:

$\displaystyle\theta_{d}\leftarrow\text{Prox}_{\eta,r_{d}}\left(\theta_{d}-\eta\nabla{\mathcal{F}}(\theta_{d})+\mathcal{N}(0,2\eta\cdot
o\left(\eta,k,j\right){\mathbf{I}})\right)$ (8)

where ${\mathcal{N}}(0,{\mathbf{I}})$ is the standard Gaussian distribution,
$o(\eta,k,j)$ is a function of the step size $\eta$, epoch index $k$ and
iteration index $j$ to control the magnitude of the calibrated noise. By
incorporating the update scheme (8) into Algorithm 1, we obtain Algorithm 2,
which will be proved to guarantee differential privacy in the following
section.

###  4.2 Privacy Loss of Sub-problems

We now study the privacy loss of Algorithm 2. Leveraging the post-processing
immunity and composition property, we can establish an upper bound of the
privacy loss of Algorithm 2 by summing the privacy losses of its individual
sub-problems. Consequently, our primary focus here is to estimate the privacy
loss associated with each sub-problem. For notation simplicity, we omit the
subscript $d$ in this subsection, as our analyses apply to any sub-problem.

In each iteration of Algorithm 2, the value of $\theta$ is updated by (8) and
then normalized by (2). Among them, it is clear that the scaling operation of
$\theta$ in (2) does not contribute to the privacy loss, so we focus on the
update scheme (8).

We regard the update scheme (8) in Algorithm 2 as a diffusion process [5, 9,
32]. Specifically, the update scheme consists of three parts: The gradient
descent part $\theta-\eta\nabla\mathcal{F}(\theta)$; The noise part
$o(\eta,k,j)$; The proximal operator associated with a convex regularization
function $r$. From a distributional perspective, let $\Theta$ be the
distribution of the parameter $\theta$, then the distribution of the parameter
after one-step update in (8) can be represented as follows:

$\displaystyle\widetilde{\Theta}$
$\displaystyle=T_{\\#}(F_{\\#}(\Theta)*{\mathcal{N}}(0,2t\cdot
o(\eta,k,j){\mathbb{I}}_{d}))$ (9)

where $F_{\\#}$ and $T_{\\#}$ are two push-forward mappings. $F$ represents
the gradient descent update, $T$ represents the proximal operator, and $*$
represents the convolution operator between two distributions.

Based on the smoothness property of ${\mathcal{F}}(\theta)$ indicated in Lemma
3.2, we prove the Lipschitz continuity of the first part of the update scheme
(8).

######  Lemma 4.1 (Lipschitz continuity for $F$)

If ${\mathcal{F}}(\theta)$ is a $\beta$-smooth function and
$\nabla^{2}{\mathcal{F}}(\theta)\geq\omega$, then the update function
$F(\theta)=\theta-\eta\nabla{\mathcal{F}}(\theta)$ is Lipschitz continuous
with a constant $L_{F}\leq\max\\{|1-\eta\omega|,|1-\eta\beta|\\}$.

We also need to highlight that the $\mathcal{F}(\theta)$ in the Lemma 4.1
assumes that other parameters except $\theta$ are fixed. In addition, the
bound of the Lipschitz constant derived in Lemma 4.1 does not depend on other
parameters. That is to say, the bound in Lemma 4.1 is valid for arbitrary
values of other parameters. Since ${\mathcal{F}}(\theta)$ is proven convex in
Section 3, $0\leq\omega\leq\beta$. As a result, the Lipschitz constant will be
dominated by the convexity term $|1-\eta\omega|$ when the step size
$\eta\leq\frac{2}{\omega+\beta}$ and otherwise the smoothness term
$|1-\eta\beta|$.

Similarly, we can prove the Lipschitz continuity of the third part of the
update scheme (8).

######  Lemma 4.2 (Lipschitz continuity for $T$)

If $\eta>0$ and $r(\theta)$ is a convex function, then the proximal operator
function
$T(\theta)=\text{Prox}_{\eta,r}(\theta)=\operatorname*{arg\,min}_{\widetilde{\theta}}\left\\{r(\widetilde{\theta})+\frac{1}{2\eta}\|\widetilde{\theta}-\theta\|^{2}_{2}\right\\}$
is Lipschitz continuous with a constant $L_{T}\leq 2$.

Typical examples of the regularization function $r$ include 1) no
regularization: $r(\theta)=0$, and then $\text{Prox}_{\eta,r}(\theta)=\theta$;
2) $l_{2}$ regularization in weight decay:
$r(\theta)=\frac{1}{2}\|\theta\|_{2}^{2}$, and then
$\text{Prox}_{\eta,r}(\theta)=\frac{\eta}{1+\eta}\theta$; 3) $l_{1}$
regularization in LASSO: $r(\theta)=\|\theta\|_{1}$, and then
$\text{Prox}_{\eta,r}(\theta)=sign(\theta)\cdot\max(0,|\theta|-\eta)$. In all
these three cases, the proximal function is Lipschitz continuous and the
Lipschitz constant is $1$.

Now we assume that $\theta$ for each subproblem satisfies the log-Sobolev
inequality (LSI), which is a benign assumption used in Vempala and Wibisono
[30], Ye and Shokri [32]. The formal definition of log-Sobolev inequality is
provided in Definition 4.3. Based on the log-Sobolev inequality assumptions
and Lipschitzness (Lemma 4.1,4.2), we consider the recursive privacy dynamics
for Equation (9) and bound the change rate of RDP during one step of noisy
mini-batch proximal gradient descent.

###### Definition 4.3

(Log-Sobolev Inequality [30]) A distribution $\nu$ over ${\mathbb{R}}^{d}$
satisfies log-Sobolev inequality (LSI) with a constant $c$ if $\forall$ smooth
function $g:{\mathbb{R}}^{d}\to{\mathbb{R}}$ with
$\mathbb{E}_{\theta\sim\nu}[g^{2}(\theta)]<+\infty$,

$\mathbb{E}_{\theta\sim\nu}[g^{2}(\theta)\log\left(g^{2}(\theta)\right)]-\mathbb{E}_{\theta\sim\nu}[g^{2}(\theta)]\log\mathbb{E}_{\theta\sim\nu}[g^{2}(\theta)]\leq\frac{2}{c}\mathbb{E}_{\theta\sim\nu}[\|\nabla
g(\theta)\|^{2}_{2}]$ (10)

It is an extension of Ye and Shokri [32, Lemma 3.2] to the cases of non-convex
loss functions, proximal gradient descent and adaptive calibrated noise.

To derive the privacy loss of Algorithm 2, we assume a bounded sensitivity of
the total gradient.

###### Assumption 4.4

(Sensitivity of the Total Gradient) The $l_{2}$ sensitivity of the total
gradient $\mathbb{E}_{D}\nabla{\mathcal{F}}(\theta)$ is finite. That is to
say, $\exists S_{g}<+\infty$ such that for any dataset $D$ and its
neighbouring dataset $D^{\prime}$ that only differs in one instance, we have
$S_{g}=\max_{D,D^{\prime},\theta}\|\mathbb{E}_{D}\nabla{\mathcal{F}}(\theta)-\mathbb{E}_{D^{\prime}}\nabla{\mathcal{F}}(\theta)\|_{2}$.

Under Assumption 4.4, we obtain the privacy loss of the Algorithm 2 for each
iteration.

###### Corollary 4.5

Under Assumption 4.4 where the sensitivity of the total gradient is
$S_{g}<+\infty$, let $D$, $D^{\prime}$ be an arbitrary pair of the neighboring
datasets that only differ in the $i_{0}$-th data point (i.e. $x_{i_{0}}\neq
x_{i_{0}}^{\prime}$). Let $B_{k}^{j}$ be a fixed mini-batch used in the $j$-th
iteration of the $k$-th epoch in Algorithm 2, which contains $b$ different
training instances whose indices are sampled from $\\{0,1,\ldots,n-1\\}$. We
denote $\theta_{k}^{j}$ and ${\theta^{\prime}}_{k}^{j}$ as the intermediate
parameters in Algorithm 2 when using datasets $D$ and $D^{\prime}$,
respectively. If the distributions of $\theta_{k}^{j}$ and
${\theta^{\prime}}_{k}^{j}$ satisfy log-Sobolev inequality with a constant
$c$, the update function $F(\theta)=\theta-\eta\nabla{\mathcal{F}}(\theta)$
and the proximal operator $T(\theta)=Prox_{\eta,r}(\theta)$ are Lipschitz
continuous with Lipschitz constant $L_{F}$ and $L_{T}$, respectively, then the
following recursive bound for Rényi divergence holds for any order $\alpha>1$:

1) If $i_{0}\not\in B_{k}^{j}$, then
$\frac{R_{\alpha}(\theta_{k}^{j+1}||{\theta^{\prime}}_{k}^{j+1})}{\alpha}$ is
upper bounded by
$\frac{R_{\alpha^{\prime}}(\theta_{k}^{j}||{\theta^{\prime}}_{k}^{j})}{\alpha^{\prime}}\cdot\left(1+\frac{c\cdot
2\eta\cdot o(\eta,k,j)}{L_{F}^{2}}\right)^{-1/L_{T}^{2}}$ where the order
$\alpha^{\prime}=(\alpha-1)\left(1+\frac{c\cdot 2\eta
o(\eta,k,j)}{L_{F}^{2}}\right)^{-1}+1$.

2) If $i_{0}\in B_{k}^{j}$, then
$\frac{R_{\alpha}(\theta_{k}^{j+1}||{\theta^{\prime}}_{k}^{j+1})}{\alpha}$ is
upper bounded by
$\frac{R_{\alpha}(\theta_{k}^{j}||{\theta^{\prime}}_{k}^{j})}{\alpha}+\frac{\eta
S_{g}^{2}}{4b^{2}\cdot o(\eta,k,j)}$.

Compared with the results discussed in Ye and Shokri [32] which only study the
case without proximal operator, the privacy loss decay rate in the first case
of Corollary 4.5 is powered by $-1/L_{T}^{2}$ instead of $-1$, corresponding
to the factor $1/L_{T}^{2}$ in the formulation of $c_{t}$ in the change rate
of RDP. This indicates that the Lipschitz constant $L_{T}$ of the proximal
operator also affects the privacy loss decay, a.k.a. privacy amplification
when we run Algorithm 2 in the hidden state assumption. The smaller
$L_{T}^{2}$ is, the better privacy guarantee will be obtained. Corollary 4.5
concludes the change of the privacy loss for one iteration in Algorithm 2.

By applying Corollary 4.5 iteratively, we can obtain the algorithm’s privacy
loss for the whole training phase. The formal theorem is demonstrated below.

###### Theorem 4.6

Under Assumption 4.4 where the sensitivity of the total gradient is
$S_{g}<+\infty$, the distribution of $\theta$ satisfies log-Sobolev inequality
with a constant $c$. In addition, the update function
$F(\theta)=\theta-\eta\nabla{\mathcal{F}}(\theta)$ and the proximal operator
$T(\theta)=\mathrm{Prox}_{\eta,r}(\theta)$ are Lipschitz continuous with
Lipschitz constant $L_{F}$ and $L_{T}$, respectively. If we use Algorithm 2 to
train model parameters $\theta$ for $K\geq 1$ epochs, then the algorithm
satisfies $(\alpha,\varepsilon(\alpha))$-Rényi differential privacy with the
constant:

$\varepsilon_{K}(\alpha)\leq\frac{1}{\alpha-1}\log\left(\sum_{j_{0}=0}^{n/b-1}\frac{b}{n}\cdot
e^{(\alpha-1)\left(\varepsilon_{K}(\alpha,j_{0})\right)}\right)$

where:

$\varepsilon_{K}(\alpha,j_{0})\leq\alpha\sum_{k=0}^{K-1}\frac{\eta
S_{g}^{2}}{4b^{2}\cdot
o(\eta,k,j_{0})}\cdot\left(\frac{c^{j_{0}+1}_{k}}{c^{n/b-1}_{K}}\left(\frac{1}{L_{F}^{2}L_{T}^{2}}\right)^{(n/b-1)(K-k)-j_{0}}\prod_{l=k}^{K}\frac{c^{j_{0}+1}_{l}}{c^{j_{0}}_{l}}\right)^{-1/L_{T}^{2}}$
(11)

In Inequality (11), $c^{j}_{k}$ is the log-Sobolev inequality constant for the
distribution of the model parameters in the $j$-th iteration of the $k$-th
epoch. The value of $c^{j}_{k}$ is calculated based on Lemma 4.7.

Proof Sketch. For each iteration of the Algorithm 2, the update scheme (8)
fixed parameters except the $\theta$. Hence, although the
$\mathcal{F}(\theta)$ in the update scheme differs among each iteration
because of different fixed parameters, it maintains Lipschitzness in each
iteration. Hence, we could use Corollary 4.5 to analyze the algorithm’s
privacy loss. In each epoch, there is one and only one different mini-batch
for two neighboring datasets, so we assume it is the $j_{0}$-th batch w.l.o.g.
and apply case 2) of Corollary 4.5 for this mini-batch update and case 1) of
Corollary 4.5 for the other updates. For any $\alpha$, the original privacy
loss is $0$ and the recursive bound in Corollary 4.5 holds. Therefore, we can
uniformly bounded the value of $\frac{\varepsilon_{K}(\alpha,j_{0})}{\alpha}$
for any $\alpha$. Finally, since $j_{0}$ is uniformly distributed among the
index set $\\{0,1,\ldots,n/b-1\\}$, we use the joint convexity of scaled
exponentiation of Rényi divergence to bound the final privacy loss
$\varepsilon_{K}(\alpha)$. $\Box$

###### Lemma 4.7

(LSI constant sequence in Algorithm 2) For each layer’s update scheme in
Algorithm 2 with a batch size of $b$, if the update function
$F(\theta)=\theta-\eta\nabla f(\theta)$ and the proximal operator
$T(\theta)=Prox_{\eta,r}$ are Lipschitz continuous with Lipschitz constant
$L_{F}$ and $L_{T}$, respectively, then the distribution of parameter
$\theta_{k}^{j}$ in the $j$-th iteration of the $k$-th epoch satisfies
$c_{k}^{j}$ log-Sobolev inequality (LSI) and the constant $c_{k}^{j}$ is
calculated by:

$\displaystyle c_{k}^{j}$ $\displaystyle=\frac{1}{2\eta
L_{T}^{2}}\left(\sum^{k-1}_{k^{\prime}=0}\sum^{n/b-1}_{j^{\prime}=0}o(\eta,k^{\prime},j^{\prime})(L_{F}L_{T})^{2((k-k^{\prime})(n/b)-j^{\prime}+j-1)}\right.+\left.\sum_{j^{\prime}=0}^{j-1}o(\eta,k,j^{\prime})(L_{F}L_{T})^{2(j-j^{\prime}-1)}\right)^{-1}$

$\varepsilon_{K}(\alpha,j_{0})$ in the Theorem 4.6 represents the privacy loss
when the only different instance of the two neighboring datasets is in the
$j_{0}$-th mini-batch of each epoch. The $\varepsilon_{K}(\alpha,j_{0})$ shows
that the overall privacy loss is the summation of each epoch’s privacy loss
term $\frac{\eta S_{g}^{2}}{4b^{2}\cdot o(\eta,k,j)}$ times a decay rate term
$\left(\frac{c^{j_{0}+1}_{k}}{c^{n/b-1}_{K}}\left(\frac{1}{L_{F}^{2}L_{T}^{2}}\right)^{(n/b-1)(K-k)-j_{0}}\prod_{l=k}^{K}\frac{c^{j_{0}+1}_{l}}{c^{j_{0}}_{l}}\right)^{-1/L_{T}^{2}}$.
More importantly, Algorithm 2 maintains the decay rate term smaller than $1$
and decreases with the increase in $K$.

Theorem 4.6 improves the results in existing works from many aspects for
estimating the differential privacy under hidden state assumptions. Firstly,
it is more generally applicable to different algorithms. Theorem 4.6 could
easily extend the analyses and privacy guarantees from the gradient descent
algorithm with calibrated noise from a fixed distribution to proximal gradient
descent with adaptive calibrated noise. Second, it provides a feasible privacy
loss accountant for non-convex problems with adaptive noise. In contrast to
the assumption of strong convexity and $\beta$-smoothness on the objective
function in existing results, Theorem 4.6 shows that Algorithm 2 applicable to
general neural networks with Lipschitz constraints. Finally, even when
downgrading to the case of gradient descent with calibrated noise sampled from
fixed distributions, Theorem 4.6 has a tighter bound than previous work [32,
Theorem 3.3]. This is because we directly bound
$\varepsilon_{K}(\alpha,j_{0})$ by recursively applying Corollary 4.5. By
contrast, Ye and Shokri [32] approximate the bound
$\varepsilon_{K}(\alpha,j_{0})$ by part of iterations in one epoch rather than
the whole epoch.

###  4.3 Privacy Loss variation under the Adaptive Noise

As discussed above, the bound of $\varepsilon_{K}(\alpha,j_{0})$ in Theorem
4.6 elucidates how each epoch influences the cumulative privacy loss,
exhibiting a decay rate. Specifically, these contributions are inversely
proportional to $o(\eta,j,k)$, i.e., the variance of the noise, and decrease
exponentially 111While not strictly exponential due to variations in the log-
Sobolev inequality constant, the behavior closely resembles that of an
exponential function curve in simulations. as the number of iterations and
epochs increase. That is to say, under the hidden state assumption, the
calibrated noise in the last few epochs primarily contributes to the total
privacy loss.

Figure 1: Common hyper-parameter settings: Lipschitz constant $\rho=0.99$,
batch size $b=100$, stepsize $\eta=0.01$, data set $n=2100$. (a) Each epoch’s
privacy loss contribution for the Algorithm 2 for $K=30$ epochs. We study the
scenarios of both fixed and adaptive noise. Each scenario contains three
situations($j_{0}=0,15,30$). In the fixed noise scenario, the
$o(\eta,k,j)=0.01$, while in the adaptive noise scenario, the
$o(\eta,k,j)=0.01-0.003k$. (b) Privacy loss for different numbers of epochs
$K$ for Algorithm 2. We show four scenarios: noise decay means
$o(\eta,k,j)=0.001-0.0003k$, noise constant means $o(\eta,k,j)=0.0005$, noise
increase means $o(\eta,k,j)=0.0001+0.0003k$, and noise decrease-constant means
that $o(\eta,k,j)=0.0005-0.00003k$ where $k\in[1,10]$ and remain
$o(\eta,k,j)=0.0002$ where $k\in[10,30]$.

We illustrate this phenomenon in Figure 1, which encompasses scenarios with
both constant and non-constant $o(\eta,j,k)$ values. The numerical results
align with the analysis, as indicated by the near-linear curves observed in
the logarithmic scale graph. Furthermore, we observe that a larger value of
$j_{0}$, signifying a delayed occurrence of the mini-batch containing the
unique instance, leads to a smaller privacy loss during the initial stages of
training. However, as the training progresses, this disparity diminishes. This
observation is consistent with Theorem 4.6, as the privacy loss is zero for
the first $j_{0}$ mini-batches of the first epoch.

Theorem 4.6 also enhances our understanding of the convergence of the privacy
loss, initially proposed in Feldman et al. [13]: when $o(\eta,k,j)$ is a
constant, an equilibrium solution emerges between the privacy loss and the
decay rate after several epochs, resulting in the convergence of privacy loss
under the hidden state assumption. In the case of adaptive calibrated noise,
Figure 1 shows the tendency of privacy loss under four distinct noise
settings. Empirical findings suggest that privacy loss converges when a
constant magnitude of noise is utilized in the later stages of training.
Conversely, the privacy loss diverges if the noise magnitude continues to
decrease in the late phase of training. In contrast, increasing the noise
magnitude can even lead to a decrease in privacy loss. However, it is worth
noting that noise with a smaller variance tends to yield better utility for
the model compared to noise with a larger variance, which is consistent with
the utility-privacy trade-off [2, 3].

##  5 Numerical Experiments

We run numerical simulations in this section to investigate the model’s
utility and privacy loss in different training phases when we use different
distributions to sample calibrated noise.

We mainly utilize the Madelon dataset in this section. The Madelon dataset was
originally introduced as a challenging classification problem in the NIPS
$2003$ feature selection challenge [17]. This synthetic dataset comprises
$6000$ instances, each with $20$ features and belonging to one of the five
classes. To ensure an unbiased evaluation, we divided the dataset into a
training set, accounting for 80% of the data, and a testing set, containing
the remaining 20%. The batch size is $960$.

We employ a multilayer perceptron (MLP) model with four layers, each of which
has $200$ neurons. The activation function is the commonly used ReLU function,
and we use squared loss as the loss function. In addition, we set the
layerwise Lipschitz constant $\rho=3$ and the step size $\eta=0.01$. To
guarantee privacy, we applied Theorem 4.6 and employed the privacy loss
calculation with $\alpha=100$. All the experiments can be efficiently executed
on a single NVIDIA RTX 5000 Ada GPU.

The experiment compares the algorithm’s utility under different noise
strategies: the constant strategy with $o(\eta,k,j)=0.01$ and the decrease
strategy with a linear decay rate of $0.0008$ per epoch and final noise
variance $o(\eta,K,j)=0.0075$. The decrease strategy is designed in a manner
so that the privacy loss of both strategies will be approximately the same for
the same number of epochs $K$. Based on the aforementioned setup, we train the
model $50$ times where the total number of epochs $K$ varies from $10$ to
$50$. We run the whole experiment 5 times and report both the average
performance and the standard deviation. The results are demonstrated in Figure
2 and Table 1.

Table 1: The accuracy(in % under 95% confidential interval) and the privacy
loss of Algorithm 2 when we use different noise strategies and train the model
for different numbers of epochs. D means noise decrease scenario and C means
noise constant scenario

epoch | Noise |  privacy loss |  AVG ACC.
---|---|---|---
10 | D | 0.040556 |  20.13($\pm 0.32$)
20 | D | 0.040648 |  42.15($\pm 9.35$)
30 | D | 0.040688 |  92.10($\pm 2.20$)
40 | D | 0.040704 |  93.98($\pm 1.38$)
50 | D | 0.040708 |  94.37($\pm 1.46$)
10 | C | 0.041408 |  20.03($\pm 0.59$)
20 | C | 0.040652 |  23.57($\pm 6.89$)
30 | C | 0.040696 |  53.35($\pm 17.68$)
40 | C | 0.040712 |  82.35($\pm 7.98$)
50 | C | 0.040716 |  91.16($\pm 3.20$)

Figure 2: Relationship between model’s utility and privacy loss under
different noise strategies. For each noise strategy, we run Algorithm 2 for
different numbers of epochs to plot the curve.

The experiment results validate the effectiveness of Algorithm 2. What’s more,
with proper settings of adaptive calibrated noise, the algorithm can
demonstrate a better trade-off between the model’s utility and privacy. For
the examples in Table 1, we see higher utilities and lower privacy loss when
we use adaptive calibrated noise. In Figure 2, we see the curve of adaptive
calibrated noise above one of its counterparts in most cases.

##  6 Conclusion

We propose differentially private stochastic block coordinate descent (DP-
SBCD) algorithm, which includes proximal gradient descent and adaptive noise,
to train neural networks. As far as we are aware, DP-SBCD is the first
algorithm capable of addressing non-convex training problems while ensuring
differential privacy guarantees under the hidden state assumption. The
adaptive noise proposed in our method can provide adjustable trade-offs
between the model’s utility and privacy. Moreover, our numerical experiments
show that under proper settings, our method could provide a better trade-off
between utility and privacy. Going forward, our future research will
concentrate on further refining the convergence and performance of the
algorithm and extending its applicability to more generic settings.

## References

  * Abadi et al. [2016] M. Abadi, A. Chu, I. Goodfellow, H. B. McMahan, I. Mironov, K. Talwar, and L. Zhang.  Deep learning with differential privacy.  In _Proceedings of the 2016 ACM SIGSAC conference on computer and communications security_ , pages 308–318, 2016.
  * Allouah et al. [2023] Y. Allouah, R. Guerraoui, N. Gupta, R. Pinot, and J. Stephan.  On the privacy-robustness-utility trilemma in distributed learning.  In A. Krause, E. Brunskill, K. Cho, B. Engelhardt, S. Sabato, and J. Scarlett, editors, _Proceedings of the 40th International Conference on Machine Learning_ , volume 202 of _Proceedings of Machine Learning Research_ , pages 569–626. PMLR, 23–29 Jul 2023.  URL https://proceedings.mlr.press/v202/allouah23a.html.
  * Alvim et al. [2012] M. S. Alvim, M. E. Andrés, K. Chatzikokolakis, P. Degano, and C. Palamidessi.  Differential privacy: on the trade-off between utility and information leakage.  In _Formal Aspects of Security and Trust: 8th International Workshop, FAST 2011, Leuven, Belgium, September 12-14, 2011. Revised Selected Papers 8_ , pages 39–54. Springer, 2012.
  * Asoodeh and Diaz [2023] S. Asoodeh and M. Diaz.  Privacy loss of noisy stochastic gradient descent might converge even for non-convex losses.  _arXiv preprint arXiv:2305.09903_ , 2023.
  * Balle et al. [2019] B. Balle, G. Barthe, M. Gaboardi, and J. Geumlek.  Privacy amplification by mixing and diffusion mechanisms.  _Advances in neural information processing systems_ , 32, 2019.
  * Behrmann et al. [2019] J. Behrmann, W. Grathwohl, R. T. Chen, D. Duvenaud, and J.-H. Jacobsen.  Invertible residual networks.  In _International conference on machine learning_ , pages 573–582. PMLR, 2019.
  * Béthune et al. [2022] L. Béthune, T. Boissin, M. Serrurier, F. Mamalet, C. Friedrich, and A. Gonzalez Sanz.  Pay attention to your loss: understanding misconceptions about lipschitz neural networks.  _Advances in Neural Information Processing Systems_ , 35:20077–20091, 2022.
  * Béthune et al. [2023] L. Béthune, T. Masséna, T. Boissin, Y. Prudent, C. Friedrich, F. Mamalet, A. Bellet, M. Serrurier, and D. Vigouroux.  Dp-sgd without clipping: The lipschitz neural network way.  _arXiv preprint arXiv:2305.16202_ , 2023.
  * Chourasia et al. [2021] R. Chourasia, J. Ye, and R. Shokri.  Differential privacy dynamics of langevin diffusion and noisy gradient descent.  _Advances in Neural Information Processing Systems_ , 34:14771–14781, 2021.
  * Dwork [2006] C. Dwork.  Differential privacy.  In _International colloquium on automata, languages, and programming_ , pages 1–12. Springer, 2006.
  * Erkin et al. [2009] Z. Erkin, M. Franz, J. Guajardo, S. Katzenbeisser, I. Lagendijk, and T. Toft.  Privacy-preserving face recognition.  In _Privacy Enhancing Technologies: 9th International Symposium, PETS 2009, Seattle, WA, USA, August 5-7, 2009. Proceedings 9_ , pages 235–253. Springer, 2009.
  * Fazlyab et al. [2019] M. Fazlyab, A. Robey, H. Hassani, M. Morari, and G. Pappas.  Efficient and accurate estimation of lipschitz constants for deep neural networks.  _Advances in Neural Information Processing Systems_ , 32, 2019.
  * Feldman et al. [2018] V. Feldman, I. Mironov, K. Talwar, and A. Thakurta.  Privacy amplification by iteration.  In _2018 IEEE 59th Annual Symposium on Foundations of Computer Science (FOCS)_ , pages 521–532. IEEE, 2018.
  * Fredrikson et al. [2015] M. Fredrikson, S. Jha, and T. Ristenpart.  Model inversion attacks that exploit confidence information and basic countermeasures.  In _Proceedings of the 22nd ACM SIGSAC conference on computer and communications security_ , pages 1322–1333, 2015.
  * Gouk et al. [2021] H. Gouk, E. Frank, B. Pfahringer, and M. J. Cree.  Regularisation of neural networks by enforcing lipschitz continuity.  _Machine Learning_ , 110:393–416, 2021.
  * Gu et al. [2020] F. Gu, A. Askari, and L. El Ghaoui.  Fenchel lifted networks: A lagrange relaxation of neural network training.  In _International Conference on Artificial Intelligence and Statistics_ , pages 3362–3371. PMLR, 2020.
  * Guyon et al. [2004] I. Guyon, S. Gunn, A. Ben-Hur, and G. Dror.  Result analysis of the nips 2003 feature selection challenge.  _Advances in neural information processing systems_ , 17, 2004.
  * Ha et al. [2019] T. Ha, T. K. Dang, T. T. Dang, T. A. Truong, and M. T. Nguyen.  Differential privacy in deep learning: an overview.  In _2019 International Conference on Advanced Computing and Applications (ACOMP)_ , pages 97–102. IEEE, 2019.
  * Haim et al. [2022] N. Haim, G. Vardi, G. Yehudai, O. Shamir, and M. Irani.  Reconstructing training data from trained neural networks.  _Advances in Neural Information Processing Systems_ , 35:22911–22924, 2022.
  * Kandpal et al. [2022] N. Kandpal, E. Wallace, and C. Raffel.  Deduplicating training data mitigates privacy risks in language models.  In _International Conference on Machine Learning_ , pages 10697–10707. PMLR, 2022.
  * Krizhevsky et al. [2012] A. Krizhevsky, I. Sutskever, and G. E. Hinton.  Imagenet classification with deep convolutional neural networks.  _Advances in neural information processing systems_ , 25, 2012.
  * Li et al. [2019] Q. Li, S. Haque, C. Anil, J. Lucas, R. B. Grosse, and J.-H. Jacobsen.  Preventing gradient attenuation in lipschitz constrained convolutional networks.  _Advances in neural information processing systems_ , 32, 2019.
  * Mahajan et al. [2017] D. Mahajan, S. S. Keerthi, and S. Sundararajan.  A distributed block coordinate descent method for training l1regularized linear classifiers.  _The Journal of Machine Learning Research_ , 18(1):3167–3201, 2017.
  * Mangold et al. [2022] P. Mangold, A. Bellet, J. Salmon, and M. Tommasi.  Differentially private coordinate descent for composite empirical risk minimization.  In K. Chaudhuri, S. Jegelka, L. Song, C. Szepesvari, G. Niu, and S. Sabato, editors, _Proceedings of the 39th International Conference on Machine Learning_ , volume 162 of _Proceedings of Machine Learning Research_ , pages 14948–14978. PMLR, 17–23 Jul 2022.
  * Mironov [2017] I. Mironov.  Rényi differential privacy.  In _2017 IEEE 30th computer security foundations symposium (CSF)_ , pages 263–275. IEEE, 2017.
  * Neyshabur et al. [2017] B. Neyshabur, S. Bhojanapalli, D. McAllester, and N. Srebro.  Exploring generalization in deep learning.  _Advances in neural information processing systems_ , 30, 2017.
  * Ponomareva et al. [2023] N. Ponomareva, H. Hazimeh, A. Kurakin, Z. Xu, C. Denison, H. B. McMahan, S. Vassilvitskii, S. Chien, and A. G. Thakurta.  How to dp-fy ml: A practical guide to machine learning with differential privacy.  _Journal of Artificial Intelligence Research_ , 77:1113–1201, 2023.
  * Shokri et al. [2017] R. Shokri, M. Stronati, C. Song, and V. Shmatikov.  Membership inference attacks against machine learning models.  In _2017 IEEE symposium on security and privacy (SP)_ , pages 3–18. IEEE, 2017.
  * Song et al. [2013] S. Song, K. Chaudhuri, and A. D. Sarwate.  Stochastic gradient descent with differentially private updates.  In _2013 IEEE global conference on signal and information processing_ , pages 245–248. IEEE, 2013.
  * Vempala and Wibisono [2019] S. Vempala and A. Wibisono.  Rapid convergence of the unadjusted langevin algorithm: Isoperimetry suffices.  _Advances in neural information processing systems_ , 32, 2019.
  * Wibisono [2019] A. Wibisono.  Proximal langevin algorithm: Rapid convergence under isoperimetry.  _arXiv preprint arXiv:1911.01469_ , 2019.
  * Ye and Shokri [2022] J. Ye and R. Shokri.  Differentially private learning needs hidden state (or much faster convergence).  _Advances in Neural Information Processing Systems_ , 35:703–715, 2022.
  * Zeng et al. [2019] J. Zeng, T. T.-K. Lau, S. Lin, and Y. Yao.  Global convergence of block coordinate descent in deep learning.  In _International conference on machine learning_ , pages 7313–7323. PMLR, 2019.
  * Zhang et al. [2017] C. Zhang, S. Bengio, M. Hardt, B. Recht, and O. Vinyals.  Understanding deep learning requires rethinking generalization.  In _International Conference on Learning Representations_ , 2017.  URL https://openreview.net/forum?id=Sy8gdB9xx.
  * Zhang and Brand [2017] Z. Zhang and M. Brand.  Convergent block coordinate descent for training tikhonov regularized deep neural networks.  _Advances in Neural Information Processing Systems_ , 30, 2017.