385 The derivative function, written $r\backslash c$, 

   385 The derivative function, written $r\backslash c$, 

   386 takes a regular expression $r$ and character $c$, and

   386 takes a regular expression $r$ and character $c$, and

   387 returns a new regular expression representing

   387 returns a new regular expression representing

   388 the original regular expression's language $L \; r$

   388 the original regular expression's language $L \; r$

   389 being taken the language derivative with respect to $c$.

   389 being taken the language derivative with respect to $c$.

   391 \begin{tabular}{lcl}

   392 \begin{tabular}{lcl}

   392 		$\ZERO \backslash c$ & $\dn$ & $\ZERO$\\  

   393 		$\ZERO \backslash c$ & $\dn$ & $\ZERO$\\  

   393 		$\ONE \backslash c$  & $\dn$ & $\ZERO$\\

   394 		$\ONE \backslash c$  & $\dn$ & $\ZERO$\\

   394 		$d \backslash c$     & $\dn$ & 

   395 		$d \backslash c$     & $\dn$ & 

   395 		$\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\

   396 		$\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\

   397 $(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, [] \in L(r_1)$\\

   398 $(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, [] \in L(r_1)$\\

   398 	&   & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\

   399 	&   & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\

   399 	&   & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\

   400 	&   & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\

   400 	$(r^*)\backslash c$           & $\dn$ & $(r\backslash c) \cdot r^*$\\

   401 	$(r^*)\backslash c$           & $\dn$ & $(r\backslash c) \cdot r^*$\\

   401 \end{tabular}

   402 \end{tabular}

   403 \noindent

   407 \noindent

   404 The most involved cases are the sequence case

   408 The most involved cases are the sequence case

   405 and the star case.

   409 and the star case.

   406 The sequence case says that if the first regular expression

   410 The sequence case says that if the first regular expression

   407 contains an empty string, then the second component of the sequence

   411 contains an empty string, then the second component of the sequence

   692 \end{center}

   696 \end{center}

   693 Sulzmann and Lu used a binary predicate, written $\vdash v:r $,

   697 Sulzmann and Lu used a binary predicate, written $\vdash v:r $,

   694 to indicate that a value $v$ could be generated from a lexing algorithm

   698 to indicate that a value $v$ could be generated from a lexing algorithm

   695 with input $r$. They call it the value inhabitation relation,

   699 with input $r$. They call it the value inhabitation relation,

   696 defined by the rules.

   700 defined by the rules.

   697 \begin{mathpar}

   702 \begin{mathpar}

   698 	\inferrule{\mbox{}}{\vdash \Char \; c : \mathbf{c}} \hspace{2em}

   703 	\inferrule{\mbox{}}{\vdash \Char \; c : \mathbf{c}} \hspace{2em}

   699 

   704 

   700 	\inferrule{\mbox{}}{\vdash \Empty :  \ONE} \hspace{2em}

   705 	\inferrule{\mbox{}}{\vdash \Empty :  \ONE} \hspace{2em}

   701 

   706 

   705 

   710 

   706 \inferrule{\vdash v_2 : r_2}{\vdash \Right \; v_2:r_1 + r_2}

   711 \inferrule{\vdash v_2 : r_2}{\vdash \Right \; v_2:r_1 + r_2}

   707 

   712 

   708 \inferrule{\forall v \in vs. \vdash v:r \land  |v| \neq []}{\vdash \Stars \; vs : r^*}

   713 \inferrule{\forall v \in vs. \vdash v:r \land  |v| \neq []}{\vdash \Stars \; vs : r^*}

   709 \end{mathpar}

   714 \end{mathpar}

   710 \noindent

   717 \noindent

   711 The condition $|v| \neq []$ in the premise of star's rule

   718 The condition $|v| \neq []$ in the premise of star's rule

   712 is to make sure that for a given pair of regular 

   719 is to make sure that for a given pair of regular 

   713 expression $r$ and string $s$, the number of values 

   720 expression $r$ and string $s$, the number of values 

   714 satisfying $|v| = s$ and $\vdash v:r$ is finite.

   721 satisfying $|v| = s$ and $\vdash v:r$ is finite.