Commit e54f9aac authored by Antonio Bucciarelli's avatar Antonio Bucciarelli
Browse files

se

parent cafa32fd
......@@ -459,8 +459,7 @@ Let $M=\lambda x.(x \oplus \id)$. The following (incomplete) derivation can be b
Note that $\multiset{M} \Redo \multiset{\two \id , \two \lambda x.\id}$; while $\der \id:\dist{\multiset{\dist{\At}} \arrow \At}$, it is necessary to have weakening in order to built a derivation proving $\der \lambda x. \id: \dist{\multiset{\dist{\At}} \arrow (\multiset{\dist{\Bt}} \arrow \Bt) }$.
\end{example}
\begin{enumerate}
\item \antonio{
\antonio{
\begin{itemize}
\item $[\lambda x. (x\oplus \id)]\Red[\frac 1 2 \lambda x. x, \frac 1 2 \lambda x. \id]$,
\item $\der \lambda x.x:\dist{\multiset{\dist{\At}} \arrow \At}$,
......@@ -473,7 +472,7 @@ but this cannot be the case since the type of $\lambda x.(x\oplus \id)$ must ha
$\dist{\two (\multiset{\dist{\At}} \arrow \At, \two (\multiset{\dist{\At}} \arrow \multiset{\dist{\Bt}} \arrow \Bt}$ (see the previous example)
}
\item \simona{
\simona{
Reading with attention the text of the subject expansion:
\begin{itemize}
\item $[\lambda x. (x\oplus \id)]\Red[\frac 1 2 \lambda x. x, \frac 1 2 \lambda x. \id]$,
......@@ -488,18 +487,18 @@ $\lambda x. (x \oplus I) : \two\dist{\multiset{}\arrow \dist{\multiset{\dist{\At
We are NOT obliged to consider all together all the types of the reduct, but just a subset of them. In fact the rule $\oplus$ allows to type just one component of a sum.
In order to make it more clear we could modify the text as I will write after the old one.
}
\item \antonio{
\begin{itemize}
\item $[\lambda x. (x\oplus \id)]\Red[\lambda x. x\oplus \lambda x. \id]$,
\item $\der \lambda x. x\oplus \lambda x. \id:\dist{\frac 1 2 \multiset{\dist{\At}} \arrow \At, \frac 1 2 \multiset{}\arrow \dist{\multiset{\dist{\At}} \arrow \At}}$
\end{itemize}
Hence, by subject expansion (new formulation), it should exist a context $\Gamma$ (greater than the empty context, hence whatsoever) such that
$\Gamma \der \lambda x.(x\oplus \id):\dist{\frac 1 2 \multiset{\dist{\At}} \arrow \At, \frac 1 2 \multiset{}\arrow \dist{\multiset{\dist{\At}} \arrow \At}}$,
but this cannot be the case since the type of $\lambda x.(x\oplus \id)$ must have the shape
$\dist{\two (\multiset{\dist{\At}} \arrow \At, \two (\multiset{\dist{\At}} \arrow \multiset{\dist{\Bt}} \arrow \Bt}$ (see the previous example)
}
%\antonio{
%\begin{itemize}
%\item $[\lambda x. (x\oplus \id)]\Red[\lambda x. x\oplus \lambda x. \id]$,
%\item $\der \lambda x. x\oplus \lambda x. \id:\dist{\frac 1 2 \multiset{\dist{\At}} \arrow \At, \frac 1 2 \multiset{}\arrow \dist{\multiset{\dist{\At}} \arrow \At}}$
%\end{itemize}
%Hence, by subject expansion (new formulation), it should exist a context $\Gamma$ (greater than the empty context, hence whatsoever) such that
%$\Gamma \der \lambda x.(x\oplus \id):\dist{\frac 1 2 \multiset{\dist{\At}} \arrow \At, \frac 1 2 \multiset{}\arrow \dist{\multiset{\dist{\At}} \arrow \At}}$,
%but this cannot be the case since the type of $\lambda x.(x\oplus \id)$ must have the shape
%$\dist{\two (\multiset{\dist{\At}} \arrow \At, \two (\multiset{\dist{\At}} \arrow \multiset{\dist{\Bt}} \arrow \Bt}$ (see the previous example)
%}
\item \simona{
\simona{
Applying the subject expansion property it turns out :
\begin{itemize}
\item $[\lambda x. (x\oplus \id)]\Red[\two \lambda x. x, \two \lambda x. \id]$,
......@@ -529,7 +528,7 @@ In fact:
and similarly for the other typing and the other term.
The idea is that we can consider the multiset of the reduct collecting a submultiset of them (so, simplifying the property, one by one).
}
\end{enumerate}
In fact the weakening rule is derivable, as the following property formalizes.
\begin{property} \label{prop:weak}
......@@ -636,12 +635,12 @@ By induction on the length of the reduction, see the Appendix.
\antonio{\begin{lemma}[Subject Expansion]\label{lem:subexp}
$\multiset{M} \Red^* \multiset{p_iN_i \mid \iI}$, $k\in I$ and $\Gamma \der
N_k:\dist{q_j\At_j}_{\jJ}$
imply $\forall l\in J$ $\Delta \der
M: p_kq_l\At_l$, for some $\Delta$, $\Gamma \leq \Delta$.
\end{lemma}}
%\antonio{\begin{lemma}[Subject Expansion]\label{lem:subexp}
% $\multiset{M} \Red^* \multiset{p_iN_i \mid \iI}$, $k\in I$ and $\Gamma \der
% N_k:\dist{q_j\At_j}_{\jJ}$
%imply $\forall l\in J$ $\Delta \der
% M: p_kq_l\At_l$, for some $\Delta$, $\Gamma \leq \Delta$.
%\end{lemma}}
In \cite{fscd} it has been proved that the system \Sis\ characterises $\hnf$s:
\begin{theorem}\label{th:char}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment