Commit 605aa696 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

new rule VarA

parent 26891d94
...@@ -631,6 +631,9 @@ takes as input $\Gamma$, $e$, and $t$, and returns an environment that ...@@ -631,6 +631,9 @@ takes as input $\Gamma$, $e$, and $t$, and returns an environment that
extends $\Gamma$ with hypotheses on the occurrences of $e$ that are extends $\Gamma$ with hypotheses on the occurrences of $e$ that are
the most general that can be deduced by assuming that $e\in t$ succeeds. the most general that can be deduced by assuming that $e\in t$ succeeds.
The notation $\tyof{e}{\Gamma}$ denotes the type that can be deduced for the occurence $e$ under the type environment $\Gamma$ in the algorithmic type system given in Section~\ref{sec:algorules}.
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{}{}$: 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} \newlength{\sk}
\setlength{\sk}{-1.3pt} \setlength{\sk}{-1.3pt}
...@@ -677,7 +680,8 @@ We start by defining the algorithm for each single occurrence, that is for the d ...@@ -677,7 +680,8 @@ We start by defining the algorithm for each single occurrence, that is for the d
All the functions above are defined if and only if so all their subexpressions are (i.e., $\occ e{\varpi.i}$ must be defined). 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 (so that all $\tyof {\occ e{\varpi}} \Gamma$ encountered are defined).
Each case of the definition of the $\constrf$ function corresponds to the Each case of the definition of the $\constrf$ function corresponds to the
application of a logical rule (\emph{cf.} Footnote~\ref{fo:rules}) in application of a logical rule (\emph{cf.} Footnote~\ref{fo:rules}) in
...@@ -700,9 +704,6 @@ remaining structural rule, \Rule{Psubs}, is accounted for by the use ...@@ -700,9 +704,6 @@ remaining structural rule, \Rule{Psubs}, is accounted for by the use
of the operators $\worra{}{}$ and $\boldsymbol{\pi}_i$ in of the operators $\worra{}{}$ and $\boldsymbol{\pi}_i$ in
the definition of $\constr{}{}$. the definition of $\constr{}{}$.
The notation $\tyof{e}{\Gamma}$ denotes the type that can be deduced for the occurence $e$ under the type environment $\Gamma$ in the algorithmic type system given in Section~\ref{sec:algorules}.
That is, $\tyof{e}{\Gamma}=\ts$ if and only if $\Gamma\vdashA e:\ts$ is provable.
\footnote{Note that the definition is well-founded. \footnote{Note that the definition is well-founded.
This can be seen by analyzing the rule \Rule{Case\Aa}: the definition of $\Refine {e,t} \Gamma$ and $\Refine {e,\neg t} \Gamma$ use This can be seen by analyzing the rule \Rule{Case\Aa}: the definition of $\Refine {e,t} \Gamma$ and $\Refine {e,\neg t} \Gamma$ use
$\tyof{\occ e{\varpi}}\Gamma$, and this is defined for all $\varpi$ since the first premisses of \Rule{Case\Aa} states that $\tyof{\occ e{\varpi}}\Gamma$, and this is defined for all $\varpi$ since the first premisses of \Rule{Case\Aa} states that
...@@ -791,11 +792,16 @@ We now have all notions needed for our typing algorithm, which is defined by th ...@@ -791,11 +792,16 @@ We now have all notions needed for our typing algorithm, which is defined by th
{ } { }
{ \Gamma, (e:\Empty) \vdashA e': \Empty } { \Gamma, (e:\Empty) \vdashA e': \Empty }
{ \begin{array}{c}\text{\tiny with priority over}\\[-1.8mm]\text{\tiny all the other rules}\end{array}} { \begin{array}{c}\text{\tiny with priority over}\\[-1.8mm]\text{\tiny all the other rules}\end{array}}
\qquad
\Infer[Var\Aa]
{ }
{ \Gamma \vdashA x: \Gamma(x) }
{ x\in\dom\Gamma}
\\ \\
\Infer[Env\Aa] \Infer[Env\Aa]
{ \Gamma\setminus\{e\} \vdashA e : \ts } { \Gamma\setminus\{e\} \vdashA e : \ts }
{ \Gamma \vdashA e: \Gamma(e) \tsand \ts } { \Gamma \vdashA e: \Gamma(e) \tsand \ts }
{ e\in\dom\Gamma} { e\in\dom\Gamma \text{ and } e \text{ not a variable}}
\qquad \qquad
\Infer[Const\Aa] \Infer[Const\Aa]
{ } { }
......
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