# HG changeset patch
# User Christian Urban <christian.urban@kcl.ac.uk>
# Date 1760696449 -3600
# Node ID ae9ffbf979ffd374a8a862493a305bec239b67f1
# Parent  432d027aa6f7c42a80a06ab84aacc63451235334
updated

diff -r 432d027aa6f7 -r ae9ffbf979ff hws/hw04.pdf
Binary file hws/hw04.pdf has changed
diff -r 432d027aa6f7 -r ae9ffbf979ff hws/hw04.tex
--- a/hws/hw04.tex	Sun Oct 12 12:50:16 2025 +0100
+++ b/hws/hw04.tex	Fri Oct 17 11:20:49 2025 +0100
@@ -261,7 +261,18 @@
   }
 
 \item Recall the functions \textit{nullable} and
-      \textit{zeroable}.  Define recursive functions
+      \textit{zeroable} from HW2. Define the cases of these
+      functions for the $r^{\{n\}}$ regular expression. Recall that the first 
+      function needs to satisfy the property $\textit{nullable}(r)$ iff $[]\in L(r)$ and
+      the second $\textit{zeroable}(r)$ iff $L(r) = \emptyset$
+
+  \solution{
+    $\textit{nullable}(r^{\{n\}}) \dn if n = 0 then true else \textit{nullable}(r)$
+
+    $\textit{zeroable}(r^{\{n\}}) \dn if n = 0 then false else \textit{zeroable}(r)$    
+  }    
+
+\item Define recursive functions
       \textit{atmostempty} (for regular expressions that match no
       string or only the empty string), \textit{somechars} (for
       regular expressions that match some non-empty string),
diff -r 432d027aa6f7 -r ae9ffbf979ff hws/hw08.pdf
Binary file hws/hw08.pdf has changed
diff -r 432d027aa6f7 -r ae9ffbf979ff hws/hw08.tex
--- a/hws/hw08.tex	Sun Oct 12 12:50:16 2025 +0100
+++ b/hws/hw08.tex	Fri Oct 17 11:20:49 2025 +0100
@@ -114,6 +114,63 @@
 Scala cannot generate jumps in between different methods (to which functions are compiled to). So cannot eliminate the tail-calls. Haskell for example can do this because it compiles the code in a big ``blob'' inside a main-method (similar to the WHILE language).
 }  
 
+\item The JVM method given below is code for the following recursive function
+
+\begin{lstlisting}[numbers=none]
+def add(x, y) = if x == 0 then y else add(x - 1, y + 1)
+\end{lstlisting}
+
+Rewrite the JVM code such that the recursive call at the end is removed.
+
+\begin{lstlisting}[language=JVMIS,numbers=none]
+.method public static add(II)I
+.limit locals 2
+.limit stack 7
+  iload 0
+  ldc 0
+  if_icmpne If_else_4
+  iload 1
+  goto If_end_5
+If_else_4:
+  iload 0
+  ldc 1
+  isub
+  iload 1
+  ldc 1
+  iadd
+  invokestatic defs/defs/add(II)I  ;; recursive call
+If_end_5:
+  ireturn
+.end method
+\end{lstlisting}
+
+\solution{
+\begin{lstlisting}[language=JVMIS,numbers=none]
+.method public static add(II)I
+.limit locals 2
+.limit stack 7
+add2_Start:
+  iload 0
+  ldc 0
+  if_icmpne If_else_4
+  iload 1
+  goto If_end_5
+If_else_4:
+  iload 0
+  ldc 1
+  isub
+  iload 1
+  ldc 1
+  iadd 
+  istore 1
+  istore 0
+  goto add2_Start
+If_end_5:
+  ireturn
+.end method
+\end{lstlisting}
+}
+
 
 \item Explain what is meant by the terms lazy evaluation and eager
   evaluation.
diff -r 432d027aa6f7 -r ae9ffbf979ff progs/Matcher2.thy
--- a/progs/Matcher2.thy	Sun Oct 12 12:50:16 2025 +0100
+++ b/progs/Matcher2.thy	Fri Oct 17 11:20:49 2025 +0100
@@ -186,7 +186,7 @@
 | "M (NMTIMES r n m) = Suc (Suc (M r)) * 2 * (Suc m) * (Suc (Suc m) - Suc n)"
 | "M (UPNTIMES r n) = Suc (M r) * 2 * (Suc n)"
 
-function der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
+fun der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 where
   "der c (NULL) = NULL"
 | "der c (EMPTY) = NULL"
@@ -197,70 +197,12 @@
 | "der c (NOT r) = NOT(der c r)"
 | "der c (PLUS r) = SEQ (der c r) (STAR r)"
 | "der c (OPT r) = der c r"
-| "der c (NTIMES r 0) = NULL"
-| "der c (NTIMES r (Suc n)) = der c (SEQ r (NTIMES r n))"
+| "der c (NTIMES r n) = (if n = 0 then NULL else (SEQ (der c r) (NTIMES r (n - 1))))"
 | "der c (NMTIMES r n m) = 
-        (if m < n then NULL else 
-        (if n = m then der c (NTIMES r n) else
-                       ALT (der c (NTIMES r n)) (der c (NMTIMES r (Suc n) m))))"
-| "der c (UPNTIMES r 0) = NULL"
-| "der c (UPNTIMES r (Suc n)) = der c (ALT (NTIMES r (Suc n)) (UPNTIMES r n))"
-by pat_completeness auto
-
-lemma bigger1:
-  "\<lbrakk>c < (d::nat); a < b; 0 < a; 0 < c\<rbrakk> \<Longrightarrow> c * a < d * b"
-by (metis le0 mult_strict_mono')
-
-termination der 
-apply(relation "measure (\<lambda>(c, r). M r)") 
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp_all del: M.simps)
-apply(simp_all only: M.simps)
-defer
-defer
-defer
-apply(subgoal_tac "Suc (Suc m) - Suc (Suc n) < Suc (Suc m) - Suc n")
-prefer 2
-     apply(auto)[1]
-
-(*
-apply (metis Suc_mult_less_cancel1 mult.assoc numeral_eq_Suc)
-apply(subgoal_tac "0 < (Suc (Suc m) - Suc n)")
-prefer 2
-apply(auto)[1]
-apply(subgoal_tac "Suc n < Suc m")
-prefer 2
-apply(auto)[1]
-apply(subgoal_tac "Suc (M r) * 2 * Suc n < Suc (Suc (M r)) * 2 * Suc m")
-prefer 2
-apply(subgoal_tac "Suc (M r) * 2 < Suc (Suc (M r)) * 2")
-prefer 2
-apply(auto)[1]
-apply(rule bigger1)
-apply(assumption)
-apply(simp)
-apply (metis zero_less_Suc)
-apply (metis mult_is_0 neq0_conv old.nat.distinct(2))
-apply(rotate_tac 4)
-apply(drule_tac a="1" and b="(Suc (Suc m) - Suc n)" in bigger1)
-prefer 4
-apply(simp)
-apply(simp)
-apply (metis zero_less_one)
-apply(simp)
-done
-*)
-sorry
+        (if m = 0 then NULL else 
+        (if n = 0 then SEQ (der c r) (UPNTIMES r (m - 1))
+         else SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))"
+| "der c (UPNTIMES r n) = (if n = 0 then NULL else SEQ (der c r) (UPNTIMES r (n - 1)))"
 
 fun 
  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -369,6 +311,7 @@
 unfolding Der_def 
 by(auto simp add: Cons_eq_append_conv Seq_def)
 
+
 lemma Der_UNION [simp]: 
   shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))"
   by (auto simp add: Der_def)
@@ -412,22 +355,24 @@
 next
   case (NTIMES r n)
   then show ?case
-    apply(induct n)
-     apply(simp)
-    apply(simp only: L.simps)
-    apply(simp only: Der_pow)
-    apply(simp only: der.simps L.simps)
-    apply(simp only: nullable_correctness)
-    apply(simp only: if_f)
-    by simp
+    apply(auto simp add: Seq_def)
+    using Der_ntimes Matcher2.Seq_def less_iff_Suc_add apply fastforce
+    using Der_ntimes Matcher2.Seq_def less_iff_Suc_add by auto
 next
   case (NMTIMES r n m)
   then show ?case 
+    apply(auto simp add: Seq_def)
+    sledgeham mer[timeout=1000]
     apply(case_tac n)
     sorry
 next
   case (UPNTIMES r x2)
-  then show ?case sorry
+  then show ?case 
+    apply(auto simp add: Seq_def)
+    apply (metis (mono_tags, lifting) Der_ntimes Matcher2.Seq_def Suc_le_mono Suc_pred atMost_iff
+        mem_Collect_eq)
+sledgehammer[timeout=1000]
+    sorry
 qed
 
 
diff -r 432d027aa6f7 -r ae9ffbf979ff progs/fun/defs.fun
--- a/progs/fun/defs.fun	Sun Oct 12 12:50:16 2025 +0100
+++ b/progs/fun/defs.fun	Fri Oct 17 11:20:49 2025 +0100
@@ -9,6 +9,9 @@
 def add(x, y) =
   if x == 0 then y else suc(add(x - 1, y));
 
+def add2(x, y) =
+  if x == 0 then y else add2(x - 1, y + 1); 
+  
 def mult(x, y) =
   if x == 0 then 0 else add(y, mult(x - 1, y));
 
@@ -83,3 +86,4 @@
 //collatz(5000)
 //facT(6, 1)
 
+
diff -r 432d027aa6f7 -r ae9ffbf979ff slides/slides03.pdf
Binary file slides/slides03.pdf has changed
diff -r 432d027aa6f7 -r ae9ffbf979ff slides/slides03.tex
--- a/slides/slides03.tex	Sun Oct 12 12:50:16 2025 +0100
+++ b/slides/slides03.tex	Fri Oct 17 11:20:49 2025 +0100
@@ -65,20 +65,42 @@
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
-{
-\setbeamercolor{background canvas}{bg=cream}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
-\frametitle{For Installation Problems}
+
+\begin{mybox3}{From Mentimeter}\it    
+Is there a specific reason Python and the other programming 
+languages have not implemented their regex matcher like the much 
+faster algorithms described in the videos?
+\end{mybox3}  
+
+\begin{mybox3}{From the Survey}\it    
+If worst case for regex with derivatives is same as a
+normal regex engine, why is there a heavy focus on regex
+for lexer given most languages don't use it.
+\end{mybox3}  
 
-\begin{itemize}
-\item Harry Dilnot (harry.dilnot@kcl.ac.uk) \\
-  \;\;Windows expert
-\item Oliver Iliffe (oliver.iliffe@kcl.ac.uk) 
-\end{itemize}
-  
 \end{frame}
-}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+%{
+%\setbeamercolor{background canvas}{bg=cream}
+%\begin{frame}[c]
+%\frametitle{For Installation Problems}
+%
+%\begin{itemize}
+%\item Harry Dilnot (harry.dilnot@kcl.ac.uk) \\
+%  \;\;Windows expert
+%\item Oliver Iliffe (oliver.iliffe@kcl.ac.uk) 
+%\end{itemize}
+%  
+%\end{frame}
+%}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -193,16 +215,16 @@
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-
-\begin{mybox3}{From Pollev last week}\it    
-  For a regular expression $r = r_1 \cdot r_2$, to prove that
-  $der\;c\;r = (der\;c\;r) \cdot r^{\{n-1\}}$, is there a
-  way to prove it in the general case instead
-  of how you do the calculations for each $n$ in the videos?
-\end{mybox3}  
-
-\end{frame}
+%\begin{frame}[c]
+%
+%\begin{mybox3}{From Pollev last week}\it    
+%  For a regular expression $r = r_1 \cdot r_2$, to prove that
+%  $der\;c\;r = (der\;c\;r) \cdot r^{\{n-1\}}$, is there a
+%  way to prove it in the general case instead
+%  of how you do the calculations for each $n$ in the videos?
+%\end{mybox3}  
+%
+%\end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 
@@ -1621,6 +1643,8 @@
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
 
+ 
+
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %\begin{frame}[c]
@@ -1842,6 +1866,31 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
+\frametitle{Hierarchy of Languages}
+
+\begin{center}
+\begin{tikzpicture}
+[rect/.style={draw=black!50, 
+              top color=white,
+              bottom color=black!20, 
+              rectangle, 
+              very thick, 
+              rounded corners}, scale=1.2]
+
+\draw (0,0) node [rect, text depth=39mm, text width=68mm] {all languages};
+\draw (0,-0.4) node [rect, text depth=28.5mm, text width=64mm] {decidable languages};
+\draw (0,-0.85) node [rect, text depth=17mm] {context sensitive languages};
+\draw (0,-1.14) node [rect, text depth=9mm, text width=50mm] {context-free languages};
+\draw (0,-1.4) node [rect] {regular languages};
+\end{tikzpicture}
+
+\end{center}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
 \frametitle{Negation}
 
 Regular languages are closed under negation:\bigskip