ninems/ninems.tex
changeset 69 4c7173b7ddca
parent 68 3c73d95cbfef
child 70 cab5eab1f6f1
equal deleted inserted replaced
68:3c73d95cbfef 69:4c7173b7ddca
   742   $\textit{code}(\Stars\,[])$ & $\dn$ & $[\Z]$\\
   742   $\textit{code}(\Stars\,[])$ & $\dn$ & $[\Z]$\\
   743   $\textit{code}(\Stars\,(v\!::\!vs))$ & $\dn$ & $\S :: code(v) \;@\;
   743   $\textit{code}(\Stars\,(v\!::\!vs))$ & $\dn$ & $\S :: code(v) \;@\;
   744                                                  code(\Stars\,vs)$
   744                                                  code(\Stars\,vs)$
   745 \end{tabular}    
   745 \end{tabular}    
   746 \end{center} 
   746 \end{center} 
   747 Here code encodes a value into a bit-sequence by converting Left into $\Z$, Right into $\S$, the start point of a non-empty star iteration into $\S$, and the border where a local star terminates into $\Z$. This conversion is apparently lossy, as it throws away the character information, and does not decode the boundary between the two operands of the sequence constructor. Moreover, with only the bitcode we cannot even tell whether the $\S$s and $\Z$s are for $\Left/\Right$ or $\Stars$. The reason for choosing this compact way of storing information is that the relatively small size of bits can be easily moved around. In order to recover the bitcode back into values, we will need the regular expression as the extra information and decode them back into value:\\
   747 Here code encodes a value into a bit-sequence by converting Left into $\Z$, Right into $\S$, the start point of a non-empty star iteration into $\S$, and the border where a local star terminates into $\Z$. This conversion is apparently lossy, as it throws away the character information, and does not decode the boundary between the two operands of the sequence constructor. Moreover, with only the bitcode we cannot even tell whether the $\S$s and $\Z$s are for $\Left/\Right$ or $\Stars$. The reason for choosing this compact way of storing information is that the relatively small size of bits can be easily moved around. In order to recover the bitcode back into values, we will need the regular expression as the extra information and decode it back into value:\\
   748 %\begin{definition}[Bitdecoding of Values]\mbox{}
   748 %\begin{definition}[Bitdecoding of Values]\mbox{}
   749 \begin{center}
   749 \begin{center}
   750 \begin{tabular}{@{}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
   750 \begin{tabular}{@{}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
   751   $\textit{decode}'\,bs\,(\ONE)$ & $\dn$ & $(\Empty, bs)$\\
   751   $\textit{decode}'\,bs\,(\ONE)$ & $\dn$ & $(\Empty, bs)$\\
   752   $\textit{decode}'\,bs\,(c)$ & $\dn$ & $(\Char\,c, bs)$\\
   752   $\textit{decode}'\,bs\,(c)$ & $\dn$ & $(\Char\,c, bs)$\\