Merge remote-tracking branch 'origin/main' into week8

week6.tex

@@ -63,8 +63,8 @@ \subsection{Syntax}
 
 \subsection{Statics}
 
-Aside from the typical pure expression typing judgement, we introduce 2 new typing judgements: $\Gamma \entails{\retsTp{E}{A}}$ for computation expressions, and $\accsTp{K}{A}$ for stacks.
-These judgements have the following additional statics rules:
+Aside from the typical pure expression typing judgement, we introduce 2 new typing judgments: $\Gamma \entails{\retsTp{E}{A}}$ for computation expressions, and $\accsTp{K}{A}$ for stacks.
+These judgments have the following additional statics rules:
 
 \begin{mathpar}
   \defrule[Lax-I][sta:comp]
@@ -105,9 +105,9 @@ \subsection{Statics}
 
 \subsection{Dynamics}
 
-The dynamics for much of the language is as we would expect; here, we present some of the new judgements and semantics.
-Specifically, with control flow stacks, we have the judgements $K \vartriangleright E$ (computation $E$ is evaluated under context $K$) and $K \vartriangleleft V$ (value $V$ is returned to stack $K$).
-These judgements have additional statics rules as follows:
+The dynamics for much of the language is as we would expect; here, we present some of the new judgments and semantics.
+Specifically, with control flow stacks, we have the judgments $K \vartriangleright E$ (computation $E$ is evaluated under context $K$) and $K \vartriangleleft V$ (value $V$ is returned to stack $K$).
+These judgments have additional statics rules as follows:
 
 \begin{mathpar}
   \defrule[Eval-OK][sta:eval]
@@ -122,7 +122,7 @@ \subsection{Dynamics}
 \end{mathpar}
 
 Note that when evaluating an expression in a given context, we cannot have any free variables in that expression.
-We further introduce the judgements $\isVal{M}$ stating that a pure expression is a value, $\iniSt{K \vartriangleright E}$ stating that this context and impure computation are the initial program state, and $\finSt{K \vartriangleleft V}$ stating that this context and value are the final program state.
+We further introduce the judgments $\isVal{M}$ stating that a pure expression is a value, $\iniSt{K \vartriangleright E}$ stating that this context and impure computation are the initial program state, and $\finSt{K \vartriangleleft V}$ stating that this context and value are the final program state.
 We also have the notion of pure expression evaluation $M \Downarrow V$, which is the same as $M \stepsTo^* V$.
 We can now define the interesting dynamics rules:
 
@@ -195,13 +195,13 @@ \section{Termination}
   \item $\HTe[A](E)$ iff $\HTk[A](K)$ implies $K \vartriangleright E \Downarrow$
 \end{itemize}
 
-The termination judgements for pure expressions are straightforward; for expressions of base types, they must evaluate to the base values, and for expressions of higher types, they must evaluate to "well-behaved" values of that type.
+The termination judgments for pure expressions are straightforward; for expressions of base types, they must evaluate to the base values, and for expressions of higher types, they must evaluate to "well-behaved" values of that type.
 For continuation and computation termination, we have a slightly more interesting formulation.
 Termination on stacks is defined in terms of eliminations; stacks are well-behaved if and only if upon returning any well-behaved value to it, evaluation will eventually terminate.
 And termination on impure computations is defined in terms of introductions; they are well-behaved if and only if evaluating them in any well-behaved context will eventually terminate.
 This flows fairly naturally from how computations and stacks work intuitively; stacks are only useful if you can return values to them, and computations are only useful if you can evaluate them in some context.
 
-We also define the judgements $\exref{\Gamma}{M}{A}$ to mean that if $\HT[\Gamma](\gamma)$ then $\HT[A](\hat{\gamma}(M))$, $\exrefe{\Gamma}{E}{A}$ to mean that if $\HT[\Gamma](\gamma)$ then $\HTe[A](\hat{\gamma}(E))$, and finally $\exrefk{K}{A}$ to mean that $\HTk[A](K)$.
+We also define the judgments $\exref{\Gamma}{M}{A}$ to mean that if $\HT[\Gamma](\gamma)$ then $\HT[A](\hat{\gamma}(M))$, $\exrefe{\Gamma}{E}{A}$ to mean that if $\HT[\Gamma](\gamma)$ then $\HTe[A](\hat{\gamma}(E))$, and finally $\exrefk{K}{A}$ to mean that $\HTk[A](K)$.
 Note that the continuation judgement does not involve a context.
 Finally, we present the relevant lemmas and the fundamental theorem:
 
@@ -222,7 +222,7 @@ \section{Termination}
   \end{itemize}
 \end{theorem}
 
-This is proved by induction on the typing judgements.
+This is proved by induction on the typing judgments.
 A particular corollary of the fundamental theorem is that if we have some closed computation $\empCtx \entails{\retsTp{E}{\ansTy}}$, then $\empStk* \vartriangleright E$ will terminate.
 In other words, any well-typed initial-state program is guaranteed to terminate!