Structural Induction

We can show a property holds for all objects of a data type by:

1. Showing the property holds for all base objects.

2. Showing that all the ways of constructing new objects, preserve the property.

What is the difference between scalar data and compound data structures?

#

Pairs

Definition. A $\text{\em Pair}$ is a datatype that supports these three operations:
\begin{quote} $\text{\em make_pair}: \text{\em Object} \times \text{\em Object} \rightarrow \text{\em Pair}$
$\text{\em pair_first}: \text{\em Pair} \rightarrow \text{\em Object}$\
$\text{\em pair_last}: \text{\em Pair} \rightarrow \text{\em Object}$\
\end{quote} where, for any objects $a$ and $b$, $\text{\em pair_first}(\text{\em make_pair}(a, b)) = a$ and $\text{\em pair_last}(\text{\em make_pair}(a, b)) = b$.

Lists

Definition (1). A List is either (1) a Pair where the second part of the pair is a List, or (2) the empty list.

Definition (2). A List is a ordered sequence of objects.

List Operations

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

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

Unique Construction property:

\begin{equation} \begin{split} \forall p \in \text{\em List} - { \text{\bf null} } \ldotp \exists q \in \text{\em List}, e \in \text{\em Object} \ldotp p = \text{\em prepend}(e, q) \; \wedge
(\forall r \in \text{\em List}, f \in \text{\em Object} \ldotp p = \text{\em prepend}(f, r) \implies r = q \wedge f = e) \end{split} \end{equation}

Why is this necessary for our length definition?

##

def list_prepend(e, l):
    return make_pair(e, l)

def list_first(l):
    return pair_first(l)

def list_rest(l):
    return pair_last(l)

def list_empty(l):
    return l == None

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$.