Lists

Definition. A list is an ordered sequence of objects. A list is either the empty list ($\lambda$), or the result of $\text{prepend}(e, l)$ for some object $e$ and list $l$.

\begin{equation} \begin{split} \text{\em first}(\text{prepend}(e, l)) &= e
\text{\em rest}(\text{prepend}(e, l)) &= l
\text{\em empty}(\text{prepend}(e, l)) &= \text{\bf False}
\text{\em empty}(\text{\bf null}) &= \text{\bf True}
\end{split} \end{equation}

Definition. The length of a list, $p$, is: \begin{equation} \begin{split} \begin{cases} 0 & \text{if}\ p\ \text{is \bf null}
\text{\em length}(q) + 1 & \text{otherwise}\ p = \text{\em prepend}(e, q)\ \text{for some object}\ e\ \text{and some list}\ q
\end{cases} \end{split} \end{equation}

def list_length(l):
    if list_empty(l):
        return 0
    else:
        return 1 + list_length(list_rest(l))

Prove: for all lists, $p$, list_length(p) returns the length of the list $p$.

Concatenation

Definition. The concatenation of two lists, $p = (p_1, p_2, \cdots, p_n)$ and $q = (q_1, q_2, \cdots, q_m)$ is $$(p_1, p_2, \cdots, p_n, q_1, q_2, \cdots, q_m).$$

Provide a constructuve definition of concatenation.

Note that $\text{prepend}(p,q)$ is not a good idea for two reasons. If we use this definition, then the first element of the constructed list will be the object (list) $p$ (as a whole) rather than the first element $p_1$ of the list $p$. Also, if we want to only define lists of specific objects, for example integers, we can still use the same recursive/constructive definition of lists by substituting “object” with “integer”, but in that case $\text{prepend}(p,q)$ will not even well defined, as it can only accept integers as first input.

#

Structural Induction

To prove proposition $P(x)$ for element $x \in D$ where $D$ is a recursively-constructed data type, we do two things:

1. Show $P(x)$ is true for all $x \in D$ that are defined using base cases.
2. Show that if $P(y)$ is true for element $y$ and $x$ is constructed from $y$ using any “construct case” rules, then $P(x)$ is true as well.

Comparing Various forms of Induction

\begin{center} \begin{tabular}{lccc} & {\bf Regular Induction} & {\bf Invariant Principle} & {\bf Structural Induction} \ \hline Works on: & natural numbers & state machines & data types
To prove $P(\cdot)$ & {\em for all natural numbers} & {\em for all reachable states} & {\em for all data type objects}
Prove {\bf base case(s)} & $P(0)$ & $P(q_0)$ & $P(\text{base object(s)})$
and {\bf inductive step} & $\forall m \in \mathbb{N} \ldotp$ & $\forall (q, r) \in G \ldotp $ & $\forall s \in \text{\em Type} \ldotp$
& $P(m) \implies P(m+1)$ & $P(q) \implies P®$ & $P(s) \implies P(t)$
& & & $\quad \forall t\ \text{constructable from}\ s$ \ \end{tabular} \end{center}

# ##

Prove. For any two lists, $p$ and $q$, $\text{length}(p + q) = \text{length}(p) + \text{length}(q)$.

#