Capture-avoiding substitution.

macros.tex

@@ -71,6 +71,7 @@
 \newcommand{\typc}[3]{#1 \vdash #2 \eff #3}
 
 \newcommand{\FTV}{\ensuremath{\mathrm{FTV}}}
+\newcommand{\FV}{\ensuremath{\mathrm{FV}}}
 
 \newcommand{\reducesto}[0]{\ensuremath{\leadsto}}
 \newcommand{\stepsto}[0]{\ensuremath{\longrightarrow}}
@@ -105,8 +106,8 @@
 \newcommand{\CompCat}{\CatName{Comp}}
 \newcommand{\ValCat}{\CatName{Val}}
 \newcommand{\VarCat}{\CatName{Var}}
-\newcommand{\ValTypeCat}{\CatName{TVal}}
-\newcommand{\CompTypeCat}{\CatName{TComp}}
+\newcommand{\ValTypeCat}{\CatName{VType}}
+\newcommand{\CompTypeCat}{\CatName{CType}}
 \newcommand{\PresenceCat}{\CatName{Presence}}
 \newcommand{\TypeCat}{\CatName{Type}}
 \newcommand{\TyVarCat}{\CatName{TVar}}
@@ -145,4 +146,9 @@
 %%
 %% Defined-as equality
 %%
-\newcommand{\defas}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\text{def}}}}{=}}}
+\newcommand{\defas}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\text{def}}}}{=}}}
+
+%%
+%% Partiality
+%%
+\newcommand{\pto}[0]{\ensuremath{\rightharpoonup}}

thesis.bib

@@ -759,3 +759,13 @@
   publisher = {Indiana University},
   address = {Indianapolis, IN, USA},
 }
+
+# The original lambda calculus reference
+@InProceedings{Church32,
+  author    = {Alonzo Church},
+  title     = {A Set of Postulates for the Foundation of Logic},
+  year      = {1932},
+  booktitle = {Annals of Mathematics},
+  pages     = {346--366},
+  volume    = {33}
+}

thesis.tex

@@ -50,6 +50,15 @@
      \textquotedblleft={ ,150}, % left quotation mark, space from right
      \textquotedblright={150, }} % right quotation mark, space from left
 
+%%
+%% Theorem environments
+%%
+\newtheorem{theorem}{Theorem}[section]
+\newtheorem{lemma}[theorem]{Lemma}
+\newtheorem{proposition}[theorem]{Proposition}
+\newtheorem{corollary}[theorem]{Corollary}
+\newtheorem{definition}[theorem]{Definition}
+
 %%
 %% Load macros.
 %%
@@ -500,11 +509,11 @@ $\TyVarCat$, to be generated by:
                                         \mid \lambda x^A .\, M \mid \Lambda \alpha^K .\, M
                                         \mid \Record{} \mid \Record{\ell = V;W} \mid (\ell~V)^R \\
                      &     &    &\\
-\slab{Computations}  &M,N \in \CompCat  &::= & V\,W \mid V\,A\\
+\slab{Computations}  &M,N \in \CompCat  &::= & V\,W \mid V\,T\\
                      &                  &\mid& \Let\; \Record{\ell=x;y} = V \; \In \; N\\
                      &                  &\mid& \Case\; V \{\ell~x \mapsto M; y \mapsto N\} \mid \Absurd^C~V\\
                      &                  &\mid& \Return~V \mid \Let \; x \revto M \; \In \; N\\
-\slab{Terms}         &T \in \TermCat    &::= & x \mid V \mid M
+\slab{Terms}         &t \in \TermCat    &::= & x \mid V \mid M
 \end{syntax}
 
 \caption{Term syntax of \BCalc{}.}
@@ -552,6 +561,37 @@ kind information (term abstraction, type abstraction, injection,
 operations, and empty cases). However, we shall omit these annotations
 whenever they are clear from context.
 
+\paragraph{Free variables} We define the function
+$\FV : \TermCat \to \VarCat$ to compute the free variables of any
+given term.
+%
+\[
+  \bl
+  \ba[t]{@{~}l@{~}c@{~}l}
+  \begin{eqs}
+    \FV(x)             &\defas& \{x\}\\
+    \FV(\lambda x^A.M) &\defas& \FV(M) \setminus \{x\}\\
+    \FV(\Lambda \alpha^K.M) &\defas& \FV(M)\\[1.0ex]
+    \FV(V\,W)           &\defas& \FV(V) \cup \FV(W)\\
+    \FV(\Return~V)    &\defas& \FV(V)\\
+  \end{eqs}
+  & \qquad\qquad &
+  \begin{eqs}
+    \FV(\Record{})     &\defas& \emptyset\\
+    \FV(\Record{\ell = V; W}) &\defas& \FV(V) \cup \FV(W)\\
+    \FV((\ell~V)^R)    &\defas& \FV(V)\\[1.0ex]
+    \FV(V\,T)           &\defas& \FV(V)\\
+    \FV(\Absurd^C~V)  &\defas& \FV(V)\\
+  \end{eqs}
+  \ea\\
+  \begin{eqs}
+    \FV(\Let\;x \revto M \;\In\;N) &\defas& \FV(M) \cup (\FV(N) \setminus \{x\})\\
+    \FV(\Let\;\Record{\ell=x;y} = V\;\In\;N) &\defas& \FV(V) \cup (\FV(N) \setminus \{x, y\})\\
+    \FV(\Case~V~\{\ell\,x \mapsto M; y \mapsto N\} &\defas& \FV(V) \cup (\FV(M) \setminus \{x\}) \cup (\FV(N) \setminus \{y\})
+  \end{eqs}
+  \el
+\]
+
 \subsection{Typing rules}
 \label{sec:base-language-type-rules}
 %
@@ -660,13 +700,17 @@ of \emph{free type variables} ($\FTV$) to ensure that we do not
 inadvertently capture a free type variable from the context.
 %
 We define $\FTV$ by mutual induction over type environments, $\Gamma$,
-and the type structure, $T$, as follows.
+and the type structure, $T$. Note that we always work up to
+$\alpha$-conversion~\cite{Church32} of types.
 %
 \[
   \ba[t]{@{~}l@{~~~~~~}c@{~}l}
+  \multicolumn{3}{c}{\begin{eqs}
+    \FTV &:& \TypeCat \to \TyVarCat
+\end{eqs}}\\
   \ba[t]{@{}l}
  \begin{eqs}
-  \FTV &:& \ValTypeCat \to \TyVarCat\\
+  % \FTV &:& \ValTypeCat \to \TyVarCat\\
   \FTV(\alpha)   &\defas& \{\alpha\}\\
   \FTV(\forall \alpha^K.C) &\defas& \FTV(C) \setminus \{\alpha\}\\
   \FTV(A \to C)  &\defas& \FTV(A) \cup \FTV(C)\\
@@ -683,12 +727,12 @@ and the type structure, $T$, as follows.
   % \FTV([R])      &\defas& \FTV(R)\\
   % \FTV(\Record{R}) &\defas& \FTV(R)\\
   % \FTV(\{R\})    &\defas& \FTV(R)\\
-  \FTV &:& \RowCat \to \TyVarCat\\
+  % \FTV &:& \RowCat \to \TyVarCat\\
   \FTV(\cdot)    &\defas& \emptyset\\
   \FTV(\rho)     &\defas& \{\rho\}\\
-  \FTV(l:P;R)    &\defas& \FTV(P) \cup \FTV(R)\\[1.0ex]
+  \FTV(l:P;R)    &\defas& \FTV(P) \cup \FTV(R)\\
 
-  \FTV &:& \PresenceCat \to \TyVarCat\\
+  % \FTV &:& \PresenceCat \to \TyVarCat\\
   \FTV(\theta)   &\defas& \{\theta\}\\
   \FTV(\Abs)     &\defas& \emptyset\\
   \FTV(\Pre{A})  &\defas& \FTV(A)\\
@@ -747,16 +791,13 @@ defined as follows.
     -[-/-] &:& \TypeCat \times \TypeCat \times \TyVarCat \to \TypeCat\\
     (A \eff E)[B/\beta] &\defas& A[B/\beta] \eff E[B/\beta]\\
     (A \to C)[B/\beta] &\defas& A[B/\beta] \to C[B/\beta]\\
-    (\forall \alpha^K.C)[B/\beta] &\defas& \begin{cases}
-                                             \forall \alpha^K.C & \text{if } \alpha = \beta\\
-                                             \forall \alpha^K.C[B/\beta] & \text{otherwise}
-                                           \end{cases}\\
+    (\forall \alpha^K.C)[B/\beta] &\defas& \forall \alpha^K.C[B/\beta] \quad \text{if } \alpha \neq \beta \text{ and } \alpha \notin \FTV(B)\\
     \alpha[B/\beta]     &\defas& \begin{cases}
                                     B & \text{if } \alpha = \beta\\
                                     \alpha & \text{otherwise}
                                   \end{cases}\\
    \Record{R}[B/\beta] &\defas& \Record{R[B/\beta]}\\
-   {[R]}[B/\beta]        &\defas& [R[B/\beta]]\\
+   {[R]}[B/\beta]      &\defas& [R[B/\beta]]\\
    \{R\}[B/\beta]      &\defas& \{R[B/\beta]\}\\
    \cdot[B/\beta]      &\defas& \cdot\\
    \rho[B/\beta]       &\defas& \begin{cases}
@@ -848,8 +889,9 @@ rule admits a continuation.
 %
 
 The semantics are based on a substitution model of computation. Thus,
-before presenting the reduction rules, we define an adequacy
-substitution function.
+before presenting the reduction rules, we define an adequate
+substitution function. As usual we work up to
+$\alpha$-conversion~\cite{Church32} of terms in $\BCalc{}$.
 %
 \paragraph{Term substitution}
 We write $M[V/x]$ for the substitution of some value $V$ for some
@@ -870,42 +912,62 @@ and we realise it by pattern matching on the first argument.
                                      V & \text{if } x = y\\
                                      x & \text{otherwise }
                                    \end{cases}\\
-    (\lambda x^A.M)[V/y] &\defas& \begin{cases}
-                                    \lambda x^A.M & \text{if } x = y\\
-                                    \lambda x^A.M[V/y] & \text{otherwise}
-                                  \end{cases}\\
+    (\lambda x^A.M)[V/y] &\defas& \lambda x^A.M[V/y] \quad \text{if } x \neq y \text{ and } x \notin \FV(V)\\
     (\Lambda \alpha^K. M)[V/y] &\defas& \Lambda \alpha^K. M[V/y]\\
     \Unit[V/y]           &\defas& \Unit\\
     \Record{\ell = W; W'}[V/y] &\defas& \Record{\ell = W[V/y]; W'[V/y]}\\
     (\ell~W)^R[V/y]      &\defas& (\ell~W[V/y])^R\\
     (W\,W')[V/y]         &\defas& W[V/y]\,W'[V/y]\\
-    (W\,A)[V/y]          &\defas& W[V/y]~A\\
-    (\Let\;\Record{\ell = x; y} = W\;\In\;N)[V/y] &\defas& \Let\;\Record{\ell = x; y} = W[V/y] \;\In\;N[V/y]\\
-    (\Case\;(\ell~V)^R\{\ba[t]{@{}l} \ell~x \mapsto M\\
-                                    ; y \mapsto N \})[V/z]\ea
-                                &\defas& \begin{cases}
-      \Case\;(\ell~V)^R\{\ell~x \mapsto M; y \mapsto N \} & \text{if } x = y = z\\
-      \Case\;(\ell~V)^R\{\ba[t]{@{}l} \ell~x \mapsto M\\
-                                      ; y \mapsto N[V/z] \}\ea & \text{if } x = z \text{ and } y \neq z\\
-      \Case\;(\ell~V)^R\{ \ba[t]{@{}l}\ell~x \mapsto M[V/z]\\
-                                      ; y \mapsto N \}\ea & \text{if } x \neq z \text{ and } y = z\\
-      \Case\;(\ell~V)^R\{ \ba[t]{@{}l} \ell~x \mapsto M[V/z]\\
-                                       ; y \mapsto N[V/z] \}\ea & \text{otherwise}
-                                         \end{cases}\\
-    (\Let\;x \revto M \;\In\;N)[V/y] &\defas& \begin{cases}
-                                                 \Let\;x \revto M[V/y]\;\In\;N & \text{if } x = y\\
-                                                 \Let\;x \revto M[V/y]\;\In\;N[V/y] & \text{otherwise}
-                                              \end{cases}
-  \end{eqs}
-\]
+    (W\,T)[V/y]          &\defas& W[V/y]~T\\
+    (\ba[t]{@{}l}
+      \Let\;\Record{\ell = x; y} = W\\
+      \In\;N)[V/z]
+     \ea &\defas&
+       \ba[t]{@{~}l}
+          \Let\;\Record{\ell = x; y} = W[V/z]\\
+          \In\;N[V/z]
+       \ea \quad
+         \ba[t]{@{}l}
+           \text{if } x \neq z, y \neq z,\\
+           \text{and } x,y\notin \FV(V)
+         \ea\\
+     (\Case\;(\ell~W)^R\{
+       \ba[t]{@{}l}
+         \ell~x \mapsto M\\
+         ; y \mapsto N \})[V/z]
+       \ea
+       &\defas&
+                 \Case\;(\ell~W[V/z])^R\{
+                   \ba[t]{@{}l}
+                     \ell~x \mapsto M[V/z]\\
+                     ; y \mapsto N[V/z] \}
+                   \ea\quad
+                        \ba[t]{@{}l}
+                          \text{if } x \neq z, y \neq z,\\
+                          \text{and } x, y \notin \FV(V)
+                        \ea\\
+     (\Let\;x \revto M \;\In\;N)[V/y] &\defas& \Let\;x \revto M[V/y] \;\In\;N[V/y] \quad\text{if } x \neq y \text{ and } x \notin \FV(V)
+   \end{eqs}
+ \]
+                        %
+                        % \begin{cases}
+                                              %    \Let\;x \revto M[V/y]\;\In\;N & \text{if } x = y\\
+                                              %    \Let\;x \revto M[V/y]\;\In\;N[V/y] & \text{otherwise}
+                                              % \end{cases}
+  % \end{eqs}
 %
+ We write $t[t_0/x_0,\dots,t_n/x_n]$ to mean the simultaneous
+ substitution of $t_0$ for $x_0$ up to $t_n$ for $x_n$ in $t$.
+ %
+
 
 \paragraph{Reduction semantics}
-Figure~\ref{fig:base-language-small-step} depicts the reduction
-rules. The application rules \semlab{App} and \semlab{TyApp}
-eliminates a lambda and type abstraction, respectively, by
-substituting the argument for the parameter in their body computation
-$M$.
+The reduction relation $\reducesto : \CompCat \pto \CompCat$ is defined
+on computation terms. Figure~\ref{fig:base-language-small-step}
+depicts the reduction rules. The application rules \semlab{App} and
+\semlab{TyApp} eliminates a lambda and type abstraction, respectively,
+by substituting the argument for the parameter in their body
+computation $M$.
 %
 Record splitting is handled by the \semlab{Split} rule: splitting on
 some label $\ell$ binds the payload $V$ to $x$ and the remainder $W$
@@ -958,6 +1020,22 @@ Thus far we have defined the syntax, static semantics, and dynamic
 semantics of \BCalc{}. In this section, we finish the definition of
 \BCalc{} by stating and proving some standard metatheoretic properties
 about the language.
+%
+
+We begin by showing that type substitutions preserve typability.
+%
+\begin{lemma}[Preservation of typing under type substitution]
+  Let $\sigma$ be any type substitution and $V$ be a value and $M$ a
+  computation such that $\typ{\Delta;\Gamma}{V : A}$ and
+  $\typ{\Delta;\Gamma}{M : C}$, then
+  $\typ{\Delta;\sigma~\Gamma}{\sigma~V : \sigma~A}$ and
+  $\typ{\Delta;\sigma~\Gamma}{\sigma~M : \sigma~C}$.
+\end{lemma}
+%
+\begin{proof}
+  By induction on the typing derivations.
+\end{proof}
+%
 
 \section{Primitive effect: general recursion}
 \label{sec:base-language-recursion}