diff --git a/macros.tex b/macros.tex index c734a9b..decf248 100644 --- a/macros.tex +++ b/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}}}}{=}}} \ No newline at end of file +\newcommand{\defas}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\text{def}}}}{=}}} + +%% +%% Partiality +%% +\newcommand{\pto}[0]{\ensuremath{\rightharpoonup}} \ No newline at end of file diff --git a/thesis.bib b/thesis.bib index 9e139c9..8851d2d 100644 --- a/thesis.bib +++ b/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} +} \ No newline at end of file diff --git a/thesis.tex b/thesis.tex index ba959c4..8cb5865 100644 --- a/thesis.tex +++ b/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}