poly.tex

\documentclass[nocopyrightspace,preprint]{sigplanconf-pldi15}

\usepackage[utf8]{inputenc} %for utf8 input
\usepackage{amssymb} %for shift symbol
\usepackage{amsmath}
\usepackage{listings} %for code
\usepackage{mathpartir} %for typing rules
\usepackage{microtype} %better micro typing
\usepackage{stmaryrd} %for llbracket
\usepackage{mathabx} % for boxes
\usepackage{graphicx} %to include png images
\usepackage{xcolor} %for colors
\usepackage{url}
\usepackage{enumitem}
\usepackage{array} %for stupid tables

%----------------------------------------------------

\usepackage{prettyref}
\newcommand{\pref}[1]{\prettyref{#1}}
\newcommand{\Pref}[1]{\prettyref{#1} \vpageref[]{#1}}
\newcommand{\ppref}[1]{\vpageref[]{#1}}
\newrefformat{fig}{Figure~\ref{#1}}
\newrefformat{app}{Appendix~\ref{#1}}
\newrefformat{tab}{Table~\ref{#1}}
\newrefformat{cha}{Challenge~\ref{#1}}
\newrefformat{thm}{Theorem~\ref{#1}}

%----------------------------------------------------

\usepackage{amsthm}
\newtheorem{lemma}{Lemma}
\newtheorem{corollary}{Corollary}
\newtheorem{theorem}{Theorem}
\newtheorem{proposition}{Proposition}

%----------------------------------------------------

\input{definitions}
\begin{document}

\section{Introduction}

\paragraph{Richer potential functions.}
Compositionality is improved over previous work by dropping
the systematic requirement of non-negativity for coefficients
of the potential functions.
%
This new accounting system is motivated
here using two example programs.

\begin{minipage}[b]{.45\linewidth}
\begin{lstlisting}
while (x > 0) {
  tick(1); x -= 1;
}
\end{lstlisting}
\end{minipage}
\begin{minipage}[b]{.45\linewidth}
\begin{lstlisting}
while (x > 0) {
  x -= 1; tick(1);
}
\end{lstlisting}
\end{minipage}

While the two loops above have the exact same cost,
the tool \toolname{} reports different bounds: $1 +
|[0,x]|$ for the first one, and $|[0,x]|$ for the
second.  Both bounds are sound, but only the second
one is tight.
%
The imprecision is caused by the swap of the two
statements in the loop body:  In the first case
we first use one resource unit, then make one
available using potential of $[0,x]$ in the
decrement; while in the second case we do the
contrary, and thus, do not require the extra
resource unit in the loop invariant.

To palliate this lack of robustness and obtain the
tight bound $|[0,x]|$ for the first loop, we introduce
the concept of \emph{borrowing}.
While analyzing the first loop, we propose to borrow
one resource unit first, and then pay it back using
the decrement statement.  Negative coefficients in
potential functions achieve precisely this borrowing.

Non-negativity of potential functions is critical for
the soundness of amortized analysis systems.  Previous
works ensure it by systematically constraining the sign
of all the
coefficients of the potential functions.
In this paper we do not escape from this requirement,
but we turn the usual syntactical criterion into a
semantic one. Non-negativity becomes a theorem proved
using meta-theoretical reasoning.

\Quentin{Another example where debts are useful.}
\begin{lstlisting}
while (x > 0) { x -= y+1; [...] x += y; }
\end{lstlisting}

\paragraph{Low-level code support.}
Previous systems based on amortized analysis get their
bounds on structured high-level languages.  In this paper
we show that amortized analysis is equally suited to
work on unstructured programs.  We use a very general
\emph{control flow graph} (CFG) representation of programs
that is similar to usual bytecode formats.
Low-level analysis presents several key advantages compared
to source-level analysis.
\begin{enumerate}
\item Cost semantics for bytecodes and such are easier to
      define and more precise than source-level cost
      semantics.
\item Embedded and critical systems need bounds on the
      compiled code.  Analyzing the compiled code directly
      leaves more freedom to the compiler than if it had
      to preserve resource bounds computed at the source
      level.
\item Programs for which the source code is not available
      can be analyzed.  For example, in the context of
      security audits to find space or time complexity
      vulnerabilities.
\end{enumerate}

\paragraph{Polynomial bounds.}
Using only local modifications of the analysis used by
\toolname{} we are now able to produce polynomial bounds
while retaining entirely the amortization abilities of
the original system.  Size changes are still accounted
naturally, but this time in a polynomial context, as
demonstrated in the example below.
%
\begin{lstlisting}
while (x > 0) { x--; y += x; }
while (y > 0) { y--; tick(1); }
\end{lstlisting}
%
Combining both negative coefficients and the new
polynomial rules, our system is the only one able
to infer the tight bound $|[0,x]|^2 - 0.5 |[0,x]| +
|[0,y]|$.  To make sure that our new
system will not regress on intricate
linear examples, in addition to the soudness proof,
we prove that all derivations made in the linear
system are valid derivations of the polynomial
system.

\paragraph{Decoupling from termination.}
We
propose to separate the resource bound problem from the
termination problem.  This splitting allows our system
to assume that the program is terminating, we then make use
of this assumption to relax even more the constraints fed
to the LP sover, hence enabling a more precise analysis.
%
This is the first work to include this split, and we
think it is an interesting new way to leverage termination
provers that can already handle a much larger class of
programs than any resource analysis tool.

More precisely, termination allows us to prove that
potential functions remain non-negative throughout
the program execution by only constraining the sign of
final potential functions.  This meta-theorem is
formalized in Coq.


\section{Low-Level Programs}

We represent low-level programs as directed graphs with
labelled edges.  The set of graph vertices
$\Vrt$ is left abstract.  Edges of the graphs
are define to be elements of the set
$\Edg := \Vrt \times \act \times \Q \times \Vrt$.
The set $\act$ is the set of program actions, it
can be simply modeled as morphisms on program
states $\State$.

The semantics of programs are defined using a step relation on
configurations $\cnf \state v \in \State \times \Vrt$:
$$
\cnf{\state_1}{v_1} \smallstep_\delta \cnf{\state_2}{v_2}
  \iff
(v_1, f, \delta, v_2) \in E  \land  \state_2 = f(\state_1).
$$
A complete program is pair $(\cnf{\state_0}{v_0}, E \subseteq \Edg)$
of an initial configuration and a set of edges.  A program is
\emph{strongly terminating} if any sequence of steps
from the initial configuration ends on a \emph{final} vertex
of the graph:
A vertex that is at the origin of no edge.
We can formalize this notion in Coq
using the accessibility predicate defined in the
standard library.

\paragraph{Safety.} Using the semantics presented, we can define
when a program configuration $\cnf{\state}{v}$ of a program runs
safely using an amount of resources~$Q$.  We denote this property
as $\safe\state v Q$, and define it inductively as
$$
\forall \state_1\, v_1.\, (\cnf\state v \smallstep_\delta \cnf{\state_1}{v_1}) {\implies}
  Q \ge \delta \land \safe{\state_1}{v_1}{Q-\delta}.
$$
Remark that if the vertex $v$ of a configuration $\cnf\state v$ is
final, safety is vacuously true.  The set of resource amounts
making an initial configuration safe $\mathcal S$ is the set of
valid resource bounds for the program.  We can define the
\emph{resource consumption} of a program as the greatest lower
bound of the set $\mathcal S$.

\paragraph{Potential.} A potential annotation annotates
each vertex $v$ of the low-level program with a potential
function $\Phi_v$ mapping program states to $\Q$.
To be \emph{valid}, a potential annotation is required
to satisfy three conditions.
%
\begin{enumerate}
\item If $v \in \Vrt$ is final,
  $\forall \state,\, \Phi_v(\state) \ge 0$.
\item If $(v_1, f, \delta, v_2) \in E$ and $\delta < 0$,
  then $\forall \state, \Phi_{v_1}(\state) \ge 0$.
\item If $(v_1, f, \delta, v_2) \in E$,
  then $\forall \state, \Phi_{v_1}(\state) \ge \Phi_{v_2}(f(\state)) + \delta$.
\end{enumerate}
%
For programs that only allocate resources, the condition~2 does not
need to be checked.

\begin{theorem}
  \label{thm:pos}
  For any strongly-terminating program $(\cnf\state v, E)$ and
  any valid potential annotation $\Phi$, we have
  $\Phi_v(\state) \ge 0$.
\end{theorem}
\begin{proof}
In Coq, we use induction over the accessibility of the initial
configuration.  Then if the vertex $v$ is final, we conclude
using the condition~1.  If not, depending on the sign of $\delta$
we either use induction with condition~3, or conclude with condition~2
directly.
\end{proof}

\begin{theorem}
  \label{thm:snd}
  For any strongly-terminating program $(\cnf\state v, E)$
  and any valid potential annotation $\Phi$, we have
  $\safe{\state}{v}{\Phi_v(\state)}$.
\end{theorem}
\begin{proof}
By induction on the accessibility, using \pref{thm:pos}
to show the part $Q \ge \delta$ of safety.  A weakening
lemma for safety is also required to get that
$Q' \ge Q \land \safe{\state}{v}{Q} \implies \safe{\state}{v}{Q'}$.
It is proved by induction on the definition of
safety.
\end{proof}

Resource analysis on non-terminating programs can sometimes
be of use, for instance, reactive systems are usually non-terminating
programs.
For these programs, it is sufficient to require that any cycle
in the low-level program graph contains a vertex $v$ where
$\forall \state, \Phi_v(\state) \ge 0$.
With this added requirement, the proof of \pref{thm:snd} can be
adapted to show that the potential function of the initial
vertex is a valid resource bound.  This extra constraint can
always be safely used, but it can lead to loser bounds when
we feed it to the LP~solver.


\section{Canonical Polynomial Potential}

The following presentation of amortized analysis for resource
inference on integer programs permits to obtain precise polynomial
bounds by naturally extending the previous linear work. Innovations
of this presentation include
\begin{enumerate}
\item the use of canonical polynoms $X^i$ at no cost on precision,
 \\ (I wish)
\item the use of negative coefficients in potential annotations,
\item the support for operations with mixed effects on multivariate potential.
\end{enumerate}

\paragraph{Index Sets}

Let $V$ be a set of variables.  An \emph{index} $I \in \ind(V)$ is a
family that maps pairs of variables to non-zero natural numbers,
$$
I = (i_{(x,y)})_{(x,y) \in V^2} .
$$
%
We identify a family $I$ with the set of pairs $\{ ((x,y),i_{(x,y)})
\mid (x,y) \in V^2\}$.
Let $\ind(V)$ denote the set of all such indices.  We write $\ind$
instead of $\ind(V)$ if the set of variables $V$ is fixed or obvious
from the context.
%

The \emph{degree} of an index $I = (i_{(x,y)})$
is defined by
$
\deg(I) = \sum_{(x,y)} i_{(x,y)}.
$
We define $\ind_k(V) = \{ I \in \ind(V) \mid \deg(I) \leq k
\}$ to be the set of indices of degree at most $k$.  Remark
that with these notations, $\ind_0(V)$ for any $V$ is a
singleton---it contains only the empty index.

\paragraph{Resource Polynomials}

Let $V$ be a set of variabls.  An index $I \in \ind(V)$ denotes a
\emph{base polynomial} $P_I : \State \to \Q$ that maps a program
state $\state$ to a rational number.  The definition of $P_I$ is
$
P_I(\state) = \prod_{(x,y)} |[\state(x),\state(y)]|^{i_{(x,y)}}.
$
Remark that following the standard convention for $\prod$, the
empty index represents the constant base polynomial 1.  We will
later use the notation $P_{xy}(\state) = |[\state(x),\state(y)]|$
to define $P_I$ as $P_I = \prod_{(x,y)} P_{xy}$.

A \emph{resource polynomial} is a linear combination of
base polynomials with rational coefficients.  Resource polynomials
form a vector space over $\Q$.

\paragraph{Potential Annotations}

We call \emph{potential annotations}
the coordinates of a resource polynomial in the basis of
all base polynomials.  An annotation $Q$ is readily represented
by a collection $(q_I)_I$ binding rational numbers to indices.
For example, the potential annotation $\{\{((x,y),2)\} \mapsto 0.5,
\emptyset \mapsto 3\}$ specifies the resource polynomial
$
  P_Q(\state) = 0.5\cdot|[\state(x),\state(y)]|^2 + 3.
$

The notion of degree can be generalized to potential annotations:
the annotation $Q = (q_I)_I$ has degree $\max_{q_I} \deg(I)$.
Remark that the degree of an annotation is exactly the degree of
the polynomial it represents.

\paragraph{Potential Method for Resource Analysis}

The previous potential annotations will be used to decorate
programs and bound their resource consumption.  A program
$C$ consumes $n$ resource units turning a state $\state$ into $\state'$,
we note this $\state \rightarrow^n_C \state'$.  The \emph{potential
method} make us look for two annotations $Q$ and $Q'$ such
that
$$
  \forall n\, \state\, \state'.\, \state \rightarrow^n_C \state'
    \implies P_Q(\state) \ge n + P_{Q'}(\state').
$$
The composition of these annotations through the whole program
using a quantitative logic permits to derive a resource bound.
In the sequel we explicit a relation that is sufficient to
satisfy the previous condition when the program $C$ is an
increment operation $x \gets x+y$.

\paragraph{Shifts of Resource Polynomials}

By symmetry we can consider the case where $C=x \gets x+y$ with
$y>0$, the case where $y \le 0$ is only a few signs away.  Let
$Q$ be a potential annotation, we will describe a $Q'$ and a
$P^y_.$ map such that if $\state \rightarrow_C \state'$ (with no resource cost),
$P_Q(\state) = P^y_{Q'}(\state')$.  We call $Q'$ a shift of $Q$ and
write $Q' = \qsh_x^+ Q$.  (When $y\le0$ we get $\qsh_x^-Q$.)

The shift of $Q$ is defined on an extended set of indices, namely
$\ind^\square = \ind(V \cup \{\square\})$.  This square is not a real
variable, but a helper with special semantics.
We can now pose $\qsh_x^+ Q = (q'_I)_{I\in\ind^\square}$ where,

\begin{align*}
q'_I =
q_{I[\square \gets x]}
\prod_z
   \binom{i_{(\square,z)} {+} i_{(x,z)}}{i_{(\square,z)}}
   \binom{i_{(z,\square)} {+} i_{(z,x)}}{i_{(z,\square)}}
   (-1)^{i_{(z,\square)}}
   .
\end{align*}

The substitution operation $I[\square \gets x]$ defines an index $J$
in $\ind(V)$ with the same degree as $I$.  This index satisfies
$$
j_{(x,z)} {=} i_{(x,z)} {+} i_{(\square,z)}, \;
j_{(z,x)} {=} i_{(z,x)} {+} i_{(z,\square)}, \;
j_{(u,v)} {=} i_{(u,v)} \mbox{ o.w.}
$$
Notations may seem heavy, but what they really express is that
replacing $\square$ by $x$ in $x^2\square^3z^2$ yields $x^5z^2$.

We now define an interpretation $P_.^y$ of indices containing
$\square$:
\begin{align*}
P^y_{\square z}(\state) &=
  \left| [\sigma(x){+}\sigma(y), \sigma(z)] \,\triangle\,
         [\sigma(x), \sigma(z)] \right| \\
P^y_{z \square}(\state) &=
  \left| [\sigma(z), \sigma(x){+}\sigma(y)] \,\triangle\,
         [\sigma(z), \sigma(x)] \right| \\
P^y_{\square \square}(\state) &= P_{x \square}(\state)
  = P_{\square x}(\state) = 0 \\
P^y_{uv}(\state) &= |[\sigma(u), \sigma(v)]| \mbox{ otherwise},
\end{align*}
we use $A \,\triangle\, B$ to denote the symmetric difference
of $A$ and $B$.
The quantity $P^y_{\square z}(\state)$ is the size change of
the interval $[x, z]$.  If $\state$ is the state before the
assignment and $\state'$ is the state after the assignment, we
have
$P_{xz}(\state) = P^y_{xz}(\state') + P^y_{\square z}(\state')$
and
$P_{zx}(\state) = P^y_{zx}(\state') - P^y_{z \square}(\state')$.
With these definitions, we have the following lemma.
\begin{lemma}
If $\state \rightarrow_C \state'$ and $\state(y)>0$ then
$P_Q(\state) = P^y_{\qsh^+_x Q}(\state')$.
\end{lemma}
\begin{proof}
\small
\begin{align*}
&P^y_{\qsh_x^+ Q}(\state')
= \sum_I q'_I \prod_{(u,v)} P_{uv}^{uv} \\
&= \sum_I q_{I[\square\gets x]} X_I \prod_z
  \binom{\square z {+} xz}{\square z}P_{\square z}^{\square z} P_{xz}^{xz}
  \binom{z\! \square\! {+} zx}{z \square}(-P_{z \square})^{z \square} P_{zx}^{zx} \\
&= \sum_J q_J X_J \sum_{I[\square\gets x] = J} \prod_z
  \binom{\square z {+} xz}{\square z}P_{\square z}^{\square z} P_{xz}^{xz}
  \binom{z\! \square\! {+} zx}{z \square}(-P_{z \square})^{z \square} P_{zx}^{zx} \\
&= \sum_J q_J X_J \prod_z
  \left( \sum_{\square z + xz = j_{xz}}
    \binom{\square z {+} xz}{\square z}P_{\square z}^{\square z} P_{xz}^{xz} \right)
  \left( \sum_{z\square {+} zx = j_{zx}} \dots \right) \\
&= \sum_J q_J X_J \prod_z
  (P_{xz} + P_{\square z})^{j_{xz}}
  (P_{zx} - P_{z \square})^{j_{zx}} \\
&= \sum_J q_J P_J(\state) = P_Q(\state)
\end{align*}
\end{proof}

\paragraph{Projection of Resource Polynomials}

\DeclareGraphicsRule{*}{mps}{*}{}

The shift operation perserves all the potential after an increment
but it introduces a new dummy variable $\square$.  Because annotations
need to be uniform for compositionality, we present in this paragraph
a projection that eliminates this extra variable.  The main identity that
we use is $P_{\square z}(\state) + P_{z \square}(\state) =
P_{0y}(\state)$.  It can be checked on all the three cases illustrated
below.
$$
\includegraphics{fig/ivals.1}
$$
In the first case, $P_{\square z}$ will be 0 and $P_{z \square}$ will
be non zero; the third case witnesses the opposite situation; and in
the second case, both are non-zero.

Given an index I from $\ind(V\cup \{ \square \})$, we define its projection
$J = I|_{0y} \in \ind(V)$ over the interval $[0,y]$ as
$$
j_{0y} = i_{0y} + \sum_{z \in V} i_{\square z} + i_{z \square}, \quad
j_{uv} = i_{uv} \mbox{ o.w.}
$$
Once again this is a degree preserving transformation.  We use it to
relate indices containing $P_{0y}^k$ and its possible \emph{developments}
in terms of $P_{\square z}$ and $P_{z \square}$.  A development gives a
possible rewrite of indices that contain the base polynomial $
|[0,y]|^k$ where k is non-zero.  Formally, it is a pair $\delta =
(\delta_0, \delta_m)$ of a natural number $\delta_0$ and a map $\delta_m$
from program variables to natural numbers such that $\delta_m(x) = 0$.
A development $\delta$ has degree $\delta_0 + \sum_z \delta_m(z)$.  We
will write $\Delta(J)$ for the set of all developments that have degree
$j_{0y}$.  We will also use the shorter functional notation $\delta(z)$
to denote $\delta_m(z)$.

To see the action of a development on an index, consider the
index $J = |[0,y]|^2$, the development $\delta = (2, \_ \mapsto 0)$
is in $\Delta(J)$ and transforms $J$ into itself.  The development
$\delta' = (1, \{ z \mapsto 1, \_ \mapsto 0\})$ is also into $\Delta(J)$ and
transforms $J$ into the resource polynomial
$|[0,y]|P_{\square z} + |[0,y]|P_{z \square}$.

If $Q$ is a resource polynomial on the index set $\ind(V\cup \{\square\})$ we
can now define the projection $Q' = Q|_{0y} \in \ind(V)$ as
$$
q'_J = \sum_{\delta \in \Delta(J)} q^\delta_J,
$$
where the numbers $q^\delta_J$ are constrained to satisfy the following
family of equations
$$
q_I = q^\delta_{I|_{0y}} \prod_z \binom{i_{\square z} + i_{z \square}}{i_{\square z}}.
$$

\begin{lemma}
If $Q \in \ind(V \cup \{\square\})$, then for all $\state$,
$P^y_Q(\state) = P_{Q|_{0y}}(\state)$.
\end{lemma}
\begin{proof}
\begin{align*}
&P_{Q|_{0y}}(\state)
  = \sum_J q_J P_J(\state)
  = \sum_J X_J \sum_{\delta \in \Delta(J)} q_J^\delta P_{0y}^{0y} \\
&= \sum_J X_J \sum_{\delta \in \Delta(J)}
    q_J^\delta P_{0y}^{\delta_0}
    \prod_z (P_{\square z} + P_{z \square})^{\delta(z)} \\
&= \sum_J X_J \sum_{\delta \in \Delta(J)}
    q_J^\delta P_{0y}^{\delta_0}
    \prod_z \sum_{i+j=\delta(z)} \binom{\delta(z)}{i}
      P_{\square z}^i P_{z \square}^j \\
&= \sum_J \sum_{I|_{0y} = J}
    q_J^{\delta_I} X_J P_{0y}^{i_{0y}}
    \prod_z \binom{i_{\square z} + i_{z \square}}{i_{\square z}}
      P_{\square z}^{i_{\square z}} P_{z \square}^{i_{z \square}} \\
&= \sum_I
    \left( q_{I|_{0y}}^{\delta_I}
    \prod_z \binom{i_{\square z} + i_{z \square}}{i_{\square z}}
    \right) P_I^y
  = \sum_I q_I P_I^y = P^y_Q(\state).
\end{align*}
\end{proof}














\clearpage
\section{Binomial Polynomial Potential}

This section presents the binomial version of the previous system.
In practice, negative coefficients could be enough to avoid having to use
this basis.  I also suspect that there is no significant simplifications
in the presentation using the binomial basis.

\paragraph{Index Sets}

Let $V$ be a set of variables.  An \emph{index} $I \in \ind(V)$ is a
family that maps two-element sets of variables to natural numbers,
that is,
$$
I = (i_{\{x,y\}})_{\{x,y\} \subseteq V} \; .
$$
%
We identify a family $I$ with the set $\{ (\{x,y\},i_{\{x,y\}})
\mid \{x,y\} \subseteq V\}$.

Let $\ind(V)$ denote the set of all such indices.  We write $\ind$
instead of $\ind(V)$ if the set of variables $V$ is fixed or obvious
from the context.
%
We assume that allways $0 \in V$ and sometimes write $i_x$ instead of $i_{\{x,0\}}$.

The \emph{degree} $\deg(I)$ of an index $I = (i_{\{x,y\}})_{\{x,y\}
  \subseteq V}$ is defined as
$$
\deg(I) = \sum_{\{x,y\} \in V} i_{\{x,y\}} \;.
$$
We define $\ind_k(V) = \{ I \mid I \in \ind(V) \text{ and } \deg(i) \leq k
\}$ to be the set of indices of degree at most $k$.

\paragraph{Resource Polynomials}

Let $V$ be a set of variables.  An index $I \in \ind(V)$ denotes a
\emph{base polynomial} $P_I : \states \to \N$ for $V$ that maps a
program state $H$ to product of binomial coefficients (a natural
number).  We define
$$
P_I(H) = \prod_{{\{x,y\}} \subseteq V} \binom {|H(x){-}H(y)|} {i_{\{x,y\}}} \; .
$$
%
A \emph{resource polynomial} $R$ for the variable set $V$ is a
non-negative linear combination of the base polynomials for $V$.

\paragraph{Potential Annotations}

A \emph{potential annotation} for the variable set $V$ is a family
$$Q = (q_I)_{I \in \ind(V)}$$
of non-negative rational numbers.  Such an annotation denotes the
resource polynomial $R_Q$ that is defined by
$$
R_Q(H) = \sum_{I \in \ind(V)} q_I \cdot P_I(H) \; .
$$
%
We say that the potential annotation $Q$ is of degree $k$ if $q_I = 0$
for $I \in \ind(V)$ with $\deg(I) > k$.

\paragraph{Additive Shifts}

Let $Q$ be a potential annotation for a variable set $V$ and let
$\{x,y\} \subseteq V$ be a two-element variable set.  The
\emph{additive shift} with respect to $\{x,y\}$ is a potential
annotation $\shift_{\{x,y\}}(Q) = (q'_I)_{I \in \ind(V)} $ for $V$
that is defined through
$$
q'_I = q_I + q_{I^{\{x,y\}{+}1}} \; .
$$
For an index $I = (i_{\{x,y\}})_{\{x,y\} \subseteq V}$ we use the
notation $I^{\{x,y\}{+}k}$ to denote the index
$(i'_{\{x,y\}})_{\{x,y\} \subseteq V}$ such that
$$
i'_{\{t,u\}} = \left\{
  \begin{array}{ll}
    i_{\{t,u\}} + k  & \text{if } \{t,u\} = \{x,y\} \\
    i_{\{t,u\}} & \text{otherwise}
  \end{array}
\right.
\;.
$$
%
The additive shift for natural numbers reflects the identity
\begin{equation}
\label{eq:shift}
\sum_{0 {\leq} i \leq {k}} q_i \binom{n+1}{i} = \sum_{0 {\leq} i \leq {k}} (q_i{+}q_{i+1}) \binom{n}{i}
\end{equation}
where $q_{k+1} = 0$.  It is used in the effect system if the
difference $n+1$ between two variables $x,y$ decreases by one.

\begin{lemma} Let $V$ be a set of variables with $x,y \in V$ and let
  $H$ be a program state. Let $|H'(t) {-} H'(u)| = |H(t) {-} H(u)|$
  for $\{t,u\} \neq \{x,y\}$ and let $|H'(x) {-} H'(y)| = |H(x) {-}
  H(y)| - 1$.
  %
  If $Q' = \shift_{\{x,y\}}(Q)$ then $R_Q(H) = R_{Q'}(H')$.
\end{lemma}

We now study the effect of multiple simultaneous shifts.  Let $Q$ be a
resource annotation for a variable set $V$ and let $U_1,\ldots,U_n
\subseteq V$ with $|U_i| = 2$ for all $i$ and $U_i \neq U_j$ for $i
\neq j$ be pairwise distinct two-element variable sets.  The
simulations additive shift $\shift_{U_1,\ldots,U_n}(Q)$ of $Q$ with
respect to $U_1,\ldots,U_n$ is defined by
$$
\shift_{U_1,\ldots,U_n}(Q) = \shift_{U_1}( \cdots \shift_{U_n}(Q) \cdots ) \; .
$$
%
\begin{proposition}
  Let $V$ be a set of variables and let $U_1,\ldots,U_n$ be pairwise
  distinct two-element variable sets.  Let $|H'(x) {-} H'(y)| = |H(x)
  {-} H(y)|$ for $\{x,y\} \not\in \{U_1,\ldots,U_n\}$ and let $|H'(x)
  {-} H'(y)| = |H(x) {-} H(y)| - 1$ for $\{x,y\} \in
  \{U_1,\ldots,U_n\}$.
  %
  If $Q' = \shift_{\{U_1,\ldots,U_n\}}(Q)$ then $R_Q(H) = R_{Q'}(H')$.
\end{proposition}
%
As shown by the following lemma, the order in which the shifts for the
individual $U_i$ are applied is insignificant.
%
\begin{lemma}
  Let $\sigma : \{1,\ldots,n\} \to \{1,\ldots,n\}$ be a
  permutation. Then $\shift_{U_1,\ldots,U_n}(Q) =
  \shift_{U_{\sigma(1)},\ldots,U_{\sigma(n)}}(Q)$.
\end{lemma}
%
For reasons of efficiency in the constraint generation, we give a more
direct formula for the simultaneous shift.  Let $I \in \ind(V)$ and
let $U_1,\ldots,U_n$ be pairwise distinct two-element variable sets.
We define the index $I^{U_1,\ldots,U_n + k}$ as the family $(i'_{\{x,y\}})_{\{x,y\} \subseteq V}$ such that
$$
i'_{\{t,u\}} = \left\{
  \begin{array}{ll}
    i_{\{t,u\}} + k  & \text{if } \{t,u\} \in \{U_1,\ldots,U_n\} \\
    i_{\{t,u\}} & \text{otherwise}
  \end{array}
\right.  \;.
$$

%
\begin{lemma}
  Let $V$ be a variable set and let $U_1,\ldots,U_n$ be pairwise
  distinct two-element variable sets.
  %
  Let $Q = (q_I)_{I \in \ind(V)}$ be a resource annotation for
  $V$ and let $ Q' = (q'_I)_{I \in \ind(V)}$ where
  $$
  q'_I = \sum_{\{j_1,\ldots,j_m\} \subseteq \{1,\ldots,n\} } q_{I^{U_{j_1},\ldots,U_{j_m}+1}} \; .
  $$
  Then $Q' = \shift_{U_1,\ldots,U_n}(Q)$.
\end{lemma}

\subsection{Binomial basis}

\begin{lemma}
  There exists a family $(c^{ij}_k)_k$, such that
  $$
  \sum_k c^{ij}_k \binom n k = \binom n i \binom n j,
  $$
  and $c^{ij}_k = \binom k j \binom j {i+j - k}$ satisfies
  the previous equation.
\end{lemma}
\begin{proof}
  \begin{align*}
    \binom n i \binom n j
      &= \sum_k \binom {n-j} k \binom j {i-k} \binom n j \\
      &= \sum_k \binom {n-j} {k-j} \binom n j \binom j {i+j-k} \\
      &= \sum_k \binom n k \binom k j \binom j {i+j-k}.
  \end{align*}
  In the first equality, we use Vandermonde's convolution
  formula on $\binom n i$.  In the second equality we change
  the summation variable to $k-j$.  And in the third equation
  we use the identity proved below.
  \begin{align*}
    \binom {n-j} {k-j} \binom n j
      &= \frac {(n-j)!} {(n-k)! (k-j)!} \; \frac {n!} {(n-j)! j!} \\
      &= \frac {n!} {(n-k)! (k-j)! j!} \\
      &= \frac {n!} {(n-k)! k!} \; \frac {k!} {(k-j)! j!} \\
      &= \binom n k \binom k j.
  \end{align*}
\end{proof}



%%
% Note: Later we need to shift in many directions at once like
%   Q' = shift_{x,y} (shift_{x,u} (Q))
% To do: Give a combined formula for that (concise constraint system).
%%

\end{document}