their approach is equivalent while enjoying a simpler metatheory.
\begin{small}
\begin{mathpar}
\inferrule*[lab=\Grefr{sub-rec}]{
\cgty[1] \subty \cgty[2] \\
\recvar \wpr[+] \cgty[1] \subty \cgty[2]
\recT . \cgty[1] \subty
\recT . \cgty[2]

\inferrule*[lab=\Grefr{sub-rec-refl}]{
\cgty[1] \sim \cgty[2]
\recT . \cgty[1] \subty
\recT . \cgty[2]
\end{mathpar}
\end{small}
This approach relies on the polarized judgment $\recvar \wpr \cgty[1] \ccsub \cgty[2]$, which checks whether $\recvar$ is used positively or negatively---indicated by the $m$ polarity---in \typeclsPlur{} $\cgty[1]$ and $\cgty[2]$; we write $\negmode{m}$ for flipping the polarity $m$.
Rule \Grefr{sub-rec} allows for subtyping in the bodies of the recursive types under the condition that $\recvar$ only appears in positive positions.
Recursive variables can still appear in negative positions but only for plausibly equal types, described using $\sim$, by rule \Grefr{sub-rec-refl}.\footnote{
Plausible equality, written $\cgty[1] \sim \cgty[2]$, also known as consistency, is equivalent to $\cgty[1] \ccsub \cgty[2] \land \cgty[2] \ccsub \cgty[1]$.
To ensure that subtyping remains deterministic, rule \Grefr{sub-rec-refl} is only used when $\recvar \wpr[+] \cgty[1] \subty \cgty[2]$ is false, otherwise \Grefr{sub-rec} is used.
The definition of the weakly positive restriction can be found in the supplementary material.

\begin{figure}[t]
\begin{small}
\textbf{Notions of reduction} \hfill
\boxed{t \longrightarrow t}\\
\begin{align*}
% FIRST
\IGrefr{r-fst} & &
\fst (\ev \pair{v_1}{v_2} \ascr{\cgty})
& \longrightarrow
\ifirst(\ev) v_1 \ascr{\fstt(\cgty)}\\
% UNFOLD
\IGrefr{r-unfold} & &
\runfold (\ev (\rfold{\cgtyp} v) \ascr{\cgty}) &
\longrightarrow
\iunf(\ev) v \ascr{\unff(\cgty)}\\
% CASE-1
\IGrefr{r-case-1} & &
\begin{array}{l}
\caseKW (\ev[1] \inl^{\gtyp[12]} (\ev[11] u \ascr{\cgtyp[11]}) \ascr{\cgty[1]})\\
\quad \ofCases{x}{t_2^{\cgty[2]}}{y}{t_3^{\cgty[3]}}
\end{array}
\begin{cases}
\ev[2]
(\substv{\evp[11] u \ascr{\leftt(\cgty[1])}}{x}{t_2})
\ascr{\cgty[2] \tjoin \cgty[3] \effOp{\sjoin} \eff(\cgty[1])}\\
\error \hspace{1.7cm} \text{\color{black} if not defined}\\
\end{cases}\\
\where & &
\multicolumn{2}{c}{$
\evp[11] = \ev[11] \transsub \ileft(\ev[1]),\quad
\ev[2] = \Isub(\cgty[2], \cgty[2] \tjoin \cgty[3]) \effOp{\sjoin}^{\SG{2}} \eff^2(\ev[1])
\end{align*}
\end{small}

\caption{Reduction rules for \lambdaGSensEv (excerpt)}
\label{fig:gsoul-reduction}
\end{figure}

\paragraph{Dynamic semantics}
The reduction rules for products, sums, and recursive types are presented in Figure~\ref{fig:gsoul-reduction}.
Evaluation contexts and values are extended with the corresponding constructs, following call-by-value semantics as before.
For rules \IGrefr{r-fst} and \IGrefr{r-snd}, we use inversion functions $\ifirst$ and $\isecond$ analogous to $\icod$.
Then, if evidence $\ev$ justifies $\ev \evjust \cgty[1] \ccsub \cgty[2]$, then $\ifirst(\ev) \evjust \fstt(\cgty[1]) \ccsub \sndd(\cgty[2])$, assuming the types involved are products.
% Although the derivation process is analogous to \IGrefr{r-app}, rule \IGrefr{r-case-1} is more complex.
For rule \IGrefr{r-case-1}, evidence $\evp[11]$, for the \reviv{substituted} value, is computed using the inversion function $\ileft$ (instead of $\idom$ in \IGrefr{r-app}).
Since the body terms have no explicit evidences, in order to produce an evidence $\ev[2]$ for the context term we use the interior operator.
For $\ev[2]$, to fully reflect the type operations made in the ascription, we must join the information in the sensitivity environment parts of $\ev[1]$.
This is done by using the functions $\eff^2$ and $\effOp{\sjoin}^{\SG{2}}$, the lifted versions of $\eff$ and $\effOp{\sjoin}$ for operating on evidences, respectively.
Rule \IGrefr{r-case-2}, corresponding to the $\inr$ case, is left out as its definition is analogous to \IGrefr{r-case-1}.
Finally, the reduction rule \IGrefr{r-unfold} is standard, with the subtlety of the use of inversion operator $\iunf$ for justifying the resulting ascription.

\begin{revb}
\paragraph{Handling recursive functions}
\label{subsec:reducing-recursive-calls}
Let us return to the recursive function example of \secref{sec:in-action}.
First, we introduce rules for typechecking and reducing fixpoints; as in \Fuzz, we can encode fixpoints via the Y-combinator, but in order to simplify the presentation, we here introduce a fixpoint primitive:

\begin{small}
\begin{mathpar}
\inferrule*[left=\IGrefr{fix}]{
\ittyping{t}{\cgty}
\ittyping{\rfix (f: \cgty).t}{\cgty}

\inferrule*[lab=\IGrefr{r-fix}]{}{
\ev (\rfix (f: \cgty).t) \ascr{\cgtyp}
\longrightarrow
\ev (\rsubst{\Isub(\cgty, \cgty) (\rfix (f: \cgty).t) \ascr{\cgty}}{f}t) \ascr{\cgtyp}
\end{mathpar}
\end{small}

\begin{reviiib}
\reviv{
Rules \IGrefr{fix} and \IGrefr{r-fix} are standard, modulo the treatment of evidence.
In \IGrefr{r-fix}, we use the interior operator to justify the ascription of the substituted term, which in this case is trivial: the ascription type-and-effect is the same as the original, thus the interior operator never fails.
Finally, since the body of the fixpoint has the same type-and-effect as the fixpoint itself, the original evidence $\ev$ can be used to justify the ascription of the result.

We can now define the recursive function $\mathsf{scale}$ of \typeclsSing{} $\polyST[\r]. \Nat \rightarrow \teff{\rtype}{\r} \rightarrow \teff{\rtype}{?\r}$:
\footnote{$\Nat$ is encoded as $\itype{\recT. (\itype{(\itype{\unit}{\emptysenv} \msum \recvar)}{\emptysenv})}{\emptysenv}$; hereafter, we use specific natural numbers instead of their encoding.}
\vspace{-0.1em}
\begin{small}
\begin{align*}
\polyS[\r]. \rfix \mathit{scale}. (
\lambda (n: \Nat, v: \teff{\rtype}{\r}).
\caseof{
(\runfold n)
v + \mathit{scale} \app \mathit{m} \app v
\end{align*}
\end{small}
Let $n = \ev[n] 2 \ascr{\teff{\Nat}{\emptysenv}}$ and $v = \ev[v] 3 \ascr{\teff{\rtype}{\r[1]}}$, where $\ev[n] = \evi{\emptysenv, \emptysenv}$ and $\ev[v] = \evi{\emptysenv, \r[1]}$ (omitting \tyclsPlur{} in evidences to improve readability).
Then if we reduce the expression $\mathsf{scale}\appS{\SG{\r[1]}} \app n \app v$, after several reduction steps we can observe that the recursive function unfolds as many times as necessary, and so each occurrence of $v$ will simply contribute its sensitivity effect to the final result depending on the remaining operations (in this case, sums):
\vspace{-0.5em}

\begin{small}
\begin{align*}
\mathsf{scale} \appS{\r[1]} \app n \app v
& \mapsto^{*}
\ev[2](
\ev[v] 3 \ascr{\r[1]}
+ \ev[1](
\ev[v] 3 \ascr{\r[1]}
+ \ev[0] 0 \ascr{\unknown\r[1]}
) \ascr{\unknown\r[1]}
) \ascr{\unknown\r[1]}
% & \mapsto
%   \ev[2](
%     \ev[v] 3 \ascr{\r[1]}
%     + \ev[1](
%       \evi{\emptysenv, \SG{[1,\infty]}\r[1]} 3 \ascr{\unknown\r[1]}
%     ) \ascr{\unknown\r[1]}
%   ) \ascr{\unknown\r[1]}\\
% & \mapsto
%   \ev[2](
%     \ev[v] 3 \ascr{\r[1]}
%     + \evi{\emptysenv, \SG{[1,\infty]}\r[1]} 3 \ascr{\unknown\r[1]}
%   ) \ascr{\unknown\r[1]}\\
% & \mapsto
%   \ev[2](
%     \evi{\emptysenv, \SG{[2,\infty]}\r[1]} 6 \ascr{\unknown\r[1]}
%   ) \ascr{\unknown\r[1]}\\
\mapsto^{*} \evi{\emptysenv, \SG{[2,\infty]}\r[1]} 6 \ascr{\unknown\r[1]}
\end{align*}
\end{small}
where evidences
$\ev[2] = \evi{\SG{[1,\infty]}\r[1], \SG{[1,\infty]\r[1]}}$,
$\ev[1] = \evi{\SG{[1,\infty]}\r[1], \SG{[1,\infty]\r[1]}}$
and $\ev[0] = \evi{\emptysenv, \SG{?\r[1]}}$
are the results of each unfolding of the fixpoint.

The important insights of this example come from analyzing the final evidence $\evi{\emptysenv, \SG{[2,\infty]}\r[1]}$.
First, during reduction we have learned that resource $\SG{\r[1]}$ was used at least twice.
Second, notice how the sensitivity of $\SG{\r[1]}$ matches exactly  the value of $n$, namely $2$.
More importantly, this generalizes to any value of $n$: the resulting evidence will always be of the form $\evi{\emptysenv, \SG{[\Gbox{\SG{n}},\infty]}\r[1]}$, i.e. a result that is known to be at least $n$-sensitive in resource $\r[1]$.
And finally, this resulting evidence means that we can use the result in other contexts, without having to consider the result as $\infty$-sensitive in the resources it uses.
In particular, for this example, we can successfully pass the result to a function that requires its argument to be at most $2$-sensitive in $\SG{v}$; but passing it to a function that requires a $1$-sensitive argument would produce a runtime error.
\end{reviiib}
\end{revb}

% \begin{figure}[!t]

%   \begin{small}
%   % \begin{mathpar}
%   %   m ::= + \mid - \and
%   %   \negmode{+} = - \and
%   %   \negmode{-} = +\\
%   % \end{mathpar}

%   % \textbf{Weakly positive restriction} \hfill
%   % \boxed{\recvar \wpr \sty[1] \subty \sty[2]}\\
%   % \begin{mathpar}
%   %   \inferrule*[lab=\Trefr{wpr-arrow}]{
%   %     \recvar \wpr[\negmode{m}] \cty[21] \subty \cty[11] \\
%   %     \recvar \wpr \cty[12] \subty \cty[22]
%   %   }{
%   %     \recvar \wpr
%   %     \cty[11] \rightarrow \cty[12] \subty
%   %     \cty[21] \rightarrow \cty[22]
%   %   }

%   %   \inferrule*[lab=\Trefr{wpr-rec-eq}]{
%   %     \recvar \notin \freevars{\cty}
%   %   }{
%   %     \recvar \wpr
%   %     \recT[\recvarp] . \cty \subty
%   %     \recT[\recvarp] . \cty
%   %   }

%   %   \inferrule*[lab=\Trefr{wpr-rec-neq},width=12em]{
%   %     \recvar \neq \recvarp\\
%   %     \recvar \wpr \cty[1] \subty \cty[2] \\
%   %     \recvarp \wpr[+] \cty[1] \subty \cty[2]
%   %   }{
%   %     \recvar \wpr \recT[\recvarp] . \cty[1] \subty
%   %     \recT[\recvarp] . \cty[2]
%   %   }
%   % \end{mathpar}

%   \textbf{Subtyping} \hfill
%   \boxed{\sty \subty \sty}\\
%   \begin{mathpar}
%     \inferrule*[lab=\Trefr{sub-rec}]{
%       \cty[1] \subty \cty[2] \\
%       \recvar \wpr[+] \cty[1] \subty \cty[2]
%     }{
%       \recT . \cty[1] \subty
%       \recT . \cty[2]
%     }

%     \inferrule*[lab=\Trefr{sub-rec-refl}]{ }{
%       \recT . \cty \subty
%       \recT . \cty
%     }
%   \end{mathpar}
%   \end{small}

%   \caption{Recursive subtyping (excerpt)}
%   \label{fig:subtyping-recursive}
% \end{figure}

\subsection{Metatheory of \lambdaGSens}
\label{sec:gsoul-metatheory}

\begin{figure}[!t]

\begin{small}
\begin{align*}
% Related numbers
% (v_1, v_2) \in \glrV{\itype{\rtype}{\gsenv}} \iff
% & (v_1, v_2) \in \glrAtom{\itype{\rtype}{\gsenv}} \land \\
% & \neg \big( \denv \cdot (\gsenvp[1] \sjoin \gsenvp[2]) \cclt \lvert u_1 - u_2 \rvert \big) \\
% & \text{\textcolor{black}{where}}~ v_i = \evi{\itype{\rtype}{\emptysenv}, \itype{\rtype}{\gsenvp[i]}}\, u_i \ascr{\itype{\rtype}{\gsenv}}\\
% Related units
(v_1, v_2) \in \glrV{\itype{\unit}{\gsenv}} \iff
& (v_1, v_2) \in \glrAtom{\itype{\unit}{\gsenv}}\\
& \text{\textcolor{black}{where}}~ v_i = \ev[i] \ttunit \ascr{\itype{\unit}{\gsenv}}\\
% Related functions
(v_1, v_2) \in \glrV{\itype{(\cgty[1] \rightarrow \cgty[2])}{\gsenv}} \iff
& (v_1, v_2) \in \glrAtom{\itype{(\cgty[1] \rightarrow \cgty[2])}{\gsenv}} \land \\
& \big( \forall j \leq k, \svp[1], \svp[2], (v_1', v_2') \in \glrV{\cgty[1]}[j-1].\\
& ({\sv[1] \app \svp[1]}, {\sv[2] \app \svp[2]}) \in \glrT{\cgty[2] \effOp{+} \gsenv}[j] \big)\\
% Related type abstractions
(v_1, v_2) \in \glrV{\itype{(\polyS[\r].\cgty)}{\gsenv}} \iff
& (v_1, v_2) \in \glrAtom{\itype{(\polyS[\r].\cgty)}{\gsenv}} \land \big(\forall j \leq k, \gsenvpp. \\
& ({\sv[1] \appS{\gsenvpp}}, {\sv[2] \appS{\gsenvpp}}) \in \glrT{\Xisubst{\cgty}[\r]{\gsenvpp} \effOp{+} \gsenv}[j] \big)\\
% Related products
(v_1, v_2) \in \glrV{\itype{(\cgty[1] \madd \cgty[2])}{\gsenv}} \iff
& (v_1, v_2) \in \glrAtom{\itype{(\cgty[1] \madd \cgty[2])}{\gsenv}} \land \\
& ({\useFst(v_1)}, {\useFst(v_2)}) \in \glrT{\cgty[1] \effOp{+} \gsenv}[k] \land \\
& ({\useSnd(v_1)}, {\useSnd(v_2)}) \in \glrT{\cgty[2] \effOp{+} \gsenv}[k]\\
% Related sums
(v_1, v_2) \in \glrV{\itype{(\cgty[1] \msum \cgty[2])}{\gsenv}} \iff
& (v_1, v_2) \in \glrAtom{\itype{(\cgty[1] \msum \cgty[2])}{\gsenv}} \land \\
& \big( \denv \cdot (\gsenvp[1] \sjoin \gsenvp[2]) \cclt \infty
\\
& \implies
({\useL(\sv[1])}, {\useL(\sv[2])}) \in \glrT{\cgty[1] \effOp{+} \gsenv}[k] \lor \\
& \phantom{\implies (} ({\useR(\sv[1])}, {\useR(\sv[2])}) \in \glrT{\cgty[2] \effOp{+} \gsenv}[k]
\big)
\\
& \text{\textcolor{black}{where}}~ v_i = \evi{\itype{\gty[i1]}{\emptysenv}, \itype{\gty[i2]}{\gsenvp[i]}}\, u_i \ascr{\itype{(\cgty[1] \msum \cgty[2])}{\gsenv}}\\
% Related folds
(v_1, v_2) \in \glrV{\itype{(\mutpe{\cgty})}{\gsenv}} \iff
& (v_1, v_2) \in \glrAtom{\itype{(\mutpe{\cgty})}{\gsenv}} \land \big(\forall j \leq k,\\
&  ({\unfold{\sv[1]}}, {\unfold{\sv[2]}}) \in \glrT{\substv{\itype{(\mutpe{\cgty})}{\emptysenv}}{\alpha}{\cgty} \effOp{+} \gsenv}[j] \big)\\
% Related computations
({t_1}, {t_2}) \in \glrT{\cgty} \iff &
\forall j < k.
(\creds[]{t_1}{\sv[1]}[j] \land
\creds[]{t_2}{\sv[2]}) \implies
(v_1, v_2) \in \glrV{\cgty}[k-j]
% Related environments
% (\venv[1], \venv[2]) \in \glrG{\tenv} \iff
% & \dom(\venv[1]) = \dom(\venv[2]) = \dom(\Gamma) ~\land\\
% & \forall x \in \dom(\Gamma). (\venv[1](x),\venv[2](x)) \in \glrV{\Gamma(x)}
\end{align*}

\begin{mathpar}
\useL(\ev (\inl^{\cgty[12]} v) \ascr{\cgty}) = \ileft(\ev) v \ascr{\leftt(\cgty)} \and
\useR(\ev (\inr^{\cgty[12]} v) \ascr{\cgty}) = \iright(\ev) v \ascr{\rightt(\cgty)} \and
\useFst(\ev \pair{v_1}{v_2} \ascr{\cgty}) = \ifirst(\ev) v_1 \ascr{\fstt(\cgty)} \and
\useSnd(\ev \pair{v_1}{v_2} \ascr{\cgty}) = \isecond(\ev) v_2 \ascr{\sndd(\cgty)}
\end{mathpar}
\end{small}

\caption{Logical relations for gradual sensitivity soundness of \lambdaGSensEv (excerpt)}
\label{fig:gradual-logical-relation}
\end{figure}

\lambdaGSens satisfies all the properties of the core gradual language.
More notably, it also satisfies both termination-insensitive and -sensitive gradual metric preservation, as well as their respective corollaries.
One important difference between \GSoulCore and \lambdaGSens is that the latter supports general recursion.
This has a direct impact on the proof of sensitivity soundness for \lambdaGSens, because the logical relation presented in \secref{sec:gradual-metric-preservation} is not well-founded in presence of recursion.
To overcome this, we modify the definition of the logical relations to use \emph{step indexing}~\cite{ahmed:esop2006,appelMcAllester:toplas2001}.
We now discuss the step-indexed logical relation, presented in Figure~\ref{fig:gradual-logical-relation}.

\paragraph{(A) Related numbers, booleans and unit}
Numbers and booleans are related as defined in Figure~\ref{fig:basic-gradual-logical-relation}, independently of the step index.
Two values of the unit type are necessarily equal, and hence related for any step index.

\paragraph{(B) Related functions and resource abstractions}
The definitions remain similar to the ones in \secref{sec:gradual-metric-preservation}, but now they are indexed by a step index $k$.
Two functions are related at \typeclsSing $\itype{(\cgty[1] \to \cgty[2])}{\gsenv}$ {\em for $k$ steps} if, for any $j \leq k$, their applications to two related arguments for $j-1$ steps yield related computations for $j$ steps.
Similarly, two resource abstractions are related for $k$ steps if, for any $j \leq k$, their applications to any sensitivity environment yield related computations for $j$ steps.
Notice that for these cases, although the same step index can used in the recursive definition (when $j = k$), the interpretations are well-founded because in each case a reduction step is always performed, lowering the index by one.

\paragraph{(C) Related pairs and injections}
Two pairs are related simply if each of their components are related.
Any two injections are related for any step index if the predicted (worst-case) output distance $\denv \cdot (\gsenvp[1] \sjoin \gsenvp[2])$ is infinity.
If it is possible that the predicted output distance is less than infinity, then the injections must be either both left injections or right injections.
Furthermore, the underlying values must be related.
Also, and as in the case of booleans, in order to account for the worst case scenario, we need to take the best case on the hypothesis side of the implication as the predicate is in a contravariant position. Therefore, the consistently-less-than operator $\cclt$ is used directly, without the need for double negation.
Finally, the partial meta-functions $\useL$, $\useR$, $\useFst$, and $\useSnd$ are defined to extract the underlying values of the injections and pairs.

\paragraph{(D) Related folds}
Analogous to functions, two folds are related for $k$ steps if, for any $j \leq k$, their unfolding yield related computations at the expected \typeclsSing---as computed by $\unff$ in \Grefr{unfold}---for $j$ steps.

\paragraph{(E) Related computations}
A pair of closed terms are related for $k$ steps whenever the first term reduces to a value in $j$ steps (where $j < k$) and the second reduces to a value in any number of steps, and those two values are related at that type for $k-j$ steps.
Notice that this definition, similar to the first logical relation presented in \secref{sec:gradual-metric-preservation}, is termination-insensitive.
Later in this section, we will revisit the topic of termination-sensitive soundness for \lambdaGSensEv.

We can now state the fundamental property of the logical relation for \lambdaGSensEv, as well as gradual metric preservation for \lambdaGSens.

\begin{restatable}[Fundamental Property for \lambdaGSensEv]{theorem}{gradualMetricPreservation}
\label{prop:gsoul-gradual-metric-preservation}
\reviv{Let $t$ be a \lambdaGSensEv term.}
If $\ittyping{t}{\cgty}$ and $t \vdash \tenv$,
then $\forall \denv, k\geq0, \venv[1], \venv[2]$ such that $\tenv \vdash \denv$ and $(\venv[1], \venv[2]) \in \glrG{\tenv}$,
we have $(\venv[1](t), \venv[2](t)) \in \glrT{\cgty}$.
\end{restatable}

\begin{restatable}[Gradual metric preservation for \reviv{\lambdaGSens} base types]{corollary}{gradualMetricPreservationBaseTypes}
\label{prop:gsoul-gradual-metric-preservation-base-types}
\reviv{Let $f$ be a \lambdaGSens function.}
If $f$ has type $\teff{(\teff{\rtype}{\r} -> \teff{\rtype}{\gsens \r})}{\emptysenv}$, for some gradual sensitivity $\gsens$, then
for any real numbers $c_1, c_2, c$ such that $\abs{c_1 - c_2} \leq c$,
if $\reval{f \app c_1}{v_1}$, and
$\reval{f \app c_2}{v_2}$, then
$\abs{\uval{v_1} - \uval{v_2}} \leq c \cdot\pi_2(\gsens)$.
\end{restatable}

% \begin{figure}

%   \begin{small}
%     \begin{align*}
%       % Related atoms
%       (v_1, v_2) \in \tsglrAtom{\cgty} \iff
%       & \ittyping{\sv[1]}{\cgty} \land \ittyping{\sv[2]}{\cgty} \land {\getev(v_1) = \getev(v_2)}\\
%       % Related terms
%       (t_1, t_2) \in \tsglrT{\cgty}[k] \iff
%       &
%         \forall j < k.
%         \creds[]{t_1}{v_1}[j]
%         \implies ({\exists v_2 . \creds[]{t_2}{v_2}[*]} \land (v_1, v_2) \in \tsglrV{\cgty}[k - j])
%     \end{align*}
%   \end{small}

%   \caption{Termination-sensitive gradual metric preservation}
%   \label{fig:ts-gradual-logical-relation-step-index}
% \end{figure}

\paragraph{Revisiting termination-sensitive gradual metric preservation}
Recursive types not only introduce the need for step indexing in the logical relation, but also make program divergence a possibility.
This requires us to revisit what termination-sensitive gradual metric preservation means.
The attentive reader may have noticed that in \secref{sec:tsmp} we mostly discuss about \emph{different termination behavior across runs} and not specifically about error behavior.
Indeed, the changes made in that section are sufficient to also capture divergence as a possible source of different runs not having uniform termination behavior.
We thus refer to non-termination as both divergence and failure.

For stating termination-sensitive gradual metric preservation for \lambdaGSens we follow the same approach as in \secref{sec:tsmp}: first, we use a second logical relation that requires evidences of related values to be identical; and second, we disallow possibly-infinite distances in the fundamental property.
Again, the definitions for related values remain unchanged with respect to Figure~\ref{fig:gradual-logical-relation}, but the logical relations for terms have to be (trivially) updated to use step indexes.
We can now prove termination-sensitive gradual metric preservation for \lambdaGSens.

\begin{restatable}[(Termination-sensitive) Fundamental Property for \lambdaGSensEv]{theorem}{tsgradualMetricPreservation}
\label{prop:gsoul-ts-gradual-metric-preservation}
\reviv{
Let $t$ be a \lambdaGSensEv term.
If $\ittyping{t}{\itype{\gty}{\gsenv}}$, $t \vdash \tenv$ and $\neg (\infty \ccleq \denv \cdot \gsenv)$,
then $\forall \denv, k\geq0, \venv[1], \venv[2]$ such that $\tenv \vdash \denv$ and $(\venv[1], \venv[2]) \in \tsglrG{\tenv}$,
we have $(\venv[1](t), \venv[2](t)) \in \tsglrT{\itype{\gty}{\gsenv}}$.
\end{restatable}

\begin{restatable}[Termination-sensitive gradual metric preservation for base types]{corollary}{gradualMetricPreservationBaseTypesTS}
\label{prop:gsoul-gradual-metric-preservation-base-types-TS}
\reviv{Let $f$ be a \lambdaGSens function.}
If $f$ has type $\teff{(\teff{\rtype}{\r} -> \teff{\rtype}{\gsens \r})}{\emptysenv}$,
for some gradual sensitivity $\gsens$, then
for any real numbers $c_1, c_2, c$ such that $\abs{c_1 - c_2} \leq c$ and $c \cdot \pi_2(\gsens) < \infty$,
if $\reval{f \app c_1}{v_1}$ then
$\reval{f \app c_2}{v_2}$ and
$\abs{\uval{v_1} - \uval{v_2}} \leq c\cdot\pi_2(\gsens)$.
\end{restatable}

All the proofs for \GSoulCore and \GSoulEvCore are subsumed by the proofs for \lambdaGSens and \lambdaGSensEv, which can be found in the supplementary material.

% %!TEX root = ../main.tex
\section{Implementation}
\label{sec:implementation}

\lambdaGSens is implemented as a prototype written in Typescript. The toolchain can be found at \href{https://darquezt.github.io/gsoul-lang/}{https://darquezt.github.io/gsoul-lang/}.

The interpreter is not meant to be an efficient implementation, but to serve as a reference and provide a playground to run interesting programs, and test the benefits and limitations of gradual sensitivity typing.

The implementation is able to both typecheck and reduce a program.
Running a program consists of three main phases: parsing and desugaring source code, elaborating (while typechecking) to evidence-augmented terms, and reducing the program.
The implementation of the elaboration and typechecking follows Figure~\ref{fig:intrinsic-elaboration}.
Reduction is implemented as a CEK machine~\cite{felleisen:fdpc1986}, closely following the reduction rules for \lambdaGSensEv{}.
The abstraction and concretization functions are not used directly: all type predicates, functions, and operators are implemented using their equivalent algorithmic characterizations.

Besides the already presented features of \lambdaGSens, the implementation also supports let and (recursive) function declarations.
Low-level features of the language, such as big lambdas for resource polymorphism, are not intended to be used by end-users.
Instead, we use them for building ergonomic features, such as the \lstinline[language=gsoul]|res| modifier.
Programmers can declare resources using \lstinline[language=gsoul]|let res|, which besides binding a variable, it also creates a resource with the same name at types level.

\begin{small}
\begin{lstlisting}[language=gsoul,numbers=none]
let r = 1;          // normal variable; type: Number
let res b = false;  // resource variable; type: Boolean[b]
\end{lstlisting}
\end{small}

Alternatively to using the \lstinline|def _[r](...)| syntax, function parameters can be declared as polymorphic resources, using the \lstinline[language=gsoul]|res| modifier.

\begin{small}
\begin{lstlisting}[language=gsoul,numbers=none]
def double(res x: Number): Number[2x] = x + x;
\end{lstlisting}
\end{small}

Finally, we augment the language with a \lstinline|List|, \lstinline|Set|, and \lstinline|Map| types, and a few primitives for manipulating them, as well as algebraic datatypes (encoded using recursive types) and type polymorphism.\footnote{
Notice that lists can already be encoded using datatypes types (which can be encoded from recursive types). However, we introduce them as a primitive type for improving the ergonomics of the language.
We expect to further extend the language with more features, which hopefully will lead to interesting use cases and challenges for gradual sensitivity typing.
% The following program is the \lambdaGSens analogous to the one presented by \citet{reedAl:icfp2010} for \Fuzz, which computes the histogram of a list of numbers.

% \begin{small}
% \begin{lstlisting}[language=gsoul,numbers=none]
% def histAux(c: Number, res db: Set<Number>): List<Set<Number>[db]> {
%   if (c >= 101) List(db)
%   else {
%     let bin, next = db.split(fn (x: Number) => c >= x);
%     bin :: histAux(c + 10, next);
%   }
% }

% let hist = fn (res db: Set<Number>): List<Number[db]> => histAux(0, db).map(
%   fn (res bin: Set<Number>) => bin.size()
% );
% \end{lstlisting}
% \end{small}

%!TEX root = ../main.tex
\begin{comment}

\section{Discussion: Mutable references}

\et{I don't think this deserves a full section. I suggest to add a "conclusion and perspectives" section after related, and include a summary of this discussion in the perspectives}

\begin{revb}
Extending the language with mutable references is not straightforward, as it would break soundness. In particular, and analogously to dynamic information-flow security languages, the presence of mutable references faces the classic problem of \emph{implicit flows} through the heap~\cite{denning:cacm1976}. Let us consider an adaptation of the classic example of \citet{austinFlanagan:plas2009}, where the high security labels $\mathsf{H}$ and $\mathsf{L}$ are replaced by $\infty r$ and $r$ respectively.

\begin{lstlisting}[language=scala]
(*$\lambda$*)x: (*$\itype{\btype}{\infty r}$*).
let y: Ref (*$\itype{\btype}{?r}$*) = ref true in
let z: Ref (*$\itype{\rtype}{r}$*) = ref 1 in
if x then y := false else unit
if !y then z := 10 else unit
\end{lstlisting}
This function has type $\itype{(\itype{\btype}{\infty r} -> \itype{\rtype}{r})}{\emptysenv}$, which by type soundness, if $r$ have relational distance $1$ ($\denv(r) = 1$), and we instantiate the function with two different values at distance $\infty$, say $\ttt$ and $\fff$, then the difference of the results should not be bigger than $1$ ($\denv(r)*1$). Sadly, this is not the case as the resulting values are $1$ and $10$, breaking metric preservation. To address this problem, we may have to consider using a program counter, and perform ``non-sensitive-upgrades'', which would endanger the dynamic gradual guarantee~\cite{toroAl:toplas2018}.

Clearly, security types and sensitivity types are not exactly the same. In security typing, program $x_{\mathsf{L}} + x_{\mathsf{L}}$ has type $\rtype_{\mathsf{L}}$, i.e. the addition of two low security values produce a low security result. But in sensitivity typing, if $x$ has type $\itype{\rtype}{y}$, then program $x + x$ has type $\itype{\rtype}{2y}$, scaling the sensitivity of the result by two.
Although the analysis are different, there must be a connection as similar issues occur when mutable references are considered. This connection escapes the scope of this work and we leave it as future work.
\end{revb}

\end{comment}

\section{Related Work}
\label{sec:related}

\emph{Sensitivity and programming languages.}
The first type system for reasoning about sensitivity is \textsc{Fuzz}~\cite{reedAl:icfp2010}, a language for differential privacy using linear types.
Several variations have been studied, such as \textsc{DFuzz} \cite{gaboardiAl:popl2013}, \textsc{Fuzzi} \cite{zhangAl:icfp2019}, \textit{Adaptive Fuzz} \cite{winogradcortAl:icfp2017}.
All of these type systems measure sensitivity and also track and enforce differential privacy.
\citet{nearAl:oopsla2010} tackle differential privacy in \textsc{Duet} with two mutually-defined languages, one dedicated to sensitivity and one to privacy.
\textsc{Jazz} \cite{toroAl:toplas2023} follows the approach of \textsc{Duet}, and includes \textsc{Sax}, a sensitivity language with contextual linear types and delayed sensitivity effects. The starting point of \lang, the static language \lambdaSens{}, is very close to \textsc{Sax}.
Whereas \textsc{Fuzz}-like languages track the sensitivity of program variables using linear types, \citet{abuahAl:arxiv2021a} propose \textsc{Solo}, which tracks a fixed amount of sensitive resources and avoids linear types.
\textsc{DDuo}~\cite{abuahAl2021b} provides a library for sensitivity tracking in Python i.e. dynamically, being able to tackle expressiveness issues of static sensitivity type systems.
However, it does not provide the ability to strengthen the static guarantees of a program, as \lambdaGSens does.
$\color{black} \mu$\textsc{Fuzz} \cite{dantoniAl:fpdcsl2013} extends the \textsc{Fuzz} compiler to generate nonlinear constraints, which are then checked by an SMT solver, which results in an automatic type-based sensitivity analysis.
There is no prior work integrating static and dynamic sensitivity analysis within one language.

\begin{ppsalb}
Regarding termination sensitivity,
% \emph{Termination-(in)sensitive metric preservation.}
% For brevity, we refer to termination-sensitive and termination-insensitive metric preservation as \TSMP and \TIMP, respectively.
\Fuzz~\cite{reedAl:icfp2010} and more recent languages~\cite{gaboardiAl:popl2013,abuahAl:arxiv2021a}
focus on the terminating fragment of their languages.
% have presented \TSMP focusing its metatheory only on
\citet{reedAl:icfp2010} discuss the tension between metric preservation and non-termination in their seminal paper, presenting three alternatives:
weakening the definition of metric preservation;
proving statically that recursive functions terminate, yielding more complex programs;
or adding \emph{fuel} to recursive functions, falling back to a default value when running out of fuel. The latter is adopted in the implementation.
\muFuzz \cite{dantoniAl:fpdcsl2013} also supports recursive types, and termination-sensitive metric preservation is obtained by reasoning only about finite distances.
\textsc{Duet} \cite{nearAl:oopsla2010} avoids divergence via terminating looping primitives.
\DDuo~\cite{abuahAl2021b} establishes termination-insensitive metric preservation, although they do not explicitly discuss this aspect.
\end{ppsalb}

Before discussing related work in the gradual typing area, let us mention that another line of approaches for sensitivity verification is based on program logics~\cite{bartheAl:popl2012,bartheAl:tpls2013,bartheAl:lics2016,satoAl:lics2019}. These approaches are generally very expressive but less automatic than type systems. On the gradualization side, it seems possible to study gradualization of such program logics, for instance by following the gradual verification approach of
\citet{baderAl:vmcai2018}, further extended to a form of separation logic~\cite{wiseAl:oopsla2020}.
Extending gradual verification to account for the aforementioned logics for sensitivity would be an interesting venue for future work.

\emph{Gradual typing}
To the best of our knowledge, gradual typing has not been applied to sensitivity typing.
It has, however, been applied in languages with one of two particularly interesting properties: languages with type-and-effect disciplines; and languages whose soundness property corresponds to a hyperproperty, such as noninterference~\cite{goguenMeseguer:ieee1982} or parametricity~\cite{reynolds:83}.
\ppsal{Interestingly, gradual security typing has only been explored for termination- (and error-)insensitive characterizations of noninterference~\cite{toroAl:toplas2018,fennellThiemann:csf2013,deAmorim:lics2020}.}
\hide{As mentioned previously, }\citet{banadosAl:icfp2014,banadosAl:jfp2016} develop a general approach to gradualize type-and-effects. \citet{toroTanter:oopsla2015} extends this approach to be able to work in the context of polymorphic effects for the Scala language.
However, this line of work is based on the generic type-and-effect system of~\citet{marinoMillstein:tldi2009}, which cannot directly handle sensitivities as quantities within a range.

% The application of AGT to languages whose soundness is defined as a hyperproperty is challenging, as it has not always yielded sound languages, requiring ad-hoc changes.
% \citet{toroAl:toplas2018} discovered that the addition of mutable references in a security language yields a gradual language that does not satisfy noninterference; ad-hoc changes to address implicit flows recover noninterference, at the expense of the dynamic gradual guarantee.
% \citet{toroAl:popl2019} showed that parametricity is also in tension with the dynamic gradual guarantee when applying AGT to System~F. Here, the application of AGT to \lambdaSens{} produces a language that satisfies both the gradual guarantee and metric preservation.
\hide{Regarding AGT-derived languages, }\citet{toroAl:toplas2018} discovered that the addition of mutable references in a security language yields a gradual language that does not satisfy noninterference; ad-hoc changes to address implicit flows recover noninterference, at the expense of the dynamic gradual guarantee.
An interesting perspective is to study an extension of \lang{} with mutable references, investigating if metric preservation and the dynamic gradual guarantee are both satisfied.
% Considering that the issue for noninterference are implicit flows, which are not
% We conjecture that we would not have the same issues as with security types, where noninterference is endangered because of implicit flows, not present in sensitivity analysis.

\reviv{
Another interesting remark is the need for sensitivity intervals in order to have a sound evidence representation in \lambdaGSensEv.
\citet{banados:arxiv2020} study \emph{forward completeness} of evidence representation, which indeed enforces soundness in terms of expected modular type-based semantic invariants.
Proving forward completeness for \lambdaGSensEv{} is an interesting exercise for future work.

\emph{Quantitative reasoning.}
Finally, sensitivity analysis can be seen as one specific case of quantitative reasoning. Several related approaches have been explored
such as bounded linear logic~\cite{girardAl:tcs1992,dalLagoGaboardi:lics2011}, quantitative type theory~\cite{atkey:lics2018}, and graded modal types~\cite{orchardAl:icfp2019}. These approaches abstract over the specific quantity being analyzed and the underlying accounting mechanism. This work should serve as a useful guide to study if and how to gradualize such general approaches to quantitative program reasoning.

% \begin{itemize}
%   \item Fuzz and children (DFuzz, Fuzzi, Adaptive Fuzz): They use type systems for sensitivity analysis but also for privacy tracking and enforcement.
%   \item Duet sensitivity language: A dp language that, given its proposition of separating the sensitivity analysis and privacy enforcement, proposes the first sensitivity type system.
%   \item Sax: Follows the multi-language approach of Duet and adds contextual linear types for delayed sensitivity effects. \lambdaSens{} is majorly based in this one.
%   \item Solo: Removes complexity from the type system reasoning in order to be usable within languages not necessarily with linear types (like Haskell).
%   \item DDuo: In contrast with prior approaches, it performs sensitivity analyses dynamically.
%   \item $\color{black} \mu$Fuzz: Is the first sensitivity-first approach. It extends from Fuzz and uses an SMT solver to perform an static sensitivity analysis.
% \end{itemize}

% None of the approach mentioned have explored the mix of dynamic and static sensitivity analysis.

% \subsection{Gradual Typing}

% \begin{itemize}
%   \item Gradual typing has never been applied to sensitivity typing.
%   \item gradual session types? gradual type and effects: Their effects do not encode variable dependant environments, but a fixed amount of multiplicities. Also, they gradualize the types, not the effects.
%   \item gradual typing and hyper-properties: The application of AGT to languages whose soundness is defined as a hyper-property is interesting, as it has not always yielded sound languages, and ad-hoc changes have had to be done. \cite{toroAl:toplas2018} discovered that the addition of mutable references in a security language caused AGT yielding a language that does not satisfy non-interference, and the dynamic gradual guarantee has to be thrown in favor of recovering soundness, using ad-hoc changes. \cite{toroAl:popl2019} actually proved that parametricity is not compatible with the dynamic gradual guarantee, and thus one must be chosen. In contrast, in our work, the application of AGT to \lambdaSens{} produced a language that satisfies both the gradual guarantee and metric preservation, without the need for changes in the semantics.
% \end{itemize}

% \begin{enumerate}
%   \item Sensitivity analyses: Chaudhuri et al \cite{chaudhuriAl:popl2010,chaudhuriAl:fse2011} (Robustness of programs), Palamidessi and Stronatti \cite{palamidessiStronatti:qapl2012} (Constraint-based sensitivity of relational algebra queries).
%   \item Sensitivity type systems: Duet's sensitivity language, Sax, $\color{black} \mu$Fuzz (Fuzz + SMT)
%   % \item Privacy static languages: Fuzz, DFUzz, Duet, Jazz, Solo/Duo
%   % \item Dinamic enforcement of privacy: Solo/Duo
%   \item Gradual typing
%   \begin{itemize}
%     \item gradual session types? gradual type and effects
%   \end{itemize}
% \end{enumerate}

%!TEX root = ../main.tex
\section{Conclusion}
\label{sec:conclusion}
\begin{revb}
We present \lambdaGSens, a gradual sensitivity calculus with support for recursive types and explicit sensitivity polymorphism, featuring both unbounded and bounded sensitivity imprecision.
Gradual sensitivity typing not only allows programmers to seamlessly choose between static and dynamic checking as they see fit, it can also accommodate features, such as recursive functions, that are too conservatively handled by the static discipline.
% ---a point we illustrate with the essential feature of recursive functions, which non-dependent static sensitivity type systems can only soundly approximate with infinite sensitivity.

% \lambdaGSens is derived from \lambdaSens, a statically-typed sensitivity language, which features a novel design for explicit sensitivity polymorphism, providing fine-grained control in sensitive resource usage specifications. We derive \lambdaGSens and its runtime semantics, \lambdaGSensEv, step-by-step using the AGT methodology, emphasizing steps where a naive design would have led to an unsound type system.
% Finally, we formally prove that \lambdaGSens is type safe and satisfies the gradual guarantee as well as sensitivity type soundness, \ie metric preservation.
% In particular, we present the challenges of designing a gradual interpretation of metric preservation, highlighting how a naive lifting of its static counterpart would yield an incorrect specification.
\reviv{
% We proved not only that \lambdaGSens is type safe and satisfies the gradual guarantee, but also that it satisfies sensitivity type soundness, i.e. metric preservation.
We have presented the challenges of designing a gradual interpretation of metric preservation, highlighting how a naive lifting of its static counterpart would yield an incorrect specification.
Furthermore, we have explored the termination aspect of metric preservation in the presence of possible runtime errors and divergence.}

A challenging venue of future work is the addition of support for mutable references.
However, akin to gradual security typing \cite{toroAl:toplas2018}, adding this feature would likely yield a language that does not satisfy metric preservation by default, and fixing it could endanger the dynamic gradual guarantee.
% Indeed, one could construct a counter-example for sensitivity soundness in a similar fashion as \citet{toroAl:toplas2018} do for non-interference, by viewing the two security levels $L$ and $H$ as the effects $\SG{1x}$ and $\SG{\infty x}$.
% It would be informative to explore in details the connection between information flow typing and sensitivity typing, in particular in the gradual setting.
% We believe there is a connection between these two kinds of analyses but we leave this question as future work.
Another possible line of future work involves the extension and application of the principles used in this work to \ppsal{other typing disciplines that rely on function sensitivity, such as differential privacy~\cite{dworkRoth:fttcs2014}, as well as} other quantitative type-based reasoning techniques~\cite{atkey:lics2018,orchardAl:icfp2019,petricekAl:icfp2014}.
\end{revb}

% \begin{acks}
% We thank ...
% \end{acks}

% \bibliographystyle{plainnat}
\bibliography{../_Bib/strings,../_Bib/pleiad,../_Bib/bib,references,../_Bib/common}

% \break

% \renewcommand*{\appendixname}{Appendices}

% \appendix

% \vspace*{\fill}
% \begin{center}
%   {\bf\LARGE\appendixname}
% \end{center}
% \vspace*{\fill}

% % \include{supplementary/sections/introduction}
% % \include{supplementary/sections/minisax}
% \include{supplementary/sections/static}
% % \include{supplementary/sections/gradual_sens}
% \include{supplementary/sections/gradual}
% \include{supplementary/sections/preamble}
% \include{supplementary/sections/galois}
% \include{supplementary/sections/type_safety}
% \include{supplementary/sections/gradual_guarantee}
% \include{supplementary/sections/soundness}
% \include{supplementary/sections/ts_soundness}

\end{document}


# Some speculations about local thermalization of nonequilibrium extended
quantum systems

M. Coppola  $|$ , D. Karevski  $|$<EMAIL_ADDRESS>It is with
great pleasure that I wish to contribute to this special edition in honor of
my dear friend Bertrand Berche, with whom I have been traveling around the
world, visiting Ukraine many times and maintained a friendship for thirty
years now. May this friendship last forever. I also want to dedicate this
paper to the memory of our mentor Loïc Turban who supervised our phds and who
guided us during all these years.

(Received November 14, 2022, in final form December 6, 2022)

###### Abstract

We discuss the possibility of defining an emergent local temperature in
extended quantum many-body systems evolving out of equilibrium. For the most
simple case of free-fermionic systems, we give an explicit formula for the
effective temperature in the case of, not necessarily unitary, Gaussian
preserving dynamics. In this framework, we consider the hopping fermions on a
one-dimensional lattice submitted to randomly distributed projective
measurements of the local occupation numbers. We show from the average over
many quantum trajectories that the effective temperature relaxes exponentially
towards infinity.

Key words: quantum statistical mechanics, nonequilibrium statistical
mechanics, open quantum systems

###### Abstract

Îáãîâîðþòüñÿ ìîæëèâñòü âèçíàåííÿ ëîêàëüíî¿ òåìïåðàòóðè ó ïðîñòîðîâèõ êâàíòîâèõ
ñèñòåìàõ áàãàòüîõ àñòèíîê, ÿê çíàõîäÿòüñÿ äàëåêî âä ñòàíó ðâíîâàãè. Äëÿ
íàéïðîñòøî¿ ìîäåëüíî¿ ñèñòåìè âëüíèõ ôåðìîíâ îòðèìàíî ÿâíèé âèðàç äëÿ
åôåêòèâíî¿ òåìïåðàòóðè ó âèïàäêó, êîëè ãàóñîâ äèíàìí ñòàíè ñèñòåìè íå çàâæäè
çàäîâîëüíÿþòü óìîâó óíòàðíîñò. Ó öüîìó íàáëèæåíí ìè ðîçãëÿäàìî ïåðåñêîêîâ
ìåõàíçìè ìãðàö¿ ôåðìîíâ íà îäíîâèìðíé ðàòö ïä âïëèâîì âèïàäêîâèõ ïðîåêòèâíèõ
âèìðþâàíü ëîêàëüíèõ èñåë çàïîâíåííÿ. Íà îñíîâ óñåðåäíåííÿ çà áàãàòüìà
êâàíòîâèìè òðàêòîðÿìè ïîêàçàíî, ùî åôåêòèâíà òåìïåðàòóðà åêñïîíåíöéíî ïðÿìó äî
áåçìåæíîñò.

Ключов слова: êâàíòîâà ñòàòèñòèêà, íåðâíîâàæíà ñòàòèñòèíà ìåõàíêà, âäêðèò
êâàíòîâ ñèñòåìè

##  1 Introduction

In the last decade, there has been a tremendous interest in the study of the
out of equilibrium properties of simple many-body systems in both unitary and
non-unitary cases. In the unitary settings, the out of equilibrium dynamics is
generated by the more or less sudden quench of some global [1, 2] or local [3,
4] Hamiltonian parameter, after which the system is left to evolve unitarily
in time. The quench may be also homogeneous or inhomogeneous, varying the
local couplings at different rates [5, 6, 7, 8]. In this scenario, one
important way of catching the non-equilibrium properties of the system is by
considering the dynamical evolution of the entanglement spreading all over the
system [9, 10]. For local short-range Hamiltonians, starting from a
disentangled initial state, it has been shown that the spreading of the
quantum correlations is a ballistic process governed by the existence of a
Lieb-Robinson bound [11]. From each points of the system, after the quench,
correlation fronts propagate at a maximum velocity, the Lieb-Robinson bound,
and give rise to local light-cones effects. For integrable one-dimensional
systems, with infinite-life time quasi-particle excitations propagating
ballistically, the entanglement spreading is linear in time, as it can be
easily understood from a simple quasi-particle picture [1, 12]. At later
times, the system relaxes locally to a generalized Gibbs state which, in
general, is defined by the knowledge of an infinite set of conserved
quantities, reflecting an extensive scaling of the entanglement entropy [13,
14, 15, 16]. However, many factors may alter the unitarity of the evolution:
in real life, the system is never perfectly isolated and it can also be
monitored non-unitarily as it is the case when projective measurements are
performed [17]. Under such a monitoring, the dynamics may be drastically
modified, leading for example to the possibility of suppressing completely the
spreading of the entanglement [18, 19, 20, 21]. The non-unitary dynamics in
many situations can be described by a Markovian dynamical map, leading to a
Lindblad time evolution equation for the density matrix of the system [22,
23], instead of the unitary Liouville equation. The opening of the quantum
system may also be global, where dissipative channels are connected to the
whole system, or may be local, where some regions of the system only are
governed by a dissipative map while the remaining part is governed by a
Hamiltonian dynamics. One such a local situation is when a finite chain is
coupled at its ends to different baths (or reservoirs of particles),
generating at large enough times a non-equilibrium steady state (NESS) [24,
25, 26, 27, 28, 29, 30, 31]. The local quantum NESS generated this way is a
stationary current full quantum state which is given by a generalized
MacLennan-Zubarev state [33, 32], which can also be called a generalized Gibbs
state, $\rho(x)\sim\mathrm{e}^{-\beta H(x)-\delta J(x)}$, where
$\beta=({\beta_{L}+\beta_{R}})/{2}$ is the average inverse temperature of the
two baths coupled to the local Hamiltonian $H(x)$ and
$\delta=\beta_{L}-\beta_{R}$ is the drift parameter coupled to a local current
operator $J(x)$ [24]. The melting of an initial domain wall may also be
described in this way since it represents locally the same physical setup [34,
35, 36, 39, 37, 38, 40, 41, 42, 43, 44, 45, 46].

In this paper we reconsider the situation of a one-dimensional quantum system
evolving according to a dynamical map which may or may not be unitary and wish
to assign to it, in the most simple possible way, a local temperature. This
attempt has been considered in the equilibrium case, where the local
temperature of a quantum system, if not properly defined, may not be a well
defined quantity in the sense that it may not be anymore an intensive quantity
and differs from the whole system temperature [47, 48, 49, 50, 51, 52, 53,
54]. Let us mention that several attempts to define the effective temperatures
appeared quite recently in the context of the system-plus-reservoir paradigm
in the strong coupling limit [55], by the introduction of a virtual
temperature in the context of quantum machines [56], or based on the analyses
of the heat flow in open quantum systems [57, 58].

In the next section we define the model and its dynamics. Section 3 is devoted
to the question of local effective temperatures. We end the paper by some
discussion in section 4.

##  2 Out of equilibrium dynamics of an extended quantum system

###  2.1 Local state

####  2.1.1 Hydrodynamical description

We consider one-dimensional free-fermionic systems defined on an infinite one-
dimensional lattice with lattice spacing $a$. The system may also be submitted
to an external potential $V(x)$ which is assumed to be a real smooth function.
To describe the local properties of the system, we split the one-dimensional
lattice into regular intervals $[x,x+a\ell[$, each containing a large number
$\ell$ of lattice sites, while keeping the width $a\ell$ of the cell small
enough such that for whatever sites $j\in[x,x+a\ell[$ the value of the
potential is constant in that interval: $V_{j}\simeq V(x)$. The Hilbert space
of the system is thus decomposed as a product of identical finite-dimensional
local Hilbert spaces $\mathfrak{H}_{x}$ located at position $x$. The
Hamiltonian $H=\int\mathrm{d}xH(x)$ of the full system is thus a sum over the
real line of the Hamiltonian density $H(x)$ which in the hydrodynamic limit,
for example for spinless fermionic tight binding models, is given by [59, 60,
61, 62, 63]

$H(x)=\frac{1}{a\ell}\int_{a\ell}\mathrm{d}y\;\left\\{\kappa(x)\left(\psi_{x}^{\dagger}(y)\psi_{x}(y+a)+\psi_{x}^{\dagger}(y+a)\psi_{x}(y)\right)+V(x)\psi_{x}^{\dagger}(y)\psi_{x}(y)\right\\},$
(2.1)

where $\kappa(x)$ is the local hopping constant and the $\psi_{x}$ and
$\psi_{x}^{\dagger}$ are Fermi fields defined in the hydrodynamical cell $x$.
Within each coarse-grained point $x$, the system can be diagonalized by a
Fourier-Bogoliubov transformation. Obviously, in order to make this continuum
limit practicable, the local scale $\ell$ should be much larger than the
inverse particle density: $\ell\gg 1/\rho$. In any case, one can always go
back to the discret nature of the system and use the discret splitting
$H=\sum_{x}H(x)$, where $H(x)$ is the local Hamiltonian defined on the lattice
sites $j\in[x,x+a\ell[$

$H(x)=c^{\dagger}(x)T(x,0)c(x)=\sum_{i,j\in
x}c^{\dagger}_{i}(x)T_{ij}(x,0)c_{j}(x).$ (2.2)

The $c^{\dagger}_{i}(x),c_{i}(x)$ are local creation and annihilation
operators satisfying the usual canonical rules

$\\{c^{\dagger}_{i}(x),c_{j}(x^{\prime})\\}=\delta_{ij}\delta_{xx^{\prime}},$
(2.3)

and $T(x,0)$ is the local one-particle Hamiltonian ($\ell\times\ell$ Hermitian
coupling matrix).

If the hydrodynamical description is valid, the lattice variables
$c^{\dagger}_{i}(x),c_{i}(x)$ may be replaced by the continuous creation and
annihilation fields $\psi^{\dagger}_{x}(y)$ and $\psi_{x}(y)$ acting at
position $y$ within the coarse-grained cell $x$, such that

$H(x)=\psi^{\dagger}_{x}T(x,0)\psi_{x}=\int_{\Delta x}\mathrm{d}y\int_{\Delta
x}\mathrm{d}y^{\prime}\;\psi^{\dagger}_{x}(y)T_{x}(y,y^{\prime})\psi_{x}(y^{\prime}),$
(2.4)

where $T_{x}(y,y^{\prime})$ is the kernel function associated to the $T(x,0)$.

####  2.1.2 Time evolution of the local state

The local initial state at position $x$ is deduced from the initial global
state $\rho(0)$ by tracing out the degrees of freedom living in the
complementary space $\mathfrak{H}_{/x}$ of the local Hilbert space
$\mathfrak{H}_{x}$:

$\rho(x,0)=\mathrm{\,tr}_{\mathfrak{H}_{/x}}\\{\rho(0)\\}\,.$ (2.5)

Up to boundary corrections, we assume that this local state is initially given
by a local canonical state111For a general argument why the canonical states
are ubiquitous states see [64, 65].

$\rho(x,0)=\omega\left(H(x),\beta(x)\right)\equiv\frac{\mathrm{e}^{-\beta(x)H(x)}}{{Z}[H(x),\beta(x)]}\,,$
(2.6)

where $H(x)$ is the local Hamiltonian (2.2) and
${Z}(H,\lambda)=\mathrm{\,tr}_{\mathfrak{H}_{x}}\\{\mathrm{e}^{-\lambda
H(x)})\\}$ is the local partition function.

At a later time $t$, the system evolves according to a dynamical map
$\Lambda_{t}$ such that

$\rho(t)=\Lambda_{t}[\rho(0)],$ (2.7)

from which the local state is obtained by taking the partial trace

$\rho(x,t)=\mathrm{\,tr}_{\mathfrak{H}_{/x}}\\{\rho(t)\\}=\mathrm{\,tr}_{\mathfrak{H}_{/x}}\\{\Lambda_{t}[\rho(0)]\\}\;.$
(2.8)

If the global dynamical map $\Lambda_{t}$ is unitary, then

$\rho(t)=\Lambda_{t}[\rho(0)]=U(t,0)\rho(0)U^{\dagger}(t,0),$ (2.9)

where $U(t,0)$ is the unitary time evolution operator defined on the global
Hilbert space $\mathfrak{H}$. In such a case, the local state is given by

$\rho(x,t)=\mathrm{\,tr}_{\mathfrak{H}_{/x}}\left\\{U(t,0)\rho(0)U^{\dagger}(t,0)\right\\}.$
(2.10)

In general, the system is not perfectly isolated and/or subject to an external
monitoring, such as discret or continuous driving of some parameter,
measurements of some local properties, and this in general breaks the
unitarity of the dynamical map $\Lambda_{t}$ [21].

However, even for a perfectly isolated system, with a global unitary dynamics,
the time evolution of the reduced density matrix, that is the local state
$\rho(x,t)$, is not in general a unitary evolution [22, 23]. Indeed, if we
assume for simplicity that the initial global state $\rho(0)$ is a tensor
product state of the $x$-cell state times, the state $\omega_{e}$ of the
remaining part, that is $\rho(0)=\rho(x,0)\otimes\omega_{e}(0)$, then the
local state at a later time is given by

$\rho(x,t)=\mathrm{\,tr}_{\mathfrak{H}_{/x}}\left\\{U(t,0)\rho(x,0)\otimes\omega_{e}(0)U^{\dagger}(t,0)\right\\}.$
(2.11)

Now, introduce the spectral decomposition of the environement state
$\omega_{e}(0)=\sum_{k}\lambda_{k}\pi_{k}$, where
$\\{\pi_{k}=|f_{k}\rangle\langle f_{k}|\\}$ is a complete family of orthogonal
projectors in the Hilbert space $\mathfrak{H}_{/x}$, and the tensor
decomposition of the unitary evolution operator

$U(t,0)=\sum_{ij}W^{ij}(t)\otimes M^{ij},$ (2.12)

where $M^{ij}=|f_{i}\rangle\langle f_{j}|$ is defined on the environement and
$W^{ij}(t)$ is a matrix defined on $\mathfrak{H}_{x}$ which can be decomposed
on an orthonormal basis $\\{|\varphi_{k}\rangle\\}$ of the local space
$\mathfrak{H}_{x}$ as $W^{ij}(t)=\sum_{kl}(W^{ij}(t))_{kl}L^{kl}$ with
$L^{kl}=|\varphi_{k}\rangle\langle\varphi_{l}|$. Plugging that into the time-
evolved reduced density matrix one obtains

$\rho(x,t)=\sum_{k}\lambda_{k}\sum_{i}W^{ik}(t)\rho(x,0){W^{ik}}^{\dagger}(t)\;.$
(2.13)

Since the $\lambda_{k}$ are the eigenvalues of the environment density
operator, they are all positive and one can redefine the Kraus operators as
$K^{ij}=\sqrt{\lambda_{j}}W^{ij}$ such that the reduced dynamical map is given
by

$\rho(x,t)=\Lambda_{(x,t)}[\rho(x,0)]=\sum_{\alpha}K^{\alpha}(t)\rho(x,0){K^{\alpha}}^{\dagger}(t),$
(2.14)

with the trace preserving condition

$\sum_{\alpha}{K^{\alpha}}^{\dagger}(t)K^{\alpha}(t)={\mathbbm{1}}_{\mathfrak{H}_{x}}.$
(2.15)

When there is only one Kraus operator left, the local dynamics is unitary too.

If the local dynamical map $\Lambda_{(x,t)}$ satisfies the Markovian semi-
group property

$\Lambda_{(x,t)}\Lambda_{(x,s)}=\Lambda_{(x,t+s)},$ (2.16)

then

$\rho(x,t)=\Lambda_{(x,t)}\rho(x,0)=\Lambda_{(x,\epsilon)}\Lambda_{(x,t-\epsilon)}\rho(x,0)=\Lambda_{(x,\epsilon)}\rho(x,t-\epsilon),$
(2.17)

from which one deduces that there is an infinitesimal generator ${\cal
L}_{x}$, such that the infinitesimal dynamical map
$\Lambda_{(x,\epsilon)}={\mathbbm{1}}+\epsilon{\cal L}_{x}$, whose exponential
gives the finite dynamics:

$\Lambda_{(x,t)}=\lim_{n\rightarrow\infty}\left({\mathbbm{1}}+\frac{t}{n}{\cal
L}_{x}\right)^{n}=\mathrm{e}^{t{{\cal L}_{x}}}.$ (2.18)

Taking the time derivative of $\rho(x,t)=\mathrm{e}^{t{{\cal
L}_{x}}}\rho(x,0)$ one has the differential equation

$\partial_{t}\rho(x,t)={\cal L}_{x}\rho(x,t),$ (2.19)

which can be written in the Lindblad form

$\partial_{t}\rho(x,t)=-\mathrm{i}[H(x),\rho(x,t)]+\sum_{k}L_{k}(x)\rho(x,t)L_{k}^{\dagger}(x)-\frac{1}{2}\left\\{L_{k}^{\dagger}(x)L_{k}(x),\rho(x,t)\right\\},$
(2.20)

where $H(x)$ and the so-called jump operators $\\{L_{k}(x)\\}$ acting on the
local Hilbert space $\mathfrak{H}_{x}$ are defined in terms of the
infinitesimal Kraus operators $\\{K^{\alpha}(\epsilon)\\}$ under a proper
scaling limit [22, 23] and with $\\{A,B\\}\equiv AB+BA$ the anticommutator of
$A$ and $B$.

Solving the Lindblad equation for a many-body system is in general a very
difficult task, even if a few exact results do exist for non-interacting
particles [24, 67] and for some Bethe-integrable systems [27, 28, 29, 68].

###  2.2 Gaussian preserving dynamics

In this context, we consider a special class of dynamical maps that preserves
the Gaussianity of the local state. Gaussian states $\rho(x)$ are states for
which Wick theorem applies and they are fully characterized by the correlation
matrix (two-point functions)

$C_{ij}(x)=\langle
c^{\dagger}_{i}c_{j}\rangle_{\rho(x)}=\mathrm{\,tr}_{\mathfrak{H}_{x}}\left\\{c^{\dagger}_{i}c_{j}\rho(x)\right\\}\;.$
(2.21)

If the initial state $\rho(x,0)$ is Gaussian, then the unitarily evolved state
$\rho(x,t)=\mathrm{e}^{\textrm{i}tH(x)}\rho(x,0)\mathrm{e}^{-\textrm{i}tH(x)}$
remains Gaussian and is fully characterized by
$C_{ij}(x,t)=\mathrm{\,tr}_{\mathfrak{H}_{x}}\\{c^{\dagger}_{i}c_{j}\rho(x,t)\\}$.

However, Gaussian Preserving Dynamics (GPD) are more general and can be
implemented by other schemes. One of them is by a continuous monitoring of the
system under projective measurements of some local densities [21], which
obviously destroys, in general, the unitarity of the dynamics. To be more
specific, consider a local observable $Q_{\Omega}$, defined on some compact
support $\Omega\subset\mathbb{Z}$,

$Q_{\Omega}=\sum_{p}q_{p}P^{(p)}_{\Omega},\quad\sum_{p}P^{(p)}_{\Omega}={\mathbbm{1}}_{\Omega},$
(2.22)

where the $P^{(p)}_{j}$ are the orthogonal projectors on the corresponding
subspace associated to the eigenvalue $q_{p}$ of the observable $Q_{\Omega}$.
Starting, for example, with a pure state $|\Psi\rangle$, just after the
measurement of the local observable $Q_{\Omega}$ with an outcome $q_{k}$, the
state is projected according to the Born rule

$|\Psi\rangle\longrightarrow\frac{P^{k}_{\Omega}|\Psi\rangle}{\langle\Psi|P^{k}_{\Omega}|\Psi\rangle}\;.$
(2.23)

In general, projective measurements will not preserve the Gaussianity of the
state. However, if one considers the measurements of the local density
$\hat{n}_{j}=c^{\dagger}_{j}c_{j}$, with the two possible outcomes $q_{0}=0$
and $q_{1}=1$, then the dynamics remains GPD. Indeed, the local density
operator can be represented by $\hat{n}_{j}=q_{1}P_{j}^{(1)}+q_{0}P_{j}^{(0)}$
with $P_{j}^{(1)}+P_{j}^{(0)}={\mathbbm{1}}_{j}$ which implies that all local
number operators are projectors:

$\hat{n}_{j}=P_{j}^{(1)}\;,\quad{\mathbbm{1}}_{j}-\hat{n}_{j}=P_{j}^{(0)}.$
(2.24)

Using the operator identity

$\mathrm{e}^{\nu\hat{n}_{j}}={\mathbbm{1}}_{j}+(\mathrm{e}^{\nu}-1)\hat{n}_{j}\,,$
(2.25)

we see that the projectors $P_{j}^{(0)}={\mathbbm{1}}_{j}-\hat{n}_{j}$ and
$P_{j}^{(1)}=\hat{n}_{j}$ can be expressed as limits of Gaussian operators:

${\mathbbm{1}}_{j}-\hat{n}_{j}=\lim_{\nu\rightarrow\infty}\mathrm{e}^{-\nu\hat{n}_{j}},\quad\hat{n}_{j}=\lim_{\nu\rightarrow\infty}\frac{\mathrm{e}^{\nu\hat{n}_{j}}}{\mathrm{e}^{\nu}-1}.$
(2.26)

Since by hypothesis the initial state is Gaussian,
$\rho\propto\mathrm{e}^{\sum_{ij}c^{\dagger}_{i}M_{ij}c_{j}}$, from the
projection rules associated to either ${\mathbbm{1}}_{j}-\hat{n}_{j}$ or
$\hat{n}_{j}$ one has to consider the expression

$\mathrm{e}^{\pm\nu\hat{n}_{j}}\mathrm{e}^{\sum_{kl}c^{\dagger}_{k}M_{kl}c_{l}}\mathrm{e}^{\pm\nu\hat{n}_{j}},$
(2.27)

which, from Baker-Campbell-Hausdorff formula, is nothing else but a Gaussian
state

$e^{\sum_{kl}c^{\dagger}_{k}K_{kl}c_{l}},$ (2.28)

associated to some new coupling matrix $K$. Notice that since a Gaussian state
is fully characterized by its correlation matrix $C_{ij}$, the projection
rules can be translated into the following rules for the two-point functions:
If the outcome of the measurement of the local density at site $k$ is $1$,
which occurs with probability $p_{k}=C_{kk}(x,t)=\langle\hat{n}_{k}\rangle$,
then

$C_{ij}(x,t)\longrightarrow\delta_{ik}\delta_{jk}+C_{ij}(x,t)-\frac{C_{ik}(x,t)C_{kj}(x,t)}{C_{kk}(x,t)}$
(2.29)

and otherwise

$C_{ij}(x,t)\longrightarrow-\delta_{ik}\delta_{jk}+C_{ij}(x,t)+\frac{[\delta_{ik}-C_{ik}(x,t)][\delta_{jk}-C_{kj}(x,t)]}{1-C_{kk}(x,t)}\;.$
(2.30)

Indeed, when the outcome of the measurement of the density at site $k$ is 1,
the projection rule transforms the two-point function
$C_{ij}=\mathrm{\,tr}\\{c_{i}^{\dagger}c_{j}\rho\\}$ into
$\mathrm{\,tr}\\{c_{i}^{\dagger}c_{j}\hat{n}_{k}\rho\hat{n}_{k}\\}=\mathrm{\,tr}\\{\hat{n}_{k}c_{i}^{\dagger}c_{j}\hat{n}_{k}\rho\\}=\langle
c^{\dagger}_{k}c_{k}c_{i}^{\dagger}c_{j}c^{\dagger}_{k}c_{k}\rangle$. After
normal ordering this six-point function, one obtains
$\delta_{ik}\delta_{jk}\langle c^{\dagger}_{k}c_{k}\rangle+\langle
c^{\dagger}_{k}c^{\dagger}_{i}c_{j}c_{k}\rangle$ and the last term is reduced
to $\langle c^{\dagger}_{k}c_{k}\rangle\langle
c^{\dagger}_{i}c_{j}\rangle-\langle c^{\dagger}_{k}c_{j}\rangle\langle
c^{\dagger}_{i}c_{k}\rangle$ thanks to Wick theorem. After dividing
$\mathrm{\,tr}\\{c_{i}^{\dagger}c_{j}\hat{n}_{k}\rho\hat{n}_{k}\\}$ by the
proper normalization factor
$\mathrm{\,tr}\\{\hat{n}_{k}\rho\hat{n}_{k}\\}=\mathrm{\,tr}\\{\hat{n}_{k}\rho\\}=C_{kk}$,
one obtains the projection rule (2.29). Following the same logic one obtains
the rule (2.30).

Whenever no measurement occurs, the time evolution is unitary and GPD such
that the correlation matrix $C$ evolves according to
$C(t+\tau)=R^{\dagger}(\tau)C(t)R(\tau)$, where $R(\tau)$ is a unitary matrix.
Consequently, the combination of the unitary evolution and these projection
rules leads to a quantum trajectory of the system which is governed by a non-
unitary GPD [21].

##  3 Local effective temperature

###  3.1 Evolution of the coupling matrix

Consider now a system initially prepared in a state such that the local
density operator is a Gibbs state (2.6) at some local inverse temperature
$\beta(x)$. We assume that at a later time the new local state generated by
the local (non-unitary) dynamical map $\Lambda_{(x,t)}$ remains gaussian:

$\rho(x,t)=\frac{1}{Z[H(x,t),\beta(x)]}\mathrm{e}^{-\beta(x)c^{\dagger}(x)T(x,t)c(x)},$
(3.1)

where the normalization factor
$Z[H(x,t),\beta(x)]=\mathrm{\,tr}_{\mathfrak{H}_{x}}\left\\{\mathrm{e}^{-\beta(x)c^{\dagger}(x)T(x,t)c(x)}\right\\}$
and with the new one particle matrix

$T(x,t)=\lambda_{(x,t)}[T(x,0)]$ (3.2)

evolved non-unitarily from the initial one particle Hamiltonian matrix
$T(x,0)$ with a dynamical map $\lambda_{(x,t)}$. One can relate the dynamical
evolution of the coupling matrix $T(x,t)$ to the dynamical evolution of the
correlation matrix $C(x,t)$ due to the relation

$C^{\text{tr}}(x,t)=\frac{1}{{\mathbbm{1}}_{x}+\mathrm{e}^{\beta(x)T(x,t)}}\quad\Leftrightarrow\quad-\beta(x)T(x,t)=\ln\frac{C^{\text{tr}}(x,t)}{{\mathbbm{1}}_{x}-C^{\text{tr}}(x,t)},$
(3.3)

where the upper script tr stands for the transposed matrix and
${\mathbbm{1}}_{x}$ is the $\ell\times\ell$ identity matrix defined on the $x$
cell.

Even if the quadratic form

$H(x,t)\equiv c^{\dagger}(x)T(x,t)c(x)$ (3.4)

entering the local state $\rho(x,t)$ may be interpreted as a new Hamiltonian,
one is not legitimate to interpret $\rho(x,t)$ as a Gibbs state since $H(x,t)$
is not the true local system Hamiltonian $H(x)$.

Let $W_{t}(x)$ be the unitary matrix diagonalizing the coupling matrix
$T(x,t)$:

$W_{t}^{\dagger}(x)T(x,t)W_{t}(x)=E(x,t),$ (3.5)

where $[E(x,t)]_{qp}=\epsilon_{p}(t)\delta_{qp}$ is the diagonal matrix
associated to $T(x,t)$. The quadratic form $H(x,t)$ may then be expressed in
terms of instantaneous diagonal Fermi operators
$\eta(x,t)=W_{t}^{\dagger}(x)c(x)$ such that

$\displaystyle H(x,t)$
$\displaystyle=c^{\dagger}(x)T(x,t)c(x)=c^{\dagger}(x)W_{t}(x)E(x,t)W_{t}^{\dagger}(x)c(x)$
$\displaystyle=\eta^{\dagger}(x,t)E(x,t)\eta(x,t)=\sum_{q}\epsilon_{q}(t)\eta^{\dagger}_{q}(x,t)\eta_{q}(x,t)\;.$
(3.6)

The relation between the instantaneous diagonal Fermi operators and the
diagonal Fermi operators (at $t=0$) of the local Hamiltonian
$H(x)=\sum_{q}\epsilon_{q}(x)\eta_{q}^{\dagger}(x)\eta_{q}(x)$ is obtained
from

$\eta(x,t)=W_{t}^{\dagger}(x)c(x)=W_{t}^{\dagger}(x)W_{0}(x)\eta(x)\equiv
D_{t}(x)\eta(x)\;,$ (3.7)

where $D_{t}(x)=W_{t}^{\dagger}(x)W_{0}(x)$ defines a unitary mapping
transforming $\eta(x)$ into $\eta(x,t)$. The instantaneous Hamiltonian (3.4)
can thus be written as

$\displaystyle H(x,t)\equiv
c^{\dagger}(x)T(x,t)c(x)=\eta^{\dagger}(x)D_{t}^{\dagger}(x)E(x,t)D_{t}(x)\eta(x)\equiv\eta^{\dagger}(x)\Omega(x,t)\eta(x)\;,$
(3.8)

where the new matrix

$\Omega(x,t)=D_{t}^{\dagger}(x)E(x,t)D_{t}(x)=W_{0}^{\dagger}(x)T(x,t)W_{0}(x)$
(3.9)

is not in general diagonal. With the matrix elements
$[\Omega(x,t)]_{qp}=\omega_{qp}(x,t)$, the explicit expression of $H(x,t)$ is:

$\displaystyle
H(x,t)=H(x)+\sum_{q}\left[\omega_{qq}(x,t)-\epsilon_{q}(x)\right]\eta_{q}^{\dagger}(x)\eta_{q}(x)+\sum_{q\neq
p}\omega_{qp}(x,t)\eta_{q}^{\dagger}(x)\eta_{p}(x)\;.$ (3.10)

The diagonal correction to $H(x)$ describes the energy level shift of the
original single-particle spectrum while the non-diagonal term makes the
transitions between the single-particle states.

###  3.2 Effective local temperature

Assuming that the system is at time $t$ in a local Gaussian state of the form
(3.1), we want to quantify how close is that state to an actual local
canonical state $\omega(H(x),\lambda)$ at inverse temperature $\lambda$. If
the local state is very close to this canonical state, we shall then identify
the parameter $\lambda$ as the effective local inverse temperature
$\beta(x,t)$ of the system at position $x$ and time $t$.

To properly quantify the closeness of the states, we consider the distance

${d}(x,t,\lambda)\equiv\|\rho(x,t)-\omega(H(x),\lambda)\|\;$ (3.11)

defined from the Hilbert-Schmidt operator norm (on bounded operators)

$\|A\|=\sqrt{\mathrm{\,tr}\\{A^{\dagger}A\\}}\;.$ (3.12)

A more natural measure of the distance between two states $\rho_{1}$ and
$\rho_{2}$ would have been given by the trace-norm
$\|\rho_{1}-\rho_{2}\|_{1}$, where

$\|A\|_{1}=\mathrm{\,tr}|A|=\mathrm{\,tr}\sqrt{A^{\dagger}A}\;,$

as this distance is small if and only if the two states are effectively
indistinguishable in the experimental sense. This is not the case for the
Hilbert-Schmidt norm since, for high-dimensional spaces, it can be small even
for perfectly distinguishable states (for example orthogonal states).
Nevertheless, the two norms are related through the inequality

$\|A\|_{1}\leqslant\sqrt{d}\|A\|,$

where $d$ is the dimension of the Hilbert space on which $A$ is defined. In
this sense, for finite-dimensional spaces, the two norms lead to physically
equivalent conclusions. The advantage of using the Hilbert-Schmidt norm is
that it is much easier to be handled.

The effective local inverse temperature $\beta(x,t)$ at time $t$ is defined
through the minimization of the distance $d(x,t,\lambda)$ over the one-
parameter canonical family $\omega(H(x),\lambda)$ :

$d(x,t,\beta(x,t))\equiv\mathrm{inf}_{\lambda}d(x,t,\lambda)\;.$ (3.13)

Taking the $\lambda$ derivative of $d^{2}(x,t,\lambda)$ one arrives at

$\partial_{\lambda}d^{2}(x,t,\lambda)=2\langle\left(H(x)-\langle
H(x)\rangle_{\omega(H(x),\lambda)}\right)\left(\rho(x,t)-\omega(H(x),\lambda)\right)\rangle_{\omega(H(x),\lambda)},$
(3.14)

where we have defined the expectation value $\langle
A\rangle_{\omega}\equiv\mathrm{\,tr}\\{A\omega\\}$. Consequently, the roots of
that equation are simply given by the vanishing of the connected correlation
function

$\langle
H(x)\Delta_{\lambda}\rho(x,t)\rangle_{\lambda}^{c}\Big{|}_{\lambda=\beta(x,t)}=0,$
(3.15)

where $\Delta_{\lambda}\rho(x,t)\equiv\rho(x,t)-\omega(H(x),\lambda)$ and
$\langle AB\rangle^{c}=\langle AB\rangle-\langle A\rangle\langle B\rangle$.
See [54, 53] for a somehow related approach based on the fidelity measure.

To give an explicit formula in the case of Gaussian states, we need to compute
the following trace

$\mathrm{\,tr}\left\\{\mathrm{e}^{c^{\dagger}(x)A(x)c(x)}e^{c^{\dagger}(x)B(x)c(x)}\right\\}.$
(3.16)

Noticing that

$[c^{\dagger}(x)A(x)c(x),c^{\dagger}(x)B(x)c(x)]=c^{\dagger}(x)[A(x),B(x)]c(x)$
(3.17)

one has from Backer-Campbell-Hausdorff formula

$\mathrm{e}^{c^{\dagger}(x)A(x)c(x)}\mathrm{e}^{c^{\dagger}(x)B(x)c(x)}=\mathrm{e}^{c^{\dagger}(x)A(x)c(x)+c^{\dagger}(x)B(x)c(x)+\frac{1}{2}[c^{\dagger}(x)A(x)c(x),c^{\dagger}(x)B(x)c(x)]+\dots}\,,$
(3.18)

that is, using the previous commutator identity,

$\mathrm{e}^{c^{\dagger}(x)A(x)c(x)}\mathrm{e}^{c^{\dagger}(x)B(x)c(x)}=\mathrm{e}^{c^{\dagger}(x)\left(A(x)+B(x)+\frac{1}{2}[A(x),B(x)]+\dots\right)c(x)}=\mathrm{e}^{c^{\dagger}(x)M(x)c(x)}\,,$
(3.19)

with the matrix $M$ defined by

$\mathrm{e}^{M(x)}=\mathrm{e}^{A(x)}\mathrm{e}^{B(x)}\;.$ (3.20)

Now, since the trace of a Gaussian state is

$\mathrm{\,tr}\left\\{\mathrm{e}^{c^{\dagger}(x)M(x)c(x)}\right\\}=\textrm{det}({\mathbbm{1}}_{x}+\mathrm{e}^{M(x)})\;,$
(3.21)

where ${\mathbbm{1}}_{x}$ is the unit matrix of size $\ell$ (the size of the
local cell), one arrives at the identity

$\mathrm{\,tr}\left\\{\mathrm{e}^{c^{\dagger}(x)A(x)c(x)}\mathrm{e}^{c^{\dagger}(x)B(x)c(x)}\right\\}=\textrm{det}({\mathbbm{1}}_{x}+\mathrm{e}^{A(x)}\mathrm{e}^{B(x)})\;.$
(3.22)

Together with the formula

$\partial_{\lambda}\textrm{det}({\mathbbm{1}}+\mathrm{e}^{\lambda
A}\mathrm{e}^{B})=\textrm{det}({\mathbbm{1}}+\mathrm{e}^{\lambda
A}\mathrm{e}^{B})\mathrm{\,tr}\\{({\mathbbm{1}}+\mathrm{e}^{\lambda
A}\mathrm{e}^{B})^{-1}A\mathrm{e}^{\lambda A}\mathrm{e}^{B}\\}$ (3.23)

and (3.1), the equation (3.15) leads to

$\displaystyle\frac{\textrm{det}({\mathbbm{1}}_{x}+\mathrm{e}^{-2\lambda
T(x,0)})}{\textrm{det}({\mathbbm{1}}_{x}+\mathrm{e}^{-\lambda
T(x,0)})}\,\mathrm{\,tr}\left\\{T(x,0)\left(\frac{1}{{\mathbbm{1}}_{x}+\mathrm{e}^{\lambda
T(x,0)}}-\frac{1}{{\mathbbm{1}}_{x}+\mathrm{e}^{2\lambda
T(x,0)}}\right)\right\\}$
$\displaystyle-\left.\frac{\textrm{det}({\mathbbm{1}}_{x}+\mathrm{e}^{-\lambda
T(x,0)}\mathrm{e}^{-\beta(x)T(x,t)})}{\textrm{det}({\mathbbm{1}}_{x}+\mathrm{e}^{-\beta(x)T(x,t)})}\right.$
$\displaystyle\left.\times\mathrm{\,tr}\left\\{T(x,0)\left(\frac{1}{{\mathbbm{1}}_{x}+\mathrm{e}^{\lambda
T(x,0)}}-\frac{1}{{\mathbbm{1}}_{x}+\mathrm{e}^{\beta(x)T(x,t)}\mathrm{e}^{\lambda
T(x,0)}}\right)\right\\}\right|_{\lambda=\beta(x,t)}=0\;.$ (3.24)

This cumbersome explicit condition is the main result we wanted to derive.

At high temperature initial state and assuming that the effective local
temperature remains high too, that is for $\lambda\sim\beta(x)\ll 1$, using
the identity $\textrm{det}({\mathbbm{1}}_{x}+\epsilon
M)=1+\epsilon\mathrm{\,tr}\\{M\\}+o(\epsilon)$, to the leading order in
$\beta(x)$, the previous equation drastically simplifies into

$\left.\lambda\mathrm{\,tr}\left\\{T^{2}(x,0)\right\\}-\beta(x)\mathrm{\,tr}\left\\{T(x,0)T(x,t)\right\\}\right|_{\lambda=\beta(x,t)}=0,$
(3.25)

which gives the effective local temperature as

$\beta(x,t)=\beta(x)\frac{\mathrm{\,tr}\\{T(x,0)T(x,t)\\}}{\mathrm{\,tr}\\{T^{2}(x,0)\\}}=\beta(x)\left(1+\frac{\mathrm{\,tr}\\{T(x,0)\Delta(x,t)\\}}{\mathrm{\,tr}\\{T^{2}(x,0)\\}}\right),$
(3.26)

where we have defined the difference matrix $\Delta(x,t)\equiv T(x,t)-T(x,0)$.
Using (3.9) we have in terms of the one-particle spectrum

$\beta(x,t)=\beta(x)\frac{\mathrm{\,tr}\\{E(x,0)\Omega(x,t)\\}}{\mathrm{\,tr}\\{E^{2}(x,0)\\}}=\beta(x)\frac{\sum_{q}\epsilon_{q}(x)\omega_{qq}(x,t)}{\sum_{q}\epsilon_{q}^{2}(x)}\;.$
(3.27)

In order to appreciate the meaning of this formula, let us introduce the
scalar product defined on $\textrm{End}(\mathfrak{H}_{x})$ by

$(A,B)=\mathrm{\,tr}\\{A^{\dagger}B\\}\;,\quad\forall\;A,B\in\textrm{End}(\mathfrak{H}_{x})\;.$
(3.28)

Equation (3.26) can thus be written as

$\beta(x,t)=\beta(x)\frac{(T(x,0),T(x,t))}{(T(x,0),T(x,0))}\;.$ (3.29)

This means that only the non-orthogonal part of the actual one-particle
Hamiltonian $T(x,t)$, with respect to the chosen reference state defined
through the one-particle Hamiltonian $T(x,0)$, contributes to the effective
local inverse temperature $\beta(x,t)$. Whatever part in $T(x,t)$ that is
orthogonal to $T(x,0)$ will not affect the value of the local inverse
temperature, it may in general nevertheless increase the distance to the
optimum canonical state $\omega(H(x),\beta(x,t))$. If the one-particle
Hamiltonian $T(x,t)$ is completely orthogonal to the coupling matrix of the
system, then this procedure will fix an infinite value to the local
temperature.

Moreover, since in a hydrodynamical cell of size $\ell$ the local system is
translation invariant, the local Hamiltonian can be decomposed into a sum over
local conserved charges
$H(x)=\sum_{k}H^{(k)}(x)=\sum_{k}q^{(k)}(x)c^{\dagger}(x)Q^{(k)}(x)c(x)$,
where the matrices $Q^{(k)}(x)$ are given by222We suppose here that the
hydrodynamical cell is large enough such that we can neglect the boundary
details. The $H^{(k)}(x)$ are charges in the sense that they commute with each
other and as a consequence with the Hamiltonian $[H(x),H^{(k)}(x)]=0$ which
implies that they are conserved quantities $\partial_{t}H^{(k)}(x)=0$.
Locally, this translates into continuity equations satisfied by the charge
densities
$q^{(k)}(x)[c^{\dagger}_{j}(x)c_{j+k}(x)+c^{\dagger}_{j+k}(x)c_{j}(x)]$.

$\left(Q^{(k)}(x)\right)_{ij}=\frac{1}{2}(\delta_{i,j+k}+\delta_{i+k,j})$
(3.30)

and $q^{(k)}(x)$s are real coefficients. Typically, $Q^{(0)}$ gives the on-
site energy contribution or potential energy

$H^{(0)}(x)=q^{(0)}(x)\sum_{j}c^{\dagger}_{j}(x)c_{j}(x)\;,$ (3.31)

while $Q^{(1)}(x)$ gives the kinetic contribution (one-site hopping terms)

$H^{(1)}(x)=q^{(1)}(x)\sum_{j}\left(c^{\dagger}_{j}(x)c_{j+1}(x)+c^{\dagger}_{j+1}(x)c_{j}(x)\right)$
(3.32)

and so on. In general, usual short range Hamiltonians contain only very few of
these charges but one may also encounter long-range hopping situations, for
which in general the physical coefficients $q^{(k)}$ are given by a decaying
function of the hopping distance $k$, such as a power law $q^{(k)}\sim
k^{-\alpha}$ with some positive exponent $\alpha$. Notice here that we do not
consider in the reference Hamiltonian $H(x)$ the presence of current like
terms, associated to antisymmetric Hermitian matrices of the form
$\textrm{i}j^{(k)}(x)(\delta_{i,j+k}-\delta_{i+k,j})$ leading to terms like
$J^{(1)}(x)=\textrm{i}j^{(1)}(x)\sum_{j}\left(c^{\dagger}_{j}(x)c_{j+1}(x)-c^{\dagger}_{j+1}(x)c_{j}(x)\right)$,
but in principle we could.

To be more specific, let us suppose that the reference Hamiltonian is the sum
over the $K+1$ first charges $Q^{(k)}$. The set of charges $\\{Q^{(k)}\\}$ for
$k=0,1,\dots,K$ is obviously not a complete set but all the charges are
orthogonal to each other since
$(Q^{k},Q^{k^{\prime}})\propto\delta_{k,k^{\prime}}$. Indeed, the $k$ matrix
$Q^{(k)}=\frac{1}{2}\left(L_{k}+R_{k}\right)$, where $L_{k}$ is the shift to
the left by a distance $k$ and $R_{k}$ the corresponding shift to the right.
For $k=0$, $Q^{(0)}=L_{0}=R_{0}={\mathbbm{1}}_{x}$. Since
$L_{k}^{\dagger}=R_{k}$, one has
$(L_{k},R_{p})=\mathrm{\,tr}\\{L_{k}^{\dagger}R_{p}\\}=\mathrm{\,tr}\\{R_{p+k}\\}=0$
and consequently

$\displaystyle(Q^{(k)},Q^{(p)})$
$\displaystyle=\frac{1}{4}\left[(L_{k},L_{p})+(R_{k},R_{p})\right]=\frac{1}{4}\left(\mathrm{\,tr}\\{L_{p-k}\\}+\mathrm{\,tr}\\{R_{p-k}\\}\right)=\frac{\ell}{2}\delta_{k,p}\quad\forall
k\neq 0\;,$ (3.33) $\displaystyle(Q^{(0)},Q^{(0)})$ $\displaystyle=\ell\;.$
(3.34)

One can develop the $T(x,t)$ coupling matrix into this set of charges plus a
remaining part which is orthogonal to it:

$T(x,t)=\sum_{k=0}^{K}q^{(k)}(x,t)Q^{(k)}(x)+T_{\perp}(x,t)\;,$ (3.35)

with

$\displaystyle(Q^{(p)}(x),T(x,t))$
$\displaystyle=q^{(p)}(x,t)\frac{\ell}{2}\quad\forall p\neq 0,$ (3.36)
$\displaystyle(Q^{(0)}(x),T(x,t))$ $\displaystyle=q^{(0)}(x,t)\ell\;.$ (3.37)

Notice here that since $Q^{(k)}=\frac{1}{2}\left(L_{k}+R_{k}\right)$, the
coefficient $(Q^{(k)}(x),T(x,t))$ is nothing else but the trace over the two
upper and lower $k$-diagonals of $T(x,t)$, that is
$\frac{1}{2}\sum_{j}[T_{j,j+k}(x,t)+T_{j+k,j}(x,t)]$. This implies that even
if within the cell $x$ the matrix $T(x,t)$ itself is not homogeneous, the
outcome to the local thermal properties is averaged over the hydrodynamical
cell. Plugging (3.35) into (3.29) gives our final formula

$\beta(x,t)=\beta(x)\frac{q^{(0)}(x)q^{(0)}(x,t)+\frac{1}{2}\sum_{k=1}^{K}q^{(k)}(x)q^{(k)}(x,t)}{\left[q^{(0)}(x)\right]^{2}+\frac{1}{2}\sum_{k=1}^{K}\left[q^{(k)}(x)\right]^{2}}\;.$
(3.38)

If the Hamiltonian $H(x)$ is a purely hopping Hamiltonian, then only
$q^{(1)}(x)$ is non-zero and the formula for the inverse temperature
simplifies into

$\beta(x,t)=\beta(x)\frac{q^{(1)}(x,t)}{q^{(1)}(x)}\;,$

which is kind of intuitive since it reflects the simplest identification of
$\beta(x,t)H(x)\simeq\beta(x)H(x,t)$, up to orthogonal parts $T_{\perp}(x,t)$,
leading in the case of a single charge to
$\beta(x,t)q^{(k)}(x)Q^{(k)}(x)\simeq\beta(x)q^{(k)}(x,t)Q^{(k)}(x)$ that is
$\beta(x,t)q^{(k)}(x)=\beta(x)q^{(k)}(x,t)$.

###  3.3 Effective temperature of the hopping fermions with projective
measurements of the local densities

Let us apply this derivation to the case of the one-dimensional hopping
fermions subjected to projective measurements of their local densities that we
described in section 2.2. The unitary dynamics is perturbed by the projective
measurements at a rate $1/\tau$ of the one-site occupation numbers
$\hat{n}_{j}$. As $\tau$ is increasing, the dynamics is getting closer and
closer to the unitary evolution. On the contrary, for a high measurement rate
(low $\tau$) the system dynamics is very far from a unitary dynamics, with a
very low initial spreading and finally a saturation of the entanglement to a
constant value [21].

The dynamics being GPD, it is fully encoded into the time-evolution of the
two-point function (2.21) through the unitary evolution
$C(t+s)=R^{\dagger}(s)C(t)R(s)$ and the projection rules (2.29) and (2.30),
from which we reconstruct the coupling matrix $T$. We averaged the deduced
inverse temperature (3.38) over different quantum trajectories333Different
quantum trajectories are generated from an initial state by following in time
the different possible outcomes and “state re-preparations” that occur after
each projective measurements of the local densities., typically we have taken
up to a 100 different trajectories for a cell of size $\ell\sim 100$ sites.

Figure 1: (Colour online) On the left, we show the time evolution of the
averaged inverse temperature starting from an initial value $\beta(0)$ (in
linear-log scale). The different colored symbols correspond to different
values of the measurement rate $1/\tau$. The dashed lines are exponential fits
with the ansatz $\langle\beta(t)\rangle/\beta(0)=\mathrm{e}^{-\alpha(\tau)t}$.
On the right, we show the evolution of the fitting parameter $\alpha(\tau)$ as
a function of $\tau$ in a log-log scale. The dashed line corresponds to
$\alpha(\tau)=2/\tau$.

We show the behavior of the effective inverse temperature in figure 1. On the
left, the scaling of the averaged inverse temperature is plotted versus time
for various measurement rates $1/\tau$, computed for several values of the
initial inverse temperature from $\beta(0)=0.1$ up to $\beta(0)=5$. We observe
a clear exponential decay toward zero (infinite temperature) at a rate
$\alpha(\tau)$ which is very well fitted by $2/\tau$, see the right-hand
figure. This value coincides with the inverse of the average life-time
$\tau/2$ of the semi-classical non-interacting quasi-particles that emerge
from a Wigner function formalism applied to such a problem [66]. Within this
picture, the average inverse temperature is proportional to the probability
that a semi-classical particle, created at the initial time, survives up to
time $t$. The precise connection of the effective local temperature with the
life-time of those semi-classical particles is still under investigation and
will be presented in a forthcoming publication.

##  4 Discussion

We have discussed the possibility of identifying an effective local
temperature for one-dimensional fermionic quantum systems undergoing a
Gaussian Preserving Dynamics. The identification relies on the comparison
between the actual Gaussian state, generated by a dynamics which can be in
general non-unitary, and a reference Gibbs state which for quadratic
Hamiltonians is Gaussian too. The effective local temperature is deduced from
the minimization of the distance between the two states, using the Hilbert-
Schmidt norm of trace class operators, and leads to a cumbersome formula which
drastically simplifies in the high temperature limit. In this regime, the
effective temperature is proportional to the projection of the actual one
particle Hamiltonian, which represents the instantaneous coupling content of
the evolving system, on the reference one-particle Hamiltonian. Decomposing
the Hamiltonian of the system on a set of local charges, representing
different orthogonal energy components of the system, we show that the part of
the actual coupling matrix which is orthogonal to the initial charge content
does not contribute to the value of the effective inverse local temperature.
We have applied this theory to the case of a GPD of one-dimensional hopping
fermions submitted to projective measurements of the fermions densities. In
such a case, we have shown numerically that the local effective temperature
increases with an exponential law toward infinity as expected, see [21].

## References

  * [1] Calabrese P., Cardy J. L., J. Stat. Mech: Theory Exp., 2005, P04010, doi:10.1088/1742-5468/2005/04/P04010.
  * [2] Amico L., Fazio R., Osterloh A., Vedral V., Rev. Mod. Phys., 2008, 80, 517, doi:10.1103/RevModPhys.80.517.
  * [3] Eisler V., Peschel I., J. Stat. Mech: Theory Exp., 2007, P06005, doi:10.1088/1742-5468/2007/06/P06005.
  * [4] Eisler V., Karevski D., Platini T., Peschel I., J. Stat. Mech: Theory Exp., 2008, P01023,
doi:10.1088/1742-5468/2008/01/P01023.

  * [5] Collura M., Karevski D., Phys. Rev. Lett., 2010, 104, 200601, doi:10.1103/PhysRevLett.104.200601.
  * [6] Collura M., Karevski D., Phys. Rev. A, 2011, 83, 023603, doi:10.1103/PhysRevA.83.023603.
  * [7] Scopa S., Karevski D., J. Phys. A: Math. Theor., 2017, 50, 425301, doi:10.1088/1751-8121/aa890f.
  * [8] Scopa S., Unterberger J., Karevski D., J. Phys. A: Math. Theor., 2018, 51, 185001, doi:10.1088/1751-8121/aab8a5.
  * [9] Eisert J., Cramer M., Plenio M. B., Rev. Mod. Phys., 2010, 82, 277, doi:10.1103/RevModPhys.82.277.
  * [10] Laflorencie N., Phys. Rep., 2016, 646, 1, doi:10.1016/j.physrep.2016.06.008.
  * [11] Lieb E. H., Robinson D. W., Nachtergaele B., Solovej J. P., Yngvason J. (Eds.), Statistical Mechanics. Springer, Berlin, Heidelberg, 1972, doi:10.1007/978-3-662-10018-9_25
  * [12] Alba V., Phys. Rev. B, 2018, 97, 245135, doi:10.1103/PhysRevB.97.245135.
  * [13] Rigol M., Dunjko V., Olshanii M., Nature, 2008, 452, 854, doi:10.1038/nature06838.
  * [14] Ilievski E., de Nardis J., Wouters B., Caux J.-S., Essler F. H. L., Prosen T., Phys. Rev. Lett., 2015, 115, 157201, doi:10.1103/PhysRevLett.115.157201.
  * [15] Ilievski E., Medenjak M., Prosen T., Zadnik L., J. Stat. Mech: Theory Exp., 2016, 2016, 064008,
doi:10.1088/1742-5468/2016/06/064008.

  * [16] Abanin D. A., Altman E., Bloch I., Serbyn M., Rev. Mod. Phys., 2019, 91, 021001,
doi:10.1103/RevModPhys.91.021001.

  * [17] Wiseman H. M., Milburn G. J., Quantum Measurement and Control, Cambridge University Press, Cambridge, 2009, doi:10.1017/CBO9780511813948.
  * [18] Cao X., Tilloy A., De Luca A., SciPost Phys., 2019, 7, 024, doi:10.21468/SciPostPhys.7.2.024.
  * [19] Skinner B., Ruhman J., Nahum A., Phys. Rev. X, 2019, 9, 031009, doi:10.1103/PhysRevX.9.031009.
  * [20] Alberton O., Buchhold M., Diehl S., Phys. Rev. Lett., 2021, 126, 170602, doi:10.1103/PhysRevLett.126.170602.
  * [21] Coppola M., Tirrito E., Karevski D., Collura M., Phys. Rev. B, 2022, 105, 094303,
doi:10.1103/PhysRevB.105.094303.

  * [22] Breuer H.-P., Petruccione F., The Theory of Open Quantum Systems, Oxford University Press, Oxford, 2007, doi:10.1093/acprof:oso/9780199213900.001.0001.
  * [23] Karevski D., Physique quantique des champs et des transitions de phase, Ellipses, Références sciences, 2022.
  * [24] Karevski D., Platini T., Phys. Rev. Lett., 2009, 102, 207207, doi:10.1103/PhysRevLett.102.207207.
  * [25] Platini T., Harris R. J., Karevski D., J. Phys. A: Math. Theor., 2010, 43, 135003, doi:10.1088/1751-8113/43/13/135003.
  * [26] Prosen T., Phys. Rev. Lett., 2011, 106, 217206, doi:10.1103/PhysRevLett.106.217206.
  * [27] Prosen T., Phys. Rev. Lett., 2011, 107, 137201, doi:10.1103/PhysRevLett.107.137201.
  * [28] Karevski D., Popkov V., Schütz G. M., Phys. Rev. Lett., 2013, 110, 047201,
doi:10.1103/PhysRevLett.110.047201.

  * [29] Popkov V., Karevski D., Schütz G. M., Phys. Rev. E, 2013, 88, 062118, doi:10.1103/PhysRevE.88.062118.
  * [30] Landi G. T., Novais E., de Oliveira M. J., Karevski D., Phys. Rev. E, 2014, 90, 042142,
doi:10.1103/PhysRevE.90.042142.

  * [31] Landi G. T., Karevski D., Phys. Rev. B, 2015, 91, 174422, doi:10.1103/PhysRevB.91.174422.
  * [32] Zubarev D. N., Nonequilibrium Statistical Thermodynamics, Consultants Bureau, New York, 1974.
  * [33] MacLennan J. A., Introduction to Nonequilibrium Statistical Mechanics, Prentice-Hall, NJ, 1988.
  * [34] Antal T., Rácz Z., Sasvári L., Phys. Rev. Lett., 1997, 78, 167, doi:10.1103/PhysRevLett.78.167.
  * [35] Antal T., Rácz Z., Rákos A., Schütz G. M., Phys. Rev. E, 1998, 57, 5184, doi:10.1103/PhysRevE.57.5184.
  * [36] Antal T., Rácz Z., Rákos A., Schütz G. M., Phys. Rev. E, 1999, 59, 4912, doi:10.1103/PhysRevE.59.4912.
  * [37] Ogata Y., Phys. Rev. E, 2002, 66, 016135, doi:10.1103/PhysRevE.66.016135.
  * [38] Ogata Y., Phys. Rev. E, 2002, 66, 066123, doi:10.1103/PhysRevE.66.066123.
  * [39] Aschbacher W. H., Pillet C.-A., J. Stat. Phys., 2003, 112, 1153, doi:10.1023/A:1024619726273.
  * [40] Bernard D., Doyon B., J. Phys. A: Math. Theor., 2012, 45, 362001, doi:10.1088/1751-8113/45/36/362001.
  * [41] Collura M., Karevski D., Phys. Rev. B, 2014, 89, 214308, doi:10.1103/PhysRevB.89.214308.
  * [42] Platini T., Karevski D., J. Phys. A: Math. Theor., 2007, 40, 1711, doi:10.1088/1751-8113/40/8/002.
  * [43] Karevski D., Eur. Phys. J. B, 2002, 27, 147, doi:10.1140/epjb/e20020139.
  * [44] Platini T., Karevski D., Eur. Phys. J. B, 2005, 48, 225, doi:10.1140/epjb/e2005-00402-2.
  * [45] Landi G. T., Karevski D., Phys. Rev. E, 2016, 93, 032122, doi:10.1103/PhysRevE.93.032122.
  * [46] Scopa S., Karevski D., (unpublished).
  * [47] Hartmann M., Mahler G., Hess O., Phys. Rev. Lett., 2004, 93, 080402, doi:10.1103/PhysRevLett.93.080402.
  * [48] Hartmann M., Mahler G., Hess O., Phys. Rev. E, 2004, 70, 066148, doi:10.1103/PhysRevE.70.066148.
  * [49] Hartmann M., Mahler G., Europhys. Lett., 2005, 70, 579, doi:10.1209/epl/i2004-10518-5.
  * [50] Eisler V., Legeza Ö., Rácz Z., J. Stat. Mech: Theory Exp., 2006, P11013,
doi:10.1088/1742-5468/2006/11/P11013.

  * [51] Garcia-Saez A., Ferraro A., Acin A., Phys. Rev. A, 2009, 79, 052340, doi:10.1103/PhysRevA.79.052340.
  * [52] Ferraro A., Garcia-Saez A., Acin A., Europhys. Lett., 2012, 98, 10009, doi:10.1209/0295-5075/98/10009.
  * [53] Kliesch M., Gogolin C., Kastoryano M. J., Riera A., Eisert J., Phys. Rev. X, 2014, 4, 031019,
doi:10.1103/PhysRevX.4.031019.

  * [54] De Pasquale A., Rossini D., Fazio R., Giovannetti V., Nat. Commun., 2016, 7, 12782, doi:10.1038/ncomms12782.
  * [55] Moreno C., Urbina J.-D., Phys. Rev. E, 2019, 99, 062135, doi:10.1103/PhysRevE.99.062135.
  * [56] Brunner N., Linden N., Popescu S., Skrzypczyk P., Phys. Rev. E, 2012, 85, 051117,
doi:10.1103/PhysRevE.85.051117.

  * [57] Morozov V., Ignatyuk V., Particles, 2018, 1, No. 1, 285–295, doi:10.3390/particles1010023.
  * [58] Latune C. L., Sinayskiy I., Petruccione F., Quantum Sci. Technol., 2019, 4, 025005,
doi:10.1088/2058-9565/aaf5f7.

  * [59] Collura M., Aufderheide H., Roux G., Karevski D., Phys. Rev. A, 2012, 86, 013615,
doi:10.1103/PhysRevA.86.013615.

  * [60] Wendenbaum P., Collura M., Karevski D., Phys. Rev. A, 2013, 87, 023624, doi:10.1103/PhysRevA.87.023624.
  * [61] Scopa S., Karevski D., J. Phys. A: Math. Theor., 2017, 50, 425301, doi:10.1088/1751-8121/aa890f.
  * [62] Scopa S., Unterberger J., Karevski D., J. Phys. A: Math. Theor., 2018, 51, 185001, doi:10.1088/1751-8121/aab8a5.
  * [63] Riggio F., Brun Y., Karevski D., Faribault A., Dubail J., Phys. Rev. A, 2022, 106, 053309,
doi:10.1103/PhysRevA.106.053309.

  * [64] Popescu S., Short A. J., Winter A., Nat. Phys., 2006, 2, 754, doi:10.1038/nphys444.
  * [65] Goldstein S., Lebowitz J. L., Tumulka R., Zanghi N., Phys. Rev. Lett., 2006, 96, 050403,
doi:10.1103/PhysRevLett.96.050403.

  * [66] Coppola M., Landi G. T., Karevski D., (unpublished).
  * [67] Prosen T., New J. Phys., 2008, 10, 043026, doi:10.1088/1367-2630/10/4/043026.
  * [68] Prosen T., J. Phys. A: Math. Theor., 2015, 48, 373001, doi:10.1088/1751-8113/48/37/373001.

Ukrainian 0

Äåÿê ìðêóâàííÿ ùîäî ëîêàëüíî¿ òåðìàëçàö¿ íåðâíîâàæíèõ ïðîñòîðîâèõ êâàíòîâèõ
ñèñòåì Ì. Êîïïîëà, Ä. Êàðåâñê

Óíâåðñèòåò Ëîòàðèíã¿, CNRS, LPCT, F-54000 Íàíñ, Ôðàíöÿ