From 6aa8f1049ce1d6b284c4fb49a3bbc885e2cc0501 Mon Sep 17 00:00:00 2001 From: Jonathan Chan Date: Sat, 19 Apr 2025 09:56:22 -0400 Subject: [PATCH] Blurb about accessibility strong normalization --- cbpv.mng | 49 ++++++++++++++++++++++++++++++++++++++++++++----- cbpv.pdf | 4 ++-- cbpv.tex | 49 ++++++++++++++++++++++++++++++++++++++++++++----- 3 files changed, 90 insertions(+), 12 deletions(-) diff --git a/cbpv.mng b/cbpv.mng index 4b93e1e..05c51b5 100644 --- a/cbpv.mng +++ b/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} diff --git a/cbpv.pdf b/cbpv.pdf index 17b26c8..8073c2a 100644 --- a/cbpv.pdf +++ b/cbpv.pdf @@ -1,3 +1,3 @@ version https://git-lfs.github.com/spec/v1 -oid sha256:5ac9dfc36f6dc1a73d3878b7c4408b89a4e7b44653d9f6f759289da3c0919b46 -size 262118 +oid sha256:6b47374d9c9e93b76795f55b889583534a95ee4308ff58da760aad9ede4b3084 +size 271966 diff --git a/cbpv.tex b/cbpv.tex index 9c95ee3..d66ff0e 100644 --- a/cbpv.tex +++ b/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}