etnms/20200205.tex
changeset 125 788f4aa28bc5
parent 124 d9d2da923b7f
equal deleted inserted replaced
124:d9d2da923b7f 125:788f4aa28bc5
  1382 version of $\simp$.
  1382 version of $\simp$.
  1383 
  1383 
  1384 Why?
  1384 Why?
  1385 
  1385 
  1386 During the first derivative operation, 
  1386 During the first derivative operation, 
  1387 $\rup\backslash a=(    _0[ \ONE\cdot {\bf b}] + _1( _0[ _1\ONE \cdot {\bf a}^*] + [ \ONE \cdot {\bf a}])      )$ 
  1387 \begin{center}
  1388 is in the form of a sequence regular expression with
  1388 $\rup\backslash a=(    _0[ \ONE\cdot {\bf b}] + _1( _0[ _1\ONE \cdot {\bf a}^*] + [ \ONE \cdot {\bf a}])      )$,
  1389 two components, the first
  1389 \end{center}
  1390 one $\ONE + \ZERO$ being nullable. 
  1390 \noindent
  1391 Recall again the simplification function definition:
  1391  the second derivative gives us
  1392 \begin{center}
       
  1393   \begin{tabular}{@{}lcl@{}}
       
  1394    
       
  1395   $\textit{simp} \; (\textit{SEQ}\;bs\,a_1\,a_2)$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp}  \; a_2) \; \textit{match} $ \\
       
  1396    &&$\quad\textit{case} \; (\ZERO, \_) \Rightarrow  \ZERO$ \\
       
  1397    &&$\quad\textit{case} \; (\_, \ZERO) \Rightarrow  \ZERO$ \\
       
  1398    &&$\quad\textit{case} \;  (\ONE, a_2') \Rightarrow  \textit{fuse} \; bs \;  a_2'$ \\
       
  1399    &&$\quad\textit{case} \; (a_1', \ONE) \Rightarrow  \textit{fuse} \; bs \;  a_1'$ \\
       
  1400    &&$\quad\textit{case} \; (a_1', a_2') \Rightarrow  \textit{SEQ} \; bs \; a_1' \;  a_2'$ \\
       
  1401 
       
  1402   $\textit{simp} \; (\textit{ALTS}\;bs\,as)$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\
       
  1403   &&$\quad\textit{case} \; [] \Rightarrow  \ZERO$ \\
       
  1404    &&$\quad\textit{case} \; a :: [] \Rightarrow  \textit{fuse bs a}$ \\
       
  1405    &&$\quad\textit{case} \;  as' \Rightarrow  \textit{ALTS}\;bs\;as'$\\ 
       
  1406 
       
  1407    $\textit{simp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$   
       
  1408 \end{tabular}    
       
  1409 \end{center}    
       
  1410 
       
  1411 \noindent
       
  1412 
       
  1413 and the difinition of $\flatten$:
       
  1414  \begin{center}
  1392  \begin{center}
  1415  \begin{tabular}{c c c}
  1393 $\rup\backslash a=(_0( [\ZERO\cdot {\bf b}] + 0) + _1( _0( [\ZERO\cdot {\bf a}^*] + _1[ _1\ONE \cdot {\bf a}^*]) + _1( [\ZERO \cdot {\bf a}] + \ONE)  ))$,
  1416  $\flatten \; []$ & $\dn$ & $[]$\\
  1394 \end{center}
  1417  $\flatten \; \ZERO::rs$ & $\dn$ & $rs$\\
  1395 
  1418  $\flatten \;(_{\textit{bs}_1}\oplus \textit{rs}_1 ::rs)$ & $\dn$ & $(\map \, (\fuse \, \textit{bs}_1) \,\textit{rs}_1) ::: \flatten(rs)$\\
  1396 \noindent
  1419  $\flatten \; r :: rs$ & $\dn$ & $r::\flatten(rs)$
  1397 and this simplifies to
  1420  \end{tabular}
  1398 \begin{center}
  1421  \end{center}
  1399 $ _1(_{011}{\bf a}^* +  _1\ONE)  $ 
  1422  
  1400 \end{center}
  1423  \noindent
  1401 
  1424 
  1402 If, after the first derivative we apply simplification we get
  1425 If we call $\simp$ on $\rup\backslash a$,
  1403 $(_0{\bf b}  + _{101}{\bf  a}^* + _{11}{\bf a}  )$,
  1426 then we would go throught the third clause of 
  1404 and we do another derivative, getting
  1427 the sequence case:$\quad\textit{case} \;  (\ONE, a_2') \Rightarrow  \textit{fuse} \; bs \;  a_2'$.
  1405 $(\ZERO  + (_{101}(\ONE \cdot _1{\bf a}^*)+_{11}\ONE)$,
  1428 The $\ZERO$ of $(_0\ONE  + \ZERO)$ is thrown away 
  1406 which simplifies to 
  1429 by $\flatten$ and 
  1407 \begin{center}
  1430 $_0\ONE$ merged into $(_0a  +  _1a^*)$ by simply
  1408 $ (_{1011}a^* +  _{11}\ONE)  $ 
  1431 putting its bits($_0$) to the front of the second component:
  1409 \end{center}
  1432  ${\bf_0}(_0a  +  _1a^*)$. 
  1410 
  1433  After a second derivative operation,
  1411 
  1434  namely, $(_0(_0a  +  _1a^*))\backslash a$, we get 
       
  1435  $
       
  1436  _0(_0 \ONE  +  _1(_1\ONE \cdot a^*))
       
  1437  $, and this simplifies to $_0(_0 \ONE  +  _{11} a^*)$
       
  1438  by the third clause of the alternative case:
       
  1439  $\quad\textit{case} \;  as' \Rightarrow  \textit{ALTS}\;bs\;as'$.
       
  1440 The outmost bit $_0$ stays with 
       
  1441 the outmost regular expression, rather than being fused to
       
  1442 its child regular expressions, as what we will later see happens
       
  1443 to $\simp(\rup\backslash \, s)$.
       
  1444 If we choose to not simplify in the midst of derivative operations,
       
  1445 but only do it at the end after the string has been exhausted, 
       
  1446 namely, $\simp(\rup\backslash \, s)=\simp((\rup\backslash a)\backslash a)$,
       
  1447 then at the {\bf second} derivative of 
       
  1448 $(\rup\backslash a)\bf{\backslash a}$
       
  1449 we will go throught the clause of $\backslash$:
       
  1450 \begin{center}
       
  1451 \begin{tabular}{lcl}
       
  1452 $(\textit{SEQ}\;bs\,a_1\,a_2)\,\backslash c$ & $\dn$ &
       
  1453      $(when \; \textit{bnullable}\,a_1)$\\
       
  1454 					       & &$\textit{ALTS}\,bs\,List(\;\;(\textit{SEQ}\,[]\,(a_1\,\backslash c)\,a_2),$\\
       
  1455 					       & &$(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))\;\;)$\\
       
  1456 \end{tabular}
       
  1457 \end{center}
       
  1458 
       
  1459 because
       
  1460 $\rup\backslash a = (_0\ONE  + \ZERO)(_0a  +  _1a^*)$  
       
  1461 is a sequence
       
  1462 with the first component being nullable
       
  1463 (unsimplified, unlike the first round of running$\backslash_{simp}$).
       
  1464 Therefore $((_0\ONE  + \ZERO)(_0a  +  _1a^*))\backslash a$ splits into
       
  1465 $\rup\backslash a=(_0( [\ZERO\cdot {\bf b}] + 0) + _1( _0( [\ZERO\cdot a^*] + _1[ _1\ONE \cdot {\bf a}^*]) + _1( [\ZERO \cdot {\bf a}] + \ONE)  ))$ 
       
  1466 
       
  1467 $([(\ZERO + \ZERO)\cdot(_0a  +  _1a^*)] + _0( _0\ONE  + _1[_1\ONE \cdot a^*]))$.
       
  1468 After these two successive derivatives without simplification,
       
  1469 we apply $\simp$ to this regular expression, which goes through
       
  1470 the alternative clause, and each component of 
       
  1471 $([(\ZERO + \ZERO)\cdot(_0a  +  _1a^*)] + _0( _0\ONE  + _1[_1\ONE \cdot a^*]))$ 
       
  1472 will be simplified, giving us the list:$[\ZERO, _0(_0\ONE  + _{11}a^*)]$
       
  1473 This list is then "flattened"--$\ZERO$ will be
       
  1474 thrown away by $\textit{flatten}$; $ _0(_0\ONE  + _{11}a^*)$
       
  1475 is opened up to make the list consisting of two separate elements 
       
  1476 $_{00}\ONE$ and $_{011}a^*$, note that $flatten$ 
       
  1477 $\fuse$s the bit(s) $_0$ to the front of $_0\ONE $ and $_{11}a^*$.
       
  1478 The order of simplification, which impacts the order that alternatives
       
  1479 are  opened up, causes
       
  1480 the bits to be moved differently.
       
  1481 
  1412 
  1482 
  1413 
  1483 
  1414 
  1484 We have changed the algorithm to suppress the old
  1415 We have changed the algorithm to suppress the old
  1485 counterexample, but this gives rise to new counterexamples.
  1416 counterexample, but this gives rise to new counterexamples.