Commit 62a636a6 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

k

parent cde7debd
\documentclass{article}
\input{enTeteArticle}
\usepackage{geometry}
\geometry{left=3cm, right=3cm, bottom=3cm}
\DeclareMathOperator{\Kind}{Kind}
\DeclareMathOperator{\Type}{Type}
\DeclareMathOperator{\support}{supp}
\DeclareMathOperator{\FreeVar}{FV}
\DeclareMathOperator{\SN}{SN}
\DeclareMathOperator{\WN}{WN}
\DeclareMathOperator{\NF}{NF}
\DeclareMathOperator{\RED}{RED}
\DeclareMathOperator{\domain}{dom}
\DeclareMathOperator{\arity}{ar}
\DeclareMathOperator{\Acc}{Acc}
\DeclareMathOperator{\AccVar}{AccVar}
\DeclareMathOperator{\lfp}{lfp}
\DeclareMathOperator{\Froz}{FrozTyp}
\DeclareMathOperator{\Candidates}{Cand}
\DeclareMathOperator{\Position}{Pos}
\DeclareMathOperator{\AccPosHd}{AccPosHd}
\DeclareMathOperator{\AccPosCstr}{AccPosCstr}
\DeclareMathOperator{\InferTypeHd}{InferTypeHd}
\DeclareMathOperator{\InferTypeCstr}{InferTypeCstr}
\DeclareMathOperator{\SCT}{SCT}
\newcommand{\red}[2]{\RED_{\paren{#1}}\paren{#2}}
\newcommand{\rul}{\hookrightarrow}
\newcommand{\rew}{\rightarrow}
\newcommand{\reww}{\rew^*}
\newcommand{\conv}{\leftrightarrow^*}
\newcommand{\call}{~\widetilde{\succ}~}
\newcommand{\preced}{\preccurlyeq}
\newcommand{\subterm}{\triangleleft}
\newcommand{\surterm}{\triangleright}
\newcommand{\interp}[1]{\left\llbracket{#1}\right\rrbracket}
\DeclareMathOperator{\ype}{ype}
\newcommand{\TType}{\mathbb{T}\!\ype}
\DeclareMathOperator{\ind}{ind}
\newcommand{\KKind}{\mathbb{K}\!\ind}
\newcommand{\Sort}{\mcal{S}}
\newcommand{\Var}{\mcal{X}}
\newcommand{\Func}{\mcal{F}}
\newcommand{\CTyp}{\mcal{C}_T}
\newcommand{\CObj}{\mcal{C}_o}
\newcommand{\FTyp}{\mcal{F}_T}
\newcommand{\FObj}{\mcal{F}_o}
\newcommand{\Rules}{\mcal{R}}
\newcommand{\Terms}{\Lm}
\newcommand{\NTyp}{\mcal{N}_T}
\newcommand{\NObj}{\mcal{N}_o}
\newcommand{\cstrHeaded}{\mbb{D}}
\newcommand{\geqts}{\succcurlyeq}
\newcommand{\gstrts}{\succ}
\newcommand{\eqts}{\approx}
\newcommand{\intType}{\interp{\Type}}
\DeclareMathOperator{\order}{Ord}
\DeclareMathOperator{\lexico}{lex}
\DeclareMathOperator{\product}{prod}
\lstset{backgroundcolor=\color{grispale},language={Dedukti}}
\usepackage{mdframed}
\theoremstyle{plain}
\newtheorem{condition}[thm]{Condition}
\newenvironment{cond}[1]
{
\begin{mdframed}
\color{blue}
\begin{condition}
\label{#1}
}
{\end{condition}
\end{mdframed}}
\newcommand\indcond[1]{(see Cond. \ref{#1})}
\title{Interpr\'etation des types positifs}
\author{Guillaume Genestier}
\date{Mai 2019}
% If the following line is uncommented, discussions are hidden.
%\renewcommand\answer\hide \renewcommand\question\hide \renewcommand\todo\hide \renewcommand\remark\hide
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
\maketitle
\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.}}\].
\end{defi}
\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'$.
\end{defi}
\begin{defi}[Statut]
On munit chaque $F\in\FTyp'$ d'arit\'e $k$ d'un tuple d'entiers inf\'erieurs \`a $k$ : $(i_1,\dots,i_n)$.
\end{defi}
\begin{defi}[Ordre sur les types construits]
Soit $F\in\FTyp'$ de statut $(i_1,\dots,i_n)$ et $F'\in\FTyp'$ de statut $(j_1,\dots,j_{n'})$.
On a $F\,\bar t\>F'\,\bar u$ si l'une des 2 conditions suivantes sont v\'erifi\'ees :
\begin{itemize}
\item $F\succ F'$,
\item $F\approx F'$ et $(t_{i_1},\dots,t_{i_n})\unrhd_{lex}(u_{j_1},\dots,u_{j_{n'}})$.
\end{itemize}
Remarquons que l'ordre strict est d\'efini comme l'ordre large, sauf que $\rhd$ remplace $\unrhd$ dans la derni\`ere condition.
\end{defi}
\remark{Si chaque classe d’équivalence pour $\approx$,
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 $\Pi(f:Nat\impli Ord).(\Pi(n:Nat).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).}
\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 :
\begin{align*}
T_{\<F\bar l}&::=\Pi(x:U_{<F\bar l}).T_{\<F\bar l}\,\mid\,F'\,u_1,\dots,u_{\arity(F')}&\text{where }F'\,\bar u\<F\,\bar l\\
T_{<F\bar l}&::=\Pi(x:U_{\<F\bar l}).T_{<F\bar l}\,\mid\,F'\,u_1,\dots,u_{\arity(F')}&\text{where }F'\,\bar u<F\,\bar l\\
\end{align*}
On note ces 2 ensembles $\Froz_{\<F\bar l}$ et $\Froz_{<F\bar l}$ respectivement.
\end{defi}
\remark{Ici, on a d\'efini la positivit\'e non-stricte,
\c{c}a ne semble pas poser de probl\`eme pour les preuves.}
\begin{cond}{R\'e\'ecriture d\'ecroissante}
Pour tout $F\in\FTyp'$, pour toute r\`egle $F\,\bar l\rul r$,
on a $\valabs{l}=\arity(F)$ et $r\in\Froz_{\<F\bar l}$.
\end{cond}
\begin{defi}[Constructeurs]
\[\CObj=\enscond{f\in\FObj}{\tau(f)=\Pi\overline{(x:T)}.C\,t_1\dots t_{\arity(C)}}\]
\end{defi}
\todo{Supprimer la restriction interdisant les constructeurs de types d\'efinis.}
\remark{La pleine application de $C$ est impos\'ee par typage, ce n'\'etait pas utilde de la remettre ici.}
\begin{defi}[Position accessible]
Soit $f\in\CObj$, tel que $\tau(f)=\Pi\overline{(x:T)}.C\,t_1\dots t_{\arity(C)}$, on a :
\[\Acc(f) = \enscond{i\<\arity(f)}{T_i \in\Froz_{\<C\bar t}}.\]
\end{defi}
\remark{On d\'efinira $\rhd_{acc}$ plus tard car l'on a besoin de l'intrepr\'etation pour cela.}
\section{Interpr\'etations}
\end{document}
......@@ -104,6 +104,7 @@
\newcommand{\todo}[1]{\textcolor{red}{{\large TO DO} \fbox{\begin{minipage}{0.7\textwidth}{#1}\end{minipage}}}}
\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}}}}
\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