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.

# ##

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

# ##

Induction Summary

\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}

Challenge-Response Protocols

1. Verifier: picks random challenge, $y$.

2. Prover: proves knowledge of $x$ by revealing $f(x, y)$.

3. Verifer: can verify prover knows $x$ from response, but learns nothing (useful) about $x$.

How can you know the website you are sending your password to is what you think it is?