Commit 605163ca authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

p

parent 45b6ca61
......@@ -133,7 +133,8 @@ Remarquons que l'ordre strict est d\'efini comme l'ordre large, sauf que ``$F\in
il existe un entier $n$ tel que les $st(C)$ sont de taille inférieure à $n$,
alors $>$ est bien fondé.}
\todo{On aimerait utiliser ce que l'on d\'efinit un peu plus tard dans cette d\'efinition, que ce soit $\rhd_{acc}$ pour pouvoir g\'erer un constructeur de type $(f:Nat\impli Ord)\impli((n:Nat)\impli T\,(f\,n))\impli T\,(lim\,n)$, ou SCT pour ne pas se restreindre \`a un ordre lexicographique. (Attention ici, la pr\'esence de = sur la diagonale des boucles idempotentes ne suffit pas dans le cas o\`u l'on d\'esire un inf\'erieur large).}
\todo{On aimerait utiliser ce que l'on d\'efinit un peu plus tard dans cette d\'efinition, que ce soit $\rhd_{acc}$ pour pouvoir g\'erer un constructeur de type $(f:Nat\impli Ord)\impli((n:Nat)\impli T\,(f\,n))\impli T\,(lim\,n)$, ou SCT pour ne pas se restreindre \`a un ordre lexicographique. (Attention ici, la pr\'esence de = sur la diagonale des boucles idempotentes ne suffit pas dans le cas o\`u l'on d\'esire un inf\'erieur large).
On doit pouvaoir en revanche envisager le plus grand ordre large compatible avec l'ordre strict induit par SCT.}
\begin{defi}[Types gel\'es]
Pour $F\in\FTyp'$, $\bar t$ des termes tels que $\valabs{\bar t}=\arity(F)$, on d\'efinit les deux grammaires :
......@@ -188,6 +189,12 @@ Dans cette d\'efinition, $\alpha$ est un ordinal, $\mu$ est un ordinal limite, $
\bigcup_{X<Y}\overline{\interp{\Type}_X}\cup\enscond{C\,\bar t\in\VTyp}{C\,\bar t\approx Y}\\
\omit\rlap{$\overline{\interp{\Type}_X}$ est le point fixe de la suite croissante $\paren{\interp{\Type}^\alpha_X}_\alpha$}
\end{align*}
\end{defi}
\remark{Pour que cette définition soit une ``bonne définition'', il faut que pour tout $A\in\interp{\Type}^\alpha_X$, l'on puisse définir $\interp{A}$.}
\begin{defi}
Soit $C\,\bar t\in\VTyp$ avec $C\in\CTyp$.
On d\'efinit alors $\bar C=\enscond{C'\in\CTyp}{C'\approx C}=(C_1,\dots,C_n)$, o\`u l'on omet la conversion entre ensemble et tuple pour des questions de lisibilit\'e.
On d\'efinit alors :
......@@ -213,10 +220,14 @@ On d\'efinit alors :
avec $R_{C\bar t}(T,(X_k))=
\left\{
\begin{array}{ll}
X_i& \text{s'il y a des }\bar l\text{ tels que }T=C_i\,\bar l\\
X_i& \text{s'il y a des }\bar l\text{ tels que }T=C_i\,\bar l\text{ et }C\,\bar t\approx C_i\,\bar l\\
\multicolumn{2}{l}{\enscond{t\in\Lm}{\text{pour tout }u\in R_{C\bar t}(T_1,\bar X),t\,u\in R_{C\bar t}(\subst{T_2}{x}{u},\bar X)}\text{ si }T=(x:T_1)\impli T_2}\\
\interp{C'\bar u}&\text{si }T=C'\,\bar u\text{ et }C'\,\bar u<C\,\bar t\\
\end{array}
\right.
\right.$
\end{defi}
\remark{Pour que cette définition soit une ``bonne définition'',
il faut que pour tout $C'\,\bar u<C\,\bar t$, $\interp{C'\,\bar u}$ soit défini.}
\end{document}
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