\documentclass[a4]{seminar}

\usepackage{amsmath,amssymb}
\usepackage{amsthm,amsfonts}
\usepackage{enumerate}
\usepackage[french]{babel}
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}

\usepackage[all]{xy}
\usepackage[purexy]{qsymbols}

\usepackage{psfig}
\usepackage{proof}

\newcommand{\X}{$\mathcal X$}

\newcommand{\ul}{\ar[ul]}
\newcommand{\ur}{\ar[ur]}
\newcommand{\ulr}{\ar[ul] \ar[ur]}

\newcommand{\hasse}[1]{\xymatrix@R-1em@C-2em{#1}}
\newcommand{\reduction}{$$x ``[= y   "<==>" `A y ``<= y', x \uparrow  y'$$}

\newtheorem*{faits}{Faits}
\newtheorem*{fait}{Fait}
\newtheorem*{thm}{Théorème}

\begin{document}
\begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{Typing Constraint Logic Programs}
\author{François Fages, Emmanuel Coquery}
\date{}
\maketitle

\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

{\tiny \tableofcontents}

\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Introduction}

\subsection{Motivations}

\begin{itemize}
\item Traditionnellement, les langages de programmation logique 
dérivés de Prolog ne sont pas typés.

\item Prolog ne travaille que sur des termes de Herbrand, sans
les interpréter dans des univers mathématiques autrement
que comme des termes.
\end{itemize}

\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{itemize}
\item Dans CLP(\X), cependant, les objets sur lesquels portent
les contraintes vivent dans des univers (entiers, réels, booléens,
listes, termes finis ou infinis).

\item Comme dans tout langage non typé, il est facile
de se tromper et d'écrire des programmes grossierement
faux, par exemple en utilisant l'opérateur d'addition
sur les entiers pour concaténer deux listes.

\item On voudrait avoir un système de types pour CLP(\X)
qui permette de capturer statiquement ces erreurs. 
\end{itemize}

\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Spécificités de CLP(\X)}

\begin{itemize}
\item Le langage est générique, parametré par un domaine \X~
arbitraire. Le système de types devra être également générique.

\item Le polymorphisme paramétrique à la ML a fait ses preuves;
on veut avoir des types parametrés, comme $list (\alpha)$.

\item Les erreurs de type peuvent ne pas provoquer d'erreur
dynamiquement, mais juste l'échec de la résolution, ou des
fausses solutions (moralement mal typées). Il faudra voir 
comment capturer ces erreurs.
\end{itemize}

\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{itemize}
\item On veut garder la souplesse des coercions implicites.
Par exemple, un entier peut être vu comme un réel, et tout
objet peut être vu comme un terme. On va donc travailler
avec une notion de sous-typage et une règle de subsomption.

\item Contrairement à ML, cependant, on ne travaille pas
avec des types fonctionnels; cela va simplifier l'étude
du sous-typage, mais il faudra faire attention à ce que devient la 
contravariance de la flèche.
\end{itemize}

\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Le système de types}

\subsection{Algèbre des types}

Les types $\tau$ sont les termes finis sur une signature donnée
par un ensemble fini de constructeurs munis d'une arité $\in \mathbb N$,
et des variables de types.

$\mathcal U = \alpha, \beta, \ldots$ (variables)

$\mathcal K = K, \ldots$ (constructeurs)

Les types de bases sont les constructeurs d'arité 0. En particulier,
on suppose qu'il y a un type de base $bool$.

\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Sous-typage}

L'ensemble des constructeurs est muni d'une relation
de sous-typage $``<=$ qui est un ordre.

On suppose donnée, pour tout couple de constructeurs $K$,$K'$ 
d'arités respectives $m$,$m'$ tels que $K``<= K'$, 
une injection $\iota_{K,K'}:\{1,\ldots, m'\} \rightarrow \{1,\ldots, m\}$
de sorte que :

\begin{itemize}
\item $\iota_{K,K''} = \iota_{K,K'} \circ \iota_{K',K''}$ lorsque 
$K ``<= K' ``<= K''$

\item $\iota_{K,K} = id$
\end{itemize}

On suppose également que pour tout constructeur, l'ensemble de
ses majorants admet un plus grand élément.

\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Les constructeurs sont covariants en chacun de leurs
arguments. Les injections $\iota_{K,K'}$ indiquent
comment sont reliés les positions des arguments de deux
constructeurs en relation de sous-typage.

Formellement, on défini la relation de sous-typage
sur les types par les règles:

$$
\infer[(Par)]{ \alpha ``<= \alpha }{}
$$

$$
\infer[(Constr)]{ K(\tau_1,\ldots,\tau_m) ``<= K'(\tau'_1,\ldots,\tau'_m) } 
           {\tau_{\iota(1)} ``<= \tau_1 & \ldots & \tau_{\iota(m')}
             ``<= \tau_m'  & K ``<= K' & \iota=\iota_{K,K'} }
$$

(Ce système est algorithmique)

C'est un ordre, et pour tout typage, l'ensemble de ses majorants
admet un plus grand élément.

\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

On peut considérer par exemple les constructeurs:

\hasse{
 & term \\
float \ur & bool \ar[u] & list(\alpha) \ul \\
int \ar[u] \ar[ur] \\
}

On décide de s'autoriser à voir un entier comme un flottant, mais aussi comme
un booléen ($true$ si non nul).

\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{CLP(\X) explicitement typé}

On considère des programmes CLP(\X) où les symboles
de fonctions et de prédicats (prédicats de contrainte et de programme)
ont chacun un schéma de type déclaré:
$f_{\tau_1, \ldots, \tau_n \rightarrow \tau}$,
$p_{\tau_1, \ldots, \tau_n}$.
L'égalité est un prédicat dont le schéma est $\alpha,\alpha$.

Moralement, les variables de types dans les $\tau_i$ 
sont quantifiées universellement.

On se donne un environnement de typage des variables
du programme $U = \{ x_i: \tau_i \}$.

On dit qu'un élément est bien typé lorsque le système
ci-après lui donne un type pour un certain environnement
de typage.

\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Typage des objets et des atomes (contraintes et vrais atomes):

$$\infer[(Sub)]{ t:\tau' }{ t:\tau ``<=\tau' }$$
$$\infer[(Var)]{ x:\tau }{ (x:\tau) \in U }$$
$$\infer[(Func)]{ f_{\overrightarrow{\tau_i} \rightarrow \tau}
  (\overrightarrow{t_i}):\tau \Theta} { t_i:\tau_i \Theta }$$
$$\infer[(Atom)]{ p_{\overrightarrow{\tau_i} } (\overrightarrow{t_i})
  {\bf~Atom} } { t_i:\tau_i \Theta }$$

$\Theta$ est une substitution (des variables de types
vers les types).

\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Typage des requêtes et des clauses:

$$\infer[(Query)]{A_1,\ldots,A_n {\bf~Query}}{A_i {\bf~Atom}}$$

$$\infer[(Clause)]{ p_{\overrightarrow{\tau_i}}(\overrightarrow{t_i}) \leftarrow Q
  {\bf~Clause} }
{ t_i:\tau_i \Theta & Q {\bf~Query} }$$

$\Theta$ est un {\bf renommage} des variables de types.

\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{La résolution CSLD préserve le typage}

Interdire une substitution arbitraire dans le typage
des membres gauche permet d'assurer le principe de définition
générique et la {\sl subject reduction} vis-à-vis de la
résolution.

\begin{thm}
Soit $Q$ une requête bien typée dans l'environnement $U$, 
$Q'$ une resolvante de $Q$ par une clause bien typée.
Alors $Q'$ est une requête bien typée dans un certain environnement 
qui étend $U$.
\end{thm}

{\small 
Sans la restriction de définition générique, le 
résultat est faux.
Prenons $\tau_a, \tau_b$ deux types sans majorant commun,
deux constantes $a:\tau_a, b:\tau_b$, et un prédicat
$p_{\alpha}$ défini par une clause $p(a)$. Alors
la requête $p(b)$, bien typée, donne une resolvante
$a=b$ mal typée.
}
\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Faiblesses du résultat}

Remarquons que le résultat de {\sl subject reduction} est assez
faible dans ce cadre. Si tous les constructeurs ont un majorant commun
(par exemple, $term$), alors il ne dit rien.
En effet, les seuls atomes nouveaux qui apparaissent dans une 
résolvante sont des contraintes d'égalité, qui seraient alors
toujours bien typées.

\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Considérons un prédicat $p_{int}$ défini par le programme
$p(X)$. La requête $Y = true, p(Y)$ est bien typée
dans $\{ Y : int \}$, et succède effectivement,
avec le système de contrainte $\{ Y = true \}$. Dans le cadre
non typé, cette contrainte est satisfiable, et l'on
n'a pas changé la notion de satisfiabilité pour prendre
en compte les types.

Une solution, pour rester dans le même formalisme,
c'est d'introduire {\bf des contraintes qui parlent des types}.

On peut voir aussi apparaître le problème avec
une sémantique plus précise que la seule
résolution CSLD, par exemple si on s'autorise
à {\bf propager les contraintes d'égalités}; 
en effet, la requête
précédente amène à considérer la résolvante
$p(true)$, qui, elle, est mal typée.

\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Résolution + substitution}

On peut utiliser l'information que l'on a sur les types 
pour bloquer les résolutions
qui introduisent des égalités contradictoires.

L'idée, c'est de garder cette information sous la forme
de contraintes de types $t : \tau$. Il faut donc pouvoir
interpreter ces contraintes. Cela se fait naturellement
en voyant les types de base comme des ensembles de valeurs
(sous-ensembles de \X) et les autres constructeurs 
comme des applications, de sorte que la relation
de sous-typage entraine bien l'inclusion.

Les valuations permettent d'interpreter les variables
du programmes et les variables de type.

Le nouveau langage, qui est encore une instance
de CLP, est noté TCLP.

\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Le point fondamental, c'est que les deux contraintes
$\{ X : \tau ; X = t \}$ entrainent $t : \tau$.

À toute clause bien typée dans un environnement $U$,
on associe une clause TCLP obtenu en lui ajoutant
les contraintes de type données par $U$. De même pour
les requêtes. On considère un programme TCLP obtenu
ainsi et des résolution CSLD à partir de ses clauses.

\begin{thm}
Soit $Q$ une requête TCLP bien typée dans l'environnement $U$,
$Q'$ une résolvante de $Q$. Alors $Q'$ est bien typée
dans un certain environnement $U'$ qui étend $U$, et de plus,
si $Q'$ a une contrainte $X=t$, alors la requête
$Q'[t/X]$ est bien typée dans $U'$.
\end{thm}

\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Dans l'exemple avec le prédicat $p_{int}$ (défini par $p(X)$)
et la requête $Y = true, p(Y)$ bien typée
dans $\{ Y : int \}$, on voit que la requête augmentée elle-même
a un jeu de contraintes non-satisfiable ($Y = true; Y : int$),
donc elle est rejetée immédiatemment.

Mais il ne faut pas croire que les nouvelles contraintes
servent juste à faire une vérification statique. Même si
tout est bien typée avec les contraintes de type rajoutées,
il faut {\bf conserver ces contraintes lors de l'exécution}.

Prenons l'exemple d'un prédicat $p_{float}$ défini par
$p(X) \leftarrow X = 2,5$ et d'une requête $p(Y)$ typée
avec $\{ Y : int \}$. Elle est satisfiable (seule contrainte:
$Y : int$), et si on oublie les contraintes de type lors
de la résolution, on arrive à une solution intuitivement mal typée.

{\small Note: avec ces nouvelles contraintes de type, on peut
se passer de la restriction de définition générique. C'est-à-dire
que l'on peut donner des définitions spécialisées à certains
types pour des prédicats génériques.}

\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\section{Vérification et inférence}

\subsection{Vérification}

Le système de types donné ne donne pas directement un
algorithme de vérification.  Pour obtenir
un tel algorithme, on commence par intégrer, 
de manière tout à fait classique, la règle de 
subsomption aux autres règles.

La forme des dérivations de typage étant alors imposée par 
le système, il reste à trouver comment construire les 
substitutions qui apparaissent dans les règles. 
Pour cela, on renomme toutes les variables de type
des instances des prédicats et des fonctions dans la dérivation,
et on collecte le long de celle-ci les contraintes de 
sous-typage. 

\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Voici les règles de l'algorithme:
{\small
$$\infer[(Var)]{ x:\tau }{ (x:\tau) \in U }$$

$$\infer[(Func')]{ f_{\overrightarrow{\tau_i} \rightarrow \tau}
  (\overrightarrow{t_i}):\tau \Theta} { t_i : \sigma_i ``<= \tau_i \Theta }$$

$$\infer[(Atom')]{ p_{\overrightarrow{\tau_i} } (\overrightarrow{t_i})
  {\bf~Atom} } { t_i : \sigma_i ``<= \tau_i \Theta }$$

$$\infer[(Query)]{A_1,\ldots,A_n {\bf~Query}}{A_i {\bf~Atom}}$$

$$\infer[(Clause')]{ p_{\overrightarrow{\tau_i}}(\overrightarrow{t_i}) \leftarrow Q
  {\bf~Clause} }
{ t_i : \sigma_i ``<= \tau_i \Theta & Q {\bf~Query} }$$}
\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Résolution du système}

Le système a une forme très particulière: il est {\bf linéaire
à gauche} (les variables ont au plus une occurence à gauche
des inégalités) et {\bf acyclique} (on peut mettre un bon ordre
sur les variables de sorte que dans chaque contrainte,
les variables à gauche sont plus petites strictement
que celles à droite).

La résolution d'un tel système est un problème
de {\bf complexité linéaire} en le nombre de symboles.
Ce qui rend le problème facile, c'est d'une part la covariance
de tous les constructeurs et d'autre part l'existence
d'un plus grand majorant pour tous les types.
Par exemple, une contrainte $\alpha ``<= \tau$ est transformée
en $\alpha = \tau$, alors que $\tau ``<= \alpha$ donne
$\alpha = Max (\tau)$ (le plus grand majorant de $\tau$)
lorsque $\alpha$ n'apparaît jamais dans un membre gauche.


\end{slide} \begin{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Inférence}

Il n'est pas difficile d'inférer le type des variables dans
les clauses et les requêtes. On obtient comme pour la
vérification un système de contraintes de sous-typage.
Il est toujours acyclique, mais plus linéaire à gauche.

{\small 
(sous l'hypothèse que l'ordre de sous-typage est un treillis,
le problème peut être résolu en temps cubique; sinon, on
est plutôt autour de Pspace)
}

Sous certaines conditions, il est possible également
d'inférer le type des prédicats. Cependant, s'il y a une 
solution, on peut toujours prendre des types maximaux
Par exemple, si $term$ est le plus grand type,
on peut typer tous les prédicats par $term,\ldots,term$, 
mais ce n'est pas très intéressant; on cherche un type
qui donne plus d'information.

\end{slide}
\end{document}