COMP[39]161 Concepts of Programming Languages
Semester 2, 2018

M → L Proof

Table of Contents

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

Announcements RSS