%% LyX 2.2.1 created this file.  For more info, see http://www.lyx.org/.
%% Do not edit unless you really know what you are doing.
\documentclass[english]{beamer}
\usepackage{mathptmx}
\usepackage[T1]{fontenc}
\usepackage[latin9]{inputenc}
\setcounter{secnumdepth}{3}
\usepackage{verbatim}
\usepackage{mathtools}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{setspace}
\usepackage{xargs}[2008/03/08]
\setstretch{0.8}

\makeatletter
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Textclass specific LaTeX commands.
 % this default might be overridden by plain title style
 \newcommand\makebeamertitle{\frame{\maketitle}}%
 % (ERT) argument for the TOC
 \AtBeginDocument{%
   \let\origtableofcontents=\tableofcontents
   \def\tableofcontents{\@ifnextchar[{\origtableofcontents}{\gobbletableofcontents}}
   \def\gobbletableofcontents#1{\origtableofcontents}
 }

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% User specified LaTeX commands.
\def\unq@#1=00#2#3#4#5#6&#7&#8&{\csname#4#5\endcsname#6&#7#1&#8&}
\def\def@#1#2#3{\expandafter\def\csname#1#2\endcsname#3}
\def\?#1#2#3{\def@#1#2{##1&##2&##3&{\unq@##1&#3&}}}
\?10{#2\text{-}&#3}
\?23{#2\#&#3}
\?25{#2\%&#3}
\?3D{#2=&#3}
\?5B{#2[&#3}
\?5D{#2]&#3}
\?7B{&#2&#3}
\?7D{#3{#2}}
\?C4{#2\"A&#3}
\?D6{#2\"O&#3}
\?E4{#2\"a&#3}
\?F6{#2\"o&#3}
\def@00{&#1&&{#1}}
\def@24{#1 #2&#3&{\expandafter\rec@\csname#1\endcsname#2&#3&}}
\def\rec@#1#2&#3&{\unq@#2&#3#1&}
\def\label@in@display#1{\tag*{{\large$\scriptstyle(\unq@#1 =000000&&&)$}}\gdef\df@label{#1}}

\delimiterfactor=547
\delimitershortfall=99pt
\let\oldleft\left
\let\oldright\right 
\def\left{\mathopen{}\mathclose\bgroup\oldleft}
\def\right{\aftergroup\egroup\oldright}

\usepackage{graphicx}
\usepackage{xcolor}
\usepackage{hyperref}
\usepackage[mathcal]{euscript}
%Dioihin
\usepackage{setspace}
\let\hbar\undefined
\beamertemplatenavigationsymbolsempty
\setbeamertemplate{footline}[frame number]

\makeatother

\usepackage{babel}
\begin{document}
\noindent\begin{minipage}[t]{1\columnwidth}%
\global\let \oldquad\quad
\global\let \oldqquad\qquad

\global\long\def\skip{}
\global\long\def\s{\ }
\global\long\def\quad{\oldquad}
\global\long\def\qquad{\oldqquad}

\global\long\def\veny#1#2#3{\text{{\scalebox{#3}[#2]{\ensuremath{#1}}}}}

\global\long\def\nouse#1#2{\raisebox{#2ex}{\ensuremath{#1}}}

\global\long\def\makeop#1{\operatorname{#1}}

\global\long\def\makelim#1#2{\operatorname*{#1}\limits _{#2}}

\global\long\def\back#1{\hspace{-#1em}}

\newcommandx\integ[2][usedefault, addprefix=\global, 1=\skip]{\int_{#2}^{#1}\negthickspace}

\global\long\def\set#1#2{\left\{  #1\,\vphantom{\overset{o}{O}}\middle|\,#2\right\}  }

\global\long\def\url#1{\text{\href{#1}{#1}}}

\global\long\def\seq#1{\vec{#1}}
\global\long\def\tuple#1{\vec{#1}}

\global\long\def\simprule#1#2{\begin{array}{c}
 \negthickspace#1\negthickspace\\
\hline\hline  \negthickspace#2\negthickspace
\end{array}}
\global\long\def\holdsIn{\mathrel{\veny{\models}1{-1}}}

\global\long\def\tihkutaulu{\setlength\arraycolsep{0pt}}

\global\long\def\vaihda#1#2#3{{\alt<#2->{#3}{\mathrlap{#1}\phantom{#3}}}}
%pitenee

\global\long\def\vaihdaa#1#2#3{{\alt<#2->{\mathrlap{#3}\phantom{#1}}{#1}}}
%lyhenee

\global\long\def\vaihdax#1#2#3{{\alt<#2->{#3}{\phantom{#3}\mathllap{#1}}}}
%vasen pitenee

\global\long\def\Vaihda#1#2#3{{\alt<#2->{#3}{\mathrlap{#1}\phantom{#3}}}}
%suurenee

\global\long\def\erotuA#1#2{{\alt<#2>{\color{red}#1}{#1}}}
\begin{comment}
\textcolor{red}{Punakorostus}
\end{comment}

\global\long\def\erotuB#1#2{{\alt<#2>{\color{blue}#1}{#1}}}
\begin{comment}
\textcolor{blue}{Sinikorostus}
\end{comment}
%
\end{minipage}

\linespread{1.3}\selectfont{}\let\overrightarrow\vec

\global\long\def\sulut#1{\left(#1\right)}

\newcommandx\Sum[2][usedefault, addprefix=\global, 1=n\text{=}0, 2=m]{\mathchoice{{\textstyle \sum\limits _{#1}^{#2}}\skip}{{\textstyle \mathop{\overset{#2}{\underset{#1}{\Sigma}}}}\skip}{{\textstyle \mathop{\overset{#2}{\underset{#1}{\Sigma}}}}\skip}{{\scriptstyle \mathop{\overset{#2}{\underset{#1}{\Sigma}}}}\skip}}

\global\long\def\GeneralizeTransitions#1#2#3{\vaihdaa{#1}4{\vaihda{\:\phantom{#3}#2}5{\vaihda{#1}6{\phantom{#3}\vaihda{\#f}7{\s s}}}}}

$\mathrlap{}$

\title{{\Large{}Recurrence-Driven Summations}\\
{\Large{}in Automated Deduction}}

\author{$\begin{array}{l}
\text{Visa Nummelin}\\
{\scriptstyle \text{Joint work with Jasmin Blanchette and Sander R. Dahmen}}
\end{array}$}

\date{FroCoS 2023\\
21\textsuperscript{st} September}
\makebeamertitle
\begin{frame}{Questions of interest}
\begin{itemize}[<+->]
\item Prove equations between summation expressions
\item Integrate the heuristic to an automatic base prover (in theory)
\item $\Sum n2^{n}=\left(m-1\right)2^{m}+1\qquad\qquad\Sum n^{3}=\sulut{\Sum n}^{2}$\alt<3>{\\
Arithmetic and induction are in the heart of the tasks} 
\item $\sulut{x+y}^{m}=\Sum\binom{m}{n}x^{n}y^{m-n}\qquad\qquad\binom{x+y}{m}=\Sum\binom{x}{n}\binom{y}{m-n}$\alt<4>{\\
Theory of holonomic formulas provides ground work} 
\item $\sulut{x+y}^{m}=\Sum\binom{m}{n}x\sulut{x-n}^{n-1}\sulut{y+n}^{m-n}$\alt<5>{\\
Beyond holonomic: demand less recurrences} 
\item $\Sum f_{m-n}=\Sum f_{n}\qquad\qquad\Sum\Sum[k=0][n]f_{n,k}=\Sum[k=0]\Sum[n=k]f_{n,k}$\alt<6>{\\
Beyond holonomic: allow heterogeneous recurrences} 
\end{itemize}
\end{frame}
%
\begin{frame}{Source of recurrences}

Summation $\Sum a_{n}=:g_{m}$ can be defined by
\begin{itemize}
\item the base case $g_{0}=a_{0}$; and
\item the recurrence equation $g_{m+1}=g_{m}+a_{m+1}$
\end{itemize}
Recurrences are useful to define other sequences too
\begin{itemize}[<+(1)->]
\item exponential: $b^{n+1}=b\cdot b^{n}$ \alt<2>{with base case $b^{0}=1$}~
\item Fibonacci: $F_{n+2}=F_{n+1}+F_{n}$ \alt<3>{with base cases $F_{0}=0$,
$F_{1}=1$}~
\item factorial: $\sulut{n+1}!=\sulut{n+1}\cdot n!$ \alt<4>{with base
case $0!=1$}~
\item binomial coefficient: for $\binom{m}{n}=\frac{m!}{n!\sulut{m-n}!}$
holds\\
 $\binom{m+1}{n}=\frac{m+1}{m-n+1}\binom{m}{n}\quad\text{and}\quad\binom{m}{n+1}=\frac{m-n}{n+1}\binom{m}{n}$
\item polynomial $P$: if $d=\makeop{deg}P+1$ then for all $n$\\
 $P\sulut{n+d}+...+\sulut{-1}^{d-j}\binom{d}{j}P\sulut{n+j}+...+\sulut{-1}^{d}P\sulut n=0$
\end{itemize}
\end{frame}
%
\begin{frame}{Application of recurrences}
\begin{itemize}
\item Our recurrences are linear, finite in length and\\
have polynomial coefficients
\item<2-> To prove equation $f_{n}=0$ for $n\in\mathbb{N}$, it suffices to
find\\
- recurrence $c_{n,}{}_{d}f_{n+d}=c_{n,}{}_{d-1}f_{n+d-1}+...+c_{n,}{}_{0}f_{n}$;
and\\
- prove base cases $f_{0}=...=f_{d-1}=0$ and $\exists c_{n,d}^{-1}$
\item<3-> \global\long\def\plusplus{+\negthickspace...\negthickspace+}
$\Vaihda{f_{\vaihda d4{d+1}}=c_{\vaihda 041,d}^{-1}\sulut{c_{\vaihda 041,d-1}f_{\vaihdaa{d-1}4d}\plusplus c_{\vaihda 041,0}f_{\vaihdaa 041}}=c_{\vaihda 041,d}^{-1}\sulut{0\plusplus0}=0}5{+,\cdot,\Sigma\text{ and substitutions build expressions}}$
\item<6-> Example decomposition: $\vaihdaa{\erotuA{\Sum a_{m-n}}8}9{\qquad C_{m}}\s\vaihda =7{\vaihda{\erotuB -8}9+}\s\vaihda{\erotuB{g_{m}}8}9{G_{m}}\vaihda{}7{{}=0}$\\
$\vaihda{}9{G_{m}=\vaihdaa{\erotuA -{10}\erotuB{g_{m}}{10}}{11}{\sulut{-1}\cdot g_{m}}}$\\
$\vaihda{}9{C_{m}=\Sum\vaihda{\erotuA{a_{m-n}}{12}}{13}{B_{m}^{n}}}$\\
$\vaihda{}{13}{B_{m}^{n}=\vaihda{a_{\erotuA{m-n}{14}}}{15}{\left\{ k\mapsto m-n\right\} a_{k}}}$
\end{itemize}
\end{frame}
%
\begin{frame}{Example (recurrence derivation)}
\begin{itemize}
\item Key idea: From recurrences of sequences $f_{m}^{n}$ and $h_{m}^{n}$\\
derive recurrences for $f_{m}^{n}+h_{m}^{n}$ , $f_{m}^{n}h_{m}^{n}$
, $\Sum f_{m}^{n}$ , $f_{\gamma n+\delta m}^{\alpha n+\beta m}$\\
 
\item Let $g_{0}=a_{0}$, $g_{1}=a_{0}+a_{1}$, $\erotuA{g_{m+2}=g_{m}+a_{m+1}+a_{m+2}}2$
\item Claim $\Sum a_{m-n}=g_{m}$ for $m\geq0$
\item<2-> Take $\erotuA{\text{one}}2$ recurrence for $g$ and none for $a$
\item<3-> Recurrence of $B_{m}^{n}:=a_{m-n}$ is $B_{m+1}^{n+1}=B_{m}^{n}$\\
because $\left(m+1\right)-\left(n+1\right)=m-n$
\end{itemize}
\end{frame}
%
\begin{frame}{Example (recurrence of $C_{m}:=\Sum B_{m}^{n}$)}
\begin{itemize}
\item Next consider the sequence $C_{m}:=\Sum B_{m}^{n}=\Sum a_{m-n}$
\item To normalize indices, for any sequence $f$ we have 
\begin{align*}
{\textstyle \Sum}f_{j}^{n+1} & ={\textstyle \Sum}f_{j}^{n}+f_{j}^{m+1}-f_{j}^{0}\\
{\textstyle \Sum}f_{m+1}^{n} & =\left\{ m\mapsto m+1\right\} \left({\textstyle \Sum}f_{m}^{n}-f_{m}^{m}\right)
\end{align*}
\item<2-> Apply these to $0=\Sum\left(B_{m+1}^{n+1}-B_{m}^{n}\right)=\Sum B_{m+1}^{n+1}-C_{m}\vaihda{}3=$
\[
\tihkutaulu\smash{\begin{array}{lll}
 & \phantom{\Sum}\\
\vaihda{}3{{}=\Sum B_{m+1}^{n}} & \vaihda{}3{{}+B_{m+1}^{m+1}-B_{m+1}^{0}} & \vaihda{}3{{}-C_{m}}\vaihda{}4{{}=}\\
\vaihda{}4{{}=\Sum[][m+1]B_{m+1}^{n}-B_{m+1}^{m+1}} & \vaihda{}4{{}+B_{m+1}^{m+1}-a_{m+1-0}} & \vaihda{}4{{}-C_{m}}\vaihda{}5{{}=}\\
\vaihda{}5{\mathrlap{{}=C_{m+1}-a_{m+1}-C_{m}}}
\end{array}}
\]
\end{itemize}
\end{frame}
%
\begin{frame}{Example (recurrence of $D_{m}:=C_{m}-g_{m}$)}

To find recurrences of $D_{m}:=C_{m}-g_{m}$, use term ordering s.t.
$D\prec C,g$ and derive consequences from known recurrences:

$\hspace{3em}\begin{aligned}C_{m+1} & =C_{m}+a_{m+1} & \hspace{4.5em}\sulut{\alpha_{m}}\\
g_{m} & =C_{m}-D_{m} & \sulut{\beta_{m}}
\end{aligned}
$

$\back 2\Vaihda{\begin{array}{lll}
 & g_{m+2}=g_{m}+a_{m+2}+a_{m+1} & \sulut{\gamma_{m}}\\
\phantom{-\quad} & \vaihda{}2{g_{m+2}=C_{m+2}-D_{m+2}} & \vaihda{}2{\sulut{\beta_{m+2}}}\\
 & \phantom{C_{m+2}=g_{m}+a_{m+2}+a_{m+1}+D_{m+2}}\\
\\
\\
\\
\\
\\
\\
\end{array}}3{\Vaihda{\begin{array}{lll}
 & g_{m+2}=\erotuA{g_{m}+a_{m+2}+a_{m+1}}3 & \sulut{\gamma_{m}}\\
-\quad & g_{m+2}=\erotuB{C_{m+2}-D_{m+2}}3 & \sulut{\beta_{m+2}}\\
\hline  & \erotuB{C_{m+2}}3=\erotuA{g_{m}+a_{m+2}+a_{m+1}}3+\erotuB{D_{m+2}}3\\
 & \vaihda{}4{C_{m+2}=C_{m+1}+a_{m+2}} & \vaihda{}4{\sulut{\alpha_{m+1}}}\\
\\
\\
\\
\\
\\
\end{array}}5{\Vaihda{\begin{array}{lll}
 & g_{m+2}=g_{m}+a_{m+2}+a_{m+1} & \sulut{\gamma_{m}}\\
-\quad & g_{m+2}=C_{m+2}-D_{m+2} & \sulut{\beta_{m+2}}\\
\hline  & C_{m+2}=\erotuA{g_{m}}5+a_{m+2}+\erotuA{a_{m+1}+D_{m+2}}5\\
- & C_{m+2}=\erotuB{C_{m+1}}5+a_{m+2} & \sulut{\alpha_{m+1}}\\
\hline  & \erotuB{C_{m+1}}5=\erotuA{g_{m}+a_{m+1}+D_{m+2}}5\\
 & \vaihda{}6{C_{m+1}=C_{m}+a_{m+1}} & \vaihda{}6{\sulut{\alpha_{m}}}\\
\\
\\
\\
\end{array}}7{\Vaihda{\begin{array}{lll}
 & g_{m+2}=g_{m}+a_{m+2}+a_{m+1} & \sulut{\gamma_{m}}\\
-\quad & g_{m+2}=C_{m+2}-D_{m+2} & \sulut{\beta_{m+2}}\\
\hline  & C_{m+2}=g_{m}+a_{m+2}+a_{m+1}+D_{m+2}\\
- & C_{m+2}=C_{m+1}+a_{m+2} & \sulut{\alpha_{m+1}}\\
\hline  & C_{m+1}=\erotuA{g_{m}}7+a_{m+1}+\erotuA{D_{m+2}}7\\
- & C_{m+1}=\erotuB{C_{m}}7+a_{m+1} & \sulut{\alpha_{m}}\\
\hline  & \erotuA{g_{m}}7=\erotuB{C_{m}}7-\erotuA{D_{m+2}}7\\
 & \vaihda{}8{g_{m}=C_{m}-D_{m}} & \vaihda{}8{\sulut{\beta_{m}}}\\
\\
\end{array}}9{\begin{array}{lll}
 & g_{m+2}=g_{m}+a_{m+2}+a_{m+1} & \sulut{\gamma_{m}}\\
-\quad & g_{m+2}=C_{m+2}-D_{m+2} & \sulut{\beta_{m+2}}\\
\hline  & C_{m+2}=g_{m}+a_{m+2}+a_{m+1}+D_{m+2}\\
- & C_{m+2}=C_{m+1}+a_{m+2} & \sulut{\alpha_{m+1}}\\
\hline  & C_{m+1}=g_{m}+a_{m+1}+D_{m+2}\\
- & C_{m+1}=C_{m}+a_{m+1} & \sulut{\alpha_{m}}\\
\hline  & g_{m}=C_{m}-D_{m+2}\\
- & g_{m}=C_{m}-D_{m} & \sulut{\beta_{m}}\\
\hline  & D_{m+2}=D_{m}
\end{array}}}}}$
\end{frame}
\begin{comment}
%
\begin{frame}{Elimination as key derivation step}
\begin{itemize}
\item In the derivation of $D_{m+2}=D_{m}$, we \emph{eliminated} terms
containing $C$ or $g$ by ordering $D\prec C,g$
\end{itemize}
Generally:
\begin{itemize}
\item Before applying $\Sum$ to recurrences,\\
eliminate terms with $n$-dependent coefficients
\item<2-> Before applying $\left\{ n\mapsto0\right\} $ to recurrences,\\
eliminate terms with shifted $n$-index
\item<2-> All linear substitutions are handled by \textquotedblleft eliminating
shifts\textquotedblright{}
\item<3-> Product $f_{n}g_{n}=\left\{ m\mapsto n\right\} \left(f_{n}g_{m}\right)$
is written variable disjoint
\item<3-> By linearity, recurrences of $f_{n}g_{m}$ are union of\\
recurrences of $f_{n}$ and $g_{m}$ multiplied by $g_{m}$ or $f_{n}$
\end{itemize}
\end{frame}
\end{comment}
%
\begin{frame}{Normalization of sequences}
\begin{itemize}
\item Homogeneous $D_{m+2}{=}D_{m}$ does induction $D_{m}{=}0\Rightarrow D_{m+2}{=}0$
\item Heterogeneous recurrence (e.g. $D_{m+2}-D_{m}=\makeop{bad}_{m}$)
wouldn't
\item<2-> Fix such by rewriting ($\to$) between propagation steps
\item<2-> E.g. $-B_{m+1}^{m+1}+B_{m+1}^{m+1}-B_{m+1}^{0}\to-a_{m+1}$ where
$B_{m}^{n}=a_{m-n}$
\item<3-> Sort, cancel and distribute in + and $\cdot$ expressions
\item<3-> Rewrite ($f,g$ sequences; $\sigma,\widehat{\sigma}$ substitutions;
$c\in\mathbb{N}$)
\begin{align*}
{\textstyle \Sum[][c]}f_{\overrightarrow{m}}^{n} & \to f_{\overrightarrow{m}}^{0}+...+f_{\overrightarrow{m}}^{c} & \left\{ \overrightarrow{m}\mapsto\overrightarrow{x}\right\} m_{j} & \to x_{j}\\
g_{\overrightarrow{m}}\cdot{\textstyle \Sum[][x]}f_{\overrightarrow{m}}^{n} & \to{\textstyle \Sum[][x]}g_{\overrightarrow{m}}f_{\overrightarrow{m}}^{n} & \sigma\sulut{f_{\overrightarrow{m}}g_{\overrightarrow{m}}} & \to\sigma f_{\overrightarrow{m}}\cdot\sigma g_{\overrightarrow{m}}\\
\sigma{\textstyle \Sum[][x]}f_{\overrightarrow{m}}^{n} & \to{\textstyle \Sum[][\sigma x]}\sigma f_{\overrightarrow{m}}^{n} & \widehat{\sigma}\sigma f_{\overrightarrow{m}} & \to\sulut{\widehat{\sigma}\circ\sigma}f_{\overrightarrow{m}}
\end{align*}
\end{itemize}
\end{frame}
%
\begin{frame}{Integration to superposition calculus}
\begin{itemize}
\item The base prover could use higher-order superposition
\item<2-> During proving detect clauses $g\left[\vaihda s3{\overrightarrow{s}}\right]\neq0$
containing $\sum$
\item<2-> To them apply new inference rule 
\[
\frac{g\left[\vaihda s3{\overrightarrow{s}}\right]\neq\vaihda 03{0\vee C}\quad\text{initial recurrences}}{\smash{\bigvee\limits _{\vaihda b3{\overrightarrow{b}}\in B}}g\left[\vaihda b3{\overrightarrow{b}}\right]\neq\vaihda 03{0\vee C\vee L}}\s,\quad\text{where}
\]

\begin{itemize}
\item<2-> choose subterm$\vaihdax s3{\text{s }\overrightarrow{s}}$ to be generalized
\item<2-> get base cases $B$ from recurrences derived to $g$
\item<3-> $L=$ leading coefficients have inverses
\end{itemize}
\end{itemize}
\end{frame}
%
\begin{frame}{Base cases of induction}
\begin{itemize}
\item To refute $g\left[\overrightarrow{s}\right]\neq0$, prove generally
$\forall\overrightarrow{n}{\in}\mathbb{N}^{{\scriptscriptstyle \#}\overrightarrow{s}}\negthickspace:g\left[\overrightarrow{n}\right]=0$
\item<2-> Largest shift in recurrence of $g$ determines base cases
\item<2-> Base cases of $c_{n,b}^{\vaihda{}3{m,a}}g\left[n+b\vaihda{}3{,m+a}\right]+...+c_{n,0}^{\vaihda{}3{m,0}}g\left[n\vaihda{}3{,m}\right]=0$
are $g\left[0\vaihda{}3{,i}\right]=...=g\left[b-1\vaihda{}3{,i}\right]=\vaihda 03{0=g\left[i,0\right]=...=g\left[i,a-1\right]\s\forall i}$
\item<4-> Compare shifts (e.g. $n,m{+}3$ vs $n{+}3,m$) lexicographically
\item<4-> With many recurrences, intersect base case sets
\end{itemize}
\end{frame}
%
\begin{frame}{Conclusion}
\begin{itemize}
\item Recurrences prove an induction step for an equation
\item Recurrences of a sum can be derived from\\
recurrences of the summand
\item This way holonomic sequences can be integrated to\\
superposition and other proof calculi
\end{itemize}
\end{frame}

\end{document}
