Discrete Mathematics
This is a preserved file from cs2102 Fall 2016. An updated version may exist at https://uvacs2102.github.io/

Class 16: Recursive Data Types


Schedule

You should read MCS Chapter 7 this week.

Problem Set 7 is due 28 October (Friday) at 6:29pm.

Python code from class and list definitions: pairs.py

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