exam draft
authorlammich <lammich@in.tum.de>
Tue, 03 Jul 2018 16:50:01 +0200
changeset 69941 af2719b74080
parent 69940 e04bcdda9c3a
child 69942 3c344ec103ae
exam
SS18/Exercises/exam.pdf
SS18/Exercises/exam/Q_Min_BST.thy
SS18/Exercises/exam/Q_Trie.thy
SS18/Exercises/exam/Q_Unique_SBN.thy
SS18/Exercises/exam/document/root.tex
SS18/Exercises/exam/exam.thy
Binary file SS18/Exercises/exam.pdf has changed
--- a/SS18/Exercises/exam/Q_Min_BST.thy	Tue Jul 03 11:21:09 2018 +0200
+++ b/SS18/Exercises/exam/Q_Min_BST.thy	Tue Jul 03 16:50:01 2018 +0200
@@ -6,28 +6,36 @@
 begin
 (*>*)
   section \<open>Binary Search Trees with Priority Annotations\<close>
-  text \<open>Recall the standard annotated tree data type, where \<open>'a\<close> are
-    the items stored in the tree and \<open>'b\<close> is some node annotation.\<close>
+  text \<open>Recall the standard annotated tree data type, where \<open>'a\<close> is the type of
+    items stored in the tree and \<open>'b\<close> is some node annotation.\<close>
   datatype ('a,'b) tree = Leaf | Node 'b "('a,'b) tree" 'a "('a,'b) tree"
 
   subsection \<open>Part 1\<close>
+  text \<open>Specify a function to obtain the set of items stored in a tree:\<close>
+  fun items :: "('a,'p)tree \<Rightarrow> 'a set"
+  (*<*)
+  where
+    "items Leaf = {}" |
+    "items (Node _ l a r) = insert a (items l \<union> items r)"
+  (*>*)
+
+
+  (*<*)
   text \<open>Specify the inorder traversal function:\<close>
 
   fun inorder :: "('a,'p)tree \<Rightarrow> 'a list"
-  (*<*)
   where
     "inorder Leaf = []" |
     "inorder (Node _ l a r) = inorder l @ a # inorder r"
   (*>*)
-  text_raw \<open>\vspace{5em}\<close>
 
   subsection \<open>Part 2\<close>
-  text \<open>Now assume we have linearly ordered items of type \<open>'a::linorder\<close>.
-    Moreover, we have a (fixed) function \<open>prio :: 'a \<Rightarrow> 'p::linorder\<close> that
+  text \<open>Now assume we have linearly ordered items of type \<open>('a::linorder)\<close>.
+    Moreover, we have a (fixed) function \<open>prio :: 'a \<Rightarrow> ('p::linorder)\<close> that
     assigns each item a priority.
   \<close>
   context
-    fixes prio :: "'a::linorder \<Rightarrow> 'p::linorder"
+    fixes prio :: "('a::linorder) \<Rightarrow> ('p::linorder)"
   begin
 
     text \<open>The annotation of each node shall be an item with minimum priority
@@ -42,8 +50,8 @@
       "inva Leaf \<longleftrightarrow> True"
     | "inva (Node p l a r) \<longleftrightarrow>
           inva l \<and> inva r
-        \<and> p\<in>set (inorder l @ a # inorder r)
-        \<and> (\<forall>x\<in>set (inorder l @ a # inorder r). prio p \<le> prio x)"
+        \<and> p\<in>items (Node p l a r)
+        \<and> (\<forall>x\<in>items (Node p l a r). prio p \<le> prio x)"
 
     definition "invar t \<longleftrightarrow> inva t \<and> sorted_wrt op< (inorder t)"
 
@@ -52,8 +60,9 @@
     (*>*)
 
     subsection \<open>Part 3\<close>
-    text \<open>Specify a function to insert an element into a BST, preserving
-      the search tree property and the correctness of the annotations.
+    text \<open>Specify a function to insert an element into an annotated BST,
+      preserving both the search tree property and the correctness of the
+      annotations.
 
       \textbf{No proofs required!}
       \<close>
--- a/SS18/Exercises/exam/Q_Trie.thy	Tue Jul 03 11:21:09 2018 +0200
+++ b/SS18/Exercises/exam/Q_Trie.thy	Tue Jul 03 16:50:01 2018 +0200
@@ -9,7 +9,7 @@
 text \<open>The following kind of tree is a variant of a trie that
   \<^item> contains only \<open>bool list\<close>s of the same length
   \<^item> can compress subtrees that are full (or empty),
-    i.e. that contain every (or no) \<open>bool list\<close> of some length.
+    i.e. that contain every (or no) \mbox{\<open>bool list\<close>} of some length.
 
 \<close>
 
@@ -22,7 +22,9 @@
 "\<alpha> (Nd l r) d = Cons True ` \<alpha> l (d-1) \<union> Cons False ` \<alpha> r (d-1)"
 
 text \<open>where the the infix operator \<open>`\<close> is the image of a function over a set:
-\<open>f ` A = {b. \<exists>a \<in> A. b = f a}\<close>. The parameter \<open>d\<close> specifies the length of the \<open>bool list\<close>s
+\<open>f ` A = {b. \<exists>a \<in> A. b = f a}\<close>, and \<open>Cons x xs = x#xs\<close>.
+
+The parameter \<open>d\<close> specifies the length of the \<open>bool list\<close>s
 in the tree. It is necessary because \<open>Lf True\<close> represents all lists of some unspecified length.
 Parameter \<open>d\<close> should be at least the height of the tree, otherwise the tree is cut off below depth \<open>d\<close>.
 
@@ -49,10 +51,10 @@
   \<^enum> Define an intersection function \<open>inter :: bt \<Rightarrow> bt \<Rightarrow> bt\<close>
     with the specification \<open>\<alpha> (inter t1 t2) d = \<alpha> t1 d \<inter> \<alpha> t2 d\<close> and \<open>d\<ge>ht (inter t1 t2)\<close>
     if \<open>d \<ge> ht t1\<close> and \<open>d \<ge> ht t2\<close>.
+  \<^enum> Define a function \<open>compressed :: bt \<Rightarrow> bool\<close> that
+    tests if all subtrees in a tree are fully compressed.
   \<^enum> Define a compression function \<open>compress :: bt \<Rightarrow> bt\<close> that
     compresses full (and empty!) subtrees into leaves as much as possible.
-  \<^enum> Define a function \<open>compressed :: bt \<Rightarrow> bool\<close> that
-    tests if all subtrees in a tree are fully compressed.
 
 \<close>
 
--- a/SS18/Exercises/exam/Q_Unique_SBN.thy	Tue Jul 03 11:21:09 2018 +0200
+++ b/SS18/Exercises/exam/Q_Unique_SBN.thy	Tue Jul 03 16:50:01 2018 +0200
@@ -29,21 +29,18 @@
 
 subsection \<open>Part 1\<close>
 
-text \<open>We assume that all elements of an SBN \<open>s\<close> are less than \<open>K\<close>.
-  Specify an upper bound for the number represented by \<open>s\<close> in terms of \<open>K\<close>!
+text \<open>
+  Prove that an SBN where all elements are less than \<open>K\<close> represents
+  a number less than \<open>2\<^sup>K\<close>.
 
-  \textbf{No proof required!}
+  Hint: Induction on the reversed list, i.e., the cases are \<open>[]\<close> and \<open>xs@[x]\<close>.
 \<close>
-
 lemma SBN_upper_bound:
   assumes "invar s"
   assumes "\<forall>r\<in>set s. r<K"
-  (*<*)
-  defines "upper_bound \<equiv> 2^K"
-  (*>*)
-  shows "\<alpha> s < upper_bound"
+  shows "\<alpha> s < 2^K"
 (*<*)
-  using assms(1,2) unfolding upper_bound_def
+  using assms
 proof (induction s arbitrary: K rule: rev_induct)
   case Nil
   then show ?case by simp
@@ -62,13 +59,6 @@
 qed
 (*>*)
 
-text \<open>
-  \vspace{1em}
-  \<open>upper_bound\<close> = \underline{\hspace{5cm}}\\[1em]
-
-  Note: \<open>upper_bound\<close> may only depend on \<open>K\<close>, in particular, it must not depend on \<open>s\<close>!
-\<close>
-
 subsection \<open>Part 2\<close>
 text \<open>Prove that sparse binary number representation is unique,
   i.e., if two SBNs \<open>s\<^sub>1\<close> and \<open>s\<^sub>2\<close> represent the same number, they are already equal:
@@ -127,4 +117,6 @@
 (*<*)
 end
 (*>*)
-text_raw \<open>\blankpage\<close>
\ No newline at end of file
+text_raw \<open>\blankpage\<close>
+text_raw \<open>\blankpage\<close>
+text_raw \<open>\blankpage\<close>
--- a/SS18/Exercises/exam/document/root.tex	Tue Jul 03 11:21:09 2018 +0200
+++ b/SS18/Exercises/exam/document/root.tex	Tue Jul 03 16:50:01 2018 +0200
@@ -56,7 +56,7 @@
  {\sf
 {\Huge Final Exam} \\  \ \\
 {\Large Functional Data Structures} \\ \ \\
-{\Large   31. 07. 2017}}
+{\Large   16. 07. 2018}}
 \end{center}
 
 \fbox{\fbox{
--- a/SS18/Exercises/exam/exam.thy	Tue Jul 03 11:21:09 2018 +0200
+++ b/SS18/Exercises/exam/exam.thy	Tue Jul 03 16:50:01 2018 +0200
@@ -9,3 +9,5 @@
 
 end
 (*>*)
+text_raw \<open>\blankpage\<close>
+text_raw \<open>\blankpage\<close>