Commit 1fa6a3ee by Giuseppe Castagna

### rewording

parent 972605f5
 ... ... @@ -619,50 +619,17 @@ That is, $\tyof{e}{\Gamma}=\ts$ if and only if $\Gamma\vdashA e:\ts$ is provable We start by defining the algorithm for each single occurrence, that is for the deduction of $\pvdash \Gamma e t \varpi:t'$. This is obtained by defining two mutually recursive functions $\constrf$ and $\env{}{}$: \newlength{\sk} \setlength{\sk}{-1.3pt} \setlength{\sk}{-1.5pt} \begin{eqnarray} \constr\epsilon{\Gamma,e,t} & = & t\$\sk]\label{uno} \constr{\varpi.0}{\Gamma,e,t} & = & \neg(\arrow{\env {\Gamma,e,t}{(\varpi.1)}}{\neg \env {\Gamma,e,t} (\varpi)})\\[\sk]\label{due} \constr{\varpi.1}{\Gamma,e,t} & = & \worra{\tsrep {\tyof{\occ e{\varpi.0}}\Gamma}}{\env {\Gamma,e,t} (\varpi)}\\[\sk]\label{tre} \constr{\varpi.l}{\Gamma,e,t} & = & \bpl{\env {\Gamma,e,t} (\varpi)}\\[\sk]\label{quattro} \constr{\varpi.r}{\Gamma,e,t} & = & \bpr{\env {\Gamma,e,t} (\varpi)}\\[\sk]\label{cinque} \constr{\varpi.f}{\Gamma,e,t} & = & \pair{\env {\Gamma,e,t} (\varpi)}\Any\\[\sk]\label{sei} \constr{\varpi.s}{\Gamma,e,t} & = & \pair\Any{\env {\Gamma,e,t} (\varpi)}\\[1.5mm]\label{sette} \constr\epsilon{\Gamma,e,t} & = & t\label{uno}\\[\sk] \constr{\varpi.0}{\Gamma,e,t} & = & \neg(\arrow{\env {\Gamma,e,t}{(\varpi.1)}}{\neg \env {\Gamma,e,t} (\varpi)})\label{due}\\[\sk] \constr{\varpi.1}{\Gamma,e,t} & = & \worra{\tsrep {\tyof{\occ e{\varpi.0}}\Gamma}}{\env {\Gamma,e,t} (\varpi)}\label{tre}\\[\sk] \constr{\varpi.l}{\Gamma,e,t} & = & \bpl{\env {\Gamma,e,t} (\varpi)}\label{quattro}\\[\sk] \constr{\varpi.r}{\Gamma,e,t} & = & \bpr{\env {\Gamma,e,t} (\varpi)}\label{cinque}\\[\sk] \constr{\varpi.f}{\Gamma,e,t} & = & \pair{\env {\Gamma,e,t} (\varpi)}\Any\label{sei}\\[\sk] \constr{\varpi.s}{\Gamma,e,t} & = & \pair\Any{\env {\Gamma,e,t} (\varpi)}\label{sette}\\[1.5mm] \env {\Gamma,e,t} (\varpi) & = & \constr \varpi {\Gamma,e,t} \land \tsrep {\tyof {\occ e \varpi} \Gamma}\label{otto} \end{eqnarray} %% \[ %% \begin{array}{lcl} %% \typep+\epsilon{\Gamma,e,t} & = & t\\ %% \typep-\epsilon{\Gamma,e,t} & = & \neg t\\ %% \typep{p}{\varpi.0}{\Gamma,e,t} & = & \neg(\arrow{\Gp p{\Gamma,e,t}{(\varpi.1)}}{\neg \Gp p {\Gamma,e,t} (\varpi)})\\ %% \typep{p}{\varpi.1}{\Gamma,e,t} & = & \worra{\tsrep {\tyof{\occ e{\varpi.0}}\Gamma}}{\Gp p {\Gamma,e,t} (\varpi)}\\ %% \typep{p}{\varpi.l}{\Gamma,e,t} & = & \bpl{\Gp p {\Gamma,e,t} (\varpi)}\\ %% \typep{p}{\varpi.r}{\Gamma,e,t} & = & \bpr{\Gp p {\Gamma,e,t} (\varpi)}\\ %% \typep{p}{\varpi.f}{\Gamma,e,t} & = & \pair{\Gp p {\Gamma,e,t} (\varpi)}\Any\\ %% \typep{p}{\varpi.s}{\Gamma,e,t} & = & \pair\Any{\Gp p {\Gamma,e,t} (\varpi)}\\ \\ %% \Gp p {\Gamma,e,t} (\varpi) & = & \typep p \varpi {\Gamma,e,t} \land \tsrep {\tyof {\occ e \varpi} \Gamma}\\ %% %\underbrace{\land \tyof {\occ e \varpi} {\Gamma\setminus\{\occ e \varpi\}}}_{\text{if \occ e \varpi is not a variable}}}\\ %% \end{array} %%$ %% \begin{align*} %% &(\RefineStep p {e,t} (\Gamma))(e') = %% \left\{\begin{array}{ll} %% %\tyof {e'} \Gamma \tsand %% \bigwedge_{\{\varpi \alt \occ e \varpi \equiv e'\}} %% \Gp p {\Gamma,e,t} (\varpi) & \text{if } \exists \varpi.\ \occ e \varpi \equiv e' \\ %% \Gamma(e') & \text{otherwise, if } e' \in \dom \Gamma\\ %% \text{undefined} & \text{otherwise} %% \end{array}\right.\\ %% &\Refine p {e,t} \Gamma=\fixpoint_\Gamma (\RefineStep p {e,t})\qquad \text{(for the order $\leq$ on environments, defined in the proofs section)} %% \end{align*} All the functions above are defined if and only if the initial path $\varpi$ is valid for $e$ (i.e., $\occ e{\varpi}$ is defined) and $e$ is well-typed (which implies that all $\tyof {\occ e{\varpi}} \Gamma$ ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!