Binary file hws/hw09.pdf has changed

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/hws/hw09.tex	Wed Nov 27 21:36:30 2013 +0000
@@ -0,0 +1,86 @@
+\documentclass{article}
+\usepackage{charter}
+\usepackage{hyperref}
+\usepackage{amssymb}
+\usepackage{amsmath}
+\usepackage{tikz}
+\usetikzlibrary{automata}
+
+\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
+
+\begin{document}
+
+\section*{Homework 9}
+
+\begin{enumerate}
+\item Describe what is meant by \emph{eliminating tail recursion}, when such an 
+optimization can be applied and why it is a benefit?
+
+\item It is true (I confirmed it) that
+
+\begin{center}
+if $\varnothing$ does not occur in $r$ \;\;then\;\;$L(r) \not= \{\}$
+\end{center}
+
+\noindent
+holds, or equivalently
+
+\begin{center}
+$L(r) = \{\}$ \;\;implies\;\; $\varnothing$ occurs in $r$.
+\end{center}
+
+\noindent
+You can prove either version by induction on $r$. The best way to
+make more formal what is meant by `$\varnothing$ occurs in $r$', you can define
+the following function:
+
+\begin{center}
+\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
+$occurs(\varnothing)$      & $\dn$ & $true$\\
+$occurs(\epsilon)$           & $\dn$ &  $f\!alse$\\
+$occurs (c)$                    & $\dn$ &  $f\!alse$\\
+$occurs (r_1 + r_2)$       & $\dn$ &  $occurs(r_1) \vee occurs(r_2)$\\ 
+$occurs (r_1 \cdot r_2)$ & $\dn$ &  $occurs(r_1) \vee occurs(r_2)$\\
+$occurs (r^*)$                & $\dn$ & $occurs(r)$ \\
+\end{tabular}
+\end{center}
+
+\noindent
+Now you can prove 
+
+\begin{center}
+$L(r) = \{\}$ \;\;implies\;\; $occurs(r)$.
+\end{center}
+
+\noindent
+The interesting cases are $r_1 + r_2$ and $r^*$.
+The other direction is not true, that is if $occurs(r)$ then $L(r) = \{\}$. A counter example
+is $\varnothing + a$: although $\varnothing$ occurs in this regular expression, the corresponding
+language is not empty. The obvious extension to include the not-regular expression, $\sim r$,
+also leads to an incorrect statement. Suppose we add the clause
+  
+\begin{center}
+\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
+$occurs(\sim r)$      & $\dn$ & $occurs(r)$
+\end{tabular}
+\end{center}  
+
+\noindent
+to the definition above, then it will not be true that
+
+\begin{center}
+$L(r) = \{\}$ \;\;implies\;\; $occurs(r)$.
+\end{center}
+
+\noindent
+Assume the alphabet contains just $a$ and $b$, find a counter example to this
+property.
+  
+\end{enumerate}
+
+\end{document}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: t
+%%% End: 

--- a/progs/Matcher.thy	Wed Nov 27 08:49:51 2013 +0000
+++ b/progs/Matcher.thy	Wed Nov 27 21:36:30 2013 +0000
@@ -2,6 +2,7 @@
   imports "Main" 
 begin
 
+
 section {* Regular Expressions *}
 
 datatype rexp =
@@ -82,6 +83,34 @@
 | "nullable (STAR r) = True"
 
 fun
+ noccurs :: "rexp \<Rightarrow> bool"
+where
+  "noccurs (NULL) = True"
+| "noccurs (EMPTY) = False"
+| "noccurs (CHAR c) = False"
+| "noccurs (ALT r1 r2) = (noccurs r1 \<or> noccurs r2)"
+| "noccurs (SEQ r1 r2) = (noccurs r1 \<or> noccurs r2)"
+| "noccurs (STAR r) = (noccurs r)"
+
+lemma
+  "\<not> noccurs r \<Longrightarrow> L r \<noteq> {}"
+apply(induct r)
+apply(auto simp add: Seq_def)
+done
+
+lemma
+  "L r = {} \<Longrightarrow> noccurs r"
+apply(induct r)
+apply(auto simp add: Seq_def)
+done
+
+lemma does_not_hold:
+  "noccurs r \<Longrightarrow> L r = {}"
+apply(induct r)
+apply(auto simp add: Seq_def)
+oops
+
+fun
  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 where
   "der c (NULL) = NULL"
@@ -110,6 +139,25 @@
 by (induct r) (auto simp add: Seq_def) 
 section {* Left-Quotient of a Set *}
 
+fun
+ zeroable :: "rexp \<Rightarrow> bool"
+where
+  "zeroable (NULL) = True"
+| "zeroable (EMPTY) = False"
+| "zeroable (CHAR c) = False"
+| "zeroable (ALT r1 r2) = (zeroable r1 \<and> zeroable r2)"
+| "zeroable (SEQ r1 r2) = (zeroable r1 \<or> zeroable r2)"
+| "zeroable (STAR r) = False"
+
+
+lemma zeroable_correctness:
+  shows "zeroable r  \<longleftrightarrow>  (L r = {})"
+apply(induct r)
+apply(auto simp add: Seq_def)[6]
+done
+
+section {* Left-Quotient of a Set *}
+
 definition
   Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
 where

--- a/progs/cw1.scala	Wed Nov 27 08:49:51 2013 +0000
+++ b/progs/cw1.scala	Wed Nov 27 21:36:30 2013 +0000
@@ -95,6 +95,21 @@
   case OPT(_) => true
 }
 
+def zeroable (r: Rexp) : Boolean = r match {
+  case NULL => true
+  case EMPTY => false
+  case CHAR(_) => false
+  case ALT(r1, r2) => zeroable(r1) && zeroable(r2)
+  case SEQ(r1, r2) => zeroable(r1) || zeroable(r2)
+  case STAR(_) => false
+  case PLUS(r) => zeroable(r)
+  case NTIMES(r, i) => if (i == 0) false else zeroable(r)
+  case NUPTOM(r, i, j) => if (i == 0) false else zeroable(r)
+  case RANGE(_) => false
+  case NOT(r) => !(zeroable(r))
+  case OPT(_) => false
+}
+
 // derivative of a regular expression w.r.t. a character
 def der (c: Char, r: Rexp) : Rexp = r match {
   case NULL => NULL
@@ -212,3 +227,36 @@
 println(ders_simp("aaaaa".toList, test))
 println(ders_simp("aaaaaa".toList, test))
 println(ders_simp("aaaaaaa".toList, test))
+
+def TEST(s: String, r: Rexp) = {
+  println("Rexp |" + s + "|")
+  println("Derivative:\n" + ders_simp(s.toList, r))
+  println("Is Nullable: " + nullable(ders_simp(s.toList, r)))
+  println("Is Zeroable: " + zeroable(ders_simp(s.toList, r)))
+  Console.readLine
+}
+
+
+val ALL2 = "a" | "f"
+val COMMENT2 = ("/*" ~ NOT(ALL2.% ~ "*/" ~ ALL2.%) ~ "*/")
+
+println("1) TEST TEST")
+TEST("", COMMENT2)
+TEST("/", COMMENT2)
+TEST("/*", COMMENT2)
+TEST("/*f", COMMENT2)
+TEST("/*f*", COMMENT2)
+TEST("/*f*/", COMMENT2)
+TEST("/*f*/ ", COMMENT2)
+
+val ALL3 = "a" | "f"
+val COMMENT3 = ("/" ~ NOT(ALL3.% ~ "&" ~ ALL3.%) ~ "&")
+
+println("2) TEST TEST")
+TEST("", COMMENT3)
+TEST("/", COMMENT3)
+TEST("/", COMMENT3)
+TEST("/f", COMMENT3)
+TEST("/f&", COMMENT3)
+TEST("/f& ", COMMENT3)
+

--- a/progs/fib.j	Wed Nov 27 08:49:51 2013 +0000
+++ b/progs/fib.j	Wed Nov 27 21:36:30 2013 +0000
@@ -33,8 +33,9 @@
    .limit locals 200
    .limit stack 200
 
-getstatic java/lang/System/in Ljava/io/InputStream;
-invokevirtual java/io/InputStream/read()I
+ldc "Fib"
+invokestatic fib/fib/writes(Ljava/lang/String;)V
+ldc 19
 istore 0
 ldc 0
 istore 1

--- a/progs/fib.while	Wed Nov 27 08:49:51 2013 +0000
+++ b/progs/fib.while	Wed Nov 27 21:36:30 2013 +0000
@@ -1,9 +1,9 @@
 /* Fibonacci Program
    input: n
 */
-//write "Fib";
-read n;
-//n := 19;
+write "Fib";
+//read n;
+n := 19;
 minus1 := 0;
 minus2 := 1;
 while n > 0 do {