1 \documentclass[a4paper,UKenglish]{lipics} |
1 \documentclass[a4paper,UKenglish]{lipics} |
|
2 \usepackage{data} |
2 \usepackage{graphic} |
3 \usepackage{graphic} |
3 \usepackage{data} |
|
4 \usepackage{tikz-cd} |
4 \usepackage{tikz-cd} |
5 \usepackage{tikz} |
5 \usepackage{tikz} |
6 |
6 |
7 %\usetikzlibrary{graphs} |
7 %\usetikzlibrary{graphs} |
8 %\usetikzlibrary{graphdrawing} |
8 %\usetikzlibrary{graphdrawing} |
9 %\usegdlibrary{trees} |
9 %\usegdlibrary{trees} |
10 |
|
11 %\usepackage{algorithm} |
10 %\usepackage{algorithm} |
12 \usepackage{amsmath} |
11 \usepackage{amsmath} |
13 \usepackage{xcolor} |
12 \usepackage{xcolor} |
14 \usepackage[noend]{algpseudocode} |
13 \usepackage[noend]{algpseudocode} |
15 \usepackage{enumitem} |
14 \usepackage{enumitem} |
16 \usepackage{nccmath} |
15 \usepackage{nccmath} |
17 \usepackage{soul} |
16 \usepackage{soul} |
18 |
17 %works? |
19 \definecolor{darkblue}{rgb}{0,0,0.6} |
18 \definecolor{darkblue}{rgb}{0,0,0.6} |
20 \hypersetup{colorlinks=true,allcolors=darkblue} |
19 \hypersetup{colorlinks=true,allcolors=darkblue} |
21 \newcommand{\comment}[1]% |
20 \newcommand{\comment}[1]% |
22 {{\color{red}$\Rightarrow$}\marginpar{\raggedright\small{\bf\color{red}#1}}} |
21 {{\color{red}$\Rightarrow$}\marginpar{\raggedright\small{\bf\color{red}#1}}} |
23 |
22 |
100 |
99 |
101 |
100 |
102 If we let the alphabet |
101 If we let the alphabet |
103 where $c$ is selected from |
102 where $c$ is selected from |
104 be $\sum = \{0,1\}$, |
103 be $\sum = \{0,1\}$, |
105 then bitcodes can be defined in a |
104 then we can define the regular expression |
106 regular expression style: |
105 style bitcodes: |
107 |
106 |
108 |
107 |
109 \[ bs ::= \ZERO \mid \ONE |
108 \[ rbs ::= \ZERO \mid \ONE |
110 \mid 1 |
109 \mid 1 |
111 \mid 0 |
110 \mid 0 |
112 \mid bs_1 \cdot bs_2 |
111 \mid rbs_1 \cdot rbs_2 |
113 \mid \sum{bs_{list}} |
112 \mid \sum{rbs_{list}} |
114 \mid bs^* |
113 \mid rbs^* |
115 \] |
114 \] |
116 |
115 |
117 We can define an isomorphism between the regex |
116 This is our list definition of bitcodes: |
118 definition of bitcodes and our list definition of bitcodes: |
117 \begin{center} |
119 \begin{center} |
118 $b ::= 1 \mid 0 \qquad |
120 $b ::= 1 \mid 0 \qquad |
119 bs ::= [] \mid b::bs $ |
121 bs ::= [] \mid b::bs |
120 \end{center} |
122 $ |
121 |
123 \end{center} |
122 Define an isomorphism between bitcodes based on lists |
124 For example we can let $\sigma([])= \ONE$. |
123 and bitcodes based on regular expressions: |
125 But how to define such isomorphism in detail is not explicitly needed for now. |
124 \begin{center} |
|
125 \begin{tabular}{lcl} |
|
126 $\sigma: bit \; list$ & $\Rightarrow$ & $bit \; regex$\\ |
|
127 $\delta: bit$ & $\Rightarrow$ & $bit \; regex$\\ |
|
128 $\sigma([])$ & $=$ & $ \ONE$\\ |
|
129 $\sigma(b::bs)$ & $=$ & $\delta(b) \cdot \sigma(bs)$\\ |
|
130 $\delta(b) $ & $=$ & $b\; as \;a \;regex$ |
|
131 \end{tabular} |
|
132 \end{center} |
126 |
133 |
127 \emph{Annotated regular expressions} can be defined by the following |
134 \emph{Annotated regular expressions} can be defined by the following |
128 grammar using new $bs$ definition: |
135 grammar using the list definition of $bs$ : |
129 |
136 |
130 \begin{center} |
137 \begin{center} |
131 \begin{tabular}{lcl} |
138 \begin{tabular}{lcl} |
132 $\textit{a}$ & $::=$ & $\ZERO$\\ |
139 $\textit{a}$ & $::=$ & $\ZERO$\\ |
133 & $\mid$ & $_{bs}\ONE$\\ |
140 & $\mid$ & $_{bs}\ONE$\\ |
135 & $\mid$ & $_{bs}\sum\,as$\\ |
142 & $\mid$ & $_{bs}\sum\,as$\\ |
136 & $\mid$ & $_{bs}a_1\cdot a_2$\\ |
143 & $\mid$ & $_{bs}a_1\cdot a_2$\\ |
137 & $\mid$ & $_{bs}a^*$ |
144 & $\mid$ & $_{bs}a^*$ |
138 \end{tabular} |
145 \end{tabular} |
139 \end{center} |
146 \end{center} |
140 Let the set of all bitcoded regular expressions be $\textit{BS}$. |
147 %Let the set of all bitcoded regular expressions be $\textit{BS}$. |
141 Let the set of all annotated regular expression be $\textit{AR}$. |
148 %Let the set of all annotated regular expression be $\textit{AR}$. |
142 Let us play with the function $f: \textit{AR} \rightarrow \textit{BS}$ on annotated regular expressions: |
149 Let us play with the function $f: \textit{annotated}\; \textit{regex} \Rightarrow \textit{bit}\; \textit{regex}$ on annotated regular expressions: |
143 \begin{center} |
150 \begin{center} |
144 $f(\ZERO) = \ZERO$\\ |
151 \begin{tabular}{lcl} |
145 $f(_{bs}\ONE) = \textit{bs}$\\ |
152 $f(\ZERO)$ & $=$ & $\ZERO$\\ |
146 $f(_{bs}a) = \textit{bs} $\\ |
153 $f(_{bs}\ONE)$ & $=$ & $\sigma(\textit{bs})$\\ |
147 $f(_{bs}r_1\cdot r_2) = \textit{bs} \cdot( f(r_1) \cdot f(r_2))$\\ |
154 $f(_{bs}a)$ & $=$ & $\sigma(\textit{bs}) $\\ |
148 $f(_{bs}\sum{rs}) = \textit{bs} \cdot \sum\limits_{r \in rs}{f(\textit{r})}$\\ |
155 $f(_{bs}r_1\cdot r_2)$ & $=$ & $\sigma(\textit{bs}) \cdot( f(r_1) \cdot f(r_2))$\\ |
149 $f(_{bs}r^*) = \textit{bs} \cdot((0 \cdot f(r))^*\cdot 1) $ |
156 $f(_{bs}\sum{rs})$ & $=$ & $\sigma(\textit{bs}) \cdot \sum\limits_{r \in rs}{f(\textit{r})}$\\ |
|
157 $f(_{bs}r^*)$ & $=$ & $\sigma(\textit{bs}) \cdot((0 \cdot f(r))^*\cdot 1) $ |
|
158 \end{tabular} |
|
159 \end{center} |
|
160 |
|
161 Now define function $L: bit\;regex \Rightarrow set \; bs$ as follows: |
|
162 \begin{center} |
|
163 \begin{tabular}{lcl} |
|
164 $L(\ZERO)$ & $=$ & $\emptyset$\\ |
|
165 $L(\ONE) $ & $= $ & $\{[]\}$\\ |
|
166 $L(b\;as \; a\;regex) $ & $=$ & $\{b\; as \; a \; bit\}$\\ |
|
167 $L(bs_1 \cdot bs_2)$ & $=$ & $L(bs_1) \times L(bs_2)$\\ |
|
168 $L(\sum bss) $ & $=$ &$\bigcup\limits_{bs \in bss}{L(bs)}$\\ |
|
169 $L(bs^*)$ & $= $ & $\bigcup\limits_{0 \leq n}{(L(bs))^n}$ |
|
170 \end{tabular} |
150 \end{center} |
171 \end{center} |
151 |
172 |
152 We claim that: |
173 We claim that: |
153 \begin{center} |
174 \begin{center} |
154 $f(a) = \{bs \mid a \gg bs\}$. |
175 $L(f(a) )= \{bs \mid a \gg bs\}$. |
155 \end{center} |
176 \end{center} |
|
177 |
|
178 where contains is defined this way: |
|
179 \begin{center} |
|
180 \begin{tabular}{llclll} |
|
181 & & & $_{bs}\ONE$ & $\gg$ & $\textit{bs}$\\ |
|
182 & & & $_{bs}{\bf c}$ & $\gg$ & $\textit{bs}$\\ |
|
183 $\textit{if} \; r_1 \gg \textit{bs}_1$ & $r_2 \; \gg \textit{bs}_2$ |
|
184 & $\textit{then}$ & |
|
185 $_{bs}{r_1 \cdot r_2}$ & |
|
186 $\gg$ & |
|
187 $\textit{bs} @ \textit{bs}_1 @ \textit{bs}_2$\\ |
|
188 |
|
189 $\textit{if} \; r \gg \textit{bs}_1$ & & $\textit{then}$ & |
|
190 $_{bs}{\sum(r :: \textit{rs}})$ & |
|
191 $\gg$ & |
|
192 $\textit{bs} @ \textit{bs}_1 $\\ |
|
193 |
|
194 $\textit{if} \; _{bs}(\sum \textit{rs}) \gg \textit{bs} @ \textit{bs}_1$ & & $\textit{then}$ & |
|
195 $_{bs}{\sum(r :: \textit{rs}})$ & |
|
196 $\gg$ & |
|
197 $\textit{bs} @ \textit{bs}_1 $\\ |
|
198 |
|
199 $\textit{if} \; r \gg \textit{bs}_1\; \textit{and}$ & $_{bs}r^* \gg \textit{bs} @ \textit{bs}_2$ & $\textit{then}$ & |
|
200 $_{bs}r^* $ & |
|
201 $\gg$ & |
|
202 $\textit{bs} @ [0] @ \textit{bs}_1@ \textit{bs}_2 $\\ |
|
203 |
|
204 & & & $_{bs}r^*$ & $\gg$ & $\textit{bs} @ [1]$\\ |
|
205 \end{tabular} |
|
206 \end{center} |
|
207 |
|
208 Moreover, we claim the fact that |
|
209 \begin{center} |
|
210 $L(f(a^*)) != L(f(a^* \backslash a))$ |
|
211 \end{center} |
|
212 This is by $\exists bs \in f(a^*), s.t. bs \notin f(a^* \backslash a)$. |
|
213 Proof for the fact |
|
214 $L(f(a) )= \{bs \mid a \gg bs\}$: |
156 |
215 |
157 \bibliographystyle{plain} |
216 \bibliographystyle{plain} |
158 \bibliography{root} |
217 \bibliography{root} |
159 |
218 |
160 |
219 |