# HG changeset patch # User Christian Urban # Date 1385588190 0 # Node ID bd5a8a6b3871aafde6363fd72a93d9e5edf6f90b # Parent f824e1331fc6c6304ae1b555f83aa1e8639ab586 added diff -r f824e1331fc6 -r bd5a8a6b3871 hws/hw09.pdf Binary file hws/hw09.pdf has changed diff -r f824e1331fc6 -r bd5a8a6b3871 hws/hw09.tex --- /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: diff -r f824e1331fc6 -r bd5a8a6b3871 progs/Matcher.thy --- 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 \ bool" +where + "noccurs (NULL) = True" +| "noccurs (EMPTY) = False" +| "noccurs (CHAR c) = False" +| "noccurs (ALT r1 r2) = (noccurs r1 \ noccurs r2)" +| "noccurs (SEQ r1 r2) = (noccurs r1 \ noccurs r2)" +| "noccurs (STAR r) = (noccurs r)" + +lemma + "\ noccurs r \ L r \ {}" +apply(induct r) +apply(auto simp add: Seq_def) +done + +lemma + "L r = {} \ noccurs r" +apply(induct r) +apply(auto simp add: Seq_def) +done + +lemma does_not_hold: + "noccurs r \ L r = {}" +apply(induct r) +apply(auto simp add: Seq_def) +oops + +fun der :: "char \ rexp \ 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 \ bool" +where + "zeroable (NULL) = True" +| "zeroable (EMPTY) = False" +| "zeroable (CHAR c) = False" +| "zeroable (ALT r1 r2) = (zeroable r1 \ zeroable r2)" +| "zeroable (SEQ r1 r2) = (zeroable r1 \ zeroable r2)" +| "zeroable (STAR r) = False" + + +lemma zeroable_correctness: + shows "zeroable r \ (L r = {})" +apply(induct r) +apply(auto simp add: Seq_def)[6] +done + +section {* Left-Quotient of a Set *} + definition Der :: "char \ string set \ string set" where diff -r f824e1331fc6 -r bd5a8a6b3871 progs/cw1.scala --- 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) + diff -r f824e1331fc6 -r bd5a8a6b3871 progs/fib.j --- 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 diff -r f824e1331fc6 -r bd5a8a6b3871 progs/fib.while --- 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 {