WIP

thesis.tex

@@ -2367,6 +2367,12 @@ special instance of a statically typed programming language, where the
 typechecking function $T$ is the constant function that always returns
 true.
 
+Often we will build programming languages incrementally by starting
+from a base language and extend it with new facilities. A
+\emph{conservative extension} is a particularly well-behaved extension
+in the sense that it preserves the all of the behaviour of the
+original language.
+%
 \begin{definition}
   A programming language $\LLL = (S, T, E)$ is said to be a
   \emph{conservative extension} of a language $\LLL' = (S', T', E')$
@@ -2374,10 +2380,10 @@ true.
   \begin{itemize}
     \item $S'$ is a proper subset of $S$.
     \item $\LLL$ preserves the static semantics of $\LLL'$,
-      i.e. $T(P)$ holds if and only if $T'(P)$ holds for all programs
-      $P$ generated by $S'$.
+      i.e. $T(p)$ holds if and only if $T'(p)$ holds for all programs
+      $p$ generated by $S'$.
     \item $\LLL$ preserves the dynamic semantics of $\LLL'$, i.e.
-      $E(P)$ holds if and only if $E'(P)$ holds for all programs $P$
+      $E(p)$ holds if and only if $E'(p)$ holds for all programs $p$
       generated by $S'$.
   \end{itemize}
 \end{definition}