Binary file hws/hw01.pdf has changed
--- 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}
Binary file hws/hw02.pdf has changed
--- 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
Binary file hws/hw03.pdf has changed
--- 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,
Binary file hws/hw04.pdf has changed
--- 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.
--- 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:
+ "(\<Union> x\<le>Suc m. B x) = (B (Suc m) \<union> (\<Union> x\<le>m. B x))"
+by (metis UN_insert atMost_Suc)
+
+lemma Suc_reduce_Union:
+ "(\<Union>x\<in>{Suc n..Suc m}. B x) = (\<Union>x\<in>{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 \<Rightarrow> 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) \<union> {[]}"
| "L (NTIMES r n) = (L r) \<up> n"
| "L (NMTIMES r n m) = (\<Union>i\<in> {n..n+m} . ((L r) \<up> i))"
+| "L (NMTIMES2 r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> 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: "\<lbrakk>n \<le> i; i \<le> m\<rbrakk> \<Longrightarrow> L (NMTIMES2 r n m) = L (NMTIMES2 r n i) \<union> 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) \<union> L (NMTIMES2 r 1 (Suc m))"
+apply(rule t)
+apply(auto)
+done
+
+lemma "L (NMTIMES2 r 0 (Suc m)) = L (NMTIMES2 r 0 1) \<union> L (NMTIMES2 r 1 (Suc m))"
+apply(rule t)
+apply(auto)
+done
+
+lemma "L (NMTIMES2 r 0 1) = {[]} \<union> 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 \<Longrightarrow> L (NMTIMES2 r n m) = L (NTIMES r n) \<union> 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 \<Rightarrow> rexp \<Rightarrow> 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 (\<lambda>(c, r). M r)") (simp_all)
+sorry
+(*by (relation "measure (\<lambda>(c, r). M r)") (simp_all)*)
fun
@@ -213,8 +280,9 @@
lemma nullable_correctness:
shows "nullable r \<longleftrightarrow> [] \<in> (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 (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))"
by (auto simp add: Der_def)
-lemma Suc_Union:
- "(\<Union> x\<le>Suc m. B x) = (B (Suc m) \<union> (\<Union> x\<le>m. B x))"
-by (metis UN_insert atMost_Suc)
-
-lemma Suc_reduce_Union:
- "(\<Union>x\<in>{Suc n..Suc m}. B x) = (\<Union>x\<in>{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: