Commit 2ec5e187 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

Merge branch 'master' of gitlab.math.univ-paris-diderot.fr:beppe/occurrence-typing

parents a9f63583 605aa696
......@@ -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
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{}{}$:
\newlength{\sk}
\setlength{\sk}{-1.3pt}
......@@ -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
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
of the operators $\worra{}{}$ and $\boldsymbol{\pi}_i$ in
the definition of $\constrf$.
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.
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
......@@ -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 }
{ \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]
{ \Gamma\setminus\{e\} \vdashA e : \ts }
{ \Gamma \vdashA e: \Gamma(e) \tsand \ts }
{ e\in\dom\Gamma}
{ e\in\dom\Gamma \text{ and } e \text{ not a variable}}
\qquad
\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