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

Edits up to section 7

This commit is contained in:
Jonathan Chan 2025-04-22 12:21:13 -04:00
parent 392cced2a2
commit 98cfb5b7de
5 changed files with 62 additions and 58 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

51
cbpv.mng
View File

@ -173,7 +173,7 @@ Because we're dealing with CBPV, values have no $\beta$ reductions,
so there's no need for head reduction of values as there are no heads. so there's no need for head reduction of values as there are no heads.
Furthermore, there is only one strongly neutral value, Furthermore, there is only one strongly neutral value,
so we inline the definition as a variable where needed, so we inline the definition as a variable where needed,
but also write it as $[[v ∈ SNe]]$ for symmetry as appropriate. but also write it as \fbox{$[[v ∈ SNe]]$} for symmetry as appropriate.
Otherwise, the remaining four judgements are defined mutually below. Otherwise, the remaining four judgements are defined mutually below.
\drules[SNe]{$[[m ∈ SNe]]$}{strongly neutral computations}{Force,App,Let,Case} \drules[SNe]{$[[m ∈ SNe]]$}{strongly neutral computations}{Force,App,Let,Case}
@ -288,7 +288,7 @@ but the alternate choices likely work as well.
or right injections whose values are in that of $[[A2]]$. or right injections whose values are in that of $[[A2]]$.
\item Computations in the interpretation of the $[[F A]]$ type \item Computations in the interpretation of the $[[F A]]$ type
reduce to either a neutral computation reduce to either a neutral computation
or a return whose value is in the interpretation of $[[A]]$. or a returned value in the interpretation of $[[A]]$.
\item Computations are in the interpretation of the function type $[[A → B]]$ \item Computations are in the interpretation of the function type $[[A → B]]$
if applying them to values in the interpretation of $[[A]]$ if applying them to values in the interpretation of $[[A]]$
yields computations in the interpretation of $[[B]]$. yields computations in the interpretation of $[[B]]$.
@ -301,7 +301,7 @@ Unfortunately, this is not well defined,
since the logical relation appears in a negative position since the logical relation appears in a negative position
(to the left of an implication) in the premise of \rref{LR'-Arr}. (to the left of an implication) in the premise of \rref{LR'-Arr}.
The alternate presentation can be interpreted as a function The alternate presentation can be interpreted as a function
match on the term and the type and returning the conjunction of its premises, matching on the term and the type and returning the conjunction of its premises,
but I wanted to use a mutually defined inductive definition. but I wanted to use a mutually defined inductive definition.
\begin{figure}[H] \begin{figure}[H]
@ -328,7 +328,7 @@ determinism, which states that the interpretation indeed behaves like a function
from types to sets of terms; from types to sets of terms;
and backward closure, which states that the interpretations of computation types and backward closure, which states that the interpretations of computation types
are backward closed under multi-step head reduction. are backward closed under multi-step head reduction.
The last property is why \rref{LR'-F-var} needs to include The last property is why \rref{LR-F} needs to include
computations that \emph{reduce to} strongly neutral terms or returns, computations that \emph{reduce to} strongly neutral terms or returns,
not merely ones that are such terms. not merely ones that are such terms.
@ -352,7 +352,7 @@ not merely ones that are such terms.
\begin{proof} \begin{proof}
By mutual induction on the first derivations of the logical relation, By mutual induction on the first derivations of the logical relation,
then by cases on the second derivations. then by cases on the second.
\end{proof} \end{proof}
\begin{lemma}[Backward closure] \label{lem:closure} \begin{lemma}[Backward closure] \label{lem:closure}
@ -361,7 +361,8 @@ not merely ones that are such terms.
\end{lemma} \end{lemma}
\begin{proof} \begin{proof}
By induction on the derivation of the logical relation. By induction on the derivation of the logical relation,
using \rref{SRs-Trans',SRs-App}.
\end{proof} \end{proof}
The final key property is adequacy, The final key property is adequacy,
@ -407,15 +408,14 @@ semantically well formed with respect to a context.
\begin{definition}[Semantic well-formedness of substitutions] \begin{definition}[Semantic well-formedness of substitutions]
A substitution $[[s]]$ is well formed with respect to a context $[[G]]$, A substitution $[[s]]$ is well formed with respect to a context $[[G]]$,
written $[[G ⊧ s]]$, if for every $[[x : A ∈ G]]$ and $[[⟦A⟧ ↘ P]]$, written \fbox{$[[G ⊧ s]]$}, if for every $[[x : A ∈ G]]$ and $[[⟦A⟧ ↘ P]]$,
we have $[[x{s} ∈ P]]$. we have $[[x{s} ∈ P]]$.
In short, the substitution maps variables in the context In short, the substitution maps variables in the context
to values in the interpretations of their types. to values in the interpretations of their types.
\end{definition} \end{definition}
These judgements can be built up inductively, These judgements can be built up inductively,
as demonstrated by the below admissible rules, as demonstrated by the below admissible rules.
which are proven by cases.
{\mprset{fraction={-~}{-~}{-}} {\mprset{fraction={-~}{-~}{-}}
\drules[S]{$[[G ⊧ s]]$}{admissible semantic substitution well-formedness}{Nil,Cons} \drules[S]{$[[G ⊧ s]]$}{admissible semantic substitution well-formedness}{Nil,Cons}
@ -427,10 +427,10 @@ using semantic well formedness of substitutions to handle the context.
\begin{definition}[Semantic typing] \begin{definition}[Semantic typing]
\begin{enumerate}[rightmargin=\leftmargin] \leavevmode \begin{enumerate}[rightmargin=\leftmargin] \leavevmode
\item $[[v]]$ semantically has type $[[A]]$ under context $[[G]]$, \item $[[v]]$ semantically has type $[[A]]$ under context $[[G]]$,
written $[[G ⊧ v : A]]$, if for every $[[s]]$ such that $[[G ⊧ s]]$, written \fbox{$[[G ⊧ v : A]]$}, if for every $[[s]]$ such that $[[G ⊧ s]]$,
there exists an interpretation $[[⟦A⟧ ↘ P]]$ such that $[[v{s} ∈ P]]$. there exists an interpretation $[[⟦A⟧ ↘ P]]$ such that $[[v{s} ∈ P]]$.
\item $[[m]]$ semantically has type $[[B]]$ under context $[[G]]$, \item $[[m]]$ semantically has type $[[B]]$ under context $[[G]]$,
written $[[G ⊧ m : B]]$, if for every $[[s]]$ such that $[[G ⊧ s]]$, written \fbox{$[[G ⊧ m : B]]$}, if for every $[[s]]$ such that $[[G ⊧ s]]$,
there exists an interpretation $[[⟦B⟧ ↘ P]]$ such that $[[m{s} ∈ P]]$. there exists an interpretation $[[⟦B⟧ ↘ P]]$ such that $[[m{s} ∈ P]]$.
\end{enumerate} \end{enumerate}
\end{definition} \end{definition}
@ -444,7 +444,7 @@ Normalization holds as a corollary.
{\mprset{fraction={-~}{-~}{-}} {\mprset{fraction={-~}{-~}{-}}
\drules[S]{$[[G ⊧ v : A]]$}{admissible semantic value typing}{Var,Unit,Inl,Inr,Thunk} \drules[S]{$[[G ⊧ v : A]]$}{admissible semantic value typing}{Var,Unit,Inl,Inr,Thunk}
\drules[S]{$[[G ⊧ m : B]]$}{admissible semantic computation typing}{Force,Arr,App,Ret,Let,Case} \drules[S]{$[[G ⊧ m : B]]$}{admissible semantic computation typing}{Force,Lam,App,Ret,Let,Case}
} }
\begin{proof} \begin{proof}
@ -509,16 +509,18 @@ with respect to a traditional presentation of strongly normal terms
based on full small-step reduction \fbox{$[[v ⇝ w]]$}, \fbox{$[[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, I omit here the definitions of these reductions,
but they encompass all $\beta$-reduction rules and are congruent over all subterms, but they encompass all $\beta$-reduction rules and are congruent over all subterms,
including under binders. including under binders,
Traditional strongly normal terms, written $[[v ∈ sn]]$, $[[m ∈ sn]]$, with \fbox{$[[v ⇝* w]]$}, \fbox{$[[m ⇝* n]]$} denoting their reflexive, transitive closures.
Traditional strongly normal terms, defined below,
are accessibility relations with respect to small-step reduction. are accessibility relations with respect to small-step reduction.
Terms are inductively defined as strongly normal if they step to strongly normal terms, Terms are inductively defined as strongly normal if they step to strongly normal terms,
so terms which don't step are trivially normal. so terms which don't step are trivially normal.
This rules out looping and diverging terms, since they never stop stepping. This rules out diverging terms, since they never stop stepping.
% %
% \drules[sn]{$[[v ∈ sn]], [[m ∈ sn]]$}{strongly normalizing terms}{Val,Com} % \drules[sn]{$[[v ∈ sn]], [[m ∈ sn]]$}{strongly normal terms}{Val,Com}
\begin{mathpar} \begin{mathpar}
\fbox{$[[v ∈ sn]]$} \quad \fbox{$[[m ∈ sn]]$} \hfill \textit{strongly normalizing terms} \\ \fbox{$[[v ∈ sn]]$} \quad \fbox{$[[m ∈ sn]]$} \hfill \textit{strongly normal terms} \\
\drule[]{sn-Val} \drule[]{sn-Val}
\drule[]{sn-Com} \drule[]{sn-Com}
\end{mathpar} \end{mathpar}
@ -544,13 +546,13 @@ The strategy is to mirror the inductive characterization,
and define corresponding notions of neutral terms and head reduction, and define corresponding notions of neutral terms and head reduction,
with strongly neutral terms being those both neutral and strongly normal. with strongly neutral terms being those both neutral and strongly normal.
As before, variables are the only neutral value, As before, variables are the only neutral value,
but we write $[[v ∈ ne]]$ to say that $[[v]]$ is a variable for symmetry. but we write \fbox{$[[v ∈ ne]]$} to say that $[[v]]$ is a variable for symmetry.
\drules[sr]{$[[m ⤳' n]]$}{strong head reduction}{Thunk,Lam,Ret,Inl,Inr,App,Let} \drules[sr]{$[[m ⤳' n]]$}{strong head reduction}{Thunk,Lam,Ret,Inl,Inr,App,Let}
\drules[ne]{$[[m ∈ ne]]$}{neutral computations}{Force,App,Let,Case} \drules[ne]{$[[m ∈ ne]]$}{neutral computations}{Force,App,Let,Case}
\begin{definition}[Strongly neutral computations] \begin{definition}[Strongly neutral computations]
A strongly neutral computation, written $[[m ∈ sne]]$, A strongly neutral computation, written \fbox{$[[m ∈ sne]]$},
is a computation that is both neutral and strongly normalizing, is a computation that is both neutral and strongly normalizing,
\ie $[[m ∈ ne]]$ and $[[m ∈ sn]]$. \ie $[[m ∈ ne]]$ and $[[m ∈ sn]]$.
\end{definition} \end{definition}
@ -616,7 +618,7 @@ we first need antisubstitution to be able to undo substitutions.
\Rref{sn-Force-Thunk} holds directly by induction on the premise; \Rref{sn-Force-Thunk} holds directly by induction on the premise;
the remaining proofs are more complex. the remaining proofs are more complex.
First, given the premise $[[m{x ↦ v} ∈ sn]]$ (or $[[n{z ↦ v}]]$), First, given the premise $[[m{x ↦ v} ∈ sn]]$ (or $[[n{z ↦ v}]]$),
use \nameref{lem:antisubst-sn} to obtain $[[m ∈ sn]]$. use \nameref{lem:antisubst-sn} to obtain $[[m ∈ sn]]$ (or $[[n ∈ sn]]$).
Then proceed by double (or triple) induction on the derivations of Then proceed by double (or triple) induction on the derivations of
$[[v ∈ sn]]$ and $[[m ∈ sn]]$ (and $[[n ∈ sn]]$ for the case rules). $[[v ∈ sn]]$ and $[[m ∈ sn]]$ (and $[[n ∈ sn]]$ for the case rules).
Similarly to the admissible strongly normal rules, Similarly to the admissible strongly normal rules,
@ -635,7 +637,7 @@ of the structure of both reductions.
\begin{lemma}[Commutativity] \label{lem:commute} \begin{lemma}[Commutativity] \label{lem:commute}
If $[[m ⇝ n1]]$ and $[[m ⤳' n2]]$, then either $[[n1]] = [[n2]]$, If $[[m ⇝ n1]]$ and $[[m ⤳' n2]]$, then either $[[n1]] = [[n2]]$,
or there exists some $[[m']]$ such that or there exists some $[[m']]$ such that
$[[n1 ⤳' m']]$ and $[[n2 ⇝ m']]$. $[[n1 ⤳' m']]$ and $[[n2 ⇝* m']]$.
\end{lemma} \end{lemma}
\begin{proof} \begin{proof}
@ -676,7 +678,7 @@ All of these lemmas at last give us backward closure.
\begin{proof} \begin{proof}
By induction on the derivation of $[[m ⤳' n]]$. By induction on the derivation of $[[m ⤳' n]]$.
The cases correspond exactly to each of The cases correspond exactly to
\rref{sn-Force-Thunk,sn-App-Lam,sn-Let-Ret,sn-Case-Inl,sn-Case-Inr,sn-App-bwd,sn-Let-bwd}. \rref{sn-Force-Thunk,sn-App-Lam,sn-Let-Ret,sn-Case-Inl,sn-Case-Inr,sn-App-bwd,sn-Let-bwd}.
\end{proof} \end{proof}
@ -892,8 +894,9 @@ their typing judgements (2), the logical relation (2),
the small-step reduction relation (2), the small-step reduction relation (2),
and the mutually inductive definition of strongly neutral and normal terms and head reduction (4). and the mutually inductive definition of strongly neutral and normal terms and head reduction (4).
The tactic was used for every proof by mutual induction mentioned here. The tactic was used for every proof by mutual induction mentioned here.
Additionally, it was used twice for single induction Additionally, it was used thrice for single induction
(\ie all other motives are trivial): \rref{SN-Force-inv} and \nameref{cor:ext}. (\ie all other motives are trivial):
\rref{SN-Force-inv}, \nameref{cor:ext}, and \nameref{lem:closure}.
Because the mutual induction tactic is merely a tactic and not a top-level construct, Because the mutual induction tactic is merely a tactic and not a top-level construct,
some amount of manipulation is still required to massage the proof state some amount of manipulation is still required to massage the proof state

5
cbpv.ott
View File

@ -430,7 +430,7 @@ G ⊧ v : U B
G ⊧ force v : B G ⊧ force v : B
G, x : A ⊧ m : B G, x : A ⊧ m : B
----------------- :: Arr ----------------- :: Lam
G ⊧ λx. m : A → B G ⊧ λx. m : A → B
G ⊧ m : A → B G ⊧ m : A → B
@ -683,11 +683,10 @@ n ∈ sn
-------------- :: Let -------------- :: Let
let x m n ∈ sn let x m n ∈ sn
v ∈ sne
m ∈ sn m ∈ sn
n ∈ sn n ∈ sn
----------------------- :: Case ----------------------- :: Case
case v | y.m | z.n ∈ sn case x | y.m | z.n ∈ sn
defn defn
m ⤳' n :: :: sr :: 'sr_' m ⤳' n :: :: sr :: 'sr_'

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

Binary file not shown.

51
cbpv.tex
View File

@ -173,7 +173,7 @@ Because we're dealing with CBPV, values have no $\beta$ reductions,
so there's no need for head reduction of values as there are no heads. so there's no need for head reduction of values as there are no heads.
Furthermore, there is only one strongly neutral value, Furthermore, there is only one strongly neutral value,
so we inline the definition as a variable where needed, so we inline the definition as a variable where needed,
but also write it as $ \ottnt{v} \in \kw{SNe} $ for symmetry as appropriate. but also write it as \fbox{$ \ottnt{v} \in \kw{SNe} $} for symmetry as appropriate.
Otherwise, the remaining four judgements are defined mutually below. Otherwise, the remaining four judgements are defined mutually below.
\drules[SNe]{$ \ottnt{m} \in \kw{SNe} $}{strongly neutral computations}{Force,App,Let,Case} \drules[SNe]{$ \ottnt{m} \in \kw{SNe} $}{strongly neutral computations}{Force,App,Let,Case}
@ -288,7 +288,7 @@ but the alternate choices likely work as well.
or right injections whose values are in that of $\ottnt{A_{{\mathrm{2}}}}$. or right injections whose values are in that of $\ottnt{A_{{\mathrm{2}}}}$.
\item Computations in the interpretation of the $ \kw{F} \gap \ottnt{A} $ type \item Computations in the interpretation of the $ \kw{F} \gap \ottnt{A} $ type
reduce to either a neutral computation reduce to either a neutral computation
or a return whose value is in the interpretation of $\ottnt{A}$. or a returned value in the interpretation of $\ottnt{A}$.
\item Computations are in the interpretation of the function type $ \ottnt{A} \rightarrow \ottnt{B} $ \item Computations are in the interpretation of the function type $ \ottnt{A} \rightarrow \ottnt{B} $
if applying them to values in the interpretation of $\ottnt{A}$ if applying them to values in the interpretation of $\ottnt{A}$
yields computations in the interpretation of $\ottnt{B}$. yields computations in the interpretation of $\ottnt{B}$.
@ -301,7 +301,7 @@ Unfortunately, this is not well defined,
since the logical relation appears in a negative position since the logical relation appears in a negative position
(to the left of an implication) in the premise of \rref{LR'-Arr}. (to the left of an implication) in the premise of \rref{LR'-Arr}.
The alternate presentation can be interpreted as a function The alternate presentation can be interpreted as a function
match on the term and the type and returning the conjunction of its premises, matching on the term and the type and returning the conjunction of its premises,
but I wanted to use a mutually defined inductive definition. but I wanted to use a mutually defined inductive definition.
\begin{figure}[H] \begin{figure}[H]
@ -328,7 +328,7 @@ determinism, which states that the interpretation indeed behaves like a function
from types to sets of terms; from types to sets of terms;
and backward closure, which states that the interpretations of computation types and backward closure, which states that the interpretations of computation types
are backward closed under multi-step head reduction. are backward closed under multi-step head reduction.
The last property is why \rref{LR'-F-var} needs to include The last property is why \rref{LR-F} needs to include
computations that \emph{reduce to} strongly neutral terms or returns, computations that \emph{reduce to} strongly neutral terms or returns,
not merely ones that are such terms. not merely ones that are such terms.
@ -352,7 +352,7 @@ not merely ones that are such terms.
\begin{proof} \begin{proof}
By mutual induction on the first derivations of the logical relation, By mutual induction on the first derivations of the logical relation,
then by cases on the second derivations. then by cases on the second.
\end{proof} \end{proof}
\begin{lemma}[Backward closure] \label{lem:closure} \begin{lemma}[Backward closure] \label{lem:closure}
@ -361,7 +361,8 @@ not merely ones that are such terms.
\end{lemma} \end{lemma}
\begin{proof} \begin{proof}
By induction on the derivation of the logical relation. By induction on the derivation of the logical relation,
using \rref{SRs-Trans',SRs-App}.
\end{proof} \end{proof}
The final key property is adequacy, The final key property is adequacy,
@ -407,15 +408,14 @@ semantically well formed with respect to a context.
\begin{definition}[Semantic well-formedness of substitutions] \begin{definition}[Semantic well-formedness of substitutions]
A substitution $\sigma$ is well formed with respect to a context $\Gamma$, A substitution $\sigma$ is well formed with respect to a context $\Gamma$,
written $ \Gamma \vDash \sigma $, if for every $ \ottmv{x} : \ottnt{A} \in \Gamma $ and $ \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} \searrow \ottnt{P} $, written \fbox{$ \Gamma \vDash \sigma $}, if for every $ \ottmv{x} : \ottnt{A} \in \Gamma $ and $ \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} \searrow \ottnt{P} $,
we have $ \ottmv{x} [ \sigma ] \in \ottnt{P} $. we have $ \ottmv{x} [ \sigma ] \in \ottnt{P} $.
In short, the substitution maps variables in the context In short, the substitution maps variables in the context
to values in the interpretations of their types. to values in the interpretations of their types.
\end{definition} \end{definition}
These judgements can be built up inductively, These judgements can be built up inductively,
as demonstrated by the below admissible rules, as demonstrated by the below admissible rules.
which are proven by cases.
{\mprset{fraction={-~}{-~}{-}} {\mprset{fraction={-~}{-~}{-}}
\drules[S]{$ \Gamma \vDash \sigma $}{admissible semantic substitution well-formedness}{Nil,Cons} \drules[S]{$ \Gamma \vDash \sigma $}{admissible semantic substitution well-formedness}{Nil,Cons}
@ -427,10 +427,10 @@ using semantic well formedness of substitutions to handle the context.
\begin{definition}[Semantic typing] \begin{definition}[Semantic typing]
\begin{enumerate}[rightmargin=\leftmargin] \leavevmode \begin{enumerate}[rightmargin=\leftmargin] \leavevmode
\item $\ottnt{v}$ semantically has type $\ottnt{A}$ under context $\Gamma$, \item $\ottnt{v}$ semantically has type $\ottnt{A}$ under context $\Gamma$,
written $ \Gamma \vDash \ottnt{v} : \ottnt{A} $, if for every $\sigma$ such that $ \Gamma \vDash \sigma $, written \fbox{$ \Gamma \vDash \ottnt{v} : \ottnt{A} $}, if for every $\sigma$ such that $ \Gamma \vDash \sigma $,
there exists an interpretation $ \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} \searrow \ottnt{P} $ such that $ \ottnt{v} [ \sigma ] \in \ottnt{P} $. there exists an interpretation $ \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} \searrow \ottnt{P} $ such that $ \ottnt{v} [ \sigma ] \in \ottnt{P} $.
\item $\ottnt{m}$ semantically has type $\ottnt{B}$ under context $\Gamma$, \item $\ottnt{m}$ semantically has type $\ottnt{B}$ under context $\Gamma$,
written $ \Gamma \vDash \ottnt{m} : \ottnt{B} $, if for every $\sigma$ such that $ \Gamma \vDash \sigma $, written \fbox{$ \Gamma \vDash \ottnt{m} : \ottnt{B} $}, if for every $\sigma$ such that $ \Gamma \vDash \sigma $,
there exists an interpretation $ \mathopen{\llbracket} \ottnt{B} \mathclose{\rrbracket} \searrow \ottnt{P} $ such that $ \ottnt{m} [ \sigma ] \in \ottnt{P} $. there exists an interpretation $ \mathopen{\llbracket} \ottnt{B} \mathclose{\rrbracket} \searrow \ottnt{P} $ such that $ \ottnt{m} [ \sigma ] \in \ottnt{P} $.
\end{enumerate} \end{enumerate}
\end{definition} \end{definition}
@ -444,7 +444,7 @@ Normalization holds as a corollary.
{\mprset{fraction={-~}{-~}{-}} {\mprset{fraction={-~}{-~}{-}}
\drules[S]{$ \Gamma \vDash \ottnt{v} : \ottnt{A} $}{admissible semantic value typing}{Var,Unit,Inl,Inr,Thunk} \drules[S]{$ \Gamma \vDash \ottnt{v} : \ottnt{A} $}{admissible semantic value typing}{Var,Unit,Inl,Inr,Thunk}
\drules[S]{$ \Gamma \vDash \ottnt{m} : \ottnt{B} $}{admissible semantic computation typing}{Force,Arr,App,Ret,Let,Case} \drules[S]{$ \Gamma \vDash \ottnt{m} : \ottnt{B} $}{admissible semantic computation typing}{Force,Lam,App,Ret,Let,Case}
} }
\begin{proof} \begin{proof}
@ -509,16 +509,18 @@ with respect to a traditional presentation of strongly normal terms
based on full small-step reduction \fbox{$ \ottnt{v} \rightsquigarrow \ottnt{w} $}, \fbox{$ \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, I omit here the definitions of these reductions,
but they encompass all $\beta$-reduction rules and are congruent over all subterms, but they encompass all $\beta$-reduction rules and are congruent over all subterms,
including under binders. including under binders,
Traditional strongly normal terms, written $ \ottnt{v} \in \kw{sn} $, $ \ottnt{m} \in \kw{sn} $, with \fbox{$ \ottnt{v} \rightsquigarrow^* \ottnt{w} $}, \fbox{$ \ottnt{m} \rightsquigarrow^* \ottnt{n} $} denoting their reflexive, transitive closures.
Traditional strongly normal terms, defined below,
are accessibility relations with respect to small-step reduction. are accessibility relations with respect to small-step reduction.
Terms are inductively defined as strongly normal if they step to strongly normal terms, Terms are inductively defined as strongly normal if they step to strongly normal terms,
so terms which don't step are trivially normal. so terms which don't step are trivially normal.
This rules out looping and diverging terms, since they never stop stepping. This rules out diverging terms, since they never stop stepping.
% %
% \drules[sn]{$ \ottnt{v} \in \kw{sn} , \ottnt{m} \in \kw{sn} $}{strongly normalizing terms}{Val,Com} % \drules[sn]{$ \ottnt{v} \in \kw{sn} , \ottnt{m} \in \kw{sn} $}{strongly normal terms}{Val,Com}
\begin{mathpar} \begin{mathpar}
\fbox{$ \ottnt{v} \in \kw{sn} $} \quad \fbox{$ \ottnt{m} \in \kw{sn} $} \hfill \textit{strongly normalizing terms} \\ \fbox{$ \ottnt{v} \in \kw{sn} $} \quad \fbox{$ \ottnt{m} \in \kw{sn} $} \hfill \textit{strongly normal terms} \\
\drule[]{sn-Val} \drule[]{sn-Val}
\drule[]{sn-Com} \drule[]{sn-Com}
\end{mathpar} \end{mathpar}
@ -544,13 +546,13 @@ The strategy is to mirror the inductive characterization,
and define corresponding notions of neutral terms and head reduction, and define corresponding notions of neutral terms and head reduction,
with strongly neutral terms being those both neutral and strongly normal. with strongly neutral terms being those both neutral and strongly normal.
As before, variables are the only neutral value, As before, variables are the only neutral value,
but we write $ \ottnt{v} \in \kw{ne} $ to say that $\ottnt{v}$ is a variable for symmetry. but we write \fbox{$ \ottnt{v} \in \kw{ne} $} to say that $\ottnt{v}$ is a variable for symmetry.
\drules[sr]{$ \ottnt{m} \leadsto_{ \kw{sn} } \ottnt{n} $}{strong head reduction}{Thunk,Lam,Ret,Inl,Inr,App,Let} \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} \drules[ne]{$ \ottnt{m} \in \kw{ne} $}{neutral computations}{Force,App,Let,Case}
\begin{definition}[Strongly neutral computations] \begin{definition}[Strongly neutral computations]
A strongly neutral computation, written $ \ottnt{m} \in \kw{sne} $, A strongly neutral computation, written \fbox{$ \ottnt{m} \in \kw{sne} $},
is a computation that is both neutral and strongly normalizing, is a computation that is both neutral and strongly normalizing,
\ie $ \ottnt{m} \in \kw{ne} $ and $ \ottnt{m} \in \kw{sn} $. \ie $ \ottnt{m} \in \kw{ne} $ and $ \ottnt{m} \in \kw{sn} $.
\end{definition} \end{definition}
@ -616,7 +618,7 @@ we first need antisubstitution to be able to undo substitutions.
\Rref{sn-Force-Thunk} holds directly by induction on the premise; \Rref{sn-Force-Thunk} holds directly by induction on the premise;
the remaining proofs are more complex. the remaining proofs are more complex.
First, given the premise $ \ottnt{m} [ \ottmv{x} \mapsto \ottnt{v} ] \in \kw{sn} $ (or $ \ottnt{n} [ \ottmv{z} \mapsto \ottnt{v} ] $), First, given the premise $ \ottnt{m} [ \ottmv{x} \mapsto \ottnt{v} ] \in \kw{sn} $ (or $ \ottnt{n} [ \ottmv{z} \mapsto \ottnt{v} ] $),
use \nameref{lem:antisubst-sn} to obtain $ \ottnt{m} \in \kw{sn} $. use \nameref{lem:antisubst-sn} to obtain $ \ottnt{m} \in \kw{sn} $ (or $ \ottnt{n} \in \kw{sn} $).
Then proceed by double (or triple) induction on the derivations of Then proceed by double (or triple) induction on the derivations of
$ \ottnt{v} \in \kw{sn} $ and $ \ottnt{m} \in \kw{sn} $ (and $ \ottnt{n} \in \kw{sn} $ for the case rules). $ \ottnt{v} \in \kw{sn} $ and $ \ottnt{m} \in \kw{sn} $ (and $ \ottnt{n} \in \kw{sn} $ for the case rules).
Similarly to the admissible strongly normal rules, Similarly to the admissible strongly normal rules,
@ -635,7 +637,7 @@ of the structure of both reductions.
\begin{lemma}[Commutativity] \label{lem:commute} \begin{lemma}[Commutativity] \label{lem:commute}
If $ \ottnt{m} \rightsquigarrow \ottnt{n_{{\mathrm{1}}}} $ and $ \ottnt{m} \leadsto_{ \kw{sn} } \ottnt{n_{{\mathrm{2}}}} $, then either $\ottnt{n_{{\mathrm{1}}}} = \ottnt{n_{{\mathrm{2}}}}$, If $ \ottnt{m} \rightsquigarrow \ottnt{n_{{\mathrm{1}}}} $ and $ \ottnt{m} \leadsto_{ \kw{sn} } \ottnt{n_{{\mathrm{2}}}} $, then either $\ottnt{n_{{\mathrm{1}}}} = \ottnt{n_{{\mathrm{2}}}}$,
or there exists some $\ottnt{m'}$ such that or there exists some $\ottnt{m'}$ such that
$ \ottnt{n_{{\mathrm{1}}}} \leadsto_{ \kw{sn} } \ottnt{m'} $ and $ \ottnt{n_{{\mathrm{2}}}} \rightsquigarrow \ottnt{m'} $. $ \ottnt{n_{{\mathrm{1}}}} \leadsto_{ \kw{sn} } \ottnt{m'} $ and $ \ottnt{n_{{\mathrm{2}}}} \rightsquigarrow^* \ottnt{m'} $.
\end{lemma} \end{lemma}
\begin{proof} \begin{proof}
@ -676,7 +678,7 @@ All of these lemmas at last give us backward closure.
\begin{proof} \begin{proof}
By induction on the derivation of $ \ottnt{m} \leadsto_{ \kw{sn} } \ottnt{n} $. By induction on the derivation of $ \ottnt{m} \leadsto_{ \kw{sn} } \ottnt{n} $.
The cases correspond exactly to each of The cases correspond exactly to
\rref{sn-Force-Thunk,sn-App-Lam,sn-Let-Ret,sn-Case-Inl,sn-Case-Inr,sn-App-bwd,sn-Let-bwd}. \rref{sn-Force-Thunk,sn-App-Lam,sn-Let-Ret,sn-Case-Inl,sn-Case-Inr,sn-App-bwd,sn-Let-bwd}.
\end{proof} \end{proof}
@ -892,8 +894,9 @@ their typing judgements (2), the logical relation (2),
the small-step reduction relation (2), the small-step reduction relation (2),
and the mutually inductive definition of strongly neutral and normal terms and head reduction (4). and the mutually inductive definition of strongly neutral and normal terms and head reduction (4).
The tactic was used for every proof by mutual induction mentioned here. The tactic was used for every proof by mutual induction mentioned here.
Additionally, it was used twice for single induction Additionally, it was used thrice for single induction
(\ie all other motives are trivial): \rref{SN-Force-inv} and \nameref{cor:ext}. (\ie all other motives are trivial):
\rref{SN-Force-inv}, \nameref{cor:ext}, and \nameref{lem:closure}.
Because the mutual induction tactic is merely a tactic and not a top-level construct, Because the mutual induction tactic is merely a tactic and not a top-level construct,
some amount of manipulation is still required to massage the proof state some amount of manipulation is still required to massage the proof state

9
rules.tex
View File

@ -627,11 +627,11 @@
}} }}
\newcommand{\ottdruleSXXArr}[1]{\ottdrule[#1]{% \newcommand{\ottdruleSXXLam}[1]{\ottdrule[#1]{%
\ottpremise{ \Gamma , \ottmv{x} \mathbin{:} \ottnt{A} \vDash \ottnt{m} : \ottnt{B} }% \ottpremise{ \Gamma , \ottmv{x} \mathbin{:} \ottnt{A} \vDash \ottnt{m} : \ottnt{B} }%
}{ }{
\Gamma \vDash \lambda \ottmv{x} \mathpunct{.} \ottnt{m} : \ottnt{A} \rightarrow \ottnt{B} }{% \Gamma \vDash \lambda \ottmv{x} \mathpunct{.} \ottnt{m} : \ottnt{A} \rightarrow \ottnt{B} }{%
{\ottdrulename{S\_Arr}}{}% {\ottdrulename{S\_Lam}}{}%
}} }}
@ -672,7 +672,7 @@
\newcommand{\ottdefnSemCom}[1]{\begin{ottdefnblock}[#1]{$ \Gamma \vDash \ottnt{m} : \ottnt{B} $}{} \newcommand{\ottdefnSemCom}[1]{\begin{ottdefnblock}[#1]{$ \Gamma \vDash \ottnt{m} : \ottnt{B} $}{}
\ottusedrule{\ottdruleSXXForce{}} \ottusedrule{\ottdruleSXXForce{}}
\ottusedrule{\ottdruleSXXArr{}} \ottusedrule{\ottdruleSXXLam{}}
\ottusedrule{\ottdruleSXXApp{}} \ottusedrule{\ottdruleSXXApp{}}
\ottusedrule{\ottdruleSXXRet{}} \ottusedrule{\ottdruleSXXRet{}}
\ottusedrule{\ottdruleSXXLet{}} \ottusedrule{\ottdruleSXXLet{}}
@ -1053,11 +1053,10 @@
\newcommand{\ottdrulesnXXCase}[1]{\ottdrule[#1]{% \newcommand{\ottdrulesnXXCase}[1]{\ottdrule[#1]{%
\ottpremise{ \ottnt{v} \in \kw{sne} }%
\ottpremise{ \ottnt{m} \in \kw{sn} }% \ottpremise{ \ottnt{m} \in \kw{sn} }%
\ottpremise{ \ottnt{n} \in \kw{sn} }% \ottpremise{ \ottnt{n} \in \kw{sn} }%
}{ }{
\kw{case} \gap \ottnt{v} \gap \kw{of} \gap \lbrace \kw{inl} \gap \ottmv{y} \Rightarrow \ottnt{m} \mathrel{;} \kw{inr} \gap \ottmv{z} \Rightarrow \ottnt{n} \rbrace \in \kw{sn} }{% \kw{case} \gap \ottmv{x} \gap \kw{of} \gap \lbrace \kw{inl} \gap \ottmv{y} \Rightarrow \ottnt{m} \mathrel{;} \kw{inr} \gap \ottmv{z} \Rightarrow \ottnt{n} \rbrace \in \kw{sn} }{%
{\ottdrulename{sn\_Case}}{}% {\ottdrulename{sn\_Case}}{}%
}} }}