. draft
authornipkow
Fri, 11 Aug 2017 13:40:41 +0200
changeset 69891 6625f13189b9
parent 69890 eef3c9ef1c3e
child 69892 e8e97a214e48
.
ROOT
Slides/Binomial_Tree_Slides.thy
Slides/Braun_Tree_Slides.thy
Slides/Leftist_Heap_Slides.thy
Slides/Skew_Heap_Slides.thy
--- a/ROOT	Tue Aug 08 17:22:04 2017 +0200
+++ b/ROOT	Fri Aug 11 13:40:41 2017 +0200
@@ -12,6 +12,7 @@
     "Slides/Tree_Notation"
     "../Public/Thys/BinHeap"
     "../Public/Thys/Skew_Heap_Analysis"
+    "../Public/Thys/Skew_Heap_Analysis2"
     "../Public/Thys/Splay_Tree_Analysis"
     "../Public/Thys/Pairing_Heap"
 
--- a/Slides/Binomial_Tree_Slides.thy	Tue Aug 08 17:22:04 2017 +0200
+++ b/Slides/Binomial_Tree_Slides.thy	Fri Aug 11 13:40:41 2017 +0200
@@ -59,7 +59,11 @@
 \quad \<open>Node (rank: nat) (root: 'a) ('a tree list)\<close>}
 \bigskip\pause
   
-Invariant: Node of rank \<open>i\<close> has children \<open>[t\<^sub>i\<^sub>-\<^sub>1,\<dots>t\<^sub>0]\<close> of ranks \<open>[i-1,\<dots>,0]\<close>:
+Invariant: Node of rank \<open>r\<close>
+\begin{tabular}[t]{l}
+has children \<open>[t\<^sub>r\<^sub>-\<^sub>1,\<dots>t\<^sub>0]\<close>\\
+of ranks \<open>[r-1,\<dots>,0]\<close>
+\end{tabular}
 \pause
 \high{@{thm [display] invar_btree_simps}}
 \pause
@@ -112,7 +116,7 @@
   Intuition: Addition of binary numbers
   \smallskip\pause
 
-  Note: Handling of carry after recursive call
+  Note: Handling of carry \emph{after} recursive call
 \end{frame}
 %-------------------------------------------------------------
 \begin{frame}{Find/delete minimum element}
@@ -125,9 +129,9 @@
 
   Similar: \high{@{const_typ get_min}} \\
   Returns tree with minimal root, and remaining trees
-\bigskip\pause
+\pause
 
-\high{@{thm [display, margin=60] delete_min_def}}
+\high{@{thm [display, margin=55] del_min_def}}
 \ifMOD\else
 Why \<open>rev\<close>? \pause Rank decreasing in \<open>ts\<^sub>1\<close> but increasing in \<open>ts\<^sub>2\<close>
 \fi
@@ -176,6 +180,64 @@
   \smallskip\pause
   Yields desired linear bound!
 \end{frame}
+%-------------------------------------------------------------
+\begin{frame}{Sources}
+The inventor of the binomial heap:
+\smallskip
+
+Jean Vuillemin.\\
+A Data Structure for Manipulating Priority Queues.\\
+\emph{CACM}, 1978.
+\bigskip\pause
+
+The functional version:
+\smallskip
+
+Chris Okasaki. \emph{Purely Functional Data Structures.}
+Cambridge University Press, 1998.
+\end{frame}
+%-------------------------------------------------------------
+\section{Skew Binomial Heap}
+%-------------------------------------------------------------
+\begin{frame}{Priority queues so far}
+\begin{center}
+@{const insert}, @{const del_min} (and @{const merge})\\ have logarithmic complexity
+\end{center}
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}{Skew Binomial Heap}
+Similar to binomial heap, but involving also\\
+\concept{skew binary numbers}:\smallskip\\\pause
+\begin{tabular}{l}
+$d_1 \dots d_n$ represents $\sum_{i=1}^n d_i * (2^{i+1}-1)$\\
+where $d_i \in \{0,1,2\}$
+\end{tabular}
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}{Complexity}
+Skew binomial heap:
+\begin{center}
+\high{@{const insert} in time $O(1)$}\\
+@{const del_min} and @{const merge} still $O(\log n)$
+\end{center}
+\bigskip\pause
+
+Fibonacci heap (imperative!):
+\begin{center}
+\high{@{const insert} and @{const merge} in time $O(1)$}\\
+@{const del_min} still $O(\log n)$
+\end{center}
+\pause
+
+Every operation in time $O(1)$?
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}{Puzzle}
+\begin{center}
+Design a functional queue\\ with (worst case) constant time \<open>enq\<close> and \<open>deq\<close> functions
+\end{center}
+\end{frame}
+%-------------------------------------------------------------
 
 \begin{isabellebody}%
 *}
--- a/Slides/Braun_Tree_Slides.thy	Tue Aug 08 17:22:04 2017 +0200
+++ b/Slides/Braun_Tree_Slides.thy	Fri Aug 11 13:40:41 2017 +0200
@@ -109,6 +109,8 @@
 \item Delete leftmost element $y$
 \item Sift $y$ from the root down
 \end{enumerate}
+\pause
+Reminiscent of heapsort, but not quite \dots
 \end{frame}
 %-------------------------------------------------------------
 \begin{frame}{@{const del_left}}
@@ -120,9 +122,10 @@
 \begin{frame}{@{const sift_down}}
 \high<1>{@{const_typ sift_down}}\\\smallskip\pause
 \ifMOD
-\high<2-3>{@{text "sift_down (t\<^sub>1 = (Node l\<^sub>1 x\<^sub>1 r\<^sub>1)) a (t\<^sub>2 = (Node l\<^sub>2 x\<^sub>2 r\<^sub>2))"}}\\
-\high<2-3>{\<open>=\<close>}\\\pause
-\high<3>{@{term[break,margin=60] (sub) "(if a \<le> x1 \<and> a \<le> x2
+$\vdots$\\\pause
+\high<3-4>{@{text "sift_down (t\<^sub>1 = (Node l\<^sub>1 x\<^sub>1 r\<^sub>1)) a (t\<^sub>2 = (Node l\<^sub>2 x\<^sub>2 r\<^sub>2))"}}\\
+\high<3-4>{\<open>=\<close>}\\\pause
+\high<4>{@{term[break,margin=60] (sub) "(if a \<le> x1 \<and> a \<le> x2
    then Node t1 a t2
    else if x1 \<le> x2 then Node (sift_down l1 a r1) x1 t2
         else Node t1 x2 (sift_down l2 a r2))"}}
--- a/Slides/Leftist_Heap_Slides.thy	Tue Aug 08 17:22:04 2017 +0200
+++ b/Slides/Leftist_Heap_Slides.thy	Fri Aug 11 13:40:41 2017 +0200
@@ -253,7 +253,10 @@
 \smallskip\pause
 
 \high{@{thm[break] (sub) merge.simps(1) merge2_alt}}\\\pause
-\high{@{thm[break] (sub,dummy_pats) merge.simps(3)}}
+\high{@{const merge} \<open>(\<close>@{prop (sub) "t1 = Node n1 l1 a1 r1"}\<open>)\<close> \<open>(\<close>@{prop (sub) "t2 = Node n2 l2 a2 r2"}\<open>) =\<close>\\
+@{term [break,margin=60] (sub) "if a1 \<le> a2 then node l1 a1 (merge r1 t2)
+    else node l2 a2 (merge r2 t1)"}}
+%\high{@ {thm[break] (sub,dummy_pats) merge.simps(3)}}
 \bigskip\pause
 
 @{const node} \<open>::\<close> @{typ "'a lheap \<Rightarrow> 'a \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap"}\\\smallskip\pause
--- a/Slides/Skew_Heap_Slides.thy	Tue Aug 08 17:22:04 2017 +0200
+++ b/Slides/Skew_Heap_Slides.thy	Fri Aug 11 13:40:41 2017 +0200
@@ -140,6 +140,28 @@
 \texttt{by(induction t1 t2 rule:~merge.induct)(auto)}
 \end{frame}
 %-------------------------------------------------------------
+\begin{frame}{Node-Node case}
+
+Let @{prop (sub) "t1 = Node l1 a1 r1"}, @{prop (sub) "t2 = Node l2 a2 r2"}.\pause
+
+Case @{prop (sub) "a1 \<le> a2"}. \pause Let @{prop (sub) "m = merge t2 r1"}
+\bigskip\pause
+
+@{term (sub) "t_merge t1 t2 + \<Phi> (merge t1 t2) - \<Phi> t1 - \<Phi> t2"}\\\pause
+@{text"="} @{term (sub) "t_merge t2 r1 + 1 + \<Phi> m + \<Phi> l1 + rh m l1"}\\
+ \quad @{term (sub) "- \<Phi> t1 - \<Phi> t2"}
+\\\pause
+@{text"="} @{term (sub) "t_merge t2 r1 + 1 + \<Phi> m + rh m l1"}\\
+ \quad @{term (sub) "- \<Phi> r1 - rh l1 r1 - \<Phi> t2"}
+\\\pause
+@{text"\<le>"} @{term (sub) "lrh m + rlh t2 + rlh r1 + rh m l1 + 2 - rh l1 r1"}\\
+ \quad by IH
+\\\pause
+@{text"="} @{term (sub) "lrh m + rlh t2 + rlh t1 + rh m l1 + 1"}
+\\\pause
+@{text"="} @{term (sub) "lrh (merge t1 t2) + rlh t1 + rlh t2 + 1"}
+\end{frame}
+%-------------------------------------------------------------
 \begin{frame}{Main proof}
 @{thm (lhs,sub) a_merge}\\\pause
 @{text"\<le>"} @{thm (rhs,sub) amor_le[of t1 t2]} % by Lemma