\documentclass{article}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{proof}
\usepackage{hyperref}
\usepackage[usenames,svgnames]{xcolor}
\usepackage{framed}
\usepackage[left=3cm,top=3cm,right=4cm,nohead,bottom=3cm]{geometry}
\newtheorem{lemma}{Lemma}[section]
\newenvironment{hint}{\noindent{\bf (Hint)}}{}
\newtheorem{remark}{Remark}
\newtheorem{thm}{Theorem}
\newtheorem{definition}{Definition}
\newtheorem{task}{Task}
\newtheorem{bonus}{Bonus Task}
\renewenvironment{proof}{\trivlist \item[\hskip \labelsep{\bf
Proof:}]}{\hfill$\Box$ \endtrivlist}
\input{hw1-macros.tex}
\title{\Large\textbf{
Homework 1: Substitution and Combinators}
\normalsize\\
15-814: Types and Programming Languages\\
TA: Carlo Angiuli (cangiuli@cs.cmu.edu)\\}
\author{}
\date{%
Out: 9/17/13 \\
Due: 9/24/13 (end of day)
}
\begin{document}
\maketitle
Welcome to 15-814's first homework assignment! The goal of this assignment is
to develop and practice the basic techniques necessary for the study of
programming languages, in particular, \emph{rule induction}.
Please submit your work as a PDF to {\tt cangiuli@cs.cmu.edu} and include the
phrase ``15-814 Homework~1'' in the subject line of your email.
\section{The substitution theorem}
As a reminder, here is the presentation of the $\lambda$-calculus:
\[
\begin{array}{lcl}
\G & ::= & \cdot \mid \G,x\ok \\
M,N & ::= & x \mid M\,N \mid \lambda x.M
\end{array}
\]
with these inductive rules for a well-defined term:
\[
\infer[(\var)]{\G, x\ok \entails x\ok}{}
\quad
\infer[(\ap)]{\G \entails M\, N \ok}{\G \entails M \ok & \G \entails N \ok}
\quad
\infer[(\abs)]{\G \entails \lambda x . M \ok}{\G, x \ok \entails M \ok}
\]
\begin{remark}
In the rules above, $\G$ is a (unordered) multiset; in particular, $(x\ok,y\ok)$
is precisely the same context as $(y\ok,x\ok)$. For example, one can conclude by
the $\var$ rule that $x\ok,y\ok\entails x\ok$.
\end{remark}
\begin{remark}
In the rules above, and for this entire course, terms are only ever considered
up to $\alpha$-equivalence (as defined in class). So the judgment
$\cdot\entails \lambda x.x\ok$ is precisely the same as the judgment
$\cdot\entails \lambda y.y\ok$, and you may freely $\alpha$-vary terms in this
fashion whenever needed.
\end{remark}
\begin{definition}
We say the variable $x$ is in the context $\G$, written $x\in\dom{\G}$, when:
\[
\begin{array}{lcl}
x \in \dom{\cdot} & \iff & \text{never} \\
x \in \dom{\G, y\ok} & \iff & x = y \text{ or } x\in\dom{\G}
\end{array}
\]
\end{definition}
\begin{definition}
We say the variable $x$ is \emph{free} in the term $M$, written $x\in\FV{M}$,
when:
\[
\begin{array}{lcl}
x \in \FV{y} & \iff & x = y\\
x \in \FV{M \ N} & \iff & x \in \FV{M} \mbox{ or } x \in \FV{N}\\
x \in \FV{\lambda y.M} & \iff & x \neq y \mbox{ and } x \in \FV{M}
\end{array}
\]
\end{definition}
\begin{definition}
The \emph{substitution} relation $[N/x]M = M'$, denoting that $M'$ is the
result of substituting $N$ for all occurrences of $x$ in $M$, is defined by the
following rules:
\[
\infer[(\var\subst_1)]
{[N/x]x = N}{}
\quad
\infer[(\var\subst_2)]
{[N/x]y = y}{x \neq y}
\]
\[
\infer[(\ap\subst)]{[N/x]M_1\ M_2 = M_1' \ M_2'}
{[N/x]M_1 = M_1' & [N/x]M_2 = M_2'}
\quad
\infer[(\lambda\subst)]
{[N/x]\lambda y.M = \lambda y.M' }
{y \neq x & y \not\in\FV N & [N/x]M = M'}
\]
\end{definition}
Note that the side-conditions on the free variables in the rule for
the $\lambda$-abstraction make substitution a partial function on raw terms, but
it is in fact a total function on $\alpha$ equivalence classes of terms.
\begin{task}
What is the result of the substitution $[(\lambda x.y)/z](\lambda y.(\lambda z.z)z)$?
\end{task}
We can think of contexts as lists of hypotheses: the judgment $x\ok\entails
M\ok$ means that, if we assume $x\ok$, then $M\ok$. In the derivation of this
judgment, every occurrence of the $\var$ rule makes use of one of these
assumptions---certainly, if we assume $x$ is well-formed, then we should be able
to conclude that $x$ is well-formed.
The \emph{substitution theorem} states that we can discharge the assumption that
$x$ is well-formed by replacing $x$ with an actual well-formed term $N$. Then,
each time we would make use of our assumption $x\ok$, we can instead defer to
our proof that $N\ok$.
In order to prove it, we will need the following lemma, known as
\emph{weakening}.
\begin{task}[Weakening theorem]\label{task:wk}
Show that if $\G \entails M \ok$, then $\G, x \ok \entails M \ok$
for any $x \not\in \mathsf{dom}(\G)$. Then, show that the derivation of
$\G,x\ok\entails M\ok$ which you constructed has the same shape\footnote{By
``same shape'' we mean, for example, that the two derivations are isomorphic
as trees. You do not need to make this notion precise, but it should be
possible to argue convincingly.} as the original derivation of
$\G\entails M\ok$.
\end{task}
\begin{task}[Substitution theorem]\label{task:subst}
Show that if $\G, x \ok \entails M \ok$ and $\G \entails N \ok$,
then $\G \entails [N/x]M \ok$.
\end{task}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Combinator calculi}
We define $\beta$-reduction $M \reduces_\beta N$ on $\lambda$-terms as:
\[
\infer[(\beta\ap_1)]{M\, N \reduces_\beta M' \, N}{M \reduces_\beta M'}
\quad
\infer[(\beta\ap_2)]{M\, N \reduces_\beta M \, N'}{N \reduces_\beta N'}
\quad
\infer[(\beta)]{(\lambda x . M)\, N \reduces_\beta [N/x]M}{}
\]
The first two rules allow for reductions in an application. The last
rule substitutes $N$ for $x$ in the body $M$ of a
$\lambda$-abstraction.
Surprisingly, the power of the $\lambda$-calculus does not depend on variable
binding. It is possible to formulate calculi that, like $\lambda$-calculus,
support Turing-complete computation with first-class, higher-order functions,
but without any native support for variable binding. (Avoiding any notion of
binding means that we need not implement capture-avoiding substitution, but as
we will soon see, these calculi are less user-friendly than $\lambda$-calculus.)
In this exercise, we will investigate one such calculus, the SKI combinator
calculus. The calculus includes three combinators: $\I$, $\K$ and $\Scomb$ (so
named for historical reasons), and combinator application:
\[
\begin{array}{lcl}
E & ::= & \I \mid \K \mid \Scomb \mid E_1 \, E_2
\end{array}
\]
We define combinator reduction, written $E_1 \reduces_\SKI E_2$ as
follows (where $X, Y, Z$ stand for combinator terms):
\[
\infer[(\I)]{\I\,X \reduces_\SKI X}{}
\quad
\infer[(\K)]{\K\,X\,Y \reduces_\SKI X}{}
\quad
\infer[(\Scomb)]{\Scomb\,X\,Y\,Z \reduces_\SKI (X\,Z)\,(Y\,Z)}{}
\]
\[
\infer[(\SKI\ap_1)]{E_1\,E_2 \reduces_\SKI E_1'\, E_2}{E_1 \reduces_\SKI E_1'}
\quad
\infer[(\SKI\ap_2)]{E_1\,E_2 \reduces_\SKI E_1\, E_2'}{E_2 \reduces_\SKI E_2'}
\]
We then define \emph{iteration}, or \emph{Kleene closure}, of combinator reduction in the standard way:
\[
\infer[]{E \reduces_\SKI^* E}{}
\quad
\infer[]{E \reduces_\SKI^* E''}{E \reduces_\SKI E' \quad E' \reduces_\SKI^* E''}
\]
Intuitively, $\I$ is the \emph{identity} function; $\K$ generates \emph{constant} functions: given a term, $\K$ returns a function that returns that term for any argument; $\Scomb$ is ``augmented'' application: $\Scomb$ propagates its third argument to its first and second arguments (via application), before applying the first to the second.
Our goal is to define a way to compile a $\lambda$-term to a term in the SKI
calculus. The obvious difficulty is that we must somehow compile away all
variables and variable bindings. We do so in two steps. First, we extend the SKI
calculus to include variables
($E \ ::= \ \ldots \mid x$)
and devise a way of simulating binding in the SKI calculus. Then, we write a
translation from $\lambda$ terms to SKI-terms-with-simulated-binding.
This simulation of binding is achieved by \emph{bracket abstraction}, written
$[x]E$. $E$ stands for a SKI term and $x$ is a variable that may appear
in $E$. Here, $[x]E$ yields a SKI term that does not contain $x$ and,
when applied to a term $E_2$, essentially substitutes $E_2$ for all occurrences
of $x$ in $E$.
You will define bracket abstraction in Task~\ref{task:ski-bracket}, and in
Task~\ref{task:ski-correct} prove that it indeed works this way.
Notice that $E$ cannot itself contain bracket abstractions (because they are not
part of the syntax of $E$), so there are no concerns with capture-avoiding
substitution---all variables in $E$ are free.
Given bracket abstraction, the compilation function is straightforward: $(\cdot)^*$ takes a $\lambda$-term
and compiles it to a SKI term (making use of bracket abstraction):
\[
\begin{array}{lcl}
x^* & = & x\\
(M\,N)^* & = & M^*\,N^*\\
(\lambda x.M)^* & = & [x]M^*
\end{array}
\]
\begin{task}\label{task:ski-subst}
Define the substitution operation $[E/x]E'$ for terms from the SKI calculus extended with variables.
Be sure to distinguish the case when the variable in question matches that being abstracted and the case when it differs.
\end{task}
\begin{task}\label{task:ski-bracket}
Now, define bracket abstraction inductively over the SKI term $E$. The difficult
case is:
\[
\begin{array}{lclr}
[x]E & = & \K\,E & \mbox{for }x \not\in\mathsf{FV}_\SKI(E)\\
\end{array}
\]
Complete the definition of bracket abstraction by providing the cases for all
other $E$.
\begin{hint}
Your definition of the bracket abstraction should closely resemble your definition of substitution.
\end{hint}
\end{task}
We must now check that this translation is ``correct,'' in the sense that the
combinator term $E$ that results from the translation of a $\lambda$-term $M$
can simulate the reduction steps that can be performed by
$M$.\footnote{Technically, you will only be proving that the compilation is
\emph{complete}, which is generally only considered one part of correctness.}
You may freely use the following lemmas. Make sure you understand why they are
true, but you need not prove them.
\begin{lemma}\label{lma:ski-trans}
If $E \reduces_\SKI^* E'$ and $E' \reduces_\SKI^* E''$ then $E \reduces_\SKI^* E''$.
\end{lemma}
\begin{lemma}\label{lma:ski-ap1}
If $E \reduces_\SKI^* E'$ then for any $E''$ we have $E\,E'' \reduces_\SKI^* E'\,E''$.
\end{lemma}
\begin{lemma}\label{lma:ski-ap2}
If $E \reduces_\SKI^* E'$ then for any $E''$ we have $E''\,E \reduces_\SKI^* E''\,E'$.
\end{lemma}
We begin by first proving the correctness of bracket abstraction, that
is, the application of a bracket abstraction reduces to a
substitution.
\begin{task}\label{task:ski-correct}
Show that, for any $E$ and $E'$, $([x]E)\,E' \reduces_\SKI^* [E'/x]E$.
\begin{hint}
Proceed by induction on the structure of $E$.
\end{hint}
\end{task}
\noindent We can now prove our main result.
You may assume that $([N/x]M)^* = [N^*/x]M^*$.
\begin{task}
Show that if $M \reduces_\beta N$, then $M^* \reduces_\SKI^* N^*$.
\end{task}
\begin{task}
It turns out that the $\I$ combinator is actually redundant, in that
its reduction behavior can be mimicked by application, $\Scomb$ and
$\K$. Produce a combinator term $\mathbf{T}$ that only makes use of
$\Scomb$, $\K$ and application that can simulate the behavior of $\I$, in
the following way:
$$
\mathbf{T}\,X \reduces_\SKI^* X
$$
\end{task}
\end{document}