# HG changeset patch
# User Chengsong
# Date 1562534538 -3600
# Node ID 3c73d95cbfeffc5fe70bd9c81199dc4ece13271b
# Parent  e974c5477a8ce0b7f89b5935b8da4c2a4a2da6a0
more upd

diff -r e974c5477a8c -r 3c73d95cbfef ninems/ninems.tex
--- a/ninems/ninems.tex	Sun Jul 07 22:18:24 2019 +0100
+++ b/ninems/ninems.tex	Sun Jul 07 22:22:18 2019 +0100
@@ -728,7 +728,7 @@
 bs ::= [] \mid b:bs    
 $
 \end{center}
-They are just a string of bits, the names $S$ and $Z$  here are quite arbitrary, we can use 0 and 1 or any other set of binary symbols to substitute them. They are a compact form of parse trees.
+They are just a string of bits, the names $S$ and $Z$  here are quite arbitrary, we can use 0 and 1 or any other set of binary symbols to substitute them. Bit-codes(or bit-sequences) are a compact form of parse trees.
 Here is how values and bit-codes are related:
 Bitcodes are essentially incomplete values.
 This can be straightforwardly seen in the following transformation: 
@@ -739,14 +739,12 @@
   $\textit{code}(\Left\,v)$ & $\dn$ & $\Z :: code(v)$\\
   $\textit{code}(\Right\,v)$ & $\dn$ & $\S :: code(v)$\\
   $\textit{code}(\Seq\,v_1\,v_2)$ & $\dn$ & $code(v_1) \,@\, code(v_2)$\\
-  $\textit{code}(\Stars\,[])$ & $\dn$ & $[\S]$\\
-  $\textit{code}(\Stars\,(v\!::\!vs))$ & $\dn$ & $\Z :: code(v) \;@\;
+  $\textit{code}(\Stars\,[])$ & $\dn$ & $[\Z]$\\
+  $\textit{code}(\Stars\,(v\!::\!vs))$ & $\dn$ & $\S :: code(v) \;@\;
                                                  code(\Stars\,vs)$
 \end{tabular}    
 \end{center} 
-where $\Z$ and $\S$ are arbitrary names for the bits in the
-bitsequences. 
-Here code encodes a value into a bitsequence 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 during the lexing process. 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:\\
+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:\\
 %\begin{definition}[Bitdecoding of Values]\mbox{}
 \begin{center}
 \begin{tabular}{@{}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}