ionchy
/
CIS6700-Spring2025
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Edits

This commit is contained in:
Jonathan Chan 2025-04-21 16:53:41 -04:00
parent 6374d0a819
commit 392cced2a2
4 changed files with 32 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
cbpv.bib
View File

@ -1,4 +1,4 @@
@inproceedings{cbpv, @inproceedings{cbpv-coq,
author = {Forster, Yannick and Sch\"{a}fer, Steven and Spies, Simon and Stark, Kathrin}, author = {Forster, Yannick and Sch\"{a}fer, Steven and Spies, Simon and Stark, Kathrin},
title = {{Call-by-push-value in Coq: operational, equational, and denotational theory}}, title = {{Call-by-push-value in Coq: operational, equational, and denotational theory}},
year = 2019, year = 2019,
@ -39,3 +39,10 @@
location = {Cascais, Portugal}, location = {Cascais, Portugal},
series = {CPP 2019} series = {CPP 2019}
} }
@phdthesis{cbpv,
author = {Levy, Paul Blain},
school = {Queen Mary University of London},
title = {{Call-by-push-value}},
year = {2001}
}

22
cbpv.mng
View File

@ -44,8 +44,8 @@
\section{Introduction} \section{Introduction}
The goal of this project is to mechanize a proof of strong normalization for call-by-push-value (CBPV). The goal of this project is to mechanize a proof of strong normalization for call-by-push-value (CBPV) \citep{cbpv}.
It follows work by Forster, Sch\"afer, Spies, and Stark \citep{cbpv} on mechanizing the metatheory of CBPV in Rocq, It follows work by Forster, Sch\"afer, Spies, and Stark \citep{cbpv-coq} on mechanizing the metatheory of CBPV in Rocq,
but instead adapts the proof technique from POPLMark Reloaded \citep{poplmark}. but instead adapts the proof technique from POPLMark Reloaded \citep{poplmark}.
Both proofs, and mine, follow the same sequence of steps: Both proofs, and mine, follow the same sequence of steps:
@ -150,19 +150,19 @@ The general recipe for defining these for CBPV is as follows:
whose head positions are strongly neutral, whose head positions are strongly neutral,
while all other subterms are strongly normal. while all other subterms are strongly normal.
\item Strongly normal values are constructors \item Strongly normal values are constructors
whose subterms are strongly normal, with strongly normal subterms
or strongly neutral values, \ie variables. or strongly neutral values.
\item Strongly normal computations are constructors \item Strongly normal computations are constructors
whose subterms are strongly normal, with strongly normal subterms,
or strongly neutral computations, strongly neutral computations,
or computations which reduce to strongly normal computations or computations that reduce to strongly normal computations
(backward closure). (backward closure).
\item Strong head reduction consists of $\beta$ reductions \item Strong head reduction consists of $\beta$ reductions
for all eliminators around the corresponding constructors, for all eliminators around the corresponding constructors,
and congruent reductions in head positions. and congruent reductions in head positions.
\end{itemize} \end{itemize}
Additionally, strong reduction requires premises asserting that Additionally, head reduction requires premises asserting that
the subterms that may ``disappear'' after reduction be strongly normal the subterms that may ``disappear'' after reduction be strongly normal
so that backward closure actually closes over strongly normal terms. so that backward closure actually closes over strongly normal terms.
These subterms are the values that get substituted into a computation, These subterms are the values that get substituted into a computation,
@ -261,7 +261,7 @@ However, I want to maximize the amount of mutual inductives used in this project
so we instead define the logical relation as an inductive binary relation so we instead define the logical relation as an inductive binary relation
between the type and the set of terms of its interpretation, between the type and the set of terms of its interpretation,
denoted as $[[⟦A⟧ ↘ P]]$ and $[[⟦B⟧ ↘ P]]$ below. denoted as $[[⟦A⟧ ↘ P]]$ and $[[⟦B⟧ ↘ P]]$ below.
I use set builder notation to define the sets and set membership, I use set builder and set membership notation,
but they are implemented in the mechanization as functions but they are implemented in the mechanization as functions
that take terms and return propositions and as function applications. that take terms and return propositions and as function applications.
Here, the conjunctions ($\wedge$), disjunctions ($\vee$), equalities ($=$), implications ($\Rightarrow$), Here, the conjunctions ($\wedge$), disjunctions ($\vee$), equalities ($=$), implications ($\Rightarrow$),
@ -661,7 +661,7 @@ of the structure of both reductions.
Strong reduction of the head position eliminates the cases of $\beta$-reduction, Strong reduction of the head position eliminates the cases of $\beta$-reduction,
leaving the cases where the head position steps or the other position steps. leaving the cases where the head position steps or the other position steps.
If the head position steps, we use \nameref{lem:commute} If the head position steps, we use \nameref{lem:commute}
to join the strong reduction and the single-step reduction together, to join the strong head reduction and the single-step reduction together,
then use the first induction hypothesis. then use the first induction hypothesis.
Otherwise, we use the second induction hypothesis. Otherwise, we use the second induction hypothesis.
We need the last premise to step through either of the subterms, We need the last premise to step through either of the subterms,
@ -710,7 +710,7 @@ traditional strong normalization of well typed terms holds as a corollary.
The cases for the first three correspond to the admissible strongly normal rules, The cases for the first three correspond to the admissible strongly normal rules,
using \nameref{lem:sound-sne} as needed, using \nameref{lem:sound-sne} as needed,
except for the \rref*{SN-Red} case, which uses \nameref{lem:closure-sn}. except for the \rref*{SN-Red} case, which uses \nameref{lem:closure-sn}.
The cases for strong reduction hold by construction. The cases for strong head reduction hold by construction.
\end{proof} \end{proof}
\begin{corollary} \begin{corollary}

BIN
cbpv.pdf (Stored with Git LFS)
View File

Binary file not shown.

22
cbpv.tex
View File

@ -44,8 +44,8 @@
\section{Introduction} \section{Introduction}
The goal of this project is to mechanize a proof of strong normalization for call-by-push-value (CBPV). The goal of this project is to mechanize a proof of strong normalization for call-by-push-value (CBPV) \citep{cbpv}.
It follows work by Forster, Sch\"afer, Spies, and Stark \citep{cbpv} on mechanizing the metatheory of CBPV in Rocq, It follows work by Forster, Sch\"afer, Spies, and Stark \citep{cbpv-coq} on mechanizing the metatheory of CBPV in Rocq,
but instead adapts the proof technique from POPLMark Reloaded \citep{poplmark}. but instead adapts the proof technique from POPLMark Reloaded \citep{poplmark}.
Both proofs, and mine, follow the same sequence of steps: Both proofs, and mine, follow the same sequence of steps:
@ -150,19 +150,19 @@ The general recipe for defining these for CBPV is as follows:
whose head positions are strongly neutral, whose head positions are strongly neutral,
while all other subterms are strongly normal. while all other subterms are strongly normal.
\item Strongly normal values are constructors \item Strongly normal values are constructors
whose subterms are strongly normal, with strongly normal subterms
or strongly neutral values, \ie variables. or strongly neutral values.
\item Strongly normal computations are constructors \item Strongly normal computations are constructors
whose subterms are strongly normal, with strongly normal subterms,
or strongly neutral computations, strongly neutral computations,
or computations which reduce to strongly normal computations or computations that reduce to strongly normal computations
(backward closure). (backward closure).
\item Strong head reduction consists of $\beta$ reductions \item Strong head reduction consists of $\beta$ reductions
for all eliminators around the corresponding constructors, for all eliminators around the corresponding constructors,
and congruent reductions in head positions. and congruent reductions in head positions.
\end{itemize} \end{itemize}
Additionally, strong reduction requires premises asserting that Additionally, head reduction requires premises asserting that
the subterms that may ``disappear'' after reduction be strongly normal the subterms that may ``disappear'' after reduction be strongly normal
so that backward closure actually closes over strongly normal terms. so that backward closure actually closes over strongly normal terms.
These subterms are the values that get substituted into a computation, These subterms are the values that get substituted into a computation,
@ -261,7 +261,7 @@ However, I want to maximize the amount of mutual inductives used in this project
so we instead define the logical relation as an inductive binary relation so we instead define the logical relation as an inductive binary relation
between the type and the set of terms of its interpretation, between the type and the set of terms of its interpretation,
denoted as $ \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} \searrow \ottnt{P} $ and $ \mathopen{\llbracket} \ottnt{B} \mathclose{\rrbracket} \searrow \ottnt{P} $ below. denoted as $ \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} \searrow \ottnt{P} $ and $ \mathopen{\llbracket} \ottnt{B} \mathclose{\rrbracket} \searrow \ottnt{P} $ below.
I use set builder notation to define the sets and set membership, I use set builder and set membership notation,
but they are implemented in the mechanization as functions but they are implemented in the mechanization as functions
that take terms and return propositions and as function applications. that take terms and return propositions and as function applications.
Here, the conjunctions ($\wedge$), disjunctions ($\vee$), equalities ($=$), implications ($\Rightarrow$), Here, the conjunctions ($\wedge$), disjunctions ($\vee$), equalities ($=$), implications ($\Rightarrow$),
@ -661,7 +661,7 @@ of the structure of both reductions.
Strong reduction of the head position eliminates the cases of $\beta$-reduction, Strong reduction of the head position eliminates the cases of $\beta$-reduction,
leaving the cases where the head position steps or the other position steps. leaving the cases where the head position steps or the other position steps.
If the head position steps, we use \nameref{lem:commute} If the head position steps, we use \nameref{lem:commute}
to join the strong reduction and the single-step reduction together, to join the strong head reduction and the single-step reduction together,
then use the first induction hypothesis. then use the first induction hypothesis.
Otherwise, we use the second induction hypothesis. Otherwise, we use the second induction hypothesis.
We need the last premise to step through either of the subterms, We need the last premise to step through either of the subterms,
@ -710,7 +710,7 @@ traditional strong normalization of well typed terms holds as a corollary.
The cases for the first three correspond to the admissible strongly normal rules, The cases for the first three correspond to the admissible strongly normal rules,
using \nameref{lem:sound-sne} as needed, using \nameref{lem:sound-sne} as needed,
except for the \rref*{SN-Red} case, which uses \nameref{lem:closure-sn}. except for the \rref*{SN-Red} case, which uses \nameref{lem:closure-sn}.
The cases for strong reduction hold by construction. The cases for strong head reduction hold by construction.
\end{proof} \end{proof}
\begin{corollary} \begin{corollary}