Define a macro for definitional equality up to alpha-conversion.

macros.tex

@@ -161,6 +161,7 @@
 %%
 \newcommand{\defas}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\text{def}}}}{=}}}
 \newcommand{\defnas}[0]{\mathrel{:=}}
+\newcommand{\simdefas}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\text{def}}}}{\simeq}}}
 
 %%
 %% Partiality

thesis.tex

@@ -619,7 +619,7 @@ structure as follows.
    \begin{eqs}
     (A \eff E)\sigma &\defas& A\sigma \eff E\sigma\\
     (A \to C)\sigma &\defas& A\sigma \to C\sigma\\
-    (\forall \alpha^K.C)\sigma &\defas& \forall \alpha^K.C\sigma \quad \text{convert if } \alpha \in \dom(\sigma)\\
+    (\forall \alpha^K.C)\sigma &\simdefas& \forall \alpha^K.C\sigma\\
     \alpha\sigma     &\defas& \begin{cases}
                                       A & \text{if } (\alpha,A) \in \sigma\\
                                  \alpha & \text{otherwise}
@@ -976,7 +976,7 @@ cannot be satisfied.
 
 \paragraph{Typing computations}
 The \tylab{App} rule states that an application $V\,W$ has computation
-type $C$ if the abstractor term $V$ has type $A \to C$ and the
+type $C$ if the function-term $V$ has type $A \to C$ and the
 argument term $W$ has type $A$, that is both the argument type and the
 domain type of the abstractor agree.
 %
@@ -1050,87 +1050,83 @@ that the binder $x : A$.
 \label{fig:base-language-small-step}
 \end{figure}
 %
-In this section we present the dynamic semantics of \BCalc{}. We
+In this section we present the dynamic semantics of \BCalc{}. We opt
-choose to use a contextual small-step semantics, since in conjunction
+to use a \citet{Felleisen87}-style contextual small-step semantics,
-with fine-grain call-by-value, it yields a considerably simpler
+since in conjunction with fine-grain call-by-value (FGCBV), it yields
-semantics than the traditional structural operational semantics
+a considerably simpler semantics than the traditional structural
-(SOS)~\cite{Plotkin04a}, because only the rule for let bindings admits
+operational semantics (SOS)~\cite{Plotkin04a}, because only the rule
-a continuation whereas in ordinary call-by-value SOS each congruence
+for let bindings admits a continuation wheres in ordinary
-rule admits a continuation.
+call-by-value SOS each congruence rule admits a continuation.
 %
+The simpler semantics comes at the expense of a more verbose syntax,
+which is not a concern as one can readily convert between fine-grain
+call-by-value and ordinary call-by-value.
 
-The semantics are based on a substitution model of computation. Thus,
+The reduction semantics are based on a substitution model of
-before presenting the reduction rules, we define an adequate
+computation. Thus, before presenting the reduction rules, we define an
-substitution function. As usual we work up to
+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
+We define a term substitution map,
-variable $x$ in some computation term $M$. We use the same notation
+$\sigma : (\VarCat \times \ValCat)^\ast$ as list of pairs mapping a
-for substitution on values, i.e. $W[V/x]$ denotes the substitution of
+variable to its value replacement. We denote a single mapping as $V/x$
-$V$ for $x$ in some value $W$. We define substitution as a ternary
+meaning substitute $V$ for the variable $x$. We write multiple
-function, whose signature is given by
+mappings using list notation, i.e. $[V_0/x_0,\dots,V_n/x_n]$. The
+domain of a substitution map is set generated by projecting the first
+component, i.e.
 %
 \[
--[-/-] : \TermCat \times \ValCat \times \VarCat \to \CompCat,
+  \bl
+     \dom : (\VarCat \times \ValCat)^\ast  \to \ValCat\\
+     \dom(\sigma) \defas \{ x \mid (\_/x) \in \sigma \}
+  \el
 \]
 %
-and we realise it by pattern matching on the first argument.
+The application of a type substitution map on a term $t \in \TermCat$,
+written $t\sigma$, is defined inductively on the term structure as
+follows.
 %
 \[
+\ba[t]{@{~}l@{~}c@{~}r}
+   \begin{eqs}
+     x\sigma &\defas& \begin{cases}
+                          V & \text{if } (x, V) \in \sigma\\
+                          x & \text{otherwise}
+                      \end{cases}\\
+    (\lambda x^A.M)\sigma &\simdefas& \lambda x^A.M\sigma\\
+    (\Lambda \alpha^K.M)\sigma &\defas& \Lambda \alpha^K.M\sigma\\
+    (V~T)\sigma     &\defas& V\sigma~T
+  \end{eqs}
+  &~~&
   \begin{eqs}
-    x[V/y]               &\defas& \begin{cases}
+    (V~W)\sigma      &\defas& V\sigma~W\sigma\\
-                                     V & \text{if } x = y\\
+    \Unit\sigma      &\defas& \Unit\\
-                                     x & \text{otherwise }
+    \Record{\ell = V; W}\sigma &\defas& \Record{\ell = V\sigma;W\sigma}\\
-                                   \end{cases}\\
+    (\ell~V)^R\sigma &\defas& (\ell~V\sigma)^R\\
-    (\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)\\
+  \end{eqs}\bigskip\\
-    (\Lambda \alpha^K. M)[V/y] &\defas& \Lambda \alpha^K. M[V/y]\\
+  \multicolumn{3}{c}{
-    \Unit[V/y]           &\defas& \Unit\\
+    \begin{eqs}
-    \Record{\ell = W; W'}[V/y] &\defas& \Record{\ell = W[V/y]; W'[V/y]}\\
+      (\Let\;\Record{\ell = x; y} = V\;\In\;N)\sigma &\simdefas& \Let\;\Record{\ell = x; y} = V\sigma\;\In\;N\sigma\\
-    (\ell~W)^R[V/y]      &\defas& (\ell~W[V/y])^R\\
+      (\Case\;(\ell~V)^R\{
-    (W\,W')[V/y]         &\defas& W[V/y]\,W'[V/y]\\
+          \ell~x \mapsto M
-    (W\,T)[V/y]          &\defas& W[V/y]~T\\
+          ; y \mapsto N \})\sigma
-    (\ba[t]{@{}l}
+       &\simdefas&
-      \Let\;\Record{\ell = x; y} = W\\
+       \Case\;(\ell~V\sigma)^R\{
-      \In\;N)[V/z]
+         \ell~x \mapsto M\sigma
-     \ea &\defas&
+         ; y \mapsto N\sigma \}\\
-       \ba[t]{@{~}l}
+     (\Let\;x \revto M \;\In\;N)\sigma &\simdefas& \Let\;x \revto M[V/y] \;\In\;N\sigma
-          \Let\;\Record{\ell = x; y} = W[V/z]\\
+   \end{eqs}}
-          \In\;N[V/z]
+\ea
-       \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
+The attentive reader will notice that we are using the same notation
- substitution of $t_0$ for $x_0$ up to $t_n$ for $x_n$ in $t$.
+for type and term substitutions. We justify this choice by the fact
- %
+that we can lift type substitution pointwise on the term syntax
-
+constructors, enabling us to use one uniform notation for
+substitution. Thus we shall generally allow a mix of pairs of
+variables and values and pairs of type variables and types to occur in
+the same substitution map.
 
 \paragraph{Reduction semantics}
 The reduction relation $\reducesto : \CompCat \pto \CompCat$ is defined