\documentclass[11pt]{article}

\setlength{\oddsidemargin}{0cm}
\setlength{\topmargin}{0cm}
\setlength{\headheight}{0cm}
\setlength{\headsep}{0cm}
\setlength{\textwidth}{16cm}
\setlength{\textheight}{24cm}

\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{concmath}
\renewcommand{\ttdefault}{pxtt}

\usepackage{amssymb}
\usepackage{proof}

\newcommand{\lam}{\lambda}
\newcommand{\Lam}{\Lambda}

\begin{document}

\thispagestyle{empty}

\begin{center}\Large
\textbf{Exercises} ''MTAT.05.105 Type Theory''
\end{center}

\subsection*{Simply typed $\lam$-calculus}

\begin{enumerate}
\item In the following derivation, replace questionmarks with correct
types and terms:
\[
\infer{\vdash ? : \alpha\to\beta\to(\alpha\to\beta\to\gamma)\to\gamma}{
 \infer{x{:}? \vdash ? : \beta\to(\alpha\to\beta\to\gamma)\to\gamma}{
  \infer{x{:}?,\, y{:}? \vdash ? : (\alpha\to\beta\to\gamma)\to\gamma}{
   \infer{x{:}?,\, y{:}?,\,f{:}? \vdash ? :\gamma}{
    \infer{x{:}?,\, y{:}?,\,f{:}? \vdash ? : \beta}{} 
    &
    \infer{x{:}?,\, y{:}?,\,f{:}? \vdash ? : \beta\to\gamma}{
     \infer{x{:}?,\, y{:}?,\,f{:}? \vdash ? : \alpha}{}
     &
     \infer{x{:}?,\, y{:}?,\,f{:}? \vdash ? : \alpha\to\beta\to\gamma}{
     }
    }
   }
  }
 }
}
\]
\item Find inhabitants (ie.\ \emph{closed} terms) of the following
types:
\begin{enumerate}
\item $((\alpha\to\beta\to\alpha)\to\alpha)\to\alpha$
\item $\beta\to((\alpha\to\beta)\to\gamma)\to\gamma$
\end{enumerate}
\item Give a derivation of the following judgement:
\[
\vdash \lam x\,y.\,y\,(\lam z.\,y\,x)
 : (\alpha\to\beta)\to((\alpha\to\beta)\to\beta)\to\beta
\]
\item Let $\mathbf{2} \equiv \lam f\,z.\ f(f\,z)$ and $\mathbf{K}
\equiv \lam x\,y.x$. Show that the $\lam$-term
$\mathbf{2}\,\mathbf{K}$ is not typable in Curry-style $\lam{\to}$.
\end{enumerate}

\subsection*{Second-order $\lam$-calculus}

\begin{enumerate}
\setcounter{enumi}{4}
\item Find a type for $\lam x.\,x\,x\,x$ and give the corresponding
Church-style $\lam$-term.
\item Show that all normal forms are typable in Curry-style $\lam 2$.
\end{enumerate}

\subsection*{The $\lam$-cube}

\begin{enumerate}
\setcounter{enumi}{6}
\item A raw environment $\Gamma$ is called \emph{valid} if it occurs
in some derivable judgement. Show that an environment $\Gamma$ is
valid iff $\Gamma \vdash * : \Box$.
\item Let $\bot \equiv \Pi\alpha{:}{*}.\alpha$. Give derivation trees
for the following judgements. What are the simplest systems of the
$\lam$-cube in which the judgements are valid?
\[
\begin{array}{lrcl}
\mbox{(a)} & &
\vdash & (\lam \beta{:}{*}. \lam a{:}\bot. a\,\beta)
        : (\Pi \beta{:}{*}. \bot\to\beta) \\
\mbox{(b)} & A{:}*,\, P{:}A\to{*} &
\vdash & (\lam a{:}A. Pa\to\bot) : (A \to {*})
\end{array}
\]
\end{enumerate}

\end{document}
