Blurb about accessibility strong normalization

cbpv.mng

@@ -9,7 +9,7 @@
 \usepackage{enumitem,float,booktabs,xspace,doi}
 \usepackage{amsmath,amsthm,amssymb}
 \usepackage[capitalize,nameinlink,noabbrev]{cleveref}
-\usepackage{mathpartir,mathtools,stmaryrd}
+\usepackage{mathpartir,mathtools,stmaryrd,latexsym}
 
 \setlist{nosep}
 \hypersetup{
@@ -187,7 +187,7 @@ I present them below as judgement pseudorules
 using a dashed line to indicate that they are admissible rules.
 These are all proven either by construction
 or by induction on the first premise.
-
+%
 \begin{mathpar}
 \mprset{fraction={-~}{-~}{-}}
 \drule[]{SRs-Once}
@@ -481,7 +481,46 @@ Normalization holds as a corollary.
 
 \section{Strong Normalization as an Accessibility Relation} \label{sec:sn-acc}
 
-\drules[sn]{$[[v ∈ sn]], [[m ∈ sn]]$}{strongly normalizing terms}{Val,Com}
+How do we know that our definition of strongly normal terms is correct?
+What are the properties that define its correctness?
+It seems to be insufficient to talk about strongly neutral and normal terms alone.
+
+For instance, we could add another rule asserting that $[[m ∈ SN]]$ if $[[m ⤳ m]]$,
+which doesn't appear to violate any of the existing properties we require.
+Then $[[(λx. (force x) x) (thunk (λx. (force x) x))]]$,
+which reduces to itself, would be considered a ``strongly normal'' term,
+and typing rules that can type this term (perhaps with a recursive type)
+would still be sound with respect to our logical relation.
+
+To try to rule out this kind of mistake in the definition,
+we might want to prove that strongly normal terms never loop,
+\ie $[[m ∈ SN ∧ m ⤳* m]]$ is impossible.
+However, this does not cover diverging terms that grow forever.
+Furthermore, $[[m ⤳ n]]$ isn't really a full reduction relation on its own,
+since it's defined mutually with strongly normal terms,
+and it doesn't describe reducing anywhere other than in the head position.
+
+The solution in POPLMark Reloaded is to prove that $\kw{SN}$ is sound
+with respect to a traditional presentation of strongly normal terms
+based on full small-step reduction $[[v ⇝ w]]$, $[[m ⇝ n]]$ of values and computations.
+I omit here the definitions of these reductions,
+but they encompass all $\beta$-reduction rules and are congruent over all subterms,
+including under binders.
+Traditional strongly normal terms, written $[[v ∈ sn]]$, $[[m ∈ sn]]$,
+are accessibility relations with respect to small-step reduction.
+Terms are inductively defined as strongly normal if they step to strongly normal terms,
+so terms which don't step are trivially normal.
+This rules out looping and diverging terms, since they never stop stepping.
+%
+% \drules[sn]{$[[v ∈ sn]], [[m ∈ sn]]$}{strongly normalizing terms}{Val,Com}
+\begin{mathpar}
+\fbox{$[[v ∈ sn]]$} \quad \fbox{$[[m ∈ sn]]$} \hfill \textit{strongly normalizing terms} \\
+\drule[]{sn-Val}
+\drule[]{sn-Com}
+\end{mathpar}
+
+
+
 \drules[sr]{$[[m ⤳' n]]$}{strong head reduction}{Thunk,Lam,Ret,Inl,Inr,App,Let}
 \drules[ne]{$[[m ∈ ne]]$}{neutral computations}{Force,App,Let,Case}
 
@@ -604,7 +643,7 @@ Normalization holds as a corollary.
   since we have no congruence rule for when the head position is not neutral.
 \end{proof}
 
-\begin{lemma}[Backward closure] \label{lem:closure}
+\begin{lemma}[Backward closure] \label{lem:closure-sn}
   If $[[m ⤳' n]]$ and $[[n ∈ sn]]$ then $[[m ∈ sn]]$.
 \end{lemma}
 
@@ -636,7 +675,7 @@ Normalization holds as a corollary.
   $[[m ∈ SNe]]$, $[[v ∈ SN]]$, $[[m ∈ SN]]$, and $[[m ⤳ n]]$.
   The cases for the first three correspond to the admissible strongly normal rules,
   using \nameref{lem:sound-sne} as needed,
-  except for the \rref*{SN-Red} case, which uses \nameref{lem:closure}.
+  except for the \rref*{SN-Red} case, which uses \nameref{lem:closure-sn}.
   The cases for strong reduction hold by construction.
 \end{proof}
 

cbpv.tex

@@ -9,7 +9,7 @@
 \usepackage{enumitem,float,booktabs,xspace,doi}
 \usepackage{amsmath,amsthm,amssymb}
 \usepackage[capitalize,nameinlink,noabbrev]{cleveref}
-\usepackage{mathpartir,mathtools,stmaryrd}
+\usepackage{mathpartir,mathtools,stmaryrd,latexsym}
 
 \setlist{nosep}
 \hypersetup{
@@ -187,7 +187,7 @@ I present them below as judgement pseudorules
 using a dashed line to indicate that they are admissible rules.
 These are all proven either by construction
 or by induction on the first premise.
-
+%
 \begin{mathpar}
 \mprset{fraction={-~}{-~}{-}}
 \drule[]{SRs-Once}
@@ -481,7 +481,46 @@ Normalization holds as a corollary.
 
 \section{Strong Normalization as an Accessibility Relation} \label{sec:sn-acc}
 
-\drules[sn]{$ \ottnt{v}  \in \kw{sn} ,  \ottnt{m}  \in \kw{sn} $}{strongly normalizing terms}{Val,Com}
+How do we know that our definition of strongly normal terms is correct?
+What are the properties that define its correctness?
+It seems to be insufficient to talk about strongly neutral and normal terms alone.
+
+For instance, we could add another rule asserting that $ \ottnt{m}  \in \kw{SN} $ if $ \ottnt{m}  \leadsto  \ottnt{m} $,
+which doesn't appear to violate any of the existing properties we require.
+Then $  (   \lambda  \ottmv{x}  \mathpunct{.}   (  \kw{force} \gap  \ottmv{x}  )    \gap  \ottmv{x}  )   \gap   (  \kw{thunk} \gap   (   \lambda  \ottmv{x}  \mathpunct{.}   (  \kw{force} \gap  \ottmv{x}  )    \gap  \ottmv{x}  )   )  $,
+which reduces to itself, would be considered a ``strongly normal'' term,
+and typing rules that can type this term (perhaps with a recursive type)
+would still be sound with respect to our logical relation.
+
+To try to rule out this kind of mistake in the definition,
+we might want to prove that strongly normal terms never loop,
+\ie $  \ottnt{m}  \in \kw{SN}   \wedge   \ottnt{m}  \leadsto^*  \ottnt{m}  $ is impossible.
+However, this does not cover diverging terms that grow forever.
+Furthermore, $ \ottnt{m}  \leadsto  \ottnt{n} $ isn't really a full reduction relation on its own,
+since it's defined mutually with strongly normal terms,
+and it doesn't describe reducing anywhere other than in the head position.
+
+The solution in POPLMark Reloaded is to prove that $\kw{SN}$ is sound
+with respect to a traditional presentation of strongly normal terms
+based on full small-step reduction $ \ottnt{v}  \rightsquigarrow  \ottnt{w} $, $ \ottnt{m}  \rightsquigarrow  \ottnt{n} $ of values and computations.
+I omit here the definitions of these reductions,
+but they encompass all $\beta$-reduction rules and are congruent over all subterms,
+including under binders.
+Traditional strongly normal terms, written $ \ottnt{v}  \in \kw{sn} $, $ \ottnt{m}  \in \kw{sn} $,
+are accessibility relations with respect to small-step reduction.
+Terms are inductively defined as strongly normal if they step to strongly normal terms,
+so terms which don't step are trivially normal.
+This rules out looping and diverging terms, since they never stop stepping.
+%
+% \drules[sn]{$ \ottnt{v}  \in \kw{sn} ,  \ottnt{m}  \in \kw{sn} $}{strongly normalizing terms}{Val,Com}
+\begin{mathpar}
+\fbox{$ \ottnt{v}  \in \kw{sn} $} \quad \fbox{$ \ottnt{m}  \in \kw{sn} $} \hfill \textit{strongly normalizing terms} \\
+\drule[]{sn-Val}
+\drule[]{sn-Com}
+\end{mathpar}
+
+
+
 \drules[sr]{$ \ottnt{m}  \leadsto_{ \kw{sn} }  \ottnt{n} $}{strong head reduction}{Thunk,Lam,Ret,Inl,Inr,App,Let}
 \drules[ne]{$ \ottnt{m}  \in \kw{ne} $}{neutral computations}{Force,App,Let,Case}
 
@@ -604,7 +643,7 @@ Normalization holds as a corollary.
   since we have no congruence rule for when the head position is not neutral.
 \end{proof}
 
-\begin{lemma}[Backward closure] \label{lem:closure}
+\begin{lemma}[Backward closure] \label{lem:closure-sn}
   If $ \ottnt{m}  \leadsto_{ \kw{sn} }  \ottnt{n} $ and $ \ottnt{n}  \in \kw{sn} $ then $ \ottnt{m}  \in \kw{sn} $.
 \end{lemma}
 
@@ -636,7 +675,7 @@ Normalization holds as a corollary.
   $ \ottnt{m}  \in \kw{SNe} $, $ \ottnt{v}  \in \kw{SN} $, $ \ottnt{m}  \in \kw{SN} $, and $ \ottnt{m}  \leadsto  \ottnt{n} $.
   The cases for the first three correspond to the admissible strongly normal rules,
   using \nameref{lem:sound-sne} as needed,
-  except for the \rref*{SN-Red} case, which uses \nameref{lem:closure}.
+  except for the \rref*{SN-Red} case, which uses \nameref{lem:closure-sn}.
   The cases for strong reduction hold by construction.
 \end{proof}