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

Formatting

This commit is contained in:
Jonathan Chan 2025-04-21 14:37:15 -04:00
parent b24ea900cd
commit b1ce61eaf2
3 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
cbpv.mng
View File

@ -505,7 +505,7 @@ and it doesn't describe reducing anywhere other than in the head position.
The solution we take from 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.
based on full small-step reduction \fbox{$[[v ⇝ w]]$}, \fbox{$[[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.

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

Binary file not shown.

2
cbpv.tex
View File

@ -505,7 +505,7 @@ and it doesn't describe reducing anywhere other than in the head position.
The solution we take from 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.
based on full small-step reduction \fbox{$ \ottnt{v} \rightsquigarrow \ottnt{w} $}, \fbox{$ \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.