168 $\sum ( rs_a@[a]@rs_c)$ |
168 $\sum ( rs_a@[a]@rs_c)$ |
169 \end{center} |
169 \end{center} |
170 using a function similar to $\distinctBy$, |
170 using a function similar to $\distinctBy$, |
171 but this time |
171 but this time |
172 we allow a more general list rewrite: |
172 we allow a more general list rewrite: |
173 \begin{mathpar} |
173 \begin{mathpar}\label{cubicRule} |
174 \inferrule{\vspace{0mm} }{rs_a@[a]@rs_c |
174 \inferrule{\vspace{0mm} }{rs_a@[a]@rs_c |
175 \stackrel{s}{\rightsquigarrow } |
175 \stackrel{s}{\rightsquigarrow } |
176 rs_a@[\textit{prune} \; a \; rs_a]@rs_c } |
176 rs_a@[\textit{prune} \; a \; rs_a]@rs_c } |
177 \end{mathpar} |
177 \end{mathpar} |
178 %L \; a_1' = L \; a_1 \setminus (\cup_{a \in rs_a} L \; a) |
178 %L \; a_1' = L \; a_1 \setminus (\cup_{a \in rs_a} L \; a) |
179 where $\textit{prune} \;a \; acc$ traverses $a$ |
179 where $\textit{prune} \;a \; acc$ traverses $a$ |
180 without altering the structure of $a$, removing components in $a$ |
180 without altering the structure of $a$, removing components in $a$ |
181 that have appeared in the accumulator $acc$. |
181 that have appeared in the accumulator $acc$. |
182 For example |
182 For example |
400 We would like to preserve the correctness like the one |
400 We would like to preserve the correctness like the one |
401 we had for $\blexersimp$: |
401 we had for $\blexersimp$: |
402 \begin{conjecture}\label{cubicConjecture} |
402 \begin{conjecture}\label{cubicConjecture} |
403 $\blexerStrong \;r \; s = \blexer\; r\;s$ |
403 $\blexerStrong \;r \; s = \blexer\; r\;s$ |
404 \end{conjecture} |
404 \end{conjecture} |
405 |
405 \noindent |
406 To implement this idea into an algorithm, we define a "pruning function" |
406 We introduce the new rule \ref{cubicRule} |
407 $\textit{prune}$, that takes away parts of all terms in $r$ that belongs to |
407 and augment our proofs in chapter \ref{Bitcoded2}. |
408 $\textit{acc}$, which acts as an element |
408 The idea is to maintain the properties like |
409 is a stronger version of $\textit{distinctBy}$. |
409 $r \stackrel{*}{\rightsquigarrow} \textit{bsimp} \; r$ etc. |
410 Here is a concise version of it (in the style of Scala): |
410 |
411 |
411 In the next section, |
412 |
412 we will describe why we |
413 |
413 believe a cubic bound can be achieved. |
414 |
414 We give an introduction to the |
415 \noindent |
415 partial derivatives, |
416 The pruning function can be defined recursively: |
416 which was invented by Antimirov \cite{Antimirov95}, |
417 |
417 and then link it with the result of the function |
418 |
418 $\bdersStrongs$. |
419 |
419 |
420 |
420 \section{Antimirov's partial derivatives} |
421 This suggests a link towrads "partial derivatives" |
421 This suggests a link towrads "partial derivatives" |
422 introduced by Antimirov \cite{Antimirov95}. |
422 introduced The idea behind Antimirov's partial derivatives |
423 |
|
424 \section{Antimirov's partial derivatives} |
|
425 The idea behind Antimirov's partial derivatives |
|
426 is to do derivatives in a similar way as suggested by Brzozowski, |
423 is to do derivatives in a similar way as suggested by Brzozowski, |
427 but maintain a set of regular expressions instead of a single one: |
424 but maintain a set of regular expressions instead of a single one: |
428 |
425 |
429 %TODO: antimirov proposition 3.1, needs completion |
426 %TODO: antimirov proposition 3.1, needs completion |
430 \begin{center} |
427 \begin{center} |
498 $(r_1 + r_2) \cdot r_3 \longrightarrow (r_1 \cdot r_3) + (r_2 \cdot r_3)$, |
495 $(r_1 + r_2) \cdot r_3 \longrightarrow (r_1 \cdot r_3) + (r_2 \cdot r_3)$, |
499 |
496 |
500 |
497 |
501 |
498 |
502 |
499 |
503 |
500 \section{The NTIMES Constructor, and the Size Bound and Correctness Proof for it} |
|
501 The NTIMES construct has the following closed form: |
|
502 \begin{verbatim} |
|
503 "rders_simp (RNTIMES r0 (Suc n)) (c#s) = |
|
504 rsimp ( RALTS ( (map (optermsimp r0 ) (nupdates s r0 [Some ([c], n)]) ) ))" |
|
505 \end{verbatim} |
504 %---------------------------------------------------------------------------------------- |
506 %---------------------------------------------------------------------------------------- |
505 % SECTION 1 |
507 % SECTION 1 |
506 %---------------------------------------------------------------------------------------- |
508 %---------------------------------------------------------------------------------------- |
507 |
509 |
508 \section{Adding Support for the Negation Construct, and its Correctness Proof} |
510 \section{Adding Support for the Negation Construct, and its Correctness Proof} |