From 423d76d3069d76aca195b39213d488553f8535fe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bart=C5=82omiej=20Kr=C3=B3likowski?= Date: Wed, 17 Jan 2024 02:44:14 +0100 Subject: [PATCH 1/2] added an explanaiton for biorthogonal closure in section 5.2. --- chapter/biorthogonality.tex | 51 +++++++++++++++++++++++++++++++------ 1 file changed, 43 insertions(+), 8 deletions(-) diff --git a/chapter/biorthogonality.tex b/chapter/biorthogonality.tex index 5853cd7..121096e 100644 --- a/chapter/biorthogonality.tex +++ b/chapter/biorthogonality.tex @@ -134,15 +134,47 @@ \section{Type System for \texttt{call/cc}} \section{Biorthogonal Closure} \label{sec:biorthogonal-closure} +Now we would like to prove that our type system is safe and that every typable +term terminates. In previous chapter we have learned a method of logical relations +and seen that they provide a clearer and more scalable approach. It is natural +to ask whether it is possible to use that approach in our current situation. +The answer is yes, if only we modify the expression closure operator. The problem +is, it does not make sense to speak of reductions of arbitrary expressions in our +system. The reduction relation is defined only for whole programs. Therefore, to +be able to express properties of expressions in the language of reductions we need +to transform them to programs. We will notice the natural solution if we recall +our observation from the previous section: evaluation contexts are exactly those +kind of ”functions” that transform expressions into programs. + +Actually, because the properties we want to observe in our expressions are about +programs, we will extract their statements into a new relation $\Obs$ on programs +that, in the proof of safety, will equal $\rawSafe$ and in the proof of +termination will equal $\{ p \mid \exists v. p \longrightarrow^* v\}$. Most of +the time we will treat $\Obs$ as a parameter, though, assuming only that if +$p \longrightarrow p'$ and $p' \in \Obs$ then $p \in \Obs$. + +We already know that the $\mathcal{E}$ operator should select those expressions $e$, +for which $E[e] \in \Obs$. The question is, where to take $E$ from. On one hand, +it should not be too specific, so that properties of $E[e]$ were reflecting +properties of $e$, but on the other hand we should allow only contexts that +create correct (i.e. safe/terminating) programs. The solution is to introduce +another closure operator, this time for contexts: $\mathcal{K}$. A context $E$ +will be in a closure of relation $R$ if it behaves well on values $v$ from $R$, +that is if $E[v] \in \Obs$. + +Our new set of operators is following +\begin{alignat*}{2} + \mathcal{E}R &= \{ e \mid \forall E \in \mathcal{K} R. E[e] \in \Obs \} \\ + \mathcal{K}R &= \{ E \mid \forall v \in R. E[v] \in \Obs \} +\end{alignat*} +and denotation of types is standard +\begin{alignat*}{2} + \Denot{\tau_1 \to \tau_2} &= \{ v \mid \forall v' \in \Denot{\tau_1}. v\_v' \in \mathcal{E}\Denot{\tau_2} \} \\ + \Denot{\bot} &= \varnothing +\end{alignat*} -$\mathcal{E}R = \{ e \mid \forall E \in \mathcal{K} R. E[e] \in \Obs \}$ - -$\mathcal{K}R = \{ E \mid \forall v \in R. E[v] \in \Obs \}$ - -Type safety: $\Obs = \rawSafe$ - -Termination: $\Obs = \{ p \mid \exists v. p \longrightarrow^* v\}$ - +Now we just need to apply standard techniques to make the proof, so let us just +look at selected proofs of compatibility lemmas. \begin{lemma} If $e_1 \in \mathcal{E}\Denot{\tau_2 \to \tau_1}$ and $e_2 \in \mathcal{E}\Denot{\tau_2}$ @@ -163,6 +195,8 @@ \section{Biorthogonal Closure} and assumptions over $v_2$ and $E$. \end{proof} + + \begin{lemma}\label{lem:biortho_obs_red}. If $p \longrightarrow p'$ and $p' \in \Obs$, then $p \in \Obs.$ \end{lemma} @@ -189,3 +223,4 @@ \section{Biorthogonal Closure} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Further Reading} + From 32bd5013dfeb05cc00fdfd4da789327cb23a2966 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bart=C5=82omiej=20Kr=C3=B3likowski?= Date: Wed, 17 Jan 2024 02:56:50 +0100 Subject: [PATCH 2/2] more explanations in 5.2. --- chapter/biorthogonality.tex | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/chapter/biorthogonality.tex b/chapter/biorthogonality.tex index 121096e..e71d668 100644 --- a/chapter/biorthogonality.tex +++ b/chapter/biorthogonality.tex @@ -194,8 +194,11 @@ \section{Biorthogonal Closure} by the fact that $v_1\in\Denot{\tau_2\to\tau_1}$ and assumptions over $v_2$ and $E$. \end{proof} - - +here we have taken advantage of the fact that we defined contexts with +plug operation "$[ \quad ]$" as inside-out zippers: we can perform a step +forwards or backwards, getting bigger or smaller contexts with expressions +plugged to them like in $E[e_1\;e_2] = (E\;e_2)[e_1]$ or +$(E\;e_2)[v_1] = E[v_1\;e_2]$. \begin{lemma}\label{lem:biortho_obs_red}. If $p \longrightarrow p'$ and $p' \in \Obs$, then $p \in \Obs.$