\documentclass{article}

\usepackage[utf8]{inputenc}

\usepackage[english]{babel}

\usepackage{listings}

 \usepackage{amsthm}

 \usepackage[margin=0.5in]{geometry}

\theoremstyle{theorem}

\newtheorem{theorem}{Theorem}

\theoremstyle{lemma}

\newtheorem{lemma}{Lemma}

\theoremstyle{definition}

 \newtheorem{definition}{Definition}

\begin{document}

This is a sketch proof for the correctness of the algorithm ders\_simp.

\section{Function Definitions}

\begin{definition}{Bits}

\begin{verbatim}

abstract class Bit

case object Z extends Bit

case object S extends Bit

case class C(c: Char) extends Bit

type Bits = List[Bit]

\end{verbatim}

\end{definition}

\begin{definition}{Annotated Regular Expressions}

\begin{verbatim}

abstract class ARexp 

case object AZERO extends ARexp

case class AONE(bs: Bits) extends ARexp

case class ACHAR(bs: Bits, f: Char) extends ARexp

case class AALTS(bs: Bits, rs: List[ARexp]) extends ARexp 

case class ASEQ(bs: Bits, r1: ARexp, r2: ARexp) extends ARexp 

case class ASTAR(bs: Bits, r: ARexp) extends ARexp 

\end{verbatim}

\end{definition}

\begin{definition}{bnullable}

\begin{verbatim}

  def bnullable (r: ARexp) : Boolean = r match {

    case AZERO => false

    case AONE(_) => true

    case ACHAR(_,_) => false

    case AALTS(_, rs) => rs.exists(bnullable)

    case ASEQ(_, r1, r2) => bnullable(r1) && bnullable(r2)

    case ASTAR(_, _) => true

  }

\end{verbatim}

\end{definition}

\begin{definition}{ders\_simp}

\begin{verbatim}

def ders_simp(r: ARexp, s: List[Char]): ARexp = {

 s match {

   case Nil => r 

   case c::cs => ders_simp(bsimp(bder(c, r)), cs)

 }

}\end{verbatim}

\end{definition}

\begin{definition}{bder}

\begin{verbatim}

def bder(c: Char, r: ARexp) : ARexp = r match {

 case AZERO => AZERO

 case AONE(_) => AZERO

 case ACHAR(bs, f) => if (c == f) AONE(bs:::List(C(c))) else AZERO

 case AALTS(bs, rs) => AALTS(bs, rs.map(bder(c, _)))

 case ASEQ(bs, r1, r2) => {

  if (bnullable(r1)) AALT(bs, ASEQ(Nil, bder(c, r1), r2), fuse(mkepsBC(r1), bder(c, r2)))

  else ASEQ(bs, bder(c, r1), r2)

  }

 case ASTAR(bs, r) => ASEQ(bs, fuse(List(S), bder(c, r)), ASTAR(Nil, r))

}

\end{verbatim}

\end{definition}

\begin{definition}{bsimp}

\begin{verbatim}

  def bsimp(r: ARexp): ARexp = r match {

    case ASEQ(bs1, r1, r2) => (bsimp(r1), bsimp(r2)) match {

        case (AZERO, _) => AZERO

        case (_, AZERO) => AZERO

        case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)

        case (r1s, r2s) => ASEQ(bs1, r1s, r2s)

    }

    case AALTS(bs1, rs) => {

      val rs_simp = rs.map(bsimp)

      val flat_res = flats(rs_simp)

      val dist_res = distinctBy(flat_res, erase)

      dist_res match {

        case Nil => AZERO

        case s :: Nil => fuse(bs1, s)

        case rs => AALTS(bs1, rs)  

      }

    }

    //case ASTAR(bs, r) => ASTAR(bs, bsimp(r))

    case r => r

  }

\end{verbatim}

\end{definition}

\begin{definition}{sub-parts of bsimp}

\begin{itemize}

\item{flats}\\

flattens the list.

\item{dB}\\

means distinctBy

\item{Co}\\

The last matching clause of the function bsimp, namely

      dist\_res match {

        case Nil => AZERO

        case s :: Nil => fuse(bs1, s)

        case rs => AALTS(bs1, rs)  

      }

\end{itemize}

\end{definition}

\begin{definition}{fuse}

\begin{verbatim}

  def fuse(bs: Bits, r: ARexp) : ARexp = r match {

    case AZERO => AZERO

    case AONE(cs) => AONE(bs ++ cs)

    case ACHAR(cs, f) => ACHAR(bs ++ cs, f)

    case AALTS(cs, rs) => AALTS(bs ++ cs, rs)

    case ASEQ(cs, r1, r2) => ASEQ(bs ++ cs, r1, r2)

    case ASTAR(cs, r) => ASTAR(bs ++ cs, r)

  }

\end{verbatim}

\end{definition}

\begin{definition}{mkepsBC}

\begin{verbatim}

  def mkepsBC(r: ARexp) : Bits = r match {

    case AONE(bs) => bs

    case AALTS(bs, rs) => {

      val n = rs.indexWhere(bnullable)

      bs ++ mkepsBC(rs(n))

    }

    case ASEQ(bs, r1, r2) => bs ++ mkepsBC(r1) ++ mkepsBC(r2)

    case ASTAR(bs, r) => bs ++ List(Z)

  }

\end{verbatim}

\end{definition}

\begin{definition}{mkepsBC equicalence}

\\

Given 2 nullable annotated regular expressions r1, r2, if mkepsBC(r1) == mkepsBC(r2)

then r1 and r2 are mkepsBC equivalent, denoted as r1 $\sim_{m\epsilon}$ r2

\end{definition}

\begin{definition}{shorthand notation for ders}

\\For the sake of reducing verbosity, we sometimes use the shorthand notation

$d_{c}(r)$ for the function application bder(c, r) and $s(r)$(s here stands for simplification) for the function application bsimp(r) .

\\We omit the subscript when it is clear from context what that character is and write $d(r)$ instead of $d_{c}(r)$. 

\\And we omit the parentheses when no confusion can be caused. For example ders\_simp(c, r) can be written as $s(d_{c}(r))$ or even $s d r$ as we know the derivative operation is w.r.t the character c. Here the s and d are more like operators that take an annotated regular expression as an input and return an annotated regular expression as an output

\end{definition}

\begin{definition}{mkepsBC invariant manipulation of bits and notation}\\

ALTS(bs, ALTS(bs1, rs1), ALTS(bs2, rs2)) $\sim_{m\epsilon}$ ALTS(bs, rs1.map(fuse(bs1, \_)) ++ rs2.map(fuse(bs2, \_)) ). \\

We also use $bs2>>rs2 $ as a shorthand notation for rs2.map(fuse(bs2,\_)).

\end{definition}

\begin{definition}{distinctBy operation expressed in a different way--how it transforms the list}\\

Given two lists rs1 and rs2, we define the operation $--$:\\

$rs1 -- rs2 := [r \in rs1 |  r \notin rs2]$

Note that the order is preserved as in the original list.

\end{definition}

\section{Main Result}

\begin{lemma}{simplification function does not simplify an already simplified regex}\\

bsimp(r) == bsimp(bsimp(r)) holds for any annotated regular expression r.

\end{lemma}

\begin{lemma}{simp and mkeps}\\

When r is nullable, we have that

mkeps(bsimp(r)) == mkeps(r)

\end{lemma}

\begin{lemma}{mkeps equivalence  w.r.t some syntactically different regular expressions(1 ALTS)}\\

When one of the 2 regular expressions $s(r_1)$ and $s(r_2)$ is ALTS(bs1, rs1), we have that $ds(ALTS(bs, r1, r2)) \sim_{m\epsilon} d(ALTS(bs, sr_1, sr_2))$

\end{lemma}

\begin{proof}

By opening up one of the alts and show no additional changes are made.

\end{proof}

\begin{lemma}{mkepsBC equivalence w.r.t syntactically different regular expressions(2 ALTS)}\\

$sr_1 = ALTS(bs1, rs1)$ and $sr_2 = ALTS(bs2, rs2)$ we have  $  d(sr_1 +sr_2 ) \sim_{m\epsilon} d(ALTS(bs, bs1>>rs1 ++ bs2>>rs2))$ 

\end{lemma}

\begin{proof}

We are just fusing bits inside here, there is no other structural change.

\end{proof}

\begin{lemma}{mkepsBC equivalence w.r.t syntactically different regular expressions(2 ALTS+ some deletion)}\\

$d Co(ALTS(bs, dB(bs1>>rs1 ++ bs2>>rs2))) \sim_{m\epsilon} d Co(ALTS(bs, dB(bs1>>rs1 ++ ((bs2>>rs2)--rs1)        ))) $ 

\end{lemma}

\begin{proof}

The removed parts have already appeared before in $rs_1$, so if any of them is truly nullable and is chosen as the mkeps path, it will have been traversed through in its previous counterpart.\\

(We probably need to switch the position of lemma5 and lemma6)

\end{proof}

\begin{lemma}{after opening two previously simplified alts up into terms, length must exceed 2}\\

 $d Co(ALTS(bs, rs        )) \sim_{m\epsilon} d(ALTS(bs, rs))$ if $rs$ is a list of length greater than or equal to 2.

\end{lemma}

\begin{proof}

As suggested by the title of this lemma

\end{proof}

\begin{theorem}{Correctness Result}

\begin{itemize}

\item{}

When s is a string in the language L(ar), \\

ders\_simp(ar, s)  $\sim_{m\epsilon}$ ders(ar, s), \\

\item{}

when s is not a string of the language L(ar)

ders\_simp(ar, s) is not nullable

\end{itemize}

\end{theorem}

\begin{proof}{Split into 2 parts.}

\begin{itemize}

\item

When we have an annotated regular expression ar and a string s that matches ar, by the correctness of the algorithm ders, we have that ders(ar, s) is nullable, and that mkepsBC will extract the desired bits for decoding the correct value v for the matching, and v is a POSIX value. Now we prove that mkepsBC(ders\_simp(ar, s)) yields the same bitsequence.

\\

We first open up the ders\_simp function into nested alternating sequences of ders and simp.

Assume that s = $c_1...c_n$($n \geq 1$ ) where each of the $c_i$ are characters. 

Then $ders\_simp(ar, s)$ = $s(d_{c_n}(...s(d_{c_1}(r))...))$ = $sdsd......sdr$. If we can prove that

$sdr \sim_{m\epsilon} dsr$ holds for any regular expression and any character, then we are done. This is because then we can push ders operation inside and move simp operation outside and have that $sdsd...sdr \sim_{m\epsilon} ssddsdsd...sdr \sim_{m\epsilon} ... \sim_{m\epsilon} s....sd....dr$ and using lemma1 we have that $s...sd....dr = sd...dr$. By lemma2, we have $RHS \sim_{m\epsilon} d...dr$.\\

Now we proceed to prove that $sdr \sim_{m\epsilon} dsr$. This can be reduced to proving $dr \sim_{m\epsilon} dsr$ as we know that $dr \sim_{m\epsilon} sdr$ by lemma2.\\

we use an induction proof. Base cases are omitted. Here are the 3 inductive cases.

\begin{itemize}

\item{$r_1+r_2$}

$r_1+r_2$\\

The most difficult case is when $sr1$ and $sr2$ are both ALTS, so that they will be opened up in the flats function and some terms in sr2 might be deleted. Or otherwise we can use the argument that $d(r_1+r_2) = dr_1 + dr_2  \sim_{m\epsilon} dsr_1 + dsr_2 \sim_{m\epsilon} ds(r_1+r_2)$,

 the last equivalence being established by lemma3.

When $s(r_1), s(r_2)$ are both ALTS, we have to be more careful for the last equivalence step, namelly, $dsr_1 + dsr_2 \sim_{m\epsilon} ds(r_1+r_2)$. \\

We have that $LHS = dsr_1 + dsr_2 = d(sr_1 +sr_2)$. Since $sr_1 = ALTS(bs1, rs1)$ and $sr_2 = ALTS(bs2, rs2)$ we have  $  d(sr_1 +sr_2 ) \sim_{m\epsilon} d(ALTS(bs, bs1>>rs1 ++ bs2>>rs2))$ by lemma4.

On the other hand, $RHS = ds(ALTS(bs, r1, r2)) \sim_{m\epsilon}d Co(ALTS(bs, dB(flats(s(r1), s(r2))))) == d Co(ALTS(bs, dB(bs1>>rs1 ++ bs2>>rs2)))$ by definition of bsimp and flats.\\  $d Co(ALTS(bs, dB(bs1>>rs1 ++ bs2>>rs2))) \sim_{m\epsilon} d Co(ALTS(bs, (bs1>>rs1 ++ ((bs2>>rs2)--rs1)        ))) $ by lemma5.\\ $d Co(ALTS(bs, (bs1>>rs1 ++ ((bs2>>rs2)--rs1)        ))) \sim_{m\epsilon} d(ALTS(bs, bs1>>rs1 ++ (bs2>>rs2)--rs1))$ by lemma6. \\

 Using lemma5 again, we have  $d(ALTS(bs, bs1>>rs1 ++ (bs2>>rs2)--rs1)) \sim_{m\epsilon} d(ALTS(bs, bs1>>rs1 ++ bs2>>rs2))$.\\

 This completes the proof.

\item{$r*$}\\

s(r*) = s(r).

\item{$r1.r2$}\\

using previous.

\end{itemize}

\item

Proof of second part of the theorem: use a similar structure of argument as in the first part.

\end{itemize}

\end{proof}

\end{document}

%The second part might still need some more development.

%When s is not in the set L(ar), we have that s = s1@s2 s.t. s1 $\in$ L(ar), and any longer string that is a prefix of s does not belong to L(ar).\\

%By first part of proof, we have ders(ar, s1) $\sim_{m\epsilon}$ ders\_simp(ar, s1)

%.....somehow show that by correctness, der(c, ders\_simp(ar, s1)) must be not nullable. But this will need that L(ders(ar, s1)) == L(ders\_simp(ar, s1)). By part 1 of proof we only have that for any string s1c s.t. s1c $\in$ L(ar) (which is equivalent to s $\in$ L(ders(ar, s1))), s is also in L(ders\_simp(ar, s1)). That is an inclusion, not an equality. c not in L(ders(ar, s1)) does not imply c not in L(ders\_simp(ar, s1))

%So this path stuck here.