Exercises Week 1

Getting started with Haskell

If you haven't programmed in Haskell before, please have a look at the tutorial here. In particular Chapter 8 on expression trees is relevant for this course.
To install it, follow the directions from the here.

Ambiguity and Syntax

Consider the language of boolean expressions (with operators: \(\wedge\) (and), \(\vee\) (or), ¬ (not), constant values True and False , and parentheses).

Give a simple (non-simultaneous) inductive definition for this language using only judgements of the form e Bool.

\begin{eqnarray*} \dfrac{ e_1\; Bool \quad e_2 \;Bool }{ e_1 \vee e_2\; Bool } \qquad \dfrac{ e_1\; Bool \quad e_2 \;Bool }{ e_1 \wedge e_2\; Bool } \\ \phantom{asd}\\ \dfrac{c \in\{true, false\}}{c\;Bool}\qquad \dfrac{e\;Bool}{\neg e\;Bool} \qquad \dfrac{e\;Bool}{(e)\;Bool} \end{eqnarray*}

Show that this language is ambiguous: That is, find an expression that can be parsed in multiple ways.
Now, give a second definition for the same language which is not ambiguous. (to disambiguate: ¬ has the highest precedence; ∧ has a higher precedence than ∨, both are left associative).

\begin{eqnarray*} \dfrac{ e_1\; XBool \quad e_2 \;ABool }{ e_1 \vee e_2\; XBool } \qquad \dfrac{e\;ABool}{e\;XBool} \\ \dfrac{ e_1\; ABool \quad e_2 \;NBool }{ e_1 \wedge e_2\; ABool } \qquad \dfrac{e\;NBool}{e\;ABool}\\ \phantom{asd}\\ \dfrac{c \in\{true, false\}}{c\;NBool}\qquad \dfrac{e\;NBool}{\neg e\;NBool} \qquad \dfrac{e\;XBool}{(e)\;NBool} \end{eqnarray*}

Assume you want to prove a property P for all boolean expressions using rule induction over the rules of the first version. Which cases do you have to consider? What is the induction hypothesis for each case?
- Base Case: \(\mathit{expr} Bool\), since \(expr\) in \(\{\mathit{true}, \mathit{false}\}\) show that \(P (\mathit{true})\), \(P (\mathit{false})\) hold.
- Induction Steps
  - Case 1: \(\mathit{expr} = ¬ \mathit{expr}_1\). Show: \(P(expr)\). (a1) and I.H. can (and usually have to) be used for the proof.
    - (a1) \(\mathit{expr}_ 1\; Bool\)
    - I.H.: \(P(\mathit{expr}_ 1 )\)
  - Case 2: \(\mathit{expr} = (\mathit{expr}_ 1 )\),
    - (a1) \(\mathit{expr}_ 1 Bool\)
    - I.H.: \(P(\mathit{expr}_ 1 )\) show: \(P(expr)\)
- Case 3: \(\mathit{expr} = \mathit{expr}_ 1 \vee \mathit{expr}_ 2\),
  - (a1) \(\mathit{expr}_ 1\; Bool\)
  - (a2) \(\mathit{expr}_ 2\; Bool\)
  - I.H.: \(P(\mathit{expr}_ 1 ), P(\mathit{expr}_ 2)\)
- Case 4: \(\mathit{expr} = \mathit{expr}_ 1 \wedge \mathit{expr}_ 2\),
  - (a1) \(\mathit{expr}_ 1 \; Bool\)
  - (a2) \(\mathit{expr}_ 2 \; Bool\)
  - I.H.: \(P(\mathit{expr}_ 1 )\), \(P(\mathit{expr}_ 2)\)

Simultaneous Induction

In the lecture, we discussed two alternative definitions of a language of parenthesised expressions:

\begin{eqnarray*} (M-1)&\qquad\phantom{a} & {\dfrac{}{{\epsilon}\;\mathit{M}}}\\ \phantom{a}\\ (M-2)& & {\dfrac{{s_1}\;\mathit{M}\quad{s_2}\;\mathit{M}}{{s_1s_2}\;\mathit{M}}}\\ \phantom{a}\\ (M-3)&& {\dfrac{{s}\;\mathit{M}}{{\mathtt{(}\mathit{s}\mathtt{)}}{\;M}}} \end{eqnarray*}

and

\begin{eqnarray*} (L-1) &\qquad\phantom{a}& \dfrac{}{{\epsilon}\;\mathit{L}}\qquad\\ \phantom{a}\\ (L-2) && \dfrac{{s_1}\;\mathit{N}\quad{s_2}\;\mathit{L}}{{s_1 s_2}\;\mathit{L}}\\ \phantom{a}\\ (N-1) && \dfrac{{s}\;\mathit{L}}{{\mathtt{(}s\mathtt{)}}\;\mathit{N}}\\ \end{eqnarray*}

In the lecture notes, there is a proof that \(s\; \mathit{M}\) implies \(s\; \mathit{L}\) . Show that the reverse direction of the implication is also true, and therefore \(M\) defines the same language as \(L\).

Hint: similar to the proof discussed in the notes, it is not possible to prove it using straight forward rule induction. However, first try induction and to see what is missing, then adjust your proof accordingly.

Solution Instead of proving that \(s\; L\) implies \(s\; M\), we prove a stronger, more general property (as suggested in the lecture notes, proofs over sets which are defined via simoultaneuos induction). We prove that \(s\; L\) or \(s\; L\) implies \(s\; N\) implies \(s\; M\). We now have to do three proofs (for the two rules for \(L\) and the rule for \(N\), but our induction hypothesis is now not only true for substrings in \(L\), but also in \(N\). If \(s\; L\) or \(s\; N\), then either (Case 1/Base case) \(s = \epsilon\) or (Case 2) there are two strings \(s_1\) and \(s_2\) with \(s = s_1 s_2\), and \(s_1\; N\) and \(s_2\; L\), or (Case 3) \(s = \mathtt{(}s_1\mathtt{)}\) for some \(s_2\; N\)

Case (1): in this case, we can directly infer \(s\; M\) as

\begin{eqnarray*} (M-1) &\qquad\phantom{a}& \dfrac{}{{\epsilon}\;\mathit{M}}\qquad\\ \phantom{a}\\ \end{eqnarray*}

Case (2): \(s = s_1 s_2\), for
- (a1) \(s_1\; N\)
- (a2) \(s_2\; L\)
- (I.H.-1) \(s_1\; M\)
- (I.H.-2) \(s_2\; M\)

We need to show that \(s_1 s_2 \;M\):

\begin{eqnarray*} \dfrac{ \dfrac{\dfrac{\dfrac{}{s_1\;N}(a1) \quad \dfrac{}{\epsilon\;L}(L-1) }{s_1\;L}(L-2) }{s_1\;M}(I.H.-1)\qquad \dfrac{\dfrac{}{s_2\;L}(a2)}{s_2\;M}(I.H.-2) }{ s_1 s_2\; M }(M-2) \end{eqnarray*}

Case (3): \(s = \mathtt{(} s_1 \mathtt{)}\), for

(a) \(s_1\; L\)
(I.H.) \(s_1\; M\)

We need to show that \( \mathtt{(} s_1 \mathtt{)}\;M\): \begin{eqnarray*} \dfrac{ \dfrac{}{s_1\;M}(I.H.) }{ \mathtt{(} s_1 \mathtt{)}\; M }(M-3) \end{eqnarray*}

Advanced exercises

If you are already familiar with Haskell as well as the theory part covered this week, you might find the advanced exercises more interesting.

(solutions are separate)

Last modified: Thu Aug 1 22:12:44 CEST 2024