Commit bc17dafe authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Typing in english

parent b377552a
\section{Typage}
\section{Typing}
\subsection*{Formation des contextes}
\subsection*{Context formation}
\begin{center}
\begin{tabular}{rcl}
\AxiomC{$\phantom{\Gamma\vdash A}$}
\UnaryInfC{$[]$ bien formé}
\UnaryInfC{$[]$ well-formed}
\DisplayProof&&
\AxiomC{$\Gamma\vdash A:s$}
\RightLabel{$\sys{x\notin\support(\Gamma)}{s\in\Sort}$}
\UnaryInfC{$\Gamma,x:A$ bien formé}
\UnaryInfC{$\Gamma,x:A$ well-formed}
\DisplayProof
\end{tabular}
\end{center}
\subsection*{Axiomes}
\subsection*{Axioms}
\begin{center}
\begin{tabular}{rcl}
\AxiomC{$\Gamma$ bien formé}
\AxiomC{$\Gamma$ well-formed}
\UnaryInfC{$\Gamma\vdash \Type:\Kind$}
\DisplayProof&&
\AxiomC{$\Gamma$ bien formé}
\AxiomC{$\Gamma$ well-formed}
\RightLabel{$x:A\in\Gamma$}
\UnaryInfC{$\Gamma\vdash x:A$}
\DisplayProof
......@@ -30,11 +30,11 @@
\end{center}
\todo{
On peut remplacer ce prédicat bien formé par une règle d'affaiblissement (cf FSCD).
Quel impact ce changement a-t-il ?
We can replace the ``well-formed'' predicate by a weakening (cf. FSCD).
Does it change anything?
}
\subsection*{Produit}
\subsection*{Product}
\begin{prooftree}
\AxiomC{$\Gamma\vdash A:\Type$}
......@@ -60,7 +60,7 @@ Quel impact ce changement a-t-il ?
\BinaryInfC{$\Gamma\vdash t\,u:\subst{B}{x}{u}$}
\end{prooftree}
\subsection*{Symbole de la signature}
\subsection*{Signature symbol}
\begin{prooftree}
\def\defaultHypSeparation{\hskip 0em}
......@@ -68,7 +68,7 @@ Quel impact ce changement a-t-il ?
\UnaryInfC{$\Gamma\vdash f:\tau(f)$}
\end{prooftree}
\todo{Si l'on a l'affaiblissement, $\G$ peut être supprimé dans cette règle.}
\todo{If we have the weakening, $\G$ can be suppressed in this rule.}
\subsection*{Conversion}
......@@ -80,72 +80,80 @@ Quel impact ce changement a-t-il ?
\end{prooftree}
\begin{cond}{SubjectReduction}(Subject reduction).
On suppose que les règles préservent le typage, \cad que
pour tous termes $t$ et $t'$ tels que $t\rew t'$,
pour tout $T$,
pour tout contexte $\Gamma$ tel que $\Gamma\vdash t:T$,
on a $\Gamma\vdash t':T$.
We suppose that the rules are type preserving in the sense that :
for all terms $t$ and $t'$ such that $t\rew t'$,
for all $T$,
for all context $\Gamma$ such that $\Gamma\vdash t:T$,
then $\Gamma\vdash t':T$.
\end{cond}
\begin{rmq}
Subject reduction implique que pour toute règle $f\,\bar l\rul r$,
Subject reduction implies that for any rule $f\,\bar l\rul r$,
$\FreeVar(r)\subseteq\FreeVar(f\,\bar l)$.
\end{rmq}
\begin{defi}[Termes (version stratifiée)]
On donne les 3 grammaires suivantes :
\begin{defi}[Terms (stratified version)]
We give the 3 following grammars:
\begin{center}
\begin{tabular}{rrlr}
kinds & $K$ & $::=\Type\mid\Pi(x:U). K$\\
familles & $T,U$ & $::=\lambda (x:U).\,T\mid\Pi(x:U).T\mid T\,t\mid F$&$F\in\FTyp$\\
objets & $t,u$ & $::=x\mid\lambda (x:T).\,t\mid t\,u\mid f$&$f\in\FObj$, $x\in\Var$\\
families & $T,U$ & $::=\lambda (x:U).\,T\mid\Pi(x:U).T\mid T\,t\mid F$&$F\in\FTyp$\\
objects & $t,u$ & $::=x\mid\lambda (x:T).\,t\mid t\,u\mid f$&$f\in\FObj$, $x\in\Var$\\
\end{tabular}
\end{center}
Un \emph{terme} est $\Kind$, une \emph{kind}, une \emph{famille} ou un \emph{objet}.
A \emph{term} is $\Kind$, a \emph{kind}, a \emph{family} or an \emph{object}.
\end{defi}
\todo{Rajouter un item pour les types qui sont des familles d'arité 0 et mettre cela au bon endroit (mais ça fait une 3e grammaire) ?}
\todo{
Add a grammar for types which are families of arity 0?
But it would be a 4th grammar.
Does it offer any benefit?
}
\begin{nots}
$\mbb{K}$ désigne l'ensemble des kinds, $\mbb{F}$ l'ensemble des familles et $\mbb{O}$ l'ensemble des objets.
$\mbb{K}$ is the set of kinds,
$\mbb{F}$ the set of familles
and $\mbb{O}$ the set of objects.
De plus, $\Terms$ désigne l'ensemble de tous les termes.
Furthermore, $\Terms$ designates the set of all terms.
\end{nots}
\begin{cond}{ConsistTypSort}(Cohérence typage sortage)
$\tau$ associe :
\begin{cond}{ConsistTypSort}(Consistency between typing and sorting)
$\tau$ associates :
\begin{itemize}
\item une kind à chaque symbole de $\FTyp$ ;
\item une famille à chaque symbole de $\FObj$.
\item a kind to every symbol of $\FTyp$ ;
\item a family to every symbol of $\FObj$.
\end{itemize}
\end{cond}
\begin{defi}[Forme normale]
Soit $t\in\SN$, on note $t\Downarrow$ sa forme normale,
qui est le terme $u$ tel que $t\reww u$ et il n'existe pas de $v$ tel que $u\rew v$.
\begin{defi}[Normal form]
For $t\in\SN$, we denote by $t\Downarrow$ its normal form,
which is the term $u$ such that $t\reww u$ and there exist no $v$ such that $u\rew v$.
\end{defi}
\begin{rmq}
Grâce à l'hypothèse de confluence locale et lemme de Newman, la forme si elle existe est unique.
Thanks to the local confluence hypothesis and Newman's lemma, the normal form is unique and well-defined.
\end{rmq}
\begin{propo}[Stratification]
\label{lem-Stratification}
Si $\Delta\vdash t:A$, alors on est dans l'un des cas suivants :
\begin{propo}[Stratification lemma]
If $\D\vdash t:A$ then we are in one of the following cases:
\begin{itemize}
\item $t$ est un objet, $A$ une famille et $\D\vdash A:\Type$,
\item $t$ est une famille, $A$ une kind et $\D\vdash A:\Kind$,
\item $t$ est une kind et $A=\Kind$.
\item $t$ is an object, $A$ a family and $\D\vdash A:\Type$,
\item $t$ is an family, $A$ a kind and $\D\vdash A:\Kind$,
\item $t$ is an kind and $A=\Kind$.
\end{itemize}
\end{propo}
\begin{proof}
C'est le lemme 2.6.10 de la thèse de Ronan.
C'est aussi dans la thèse de Frédéric (numéro à chercher).
This is lemma 2.6.10 of Ronan's thesis.
\end{proof}
\begin{defi}[Transition bien typée]
Soit $\G$ et $\D$ deux contextes.
$\sg$ est \emph{une transition bien typée} entre $\G$ et $\D$ (notée $\sg:\G\rightsquigarrow\D$)
si pour tous $t,T$, $\G\vdash t:T$ implique $\D\vdash t\sg:T\sg$.
\begin{defi}[Well-typed transition]
Let $\G$ and $\D$ be two contexts.
$\sg$ is a \emph{well-typed transition} between $\G$ and $\D$ (denoted $\sg:\G\rightsquigarrow\D$)
if for all $t,T$, $\G\vdash t:T$ implies $\D\vdash t\sg:T\sg$.
\end{defi}
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