Answer as many questions as you can. For short answer questions, be as brief as possible, but not too brief. You do not need complete sentences. There is neither time enough nor space enough to write complete sentences.

1. Give the number of inhabitants for each type. If your answer has an $\aleph$ in it and it’s hard for you to write, just spell it out. For example, you can write “aleph-null” instead of $\aleph_0$. Please only show the cardinalities, do not show your work or attempt to list the functions.
   $\textsf{Bool} + \textsf{Unit}$ $\quad\underline{\quad 3\quad}$

   $\textsf{Nat} + \textsf{Void}$ $\quad\underline{\quad \aleph_0\quad}$

   $\textsf{Nat} \times \textsf{Bool}$ $\quad\underline{\quad \aleph_0\quad}$

   $\textsf{Nat} \times \textsf{Unit}$ $\quad\underline{\quad \aleph_0\quad}$

   $\textsf{Unit} \times \textsf{Void}$ $\quad\underline{\quad 0\quad}$

   $\textsf{Bool} \times \textsf{Bool}$ $\quad\underline{\quad 4\quad}$

   $\textsf{Bool} \to \textsf{Unit}$ $\quad\underline{\quad 1\quad}$

   $\textsf{Bool} \to \textsf{Void}$ $\quad\underline{\quad 0\quad}$

   $\textsf{Unit} \to \textsf{Nat}$ $\quad\underline{\quad \aleph_0\quad}$

   $\textsf{Void} \to \textsf{Nat}$ $\quad\underline{\quad 1\quad}$
2. Define inductively a type for the result of a password change request in a program. The user must submit a valid authentication token, the new password, and the new password a second time as a confirmation. Passwords must be at least 16 characters in length. Call the type $\textsf{Result}$. The result can either be (1) an indication that the request was granted, (2) an indication that the request was denied because the authentication token was invalid, (3) an indication the password request was too short and by how much, or (4) an indication that the request was denied because the new passwords did not match.
   $$ \dfrac{}{\mathsf{ok\!: Result}} \quad \dfrac{}{\mathsf{authfail\!: Result}} \quad \dfrac{n: \textsf{Nat}}{\textsf{shortby}\;n\!: \textsf{Result}} \quad \dfrac{}{\mathsf{nomatch\!: Result}} $$
3. Write a function, in typed $\lambda$-notation, that accepts a token, a candidate password, and a password confirmation for a password change request and returns a $\textsf{Result}$ (the type you defined in the previous problem). Assume the existence of functions $\textsf{isValidToken}\!: \textsf{Token} \to \textsf{Bool}$ that checks the validity of a token, (2) $\textsf{length}\!: \textsf{String} \to \textsf{Nat}$ that returns the length of a string, and (3) $\textsf{equals}\!: \textsf{String} \times \textsf{String} \to \textsf{Bool}$ that checks if two strings are equal.

   $\begin{array}{l} \lambda t_{\textsf{token}}.\;\lambda p_{\textsf{string}}.\;\lambda c_{\small {\textsf{string}}}. \\ \quad \textsf{if}\;\neg(\textsf{validToken}\;t)\;\textsf{then}\;\textsf{authfail} \\ \quad \textsf{else if}\;\textsf{length}\;p \lt 16\;\textsf{then}\;\textsf{shortby}(16 - \textsf{length}\;p) \\ \quad \textsf{else if}\; \neg\;\textsf{equals}\;(p, c)\;\textsf{then}\;\textsf{nomatch} \\ \quad \textsf{else ok} \end{array}$

4. In the Attic Philosophy video on the Curry-Howard Correspondence, Mark Jago shows how the proof of the proposition $(\beta\to\gamma)\to(\alpha\to\beta)\to(\alpha\to\gamma)$ corresponds to the proof term $\lambda x_{\beta\to\gamma}.\lambda y_{\alpha\to\beta}.\lambda z_\alpha.(x(yz))$. What proof term would correspond to the (simpler!) proposition $\beta\to(\alpha\to\beta)$?

   $\lambda x_\beta.\lambda y_\alpha.x$

5. Circle all the free occurrences in the following $\lambda$-expression:
   $λx.(λx.\;x\;\boxed{y})\;(λz.\;(x\;λw.\;w)\;(z\;λp.\;p)\;x)\;\boxed{z}$
6. Reduce $((\lambda f. \lambda x. (\lambda y.f\,y)(\textsf{square}\,x))\,\textsf{double})$ as much as you can. If you need to rename variables, use the usual scheme of choosing the next free letter in the Latin alphabet. If you see any functions that look like arithmetic functions, they are, and you should apply them too.

   $\mathsf{double} \circ \mathsf{square}$

7. Can an expression in the simply typed lambda calculus fail to reduce to a normal form? If so, give an example. If not, explain why not.
   No, every reduction step makes a smaller term. The typing prevents the formation of terms that would reduce forever.
8. What is the significance of the famous equation $Y\,f = f\,(Y\,f)$? What exactly is the equation saying and why is it so fantastical?
   The equation says that $Y$ computes a fix point of $f$. It makes recursion possible, which is fantastic!
9. In a previous quiz you were given a set $R$ and asked what $R^2$ was when interpreted as a plain set and also when interpreted as a relation. Now here is another set that we will call $R$, namely $R = \{1, 2, 3\}$. What is $R^2$ when $R$ is interpreted as an alphabet?
   The language $\{ 11, 12, 13, 21, 22, 23, 31, 32, 33\}$.