merged draft
authorlammich <lammich@in.tum.de>
Thu, 06 Jul 2017 15:01:10 +0200
changeset 69830 b73cacf0b109
parent 69829 6c684a17800e (current diff)
parent 69825 d3e83bb8db26 (diff)
child 69831 63f6734905f0
child 69833 4ac7a4754e9b
merged
--- a/ROOT	Thu Jul 06 15:00:28 2017 +0200
+++ b/ROOT	Thu Jul 06 15:01:10 2017 +0200
@@ -24,6 +24,7 @@
     Trie_Slides
     Leftist_Heap_Slides
     Braun_Tree_Slides
+    Amor_Slides
   document_files
     "root.tex"
     "root_handout.tex"
--- a/Slides/Amor_Slides.thy	Thu Jul 06 15:00:28 2017 +0200
+++ b/Slides/Amor_Slides.thy	Thu Jul 06 15:01:10 2017 +0200
@@ -3,34 +3,256 @@
 imports
   FDSlatex
 begin
+fun incr :: "bool list \<Rightarrow> bool list" where
+"incr [] = [True]" |
+"incr (False # bs) = True # bs" |
+"incr (True # bs) = False # incr bs"
+
+fun t_incr :: "bool list \<Rightarrow> real" where
+"t_incr [] = 1" |
+"t_incr (False # bs) = 1" |
+"t_incr (True # bs) = 1 + t_incr bs"
+
+definition \<Phi> :: "bool list \<Rightarrow> real" where
+"\<Phi> bs = length(filter id bs)"
+
+definition a_incr :: "bool list \<Rightarrow> real" where
+"a_incr bs = 2"
+
+lemma incr_thm: "t_incr bs + \<Phi> (incr bs) - \<Phi> bs = a_incr bs"
+by(induction bs) (auto simp: \<Phi>_def a_incr_def)
 (*>*)
 text_raw{*
 \end{isabellebody}%
-\newcommand{\revealbeamer}[1]{\uncover<+->{\invisible<handout>{#1}}}
 \section{Amortized Complexity}
 %-------------------------------------------------------------
+\subsection{Motivation}
+%-------------------------------------------------------------
+\begin{frame}
+\begin{example}
+\begin{center} $n$ increments of a binary counter starting with $0$
+\end{center}
+\end{example}
+\begin{itemize}
+\pause
+\item
+WCC of one increment? \pause
+\high{$O(\log_2 n)$}
+\pause
+\item
+WCC of $n$ increments? \pause
+\high{$O(n * \log_2 n)$}
+\pause
+\item \bad{$O(n * \log_2 n)$} is too pessimistic!
+\pause
+\item Every second increment is cheap and compensates for the more expensive increments
+\pause
+\item Fact: WCC of $n$ increments is \high{$O(n)$}
+\end{itemize}
+\onslide<2->
+WCC = worst case complexity
+\end{frame}
+%-------------------------------------------------------------
 \begin{frame}{The problem}
 \begin{center}
-Worst case complexities of \high{individual operations}\\
+WCC of \high{individual operations}\\
 may lead to \bad{overestimation} of\\
-worst case complexities of \bad{sequences of operations}
+WCC of \bad{sequences of operations}
 \end{center}
 \end{frame}
 %-------------------------------------------------------------
-\begin{frame}{Priority queues are multisets}
+\begin{frame}{Amortized analysis}
+Idea:
 \begin{center}
-The same element can be contained \high{multiple times}\\ in a priority queue
+Try to determine the average cost of each operation\\\pause (in the worst case!)
+\medskip
+
+\pause
+Use cheap operations to pay for expensive ones
+\end{center}
+\pause
+Method:
+\begin{itemize}
+\pause
+\item
+Cheap operations pay extra (into a ``bank account''), making them more expensive
+\pause
+\item
+Expensive operations withdraw money from the account, making them cheaper
+\end{itemize}
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}{Bank account = \emph{Potential}}
+\begin{itemize}
+\pause
+\item
+The potential (``credit'') is implicitly ``stored'' in the data structure.
+\pause
+\item
+\high{Potential \<open>\<Phi> :: data\<hyphen>structure \<Rightarrow> non\<hyphen>neg. number\<close>}
+tells us how much credit is stored in a data structure
+\pause
+\item
+Increase in potential =\\ deposit to pay for \emph{later} expensive operation
+\pause
+\item
+Decrease in potential =\\ withdrawal to pay for expensive operation
+\end{itemize}
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}{Back to example: counter}
+\pause
+Increment:
+\begin{itemize}
+\item
+Actual cost: 1 for each bit flip
+\pause
+\item
+Bank transaction:
+\begin{itemize}
+\pause
+\item
+pay in 1 for final $0 \to 1$ flip
+\pause
+\item
+take out 1 for each $1 \to 0$ flip
+\end{itemize}
+\pause
+\<open>\<Longrightarrow>\<close> increment has amortized cost 2 = 1+1
+\end{itemize}
+\pause
+Formalization via potential:
+
+\<open>\<Phi> counter =\<close> the number of 1's in \<open>counter\<close>
+\end{frame}
+%-------------------------------------------------------------
+\subsection{Formalization}
+%-------------------------------------------------------------
+\begin{frame}{Data structure}
+Given an implementation:
+\begin{itemize}
+\pause
+\item Type \<open>\<tau>\<close>
+\pause
+\item Operation(s) \<open>f :: \<tau> \<Rightarrow> \<tau>\<close>\\\pause (may have additional parameters)
+\pause
+\item Initial ``state'': \<open>s\<^sub>0 :: \<tau>\<close>\\ (function ``empty'')
+\end{itemize}
+\pause
+Needed for complexity analysis:
+\begin{itemize}
+\pause
+\item Time/cost: \<open>t_f :: \<tau> \<Rightarrow> num\<close>\\
+\pause
+(\<open>num\<close> = some numeric type \\\pause\ \<open>nat\<close> may be inconvenient)
+\pause
+\item
+\high{Potential \<open>\<Phi> :: \<tau> \<Rightarrow> num\<close>} \pause\quad (creative spark!)
+\end{itemize}
+\pause
+Need to prove: \high{\<open>\<Phi> s \<ge> 0\<close>} and \high{\<open>\<Phi> s\<^sub>0 = 0\<close>}
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}{Amortized and real cost}
+Sequence of operations: \<open>f\<^sub>1\<close>, \dots, \<open>f\<^sub>n\<close>
 \pause
 
-$\Longrightarrow$
+Sequence of states: \<open>s\<^sub>0\<close>, \pause \<open>s\<^sub>1\<close> \<open>:= f\<^sub>1 s\<^sub>0\<close>, \pause \dots, \<open>s\<^sub>n\<close> \<open>:= f\<^sub>n s\<^bsub>n-1\<^esub>\<close>
+\pause
+
+\begin{center}
+\high{Amortized cost := real cost + potential difference}
+\pause\medskip
+
+\<open>a\<^bsub>i+1\<^esub> := t_f\<^bsub>i+1\<^esub> s\<^sub>i + \<Phi> s\<^bsub>i+1\<^esub> - \<Phi> s\<^sub>i\<close>
+\bigskip\pause
 
-The abstract view of a priority queue is a \high{multiset}
+\<open>\<Longrightarrow>\<close>
+
+\high{Sum of amortized costs $\ge$ sum of real costs}
+\medskip\pause
+
+\begin{tabular}{rcl}
+$\sum_{i=1}^n$ \<open>a\<^sub>i\<close> & \<open>=\<close> & $\sum_{i=1}^n$ (\<open>t_f\<^sub>i s\<^bsub>i-1\<^esub> + \<Phi> s\<^sub>i - \<Phi> s\<^bsub>i-1\<^esub>\<close>)\\\pause
+ &\<open>=\<close>& ($\sum_{i=1}^n$ \<open>t_f\<^sub>i s\<^bsub>i-1\<^esub>\<close>) \<open>+ \<Phi> s\<^sub>n - \<Phi> s\<^sub>0\<close>\\\pause
+ &\<open>\<ge>\<close>& $\sum_{i=1}^n$ \<open>t_f\<^sub>i s\<^bsub>i-1\<^esub>\<close>
+\end{tabular}
 \end{center}
 \end{frame}
 %-------------------------------------------------------------
-\begin{frame}{Multisets in Isabelle}
+\begin{frame}{Verification of amortized cost}
+For each operation \<open>f\<close>:\\\pause
+provide an upper bound for its amortized cost
+\begin{center}
+ \high{\<open>a_f :: \<tau> \<Rightarrow> num\<close>}
+\end{center}
+and prove
+\begin{center}
+\high{\<open>t_f s + \<Phi>(f s) - \<Phi> s \<le> a_f s\<close>}
+\end{center}
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}{Back to example: counter}
+@{const_typ incr}\\\pause
+@{thm incr.simps}
+\medskip\pause
+
+@{prop \<open>s\<^sub>0 = []\<close>}
+\medskip\pause
+
+@{thm \<Phi>_def}
+\medskip\pause
+
+@{thm a_incr_def}
+\medskip\pause
 
-Import \texttt{"Library/Multiset"}
+\begin{lemma}
+\high{@{thm incr_thm}}
+\end{lemma}
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}{Proof obligation summary}
+\begin{itemize}
+\item \high{\<open>\<Phi> s \<ge> 0\<close>}
+\item \high{\<open>\<Phi> s\<^sub>0 = 0\<close>}
+\item For every operation \<open>f :: \<tau> \<Rightarrow> ... \<Rightarrow> \<tau>\<close>:\\
+  \high{\<open>t_f s\<close>\ $\overline{x}$\ \<open> + \<Phi>(f s\<close>\ $\overline{x}$\<open>) - \<Phi> s \<le> a_f s\<close>\ $\overline{x}$}
+\end{itemize}
+\pause
+If the data structure has an invariant \<open>invar\<close>:\\ assume precondition \<open>invar s\<close>
+\bigskip\pause
+
+If \<open>f\<close> takes 2 arguments of type \<open>\<tau>\<close>:\\
+\high{\<open>t_f s\<^sub>1 s\<^sub>2\<close>\ $\overline{x}$\ \<open> + \<Phi>(f s\<^sub>1 s\<^sub>2\<close>\ $\overline{x}$\<open>) - \<Phi> s\<^sub>1 - \<Phi> s\<^sub>2 \<le> a_f s\<^sub>1 s\<^sub>2\<close>\ $\overline{x}$}
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}{Warning: real time}
+
+Amortized analysis unsuitable for real time applications:
+\begin{center}
+\bad{Real running time for individual calls\\ may be much worse than amortized time}
+\end{center}
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}{Warning: single threaded}
+\begin{center}
+Amortized analysis is only correct for \high{single threaded} uses of the data structure.
+\medskip\pause
+
+Single threaded = no value is used more than once
+\end{center}
+\pause
+Otherwise:
+\begin{center}
+\begin{tabular}{rl}
+{\sf\emph{ let}} & \<open>counter = 0;\<close>\\
+      & \<open>bad =\<close> increment \<open>counter\<close> $2^n-1$ times;\\
+      & \<open>_ = incr bad;\<close>\\
+      & \bad{\<open>_ = incr bad;\<close>}\\
+      & \bad{\<open>_ = incr bad;\<close>}\\
+      & \bad{$\vdots$}
+\end{tabular}
+\end{center}
 \end{frame}
 %-------------------------------------------------------------
 \begin{isabellebody}%
--- a/Slides/Leftist_Heap_Slides.thy	Thu Jul 06 15:00:28 2017 +0200
+++ b/Slides/Leftist_Heap_Slides.thy	Thu Jul 06 15:01:10 2017 +0200
@@ -12,7 +12,6 @@
 (*>*)
 text_raw{*
 \end{isabellebody}%
-\newcommand{\revealbeamer}[1]{\uncover<+->{\invisible<handout>{#1}}}
 \section{Priority Queues}
 %-------------------------------------------------------------
 \begin{frame}{Priority queue informally}
--- a/Slides/document/main.tex	Thu Jul 06 15:00:28 2017 +0200
+++ b/Slides/document/main.tex	Thu Jul 06 15:01:10 2017 +0200
@@ -1,5 +1,7 @@
 \input{prelude}
 
+\newcommand{\revealbeamer}[1]{\uncover<+->{\invisible<handout>{#1}}}
+
 \renewcommand{\isadigit}[1]{\ensuremath{#1}}
 
 \newcommand{\afpentry}[1]
@@ -34,6 +36,7 @@
 \input{Braun_Tree_Slides}
 %\input{Binomial_Tree_Slides}
 
-%Amortized:
+\part{Amortized Complexity}
+\input{Amor_Slides}
 %\input{Skew_Heap_Slides}
 \end{document}
--- a/Slides/document/root_amor.tex	Thu Jul 06 15:00:28 2017 +0200
+++ b/Slides/document/root_amor.tex	Thu Jul 06 15:01:10 2017 +0200
@@ -12,6 +12,7 @@
 
 \begin{document}
 
+\part{Amortized Complexity}
 \input{session}
 
 %Amortized: