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. Also, Graham Hutton's FP intro course is useful (it's a first year course, so relatively slow, but you can jump to the parts you're interested in or unsure about)
To install the Glasgow Haskell Compiler, 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.
- 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).
- 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?
Haskell Exercise
Define a Haskell data type for boolean expression with the operators of the previous question.data BExpr = ...Using this type definition, implement a function which, given an arbitrarily complicated boolean expression, evaluates it to a boolean value:
evalBExpr :: BExpr -> Bool evalBExpr ....
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.
Last modified: Mon Nov 11 14:02:48 CET 2024