Commit b377552a authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Syntax in english

parent d5d992b6
\section{Syntaxe}
\section{Syntax}
\begin{defi}[Sortes]
On considère $\Sort=\ens{\Type,\Kind}$.
\begin{defi}[Sort]
We consider the set of \emph{sorts} $\Sort=\ens{\Type,\Kind}$.
\end{defi}
\begin{defi}[Variables]
Soit $\Var$ un ensemble infini de \emph{variables}.
Let $\Var$ be an infinite set of \emph{variables}.
\end{defi}
\begin{defi}[Signature]
Soit $\Func$ un ensemble de symboles de fonction.
Let $\Func$ be a set of function symbols.
\end{defi}
\begin{cond}{SymbolSetsDistinct}
On impose que $\Sort$, $\Var$, $\FTyp$ et $\FObj$ soient 2 à 2 disjoints.
$\Sort$, $\Var$ and $\Func$ are pairwise disjoint.
\end{cond}
\begin{defi}[Fonction de sortage]
On suppose donnée une \emph{fonction de sortage} $s:\Func\to\Sort$.
\begin{defi}[Sorting function]
We suppose given a \emph{sorting function} $s:\Func\to\Sort$.
On note alors $\FObj=\enscond{f\in\Func}{s(f)=\Type}$ et $\FTyp=\enscond{f\in\Func}{s(f)=\Kind}$.
We then denote by $\FObj=\enscond{f\in\Func}{s(f)=\Type}$ and $\FTyp=\enscond{f\in\Func}{s(f)=\Kind}$.
\end{defi}
\begin{defi}[Termes (version non-stratifiée)]
On a la grammaire :
\begin{defi}[Terms (unstratified version)]
We have the grammar:
\begin{center}
\begin{tabular}{rlr}
$t,u$ & $::=\Kind\mid\Type\mid\Pi(x:t). u\mid\lambda (x:t). u\mid t\,u\mid f\mid x$& $f\in\Func$, $x\in\Var$\\
$t,u$ & $::=s\mid\Pi(x:t). u\mid\lambda (x:t). u\mid t\,u\mid f\mid x$& where $s\in\Sort$, $f\in\Func$, $x\in\Var$\\
\end{tabular}
\end{center}
On note $\Terms$ l'ensemble des termes.
We denote by $\Terms$ the set of all \emph{terms}.
\end{defi}
\begin{defi}[Contextes]
On définit la grammaire suivante, où $x$ est une variable et $T$ est un terme :
\begin{defi}[Contexts]
In the following grammar, $x$ is a variable and $T$ is a term:
\begin{center}
\begin{tabular}{rl}
$\Gamma$ & $::=[]\mid\Gamma,x:T$
......@@ -43,67 +44,72 @@ On note $\Terms$ l'ensemble des termes.
\end{center}
\end{defi}
\begin{defi}[Fonction de typage]
On suppose donnée une fonction $\tau:\Func\to\Terms$.
\begin{defi}[Typing function]
We suppose given a function $\tau:\Func\to\Terms$.
\end{defi}
\begin{cond}{Types clos}
Pour tout symbole $f$, $\tau(f)$ est clos.
\begin{cond}{ClosedTyp}
For all symbol $f\in\Func$, $\tau(f)$ is closed.
\end{cond}
\begin{defi}[Terme restreint à une position]
Soit $t$ un terme et $p$ un mot sur l'alphabet $\ens{\circ,\bullet}\cup\N$.
\begin{defi}[Term restricted to a position]
Let $t$ be a term and $p$ a word over the alphabet $\ens{\circ,\bullet}\cup\N$.
\[
\restrict{t}{\eps}=t \qquad
\restrict{t}{a::s}=\left\{\begin{array}{l}
\restrict{t_a}{s} \text{ si } t=t_0\,t_1\dots t_n, n>0, t_0\text{ n'est pas une application et }a\in\ens{0\dots n}\\
\restrict{T_a}{s} \text{ si } t=\Pi(x_1:T_1)\dots T_n, n>1, T_n\text{ n'est pas un produit et }a\in\ens{1\dots n}\\
\restrict{A}{s} \text{ si } t=\lm (x:A).\,u\text{ et }a=\circ\\
\restrict{u}{s} \text{ si } t=\lm (x:A).\,u\text{ et }a=\bullet\\
\text{n'est pas défini} \text{ sinon}
\restrict{t_a}{s} \text{ if } t=t_0\,t_1\dots t_n, n>0, t_0\text{ is not an application and }a\in\ens{0\dots n}\\
\restrict{T_a}{s} \text{ if } t=\Pi(x_1:T_1)\dots T_n, n>1, T_n\text{ is not a product and }a\in\ens{1\dots n}\\
\restrict{A}{s} \text{ if } t=\lm (x:A).\,u\text{ and }a=\circ\\
\restrict{u}{s} \text{ fi } t=\lm (x:A).\,u\text{ and }a=\bullet\\
\text{is not defined} \text{ otherwise}
\end{array}\right.
\]
\end{defi}
\todo{
Tous les sous-termes ne sont pas accessibles par cette définition de la position.
C'est volontaire ici et je considère que ce n'est pas un bug, mais il existe des applications pour lesquelles cette définition ne convient pas.
Note here that not all sub-terms can be accessed by this definition of position.
It is intended and I do not consider it as a bug.
There is of course application for which it is problematic.
}
\begin{defi}[Arité]
Soit $F$ un symbole de la signature tel que $\tau(F)=\Pi(x_1:T_1)\dots(x_n:T_n). U$,
$U$ ne contient pas de produit.
$n$ est alors appelée \emph{arité} de $F$.
\begin{defi}[Arity]
Let $F$ be a symbol of the signature with $\tau(F)=\Pi(x_1:T_1)\dots(x_n:T_n). U$,
where $U$ does not contain any arrow.
Then $n$ is called the \emph{arity} of $F$.
\end{defi}
\begin{defi}[Symbole appliqué partiellement et pleinement]
Soit $f$ un symbole de la signature et $t$ un terme.
$f$ est \emph{pleinement appliqué} dans $t$ si, pour toute position $a$ telle que $\restrict{t}{a}=f$,
$a=a'.0$ et $\restrict{t}{a'}$ est de la forme $f\,t_1\dots t_n$ avec $n\>\arity(f)$.
Sinon, $f$ est dit \emph{partiellement appliqué} dans $t$.
\begin{defi}[Fully and partially applied symbol]
Let $f$ be a symbol of the signature and $t$ be a term.
$f$ is \emph{fully applied} in $t$ if, for every position $a$ such that $\restrict{t}{a}=f$,
$a=a'.0$ and $\restrict{t}{a'}$ has the form $f\,t_1\dots t_n$ with $n\>\arity(f)$.
Otherwise, $f$ is \emph{partially applied} in $t$.
\end{defi}
\begin{defi}[Règle de réécriture]
On suppose donnée un ensemble $\Rules$ de \emph{règles de réécriture} de la forme
\begin{defi}[Rewrite rule]
We suppose given a set $\Rules$ of \emph{rewrite rules} of the form
\[f\,t_1\dots t_n\rul r\]
:
\begin{cond}{HeadDef}(Tête définissable).
$f\in \FTyp\cup\FObj$,
where :
\begin{cond}{HeadDef}(Definable head).
$f\in \Func$,
\end{cond}
\begin{cond}{Arity}(Arité).
\begin{cond}{Arity}(Arity).
$n\<\arity(f)$,
\end{cond}
\todo{On est triste d'avoir cette condition,
mais elle nous garantit qu'une fonction pleinement appliqu\'ee est un terme neutre,
ce qui nous aide grandement dans nos preuves,
on cherchera \`a la supprimer un peu plus tard.}
\todo{
We are sad to have this condition, but it is not a priority to remove it.
It offers us the guarantee that a fully applied function symbol is a neutral term,
which is very helpful in our proofs.
}
\end{defi}
\begin{defi}[Relation de réécriture]
On note $\rew$ la \emph{relation de réécriture} qui est l'union de la $\beta$-réduction
et de la plus petite relation close par substitution et contexte contenant $\Rules$.
\begin{defi}[Rewriting relation]
We denote by $\rew$ the \emph{rewriting relation} which is the union of the $\beta$-reduction
and of the smallest relation closed by substitution and context containing $\Rules$.
\end{defi}
\begin{cond}{Confluence}(Confluence locale).
La relation de réécriture est supposée localement confluente.
\begin{cond}{Confluence}(Confluence).
The rewriting relation is supposed to be locally confluent.
\end{cond}
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