% -*- mode: LaTeX; compile-command: "mk" -*-
\documentclass{tufte-handout}
%include polycode.fmt
%\arrayhs
\usepackage{../../hshw}
\usepackage{mathpartir}
\title{\thecourse\ problem set 6}
\date{\small Revision 1: compiled \today\ at \currenttime}
\author{Due Tuesday, March 1}
\begin{document}
\maketitle
\section{Rubric}
\label{sec:rubric}
For full credit, your solutions should demonstrate a proficient
understanding of the following topics:
\begin{itemize}
\item Simply typed lambda calculus: 4 points
\item $Y$ combinator: 4 points
\item Type inference: 4 points
\item Curry-Howard isomorphism: 4 points
\end{itemize}
An extra 4 points will be awarded for completeness.
\section{The Simply-Typed Lambda Calculus}
This section provides a reference for the simply-typed
$\lambda$-calculus extended with product and sum types, as discussed
in class.
\subsection{Syntax}
\label{sec:syntax}
Types are denoted by the metavariables $\varphi$ or
$\psi$\marginnote{or occasionally $\chi$ or whatever other lowercase
Greek letter I feel like using} and are defined by the following
recursive grammar:
\[ \varphi,\psi ::= A \mid \varphi \to \psi \mid \varphi \times \psi
\mid \varphi + \psi \]
That is, a type is either a base type (denoted by a capital letter
like $A$, $B$, \dots), a function type $\varphi \to \psi$, a product
type $\varphi \times \psi$, or a sum type $\varphi + \psi$.
\newcommand{\cons}[1]{\mathsf{#1}}
\newcommand{\newcons}[1]{%
\expandafter\providecommand\csname s#1\endcsname{}\expandafter\renewcommand\csname s#1\endcsname{\cons{#1}}}
\newcons{fst}
\newcons{snd}
\newcons{left}
\newcons{right}
\newcons{case}
\newcons{of}
\newcommand{\lft}[1]{\app{\sleft}{#1}}
\newcommand{\rgt}[1]{\app{\sright}{#1}}
\newcommand{\fst}[1]{\app{\sfst}{#1}}
\newcommand{\snd}[1]{\app{\ssnd}{#1}}
\newcommand{\case}[5]{\scase\;#1\;\sof\;\{\lft #2 \to #3;\; \rgt #4 \to #5 \}}
\newcommand{\tlam}[3]{\lam{#1\!:\!#2}{#3}}
The syntax of terms is given by
\begin{align*}
t ::&= x \mid \tlam x \varphi t \mid \app{t_1}{t_2} \\
& \mid (t_1, t_2) \mid \fst t \mid \snd t \\
& \mid \lft t \mid \rgt t \mid \case t {x_1} {t_1} {x_2} {t_2}
\end{align*}
Formally, this syntax requires that the argument of a $\lambda$ must
be annotated with a type ($\tlam x \varphi t$). However, we will
sometimes omit the type annotation ($\lam x t$), either because the
type can be easily understood from the context, or because it is up to
you to deduce what its type annotation should be.
\subsection{Typing}
\label{sec:typing}
The typing rules for this version of the simply-typed
$\lambda$-calculus are shown below.
\newcommand{\shows}{\vdash}
\newcommand{\nrule}[3]{\inferrule{#2}{#3} \quad \text{#1}}
\begin{mathpar}
\nrule{Var (Ax)}{x : \varphi \in \Gamma}{\Gamma \shows x : \varphi} \\
\nrule{Lam ($\to$I)}{\Gamma, x : \varphi \shows t : \psi}{\Gamma \shows \tlam
x \varphi t : \varphi \to \psi} \and
\nrule{App ($\to$E)}{\Gamma \shows t_1 : \varphi \to \psi \and \Gamma \shows t_2
: \varphi}{\Gamma \shows \app{t_1}{t_2} : \psi} \\
\nrule{Pair ($\times$I)}{\Gamma \shows t_1 : \varphi \and \Gamma \shows t_2 :
\psi}{\Gamma \shows (t_1, t_2) : \varphi \times \psi} \\
\nrule{Fst ($\times$E$_1$)}{\Gamma \shows t : \varphi \times
\psi}{\Gamma \shows \fst t : \varphi} \and
\nrule{Snd ($\times$E$_2$)}{\Gamma \shows t : \varphi \times
\psi}{\Gamma \shows \snd t : \psi} \\
\nrule{Left ($+$I$_1$)}{\Gamma \shows t : \varphi}{\Gamma \shows
\lft t : \varphi + \psi} \and
\nrule{Right ($+$I$_2$)}{\Gamma \shows t : \psi}{\Gamma \shows
\rgt t : \varphi + \psi} \\
\nrule{Case ($+$E)}{\Gamma \shows t : \varphi + \psi \and \Gamma,
x_1 : \varphi \shows t_1 : \chi \and \Gamma, x_2 : \psi \shows t_2
: \chi}{\Gamma \shows \case t {x_1} {t_1} {x_2} {t_2} : \chi}
\end{mathpar}
\subsection{Reduction}
\label{sec:reduction}
Finally, the reduction rules are as follows:
\newcommand{\red}{\rightsquigarrow}
\newcommand{\subst}[3]{[#1 \mapsto #2]#3}
\begin{mathpar}
\nrule{$\beta$}{ }{\app {(\tlam x \varphi {t_1})}{t_2} \red \subst x
{t_2}{t_1}} \\
\nrule{Cong-AppL}{t_1 \red t_1'}{\app{t_1}{t_2} \red \app{t_1'}{t_2}}
\and
\nrule{Cong-AppR}{t_2 \red t_2'}{\app{t_1}{t_2} \red \app{t_1}{t_2'}} \\
\nrule{$\beta$-Fst}{ }{\fst {(t_1, t_2)} \red t_1} \and
\nrule{$\beta$-Snd}{ }{\snd {(t_1, t_2)} \red t_2} \\
\nrule{Cong-Fst}{t \red t'}{\fst t \red \fst {t'}} \and
\nrule{Cong-Snd}{t \red t'}{\snd t \red \snd {t'}} \\
\nrule{$\beta$-CaseL}{ }{\case {(\lft t)} {x_1}{t_1}{x_2}{t_2} \red
\subst {x_1} t {t_1}} \and
\nrule{$\beta$-CaseR}{ }{\case {(\rgt t)} {x_1}{t_1}{x_2}{t_2} \red
\subst {x_2} t {t_2}} \\
\nrule{Cong-Case}{t \red t'}{\case t {x_1}{t_1}{x_2}{t_2} \red \case
{t'} {x_1}{t_1}{x_2}{t_2}}
\end{mathpar}
\exercise Give a formal typing derivation (\ie\ a proof tree) which
assigns a type to the following term (note there are multiple correct
answers):
\[ \lam p {\case {(\fst p)} {x_1} {\rgt {x_1}} {x_2} {\app {x_2}
{(\lam z z)}}} \]
\exercise If $\Gamma \shows t : \varphi$ and $t \red t'$, will it
always be the case that $\Gamma \shows t' : \varphi$ (for the
\emph{same} type $\varphi$)? Explain how you would go about
structuring a proof of this statement. Which parts are easy? Which
parts would be more difficult?
\exercise Recall that in the untyped $\lambda$-calculus, we can define
the $Y$ combinator by \[ Y = \lam f {\app {(\lam x {\app f {(\app x
x)}})} {(\lam x {\app f {(\app x x)}})}}. \] Explain why it is
not possible\marginnote{\emph{Hint}: note that, as with anything
defined inductively/recursively, infinite types are not allowed.}
to give a type to $Y$ in the simply-typed $\lambda$-calculus.
\exercise Of course, just showing that $Y$ does not have a type is not
a proof that we have ruled out infinite recursion! Maybe there is
some other tricky thing we can do that has a type but acts like $Y$.
We would like to \emph{prove} that any well-typed term will only
reduce for a finite number of steps. If a term $t$ does not reduce
infinitely we say $t$ \term{terminates}. Otherwise we say $t$
\term{diverges}.
\newcommand{\size}{\mathsf{size}}
\newcommand{\N}{\mathbb{N}}
One obvious approach would be to prove the following statement by
(strong\footnote{The strong induction principle for natural numbers
says that in order to prove that $P$ holds for all natural numbers,
we must prove that $P$ holds for an arbitrary number $m$ under the
assumption that $P$ holds for \emph{all} numbers $k < m$. Note this
also means we must prove $P(0)$ without any assumptions, since there
are no $k < 0$. This is equivalent in power to the usual induction
principle for natural numbers, but often ``feels'' more powerful,
since the inductive hypothesis lets you assume that $P$ holds for
\emph{all} numbers smaller than $m$ instead of just the
predecessor.}) induction on the size\footnote{The $\size$ of a
$\lambda$-calculus term is defined as the number of constructors it
contains, \ie\ each $\lambda$ contributes $1$ to the size, as does
each application, pair, and so on. For example, $\size(\lam x
{(\fst {(y,z)})}) = 5$.} of $\lambda$-calculus terms:
\[ \forall n \in \N. \forall t. (\size(t) = n) \implies
t\text{ terminates}. \] Unfortunately, this does not work. Explain
why not.
\newthought{This turns out to} actually be true, but proving it is
nontrivial---much too nontrivial to include on this homework, but not
so nontrivial that you would not be able to understand the proof. If
you are interested, you can consult Chapter 12 of
Pierce\cite[0.1in]{pierce2002types} (you are welcome to borrow my
copy).
\newcons{Y}
\newcommand{\Y}[1]{\app \sY {#1}}
Now that we have cut out unrestricted recursion, suppose we want to
add it back in, but in a principled way.\footnote{Why would we go to
all the trouble of getting rid of recursion if we are just going to
add it back in again? Although adding $\sY$ gives us
unrestricted recursion again, it's now easy to tell just by looking
at a term whether it could possibly be infinitely recursive: just
see whether it contains $\sY$ or not. If it doesn't, then it will
definitely terminate. Also, as we discussed in class, there are
many benefits to having a type system besides just getting rid of
infinite recursion.} The idea is to explicitly add a new term
constructor $\sY$ to the syntax of $\lambda$-calculus terms, \ie\ in
addition to $\lambda$, application, \etc, a term $t$ can now also be
of the form $\Y t'$ for some other term $t'$. Note that in contrast
to the $Y$ from the untyped $\lambda$-calculus, which we just defined
to be a certain $\lambda$-calculus term, this new $\sY$ is just a
piece of syntax with no \emph{a priori} meaning.
\exercise Write down a typing rule for $\Y t$, that is, a rule of the form
\begin{mathpar}
\inferrule{ \dots }{ \Gamma \shows \Y(t) : \dots }
\end{mathpar}
where you fill in the dots appropriately. (\emph{Hint}: think about
the type of |fix| in Haskell.)
\exercise Write down an appropriate reduction rule for $\Y$.
\newthought{Consider the following} Haskell definitions:
\begin{spec}
data Ty where
BaseTy :: String -> Ty
Arr :: Ty -> Ty -> Ty
deriving (Eq, Show)
data Tm where
Var :: String -> Tm
Lam :: String -> Ty -> Tm -> Tm
App :: Tm -> Tm -> Tm
deriving Show
\end{spec}
|Ty| represents types of the STLC, and |Tm| represents terms. I have
provided you with the file |STLC.hs|, which contains the above
definitions along with utilities to parse and pretty-print terms and
types (that is, convert between |String| representations and the above
algebraic data types).
\exercise Implement a function\marginnote{\emph{Hint}: you may find
the |Data.Map| module useful.} \[ |inferType :: Tm -> Maybe Ty| \] which
infers the type of a term. You can use the provided parsers and
pretty-printers to test your function. For example,
\begin{verbatim}
ghci> let tm = readTmU "\\y:D -> A -> B. \\z:D. \\x:(A -> B) -> ((C -> D) -> E). x (y z)"
ghci> fmap ppTy (inferType tm)
Just "(D -> A -> B) -> D -> ((A -> B) -> (C -> D) -> E) -> (C -> D) -> E"
ghci> fmap ppTy (inferType (readTmU "\\x:A. x x"))
Nothing
\end{verbatim}
\section{The Curry-Howard isomorphism}
\exercise Some of the following propositions are provable in
propositional logic, and some are not.
\begin{itemize}
\item For those that are provable, demonstrate it \emph{by giving a
term of the STLC with a corresponding type} (you need not give a
formal typing derivation, though you may find it helpful to do so).
Equivalently, you may write a Haskell function with a corresponding
type, as long as you are careful not to use recursion or any other
Haskell features which are not part of STLC.
\item For those that are not provable, explain why not.
\end{itemize}
\begin{enumerate}[label=(\alph*)]
\item $\varphi \implies \varphi$
\item $(\varphi \implies \varphi) \implies \varphi$
\item $((\varphi \implies \varphi) \implies \varphi) \implies \varphi$
\item $(\varphi \land (\psi \lor \chi)) \implies ((\varphi \land \psi) \lor
(\varphi \land \chi))$\marginnote{D\'ej\`a vu?}
\item $(\varphi \implies (\psi \land \chi)) \implies ((\varphi \implies \psi) \land
(\varphi \implies \chi))$
\end{enumerate}
% \exercise What sort of types correspond to the propositions $\top$ and
% $\bot$? What terms might we add to STLC to represent evidence for
% their introduction and elimination rules, respectively?
\bibliographystyle{plainnat}
\bibliography{STLC}
\end{document}