Commit 42b666f9 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

m

parent 605163ca
......@@ -103,7 +103,7 @@
\section{Accessibilit\'e}
\begin{defi}[Constructeur de type]
On note \[CTyp=\enscond{F\in\FTyp}{F\text{ n'est pas la t\^ete du membre gauche d'une r\`egle.}}\]
On note \[\CTyp=\enscond{F\in\FTyp}{F\text{ n'est pas la t\^ete du membre gauche d'une r\`egle.}}\]
\end{defi}
\begin{nots}
......@@ -111,7 +111,7 @@
\end{nots}
\begin{defi}[Ordre sur les types]
On se donne $\FTyp'\subseteq\FTyp$ tel que $\CTyp\subseteq\FTyp'$ et $\succ$ un pr\'e-ordre bien fond\'e sur les symboles de $\FTyp'$.
On se donne $\FTyp'\subseteq\FTyp$ tel que $\CTyp\subseteq\FTyp'$ et $\succeq$ un pr\'e-ordre bien fond\'e sur les symboles de $\FTyp'$.
\end{defi}
\begin{defi}[Statut]
......@@ -171,8 +171,9 @@ on a $\valabs{l}=\arity(F)$ et $r\in\Froz_{\<F\bar l}$.
\section{Interpr\'etations}
Soit $\chi : \Part{\Lm}\setminus\emptyset\to\Lm$ une fonction de choix.
On laisse sous-entendu que tout d\'epend de $\chi$.
On discutera ensuite l'indiff\'erence \`a cette fonction.
\todo{On laisse sous-entendu que tout d\'epend de $\chi$.
On discutera ensuite l'indiff\'erence \`a cette fonction.}
\begin{defi}[Interpr\'etations de $\Type$ et des types]
Dans cette d\'efinition, $\alpha$ est un ordinal, $\mu$ est un ordinal limite, $X\in\VTyp\cup\ens{\bot}$ et $Y\in\VTyp$.
......@@ -187,16 +188,21 @@ Dans cette d\'efinition, $\alpha$ est un ordinal, $\mu$ est un ordinal limite, $
\bigcup_{\alpha<\mu}\interp{\Type}^\alpha_X\\
\interp{\Type}^0_Y =&
\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$}
\omit\rlap{\remark{Ici on n'a pas imposé que les $t_i$ soient dans l'interprétation de leur type !}}\\
\omit\rlap{$\overline{\interp{\Type}_X}$ est le point fixe de la suite croissante $\paren{\interp{\Type}^\alpha_X}_\alpha$\todo{Prouver la croissance}}
\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$.
Soit $C\,\bar t\in\VTyp$.
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.
\todo{Se casser les pieds avec un ordre global sur les symboles de la signature permettant de faire ce cast facilement.}
On d\'efinit alors :
\[
\deffonc{K_{C\bar t}}{\Part{\Lm}^n}{\Part{\Lm}^n}{(X_i)_{i\<n}}
......@@ -209,6 +215,7 @@ On d\'efinit alors :
\begin{array}{l}
\tau(c)=\overline{(x:T)}\impli (C_i\,\bar s)\\
m\>\arity(c)\\
(C_i\,\bar s)\crochet{\bar x\mapsto\bar v}\approx C\,\bar t\\
\text{pour tout }j\in\Acc(c), v_j\in R_{C\bar t}(T_j,(X_k))\\
\end{array}
\right.\\
......@@ -230,4 +237,10 @@ avec $R_{C\bar t}(T,(X_k))=
\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.}
On définit $\interp{C\,\bar t}$ comme la ``bonne'' projection du plus petit point fixe de la fonction croissante $K_{C\bar t}$.
\todo{Prouver la croissance}
Si
\end{document}
......@@ -32,6 +32,7 @@
\usepackage{color}
\usepackage{blkarray}
\usepackage{diagbox}
\usepackage{varwidth} %Allow varwidth variant of minipage
\theoremstyle{plain}
\newtheorem{thm}{Theorem}[section]
......@@ -93,18 +94,17 @@
\newcommand{\proba}[1]{\mathrm{Pr}\crochet{#1}}
\newcommand{\subst}[3]{#1\left[\sur{#3}{#2}\right]}
\newcommand{\encadr}[1]{\fbox{\begin{minipage}{0.9\textwidth}{#1}\end{minipage}}}
\newcommand{\encadr}[1]{\fbox{\begin{varwidth}{0.9\textwidth}{#1}\end{varwidth}}}
\definecolor{noir}{RGB}{0,0,0}
\definecolor{gris}{RGB}{150,150,150}
\definecolor{rouge}{RGB}{255,0,0}
\definecolor{bleu}{RGB}{0,0,255}
\definecolor{vert}{RGB}{0,150,0}
\newcommand{\rem}[1]{\fbox{\begin{minipage}{0.9\textwidth}\textcolor{bleu}{#1}\end{minipage}}}
\newcommand{\ajout}[1]{{\large \textcolor{vert}{#1}}}
\newcommand{\todo}[1]{\textcolor{red}{{\large TO DO} \fbox{\begin{minipage}{0.7\textwidth}{#1}\end{minipage}}}}
\newcommand{\todo}[1]{\textcolor{red}{{\large TO DO} \fbox{\begin{varwidth}{0.7\textwidth}{#1}\end{varwidth}}}}
\newcommand{\question}[1]{\textcolor{orange}{Question: #1}}
\newcommand{\answer}[1]{\textcolor{vert}{Answer: #1}}
\newcommand{\remark}[1]{\textcolor{blue}{{\large Remark} \fbox{\begin{minipage}{0.7\textwidth}{#1}\end{minipage}}}}
\newcommand{\remark}[1]{\textcolor{blue}{{\large Remark} \fbox{\begin{varwidth}{0.7\linewidth}{#1}\end{varwidth}}}}
\DeclareMathOperator{\Frac}{Frac}
\DeclareMathOperator{\Card}{Card}
......
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