Tute (Week 2)

Consider the (++) operator in Haskell.

(++) :: [a] -> [a] -> [a]
[]     ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)

1. State the formal properties of left identity, right identity and associativity for (++).
2. Try to prove these properties. In some cases, you may need to perform induction on the structure of lists. The base case of the induction will be for the empty list, and the inductive case will be to show your property for a list (x:xs), assuming the property for the list xs (this assumption is called the inductive hypothesis).

Red-black trees are binary search trees where each node in the tree is coloured either red or black. In C, red-black trees could, for example, be encoded with the following user-defined data type:

typedef struct redBlackNode* link;

struct redBlackNode { 
  Item item; // Item type defined elsewhere
  link left, right; 
  int  isRed; // 1 if node is red, 0 if black
};

and in Haskell (again, we assume the Item type is defined elsewhere)

data RBColour
  = Red
  | Black

data RBTree
  = RBLeaf
  | RBNode RBColour Item RBTree RBTree 

1. The user defined Haskell data type characterises a set of terms as RBTree. List the inference rules to define the same set. Assume there already exists a judgement \(x\ \mathbf{Item}\) which is derivable for all \(x\) in the Item type.
2. In a proper red-black tree, we can never have a red parent node with a red child, although it is possible to have black nodes with black children. Moreover, the root node cannot be red. Therefore, not all terms of type RBTree are real red-black trees. Define inference rules for a property \(t\ \mathbf{OK}\), such that \(\mathbf{OK}\) is derivable if the term \(t\) represents a proper red-black tree.

Consider the language of boolean expressions (with operators: \(\land\) (and), \(\lor\) (or), \(\neg\) (not), constant values \(\mathit{True}\) and \(\mathit{False}\), and parentheses).

1. Give a simple (non-simultaneous) inductive definition for this language using only judgements of the form \(e\ \mathbf{Bool}\).
2. Identify how this language is ambiguous: That is, find an expression that can be parsed in multiple ways.
3. Now, give a second definition for the same language which is not ambiguous. (to disambiguate: \(\neg\) has the highest precedence; \(\land\) has a higher precedence than \(\lor\), both are left associative).
4. 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?

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

\[ \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 the lecture, we showed that if \(s\ \mathbf{M}\), then \(s\ \mathbf{L}\). Show that the reverse direction of the implication is also true, and therefore \(\mathbf{M}\) defines the same language as \(\mathbf{L}\).

Hint: similar to the proof discussed in the lecture, 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.