# HG changeset patch # User Chengsong # Date 1653068914 -3600 # Node ID 6fecb7fe8cd0c4446d16f04f99de659d3a8a6fea # Parent 84938708781d4db1e96b231b364bb8aeb2602ca5 blexer2: modified for plotting diff -r 84938708781d -r 6fecb7fe8cd0 ChengsongTanPhdThesis/Chapters/Chapter1.tex --- a/ChengsongTanPhdThesis/Chapters/Chapter1.tex Tue May 17 01:44:30 2022 +0100 +++ b/ChengsongTanPhdThesis/Chapters/Chapter1.tex Fri May 20 18:48:34 2022 +0100 @@ -308,6 +308,53 @@ backtracking algorithms. However, they do not scale well with bounded repetitions.\\ + +\begin{center} +\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}} +\begin{tikzpicture} +\begin{axis}[ + ymode=log, + xlabel={$n$}, + x label style={at={(1.05,-0.05)}}, + ylabel={time in secs}, + enlargelimits=false, + xtick={1,2,...,8}, + xmax=9, + ymax=16000000, + ytick={0,500,...,3500}, + scaled ticks=false, + axis lines=left, + width=5cm, + height=4cm, + legend entries={JavaScript}, + legend pos=north west, + legend cell align=left] +\addplot[red,mark=*, mark options={fill=white}] table {re-chengsong.data}; +\end{axis} +\end{tikzpicture} +\end{tabular} +\end{center} + +Another graph: +\begin{center} +\begin{tikzpicture} + \begin{axis}[ + height=0.5\textwidth, + width=\textwidth, + xlabel=number of a's, + xtick={0,...,9}, + ylabel=maximum size, + ymode=log, + log basis y={2} +] + \addplot[mark=*,blue] table {re-chengsong.data}; + \end{axis} +\end{tikzpicture} +\end{center} + + + + Bounded repetitions, usually written in the form $r^{\{c\}}$ (where $c$ is a constant natural number), denotes a regular expression accepting strings diff -r 84938708781d -r 6fecb7fe8cd0 ChengsongTanPhdThesis/Chapters/Chapter2.tex --- a/ChengsongTanPhdThesis/Chapters/Chapter2.tex Tue May 17 01:44:30 2022 +0100 +++ b/ChengsongTanPhdThesis/Chapters/Chapter2.tex Fri May 20 18:48:34 2022 +0100 @@ -488,8 +488,8 @@ as suggested by the finiteness bound proof. And unfortunately we have concrete examples where such regexes grew exponentially large before levelling off: -$(a ^ * + (a + aa) ^ * + (a + aa + aaa) ^ * + \ldots + -(a+ aa + aaa+\ldots \underbrace{a \ldots a}_{\text{n a's}})^*$ will already have a maximum +$(a ^ * + (aa) ^ * + (aaa) ^ * + \ldots + +(\underbrace{a \ldots a}_{\text{n a's}})^*$ will already have a maximum size that is exponential on the number $n$. %TODO: give out a graph showing how the size of the regex grows and levels off at a size exponential to the original regex @@ -503,7 +503,7 @@ %---------------------------------------------------------------------------------------- % SECTION 5 %---------------------------------------------------------------------------------------- -\section{a stronger version of simplification} +\section{A Stronger Version of Simplification} %TODO: search for isabelle proofs of algorithms that check equivalence diff -r 84938708781d -r 6fecb7fe8cd0 thys2/blexer2.sc --- a/thys2/blexer2.sc Tue May 17 01:44:30 2022 +0100 +++ b/thys2/blexer2.sc Fri May 20 18:48:34 2022 +0100 @@ -983,96 +983,60 @@ starPrint(r2) println(")") case ZERO => println("0") - } // @arg(doc = "small tests") -val STARREG = //((( (STAR("aa")) | STAR("aaa") ).%).%) +def n_astar_list(d: Int) : Rexp = { + if(d == 0) STAR("a") + else ALTS(STAR("a" * d), n_astar_list(d - 1)) +} +def n_astar_alts(d: Int) : Rexp = d match { + case 0 => n_astar_list(0) + case d => STAR(n_astar_list(d)) + // case r1 :: r2 :: Nil => ALTS(r1, r2) + // case r1 :: Nil => r1 + // case r :: rs => ALTS(r, n_astar_alts(rs)) + // case Nil => throw new Error("should give at least 1 elem") +} +def n_astar_aux(d: Int) = { + if(d == 0) n_astar_alts(0) + else ALTS(n_astar_alts(d), n_astar_alts(d - 1)) +} + +def n_astar(d: Int) : Rexp = STAR(n_astar_aux(d)) +//val STARREG = n_astar(3) +// ( STAR("a") | +// ("a" | "aa").% | +// ( "a" | "aa" | "aaa").% +// ).% + //( "a" | "aa" | "aaa" | "aaaa").% | + //( "a" | "aa" | "aaa" | "aaaa" | "aaaaa").% (((STAR("a") | ( STAR("aaa")) | STAR("aaaaa"| ( STAR("aaaaaaa")) | STAR("aaaaaaaaaaa"))).%).%).% // @main - +def lcm(list: Seq[Int]):Int=list.foldLeft(1:Int){ + (a, b) => b * a / + Stream.iterate((a,b)){case (x,y) => (y, x%y)}.dropWhile(_._2 != 0).head._1.abs +} def small() = { - - -// println(lexing_simp(NOTREG, prog0)) -// val v = lex_simp(NOTREG, prog0.toList) -// println(v) - -// val d = (lex_simp(NOTREG, prog0.toList)) -// println(d) - val pderSTAR = pderUNIV(STARREG) - - val refSize = pderSTAR.map(size(_)).sum - // println("different partial derivative terms:") - // pderSTAR.foreach(r => r match { - - // case SEQ(head, rstar) => - // println(shortRexpOutput(head) ++ "~STARREG") - // case STAR(rstar) => - // println("STARREG") - - // } - // ) - // println("the total number of terms is") - // //println(refSize) - // println(pderSTAR.size) - - // val A : Rexp= ("c" | (ONE | "b") ~ "d") ~((ONE).%) - // val B : Rexp = ((ONE).%) - // val C : Rexp = ("d") ~ ((ONE).%) - // val PRUNE_REG : Rexp = (C | B | A) - // val APRUNE_REG = internalise(PRUNE_REG) - // val program_solution = pruneRexp(APRUNE_REG, breakIntoTerms(PRUNE_REG)) - // println("program executes and gives: as disired!") - // println(shortRexpOutput(erase(program_solution))) - // val simpedPruneReg = strongBsimp(APRUNE_REG) - - // println(shortRexpOutput(erase(simpedPruneReg))) - + //val pderSTAR = pderUNIV(STARREG) - for(i <- List(1,2,3,4,10, 100, 400, 841, 900 ) ){// 100, 400, 800, 840, 841, 900 - val prog0 = "a" * i - //println(s"test: $prog0") - println(s"testing with $i a's" ) - //val bd = bdersSimp(prog0, STARREG)//DB - val sbd = bdersStrongRexp(prog0, STARREG)//strongDB - starPrint(erase(sbd)) - val subTerms = breakIntoTerms(erase(sbd)) - //val subTermsLarge = breakIntoTerms(erase(bd)) - - println(s"subterms of regex with strongDB: ${subTerms.length}")//, standard DB: ${subTermsLarge.length}") - - - - println("the number of distinct subterms for bsimp with strongDB") - println(subTerms.distinct.size) - //println(subTermsLarge.distinct.size) - if(pderSTAR.size > subTerms.length) - println(s"which is less than or equal to the number of PDER terms: ${pderSTAR.size}") - - - // println(shortRexpOutput(erase(sbd))) - // println(shortRexpOutput(erase(bd))) - - println("pdersize, original, strongSimp") - println(refSize, size(STARREG), asize(sbd)) - - //val vres = strong_blexing_simp( STARREG, prog0) - //println(vres) + //val refSize = pderSTAR.map(size(_)).sum + for(n <- 6 to 6){ + val STARREG = n_astar(n) + val iMax = (lcm((1 to n).toList)) + for(i <- 1 to iMax + 50){// 100, 400, 800, 840, 841, 900 + val prog0 = "a" * i + //println(s"test: $prog0") + print(n) + print(" ") + // print(i) + // print(" ") + println(asize(bders_simp(prog0.toList, internalise(STARREG)))) + } } - // println(vs.length) - // println(vs) - - - // val prog1 = """read n; write n""" - // println(s"test: $prog1") - // println(lexing_simp(WHILE_REGS, prog1)) - // val display = ("a"| "ab").% - // val adisplay = internalise(display) - // bders_simp( "aaaaa".toList, adisplay) } def generator_test() { @@ -1161,15 +1125,15 @@ } -// small() -generator_test() +small() +// generator_test() -1 +// 1 -SEQ(SEQ(SEQ(ONE,CHAR('b')),STAR(CHAR('b'))), -SEQ(ALTS(ALTS(ZERO,STAR(CHAR('b'))), -STAR(ALTS(CHAR('a'),SEQ(SEQ(STAR(ALTS(STAR(CHAR('c')),CHAR('a'))), -SEQ(CHAR('a'),SEQ(ALTS(CHAR('b'),ZERO),SEQ(ONE,CHAR('b'))))),ONE)))),ONE)) +// SEQ(SEQ(SEQ(ONE,CHAR('b')),STAR(CHAR('b'))), +// SEQ(ALTS(ALTS(ZERO,STAR(CHAR('b'))), +// STAR(ALTS(CHAR('a'),SEQ(SEQ(STAR(ALTS(STAR(CHAR('c')),CHAR('a'))), +// SEQ(CHAR('a'),SEQ(ALTS(CHAR('b'),ZERO),SEQ(ONE,CHAR('b'))))),ONE)))),ONE)) // Sequ(Sequ(Sequ(Empty,Chr(b)),Stars(List(Chr(b), Chr(b)))),Sequ(Right(Stars(List(Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty)), Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty))))),Empty))