Semester 2, 2018

# M → L Proof

Recall the rules for the languages $$\mathbf{L}$$ (and $$\mathbf{N}$$) and $$\mathbf{M}$$.

$\dfrac{}{\varepsilon\ \mathbf{M}}{M_E}\quad \dfrac{s\ \mathbf{M}}{\texttt{(}s\texttt{)}\ \mathbf{M}}{M_N}\quad \dfrac{s_1\ \mathbf{M}\quad s_2\ \mathbf{M}}{s_1s_2\ \mathbf{M}}{M_J}$

$\dfrac{}{\varepsilon\ \mathbf{L}}{L_E}\quad \dfrac{s\ \mathbf{L}}{\texttt{(}s\texttt{)}\ \mathbf{N}}{N_N}\quad \dfrac{s_1\ \mathbf{N}\quad s_2\ \mathbf{L}}{s_1s_2\ \mathbf{L}}{L_J}$

In this document we will prove that, for any string $$s\ \mathbf{M}$$, the judgement $$s\ \mathbf{L}$$ holds. In other words, that $$\mathbf{M}$$ is a subset of $$\mathbf{L}$$.

To prove the other direction (that $$\mathbf{L}$$ is a subset of $$\mathbf{N}$$), requires simultaneous induction and is the subject of Tute 3.

## 1 Main Proof

We shall proceed by rule induction, based on the assumption $$s\ \mathbf{M}$$. The assumption $$s\ \mathbf{M}$$ could be true via one of the three rules that define $$\mathbf{M}$$. We discharge one case for each of the rules.

### 1.1 Base Case (from rule $$M_E$$)

We know that $$s = \varepsilon$$ if $$s\ \mathbf{M}$$ comes from rule $$M_E$$, so we must now show $$\varepsilon\ \mathbf{L}$$, which is easily proven by rule $$L_E$$.

### 1.2 Inductive Case (from rule $$M_N$$)

We know that $$s = \texttt{(}s'\texttt{)}$$ if $$s\ \mathbf{M}$$ comes from rule $$M_N$$, and that $$s'\ \mathbf{M}$$. This gives us an inductive hypothesis that $$s'\ \mathbf{L}$$.

We can show our goal as follows: $\dfrac{ \dfrac{ \dfrac{ }{s'\ \mathbf{L}}{\mathit{IH}} }{ \texttt{(}s'\texttt{)}\ \mathbf{N}}{N_N} \quad \dfrac{ }{\varepsilon\ \mathbf{L}}{L_E}} { \texttt{(}s'\texttt{)}\ \mathbf{L} }{L_J}$

### 1.3 Inductive Case (from rule $$M_J$$)

We know that $$s = s_1s_2$$ if $$s\ \mathbf{M}$$ comes from rule $$M_J$$, and that $$s_1\ \mathbf{M}$$ and $$s_2\ \mathbf{M}$$, giving us the two inductive hypotheses:

• $$\mathit{IH}_1$$: $$s_1\ \mathbf{L}$$
• $$\mathit{IH}_2$$: $$s_2\ \mathbf{L}$$.

Unfortunately, our goal is $$s_1s_2\ \mathbf{L}$$. If we try to show this goal using rule $$L_J$$, we get stuck, because it requires $$s_1\ \mathbf{N}$$ not $$s_1\ \mathbf{L}$$:

$\dfrac{ \dfrac{ \textbf{???} }{s_1\ \mathbf{N}}\quad \dfrac{ }{s_2\ \mathbf{L}}{\mathit{IH}_2} }{s_1s_2\ \mathbf{L}}{L_J}$

To solve this, we postulate the admissibility of an easier rule:

$\dfrac{ s_1\ \mathbf{L}\quad s_2\ \mathbf{L} }{s_1s_2\ \mathbf{L}}{\mathit{Magic}}$

This magic rule (called a lemma) will be proven in the section below. In the mean time, we can use it to discharge our goal:

$\dfrac{ \dfrac{ }{s_1\ \mathbf{L}}{\mathit{IH}_1}\quad \dfrac{ }{s_2\ \mathbf{L}}{\mathit{IH}_2} }{s_1s_2\ \mathbf{L}}{\mathit{Magic}}$

Thus, by rule induction, and with the help of the lemma proven below, we have shown that $$s\ \mathbf{M}$$ implies $$s\ \mathbf{L}$$.

## 2 Lemma

To prove our final goal, we needed to prove this magic lemma:

$\dfrac{ s_1\ \mathbf{L}\quad s_2\ \mathbf{L} }{s_1s_2\ \mathbf{L}}{\mathit{Magic}}$

We shall prove this lemma by rule induction on the assumption that $$s_1\ \mathbf{L}$$. As there are only two rules ($$L_E$$ and $$L_J$$) that define $$\mathbf{L}$$, we only have to prove two cases.

### 2.1 Base Case (from rule $$L_E$$)

If $$s_1\ \mathbf{L}$$ holds from rule $$L_E$$, that means that $$s_1 = \varepsilon$$. Thus we must show that:

$\dfrac{s_2\ \mathbf{L}}{\varepsilon s_2\ \mathbf{L}}$

Which is clearly a tautology.

### 2.2 Inductive Case (from rule $$L_J$$)

If $$s_1\ \mathbf{L}$$ holds from rule $$L_J$$, that means that $$s_1$$ is made up of two strings $$k_1k_2$$ where $$k_1\ \mathbf{N}\ (*)$$ and $$k_2\ \mathbf{L}$$. As $$k_2\ \mathbf{L}$$ we have the inductive hypothesis that:

$\dfrac{s_2\ \mathbf{L}}{k_2 s_2\ \mathbf{L}}{\mathit{IH}}$

We must show that:

$\dfrac{s_2\ \mathbf{L}}{k_1 k_2 s_2\ \mathbf{L}}$

Taking the premise $$s_2\ \mathbf{L}\ (**)$$ as an assumption, we shall derive the conclusion:

$\dfrac{\dfrac{}{k_1\ \mathbf{N}}{(*)} \quad \dfrac{\dfrac{}{ s_2\ \mathbf{L}}{(**)} }{k_2 s_2\ \mathbf{L}}{\mathit{IH}} } {k_1 k_2 s_2\ \mathbf{L}}{L_J}$

Thus, by rule induction, we have shown the magic lemma needed. No case is needed for rule $$N_N$$ as it is not part of the definition of $$\mathbf{L}$$.

2018-11-16 Fri 19:37