395 %\begin{definition}[Bitdecoding of Values]\mbox{} |
395 %\begin{definition}[Bitdecoding of Values]\mbox{} |
396 \begin{center} |
396 \begin{center} |
397 \begin{tabular}{@{}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}} |
397 \begin{tabular}{@{}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}} |
398 $\textit{decode}'\,bs\,(\ONE)$ & $\dn$ & $(\Empty, bs)$\\ |
398 $\textit{decode}'\,bs\,(\ONE)$ & $\dn$ & $(\Empty, bs)$\\ |
399 $\textit{decode}'\,bs\,(c)$ & $\dn$ & $(\Char\,c, bs)$\\ |
399 $\textit{decode}'\,bs\,(c)$ & $\dn$ & $(\Char\,c, bs)$\\ |
400 $\textit{decode}'\,(\Z\!::\!bs)\;(r_1 + r_2)$ & $\dn$ & |
400 $\textit{decode}'\,(0\!::\!bs)\;(r_1 + r_2)$ & $\dn$ & |
401 $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}\; |
401 $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}\; |
402 (\Left\,v, bs_1)$\\ |
402 (\Left\,v, bs_1)$\\ |
403 $\textit{decode}'\,(\S\!::\!bs)\;(r_1 + r_2)$ & $\dn$ & |
403 $\textit{decode}'\,(1\!::\!bs)\;(r_1 + r_2)$ & $\dn$ & |
404 $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_2\;\textit{in}\; |
404 $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_2\;\textit{in}\; |
405 (\Right\,v, bs_1)$\\ |
405 (\Right\,v, bs_1)$\\ |
406 $\textit{decode}'\,bs\;(r_1\cdot r_2)$ & $\dn$ & |
406 $\textit{decode}'\,bs\;(r_1\cdot r_2)$ & $\dn$ & |
407 $\textit{let}\,(v_1, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}$\\ |
407 $\textit{let}\,(v_1, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}$\\ |
408 & & $\textit{let}\,(v_2, bs_2) = \textit{decode}'\,bs_1\,r_2$\\ |
408 & & $\textit{let}\,(v_2, bs_2) = \textit{decode}'\,bs_1\,r_2$\\ |
409 & & \hspace{35mm}$\textit{in}\;(\Seq\,v_1\,v_2, bs_2)$\\ |
409 & & \hspace{35mm}$\textit{in}\;(\Seq\,v_1\,v_2, bs_2)$\\ |
410 $\textit{decode}'\,(\Z\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\ |
410 $\textit{decode}'\,(0\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\ |
411 $\textit{decode}'\,(\S\!::\!bs)\,(r^*)$ & $\dn$ & |
411 $\textit{decode}'\,(1\!::\!bs)\,(r^*)$ & $\dn$ & |
412 $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r\;\textit{in}$\\ |
412 $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r\;\textit{in}$\\ |
413 & & $\textit{let}\,(\Stars\,vs, bs_2) = \textit{decode}'\,bs_1\,r^*$\\ |
413 & & $\textit{let}\,(\Stars\,vs, bs_2) = \textit{decode}'\,bs_1\,r^*$\\ |
414 & & \hspace{35mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\bigskip\\ |
414 & & \hspace{35mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\bigskip\\ |
415 |
415 |
416 $\textit{decode}\,bs\,r$ & $\dn$ & |
416 $\textit{decode}\,bs\,r$ & $\dn$ & |
426 \emph{Annotated regular expressions} are defined by the following |
426 \emph{Annotated regular expressions} are defined by the following |
427 grammar:%\comment{ALTS should have an $as$ in the definitions, not just $a_1$ and $a_2$} |
427 grammar:%\comment{ALTS should have an $as$ in the definitions, not just $a_1$ and $a_2$} |
428 |
428 |
429 \begin{center} |
429 \begin{center} |
430 \begin{tabular}{lcl} |
430 \begin{tabular}{lcl} |
431 $\textit{a}$ & $::=$ & $\textit{ZERO}$\\ |
431 $\textit{a}$ & $::=$ & $\ZERO$\\ |
432 & $\mid$ & $\textit{ONE}\;\;bs$\\ |
432 & $\mid$ & $_{bs}\ONE$\\ |
433 & $\mid$ & $\textit{CHAR}\;\;bs\,c$\\ |
433 & $\mid$ & $_{bs}{\bf c}$\\ |
434 & $\mid$ & $\textit{ALTS}\;\;bs\,as$\\ |
434 & $\mid$ & $_{bs}\oplus\,as$\\ |
435 & $\mid$ & $\textit{SEQ}\;\;bs\,a_1\,a_2$\\ |
435 & $\mid$ & $_{bs}a_1\cdot a_2$\\ |
436 & $\mid$ & $\textit{STAR}\;\;bs\,a$ |
436 & $\mid$ & $_{bs}a^*$ |
437 \end{tabular} |
437 \end{tabular} |
438 \end{center} |
438 \end{center} |
439 %(in \textit{ALTS}) |
439 %(in \textit{ALTS}) |
440 |
440 |
441 \noindent |
441 \noindent |