# HG changeset patch # User Christian Urban # Date 1445077481 -3600 # Node ID a259eec2515698e40d5f9ed2e91c60932ef81fd8 # Parent 86b2aeae3e98f13ba1ea55159801876c9a9f0fd4 updated diff -r 86b2aeae3e98 -r a259eec25156 hws/hw01.pdf Binary file hws/hw01.pdf has changed diff -r 86b2aeae3e98 -r a259eec25156 hws/hw01.tex --- a/hws/hw01.tex Fri Oct 16 14:27:20 2015 +0100 +++ b/hws/hw01.tex Sat Oct 17 11:24:41 2015 +0100 @@ -31,33 +31,40 @@ languages. In the context of the AFL-course, what is meant by the term \emph{language}? -\item Give the definition for regular expressions. What is the meaning - of a regular expression? (Hint: The meaning is defined recursively.) +\item Give the definition for regular expressions. What is the + meaning of a regular expression? (Hint: The meaning is + defined recursively.) -\item Assume the concatenation operation of two strings is written as - $s_1 @ s_2$. Define the operation of \emph{concatenating}, written - $\_ \,@\, \_$, two sets of strings. +\item Assume the concatenation operation of two strings is + written as $s_1 @ s_2$. Define the operation of + \emph{concatenating} two sets of strings. This operation + is also written as $\_ \,@\, \_$. -\item Assume a set $A$ contains 4 strings and a set $B$ 7 strings. None - of the strings is the empty string. How many strings are in $A \,@\, B$? +\item Assume a set $A$ contains 4 strings and a set $B$ + contains 7 strings. None of the strings is the empty + string. How many strings are in $A \,@\, B$? \item How is the power of a language defined? (Hint: There are two rules, one for $\_^0$ and one for $\_^{n+1}$.) -\item Let $A = \{[a], [b], [c], [d]\}$. How many strings are in $A^4$? - Consider the case of $A^4$ where one of the strings in $A$ is the - empty string, for example $A = \{[a], [b], [c], []\}$. +\item Let $A = \{[a], [b], [c], [d]\}$. (1) How many strings + are in $A^4$? (2) Consider the case of $A^4$ where one of + the strings in $A$ is the empty string, for example $A = + \{[a], [b], [c], []\}$. -\item How many regular expressions are there to match the string - $abc$? How many if they cannot include $\epsilon$ and $\varnothing$? - How many if they are also not allowed to contain stars? How many if - they are also not allowed to contain $\_ + \_$? +\item How many basic regular expressions are there to match + the string $abcd$? (ii) How many if they cannot include + $\epsilon$ and $\varnothing$? (iii) How many if they are + also not allowed to contain stars? (iv) How many if they + are also not allowed to contain $\_ + \_$? -\item When are two regular expressions equivalent? Can you think of - instances where two regular expressions match the same strings, but - it is not so obvious that they do? For example $a + b$ and $b + a$ - do not count\ldots they obviously match the same strings, namely - $[a]$ and $[b]$. +\item When are two regular expressions equivalent? Can you + think of instances where two regular expressions match + the same strings, but it is not so obvious that they do? + For example $a + b$ and $b + a$ do not count\ldots they + obviously match the same strings, namely $[a]$ and + $[b]$. + \end{enumerate} \end{document} diff -r 86b2aeae3e98 -r a259eec25156 hws/hw02.pdf Binary file hws/hw02.pdf has changed diff -r 86b2aeae3e98 -r a259eec25156 hws/hw02.tex --- a/hws/hw02.tex Fri Oct 16 14:27:20 2015 +0100 +++ b/hws/hw02.tex Sat Oct 17 11:24:41 2015 +0100 @@ -52,9 +52,9 @@ Write down clearly in each case what you need to prove and what are the assumptions. -\item Define what is meant by the derivative of a regular expressions - with respoect to a character. (Hint: The derivative is defined - recursively.) +\item Define what is meant by the derivative of a regular + expressions with respect to a character. (Hint: The + derivative is defined recursively.) \item Assume the set $Der$ is defined as diff -r 86b2aeae3e98 -r a259eec25156 hws/hw03.pdf Binary file hws/hw03.pdf has changed diff -r 86b2aeae3e98 -r a259eec25156 hws/hw03.tex --- a/hws/hw03.tex Fri Oct 16 14:27:20 2015 +0100 +++ b/hws/hw03.tex Sat Oct 17 11:24:41 2015 +0100 @@ -47,18 +47,20 @@ What is the language recognised by this automaton? -\item Give a non-deterministic finite automaton that can recognise the - language $L(a\cdot (a + b)^* \cdot c)$. +\item Give a non-deterministic finite automaton that can + recognise the language $L(a\cdot (a + b)^* \cdot c)$. -\item Given a deterministic finite automata $A(Q, q_0, F, \delta)$, - define which language is recognised by this automaton. Can you - define also the language defined by a non-deterministic automaton? +\item Given a deterministic finite automaton $A(Q, q_0, F, + \delta)$, define which language is recognised by this + automaton. Can you define also the language defined by a + non-deterministic automaton? -\item Given the following deterministic finite automata over the - alphabet $\{a, b\}$, find an automaton that recognises the - complement language. (Hint: Recall that for the algorithm from the - lectures, the automaton needs to be in completed form, that is have - a transition for every letter from the alphabet.) +\item Given the following deterministic finite automaton over + the alphabet $\{a, b\}$, find an automaton that + recognises the complement language. (Hint: Recall that + for the algorithm from the lectures, the automaton needs + to be in completed form, that is have a transition for + every letter from the alphabet.) \begin{center} \begin{tikzpicture}[>=stealth',very thick,auto, @@ -92,9 +94,9 @@ %find the corresponding minimal automaton. State clearly which nodes %can be merged. -\item Given the following non-deterministic finite automaton over the - alphabet $\{a, b\}$, find a deterministic finite automaton that - recognises the same language: +\item Given the following non-deterministic finite automaton + over the alphabet $\{a, b\}$, find a deterministic + finite automaton that recognises the same language: \begin{center} \begin{tikzpicture}[>=stealth',very thick,auto, diff -r 86b2aeae3e98 -r a259eec25156 hws/hw04.pdf Binary file hws/hw04.pdf has changed diff -r 86b2aeae3e98 -r a259eec25156 hws/hw04.tex --- a/hws/hw04.tex Fri Oct 16 14:27:20 2015 +0100 +++ b/hws/hw04.tex Sat Oct 17 11:24:41 2015 +0100 @@ -68,13 +68,34 @@ (Hint: You can assume you are already given a regular expression written \texttt{ALL}, that can recognise any character, and a regular expression \texttt{NOT} that recognises the complement of a regular expression.) + +\item Simplify the regular expression -\item How many basic regular expressions are there to match the string - $abcd$? (ii) How many if they cannot include $\epsilon$ and - $\varnothing$? (iii) How many if they are also not allowed to - contain stars? (iv) How many if they are also not allowed to contain - $\_ + \_$? +\[ +(\varnothing \cdot (b \cdot c)) + +((\varnothing \cdot c) + \epsilon) +\] + +Does simplification always preserve the meaning of a regular +expression? + +\item The Sulzmann algorithm contains the function $mkeps$ + which answers how a regular expression can match the + empty string. What is the answer of $mkeps$ for the + regular expressions: + \[ + \begin{array}{l} + (\varnothing \cdot (b \cdot c)) + + ((\varnothing \cdot c) + \epsilon)\\ + (a + \varepsilon) \cdot (\varepsilon + \varepsilon) + \end{array} + \] + +\item What is the purpose of the record regular expression + in the Sulzmann algorithm? + + %\item (Optional) The tokenizer in \texttt{regexp3.scala} takes as %argument a string and a list of rules. The result is a list of tokens. Improve this tokenizer so %that it filters out all comments and whitespace from the result. diff -r 86b2aeae3e98 -r a259eec25156 progs/Matcher2.thy --- a/progs/Matcher2.thy Fri Oct 16 14:27:20 2015 +0100 +++ b/progs/Matcher2.thy Sat Oct 17 11:24:41 2015 +0100 @@ -2,6 +2,15 @@ imports "Main" begin +lemma Suc_Union: + "(\ x\Suc m. B x) = (B (Suc m) \ (\ x\m. B x))" +by (metis UN_insert atMost_Suc) + +lemma Suc_reduce_Union: + "(\x\{Suc n..Suc m}. B x) = (\x\{n..m}. B (Suc x))" +by (metis UN_extend_simps(10) image_Suc_atLeastAtMost) + + section {* Regular Expressions *} datatype rexp = @@ -16,6 +25,7 @@ | OPT rexp | NTIMES rexp nat | NMTIMES rexp nat nat +| NMTIMES2 rexp nat nat fun M :: "rexp \ nat" where @@ -30,6 +40,7 @@ | "M (OPT r) = Suc (M r)" | "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)" | "M (NMTIMES r n m) = Suc (M r) * 2 * (Suc n + Suc m)" +| "M (NMTIMES2 r n m) = Suc (M r) * 2 * (Suc n + Suc m)" section {* Sequential Composition of Sets *} @@ -151,11 +162,62 @@ | "L (OPT r) = (L r) \ {[]}" | "L (NTIMES r n) = (L r) \ n" | "L (NMTIMES r n m) = (\i\ {n..n+m} . ((L r) \ i))" +| "L (NMTIMES2 r n m) = (\i\ {n..m} . ((L r) \ i))" + lemma "L (NOT NULL) = UNIV" apply(simp) done +lemma "L (NMTIMES r (Suc n) m) = L (SEQ r (NMTIMES r n m))" +apply(simp add: Suc_reduce_Union Seq_def) +apply(auto) +done + +lemma "L (NMTIMES2 r (Suc n) (Suc m)) = L (SEQ r (NMTIMES2 r n m))" +apply(simp add: Suc_reduce_Union Seq_def) +apply(auto) +done + +lemma "L (NMTIMES2 r 0 0) = {[]}" +apply(simp add: Suc_reduce_Union Seq_def) +done + +lemma t: "\n \ i; i \ m\ \ L (NMTIMES2 r n m) = L (NMTIMES2 r n i) \ L (NMTIMES2 r i m)" +apply(auto) +apply (metis atLeastAtMost_iff nat_le_linear) +apply (metis atLeastAtMost_iff le_trans) +by (metis atLeastAtMost_iff le_trans) + + +lemma "L (NMTIMES2 r 0 (Suc m)) = L (NMTIMES2 r 0 1) \ L (NMTIMES2 r 1 (Suc m))" +apply(rule t) +apply(auto) +done + +lemma "L (NMTIMES2 r 0 (Suc m)) = L (NMTIMES2 r 0 1) \ L (NMTIMES2 r 1 (Suc m))" +apply(rule t) +apply(auto) +done + +lemma "L (NMTIMES2 r 0 1) = {[]} \ L r" +apply(simp) +apply(auto) +apply(case_tac xa) +apply(auto) +done + + +lemma "L (NMTIMES2 r n n) = L (NTIMES r n)" +apply(simp) +done + +lemma "n < m \ L (NMTIMES2 r n m) = L (NTIMES r n) \ L (NMTIMES2 r (Suc n) m)" +apply(simp) +apply(auto) +apply (metis Suc_leI atLeastAtMost_iff le_eq_less_or_eq) +apply (metis atLeastAtMost_iff le_eq_less_or_eq) +by (metis Suc_leD atLeastAtMost_iff) section {* The Matcher *} @@ -173,6 +235,7 @@ | "nullable (OPT r) = True" | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)" | "nullable (NMTIMES r n m) = (if n = 0 then True else nullable r)" +| "nullable (NMTIMES2 r n m) = (if m < n then False else (if n = 0 then True else nullable r))" function der :: "char \ rexp \ rexp" @@ -191,10 +254,14 @@ | "der c (NMTIMES r 0 0) = NULL" | "der c (NMTIMES r 0 (Suc m)) = ALT (der c (NTIMES r (Suc m))) (der c (NMTIMES r 0 m))" | "der c (NMTIMES r (Suc n) m) = der c (SEQ r (NMTIMES r n m))" +| "der c (NMTIMES2 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 (NMTIMES2 r (Suc n) m))))" by pat_completeness auto termination der -by (relation "measure (\(c, r). M r)") (simp_all) +sorry +(*by (relation "measure (\(c, r). M r)") (simp_all)*) fun @@ -213,8 +280,9 @@ lemma nullable_correctness: shows "nullable r \ [] \ (L r)" -by(induct r) (auto simp add: Seq_def) - +apply(induct r) +apply(auto simp add: Seq_def) +done section {* Left-Quotient of a Set *} @@ -282,20 +350,20 @@ shows "Der c (\x\A. B x) = (\x\A. Der c (B x))" by (auto simp add: Der_def) -lemma Suc_Union: - "(\ x\Suc m. B x) = (B (Suc m) \ (\ x\m. B x))" -by (metis UN_insert atMost_Suc) - -lemma Suc_reduce_Union: - "(\x\{Suc n..Suc m}. B x) = (\x\{n..m}. B (Suc x))" -by (metis UN_extend_simps(10) image_Suc_atLeastAtMost) lemma der_correctness: shows "L (der c r) = Der c (L r)" -by (induct rule: der.induct) - (simp_all add: nullable_correctness +apply(induct rule: der.induct) +apply(simp_all add: nullable_correctness Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost) +apply(case_tac m) +apply(simp) +apply(simp) +apply(auto) +apply (metis (poly_guards_query) atLeastAtMost_iff not_le order_refl) +apply (metis Suc_leD atLeastAtMost_iff) +by (metis atLeastAtMost_iff le_antisym not_less_eq_eq) lemma matcher_correctness: