From 4259ddee4de20759523337dd01dc368d0a666ee5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= <daniel.hillerstrom@ed.ac.uk>
Date: Fri, 28 May 2021 00:07:19 +0100
Subject: [PATCH] WIP

---
 thesis.tex | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/thesis.tex b/thesis.tex
index ac73457..25cde89 100644
--- a/thesis.tex
+++ b/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}