\documentstyle[11pt,fullpage]{article}
\input{macros}
\input{lmacros}
%\newcommand{\term}[1]{{}}
\newcommand{\term}[1]{\mbox{$#1:$}{}}
\newcommand{\jdg}[3]{#1 \mathrel{\triangleright} #2\mathrel{:}#3}
\begin{document}

\begin{center}
{\Large \bf Linear Lambda Calculus}\\
\vskip .1in
John Mitchell\\
Monday, May 8
\end{center}
\vskip .3in
This handout summarizes a ``linear'' version of typed lambda calculus
with function types and products. There are two exercises.

\section{Typing rules}

The untyped terms we consider are lambda terms extended with 
pairs and a pattern-matching form of pair destructor (instead of projection
functions). The context-free grammar of untyped terms is
\[
e \quad ::= \quad c\,|\, x \,|\, \lamb{x}e  \,|\, ee \,|\, \pair{e,e} \,|\,
\mbox{ let }\pair{x,y} \mbox{ be }e_1\mbox{ in }e_2 
\]

The type expressions are given by the grammar
\[
A \quad ::= \quad P \,|\, A \la B \,|\, A \otimes B
\]
where $P$ may be any type constant, $A \la B$ is the type of linear
functions from $A$ to $B$ (i.e., functions that use the value of their argument
exactly once) and $A \otimes B$ is a type of pairs $\pair{a,b}$,
with $a$ from $A$ and $b$ from $B$, with the property that
each component may be used exactly once.

The typing rules use assertions of the form $\jdg{\Gamma}{e}{A}$,
where $\Gamma$ is a set of assumptions
$A_1:\tau_1, \ldots,A_k:\tau_k$ associating types to term variables,
with no term variable appearing twice. 

There is one typing axiom and five typing rules.
{\it In these rules, a comma between sets, as in $\Sigma,\Delta$ in {\bf A},
means union of disjoint sets.} 
Consequently, we can
only type $e_1e_2$ if no variable appears free in both $e_1$ and $e_2$,
maintaining the intended linearity of the calculus.
(In writing $\Sigma, \term{x}A$, we similarly assume that 
$\term{x}A$ is not in $\Sigma$.)
\begin{center}
\begin{tabular}{rc}
{\bf I} &   $\begin{array}{c}
		    \term{x}A \mathrel{\triangleright} \term{x}A
		    \end{array}$ \\[.5cm]
{\bf Subst} &  $\begin{array}{c}
	    \Sigma \mathrel{\triangleright} \term{e_1}A \hspace{.4cm}
            \term{x}A, \Gamma \mathrel{\triangleright} \term{e_2}B\\
            \hline
            \Sigma, \Gamma \mathrel{\triangleright} \term{[e_1/x]e_2}B
            \end{array}$  \\[.5cm]
{\bf A}         &  $\begin{array}{c}
	    \Delta \mathrel{\triangleright} \term{e_1}(A \la B) \hspace{1cm}
            \Sigma \mathrel{\triangleright} \term{e_2}A\\
            \hline
            \Sigma, \Delta \mathrel{\triangleright} \term{(e_1 \, e_2)} B
            \end{array}$ \\[.5cm]
{\bf $\la$R}       &  $\begin{array}{c}
	    \Sigma, \term{x}A \mathrel{\triangleright} \term{e}B \\
            \hline
            \Sigma \mathrel{\triangleright} \term{\lambda x.\,e}(A \la B) 
            \end{array}$ \\[.5cm]
{\bf $\otimes$L} &  $\begin{array}{c}
	    \Delta \mathrel{\triangleright} \term{e_1}(A \otimes B) \hspace{.5cm}
	    \Sigma, \term{x}A, \term{y}B \mathrel{\triangleright} \term{e_2}C \\
            \hline
            \Sigma, \Delta \mathrel{\triangleright} 
		\term{\mbox{ let }\pair{x,y}\mbox{ be }e_1\mbox{ in } e_2} \,C
            \end{array}$ \\[.5cm]
{\bf $\otimes$R} &  $\begin{array}{c}
	    \Sigma \mathrel{\triangleright} \term{e_1}A \hspace{1cm}
            \Gamma \mathrel{\triangleright} \term{e_2}B\\
            \hline
            \Sigma, \Gamma \mathrel{\triangleright} \term{\pair{e_1,e_2}}(A \otimes B)
            \end{array}$ \\[.5cm]
\end{tabular}
\end{center}

\vskip 2ex
\noindent
\b{Exercise:}
Show that the substitution typing rule can be dropped without changing the
set of derivable typing assertions.
In other words, show that if $\jdg{\Gamma}{e}{A}$ is derivable using
the rules above, we may also prove $\jdg{\Gamma}{e}{A}$ without using
{\bf Subst.} 
\newpage

\section{Adjunctions and Currying}


There is a close correspondence between
traditional typed lambda calculus with a terminal type \b{1}, pairing
and function types and cartesian closed categories.

The adjunction between products and exponentials (function types)
in cartesian closed categories is essentially the isomorphism associated
with Currying, i.e., 
\[
A \rightarrow B \rightarrow C \quad\cong\quad 
A \times B \rightarrow C
\]
This is also sometimes written
\begin{center}
\begin{tabular}{c}
$A \rightarrow B \rightarrow C $\\ \hline\hline
$A \times B \rightarrow C$
\end{tabular}
\end{center}
where the double horizontal line indicates a \q{natural isomorphism}.
This property is proved in the typed lambda calculus by showing that
the two maps
\[
\begin{array}{lll}
\jdg{x:\sigma}{M}{\tau\rightarrow \rho} &\mapsto&
\jdg{x:\sigma,y:\tau}{My}{\rho} \\


\jdg{x:\sigma,y:\tau}{N}{\rho} &\mapsto&
\jdg{x:\sigma}{\lamb{y:\tau}N}{\tau\rightarrow \rho}
\end{array}
\]
are inverses. This proof uses the equational theory of typed lambda calculus.


The adjunction involving products and the terminal object involves the
isomorphism
\[
(A \rightarrow B) \times (A \rightarrow C) \quad\cong\quad 
A \rightarrow B \times C
\]
However, there is a slight pun here regarding the first $\times$,
which is really product in the category of categories,
while the second is product in the category at hand.
We can be clearer about this using the second notation above, writing
\begin{center}
\begin{tabular}{c}
$A \rightarrow B$, $A \rightarrow C$\\  \hline\hline
$A \rightarrow  B\times C$
\end{tabular}
\end{center}
meaning that there is a natural isomorphism between pairs of
arrows of the types given above the lines and arrows of the
type given below the lines.
This property is proved in the typed lambda calculus by showing that
the two maps
\[
\begin{array}{clc}
\jdg{x:\sigma}{M}{\tau}\quad\jdg{x:\sigma}{N}{\rho} &\mapsto&
\jdg{x:\sigma}{\pair{M,N}}{\tau\cross\rho} \\


\jdg{x:\sigma}{M}{\tau\cross\rho}  &\mapsto&
\jdg{x:\sigma}{\b{Proj}_1 M}{\tau}\quad\jdg{x:\sigma}{\b{Proj}_2 M}{\rho}
\end{array}
\]
are inverses. This proof again uses the equational theory of typed lambda calculus.

\vskip 2ex
\noindent
\b{Exercise:}
Consider the analogous properties for linear lambda calculus,
with $\la$ replacing $\rightarrow$ and $\otimes$ replacing $\times$.
Show that the first of these isomorphism holds for the linear 
lambda calculus and explain why the second would cause linearity of
functions to fail.
In order to complete this part of the problem, you will have to
make some assumptions about the equational theory of linear lambda
calculus. To help you think about this, part of a structured operational
semantics is given on the next page.

\newpage
\section{Operational semantics}

\begin{center}
\begin{tabular}{rc}
{\bf $\la$L}         &  $\begin{array}{c}
		e_1 \red \lambda x . v \hspace{1cm}
		e_2 \red c \hspace{1cm} 
		[c/x]v \red d \\
            \hline
		(e_1 e_2) \red d
            \end{array}$ \\[.5cm]
{\bf $\la$ R} &  $\begin{array}{c} 
                  \lambda x . e \red \lambda x . e
	    \end{array}$\\[.5cm]{} 
{\bf $\otimes$L} &  $\begin{array}{c}
		e_1 \red \pair{c, d} \hspace{1cm}
		[c/x, d/y]e_2 \red e \\
            \hline
		\mbox{ let }\pair{x,y} \mbox{ be }e_1\mbox{ in }e_2 
			\red e
            \end{array}$\\[.5cm]
{\bf $\otimes$R} &  $\begin{array}{c}
		e_1 \red v_1 \hspace{1cm} e_2 \red v_2 \\
            \hline
		\pair{e_1, e_2} \red \pair{v_1, v_2}
            \end{array}$\\[.5cm]
\end{tabular}
\end{center}


\end{document}
