\documentclass[a4paper,12pt]{article} \usepackage{epsfig} \psfigdriver{dvips} \usepackage[francais]{babel} \usepackage[latin1]{inputenc} \usepackage[T1]{fontenc} \usepackage{vmargin} % redéfinir les marges \setmarginsrb{2cm}{2cm}{2cm}{2cm}{0cm}{0cm}{0cm}{1cm} % Marge gauche, haute, droite, basse; espace entre la marge et le texte à % gauche, en haut, à droite, en bas \usepackage{amsmath,amssymb,chemarr} \usepackage{verbatim} \usepackage{supertabular} \usepackage{url} \usepackage{graphicx} \usepackage{fancyhdr} \newcommand\latex{ \begin{math} \mathrm{L^{A}T_{E}X} \end{math} } \newcommand\tex{ \begin{math} \mathrm{T_{E}X} \end{math} } \newcommand\ltac{$\mathcal L _{tac}$} \setlength{\parindent}{0pt} \newcommand\sautligne{ \par\vspace{12pt} } \newcommand\lo{ $\lambda_\bigcirc$ } \newcommand\Lo{ $\mathcal L_\bigcirc$ } \clubpenalty=1000 %% évite les lignes orphelines \widowpenalty=1000 %% évite les lignes veuves \hyphenpenalty=1000 %% évite de couper les mots \title{Vérification formelle d'algorithmes probabilistes} \author{Tahina Ramananandro \\ Ecole Normale Supérieure -- \textsc{Paris}} \date{27 juin -- 25 août 2005} \newtheorem{ax}{Axiome}[subsection] \newtheorem{defin}{Définition}[subsection] \newtheorem{prop}{Proposition}[subsection] \newtheorem{theo}{Théorème}[subsection] \newtheorem{lemme}{Lemme}[subsection] \newenvironment{preuve}{\textbf{Démonstration }}{\hfill$\square$} \newenvironment{liste-i}{\renewcommand\theenumi{(\roman{enumi})} \renewcommand\labelenumi{\theenumi}\begin{enumerate}}{\end{enumerate}} \begin{document} \maketitle \thispagestyle{empty} \tableofcontents \clearpage \addcontentsline{toc}{section}{Préface} \section*{Préface} J'ai effectué ce stage à l'INRIA Sophia-Antipolis\footnote{Institut National de Recherche en Informatique et en Automatique -- 2004, route des Lucioles -- 06902 \textsc{Sophia-Antipolis Cedex}, France}, au sein de l'équipe \emph{Marelle}, sous la direction de MM. Philippe Audebaud et Laurent Théry, que je remercie ainsi que tous les membres des équipes \emph{Marelle} ainsi que \emph{Everest}. L'équipe \emph{Marelle} («Mathématiques, Raisonnement, Logiciel») s'occupe de la vérification formelle de logiciels, et travaille autour du système d'aide à la preuve Coq \cite{coq}, tandis que l'équipe \emph{Everest} («Environments for Verification and Security of Software»), dans le même bâtiment, est spécialisée dans la vérification des aspects de sécurité des logiciels (notamment les protocoles cryptographiques). ~ Je dois dire que l'ambiance a été chaleureuse étant donné qu'à ma grande surprise, tout le monde se tutoie dans le laboratoire. J'ai pu avoir un aperçu significatif du travail réalisé dans ces deux équipes en participant aux séminaires, aussi bien de cryptographie que de sémantique, organisés chaque jeudi après-midi. MM. les responsables de mon stage m'ont soutenu tout au long de mon expérience, tant sur le fond que du point de vue de la méthode de travail, tout en me laissant la liberté d'explorer le sujet par moi-même, liberté dont j'ai avantageusement profité pour aboutir à une présentation «atypique» selon leurs propres termes. Pour ce qui est de l'environnement de travail, j'ai commencé par une prise de contact avec le système d'aide à la preuve Coq, et j'avoue que j'y ai pris goût -- et c'est un doux euphémisme ! Vers la fin du stage -- fin août, où il n'y a plus grand monde au laboratoire, pour cause de vacances --, MM. Philippe Audebaud et Laurent Théry m'ont efficacement conseillé pour la réalisation du diaporama de l'exposé final, ainsi que pour la rédaction du présent rapport. \clearpage \addcontentsline{toc}{section}{Introduction} \section*{Introduction} Les algorithmes probabilistes interviennent dans de nombreux domaines où une approche déterministe précise est inabordable, souvent en raison de la complexité des algorithmes déterministes. C'est le cas en algorithmique, par exemple en cryptographie (voir la preuve formelle du test de primalité de Miller-Rabin dans \cite{hurd}). Souvent, surtout dans des programmes à vocation statistique comme l'échantillonnage de données environnementales (problèmes de localisation d'un robot, mesures de grandeurs physiques), on recourt à un algorithme probabiliste afin de simuler par ordinateur une distribution de probabilité. Bien entendu, de telles simulations sont souvent abordées par une approche mathématique (voir par exemple \cite{markov}). Il s'agit ici de considérer la possibilité d'élaborer des preuves formelles de tels algorithmes de simulation dans un environnement d'aide à la preuve. ~ Pour pouvoir raisonner formellement sur un algorithme probabiliste, il faut tout d'abord savoir représenter de façon formelle non seulement l'algorithme lui-même, mais aussi les données aléatoires qu'il va utiliser, et la façon dont il va les utiliser (chapitre \ref{s-1}). Pour ce faire, le premier point concerne l'approche de programmation à adopter pour considérer l'algorithme : modèle impératif (le plus utilisé) ou modèle fonctionnel ? J'ai préféré cette dernière approche ; ainsi, les données aléatoires seront modélisées par un flot, et les tirages par des consommations de ce flot. Je considère alors la représentation des algorithmes probabilistes dans un langage fonctionnel, le \emph{Lambda-O}, ou \lo \cite{lo}, qui distingue constamment termes déterministes et expressions aléatoires, tant du point de vue de la réduction que du typage. ~ L'algorithme étant représenté, comment exprimer des propriétés probabilistes s'y rapportant, et surtout comment raisonner avec ces propriétés (chapitre \ref{s-2}) ? Ici encore, plusieurs approches existent. La plus courante est de procéder par obligations de preuve, à l'instar de Why \cite{why}. Mais pour ma part, j'ai préféré procéder par <> du programme écrit en \lo vers une formule logique décrivant son comportement et destinée à être utilisée dans le raisonnement probabiliste. Une telle formule ne comporte pas d'éléments probabilistes à proprement parler, ceux-ci n'intervenant que plus tard, dans le raisonnement sur la formule obtenue. Une fois la formule obtenue, il faut pouvoir raisonner dessus. Ceci implique la formalisation, dans un système de preuve, de la théorie des probabilités, et le lien entre cette théorie et la représentation des données aléatoires que l'on s'est proposée au départ. Pour cette formalisation, j'ai utilisé le système de preuve Coq \cite{coq}. Une fois formalisée la théorie des probabilités, je l'applique aux flots de données aléatoires et j'intègre également, dans le Calcul des Constructions Inductives \cite{cic}, le langage des formules générées à partir de programmes en \lo. ~ Cette formalisation tant de l'algorithme probabiliste que de la logique probabiliste mise en place pour raisonner, m'a permis de traiter quelques exemples simples (chapitre \ref{s-3}). Dans le cadre des simulations sur l'espace des flots dont les éléments sont des réels uniformément distribués sur $[0, 1]$, je montre comment prouver formellement en Coq la terminaison et la correction d'algorithmes de simulation de lois simples telles que la loi de Bernoulli (algorithme non récursif), la loi binomiale (récursivité déterministe), ou encore la loi géométrique (récursivité probabiliste). \clearpage \section{Représentation d'un algorithme probabiliste} \label{s-1} Pour définir formellement ce qu'est un algorithme probabiliste, j'ai choisi de suivre une voie commune à \cite{hurd} et \cite{lo} : de façon informelle, on considère qu'un algorithme probabiliste est simplement une fonction qui prend en entrée une donnée aléatoire, mais qui renvoie toujours la même sortie si la même donnée lui est passée en entrée (en somme, c'est une «vraie» fonction). \subsection{Les données aléatoires} Qu'entend-on donc par \emph{donnée aléatoire} ? Il s'agit en fait d'une donnée \emph{tirée au hasard} dans un certain espace de probabilités. Mais il faut pouvoir définir la nature de cette donnée (type, distribution, etc.), et la façon dont elle est utilisée par l'algorithme. Un algorithme probabiliste effectue des \emph{tirages aléatoires}. Ces tirages satisfont deux propriétés : \begin{itemize} \item les tirages sont indépendants deux à deux \item tous les tirages suivent la même loi de probabilité \end{itemize} ~ L'approche impérative consiste à des appels d'une procédure du style \texttt{rand()}, avec des effets de bord. ~ L'approche fonctionnelle, que j'ai choisie pour représenter les algorithmes probabilistes, amène à l'utilisation d'un \emph{flot} de données aléatoires, toutes de même type $E$ et suivant la même loi de probabilité. Un tirage sera donc assimilé à la \emph{consommation} d'un élément de ce flot. \begin{defin}[Flot de données aléatoires ; extraction] Soit $E$ un ensemble quelconque non vide. On appelle flot sur $E$ toute famille $\varphi \in E ^ \mathbb N$. Si $\alpha \in E$ et si $\varphi$ est un flot sur $E$, alors on note $\alpha :: \varphi$ le flot tel que : \begin{displaymath} \left(\alpha :: \varphi\right)_0 = \alpha \end{displaymath} \begin{displaymath} \forall n \in \mathbb N : \left(\alpha :: \varphi\right)_{n + 1} = \varphi_n \end{displaymath} On appelle fonction extractrice la fonction \begin{displaymath} \begin{array}{lllll} Extr & : & E^\mathbb N & \rightarrow & E \times E^\mathbb N \\ & & \alpha :: \varphi & \mapsto & \left(\alpha, \varphi\right) \end{array} \end{displaymath} L'application de cette fonction est l'extraction, ou la consommation, d'un élément de flot. Alors, un flot $\varphi'$ est une queue (ou un sous-flot) du flot $\varphi$ si, et seulement si, il est la partie droite ($\pi_2$) d'un nombre fini d'extractions de $\varphi$ : \begin{displaymath} \exists n \in \mathbb N : \varphi' = \left(\pi_2 \circ Extr\right) ^ n \left(\varphi\right) \end{displaymath} \end{defin} L'algorithme probabiliste sera modélisé par une fonction déterministe qui prendra en entrée un flot de données aléatoires, et qui renverra la donnée «utile» (celle qu'on veut effectivement obtenir et manipuler) et le reste du flot non consommé. \begin{defin}[Algorithme probabiliste] Soit $F$ un ensemble non vide. On appelle algorithme probabiliste calculant une donnée de l'ensemble $F$ toute fonction déterministe : \begin{displaymath} f : ~ E^\mathbb N ~ \rightarrow ~ F \times E^\mathbb N \end{displaymath} telle que pour tous flots $\varphi, \varphi'$ et pour tout $y \in F$, si $f(\varphi) = \left(y, \varphi'\right)$, alors $\varphi'$ est une queue de $\varphi$. \end{defin} Cette définition, toutefois, ne permet pas de garantir que la fonction $f$ extrait tous les éléments du flot qu'elle utilise. Considérons, par exemple, $E = \left\{ \top, \bot \right\}$, et soit l'algorithme probabiliste $f$ suivant, calculant une donnée de l'ensemble des entiers naturels : \begin{displaymath} \begin{array}{rcl} f(\varphi) & = & \left(f_1(\varphi), f_2(\varphi)\right) \\ f_1\left(\top :: \varphi'\right) & = & 0 \\ f_2\left(\top :: \varphi'\right) & = & \top :: \varphi' \\ f_1\left(\bot :: \varphi'\right) & = & f_1(\varphi') + 1 \\ f_2\left(\bot :: \varphi'\right) & = & \bot :: f_2(\varphi') \\ \end{array} \end{displaymath} Cette fonction calcule le nombre de $\bot$ en tête de flot, et les extrait, mais utilise le premier $\top$ rencontré dans le flot, sans l'extraire. Comme nous allons le voir, une telle opération est impossible dans le langage que j'ai choisi pour la représentation des algorithmes probabilistes. Mais il est difficile d'exprimer mathématiquement le fait qu'un algorithme consomme tous les éléments de flot qu'il utilise, sans avoir à parler d'une telle représentation dans un langage. Une approche possible est de dire qu'une telle fonction est «préfixe», c'est-à-dire que pour tous $\alpha_1, \dots, \alpha_n, \varphi'$, si sous une telle fonction le flot d'entrée $\alpha_1 :: \dots :: \alpha_n :: \varphi'$ donne le flot de sortie $\varphi'$, alors pour tout $\varphi''$, le flot d'entrée $\alpha_1 :: \dots :: \alpha_n :: \varphi''$ donne le flot de sortie $\varphi''$, ce qui exprime le fait que les données des queues $\varphi'$ et $\varphi''$ des flots d'entrée ne soient pas utilisées. \subsection{Le langage \lo} Pour la représentation des algorithmes probabilistes, j'ai préféré utiliser un langage fonctionnel : le langage \emph{Lambda-O}, ou \lo, mis au point par Park, Pfenning et Thrun en 2005 \cite{lo}\footnote{Je ne considère ici que la première définition du langage, c'est-à-dire sans prendre en compte les extensions pour le calcul approché.}, et qui a été présenté au \emph{POPL'05}. Le \lo était initialement destiné à étendre le langage OCaml \cite{ocaml} pour des applications comme la localisation d'un robot. ~ Certes, les algorithmes probabilistes sont le plus souvent représentés dans des langages impératifs, mais justement, j'ai préféré me placer dans le modèle fonctionnel pour sortir des sentiers battus et aborder ainsi une approche assez rare des algorithmes probabilistes. ~ Le langage \lo est fondé sur une nouvelle approche \emph{monadique} des langages fonctionnels, introduite par Park et Pfenning. Cette approche monadique consiste à distinguer deux constructions du langage : \begin{itemize} \item les \emph{termes}, dont la réduction est appelée \emph{évaluation} et n'utilise en rien la monade. \item les \emph{expressions} dont la réduction est appelée \emph{calcul} et peut utiliser la monade. \end{itemize} ~ Le langage \lo est un des produits de cette approche. Du point de vue probabiliste, les constructions de termes et d'expressions jouent les rôles suivants : \begin{itemize} \item les \emph{termes}, dont le résultat est déterministe quel que soit le flot, qui n'est pas consommé par l'évaluation. \item les \emph{expressions}, dont le résultat est rendu aléatoire par le fait que le calcul consomme au besoin des éléments du flot : il s'agit en fait de la représentation de \emph{variables aléatoires}. \end{itemize} ~ Le langage \lo a fait l'objet d'une implémentation par les auteurs. De mon côté, j'ai également écrit, en OCaml, un petit interpréteur (avec parseur et \emph{type-checker}) qui m'a servi de plate-forme d'expérimentation, mais m'a également servi de base pour la suite de mes travaux. Je l'ai baptisé \emph{Proba Caml}\footnote{Ou encore ALICE, pour «\textbf{Al}ea-\textbf{I}ncluding \textbf{C}omputations and \textbf{E}valuations», «calculs et évaluations avec aléa». -- Sources et mise en \oe uvre sur une machine : cf. annexe p. \pageref{src}}. ~ Parmi les termes, outre les constructions classiques d'un $\lambda$-calcul typé simple, le \lo permet de représenter des distributions de probabilités (structure $\mathsf{prob}$) comme \emph{mesure-image} de la mesure sur l'espace de probabilité des flots par la variable . Ce sont les expressions qui permettent d'extraire des échantillons des distributions de probabilités (structure $\mathsf{sample}$). \begin{defin}[Ensemble de base, valeur de base] Fixons une fois pour toutes un ensemble $T_0$ d'ensembles dits «de base». On appelle alors valeur de base tout élément $v \in \tau$ où $\tau \in T_0$ est un ensemble de base. \end{defin} Dans \emph{Proba Caml}, j'ai implémenté les valeurs de base des entiers naturels et des réels. \begin{defin}[Termes et expressions] Soit $\mathcal V$ un ensemble non vide de noms de variables. Alors, l'ensemble $Term$ des termes du \lo et l'ensemble $Expr$ des expressions du \lo sont définis par les grammaires suivantes : \begin{displaymath} \begin{array}{llllll} Term & ::= & | & \mathsf{true} & & \text{booléens} \\ & & | & \mathsf{false} \\ & & | & \mathsf{if} ~ a ~ \mathsf{then} ~ b ~ \mathsf{else} ~ c & (a, b, c \in Term) & \text{test} \\ \\ & & | & v & (v \in \tau, ~ \tau \in T_0) & \text{valeur de base} \\ & & | & x & (x \in \mathcal V) & \text{variable} \\ \\ & & | & (a, b) & (a, b \in Term) & \text{couple} \\ & & | & \mathsf{fst} ~ a & (a \in Term) & \text{projection gauche} \\ & & | & \mathsf{snd} ~ a & (a \in Term) & \text{projection droite} \\ \\ & & | & \lambda x. ~ c & (x \in \mathcal V, ~ c \in Term) & \text{abstraction} \\ & & | & a ~ b & (a, b \in Term) & \text{application} \\ \\ & & | & \mathsf{prob} ~ e & (e \in Expr) & \text{distribution de} \\ & & & & & \text{probabilité} \\ \\ & & | & \mathsf{fix} ~ x. ~ a & (x \in \mathcal V, ~ a \in Term) & \text{terme récursif} \\ \\ \\ Expr & ::= & | & a & (a \in Term) & \text{terme (déterministe)} \\ & & | & \mathcal S & & \text{extraction d'un} \\ & & & & & \text{élément du flot} \\ & & | & \mathsf{sample} ~ x ~ \mathsf{from} ~ a ~ \mathsf{in} ~ e & (x \in \mathcal V, ~ a \in Term, ~ e \in Expr) & \text{échantillonnage d'une} \\ & & & & & \text{distribution} \\ \end{array} \end{displaymath} \end{defin} Dans cette définition, les valeurs booléennes sont particularisées à cause du test $\mathsf{if}$, qui exige explicitement leur présence. ~ On distingue deux types de réduction : l'\emph{évaluation} (réduction des termes, n'utilisant pas le flot) et le \emph{calcul} (réduction des expressions, pouvant utiliser le flot). La réduction d'un terme ou expression doit aboutir à un terme appelé \emph{valeur} au sens de la : \begin{defin}[Valeur] L'ensemble $Val$ des valeurs est un sous-ensemble de l'ensemble $Term$ des termes. Cet ensemble est défini par la grammaire suivante : \begin{displaymath} \begin{array}{llllll} Val & ::= & | & \mathsf{true} & & \text{booléens} \\ & & | & \mathsf{false} \\ & & | & v & (v \in \tau, ~ \tau \in T_0) & \text{valeur de base} \\ & & | & \lambda x. ~ c & (x \in \mathcal V, ~ c \in Term) & \text{abstraction} \\ & & | & \mathsf{prob} ~ e & (e \in Expr) & \text{distribution de probabilité} \\ & & | & (a, b) & (a, b \in Val) & \text{couple de valeurs} \\ \end{array} \end{displaymath} \end{defin} On présente ici les règles de réduction en un pas : la sémantique proposée est une sémantique de réduction \emph{à petits pas}. On notera $\mapsto$ un pas d'évaluation, $\Rightarrow$ un pas de calcul, et $\mapsto^* , \Rightarrow^* $ les clôtures réflexives et transitives correspondantes. \subsubsection{Evaluation des termes} Les termes sont évalués selon le principe de l'appel \emph{par valeur}. Le flot n'intervient pas : la relation $\mapsto$ est donc simplement une relation entre termes. ~ \textbf{Test :} le booléen est évalué d'abord. Lorsque l'on tombe sur une valeur booléenne, on peut alors effectuer le branchement. \begin{displaymath} \frac{a \mapsto a'}{\mathsf{if} ~ a ~ \mathsf{then} ~ b ~ \mathsf{else} ~ c ~ ~ \mapsto ~ ~ \mathsf{if} ~ a' ~ \mathsf{then} ~ b ~ \mathsf{else} ~ c} ~ ~ ~ \frac{}{\mathsf{if} ~ \mathsf{true} ~ \mathsf{then} ~ b ~ \mathsf{else} ~ c ~ ~ \mapsto b} ~ ~ ~ \frac{}{\mathsf{if} ~ \mathsf{false} ~ \mathsf{then} ~ b ~ \mathsf{else} ~ c ~ ~ \mapsto c} \end{displaymath} ~ \textbf{Couple :} le membre gauche est évalué d'abord. \begin{displaymath} \frac{a \mapsto a'}{(a, b) \mapsto (a', b)} ~ ~ ~ \frac{v \in Val ~ ~ b \mapsto b'}{(v, b) \mapsto (v, b')} \end{displaymath} ~ \textbf{Projections :} elles ne sont évaluées qu'une fois que les deux membres du couple l'ont été. \begin{displaymath} \frac{c \mapsto c'}{\mathsf{fst} ~ c ~ ~ \mapsto ~ ~ \mathsf{fst} ~ c'} ~ ~ ~ \frac{c \mapsto c'}{\mathsf{snd} ~ c ~ ~ \mapsto ~ ~ \mathsf{snd} ~ c'} ~ ~ ~ \frac{v_g, v_d \in Val ~ ~}{\mathsf{fst} ~ (v_g, v_d) ~ ~ \mapsto v_g} ~ ~ ~ \frac{v_g, v_d \in Val ~ ~}{\mathsf{snd} ~ (v_g, v_d) ~ ~ \mapsto v_d} \end{displaymath} ~ \textbf{Application :} c'est la règle d'\emph{élimination} de l'abstraction. La fonction est évaluée d'abord. Puis l'argument est évalué, avant que n'intervienne la $\beta$-réduction. \begin{displaymath} \frac{a \mapsto a'}{a ~ b ~ ~ \mapsto ~ ~ a' ~ b} ~ ~ ~ \frac{b \mapsto b'}{\left(\lambda x. ~ c \right) ~ b ~ ~ \mapsto ~ ~ \left(\lambda x. ~ c \right) ~ b'} ~ ~ ~ \frac{v \in Val}{\left( \lambda x. ~ c \right) ~ v ~ ~ \mapsto c \left[ x := v \right] } \end{displaymath} où la substitution est définie de manière évidente (moyennant les $\alpha$-renommages). On voit ici que la $\beta$-réduction n'apparaît que lorsque l'argument est une valeur. C'est dire que les termes suivent un schéma d'évaluation en appel par valeur. ~ \textbf{Point fixe :} un dépliage («unfold»). \begin{displaymath} \frac{}{\mathsf{fix} ~ x. ~ a ~ ~ \mapsto a \left[ x ~ := ~ \mathsf{fix} ~ x. ~ a \right]} \end{displaymath} ~ On montre facilement qu'à partir d'un terme $a$ il existe au plus un terme $a'$ tel que $a \mapsto a'$. On montre alors, par induction sur la structure du terme, qu'entre un terme et une valeur, il existe au plus un chemin d'évaluation. \subsubsection{Calcul des expressions} Ici, le flot intervient. La relation $\Rightarrow$ est donc une relation entre les couples expression-flot, on écrira $e ~ @ ~ s ~ ~ \Rightarrow ~ ~ e' ~ @ ~ s'$. ~ \textbf{Terme en tant qu'expression :} le calcul d'un terme correspond à son évaluation, sans consommer le flot. \begin{displaymath} \frac{a \mapsto a'}{a ~ @ ~ s ~ ~ \Rightarrow ~ ~ a' ~ @ ~ s} \end{displaymath} ~ \textbf{Consommation d'un élément du flot.} \begin{displaymath} \frac{}{\mathcal S ~ @ ~ x :: t ~ ~ \Rightarrow ~ ~ x ~ @ ~ t} \end{displaymath} ~ \textbf{Echantillonnage :} c'est la règle correspondant à l'\emph{élimination} du terme $\mathsf{prob}$. On évalue d'abord le terme correspondant à la distribution de probabilité. Puis, lorsqu'on tombe sur une valeur $\mathsf{prob}$, on évalue son «expression-corps», en modifiant au besoin le flot, jusqu'à tomber sur une valeur que l'on substitue à la variable d'échantillonnage, en renvoyant le nouveau flot. \begin{displaymath} \frac{a \mapsto a'}{\mathsf{sample} ~ x ~ \mathsf{from} ~ a ~ \mathsf{in} ~ e ~ ~ @ ~ s ~ ~ \Rightarrow ~ ~ \mathsf{sample} ~ x ~ \mathsf{from} ~ a' ~ \mathsf{in} ~ e ~ ~ @ ~ s} \end{displaymath} \begin{displaymath} \frac{e_x ~ @ ~ s ~ ~ \Rightarrow ~ ~ e_x' ~ @ ~ s'}{\mathsf{sample} ~ x ~ \mathsf{from} ~ \mathsf{prob} ~ e_x ~ \mathsf{in} ~ e ~ ~ @ ~ s ~ ~ \Rightarrow ~ ~ \mathsf{sample} ~ x ~ \mathsf{from} ~ \mathsf{prob} ~ e_x' ~ \mathsf{in} ~ e ~ ~ @ ~ s'} \end{displaymath} \begin{displaymath} \frac{v \in Val}{\mathsf{sample} ~ x ~ \mathsf{from} ~ \mathsf{prob} ~ v ~ \mathsf{in} ~ e ~ ~ @ ~ s' ~ ~ \Rightarrow ~ ~ e \left[ x := v \right] ~ @ ~ s' } \end{displaymath} ~ Ici encore, on montre qu'à flot fixé $s$, à partir d'une expression $e$ il existe au plus une expression $e'$ et un flot $s'$ tels que $e ~ @ ~ s ~ ~ \Rightarrow ~ ~ e' ~ @ ~ s'$. Donc, à flot fixé, entre une expression et une valeur, il existe au plus un chemin de calcul. On montre facilement, par induction sur la structure de l'expression, que le flot résultant est un sous-flot du flot d'entrée et que seuls sont utilisés les éléments extraits. ~ En $\lambda$-calcul la pierre angulaire de l'évaluation est la $\beta$-réduction. En fait, on constate qu'en \lo elle intervient à deux niveaux : à côté de la $\beta$-réduction classique sur les termes, on peut considérer que les règles de calcul du $\mathsf{sample}$ constituent une $\beta$-réduction au niveau des expressions, où le $\mathsf{sample}$ joue le rôle d'application et le $\mathsf{prob}$ joue le rôle d'abstraction. En somme, comme les règles de l'application correspondent à l'\emph{élimination} de l'abstraction, celles du $\mathsf{sample}$ correspondent à l'élimination du terme $\mathsf{prob}$. Cf.~fig.~\ref{fig-beta} p.~\pageref{fig-beta}. \begin{figure}[ht] \begin{center} \mbox{ \begin{math} \begin{array}{l@{\extracolsep{8mm}}c@{\extracolsep{8mm}}c} & \textbf{Termes} & \textbf{Expressions} \\ \\ \hline \\ \text{\textbf{Abstraction} (terme)} & \lambda x. ~ c ~ & \mathsf{prob} ~ c \\ \text{Corps } c & \text{Terme} & \text{\emph{Expression}} \\ \\ \hline \\ \text{\textbf{Application} «} f(a) \text{»} & f ~ a & \mathsf{sample} ~ y ~ \mathsf{from} ~ f ~ \mathsf{in} ~ e \\ \text{Argument} & \text{Explicite : terme } a & \text{Implicite : flot} \\ \text{Nature de l'application} & \text{Terme} & \text{\emph{Expression}} \\ \text{Résultat} & \text{Valeur renvoyée} & \text{Valeur utilisée dans } e \text{ sous la variable } y \\ & & \text{Flot de sortie passé en entrée de } e \\ \\ \hline \\ \textbf{$\beta$-réduction} & f[x := a] & \text{Calcul du corps de la } \mathsf{prob} \\ & & \text{ sous le flot d'entrée du } \mathsf{sample} \\ \\ \end{array} \end{math}} \caption{Les deux niveaux de $\beta$-réduction en \lo} \label{fig-beta} \end{center} \end{figure} \subsubsection{Exemple de réduction} Soit l'expression suivante : ~ $\mathsf{sample} ~ x ~ \mathsf{from} ~ \mathsf{prob} ~ \mathcal S ~ \mathsf{in}$ \\ \verb+ + $\mathsf{sample} ~ y ~ \mathsf{from}$ \\ \verb+ + $\mathsf{if} ~ x > 18 ~ \mathsf{then} ~ \mathsf{prob} ~ 0 ~ \mathsf{else} ~ \mathsf{prob} ~ \mathcal S$ \\ \verb+ + $\mathsf{in} ~ x + y$ ~ (On suppose que le type $\tau_0$ des éléments de flot est le type des entiers naturels.) Etudions cet exemple sous le flot d'entrée $15 :: 1500 :: 18 :: \varphi'$ (avec $\varphi'$ quelconque mais fixé). \begin{enumerate} \item L'expression est un $\mathsf{sample}$, évaluons le terme introduit par $\mathsf{from}$ : c'est $\mathsf{prob} ~ \mathcal S$. Comme c'est un terme $\mathsf{prob}$, calculons son expression-corps, qui est $\mathcal S$ : extraction de flot. On obtient alors l'expression suivante : ~ $\mathsf{sample} ~ x ~ \mathsf{from} ~ \mathsf{prob} ~ 15 ~ \mathsf{in}$ \\ \verb+ + $\mathsf{sample} ~ y ~ \mathsf{from}$ \\ \verb+ + $\mathsf{if} ~ x > 18 ~ \mathsf{then} ~ \mathsf{prob} ~ 0 ~ \mathsf{else} ~ \mathsf{prob} ~ \mathcal S$ \\ \verb+ + $\mathsf{in} ~ x + y$ ~ et le flot est maintenant $1500 :: 18 :: \varphi'$. ~ \item L'expression-corps est $15$, c'est donc une valeur que l'on peut substituer à $x$ dans l'expression introduite par $\mathsf{in}$. On obtient l'expression suivante : ~ ~ $\mathsf{sample} ~ y ~ \mathsf{from}$ \\ \verb+ + $\mathsf{if} ~ 15 > 18 ~ \mathsf{then} ~ \mathsf{prob} ~ 0 ~ \mathsf{else} ~ \mathsf{prob} ~ \mathcal S$ \\ $\mathsf{in} ~ 15 + y$ ~ et le flot est toujours $1500 :: 18 :: \varphi'$. ~ \item L'expression est un $\mathsf{sample}$ : évaluons le terme introduit par $\mathsf{from}$. C'est un terme $\mathsf{if}$ : évaluons le booléen, $15 > 18$. Considérant qu'il s'agit d'un opérateur de base, et que $15$ et $18$ sont deux valeurs, ne faisons pas de détail sur la façon dont il est évalué, et disons directement que le booléen obtenu est $\mathsf{false}$ : ~ $\mathsf{sample} ~ y ~ \mathsf{from}$ \\ \verb+ + $\mathsf{if} ~ \mathsf{false} ~ \mathsf{then} ~ \mathsf{prob} ~ 0 ~ \mathsf{else} ~ \mathsf{prob} ~ \mathcal S$ \\ $\mathsf{in} ~ 15 + y$ ~ Comme on est en train d'évaluer un terme, le flot est inchangé. ~ \item On peut maintenant effectuer le branchement : ~ $\mathsf{sample} ~ y ~ \mathsf{from} ~ \mathsf{prob} ~ \mathcal S ~ \mathsf{in} ~ 15 + y$ ~ \item C'est donc un terme $\mathsf{prob}$ dont on va pouvoir calculer l'expression-corps, qui une nouvelle fois est une extraction de flot . On obtient donc : ~ $\mathsf{sample} ~ y ~ \mathsf{from} ~ \mathsf{prob} ~ 1500 ~ \mathsf{in} ~ 15 + y$ ~ et le nouveau flot est $18 :: \varphi'$. \item Maintenant, l'expression sous le $\mathsf{prob}$ est une valeur que l'on peut substituer à $y$ dans l'expression $15 + y$ : ~ $15 + 1500$ ~ \item C'est désormais un terme. Les deux arguments du $+$ étant des valeurs, là encore, pas de détail. On obtient donc finalement : ~ $1515$ ~ et le flot de sortie est $18 :: \varphi'$. \end{enumerate} Il y a donc eu deux consommations. Notons que si le flot d'entrée avait été $1500 :: 15 :: 18 :: \varphi'$, alors on aurait obtenu le résultat $1500$ et le flot de sortie $15 :: 18 :: \varphi'$ après une seule consommation. \subsubsection{Typage} Le \lo est simplement typé. Mais on distinguera deux notations pour le typage des termes et celui des expressions : \begin{itemize} \item $a : t$ indique que le terme $a$ est déterministe dans le type $t$ \item on écrira plutôt $e \div t$ pour dire que l'expression $e$ est une \emph{variable aléatoire} sur le type $t$. \end{itemize} \begin{defin}[Types] On confond un type de base et l'ensemble de base $\tau \in T_0$ auquel il correspond. L'ensemble $Ty$ des types du \lo sur les types de base $T_0$ est défini par la grammaire suivante : \begin{displaymath} \begin{array}{lllll} Ty & ::= & | & \mathsf{bool} \\ & & | & \tau & (\tau \in T_0) \\ & & | & t_1 \rightarrow t_2 & (t_1, t_2 \in Ty) \\ & & | & t_1 \times t_2 & (t_1, t_2 \in Ty) \\ & & | & \bigcirc ~ t & (t \in Ty) \\ \end{array} \end{displaymath} \end{defin} Dans cette définition des types, le type $\mathsf{bool}$ est particularisé car, comme on l'a vu, le terme de test $\mathsf{if}$ exige la présence explicite des booléens. ~ Soit $\Gamma$ un \emph{contexte de typage} : une partie de $\mathcal V \times Ty$, associant un type à chaque variable du contexte. \textbf{Attention :} le typage est \emph{déterministe}\footnote{On pourrait le rendre en quelque sorte «probabiliste» en autorisant les types somme ; mais au lieu de parler de «probabilité que le résultat soit d'un certain type», on parlerait plutôt de «probabilité que le résultat commence par un certain constructeur de type somme», le type somme étant déterminé par les règles de typage, qui restent tout à fait déterministes.}. ~ \textbf{Typage des termes.} Booléens et test : introduction et élimination du type $\mathsf{bool}$. \begin{displaymath} \frac{}{\Gamma \vdash \mathsf{true} : \mathsf{bool}} ~ ~ ~ \frac{}{\Gamma \vdash \mathsf{false} : \mathsf{bool}} ~ ~ ~ \frac{\Gamma \vdash a : \mathsf{bool} ~ ~ \Gamma \vdash b : t ~ ~ \Gamma \vdash c : t}{\Gamma \vdash \mathsf{if} ~ a ~ \mathsf{then} ~ b ~ \mathsf{else} ~ c ~ : t} \end{displaymath} ~ Valeur de base et variable : \begin{displaymath} \frac{\tau \in T_0 ~ ~ ~ v \in \tau}{\Gamma \vdash v : \tau} ~ ~ ~ \frac{(x, t) \in \Gamma}{\Gamma \vdash x : t} \end{displaymath} ~ Couple et projections : introduction et élimination du type couple $\times$. \begin{displaymath} \frac{\Gamma \vdash a : t_a ~ ~ \Gamma \vdash b : t_b}{\Gamma \vdash (a, b) : t_a \times t_b} ~ ~ ~ \frac{\Gamma \vdash c : t_g \times t_d}{\Gamma \vdash \mathsf{fst} ~ c ~ : t_g} ~ ~ ~ \frac{\Gamma \vdash c : t_g \times t_d}{\Gamma \vdash \mathsf{snd} ~ c ~ : t_d} \end{displaymath} ~ Abstraction et application : introduction et élimination du type flèche $\rightarrow$. \begin{displaymath} \frac{\Gamma \cup \left\{ (x, t_x) \right\} \vdash c : t_c}{\Gamma \vdash \lambda x : t_x. ~ c ~ : t_x \rightarrow t_c} ~ ~ ~ \frac{\Gamma \vdash a : t_b \rightarrow t ~ ~ \Gamma \vdash b : t_b}{\Gamma \vdash a ~ b ~ : t} \end{displaymath} ~ Distribution de probabilité : introduction du type $\bigcirc$. \begin{displaymath} \frac{\Gamma \vdash e \div t}{\Gamma \vdash \mathsf{prob} ~ e ~ : \bigcirc ~ t} \end{displaymath} ~ Point fixe : \begin{displaymath} \frac{\Gamma \cup \left\{ (x, t) \right\} \vdash a : t}{\Gamma \vdash \mathsf{fix} ~ x : t. ~ a ~ : t} \end{displaymath} ~ \textbf{Typage des expressions.} On considère que les éléments du flot sont d'un type $\tau_0 \in T_0 \cup \left\{ \mathsf{bool} \right\} $ fixé. Terme en tant qu'expression : \begin{displaymath} \frac{\Gamma \vdash a : t}{\Gamma \vdash a \div t} \end{displaymath} ~ Extraction d'un élément du flot : \begin{displaymath} \frac{}{\Gamma \vdash \mathcal S \div \tau_0} \end{displaymath} ~ Echantillonnage d'une distribution de probabilité : élimination du type $\bigcirc$. \begin{displaymath} \frac{\Gamma \vdash a : \bigcirc ~ t_x ~ ~ \Gamma \cup \left\{ (x, t_x) \right\} \vdash e \div t}{\Gamma \vdash \mathsf{sample} ~ x ~ \mathsf{from} ~ a ~ \mathsf{in} ~ e ~ \div t} \end{displaymath} ~ On montre facilement, par induction sur la structure de la relation de réduction correspondante, que l'évaluation et le calcul conservent le type. On montre également que si un terme (resp. une expression) s'évalue (resp. se calcule) en une valeur, alors il (resp. elle) est bien typé(e) (et bien entendu son type correspond à celui de la valeur obtenue). \subsection{Représentation d'un algorithme en \lo} Un algorithme, déterministe ou probabiliste, peut être modélisé par un terme du \lo. ~ Si l'algorithme a besoin d'un certain nombre de \emph{paramètres déterministes}, alors on les déclare au moyen d'\emph{abstractions} ; lors de la mise en \oe uvre de l'algorithme, on fournira ces paramètres au moyen d'\emph{applications}. Dans un premier temps, donc, l'algorithme est évalué de façon \emph{déterministe}, sans utiliser le flot. Evaluons donc un tel terme de mise en \oe uvre de l'algorithme, et regardons la valeur obtenue. ~ \begin{itemize} \item Abstraction : cela signifie que l'on n'a pas donné tous les paramètres déterministes dont l'algorithme a besoin pour tourner. \item Valeur de type de base : l'algorithme a tourné et la valeur retournée est déterministe, ne dépend pas du flot. \item Structure $\mathsf{prob}$ : il s'agit d'un \emph{algorithme probabiliste}, qu'il faut mettre en \oe uvre au moyen d'une \emph{expression}. \end{itemize} ~ Prenons par exemple le terme suivant, qui modélise l'algorithme de simulation de la loi de Bernoulli de paramètre $p$ donné de façon déterministe lors de sa mise en \oe uvre (en supposant que les flots soient des «suites de variables aléatoires réelles uniformément distribuées sur $[0, 1]$») : \begin{displaymath} \text{bernoulli} ~ := ~ \lambda p. ~ \mathsf{prob} ~ \mathsf{sample} ~ x ~ \mathsf{from} ~ \mathsf{prob} ~ \mathcal S ~ \mathsf{in} ~ x \le p \end{displaymath} L'instanciation se fera donc en deux coups : d'abord un terme d'application pour renseigner le paramètre déterministe $p$, puis une expression $\mathsf{sample}$ pour mettre en \oe uvre effectivement l'algorithme probabiliste. Le tout est donc réalisé par l'expression suivante (étant donné un réel $p_1$) : \begin{displaymath} \mathsf{sample} ~ x ~ \mathsf{from} ~ \text{bernoulli} ~ p_1 ~ \mathsf{in} ~ x \end{displaymath} Conformément aux règles de calcul, le terme introduit par $\mathsf{from}$ est évalué en premier : ici, cela correspond à la donnée, par application, du paramètre déterministe $p_1$. On obtient une valeur $\mathsf{prob}$, qui permet enfin le calcul proprement dit de l'expression correspondant à l'algorithme probabiliste instancié. \clearpage \section{Mécanisation du raisonnement sur des algorithmes probabilistes}\label{s-2} Etant donné un algorithme probabiliste, sous la forme d'un terme du \lo (que l'on appellera \emph{programme}), on veut énoncer et prouver des propriétés sur l'algorithme en considérant le comportement du terme une fois instancié. Par exemple, pour reprendre l'exemple de la loi de Bernoulli : \begin{displaymath} \lambda p. ~ \mathsf{prob} ~ \mathsf{sample} ~ x ~ \mathsf{from} ~ \mathsf{prob} ~ \mathcal S ~ \mathsf{in} ~ x \leqslant p \end{displaymath} on veut pouvoir prouver que si l'algorithme est instancié avec un paramètre $p \in \left[0, 1\right]$, alors le terme $\mathsf{prob}$ représente un algorithme de simulation de la loi de Bernoulli de paramètre $p$. \subsection{Formules associées à un programme : le transformateur $\Pi$} L'idée est d'associer à un programme une formule logique qui décrive son comportement, afin de pouvoir raisonner directement en Coq avec cette formule. Ces formules, décrivant comment le programme s'évalue ou se calcule et utilise le flot, sont toutes \emph{déterministes}. L'aspect probabiliste vient plus tard, dans le raisonnement sur la formule générée en considérant des probabilités sur le flot d'entrée (dont seule l'utilisation «brute» par le programme est exprimée par la formule générée). ~ Je construis la formule par \emph{induction sur la structure} du terme ou de l'expression, et suivant la \emph{sémantique opérationnelle} du \lo. ~ Le procédé que j'ai choisi est analogue à celui du typage : c'est d'ailleurs en modifiant la procédure de typage de mon interpréteur \emph{Proba Caml} que j'ai écrit, toujours en OCaml \cite{ocaml}, le programme de génération de la formule Coq à partir du code \lo donné en entrée, programme que j'ai appelé «transformateur $\Pi$» (car, par exemple, pour un terme $m$, je désigne par $\Pi_m$ la «\textbf{p}ropriété vérifiée par le résultat de l'évaluation du terme $m$»). ~ En toute rigueur, pour chaque élément de langage, terme ou expression, on doit disposer d'informations non seulement sur sa correction, mais aussi sur sa terminaison. Ce sont donc deux formules qu'il faut générer. ~ Supposons que l'on se place dans un contexte de variables $\Gamma$. Soient $e$ une expression et $P$ et $Q$ deux formules. Alors, lorsque l'on écrit le \emph{jugement} suivant : \begin{displaymath} \Gamma ~ \vdash ~ \left\{ P \right\} ~ e ~ \left\{ Q \right\} \end{displaymath} on dit en fait que $P$ est une \emph{condition suffisante de terminaison} et $Q$ est une \emph{propriété de correction} vérifiée par le résultat et le flot de sortie \emph{sous l'hypothèse que le programme termine}. Un tel jugement se lit : «si $P$ est vérifiée, alors le calcul de $e$ termine et $Q$ est vérifiée». ~ \textbf{Remarque : } l'espace des variables libres de $P$ est $\Gamma \cup \left\{ \sigma \right\}$, où $\sigma$ désigne le flot d'entrée, tandis que l'espace des variables libres de $Q$ est $\Gamma \cup \left\{ \sigma, \_, \sigma' \right\}$, où $\sigma'$ désigne le flot de sortie et $\_$ le résultat du calcul de $e$. Si $e$ est un terme, alors $P$ et $Q$ ne dépendent ni de $\sigma$, ni de $\sigma'$. \emph{Dans toute la suite, nous utiliserons ces conventions de notation pour désigner le flot d'entrée, la valeur résultat et le flot de sortie du calcul d'une expression}. \subsubsection{Formules spéciales : présentation informelle} Ce qu'il ne fallait surtout pas faire, c'est d'autoriser l'apparition de termes et d'expressions tels quels dans les formules générées. En effet, ces formules sont destinées à être utilisées dans Coq et le calcul des constructions inductives. Traduire directement les termes en autorisant par exemple l'apparition de l'application nécessiterait en fait que j'adopte les règles de réduction de Coq lui-même sur les termes. Or, je souhaite raisonner \emph{uniquement dans la logique d'ordre supérieur} sur les formules, et en particulier exprimer dans la logique la réduction elle-même. ~ Il a donc fallu créer des formules spéciales pour le couple, l'application et le $\mathsf{sample}$. Ces formules permettent une approche \emph{relationnelle} des structures du langage \lo, à la manière de ce que l'on peut faire en PROLOG. ~ De façon informelle, le langage des formules sera engendré par les formules <<élémentaires>> suivantes : ~ \begin{itemize} \item pour un couple $(a, b)$, on introduit la relation notée : \begin{displaymath} a \xrightleftharpoons[\otimes] \_ b \end{displaymath} qui exprime que le résultat $\_$ de l'évaluation de ce terme est un couple dont la partie gauche (resp. droite) est le résultat de l'évaluation de $a$ (resp. $b$). ~ \item pour une application $f ~ a$, on introduit la relation notée : \begin{displaymath} a \xrightarrow[\triangleright] f \_ \end{displaymath} qui exprime que le résultat $\_$ de l'évaluation de ce terme est le résultat de l'application de $f$ à $a$. \\ \item pour un $\mathsf{sample} ~ x ~ \mathsf{from} ~ m ~ \mathsf{in} ~ e$, on introduit la relation notée : \begin{displaymath} s \xrightarrow[\square] m \langle x, s' \rangle \end{displaymath} qui exprime que l'évaluation de $m$ donne un terme $\mathsf{prob}$ et que le calcul de l'expression-corps de ce $\mathsf{prob}$ sous le flot d'entrée $s$ donne une valeur $x$ et un flot de sortie $s'$ (qui sera passé en entrée au calcul de $e$). \end{itemize} ~ Bien entendu, il s'agit ici d'une présentation informelle, et dans la pratique, les termes et expressions apparaissant dans les relations seront remplacés par des variables ou des valeurs de base (ou plus généralement des «termes de logique» obtenus à partir de variables et valeurs de base par des opérations de base fixées une fois pour toutes, par exemple l'addition sur les réels). \subsubsection{Formules spéciales : première définition} \label{s-pi-light} Je présente ici de manière plus ou moins formelle le mécanisme que j'ai adopté et employé pour les formules de correction, mécanisme adapté aux programmes ne contenant pas de point fixe. ~ Voici le mécanisme d'\emph{introduction} des flèches $\xrightleftharpoons[\otimes]{}$, $\xrightarrow[\triangleright]{}$ et $\xrightarrow[\square]{}$. ~ \begin{itemize} \item pour les projections $\mathsf{fst} ~ c$ et $\mathsf{snd} ~ c$, que nous noterons $a$ et $b$, on génère la formule $\Pi_c(\_)$ correspondant à $c$ et dépendant du résultat $\_$ de son évaluation, et alors on obtient : \begin{displaymath} \Pi_a(\_) ~ := ~ \exists c', \exists b : ~ \_ \xrightleftharpoons[\otimes] {c'} b ~ \land ~ \Pi_c(c') \end{displaymath} \begin{displaymath} \Pi_b(\_) ~ := ~ \exists c', \exists a : ~ a \xrightleftharpoons[\otimes] {c'} \_ ~ \land ~ \Pi_c(c') \end{displaymath} \\ \item pour une application $f ~ a$, que nous noterons $y$, on génère les formules $\Pi_f(\_)$ et $\Pi_a(\_)$ correspondant aux formules vérifiées par $f$ et par $a$, dépendant chacune du résultat $\_$ de leur évaluation, et alors on obtient pour $y$ : \begin{displaymath} \Pi_y(\_) ~ := ~ \exists f', \exists a' : ~ \Pi_f(f') ~ \land ~ \Pi_a(a') ~ \land ~ a' \xrightarrow[\triangleright] {f'} \_ \end{displaymath} \\ \item pour une expression $\mathsf{sample} ~ x ~ \mathsf{from} ~ m ~ \mathsf{in} ~ e$, que nous noterons $g$, on génère les formules $\Pi_m(\_)$, correspondant à $m$ et dépendant du résultat $\_$ de l'évaluation de $m$, et $\Pi_e(x, \sigma, \_, \sigma')$, correspondant à $e$ et dépendant de la variable $x$ libre dans $e$, du flot d'entrée $\sigma$ passé à $e$, et du résultat $\_$ et du flot de sortie $\sigma'$ obtenus lors du calcul de $e$. Et alors on obtient : \begin{displaymath} \Pi_g(\sigma, \_, \sigma') ~ := ~ \exists s, \exists x, \exists m' : ~ \Pi_m(m') ~ \land ~ \sigma \xrightarrow[\square] {m'} \left\langle x, s \right\rangle ~ \land ~ \Pi_e(x, s, \_, \sigma') \end{displaymath} où, cette fois, $\sigma$ désigne le flot d'entrée, $\_$ le résultat et $\sigma'$ le flot de sortie lors du calcul de \emph{toute l'expression $\mathsf{sample}$}. \\ \end{itemize} ~ Pour pouvoir raisonner avec de telles formules, il est nécessaire de disposer également d'un mécanisme d'\emph{élimination} de telles formules : ~ \begin{itemize} \item pour un couple $(a, b)$, que nous noterons $c$, on génère les formules $\Pi_a(\_)$ et $\Pi_b(\_)$ correspondant à $a$ et $b$ et dépendant du résultat $\_$ de leurs évaluations respectives, et alors on obtient : \begin{displaymath} \Pi_c(\_) ~ := ~ \forall a', \forall b' : ~ a' \xrightleftharpoons[\otimes]\_ b' ~ \Rightarrow ~ \Pi_a(a') ~ \land ~ \Pi_b(b') \end{displaymath} où $\_$ représente le résultat de l'évaluation du couple $c$. \\ \item pour une abstraction $\lambda x. ~ c$, que nous noterons $f$, on génère la formule $\Pi_c(x, \_)$, dépendant de la variable $x$ libre dans $c$ et du résultat $\_$ de l'évaluation de $c$ à $x$ fixé, et alors on obtient : \begin{displaymath} \Pi_f(\_) ~ := ~ \forall x, \forall y : ~ x \xrightarrow[\triangleright]{\_} y ~ \Rightarrow ~ \Pi_c(x, y) \end{displaymath} En effet, dans cette formule, $\_$, résultat de l'évaluation du terme abstraction $f$, désigne le terme abstraction lui-même (d'où son occurrence sur la flèche $\xrightarrow[\triangleright]{\_}$), car c'est une valeur. \\ \item pour un terme $\mathsf{prob} ~ e$, que nous noterons $m$, on génère la formule $\Pi_e(\sigma, \_, \sigma')$ correspondant à $e$ et dépendant du flot d'entrée $\sigma$ passé à $e$ et du résultat $\_$ et du flot de sortie $\sigma'$ obtenus lors du calcul de $e$ sous $\sigma$, et alors on obtient : \begin{displaymath} \Pi_m(\_) ~ := ~ \forall s, \forall y, \forall s' : ~ s \xrightarrow[\square]\_ \left\langle y, s' \right\rangle ~ \Rightarrow ~ \Pi_e(s, y, s') \end{displaymath} Là encore, $\_$ représente le terme $\mathsf{prob}$ lui-même, car c'est une valeur. \end{itemize} ~ Une quatrième structure qui aurait pu faire l'objet de la création d'une nouvelle formule logique est l'expression $\mathcal S$ de consommation de l'élément de flot. Seulement, si j'avais créé une telle relation, le mécanisme d'introduction aurait été évident puisqu'il aurait correspondu à la formule pour $\mathcal S$, mais il n'aurait pas existé \emph{a priori} de mécanisme d'élimination d'une telle relation. C'est pourquoi j'ai opté cette fois-ci pour l'ajout d'un «terme de formule», le \emph{conse} $::$, qui, en fait, correspond plutôt à un terme de théorie des flots : \begin{displaymath} \Pi_{\mathcal S}(\sigma, \_, \sigma') ~ := ~ \sigma = \_ :: \sigma' \end{displaymath} ~ \textbf{Exemple. } Supposons que l'on dispose des réels avec les opérations et relations élémentaires. Supposons que le type $\tau_0$ des éléments de flot soit le type $\mathsf R$ des réels. Considérons le terme suivant : \begin{displaymath} \lambda p : \mathsf R . ~ \mathsf{prob} ~ \mathsf{sample} ~ x ~ \mathsf{from} ~ \mathsf{prob} ~ \mathcal S ~ \mathsf{in} ~ x \leqslant p \end{displaymath} C'est une abstraction. Alors, générons la formule $\Pi_1(p, \_)$ de son terme-corps : \begin{displaymath} m_1 := ~ \mathsf{prob} ~ \mathsf{sample} ~ x ~ \mathsf{from} ~ \mathsf{prob} ~ \mathcal S ~ \mathsf{in} ~ x \leqslant p \end{displaymath} Le terme $m_1$ est un $\mathsf{prob}$, alors, générons la formule $\Pi_{11}(p, \sigma, \_, \sigma')$ de son expression-corps : \begin{displaymath} e_{11} := ~ \mathsf{sample} ~ x ~ \mathsf{from} ~ \mathsf{prob} ~ \mathcal S ~ \mathsf{in} ~ x \leqslant p \end{displaymath} L'expression $e_{11}$ est un $\mathsf{sample}$. Alors, générons d'abord la formule $\Pi_{111}(p, \_)$ du terme introduit par $\mathsf{from}$ : \begin{displaymath} m_{111} := ~ \mathsf{prob} ~ \mathcal S \end{displaymath} Le terme $m_{111}$ est un $\mathsf{prob}$, alors, générons la formule $\Pi_{1111}(p, \sigma, \_, \sigma')$ de son expression-corps : \begin{displaymath} e_{1111} := ~ \mathcal S \end{displaymath} L'expression $e_{1111}$ est un $\mathcal S$, sa formule vient immédiatement : \begin{displaymath} \Pi_{1111}(p, \sigma, \_, \sigma') := ~ \sigma = \_ :: \sigma' \end{displaymath} On revient alors à la formule $\Pi_{111}(p, \_)$ du terme $m_{111}$ qui est un $\mathsf{prob}$ : c'est donc \begin{displaymath} \begin{array}{rcl} \Pi_{111}(p, \_) & := & \forall s_{111}, \forall y_{111}, \forall s'_{111} : ~ s_{111} \xrightarrow[\square]\_ \langle y_{111}, s'_{111} \rangle ~ \Rightarrow \Pi_{1111}(p, s_{111}, y_{111}, s'_{111}) \\ & \equiv & \forall s_{111}, \forall y_{111}, \forall s'_{111} : ~ s_{111} \xrightarrow[\square]\_ \langle y_{111}, s'_{111} \rangle ~ \Rightarrow s_{111} = y_{111} :: s'_{111} \\ \end{array} \end{displaymath} Revenons donc à l'expression $e_{11}$ : il faut maintenant générer la formule $\Pi_{112}(p, x, \sigma, \_, \sigma')$ de l'expression introduite par $\mathsf{in}$ : \begin{displaymath} e_{112} := ~ x \leqslant p \end{displaymath} C'est un terme : il y aura donc $\sigma' = \sigma$, et comme on a un terme spécial $\leqslant$, on peut dire que la formule obtenue est : \begin{displaymath} \Pi_{112}(p, x, \sigma, \_, \sigma') := ~ (\_ = \mathsf{true} \Leftrightarrow x \leqslant p) ~ \land ~ \sigma' = \sigma \end{displaymath} Revenant à $e_{11}$, on obtient désormais : \begin{displaymath} \begin{array}{rcll} \Pi_{11}(p, \sigma, \_, \sigma') & := & & \exists s_{11}, \exists x_{11}, \exists m_{111} : \\ & & & \Pi_{111}(p, m_{111}) \\ & & \land & \sigma \xrightarrow[\square] {m_{111}} \left\langle x_{11}, s_{11} \right\rangle \\ & & \land & \Pi_{112}(p, x_{11}, s_{11}, \_, \sigma') \\ \\ & \equiv & & \exists s_{11}, \exists x_{11}, \exists m_{111} : \\ & & & \left( \forall s_{111}, \forall y_{111}, \forall s'_{111} : ~ s_{111} \xrightarrow[\square]{m_{111}} \langle y_{111}, s'_{111} \rangle ~ \Rightarrow s_{111} = y_{111} :: s'_{111} \right) \\ & & \land & \sigma \xrightarrow[\square] {m_{111}} \left\langle x_{11}, s_{11} \right\rangle \\ & & \land & \left( (\_ = \mathsf{true} \Leftrightarrow x_{11} \leqslant p) ~ \land ~ \sigma' = s_{11} \right) \\ \end{array} \end{displaymath} qui est déjà difficile à lire. Pour en revenir au terme $m_1$, qui est un $\mathsf{prob}$, on obtient la formule suivante : \begin{displaymath} \begin{array}{rcll} \Pi_1(p, \_) & := & & \forall s_1, \forall y_1, \forall s'_1 : \\ & & & s_1 \xrightarrow[\square]{\_} \langle y_1, s'_1 \rangle ~ \Rightarrow \\ & & & \exists s_{11}, \exists x_{11}, \exists m_{111} : \\ & & & \left( \forall s_{111}, \forall y_{111}, \forall s'_{111} : ~ s_{111} \xrightarrow[\square]{m_{111}} \langle y_{111}, s'_{111} \rangle ~ \Rightarrow s_{111} = y_{111} :: s'_{111} \right) \\ & & \land & s_1 \xrightarrow[\square] {m_{111}} \left\langle x_{11}, s_{11} \right\rangle \\ & & \land & \left( (y_1 = \mathsf{true} \Leftrightarrow x_{11} \leqslant p) ~ \land ~ s'_1 = s_{11} \right) \\ \end{array} \end{displaymath} Et enfin, la formule pour notre terme abstraction de départ : \begin{displaymath} \begin{array}{rcll} \Pi(\_) & := & & \forall p, \forall m_1 : \\ & & & p \xrightarrow[\triangleright]\_ m_1 ~ \Rightarrow \\ & & & \forall s_1, \forall y_1, \forall s'_1 : \\ & & & s_1 \xrightarrow[\square]{m_1} \langle y_1, s'_1 \rangle ~ \Rightarrow \\ & & & \exists s_{11}, \exists x_{11}, \exists m_{111} : \\ & & & \left( \forall s_{111}, \forall y_{111}, \forall s'_{111} : ~ s_{111} \xrightarrow[\square]{m_{111}} \langle y_{111}, s'_{111} \rangle ~ \Rightarrow s_{111} = y_{111} :: s'_{111} \right) \\ & & \land & s_1 \xrightarrow[\square] {m_{111}} \left\langle x_{11}, s_{11} \right\rangle \\ & & \land & \left( (y_1 = \mathsf{true} \Leftrightarrow x_{11} \leqslant p) ~ \land ~ s'_1 = s_{11} \right) \\ \end{array} \end{displaymath} \subsubsection{Langage de formules \Lo : définition formelle} Maintenant que nous avons présenté informellement les trois relations spéciales de notre logique : $\xrightleftharpoons[\otimes]{}$ pour les projections, $\xrightarrow[\triangleright]{}$ pour les applications, et $\xrightarrow[\square]{}$ pour les expressions $\mathsf{sample}$, nous pouvons les décrire formellement en définissant de manière rigoureuse le langage \Lo des formules où elles vont apparaître, avant d'établir le schéma définitif des règles de génération. ~ \begin{defin}[Langage de formules \Lo sur un contexte de variables] Fixons une fois pour toutes un ensemble $T_0$ de types de base, et un ensemble $\mathcal R$ de relations et un ensemble $\mathcal O$ d'opérations sur ces types de base ainsi que les booléens. Soit $\Gamma$ un ensemble non vide de variables, ou contexte. Alors, l'ensemble $TF^\Gamma$ des termes de formule et l'ensemble $\mathcal L_\bigcirc^\Gamma$ des formules logiques sur le contexte $\Gamma$ décrivant sont définis par la grammaire suivante : \begin{displaymath} \begin{array}{llllll} TF^\Gamma & ::= & \\ & & | & v & (v\text{ valeur de base}) \\ & & | & x & (x \in \Gamma) & \text{Variable} \\ & & | & x :: t & (x, t \in TF^\Gamma) & \text{Consommation du flot} \\ & & | & O(x_1, \dots, x_n) & (O \in \mathcal O, ~ x_1, \dots, x_n \in TF^\Gamma) & \text{Opération} \\ \\ \mathcal L_\bigcirc^\Gamma & ::= & \\ & & | & \top & & \text{formule vraie} \\ \\ & & | & R(x_1, \dots, x_n) & (R \in \mathcal R, ~ x_1, \dots, x_n \in TF^\Gamma) & \text{Relation} \\ \\ & & | & a \xrightleftharpoons[\otimes]{c} b & (a,b,c \in TF^\Gamma) & \text{Couple} \\ \\ & & | & a \xrightarrow[\triangleright]{f} y & (a,f,y \in TF^\Gamma) & \text{Application} \\ \\ & & | & s \xrightarrow[\square]{m} \left\langle x, t \right\rangle & (s, m, x, t \in TF^\Gamma) & \text{Echantillonnage} \\ \\ & & | & s = t & (s, t \in TF^\Gamma) & \text{Egalité} \\ \\ & & | & \lnot F & (F \in \mathcal L_\bigcirc^\Gamma) & \text{Opérations logiques} \\ & & | & F \land G & (F, G \in \mathcal L_\bigcirc^\Gamma) \\ & & | & F \lor G & (F, G \in \mathcal L_\bigcirc^\Gamma) \\ & & | & F \Rightarrow G & (F, G \in \mathcal L_\bigcirc^\Gamma) \\ & & | & F \Leftrightarrow G & (F, G \in \mathcal L_\bigcirc^\Gamma) \\ \\ & & | & \exists v : F & (v \notin \Gamma, ~ F \in \mathcal L_\bigcirc ^{\Gamma \cup \left\{ v \right\} }) & \text{Quantifications} \\ & & | & \forall v : F & (v \notin \Gamma, ~ F \in \mathcal L_\bigcirc^{\Gamma \cup \left\{ v \right\} }) \\ \end{array} \end{displaymath} \end{defin} Comme nous allons le voir dans la description formelle du système de génération des formules : pour le raisonnement avec des formules du langage \Lo, le raisonnement avec les formules spéciales ne nécessite pas d'autres règles logiques que celles de la logique «classique» des prédicats (logique du second ordre). \subsubsection{Règles de génération des formules : termes (sauf points fixes)} Dans cette sous-section ainsi que les deux suivantes, je présente les règles définitives de génération des formules suivant la syntaxe du \lo, avec les points fixes, ce qui nécessite de parler de la terminaison, sous la forme des jugements $\Gamma ~ \vdash ~ \{ P \} ~ m ~ \{ Q \}$ avec $P$ condition suffisante de terminaison et $Q$ prédicat de correction vérifiée par le résultat sous l'hypothèse que le programme termine. ~ \textbf{Attention :} la notation utilisée ici, sous forme de règles d'inférence, \emph{ne correspond pas} à une éventuelle sémantique axiomatique, car la génération des formules suivant la sémantique opérationnelle conduit à propager les informations \emph{vers la racine} et non les feuilles. ~ Les formules pour les termes ne dépendent pas des flots. Dans cette section, je reprends les règles de génération des formules de correction de la section \ref{s-pi-light} mais en y intégrant la terminaison. ~ \textbf{$\mathsf{true}$, $\mathsf{false}$ ou valeur de base :} une telle valeur termine toujours. \begin{displaymath} \frac{v\text{ valeur de base}}{\Gamma ~ \vdash ~ \{ \top \} ~ v ~ \{ \_ = v \} } \end{displaymath} ~ \textbf{Variable :} lorsque l'on tente d'évaluer une variable, en fait, au niveau où on réduit le terme ou l'expression où elle figure, elle est remplacée par un terme dont l'évaluation termine toujours (ce qui est vrai dans le cas où la variable désigne le point fixe dans son corps, sous les restrictions annoncées plus loin). Donc, elle termine toujours. \begin{displaymath} \frac{x \in \Gamma}{\Gamma ~ \vdash ~ \{ \top \} ~ x ~ \{ \_ = x \} } \end{displaymath} ~ \textbf{Test :} si le booléen termine, alors on peut effectuer le branchement, et la condition de terminaison varie en fonction de la valeur du booléen. \begin{displaymath} \frac{\Gamma ~ \vdash ~ \{ P_a \} ~ a ~ \{ Q_a(\_) \} ~ ~ ~ \Gamma ~ \vdash ~ \{ P_b \} ~ b ~ \{ Q_b(\_) \} ~ ~ ~ \Gamma ~ \vdash ~ \{ P_c \} ~ c ~ \{ Q_c(\_) \} ~ ~ ~ }{ \Gamma ~ \vdash ~ \left\{ \begin{array}{ll} & P_a \\ \land & \forall a' : \\ & P_a \land Q_a(a') ~ \Rightarrow \\ & (a' = \mathsf{true} ~ \Rightarrow ~ P_b) \\ \land & (a' = \mathsf{false} ~ \Rightarrow ~ P_c) \\ \end{array} \right\} ~ \mathsf{if} ~ a ~ \mathsf{then} ~ b ~ \mathsf{else} ~ c ~ \left\{ \begin{array}{ll} & \exists a' : \\ & Q_a(a') \\ \land & (a' = \mathsf{true} ~ \Rightarrow ~ Q_b(\_)) \\ \land & (a' = \mathsf{false} ~ \Rightarrow ~ Q_c(\_)) \\ \end{array} \right\} } \end{displaymath} ~ \textbf{Application :} il faut d'abord assurer la terminaison de la fonction et de l'argument. Mais la formule de correction de la fonction contient aussi la condition pour que l'application termine «après la $\beta$-réduction», en quelque sorte, condition qui doit être entraînée par la formule de correction de l'argument. \begin{displaymath} \frac{ \Gamma ~ \vdash ~ \{P_a \} ~ a ~ \{ Q_a(\_) \} ~ ~ ~ \Gamma ~ \vdash ~ \{P_b \} ~ b ~ \{ Q_b(\_) \} ~ ~ ~ }{ \Gamma ~ \vdash ~ \left\{ \begin{array}{ll} & P_a \land P_b \\ \land & \forall a', \forall b' : \\ & P_a \land P_b \land Q_a(a') \land Q_b(b') ~ \Rightarrow \\ & \exists y : ~ b' \xrightarrow[\triangleright] {a'} y \\ \end{array} \right\} ~ a ~ b ~ \left\{ \begin{array}{ll} & \exists a', \exists b' : \\ & Q_a(a') \land Q_b(b') \\ \land & b' \xrightarrow[\triangleright] {a'} \_ \\ \end{array} \right\} } \end{displaymath} ~ \textbf{Abstraction :} elle-même termine toujours (c'est une valeur). C'est dans la correction que l'on doit insérer la propriété de «terminaison de la fonction une fois appliquée». A $\alpha$-renommage près, on peut supposer que la variable $x \notin \Gamma$. \begin{displaymath} \frac{ \Gamma \cup \{ x \} ~ \vdash ~ \{ P_c(x) \} ~ c ~ \{ Q_c(x, \_) \} }{ \Gamma ~ \vdash ~ \{ \top \} ~ \lambda x. ~ c ~ \left\{ \begin{array}{ll} & \left( \forall x : ~ P_c(x) ~ \Rightarrow ~ \exists y : ~ x \xrightarrow[\triangleright]{\_} y \right) \\ \land & \left( \forall x, \forall y : ~ x \xrightarrow[\triangleright]{\_} y ~ \Rightarrow ~ Q_c(x, y) \right) \\ \end{array} \right\} } \end{displaymath} ~ \textbf{Couple :} termine si et seulement si ses deux membres terminent. \begin{displaymath} \frac{ \Gamma ~ \vdash ~ \{ P_a \} ~ a ~ \{ Q_a(\_) \} ~ ~ ~ \Gamma ~ \vdash ~ \{ P_b \} ~ b ~ \{ Q_b(\_) \} }{ \Gamma ~ \vdash ~ \{ P_a \land P_b \} ~ (a, b) ~ \left\{ \begin{array}{l} \forall a', \forall b' : \\ a' \xrightleftharpoons[\otimes] \_ b' ~ \Rightarrow ~ Q_a(a') \land Q_b(b') \end{array} \right\} } \end{displaymath} ~ \textbf{Projections :} terminent si et seulement si le couple dont on veut une projection termine. \begin{displaymath} \frac{ \Gamma ~ \vdash ~ \{ P_c \} ~ c ~ \{ Q_c(\_) \} ~ ~ ~ }{ \Gamma ~ \vdash ~ \{ P_c \} ~ \mathsf{fst} ~ c ~ \left\{ \begin{array}{l} \exists c', \exists b : \\ \_ \xrightleftharpoons[\otimes] {c'} b ~ \land ~ Q_c(c') \end{array} \right\} } ~ ~ ~ \frac{ \Gamma ~ \vdash ~ \{ P_c \} ~ c ~ \{ Q_c(\_) \} ~ ~ ~ }{ \Gamma ~ \vdash ~ \{ P_c \} ~ \mathsf{snd} ~ c ~ \left\{ \begin{array}{l} \exists c', \exists a : \\ a \xrightleftharpoons[\otimes] {c'} \_ ~ \land ~ Q_c(c') \end{array} \right\} } \end{displaymath} ~ \textbf{Terme $\mathsf{prob}$ :} lui-même termine toujours (c'est une valeur). Mais lorsque l'on génère les formules de terminaison et de correction de son expression-corps, celles-ci dépendent des flots d'entrée $\sigma$ et de sortie $\sigma'$. Cette dépendance est «capturée» par la relation $\xrightarrow[\square]{}$. De plus, comme pour l'abstraction, la terminaison de l'expression $e$, une fois le $\mathsf{prob}$ échantillonné par un $\mathsf{sample}$, apparaît dans la formule de correction du $\mathsf{prob}$. \begin{displaymath} \frac{ \Gamma ~ \vdash ~ \{ P_e(\sigma) \} ~ e ~ \{ Q_e(\sigma, \_, \sigma') \} }{ \Gamma ~ \vdash ~ \{ \top \} ~ \mathsf{prob} ~ e ~ \left\{ \begin{array}{ll} & \left( \forall s : ~ P_e(s) ~ \Rightarrow ~ \exists y, \exists s' : ~ s \xrightarrow[\square] \_ \langle y, s' \rangle \right) \\ \land & \left( \forall s, \forall y, \forall s' : ~ s \xrightarrow[\square] \_ \langle y, s' \rangle ~ \Rightarrow ~ Q_e(s, y, s') \right) \\ \end{array} \right\} } \end{displaymath} \subsubsection{Règles de génération des formules : expressions} Cette fois, les formules dépendent des flots d'entrée $\sigma$ et de sortie $\sigma'$ de l'expression. ~ \textbf{Terme en tant qu'expression :} il faut générer les formules du terme, mais aussi exprimer que le flot est inchangé. En ce sens, en toute rigueur, il faudrait distinguer les deux sortes de générations de formules, les termes d'un côté et les expressions de l'autre, comme on fait pour le typage. \begin{displaymath} \frac{ \Gamma ~ \vdash ~ \{ P_m \} ~ m ~ \{ Q_m(\_) \} }{ \Gamma ~ \vdash ~ \{ P_m \} ~ m ~ \{ Q_m(\_) ~ \land ~ \sigma' = \sigma \} } \end{displaymath} ~ \textbf{Extraction $\mathcal S$ d'un élément de flot :} elle termine toujours. \begin{displaymath} \frac{}{ \Gamma ~ \vdash ~ \{ \top \} ~ \mathcal S ~ \{ \sigma = \_ :: \sigma' \} } \end{displaymath} ~ \textbf{Echantillonnage $\mathsf{sample} ~ x ~ \mathsf{from} ~ m ~ \mathsf{in} ~ e$ :} Là, la formule de terminaison est plus compliquée, car il faut s'assurer de trois choses : \begin{itemize} \item S'assurer que l'évaluation du terme $m$ termine. \item S'assurer, une fois que le terme $m$ est réduit à un $\mathsf{prob} ~ e_m$, que sous le flot d'entrée $\sigma$ du $\mathsf{sample}$, l'expression $e_m$ termine \item S'assurer, une fois que l'expression $e_m$ donne un flot de sortie $t$ et une valeur $v$, que l'expression $e[x := v]$ termine sous le flot d'entrée $t$. \end{itemize} Là encore, à $\alpha$-renommage près, on peut supposer que $x \notin \Gamma$. \begin{displaymath} \frac{ \Gamma ~ \vdash ~ \{ P_m \} ~ m ~ \{ Q_m(\_) \} ~ ~ ~ \Gamma \cup \{ x \} ~ \vdash ~ \{ P_e(x, \sigma) \} ~ e ~ \{ Q_e(x, \sigma, \_, \sigma') \} }{ \Gamma ~ \vdash ~ \left\{ \begin{array}{ll} & P_m \\ \land & ( \forall m' : \\ & P_m \land Q_m(m') ~ \Rightarrow \\ & \exists x, \exists t : ~ \sigma \xrightarrow[\square] {m'} \langle x, t \rangle ) \\ \land & ( \forall m', \forall x, \forall t : \\ & P_m \land Q_m(m') ~ \land ~ \sigma \xrightarrow[\square] {m'} \langle x, t \rangle ~ \Rightarrow \\ & P_e(x, t) ) \\ \end{array} \right\} ~ \mathsf{sample} ~ x ~ \mathsf{from} ~ m ~ \mathsf{in} ~ e ~ \left\{ \begin{array}{ll} & \exists m', \exists x, \exists t : \\ & Q_m(m') \\ \land & \sigma \xrightarrow[\square] {m'} \langle x, t \rangle \\ \land & Q_e(x, t, \_, \sigma') \\ \end{array} \right\} } \end{displaymath} \subsubsection{Règles de génération des formules : points fixes} \label{s-pi-fix} La terminaison d'un point fixe est une vaste question. Comme il est naturellement hors de portée de vouloir la traiter en toute généralité, je me suis borné à étudier les deux formes récursives suivantes, qui me semblent les plus courantes dans les algorithmes probabilistes : ~ \begin{itemize} \item Les points fixes «déterministes» : il s'agit d'algorithmes dont on peut exhiber un \emph{variant déterministe}. Le plus souvent, l'algorithme est une fonction et le variant est son argument récursif. Le cas classique est, bien entendu, celui de la \emph{factorielle}, qui appartient à la classe très connue des programmeurs impératifs des \emph{boucles \texttt{for}}. Une telle boucle, qui s'écrirait en gros en impératif : \\ $result$\verb+ := +$init$\verb+;+ \\ \verb+for +$n$\verb+ = 1 to +$fin$ \\ \verb+do+ \\ \verb+ + $result$\verb+ := +$corps$\verb+;+ \\ \verb+done;+ \\ \verb+return +$result$\verb+;+\\ s'écrirait, en \lo, dans le cas où $corps$ est un terme de type $\mathsf{nat} \rightarrow t \rightarrow \bigcirc ~ t$ (permettant de calculer une valeur aléatoire en fonction du compteur $n$ et du résultat de l'itération précédente) : ~ $\mathsf{sample} ~ return ~ \mathsf{from} ~ ($\\ \verb+ + $\mathsf{fix} ~ boucle : ~ \mathsf{nat} \rightarrow \bigcirc ~ t . ~ \lambda n : \mathsf{nat} . ~ \mathsf{prob} $\\ \verb+ + $\mathsf{if} ~ n = 0$ \\ \verb+ + $\mathsf{then} ~ \mathsf{prob} ~ init $ \\ \verb+ + $\mathsf{else} ~ \mathsf{prob} ~ $ \\ \verb+ + $\mathsf{sample} ~ result_{prev} ~ \mathsf{from} ~ boucle ~ (n - 1) ~ \mathsf{in}$ \\ \verb+ + $\mathsf{sample} ~ result ~ \mathsf{from} ~ corps ~ n ~ result_{prev} ~ \mathsf{in}$ \\ \verb+ + $result$ \\ $) ~ fin$ \\ $\mathsf{in} ~ return$ \\ ~ \item Les points fixes «probabilistes» : il s'agit d'algorithmes dont le variant est probabiliste. Dans le cadre des simulations de lois de probabilité, on rencontre souvent ce que l'on appelle en langage impératif des \emph{boucles \texttt{repeat}...\texttt{until}}. Une telle boucle, qui s'écrirait en gros en impératif : \\ \verb+repeat+ \\ \verb+ + $result$\verb+ := +$corps$\verb+;+ \\ \verb+until +$cond$\verb+;+ \\ \verb+return +$result$\verb+;+\\ s'écrirait, en \lo, dans le cas où $corps$ est un terme de type $\bigcirc ~ t$ (permettant de calculer une valeur aléatoire) et $cond$ est un terme de type $t \rightarrow \bigcirc ~ \mathsf{bool}$ (condition aléatoire, calcul d'un booléen aléatoire en fonction du résultat obtenu) : ~ $\mathsf{sample} ~ return ~ \mathsf{from}$\\ \verb+ + $\mathsf{fix} ~ boucle : ~ \bigcirc ~ t . ~ \mathsf{prob} $\\ \verb+ + $\mathsf{sample} ~ result ~ \mathsf{from} ~ corps ~ \mathsf{in}$ \\ \verb+ + $\mathsf{sample} ~ b ~ \mathsf{from} ~ cond ~ result ~ \mathsf{in}$ \\ \verb+ + $\mathsf{sample} ~ return_0 ~ \mathsf{from}$ \\ \verb+ + $\mathsf{if} ~ b$ \\ \verb+ + $\mathsf{then} ~ \mathsf{prob} ~ result $ \\ \verb+ + $\mathsf{else} ~ boucle$\\ \verb+ + $\mathsf{in} ~ return_0$ \\ $\mathsf{in} ~ return$ \\ \end{itemize} ~ Je n'ai donc considéré que ces deux classes de points fixes, et j'ai donc restreint à ces deux formes la définition du terme $\mathsf{fix}$ du \lo : \begin{displaymath} \begin{array}{llllll} Term & ::= & \dots & & & \text{termes non récursifs} \\ & & | & \mathsf{fix} ~ x. ~ \lambda n. ~ c & (x,n \in \mathcal V, ~ c \in Term) & \text{Point fixe déterministe} \\ & & | & \mathsf{fix} ~ x. ~ \mathsf{prob} ~ e & (x \in \mathcal V, ~ e \in Expr) & \text{Point fixe probabiliste} \\ \end{array} \end{displaymath} Ainsi, l'évaluation du point fixe en lui-même termine toujours, car elle consiste en un seul dépliage : $\lambda n. ~ c[x := \mathsf{fix} \dots]$ ou $\mathsf{prob} ~ e[x := \mathsf{fix} \dots]$, lesquels termes obtenus après ce dépliage sont des valeurs. En outre, cela justifie, sous ces restrictions, que «l'évaluation d'une variable termine toujours», car la variable $x$ est remplacée par le terme point fixe, dont on vient de montrer qu'il termine. ~ \textbf{Formules pour un point fixe déterministe. } L'approche choisie est tout à fait classique : on a besoin de spécifier un \emph{variant} et un \emph{ordre bien fondé} selon lequel le variant décroît strictement. \emph{On convient que le variant est l'argument $n$ dans $\mathsf{fix} ~ x. ~ \lambda n. ~ c$}. En effet, on peut toujours se ramener à ce cas : \begin{itemize} \item Si le variant est constitué de plusieurs arguments (par exemple, avec l'ordre lexicographique), on «décurryfie» la fonction pour qu'elle ne prenne qu'un seul argument de type couple. \item Si le variant est constitué du résultat d'une opération $F$ fixée sur l'argument $n$, il suffit de modifier la définition de l'ordre pour y «intégrer» l'opération $F$. \end{itemize} ~ L'ordre est alors indiqué en décorant le terme. Dans le cadre de la génération des formules : comme on a vu que le point fixe en lui-même termine toujours, la condition de terminaison du «point fixe une fois appliqué» apparaît à l'intérieur de la formule de correction du point fixe. Etant donné un $n$, pour que l'application termine au point $n$, il suffit qu'elle termine pour les éléments plus petits que $n$ et que la condition de terminaison du corps soit vérifiée pour $n$. Charge alors à l'utilisateur de prouver la terminaison de l'application pour $n$ en exhibant la preuve de bonne fondation de l'ordre sur le variant. Cette formule de terminaison est alors simplement conjointe à la formule de correction de l'abstraction comme s'il ne s'agissait pas d'un point fixe (étant donné que cette formule \emph{suppose} la terminaison de l'application). \begin{displaymath} \frac{ \Gamma \cup \{ x, n \} ~ \vdash ~ \{ P_c(x, n) \} ~ c ~ \{ Q_c(x, n, \_) \} }{ \Gamma ~ \vdash ~ \{ \top \} ~ \mathsf{fix} ~ x. ~ \lambda_\prec n. ~ c ~ \left\{ \begin{array}{ll} & \left( \forall n : \begin{array}{ll} & P_c(\_, n) ~ \land ~ \left( \forall m : ~ m \prec n ~ \Rightarrow ~ \exists z : ~ m \xrightarrow[\triangleright] \_ z \right) \\ \Rightarrow & \exists y : ~ n \xrightarrow[\triangleright] \_ y \\ \end{array} \right) \\ \land \\ & \left( \forall n, \forall y : ~ n \xrightarrow[\triangleright] \_ y ~ \Rightarrow ~ Q_c(\_, n, y) \right) \\ \end{array} \right\} } \end{displaymath} où $\prec$ est l'ordre sur le variant, supposé bien fondé. ~ \textbf{Formules pour un point fixe probabiliste. } L'idée fondamentale est de dire qu'un point fixe probabiliste est simplement un point fixe dont \emph{le variant est le flot de données aléatoires lui-même}. Cependant, ce n'est pas suffisant. En effet, nombreux sont les algorithmes probabilistes qui ne terminent pas de façon déterministe. Un des plus simples est la simulation suivante de la distribution géométrique de paramètre $p$ : ~ \verb+ + $\mathsf{fix} ~ boucle : ~ \bigcirc ~ \mathsf{nat}. ~ \mathsf{prob} $\\ \verb+ + $\mathsf{sample} ~ x ~ \mathsf{from} ~ \mathsf{prob} ~ \mathcal S ~ \mathsf{in}$ \\ \verb+ + $\mathsf{sample} ~ return ~ \mathsf{from}$ \\ \verb+ + $\mathsf{if} ~ x \leqslant p$ \\ \verb+ + $\mathsf{then} ~ \mathsf{prob} ~ 0 $ \\ \verb+ + $\mathsf{else} ~ \mathsf{prob} ~ \mathsf{sample} ~ y ~ \mathsf{from} ~ boucle ~ \mathsf{in} ~ y + 1$\\ \verb+ + $\mathsf{in} ~ return$ \\ Un tel algorithme peut boucler indéfiniment si le flot d'entrée est par exemple constitué uniquement de valeurs plus grandes que $p$. Il faut donc que l'utilisateur spécifie un ensemble sur lequel il sait que l'algorithme termine, c'est-à-dire tel que l'appartenance du flot d'entrée à cet ensemble soit une condition suffisante de terminaison, cette condition étant déterministe. Par conséquent, l'utilisateur pourra montrer plus tard que l'algorithme termine avec probabilité plus grande que la mesure de l'ensemble indiqué. Pour montrer la terminaison avec probabilité 1, il suffit donc d'exhiber un tel ensemble de mesure 1. Supposant que le flot d'entrée est dans cet ensemble, pour montrer la terminaison de l'algorithme, l'utilisateur fera comme s'il s'agissait d'un point fixe déterministe : indiquer un ordre bien fondé sur les flots appartenant à cet ensemble. Aussi les formules générées pour un tel point fixe sont-elles très voisines de celles générées pour un point fixe déterministe. \begin{displaymath} \frac{ \Gamma \cup \{ x \} ~ \vdash ~ \{ P_c(x, \sigma) \} ~ c ~ \{ Q_c(x, \sigma, \_, \sigma') \} }{ \Gamma ~ \vdash ~ \{ \top \} ~ \mathsf{fix} ~ x. ~ \mathsf{prob}_{S,\prec} ~ c ~ \left\{ \begin{array}{ll} & \left( \forall s : \begin{array}{ll} & P_c(\_, s) ~ \land ~ s \in S ~ \land ~ \\ & \left( \forall t : ~ t \in S ~ \land ~ t \prec s ~ \Rightarrow ~ \exists z, t' : ~ t \xrightarrow[\square] \_ \langle z, t' \rangle \right) \\ \Rightarrow & \exists y, \exists s' : ~ s \xrightarrow[\square] \_ \langle y, s' \rangle \\ \end{array} \right) \\ \land \\ & \left( \forall s, \forall y, \forall s' : ~ s \xrightarrow[\square] \_ \langle y, s' \rangle ~ \Rightarrow ~ Q_c(\_, s, y, s') \right) \\ \end{array} \right\} } \end{displaymath} où $S$ est l'<> pour la terminaison de l'algorithme, et $\prec$ l'ordre bien fondé sur cet ensemble. \subsubsection[Mise en \oe uvre du transformateur $\Pi$]{Mise en \oe uvre du transformateur $\Pi$\protect\footnote{Pour des informations d'ordre pratique (comment utiliser effectivement $\Pi$ sur une machine), on se réfèrera à l'annexe, page~\pageref{src}.}} Nous venons de présenter un système de génération de deux formules, l'une de terminaison, l'autre de correction, pour chaque élément du langage \lo. Nous obtenons donc en sortie provisoire, pour un programme $m$ passé en entrée de $\Pi$, un jugement de la forme : \begin{displaymath} \Gamma ~ \vdash ~ \{ P \} ~ m ~ \{ Q(\_) \} \end{displaymath} Mais sous cette forme, le jugement généré n'est pas encore exploitable dans un système de preuve, pas plus que ne l'est le couple $(P, Q)$ des formules obtenues. ~ Il y a donc une dernière étape à accomplir, au niveau \emph{global} cette fois : réunir ces deux formules en une seule, \emph{que l'on pourra utiliser pour raisonner en Coq}. Rappelons qu'un tel jugement se lit : <>. C'est suivant cette lecture que le transformateur génère la formule finale globale à partir des deux formules de terminaison $P$ et de correction $Q$. ~ On rappelle que le programme $m$ est un \emph{terme}; on peut considérer que ce terme va être stocké dans une variable «globale». Sous le contexte $\Gamma$ des variables globales déclarées avant le terme $m$, le transformateur $\Pi$ fonctionne alors, en supposant que le terme soit stocké dans la variable $v_m$, de la manière suivante : \begin{enumerate} \item $\Pi$ génère les formules $P$ et $Q(\_)$ telles que \[\Gamma ~\vdash \{ P \} ~ m ~ \{ Q(\_) \}\] \item et alors la formule \emph{globale} obtenue pour le programme est $P ~ \Rightarrow ~ Q(v_m)$. \end{enumerate} En fait, la variable $v_m$ existe toujours en Coq, mais la terminaison est quand même «comprise» dans cette formule en ce sens que si $P$ n'est pas vérifiée, alors \emph{le comportement du programme est indéterminé}. Cependant, on ne peut pas dire \emph{a priori} que le programme ne termine pas, car $P$, on le rappelle, est une \emph{condition suffisante} de terminaison. Toutefois, en pratique, le terme $m$ est une abstraction ou un $\mathsf{prob}$ : c'est donc une valeur, qui «termine toujours» au sens où $P \equiv \top$, donc le problème ne se pose pas. \subsection{Formalisation en Coq} J'ai mis en \oe uvre dans le système Coq la représentation des données aléatoires par une formalisation sous deux aspects : \begin{itemize} \item l'axiomatique des espaces mesurables et des probabilités en général (fichier \texttt{proba.v}) \item l'application aux flots de données aléatoires, à partir d'un espace élémentaire donné en paramètre (à cet égard, le système de modules de Coq est d'utilisation très commode), et le langage de formules \Lo (fichier \texttt{lo\_axiom.v}) \end{itemize} ~ Ces formalisations ont donc fait l'objet de deux fichiers Coq. Mais j'ai dû regrouper dans un seul fichier les modules sur les flots et ceux sur le langage de formules \Lo, car ils sont intimement liés. Voici comment ce fichier est structuré : ~ \begin{itemize} \item Signature \texttt{PROBA\_FLOTS\_PARAM} d'un module de paramètres : pour spécifier l'espace des éléments de flot (et au passage le type de données $\tau_0$ des éléments de flot). \item Foncteur \texttt{Principal} prenant en entrée un tel module de paramètres. \begin{itemize} \item Définition d'un flot (pas de sous-module) \item Sous-module \texttt{Lambda\_o} du langage de formules \Lo (qui se rapporte à \lo, d'où le nom du module). \item Sous-module \texttt{Proba\_flots} de probabilités sur les flots. \item Sous-module \texttt{Proba\_locale} : probabilités locales sur les flots (cf. \ref{s-proba-locale}) \end{itemize} \end{itemize} ~ Et alors, à partir de ces modules de base, je dégage une méthodologie particulière pour structurer la mécanisation d'un raisonnement probabiliste en Coq. ~ Pour écrire mes modules Coq, je tire parti des librairies standard sur les réels, les entiers naturels, les ordres bien fondés, les ensembles, etc. Tous mes modules Coq sont disponibles sur le Web (voir annexe page~\pageref{src}). \subsubsection{Axiomatisation des probabilités en Coq} J'ai d'abord formalisé en Coq, dans le fichier \texttt{proba.v}, la théorie des probabilités sur un ensemble quelconque. Cet <> de départ sur lequel je greffe des structures de probabilités est en fait un objet $U$ de sorte \texttt{Type} en Coq. En effet, j'ai besoin d'être aussi général que possible sur l'ensemble de base. Pourtant, lorsque j'ai besoin de parler des parties de cet ensemble, ainsi que de toute autre structure ensembliste par-dessus $U$, je me sers du module \texttt{Ensembles} de la librairie standard, qui définit les ensembles à partir des prédicats vérifiés par leurs éléments, prédicats de type $U \rightarrow \texttt{Prop}$ en Coq ; pour montrer l'égalité de deux ensembles, il est suffisant, grâce à l'axiome d'extensionnalité, de montrer que leurs prédicats caractéristiques sont équivalents. ~ Pour exprimer les définitions, axiomes et théorèmes de la théorie des probabilités, j'ai suivi l'approche de \cite{hurd}. En revanche, j'ai choisi de ne pas changer de terminologie entre la théorie des mesures et celle des probabilités. Tout au long de mon stage, je continue de parler de partie mesurable au lieu d'événement, etc. Certes, il aurait été intéressant, dans l'absolu, de différencier les deux terminologies afin de pouvoir savoir, dans une preuve, de quelle théorie l'on a réellement besoin. Cependant, en pratique, tous les raisonnements que j'ai faits ont nécessité un dépliage des définitions, de sorte qu'un renommage aurait entraîné une étape de dépliage inutile. J'obtiens donc correctement, et moyennant quelques gros théorèmes posés en axiomes\footnote{Par exemple le théorème de Carathéodory, dont la formalisation en HOL par Hurd \cite{hurd} a nécessité deux semaines.}, la définition d'une algèbre, et d'un espace mesuré\footnote{Dans les sources, je parle à tort d'<> pour désigner un espace mesuré.}. ~ \textbf{Remarque :} pour la définition de la tribu (ou $\sigma$-algèbre) engendrée par une famille de parties, je propose deux définitions Coq : l'une par formule ensembliste (\texttt{sigma} : l'intersection de toutes les tribus contenant cette famille), l'autre par induction Coq (\texttt{sigma2} : la plus petite tribu contenant cette famille). Je montre ensuite que ces deux définitions donnent les mêmes objets. \\ \texttt{~ \\Inductive sigma2 (U : Type) (G : Ensemble (Ensemble U)) : \\ Ensemble (Ensemble U) := \\ ~ \\ | sigma\_0 : forall (e : Ensemble U), \\ In (Ensemble U) G e -> In (Ensemble U) (sigma2 U G) e \\ ~ \\ | sigma\_vide : In (Ensemble U) (sigma2 U G) (Empty\_set U) \\ ~ \\ | sigma\_complement : forall (e : Ensemble U), \\ In (Ensemble U) (sigma2 U G) e -> \\ In (Ensemble U) (sigma2 U G) (Complement U e) \\ ~ \\ | sigma\_union : forall (e1 e2 : Ensemble U), \\ In (Ensemble U) (sigma2 U G) e1 -> In (Ensemble U) (sigma2 U G) e2 -> \\ In (Ensemble U) (sigma2 U G) (Union U e1 e2) \\ ~ \\ | sigma\_union\_denomb : forall (A : Familles\_parties.Famille\_parties U nat), \\ (forall n:nat, In (Ensemble U) (sigma2 U G) (A n)) -> \\ In (Ensemble U) (sigma2 U G) (Familles\_parties.Union U nat A). \\ ~ \\ ~ \\ Definition sigma (U:Type) (G: Ensemble (Ensemble U)) : \\ Ensemble (Ensemble U) := \\ let e := Ensemble U in let E := Ensemble e in \\ let F : Ensemble E := fun f:E => (Sigma\_algebre U f /\textbackslash{} Included e G f) in \\ Operations\_ensembles.Intersection e F. \\ ~ \\ Theorem sigma\_est\_sigma2 : forall (U : Type) (G : Ensemble (Ensemble U)), \\ sigma2 U G = sigma U G. \\ } ~ Par exemple, je définis l'espace des boréliens, en posant comme axiome l'existence de la mesure de Lebesgue : \\ \texttt{Definition Boreliens (E : Ensemble R) : Ensemble (Ensemble R) := \\ ~ sigma R (fun A => exists u:~ R, exists v:~ R, \\ Intersection R E A = Intervalle\_ferme u v). \\ ~ \\ Axiom Existe\_Lebesgue : \\ forall E : Ensemble R, exists lambda : Ensemble R -> R, \\ Espace\_mesurable R (Boreliens E) lambda /\textbackslash \\ forall u v : R, \\ u <= v -> Included R (Intervalle\_ferme u v) E -> \\ lambda (Intervalle\_ferme u v) = v - u. } ~ \textbf{Remarque :} pour construire la tribu borélienne sur un intervalle\footnote{Ces définitions me permettent même de construire un espace des boréliens sur une partie autre qu'un intervalle.} $I$ (noté \texttt{E} dans le code Coq), je ne me restreins pas aux parties de $I$. Je considère \emph{toutes} les parties de $\mathbb R$, et simplement en termes de mesurabilité et de mesure, je ne m'intéresse qu'à l'intersection avec $I$ des parties. On pourra obtenir des résultats farfelus comme celui-ci : si $Z$ est une partie de $\mathbb R$ non mesurable au sens de l'espace des boréliens sur tout $\mathbb R$ (on sait qu'il existe un tel $Z$, voir par exemple \cite{hurd}), alors, pour tout intervalle $I$, $Z \backslash I$ n'est pas mesurable au sens des boréliens sur $\mathbb R$, mais l'est au sens des boréliens sur $I$, car, intersecté avec $I$, c'est la partie vide ! \subsubsection{Les flots} Je considère comme un paramètre du développement l'ensemble $E$ des éléments de flot : c'est une clause \texttt{Parameter} de la signature \texttt{PROBA\_FLOTS\_PARAM}, qui permet en fait, grâce à la structure de foncteur \texttt{Principal} qui prend en entrée un module de cette signature, de créer des modules différents en fonction du type choisi pour les éléments de flot. Je définis les flots sous la forme la plus commune en informatique : la forme co-inductive, au lieu d'adopter l'approche mathématique d'une famille indicée par $\mathbb N$. Ceci me permet de considérer le \emph{conse} $::$ de manière structurelle, et non plus comme un alias. De plus, ceci permet de mieux modéliser la consommation d'un élément de flot. Pour utiliser la clause \texttt{CoInductive}, afin de définir mon type des flots dépendant du paramètre de type $E$, il a fallu que ce paramètre, que j'ai nommé \texttt{Element\_flot} en Coq, soit de sorte \texttt{Set} en Coq, et non de sorte \texttt{Type}. ~ Notons que \cite{lo} choisit d'emblée les réels pour l'ensemble $E$ des éléments de flot, tandis que \cite{hurd} choisit les booléens. En considérant $E$ comme un paramètre, je permets à l'utilisateur de se prononcer le plus tard possible, et je montre des propriétés très générales sur les flots et les probabilités sur les flots indépendamment de la nature de leurs éléments. \subsubsection{Langage de formules \Lo} Comme on l'a vu, je n'ai pas voulu mapper les structures du \lo vers les structures du Calcul des Constructions Inductives (CIC)\cite{cic} de Coq, afin de ne pas utiliser les règles de réduction du CIC sur les structures du langage \lo. Par conséquent, j'ai dû créer des types Coq spéciaux pour modéliser les types flèche et couple du \lo, au lieu d'utiliser les types fournis par Coq. (Par contre, pour les types de base, pas question de réinventer la roue.) Ces types sont simplement définis en Coq par des clauses \texttt{Variable} ; j'introduis ensuite, pour faciliter la lecture, des notations plus proches de celles de la grammaire. ~ Les relations spéciales $\xrightleftharpoons[\otimes]{}$ pour les projections $\mathsf{fst}, \mathsf{snd}$, $\xrightarrow[\triangleright]{}$ pour les applications et $\xrightarrow[\square]{}$ pour les expressions $\mathsf{sample}$ sont simplement définies par des clauses \texttt{Variable} et portent le nom, respectivement, de \texttt{Relation\_croix}, \texttt{Relation\_triangle}, \texttt{Relation\_carre}. Puis, je définis des notations afin, là encore, de me rapprocher de la grammaire. ~ A côté de ces relations, je définis un «raccourci» pour les formules permettant leur élimination : les formules de correction pour les projections, l'abstraction et le terme $\mathsf{prob}$. \begin{displaymath} \begin{array}{rccc} & \textbf{Notation} & \textbf{Notation Coq} & \textbf{Signification} \\ \\ \hline \\ \textbf{Couple} & c \otimes P & \texttt{Croix c P} & \forall a, \forall b : ~ a \xrightleftharpoons[\otimes]{c} b ~ \Rightarrow P(a, b) \\ \\ \textbf{Abstraction} & f \triangleright P & \texttt{Triangle f P} & \forall x, \forall y : ~ x \xrightarrow[\triangleright]{f} y ~ \Rightarrow ~ P(x, y) \\ \\ \textbf{Terme }\mathsf{prob} & m ~ \square ~ P & \texttt{Carre m P} & \forall s, \forall y, \forall s' : s \xrightarrow[\triangleright]{m} \langle x, s' \rangle ~ \Rightarrow ~ P(s, y, s') \\ \end{array} \end{displaymath} En réalité, j'ai commencé mon stage en introduisant ces formules \emph{avant même} de parler des relations spéciales. Ceci explique l'origine des symboles $\otimes, \triangleright, \square$ sous les flèches. Quant à l'origine de ces symboles même pour les formules de correction ci-dessus, on pourrait l'expliquer par leur similitude avec les symboles des types correspondants : $\otimes$ pour le type couple $\times$, mais aussi $\triangleright$ pour le type flèche $\rightarrow$, et enfin $\square$ pour le type $\bigcirc$. Pour ce dernier symbole, le lien avec le symbole du type est difficile à voir. Mais il suffit de se dire que dans les trois cas, on arrive au symbole de formule par une \emph{déformation} du symbole du type correspondant. Cela illustre à quel point sont similaires le typage et la génération des formules. ~ Par la suite, il a fallu rajouter des formules de terminaison : par exemple, pour la formule de terminaison de l'application d'une abstraction (qui est une partie de la formule de correction de l'abstraction), j'introduis, pour une abstraction $f$ et un prédicat $P(x)$ portant sur l'argument $x$ de l'abstraction, le terme Coq \texttt{Terminaison\_triangle f P}, correspondant à la formule «si $P(x)$ est vérifiée, alors l'application $f(x)$ termine» : \begin{displaymath} \forall x : ~ P(x) ~ \Rightarrow ~ \exists y : ~ x \xrightarrow[\triangleright] f y \end{displaymath} J'ai défini de même les termes Coq \texttt{Terminaison\_croix} et \texttt{Terminaison\_carre}. Enfin, je combine terminaison et correction en introduisant des termes Coq tels que \texttt{Double\_carre m P Q} correspondant à \texttt{Terminaison\_carre m P /\textbackslash{} Carre m Q}. ~ Toutes ces définitions servent à rendre la formule relativement plus lisible. De plus, comme les formules générées par $\Pi$ sont, pour la plupart, sous cette forme, un éventuel changement de leur implémentation sous Coq n'affecterait pas la validité des formules générées par le transformateur $\Pi$, sous réserve que l'implémentation sous Coq de ces définitions soit elle-même valide. ~ Cependant, pour pouvoir modéliser correctement le comportement des programmes en \lo, il a fallu introduire des axiomes cruciaux : ~ \begin{itemize} \item des axiomes de fonctionnalité, exprimant l'unicité sous réserve d'existence, du résultat d'une fonction, ou d'un échantillonnage \emph{à flot fixé} : \begin{displaymath} \forall c, \forall a_1, \forall a_2, \forall b_1, \forall b_2 : ~ a_1 \xrightleftharpoons[\otimes]c b_1 ~ \land ~ a_2 \xrightleftharpoons[\otimes]c b_2~ \Rightarrow ~ a_1 = a_2 ~ \land ~ b_1 = b_2 \end{displaymath} \begin{displaymath} \forall f, \forall x, \forall y_1, \forall y_2 : ~ x \xrightarrow[\triangleright]f y_1 ~ \land ~ x \xrightarrow[\triangleright]f y_2~ \Rightarrow ~ y_1 = y_2 \end{displaymath} \begin{displaymath} \forall m, \forall s, \forall y_1, \forall y_2, \forall s'_1, \forall s'_2 : ~s \xrightarrow[\square]m \langle y_1, s'_1 \rangle ~ \land ~ s \xrightarrow[\square]m \langle y_2, s'_2 \rangle ~ \Rightarrow ~ y_1 = y_2 ~ \land ~ s'_1 = s'_2 \end{displaymath} ~ \item un axiome énonçant que le flot de sortie d'un échantillonnage est une queue du flot d'entrée. \end{itemize} \subsubsection{Probabilités sur les flots} Pour la définition de l'espace des flots, j'ai d'abord adapté la définition suivante de \cite{hurd}, et je l'ai mise en \oe uvre en Coq. J'ai ensuite appliqué la théorie des probabilités à cet espace. \begin{defin}[Espace des flots] Soit $E$ un ensemble non vide, l'ensemble des éléments de flot. Supposons que l'on dispose d'un espace de probabilités $(\mathcal E, \mu)$ sur $E$, l'espace des éléments de flot. Alors, on définit l'espace des flots sur $\mathcal E$ comme suit : \begin{itemize} \item La tribu $\mathcal E ^\infty$ des flots sur $\mathcal E$ est la $\sigma$-algèbre engendrée par les rectangles de flots (c'est-à-dire les flots dont un nombre fini d'extractions est dans un produit fini d'espaces $\mathcal E$-mesurables). \begin{displaymath} \mathcal E ^ \infty = \sigma \left\{ \left\{ \varphi \in E ^ \mathbb N : ~ \forall n < N, \varphi_n \in E_n \right\} ; ~ N \in \mathbb N, ~ E_1, \dots, E_N \in \mathcal E \right\} \end{displaymath} \item La mesure $\mu^\infty$ des flots sur $\mathcal E$ selon la mesure $\mu$ est la mesure qui vaut, pour un rectangle formé par $N$ ensembles $E_1, \dots, E_n$ $\mathcal E$-mesurables, le produit des mesures des $E_i$ au sens de la mesure $\mu$ sur les ensembles d'éléments de flot. \begin{displaymath} \forall N \in \mathbb N, \forall E_1, \dots, E_n \in \mathcal E : ~ \mu ^ \infty \left\{ \varphi \in E ^ \mathbb N : ~ \forall n < N, \varphi_n \in E_n \right\} = \prod_i E_i \end{displaymath} \end{itemize} \end{defin} L'existence d'une telle mesure se démontre comme pour la mesure de Lebesgue ; pour ma part, je l'ai posée en axiome. L'axiome de la mesure d'un rectangle exprime la propriété que deux extractions distinctes sont indépendantes. \subsection{Probabilités sur des événements de programme} \label{s-proba-locale} Reprenons l'exemple de la distribution de Bernoulli. \begin{displaymath} \lambda p. ~ \mathsf{prob} ~ \mathsf{sample} ~ x ~ \mathsf{from} ~ \mathsf{prob} ~ \mathcal S ~ \mathsf{in} ~ x \leqslant p \end{displaymath} Comment énoncer formellement qu'une fois ce terme appliqué sous le paramètre $p$, la probabilité que j'aie un échantillonnage me retournant le résultat $\mathsf{true}$ est $p$ ? Il y a deux façons de le faire : ~ \begin{itemize} \item soit écrire formellement la mesure de l'ensemble des flots $\sigma$ vérifiant que l'échantillonnage du terme $\mathsf{prob}$ sous le flot d'entrée $\sigma$ donne $\mathsf{true}$ : \begin{displaymath} \mu^\infty \left\{ \sigma \in E^\mathbb N : ~ \exists y, \exists \sigma' : ~ \sigma \xrightarrow[\square]{} \langle y, \sigma' \rangle ~ \land ~ y = \mathsf{true} \right\} = p \end{displaymath} Pour raisonner avec cette probabilité <>, on procède en deux étapes : \begin{enumerate} \item D'abord, on se ramène à un mesurable <>, c'est-à-dire que l'on montre que l'ensemble à mesurer s'exprime comme un ensemble mesurable de l'espace des flots. \item Ensuite, on calcule la mesure de cet ensemble à partir de l'axiome sur la mesure $\mu^\infty$. \end{enumerate} ~ \item soit parler de ce que j'ai appelé \emph{probabilité locale} sur le flot $s$. Je n'ai pas formalisé mathématiquement ce concept, mais je l'ai introduit en tant qu'outil de raisonnement en Coq. On écrira en Coq : \\ \texttt{forall s, Carre s (fun y t => Proba\_locale s (y = true) = p)} \\ qui exprime que si $s$ est passé en flot d'entrée, alors la probabilité qu'il donne un échantillon $y = \mathsf{true}$ est p. Cette formule exprime en fait une probabilité sur un objet \emph{déjà défini} et dont on considère qu'il est distribué comme un flot d'entrée de tout le programme. Mais on doit alors supposer que l'on ne dispose d'\emph{aucune autre propriété} sur le flot. A cet égard, le manque de formalisme autour de cette notion fait qu'il faut la manipuler avec circonspection. ~ Toutefois, la probabilité locale est surtout utile lorsque l'on raisonne avec des distributions de probabilité auxiliaires. Par exemple, beaucoup d'algorithmes de simulation ont besoin de simuler localement la loi de Bernoulli (comme la loi binomiale, fig.~\ref{fig-coqide-binomial} p.~\pageref{fig-coqide-binomial}). A cet égard, la probabilité locale permet d'exprimer localement que tel fragment de code \lo simule la loi de Bernoulli . En réalité, on peut dire que la probabilité locale sur un flot $s$ exprime une probabilité sur le flot d'entrée $\sigma$ de tout le programme, \emph{conditionnée} par les consommations qui ont eu lieu sur $\sigma$ pour obtenir $s$. ~ De plus, on constate qu'aucune mention n'est faite des opérations sur les flots. Mais pour des algorithmes à récursivité probabiliste comme la simulation de la loi géométrique, il faut pouvoir raisonner ainsi, sur les flots eux-mêmes, donc cette approche est inadaptée pour ce genre de programme. En outre, on aura remarqué que le terme \texttt{Proba\_locale} est <> le carré : donc, cela suppose l'existence du résultat $y$ et du flot de sortie $s'$. C'est dire que la probabilité locale ne peut être utilisée que dans un raisonnement de correction partielle, en supposant la terminaison. ~ Pour raisonner avec les probabilités locales, j'ai introduit deux axiomes : \\ \begin{ax}[Probabilité locale des flots équivalents] \label{ax-locale-equiv} Sous le même flot d'entrée $s$, deux propriétés équivalentes ont même probabilité locale. \end{ax} ~ \\ \begin{ax}[Probabilité locale et globale] \label{ax-locale-globale} Pour un prédicat $\psi(s)$, la probabilité locale sur le flot $s$ que $s$ vérifie $\psi(s)$ est la mesure $\mu^\infty \left\{ s : \psi(s) \right\}$ \end{ax} ~ \\ On constate qu'ils constituent des étapes précédant celles du calcul de probabilité <> avec $\mu^\infty$ : dans un premier temps, on utilise le premier axiome pour réécrire la propriété dont on veut calculer la probabilité sous la forme $\psi(s)$, puis grâce au deuxième axiome, on se ramène au premier cas (global). \end{itemize} ~ \textbf{Remarque :} lorsque je raisonne sur un programme en \lo, je n'ai jamais besoin de considérer des tribus sur autre chose que les flots ou les éléments de flot. En effet, pour calculer une probabilité, je me ramène toujours à un ensemble de flots à mesurer. \subsection{Structure d'une preuve sur un algorithme probabiliste} Pour prouver en Coq une propriété sur un programme en \lo, il est nécessaire de suivre une discipline toute particulière en matière de structure du module de preuve, que j'ai mise en place au travers des exemples de preuves formelles que j'ai menés à bien, surtout pour des algorithmes récursifs comme pour la loi binomiale ou la loi géométrique. ~ Le transformateur $\Pi$ produit un fichier Coq contenant \begin{itemize} \item la déclaration des variables libres du programme \item la formule $\Pi$ correspondant au programme, sous la forme d'une hypothèse (clause \texttt{Hypothesis}) \end{itemize} sous la forme d'une section Coq comme sur la figure~\ref{fig-pcaml-bernoulli} page~\pageref{fig-pcaml-bernoulli}. ~ Ce fichier doit être complété en rajoutant les \emph{hypothèses sur les variables libres} du programme, évidemment, car $\Pi$ ne sait rien \emph{a priori} sur les variables libres, qui en fait représentent simplement l'utilisation d'algorithmes auxiliaires. D'ailleurs, cela permet d'avoir une certaine forme de \emph{compositionnalité} du raisonnement de ce point de vue-là : dans ce genre de situation, on n'indique que les propriétés dont on a besoin sur ces algorithmes auxiliaires. Mais ces hypothèses ne sont pas nécessairement des formules du langage \Lo telles que les produirait le transformateur $\Pi$. Il peut très bien s'agir de formules probabilistes, avec la mesure $\mu^\infty$, ou même, et c'est ici qu'il est intéressant d'en reparler, la probabilité locale, car elle permet par exemple de parler de l'algorithme auxiliaire uniquement de manière qualitative, comme une «spécification», sans parler de la consommation du flot par exemple. C'est l'approche souvent choisie lorsque l'on utilise de façon auxiliaire un algorithme simulant la loi de Bernoulli, par exemple pour la loi binomiale (voir figure~\ref{fig-coqide-binomial}, page~\pageref{fig-coqide-binomial}). ~ Une fois indiquées toutes les hypothèses, que ce soit les hypothèses sur les algorithmes auxiliaires ou la formule $\Pi$ du programme, on peut alors énoncer et prouver la ou les propriétés voulues sur le programme. Ces propriétés peuvent traiter de la terminaison seulement, de la correction sous hypothèse de terminaison seulement, ou des deux à la fois. En tous cas, il faut, autant que possible, \emph{séparer formules de terminaison et formules de correction} et commencer par prouver les formules de \emph{terminaison}. En effet, certaines preuves de formules de correction exigent que la terminaison ait été prouvée. ~ On aboutira donc à la structure suivante pour un module de preuve : \begin{enumerate} \item Variables libres (données par $\Pi$) \item Hypothèses sur les variables libres \item Variable du programme (donnée par $\Pi$), représentant l'algorithme sur lequel porteront les preuves \item Hypothèse sur le programme : formule donnée par le transformateur $\Pi$ \item Preuves de terminaison : prouver des conditions suffisantes déterministes pour qu'un algorithme termine (on ne calculera pas ici la <>), ou alors ramener ces conditions à des ensembles mesurables de flots (réécrire cet événement de programme sous la forme d'une propriété sur les flots d'entrée définissant un ensemble mesurable) \item Preuves de correction : \begin{itemize} \item si l'on veut prouver des conditions déterministes sur les paramètres, ou si l'on raisonne avec les probabilités locales, on peut raisonner directement \item si l'on raisonne sur des conditions probabilistes avec la probabilité <>, ramener les propriétés de correction à des ensembles mesurables de flots \end{itemize} \item Preuves de mesurabilité des ensembles à mesurer \item Mesures de ces ensembles \label{enum-correction-f} \end{enumerate} Ainsi, on effectue deux séparations : \begin{itemize} \item séparer terminaison et correction \item séparer mesurabilité et probabilité \end{itemize} Ces séparations rendent les preuves plus claires et permettent également de réutiliser des fragments de preuves concernant terminaison ou correction, dans d'autres preuves sur d'autres programmes. En outre, elles permettent de rendre \emph{indépendants} les preuves sur les programmes, et des preuves que l'on pourra considérer comme «annexes» (des lemmes, en quelque sorte), sur des structures «intermédiaires» dont les propriétés ne parlent plus du comportement du programme. De plus, de telles structures peuvent également apparaître dans d'autres occasions, et à ce titre, elles pourront être définies et traitées dans d'autres fichiers Coq que l'on chargera dynamiquement. Par exemple, on trouvera dans le fichier \texttt{lo\_axiom.v} une section \texttt{Ensf\_ord} qui définit de manière générale un ensemble et un ordre bien fondé sur les flots ; j'ai rajouté cette structure au moment où j'ai voulu prouver la correction d'un algorithme de simulation de la loi géométrique (cf. \ref{s-geom} pour plus de détails), mais je l'ai inclus dans le fichier \texttt{lo\_axiom.v} car je pense que cette structure générale peut être utilisée dans d'autres contextes. \subsection{Technique : comment se débrouiller avec les formules $\Pi$ dans Coq} \label{s-tech} Les formules générées par le transformateur $\Pi$ sont souvent très longues : ne serait-ce que pour la simulation de la loi de Bernoulli, on se reportera à la figure \ref{fig-pcaml-bernoulli}, page \pageref{fig-pcaml-bernoulli}, pour s'en convaincre ! Aussi m'a-t-il paru nécessaire d'inclure dans ce rapport quelques éléments techniques permettant l'utilisation des modules Coq que j'ai écrits pour prouver des propriétés sur d'autres algorithmes probabilistes, et décrivant en particulier l'usage des \emph{tactiques} qui a été mien pour mes exemples de preuves. Toutefois, cette section rend compte de l'incomplétude de mon travail en matière d'\emph{automatisation} de la preuve : tous les éléments que je vais donner ici pourraient donner lieu à l'écriture de tactiques en \ltac, le langage des tactiques de Coq (cf. \cite{cic}, chap. 7, «Tactics and Automation»). ~ Tout d'abord, je déplie toutes les définitions des termes Coq du triangle, carré, croix, etc. en utilisant la tactique \texttt{generalize} sur toutes les hypothèses fournies (ce qui me les injecte dans le but à prouver), puis en effectuant \texttt{unfold} sur le but pour chaque terme, et enfin \texttt{intros} pour réintroduire les hypothèses dépliées. ~ Les formules $\Pi$ contiennent beaucoup de conjonctions et de quantifications existentielles (toutefois souvent cachées sous des universels). J'ai écrit une tactique très utile, \texttt{casser\_les\_cailloux}, permettant : \begin{itemize} \item de remplacer l'hypothèse \texttt{P /\textbackslash{} Q} par les hypothèses \texttt P et \texttt Q \item de remplacer l'hypothèse \texttt{exists x, P} par les hypothèses \texttt x et \texttt P \end{itemize} ~ Le gros du travail de manipulation a lieu lors des «réductions» : dès lors que j'ai deux hypothèses des formes suivantes (correspondant à la relation $s \xrightarrow[\square] m \langle y, t \rangle$) : \begin{itemize} \item \texttt{ H1 : forall s y t, \{ s \textgreater{}\textgreater{} m \~{} y \textgreater{}\textgreater{} t \} -> P } \item \texttt{ H2 : \{ s \textgreater{}\textgreater{} m \~{} y \textgreater{}\textgreater{} t \} } \end{itemize} Je peux alors obtenir \texttt P en exécutant la tactique : \begin{center} \texttt{generalize (H1 \_ \_ \_ H2) ; intros} \end{center} De même, dès lors que j'ai deux hypothèses des formes suivantes (correspondant à la relation $x \xrightarrow[\triangleright]f y$) : \begin{itemize} \item \texttt{ H1 : forall x y, x -{}- f -{}-> y -> P } \item \texttt{ H2 : x -{}- f -{}-> y } \end{itemize} Je peux alors obtenir \texttt P en exécutant la tactique : \begin{center} \texttt{generalize (H1 \_ \_ H2) ; intros} \end{center} ~ En combinant toutes ces tactiques, je peux en fait «exécuter le programme pas à pas» en décrivant en logique les différentes étapes d'exécution. ~ Il serait intéressant d'automatiser ces tactiques avec \ltac : en effet, dans mes raisonnements, je perds beaucoup de temps à chercher les numéros des hypothèses correspondantes, d'une part parce qu'elles sont très nombreuses et très complexes, d'autre part parce qu'une modification de la preuve en amont «décale» complètement toute la numérotation. Mais il faut faire attention aux points fixes : une tactique d'automatisation mal écrite peut faire boucler le raisonnement ! \clearpage \section{Application : distributions simples}\label{s-3} La formalisation que j'ai réalisée en Coq de la théorie des probabilités ainsi que du langage de formules \Lo m'a permis de traiter des exemples de lois simples : \begin{itemize} \item des distributions «de base» qui se simulent par des algorithmes non récursifs, comme la loi de Bernoulli ou la loi exponentielle \item la loi binomiale, se simulant par un algorithme à récursivité déterministe \item la loi géométrique, par un algorithme à récursivité probabiliste \end{itemize} ~ Pour traiter ces simulations, je me suis placé dans le cadre de \cite{lo} : des flots de réels uniformément distribués sur $[0, 1]$. On supposera donc que l'on dispose des réels, ainsi que des entiers naturels (quasi incontournables en Coq), avec leurs opérations arithmétiques et relations élémentaires. ~ \textbf{Remarque :} j'ai préféré traiter les boréliens sur $[0, 1]$ au lieu de $]0, 1]$ car il m'a semblé plus simple de raisonner avec des inégalités larges. Toutefois, nous verrons que cela m'a posé quelques problèmes pour la loi exponentielle. ~ Tous les exemples cités ici sont disponibles sur mon site Web, sous-dossier \texttt{coq} (pour des informations sur le téléchargement, voir annexe page \pageref{src}). \subsection{Simulations par algorithmes non récursifs} \subsubsection{Loi de Bernoulli}\label{s-bernoulli} La loi de Bernoulli est une des lois de base en probabilités, et même en statistiques. C'est même une des lois fondamentalement utilisées, et peut-être même la brique de base, pour la représentation des lois discrètes (ce qui n'a pas échappé à \cite{hurd}, en considérant des flots de booléens suivant la loi de Bernoulli de paramètre $1/2$). Du point de vue de la simulation, l'algorithme est très simple, et ce sont ces deux arguments, importance et simplicité, qui m'ont conduit à citer cet exemple en de nombreux points de mon rapport. En \lo, on écrit donc : \begin{displaymath} \lambda p. ~ \mathsf{prob} ~ \mathsf{sample} ~ x ~ \mathsf{from} ~ \mathsf{prob} ~ \mathcal S ~ \mathsf{in} ~ x \leqslant p \end{displaymath} Lors du passage au transformateur $\Pi$, on obtient une formule très «lourde» en comparaison de la simplicité du code \lo représentant l'algorithme, comme on peut le constater sur les figures \ref{fig-pcaml-bernoulli} (page~\pageref{fig-pcaml-bernoulli}) et \ref{fig-coqide-bernoulli-hyp} (page~\pageref{fig-coqide-bernoulli-hyp}). \begin{figure}[p] \begin{center} \mbox{\epsfig{file=pcaml-bernoulli.eps}} \\ ~ \\ \caption{La formule générée par le transformateur $\Pi$ pour la simulation de la loi de Bernoulli, prête à être copiée dans Coq.} \label{fig-pcaml-bernoulli} \end{center} \end{figure} \begin{figure}[p] \begin{center} \mbox{\epsfig{file=coqide-bernoulli-hyp.eps}} \\ ~ \\ \caption{La même formule, copiée dans Coq, et imprimée par le \emph{pretty-printer} de Coq.} \label{fig-coqide-bernoulli-hyp} \end{center} \end{figure} On veut donc prouver que cet algorithme simule la loi de Bernoulli. Il faut donc prouver les deux : \begin{theo}[Loi de Bernoulli, probabilité du $\mathsf{true}$] Soit $p \in [0, 1]$. La mise en \oe uvre de l'algorithme ci-dessus avec le paramètre $p$ donne un algorithme probabiliste tel que si l'on l'échantillonne, alors il termine et on obtient $\mathsf{true}$ avec la probabilité $p$. \end{theo} \begin{theo}[Loi de Bernoulli, probabilité du $\mathsf{false}$] Soit $p \in [0, 1]$. La mise en \oe uvre de l'algorithme ci-dessus avec le paramètre $p$ donne un algorithme probabiliste tel que si l'on l'échantillonne, alors il termine et on obtient $\mathsf{false}$ avec la probabilité $1 - p$. \end{theo} Pour ma part, j'ai prouvé le premier théorème, dans le fichier \texttt{bernoulli.v}. Mais comme il s'agissait d'un des premiers algorithmes que j'ai prouvés, je n'ai pas dissocié terminaison et correction. Toutefois, on pourra constater, au vu de la figure~\ref{fig-coqide-bernoulli-demo}, page ~\pageref{fig-coqide-bernoulli-demo}, une «coupure» dans la preuve du théorème, entre terminaison et correction, signalée par un simple commentaire. C'est ce qui m'a donné l'\emph{intuition} de structurer mes raisonnements (intuition confirmée par la situation analogue que j'ai rencontrée ensuite pour la loi exponentielle), que j'ai concrétisée plus tard pour les raisonnements sur la loi binomiale et la loi géométrique. \begin{figure}[p] \begin{center} \mbox{\epsfig{file=coqide-bernoulli.eps}} \\ ~ \\ \caption{Simulation de la loi de Bernoulli prête à être prouvée sous CoqIDE} \label{fig-coqide-bernoulli} \end{center} \end{figure} \begin{figure}[p] \begin{center} \mbox{\epsfig{file=coqide-bernoulli-demo.eps}} \\ ~ \\ \caption{Preuve en cours sous CoqIDE de la simulation de la loi de Bernoulli} \label{fig-coqide-bernoulli-demo} \end{center} \end{figure} Pour démontrer ce théorème, j'ai choisi de le faire par probabilités locales (cf. section \ref{s-proba-locale}). En effet, comme on l'a vu, la loi de Bernoulli est souvent utilisée de manière auxiliaire dans d'autres lois. J'énonce le théorème en Coq comme suit : \\ \texttt{Theorem Concl\_bernoulli : \\ Double\_triangle bernoulli (fun \_ => True) (fun p f => \\ 0 <= p <= 1 -> \\ Double\_carre f (fun \_ => True) (fun s y \_ => \\ Proba\_locale s (y = true) = p) \\ ). \\ } Les termes Coq \texttt{Double\_triangle}, \texttt{Double\_carre} expriment le fait que je n'aie pas séparé terminaison et correction. Les termes Coq \texttt{(fun \_ => True)} indiquent que l'algorithme termine toujours. La terminaison se démontre facilement, en dépliant les définitions et en «suivant» les réductions à la manière de la technique développée à la section \ref{s-tech}. Pour la correction, je me ramène à mesurer l'ensemble des flots $\alpha :: \varphi$ tels que la tête $\alpha \leqslant p$. Pour cela, j'ai recours à un lemme, \texttt{Bernoulli1}, que j'ai démontré dans le fichier \texttt{lo\_axiom.v} (mais que j'aurais pu inclure dans le fichier \texttt{bernoulli.v}), selon lequel cet ensemble de flots est de mesure $p$. Donc, en injectant simplement, par une tactique \texttt{rewrite} (cf. fig.~\ref{fig-coqide-bernoulli-demo} p.~\pageref{fig-coqide-bernoulli-demo}), l'égalité fournie par ce lemme, j'obtiens alors une égalité de la forme \texttt{Proba\_locale s P = Ef\_mesure Q}, où \texttt Q est une fonction (prédicat à une variable). Alors, je réécris \texttt{Ef\_mesure Q = Proba\_locale s (Q s)}, en utilisant l'axiome de la probabilité locale et globale (\ref{ax-locale-globale}, page \pageref{ax-locale-globale}), et enfin, je me ramène à montrer que les propriétés \texttt P et \texttt{(Q s)} sont équivalentes (en appliquant \ref{ax-locale-equiv}, page \pageref{ax-locale-equiv}). ~ J'ai omis de démontrer le second théorème, concernant la probabilité du $\mathsf{false}$. Toutefois, on pourrait le faire par probabilité locale (en supposant la terminaison) et en disant que je mesure le complémentaire de l'ensemble des flots tels que j'obtienne $\mathsf{true}$. \subsubsection{Loi exponentielle de paramètre 1}\label{s-expo} La loi exponentielle de paramètre 1 se simule par un algorithme similaire à celui de la loi de Bernoulli. En \lo le code correspondant est : \begin{displaymath} \mathsf{prob} ~ \mathsf{sample} ~ x ~ \mathsf{from} ~ \mathsf{prob} ~ \mathcal S ~ \mathsf{in} ~ 0 - \ln x \end{displaymath} On veut prouver que cet algorithme simule la loi exponentielle de paramètre 1. Il faut donc prouver le : \begin{theo}[Loi exponentielle de paramètre 1] \label{theo-expo} Si on échantillonne l'algorithme probabiliste ci-dessus, alors pour tout $p \geqslant 0$, la probabilité qu'il termine et renvoie une valeur $y \geqslant p$ est égale à $e^{-p}$. \end{theo} Ce théorème est suffisant, car il décrit la loi par sa \emph{fonction de distribution}. Cependant, un problème va se poser pour la terminaison : étant donné que j'autorise qu'une valeur de flot soit nulle, je risque de vouloir évaluer un $\ln 0$, où le zéro est la valeur de la tête du flot. Je considère donc que si le flot a une tête strictement positive, alors le programme termine. Pour ma part, j'ai montré une proposition légèrement plus faible : l'algorithme termine pour les flots de tête non nulle, et la probabilité, \emph{conditionnée par la terminaison}, que la valeur retournée soit plus grande que $p$ est $e^{-p}$. On pourrait par la suite compléter cette démonstration en montrant que l'ensemble de terminaison est de probabilité 1. ~ La terminaison sur l'ensemble des flots de tête non nulle se fait par «extraction» de l'hypothèse correspondante (en gros, une tactique \texttt{apply}) et également en suivant les réductions au passage. Pour la correction, je fais exactement comme pour la loi de Bernoulli. Pour l'énoncer, j'utilise les probabilités locales ; pour la démontrer, j'ai recours à un lemme, \texttt{Expo1}, selon lequel la mesure de l'ensemble des flots $\alpha :: \varphi$ tels que $0 - \ln \alpha \geqslant p$ est $e^{-p}$. Je m'y ramène comme pour Bernoulli, par réécriture d'égalités. Le point plus subtil est celui de la démonstration du lemme \texttt{Expo1}. En gros, je veux transformer l'inégalité $- \ln \alpha \geqslant p$ en $\alpha \leqslant e^{-p}$, «en appliquant le logarithme des deux côtés de la deuxième inégalité», afin de me ramener au lemme \texttt{Bernoulli1} (ce qui, au passage, montre l'intérêt de l'avoir placé directement dans le fichier \texttt{lo\_axiom.v} au lieu de le cantonner dans \texttt{bernoulli.v}) pour prouver que la mesure de l'ensemble est $e^{-p}$. Mais pour effectuer cette transformation, je dois m'assurer que $\alpha > 0$. C'est ici que je me sers d'un lemme (que j'ai démontré en Coq) selon lequel en retirant un point (ici le point $0$) d'un intervalle, on ne change pas sa mesure. Pour montrer le théorème \ref{theo-expo} de façon plus rigoureuse avec les probabilités globales, on pourrait aussi se servir de ce lemme. \subsection{Récursivité déterministe : loi binomiale}\label{s-binomiale} En impératif, la loi binomiale de paramètres $n$ et $p$ est simulée par une «boucle \emph{for}» : \\ \verb+procedure +$binomial$\verb+ (+$p$\verb+ : R, +$n$\verb+ : nat) : nat+\\ \verb+begin+\\ \verb+ +$result$\verb+ := 0;+ \\ \verb+ for +$i$\verb+ = 1 to +$n$ \\ \verb+ do+ \\ \verb+ if +$bernoulli$\verb+(+$p$\verb+) then +$result$\verb+ := +$result$\verb- + 1;-\\ \verb+ done;+ \\ \verb+ return +$result$\verb+;+\\ \verb+end.+\\ qui s'écrit, en \lo : ~ $\lambda p : \mathsf R . ~ \mathsf{fix} ~ boucle : \mathsf{nat} \rightarrow \bigcirc ~ \mathsf{nat} . ~ \lambda n : \mathsf{nat} .$\\ \verb+ + $\mathsf{if} ~ n = 0$ \\ \verb+ + $\mathsf{then} ~ \mathsf{prob} ~ 0 $ \\ \verb+ + $\mathsf{else} ~ \mathsf{prob} ~ $ \\ \verb+ + $\mathsf{sample} ~ result_{prev} ~ \mathsf{from} ~ boucle ~ (n - 1) ~ \mathsf{in}$ \\ \verb+ + $\mathsf{sample} ~ b ~ \mathsf{from} ~ bernoulli ~ p ~ \mathsf{in}$ \\ \verb+ + $\mathsf{if} ~ b ~ \mathsf{then} ~ result_{prev} + 1 ~ ~ \mathsf{else} ~ result_{prev} \ $ \\ \begin{figure}[p] \begin{center} \mbox{\epsfig{file=coqide-binomial.eps}} \\ ~ \\ \caption{Simulation de la loi binomiale : hypothèses nécessaires à la preuve} ~ \\ \label{fig-coqide-binomial} \emph{La variable libre \texttt{bernoulli} représente l'algorithme de simulation de la loi de Bernoulli, utilisé comme algorithme auxiliaire, c'est pourquoi on a mis en évidence, en les entourant grossièrement, les hypothèses \texttt{Hyp\_bernoulli} et \texttt{Hyp\_bernoulli\_mesurable} sur cette variable.} \end{center} \end{figure} Comme on le constate dans cet algorithme, apparaît une variable libre, $bernoulli$ : en fait, cet algorithme fait appel à une simulation de la loi de Bernoulli comme loi auxiliaire. Il faut donc spécifier, en Coq, les hypothèses nécessaires à propos de cette variable $bernoulli$ : selon la figure~\ref{fig-coqide-binomial}, page~\pageref{fig-coqide-binomial}, j'indique que cette variable est un algorithme prenant en paramètre un réel $p$ et tel que sous ce paramètre, il simule la loi de Bernoulli ; je formule cette dernière propriété \emph{en utilisant les probabilités locales}, et \emph{sans avoir à spécifier comment l'algorithme utilise le flot} de données aléatoires. ~ A partir de ces hypothèses, on veut montrer le : \begin{theo}[Loi binomiale] Soit $p \in [0, 1]$. Alors, sous le premier paramètre $p$, et pour tous entiers naturels $n$ et $r \leqslant n$, si $n$ est passé en second paramètre, alors l'échantillonnage termine toujours et la probabilité que le résultat soit $r$ est $\left(\begin{array}{l}n \\ r\end{array} \right) p^r (1 - p)^{n - r}$. \end{theo} Ici, fort de mes expériences lors de la démonstration de la simulation des lois de Bernoulli et exponentielle, j'ai commencé à dégager une structure dans mon module de preuve : j'ai clairement séparé terminaison et correction. Voici les trois énoncés Coq que j'ai isolés : ~ \texttt{Theorem Concl\_binomial\_termine : \\ Double\_triangle binomial (fun \_ => True) (fun p binp => \\ 0 <= p -> p <= 1 -> \\ Double\_triangle binp (fun \_ => True) (fun n f => \\ Terminaison\_carre f (fun \_ => True) \\ )). \\ ~ \\ Axiom Concl\_binomial\_mesurable : \\ Triangle binomial (fun p binp => 0 <= p -> p <= 1 -> \\ Triangle binp (fun n f => \\ Carre f (fun \_ y \_ => \\ forall r:nat, (Le r n) -> In \_ Espace\_flots (fun \_ => y = r) \\ ))). \\ ~ \\ Theorem Concl\_binomial : \\ Triangle binomial (fun p binp => 0 <= p -> p <= 1 -> \\ Triangle binp (fun n f => \\ Carre f (fun s y t => \\ forall r:nat, (Le r n) -> \\ Proba\_locale s (y = r) = C n r * p \^{} r * (1 - p) \^{} (n - r) \\ ))).} ~ Comme on l'aura constaté, j'ai posé en axiome le second énoncé. Mais on pourrait le démontrer en suivant, en fait, la structure de la preuve du théorème \texttt{Concl\_binomial}. ~ Pour démontrer la terminaison, j'ai besoin d'exhiber deux fois la preuve de bonne fondation de la relation $<$ (\texttt{Lt}) sur les entiers naturels : une fois pour prouver que \texttt{binp} (la boucle elle-même) termine, et une fois pour prouver que \texttt{f} (le terme $\mathsf{prob}$ contenu dans la boucle) termine. ~ Pour démontrer la correction, il faut d'abord démontrer un lemme : la sortie de l'échantillonnage est toujours inférieure ou égale au paramètre $n$. En effet, je souhaite pouvoir raisonner \emph{par induction sur $n$} pour prouver le théorème de correction, or celui-ci exige que $r \leqslant n$. La raison de cette exigence est que les coefficients binomiaux de Coq (le terme \texttt{C n r}) sont mal définis pour $r > n$. La convention en mathématiques est qu'ils vaillent zéro, mais ce n'est pas le cas en Coq. C'est d'ailleurs la raison pour laquelle, pour montrer ce théorème de correction, j'ai besoin, dans le cas inductif, de distinguer trois cas : \begin{itemize} \item le cas $r = n$ : tous les échantillonnages de Bernoulli donnent $\mathsf{false}$, correspondant à une probabilité $(1 - p)^n$, le coefficient binomial valant 1. \item le cas $r = 0$ : tous les échantillonnages de Bernoulli donnent $\mathsf{true}$, correspondant à une probabilité $p^n$, le binomial valant 1. \item le cas $0 < r < n$ : les deux branches du test sont explorées. Ce cas entraîne l'utilisation de la formule de Pascal ( définie dans la librairie standard de Coq) : \begin{displaymath} \left( \begin{array}{l} n \\ r \end{array} \right) + \left( \begin{array}{l} n \\ r + 1 \end{array} \right) = \left( \begin{array}{l} n + 1 \\ r + 1 \end{array} \right) \end{displaymath} Cette formule exprime en elle-même le passage du cas $n$ au cas $n + 1$. La somme traduit le fait que le test donne lieu à deux branches disjointes ; elle apparaît grâce à la propriété d'additivité de la mesure. \end{itemize} En effet, si les coefficients binomiaux étaient définis correctement en Coq, alors j'aurais pu utiliser directement la formule de Pascal, pour laquelle les cas $r = 0$ et $r = n$ conduisent à l'annulation de l'un des coefficients binomiaux. ~ On remarquera, pour conclure, que les méthodes de preuve sont très différentes pour la terminaison et pour la correction. En effet, la terminaison se démontre avec l'ordre bien fondé, tandis que la correction se démontre par induction structurelle sur $n$. \subsection{Récursivité probabiliste : loi géométrique}\label{s-geom} En impératif, la loi géométrique de paramètre $p$ est simulée par une «boucle \emph{while}» probabiliste : \\ \verb+procedure +$geometric$\verb+ (+$p$\verb+: R) : nat+\\ \verb+begin+\\ \verb+ +$result$\verb+ := 0;+ \\ \verb+ while not +$bernoulli$\verb+(+$p$\verb+)+ \\ \verb+ do+ \\ \verb+ +$result$\verb+ := +$result$\verb- + 1;- \\ \verb+ done;+ \\ \verb+ return +$result$\verb+;+\\ \verb+end.+\\ qui s'écrit, en \lo : ~ $\lambda p : \mathsf R . ~ \mathsf{fix} ~ boucle : \bigcirc ~ \mathsf{nat} . ~ \mathsf{prob} $\\ \verb+ + $\mathsf{sample} ~ b ~ \mathsf{from} ~ bernoulli ~ p ~ \mathsf{in} $ \\ \verb+ + $\mathsf{sample} ~ return ~ \mathsf{from} $ \\ \verb+ + $\mathsf{if} ~ b ~ $ \\ \verb+ + $\mathsf{then} ~ \mathsf{prob} ~ 0$ \\ \verb+ + $\mathsf{else} ~ \mathsf{prob}$\\ \verb+ + $\mathsf{sample} ~ result_{prev} ~ \mathsf{from} ~ boucle ~ \mathsf{in} ~ result_{prev} + 1$\\ \verb+ + $\mathsf{in} ~ return$ \\ ~ Ici aussi, la variable libre $bernoulli$ apparaît. Mais nous avons affaire à une récursivité probabiliste, dont le variant est \emph{le flot lui-même}. Nous allons donc devoir parler en détail des opérations effectuées sur le flot. Donc, première conséquence, \emph{pas d'utilisation des probabilités locales}. L'hypothèse sur l'algorithme de simulation de la loi de Bernoulli doit être exprimée avec précision quant à la consommation du flot. Ici, l'algorithme auxiliaire choisi agit en une consommation : ~ \texttt{Hypothesis Hyp\_bernoulli\_conso : \\ Triangle bernoulli (fun p f => 0 <= p -> p <= 1 -> \\ Carre f (fun s y t => exists x, s = x }\verb+::+\texttt{ t /\textbackslash{} \\ (y = true -> x <= p) /\textbackslash{} (y = false -> \~{} (x <= p)) \\ )).} ~ On veut alors montrer le : \begin{theo}[Loi géométrique] Soient $p \in [0, 1]$, $n \in \mathbb N$. Alors, sous le paramètre $p$, la probabilité que l'échantillonnage de l'algorithme probabiliste ci-dessus termine et donne le résultat $n$ est $(1 - p)^n p$. \end{theo} Comme je l'ai annoncé à la section \ref{s-pi-fix}, pour pouvoir raisonner sur cet algorithme, j'ai besoin de considérer un ensemble de flots sur lequel je sais que l'algorithme termine, et un ordre bien fondé sur cet ensemble. Je «vois» dans l'algorithme une «porte de sortie» de la boucle : lorsque le booléen $b$ obtenu par échantillonnage de la loi de Bernoulli est $\mathsf{true}$. Au niveau du flot, cela se traduit par le fait de tomber sur un élément de tête plus petit que $p$. Donc, une condition \emph{suffisante} pour que l'algorithme termine est qu'il comporte au moins un élément plus petit que $p$. Je «vois» aussi dans l'algorithme la situation d'appel récursif : lorsque ce même booléen $b$ est $\mathsf{false}$, on refait une itération. Au niveau du flot, cela se traduit par le fait de tomber sur un élément de tête plus grand que $p$. A ce moment-là, le point fixe rappelé avec la queue du flot. Donc, le flot avec sa tête plus grande que $p$ doit être «plus grand» que sa queue, au sens de l'ordre sur le variant. En somme : \begin{itemize} \item si je considère l'ensemble des flots tels que l'on tombe sur un élément $x \leqslant n$ au bout d'un nombre \emph{fini} d'itérations, alors il est suffisant que le flot soit dans cet ensemble pour que l'algorithme termine. \item sur cet ensemble, l'ordre bien fondé $\prec$ doit vérifier que si je soumets à l'algorithme le flot d'entrée $\alpha :: \varphi$, avec $\alpha > p$, alors je vais le rappeler avec $\varphi$, donc il faut que $\varphi \prec \alpha :: \varphi$. \end{itemize} ~ Or, il se trouve qu'un tel ensemble peut être assez facilement muni d'un tel ordre, et cela de façon générale : la propriété $\alpha \leqslant p$ peut être remplacée par n'importe quel prédicat $P(\alpha)$. C'est pourquoi j'ai défini directement dans le fichier \texttt{lo\_axiom.v} (section \texttt{Ensf\_ord}) un tel ensemble et un ordre bien fondé paramétrés par le prédicat $P$. \begin{defin} Soit P un prédicat à une variable de l'ensemble $E$ des éléments de flot, notons E(P) l'ensemble des flots $\varphi$ tels que $P(\varphi_n)$ pour un certain $n$. \end{defin} En Coq, il est défini inductivement : la tête vérifie $P$, ou alors, dans le cas contraire, la queue est dans l'ensemble. ~ \texttt{Inductive Ensf : Ensemble Flot := \\ | ensf\_0 : forall (x : Element\_flot) (t : Flot), \\ P x -> In \_ Ensf (x }\verb+::+\texttt{ t) \\ ~ \\ | ensf\_S : forall (x : Element\_flot) (t : Flot), \\ \~{} P x -> In \_ Ensf t -> In \_ Ensf (x }\verb+::+\texttt{ t) \\ .} ~ Il se trouve que la définition inductive de $E(P)$ est très proche de celle de $n$ (ce qui est indiqué implicitement dans les clauses d'induction) : les flots commençant par un élément vérifiant $P$ sont «des zéros», tandis que les autres, commençant par un élément ne vérifiant pas $P$, sont «les successeurs de leurs queues». Aussi peut-on se servir de cette similitude pour définir l'ordre. Rappelons que l'ordre sur $\mathbb N$ est défini de la manière suivante : \begin{itemize} \item pour tout $n$, $0 < S(n)$ \item pour tous $n, n'$, si $n < n'$, alors $S(n) < S(n')$ \end{itemize} Alors, définissons l'ordre sur $E(P)$ en suivant ce modèle : \begin{defin} On dit que deux flots $\alpha :: \varphi ~ \prec ~ \alpha' :: \varphi'$ si, et seulement si : \begin{itemize} \item soit $P(\alpha)$ et $\lnot P(\alpha')$ et $\varphi' \in E(P)$ (cas zéro) \item soit $\lnot P(\alpha)$ et $\lnot P(\alpha')$ et $\varphi \prec \varphi'$ (cas successeur). \end{itemize} \end{defin} Cet ordre est défini \emph{a priori} sur tous les flots, mais on montre facilement que deux flots comparables sont nécessairement dans $E(P)$. Il se trouve qu'il vérifie la propriété voulue : \begin{lemme} Si $\alpha$ ne vérifie pas $P$ et si $\varphi \in E(P)$, alors $\varphi ~ \prec ~ \alpha :: \varphi$. \end{lemme} que j'ai démontrée en Coq. En fait, ce lemme est similaire à celui que l'on connaît sur les entiers naturels : $n < S(n)$. ~ Pour montrer que $\prec$ est bien fondé, je procède alors par étapes : \begin{enumerate} \item je définis d'abord une famille, indicée par $\mathbb N$, de flots \emph{de référence}. Mais, pour pouvoir les définir, j'ai besoin d'un élément $\top \in E$ vérifiant $P$ et d'un élément $\bot \in E$ ne vérifiant pas $P$. Etant donnés deux tels éléments, je définis $\Phi(0)$ comme étant le flot constant $\top$, et par induction sur $n$, $\Phi(n + 1) = \bot :: \Phi(n)$. Ces flots sont dans $E(P)$, et $\Phi(n) \prec \Phi(n + 1)$ \item je démontre alors que tout flot de $E(P)$ est majoré par un certain flot de référence $\Phi(n)$ au sens de $\prec$ \item je montre ensuite la propriété très importante suivante : si $\varphi \prec \varphi' \prec \Phi(n + 1)$, alors $\varphi \prec \Phi(n)$. En d'autres termes, il n'y a «rien entre $\Phi(n)$ et $\Phi(n + 1)$» \item cette propriété très importante me permet de montrer que tout flot majoré par un flot de référence est accessible \item or, je sais que tout flot de $E(P)$ est majoré par un tel flot de référence. Donc, tous les flots de $E(P)$ sont accessibles. Comme deux flots comparables sont nécessairement dans $E(P)$, je sais alors que les flots hors de cet ensemble sont accessibles (par vacuité). Donc, $\prec$ est bien fondé. \end{enumerate} Et voilà, j'ai défini un ensemble $E(P)$ et un ordre $\prec$ bien fondé sur les flots, et vérifiant la propriété voulue. Il ne me reste plus qu'à l'appliquer au prédicat $P(\alpha) := \alpha \leqslant p$, et, moyennant les éléments $\top := p$ vérifiant $P$ et $\bot := p + 1$ ne vérifiant pas $P$, j'ai une instance de cet ensemble et de cet ordre bien fondé pour le problème qui m'intéresse ici, à savoir l'algorithme de simulation de la loi géométrique, dont je pourrai prouver la terminaison grâce à cet ensemble. \begin{figure}[p] \begin{center} % \mbox{\epsfig{file=coqide-geometric.eps,width=17cm,height=21cm}} \\ \mbox{\epsfig{file=coqide-geometric.eps}} \\ ~ \\ \caption{Simulation de la loi géométrique : hypothèses nécessaires à la preuve} \label{fig-coqide-geometric} \end{center} \end{figure} ~ Pour montrer la correction, ne pouvant pas utiliser l'outil des probabilités locales, je suis obligé de raisonner directement en probabilité globale. Alors je montre, par induction sur $n$, que l'ensemble des flots $\varphi$ tels que la mise en \oe uvre de l'algorithme termine et donne $n$ est l'ensemble $E_n$ (noté en Coq \texttt{Ens\_geom\_n p}) des flots $\varphi$ commençant par $n$ éléments plus grands que $p$ : ~ \texttt{Fixpoint Ens\_geom\_n (p : R) (n:nat) {struct n} : Ensemble Flot := \\ match n with \\ | Zero\footnote{\texttt{Zero} est un alias pour \texttt{0\%nat} et \texttt{Succ} pour \texttt{S}.} => Produit\_ensembles\_flots (fun x => x <= p) (Full\_set \_) \\ | Succ n' => Produit\_ensembles\_flots (fun x => \~{}(x <= p)) (Ens\_geom\_n p n') \\ end. \\ ~ \\ Theorem Concl\_geometric\_ensemble : \\ Triangle geometric (fun p g => 0 <= p -> p <= 1 -> forall n : nat, \\ ((fun s => exists y, exists t, \{s \textgreater{}\textgreater{} g \~{}> y \textgreater{}\textgreater{} t\} /\textbackslash{} y = n) : Ensemble Flot) = \\ Ens\_geom\_n p n \\ ).} ~ La notation \texttt{\{s \textgreater{}\textgreater{} g \~{}> y \textgreater{}\textgreater{} t\}} correspond en fait à la relation $s \xrightarrow[\square] g \langle y, t \rangle$. ~ C'est cet ensemble $E_n$ dont je vais montrer qu'il est mesurable et dont je vais calculer la mesure, toujours par induction sur $n$. ~ \textbf{Remarque :} au passage, on pourrait montrer que si l'algorithme termine, alors nécessairement le flot d'entrée est dans un des $E_n$ ; en montrant alors que $E(P) = \bigcup_n E_n$, alors on aura montré que l'appartenance à $E(P)$ est aussi une condition nécessaire à la terminaison. ~ Ici encore, comme pour la loi binomiale, la terminaison se démontre en utilisant l'ordre bien fondé sur les flots, tandis que pour la correction, on raisonne par induction structurelle sur le résultat $n$. \clearpage \addcontentsline{toc}{section}{Conclusion} \section*{Conclusion} L'approche que j'ai proposée durant ce stage me permet d'avoir une vision formelle des algorithmes probabilistes me permettant de raisonner correctement dessus au moyen d'un système d'aide à la preuve tel que Coq. Le fait d'avoir transporté le programme en logique, par le biais du transformateur $\Pi$, me permet de raisonner sur les algorithmes probabilistes à partir de formules déterministes sur les programmes. Les formules probabilistes, que je ne rencontre que par la suite dans le raisonnement lui-même, font intervenir des calculs de probabilités qui se ramènent en fait à des mesures d'ensembles, mesures qui s'effectuent en se ramenant directement à des ensembles mesurables de flots. Ainsi, je ne parle d'aucun autre espace de probabilités que celui des flots ou celui des éléments de flots. Par cette approche, je peux montrer qu'un algorithme, donné sous la forme d'un programme en \lo, respecte sa «spécification» probabiliste, donnée sous la forme d'un théorème à prouver sous l'hypothèse de la formule $\Pi$ modélisant le comportement du programme, et sous les hypothèses sur les variables libres, concernant les algorithmes auxiliaires. \addcontentsline{toc}{subsection}{Ce qu'il reste à faire} \subsection*{Ce qu'il reste à faire} Par manque de temps (deux mois, c'est très court), je suis allé à l'essentiel, droit au but ; par conséquent, il reste à compléter certaines formalisations en Coq plus périphériques comme le théorème de Carathéodory et la mesure de Lebesgue. Mais une formalisation beaucoup plus importante et sur laquelle il faut réellement approfondir la réflexion est la notion de \emph{probabilités locales}. En effet, je n'ai défini et utilisé cette notion qu'en tant qu'outil de raisonnement en Coq. Pour justifier l'approche proposée, il faut donner à cette notion de bonnes bases mathématiques qui n'ont pas pu être jetées au cours de ce stage. ~ En plus ces deux points permettant de compléter la formalisation de la théorie sous-jacente à ce stage, il pourrait être intéressant d'améliorer des points touchant à la mise en pratique des méthodes de raisonnement mécanisé proposées dans ce stage. Ces améliorations portent principalement sur les formules générées par le transformateur $\Pi$. En effet, on aura constaté l'extrême complexité de ces formules. La section \ref{s-tech} pourrait constituer une première piste dans l'écriture de tactiques Coq en \ltac{} pour la manipulation des formules. Mais on pourrait aussi songer à optimiser la génération même des formules par le transformateur. Lors d'une telle optimisation, on prendra bien sûr garde à ne pas perdre en expressivité, c'est-à-dire qu'il ne faudra pas perdre d'informations sur le programme. \addcontentsline{toc}{subsection}{Elargissements possibles} \subsection*{Elargissements possibles} Un élargissement important réside dans la réflexion sur la principale restriction du modèle que j'ai choisi : la restriction à deux classes de points fixes ($\mathsf{fix} ~ boucle. ~\lambda n$ et $\mathsf{fix} ~ boucle. ~\mathsf{prob}$), à variant uniquement déterministe ou uniquement probabiliste. Ce modèle ne me permet pas de raisonner sur des algorithmes probabilistes récursifs plus complexes, ceux dont le variant est «mixte», à la fois un argument récursif «déterministe» et le flot de données aléatoires (du genre $\mathsf{fix} ~ boucle. ~\lambda n. ~ \mathsf{prob}$). Cet élargissement nécessiterait de considérer une classe plus générale de variants, et permettrait de réunifier les deux classes de points fixes que j'ai distinguées. ~ Enfin, si mon approche me permet de relier un algorithme et sa spécification (probabiliste) lorsqu'ils sont \emph{donnés}, en \emph{vérifiant} (et c'est précisément le titre du stage) que l'algorithme respecte sa spécification, en revanche je n'ai rien évoqué sur la notion d'\emph{extraction} d'un programme probabiliste à partir de la seule spécification. C'est un élargissement qui pourrait se révéler intéressant. En effet, une telle approche permet l'élaboration presque \emph{ex nihilo} de programmes déjà certifiés et qu'il n'est plus nécessaire de vérifier. \addcontentsline{toc}{subsection}{Comparaison avec d'autres approches} \subsection*{Comparaison avec d'autres approches} \begin{itemize} \item La génération des formules correspondant à un programme (par le transformateur $\Pi$) suit la sémantique opérationnelle. Mais il serait possible d'aborder plutôt une approche axiomatique pour décrire le comportement des programmes. Cependant, cette approche axiomatique impose le développement d'un concept d'interprétation des types, termes et expressions du \lo, et, rapporté au thème des algorithmes probabilistes, il faudrait pouvoir parler de tribus sur des ensembles très généraux donnés par les interprétations sur les types. Mais je considère cela comme un niveau \emph{méta}, raisonnement probabiliste sur l'ensemble des programmes eux-mêmes, alors que l'approche que j'ai proposée raisonne au niveau d'un programme donné, et ne parle que des tribus sur les flots et les éléments de flot. ~ \item Il aurait également été intéressant d'aborder la terminaison et la correction des algorithmes probabilistes suivant une approche similaire à celle de Why \cite{why}. Cette approche par obligations de preuves pourrait proposer une approche plus «locale» du raisonnement sur les algorithmes probabilistes. En effet, l'approche que j'ai proposée nécessite un raisonnement global sur une formule donnant le comportement global de tout un programme en \lo, alors que classiquement, on raisonne sur un programme en montrant plusieurs lemmes, les obligations de preuves, portant sur des fragments locaux de programme. \end{itemize} \clearpage \addcontentsline{toc}{section}{Bilan du stage} \section*{Bilan du stage} Ce stage m'a permis de découvrir de façon pratique le monde de la recherche, au sein des deux équipes \emph{Marelle} et \emph{Everest}. Je dois dire que la méthode de travail que j'ai personnellement mise en \oe uvre au cours de ce stage était très voisine de celle des chercheurs que j'ai côtoyés (en partie étudiants en thèse de doctorat). J'ai pu mettre en évidence, en gros, deux approches différentes de la recherche : \begin{itemize} \item s'aider de documents tout au long du chemin de recherche, en guise de <> \item à partir de documents de base, tracer son chemin de recherche de façon quasi autonome, éventuellement en reconstruisant des théories déjà existantes \end{itemize} C'est plutôt la seconde méthode, moins fréquente que la première, que j'ai appliquée durant ce stage : elle facilite la compréhension du sujet en m'impliquant à fond dans tous ses détails, mais demande peut-être un peu plus de temps que l'approche <>. ~ Ce stage a confirmé mes ambitions de poursuivre mes études en informatique fondamentale dans le domaine de la sémantique et de la vérification de programmes, en m'en faisant découvrir pour ainsi dire les entrailles, les différents domaines en exploitation : on aborde entre autres la sémantique de compilateurs ou de machines virtuelles comme JVM... Mais le travail de recherche de l'équipe \emph{Everest} (qui travaille dans le même bâtiment que l'équipe \emph{Marelle} au sein de laquelle je travaillais) montre que je peux aussi combiner efficacement la sémantique et d'autres domaines de l'informatique fondamentale comme la cryptographie. \clearpage \addcontentsline{toc}{section}{Annexe : utilisation des fichiers relatifs au stage} \section*{Annexe : utilisation des fichiers relatifs au stage} \label{src} \addcontentsline{toc}{subsection}{Téléchargement depuis le Web} \subsection*{Téléchargement depuis le Web} Tous les fichiers du stage se trouvent sur ma page Web, à l'adresse suivante : \begin{center} \url{http://www.eleves.ens.fr/home/ramanana/travail/lo/} \end{center} Les fichiers que j'ai créés durant ce stage se classent en plusieurs sous-dossiers : \begin{itemize} \item \texttt{pcaml} : les sources OCaml de l'interpréteur \emph{Proba Caml} \item \texttt{pi} : les sources OCaml du transformateur $\Pi$ \item \texttt{coq} : les sources Coq des théories formalisées (probabilités, flots, formules \Lo, etc.) ainsi que des exemples traités au chapitre \ref{s-3} avec leurs sources \lo (dans la syntaxe du \lo de $\Pi$) \item \texttt{tex} : les sources \tex des rapports de ce stage (dont le présent rapport technique) \end{itemize} ~ En plus de ces sous-dossiers, on trouvera les archives compressées \verb+*.tar.gz+ (et \verb+*.zip+ pour Windows) des sous-dossiers \verb+pcaml+ et \verb+pi+, ainsi que les diapositives de la présentation (aux formats MS PowerPoint 97 mais aussi PS et PDF). \addcontentsline{toc}{subsection}{Interpréteur \emph{Proba Caml}} \subsection*{Interpréteur \emph{Proba Caml}} J'ai écrit l'interpréteur \emph{Proba Caml} en OCaml. On en trouvera les sources dans le sous-dossier \texttt{pcaml}. On peut les consulter directement en ligne, ou bien télécharger l'archive \texttt{pcaml.tar.gz} que l'on décompressera en tapant successivement les deux commandes suivantes : \\ \texttt{gunzip pcaml.tar.gz} \\ \texttt{tar xvf pcaml.tar} \\ Sous Windows, on téléchargera l'archive \texttt{pcaml.zip} que l'on décompressera soit avec l'outil des Dossiers compressés de l'Explorateur Windows (sur des versions récentes comme Windows XP), soit avec des utilitaires tiers comme WinZip (sur des versions plus anciennes comme Windows 95). ~ J'ai volontairement omis de proposer une distribution directement exécutable, en raison de la très grande variété de plates-formes existant dans le monde informatique (moi-même, je disposais de trois plates-formes différentes pour travailler durant ce stage). C'est pourquoi, pour utiliser l'interpréteur, il faudra recompiler soi-même les sources fournies. Pour ce faire, il faut bien entendu disposer d'un compilateur OCaml. On en trouve plusieurs distributions sur le site Internet officiel du langage Objective Caml \cite{ocaml}. ~ Les fichiers source ont chacun leur rôle : ~ \begin{tabular}{ll} \textbf{Fichier} & \textbf{Description} \\ \verb+lo.ml+ & L'interpréteur proprement dit (<>) \\ \verb+lo_parse.mly+ & Le parseur (<>, format \verb+ocamlyacc+) \\ \verb+lo_lex.mll+ & Le lexeur (format \verb+ocamllex+) \\ \verb+lo_print.ml+ & L'imprimeur, permettant d'afficher à l'écran les éléments de langage \\ \verb+lo_top.ml+ & Le <> : entrée interactive ou lecture d'un fichier \lo. \\ \end{tabular} ~ La compilation s'effectue à la main : \\ \verb+ocamlyacc lo_parse.mly+ \\ \verb+ocamllex lo_lex.mll+ \\ \verb+ocamlopt -o pcaml nums.cmxa lo.ml lo_parse.mli lo_parse.ml \ + \\ \verb+ lo_lex.ml lo_print.ml lo_top.ml+ \\ \textbf{Remarque : } certaines distributions d'Objective Caml ne disposent pas d'un compilateur vers code natif (\verb+ocamlopt+), comme la distribution Cygwin. Dans ce cas, il faut utiliser le compilateur \emph{bytecode} (\verb+ocamlc+), en utilisant le fichier librairie \verb+nums.cma+ au lieu de \verb+nums.cmxa+ : \\ \verb+ocamlc -o pcaml nums.cma lo.ml lo_parse.mli lo_parse.ml \ + \\ \verb+ lo_lex.ml lo_print.ml lo_top.ml+ \\ On obtient alors un programme nommé \verb+pcaml+. Lancé sans paramètre, il lance simplement l'invite d'entrée interactive. Sinon, on peut spécifier une suite de fichiers source, que l'interpréteur lira dans l'ordre, un fichier pouvant dépendre de tous les fichiers précédents ; dans cette liste, on peut intercaler les options suivantes : ~ \begin{tabular}{ll} \verb+-v+ & Affiche les erreurs sur la sortie erreur standard (défaut) \\ \verb+-q+ & N'affiche pas les erreurs \\ \verb+-l+ & Affiche le résultat produit sur la sortie standard (défaut) \\ \verb+-s+ & N'affiche pas le résultat produit \\ \verb+-o+ $fichier$ & Enregistre le résultat produit dans un fichier \\ \verb+-e+ $fichier$ & Enregistre les erreurs dans un fichier \\ \verb+--+ $fichier$ & Permet de lire un fichier d'entrée dont le nom commence par \verb+-+ \\ \verb+-k+ & Passe la main à l'utilisateur (invite clavier) \\ \verb+-h+, \verb+--help+ & Affiche le message d'aide des options acceptées. \\ \end{tabular} ~ L'interpréteur prend les fichiers et les options \emph{dans l'ordre où ils apparaissent} : les options \verb+-v+, \verb+-q+, etc. valent pour tous les fichiers indiqués \emph{après} leur déclaration, jusqu'à l'indication d'une autre telle option. Par exemple, si l'on veut exécuter un fichier \verb+fich1.lo+ et sortir les résultats dans \verb+fich1.out+, puis exécuter un second fichier \verb+fich2.lo+ et sortir les résultats à l'écran, alors on écrira : \begin{center} \texttt{pcaml -o fich1.out fich1.lo -l fich2.lo} \end{center} ~ A l'entrée interactive, ou dans un fichier «source dans le langage \lo de \emph{Proba Caml}», on peut entrer les \emph{instructions} suivantes : \\ \begin{itemize} \item $expr$ \texttt . \\ Une expression à calculer (ou un terme à évaluer) \\ \item \texttt{let } \lbrack\texttt{rec}\rbrack\texttt{ }$var$ \texttt : $ty$ \texttt{:=} $terme$ \texttt . \\ Déclaration d'un algorithme auxiliaire. \\ \item \texttt{let } $var$ \texttt : $ty$ \texttt := $terme$ \texttt{ and } $var$ \texttt : $ty$ \texttt{:=} $terme$ \lbrack \texttt{and} $\dots$ \rbrack \texttt . \\ Déclaration de plusieurs algorithmes auxiliaires \emph{non récursifs}. \\ \end{itemize} Ne pas oublier le point à la fin de chaque instruction. ~ \textbf{Remarque :} l'entrée interactive ne reconnaît pas plusieurs instructions s'enchaînant sur une même ligne. (En revanche, on peut procéder ainsi si on passe par un fichier.) ~ La syntaxe du \lo de \emph{Proba Caml} a été dernièrement unifiée avec celle du \lo du transformateur $\Pi$. Le rôle de $\Pi$ étant de produire une formule Coq à partir d'un programme en \lo, cette syntaxe est donc plus proche de celle du <> de Coq lui-même, dit \emph{vernaculaire}, à ne pas confondre avec \ltac, le langage des tactiques de Coq.}>> que du <> Caml, par l'utilisation, par exemple, du symbole \verb+=>+ à la place de \verb+->+ pour le constructeur de fonctions. ~ \textbf{Variables.} Dans le \lo de \emph{Proba Caml}, les variables sont des identificateurs uniquement composés des lettres latines, majuscules ou minuscules, non accentuées, ainsi que des chiffres de 0 à 9. Ils doivent commencer par une minuscule. ~ \textbf{Types.} Les parenthèses pour le type couple \verb+*+ sont obligatoires ; elles sont facultatives pour le type flèche \verb+->+ qui est associatif à droite : \begin{center} \begin{tabular}{ll} $ty ::= $ & \verb+bool+ | \verb+nat+ | \verb+R+ | $ty$ \verb+->+ $ty$ | \verb+(+ $ty$ \verb+*+ $ty$ \verb+)+ | \verb+O + $ty$ \\ \end{tabular} \end{center} où \verb+nat+ (resp. \verb+R+) représente le type des entiers naturels (resp. des réels), comme en Coq. ~ \textbf{Termes et expressions.} Les parenthèses pour le couple sont obligatoires. L'application est associative à gauche et prioritaire devant l'abstraction \verb+fun+. Un flottant est un nombre «à virgule» (en fait un point), comme en Caml ; un entier est un nombre «sans virgule» ; les entiers et toutes les opérations infixes doivent nécessairement être «scopés à la Coq», c'est-à-dire que le type de leurs arguments doit être indiqué au moyen d'une clause \verb+%+ (ce sont les termes notés $terme^{\mathsf \%}$). Le type correspond à la clause \verb+%+ «la plus interne». Les parenthèses sont obligatoires là où elles apparaissent (en particulier pour les opérations infixes). \clearpage \begin{center} \begin{tabular}{lll} $terme$ & $::=$ & \verb+true+ | \verb+false+ | $special$ | $flottant$ | $var$ \\ & & | \verb+fun +$var$\verb+ : +$ty$\verb+ => +$terme$ | $terme$ $terme$ | \verb+prob +$expr$ \\ & & | \verb+fix +$var$\verb+ : +$ty$\verb+ := +$terme$ \\ & & | \verb+if +$terme$ \verb+ then +$terme$ \verb+ else +$terme$ \\ & & | \verb+(+ $terme$ \verb+,+ $terme$ \verb+)+ | \verb+fst +$terme$ | \verb+snd +$terme$ \\ & & | \verb+(+$terme^{\mathsf \%}$\verb+ % +$ty$\verb+)+ \\ \\ $terme^{\mathsf \%}$ & $::=$ & \verb+true+ | \verb+false+ | $special$ | $flottant$ | $var$ \\ & & | \verb+fun +$var$\verb+ : +$ty$\verb+ => + $terme^{\mathsf \%}$ | $terme^{\mathsf \%}$ $terme^{\mathsf \%}$ | \verb+prob +$expr^{\mathsf \%}$ \\ & & | \verb+fix +$var$\verb+ : +$ty$\verb+ := +$terme^{\mathsf \%}$ \\ & & | \verb+if +$terme^{\mathsf \%}$ \verb+ then +$terme^{\mathsf \%}$ \verb+ else +$terme^{\mathsf \%}$ \\ & & | \verb+(+ $terme^{\mathsf \%}$ \verb+,+ $terme^{\mathsf \%}$ \verb+)+ | \verb+fst +$terme^{\mathsf \%}$ | \verb+snd +$terme^{\mathsf \%}$ \\ & & | \verb+(+$terme^{\mathsf \%}$\verb+ % +$ty$\verb+)+ \\ & & | $entier$ | \verb+(+ $terme^{\mathsf \%}$ $op$ $terme^{\mathsf \%}$ \verb+)+ \\ \\ $expr$ & $::=$ & $terme$ | \verb+S+ | \verb+sample +$var$\verb+ from + $terme$ \verb+ in +$expr$ \\ \\ $expr^{\mathsf \%}$ & $::=$ & $terme^{\mathsf \%}$ | \verb+S+ | \verb+sample +$var$\verb+ from + $terme^{\mathsf \%}$ \verb+ in + $expr^{\mathsf \%}$ \\ \\ $op$ & $::=$ & \verb-+- | \verb+-+ | \verb+*+ | \verb+/+ | \verb+<+ | \verb+<=+ | \verb+>+ | \verb+>=+ \\ $special$ & $::=$ & \verb+Rplus+ | \verb+Rminus+ | \verb+Rmult+ | \verb+Rdiv+ | \verb+Rlt+ | \verb+Rle+ | \verb+Rgt+ | \verb+Rge+ \\ & & | \verb+Plus+ | \verb+Minus+ | \verb+Mult+ | \verb+Lt+ | \verb+Le+ | \verb+Gt+ | \verb+Ge+ \\ & & | \verb+Ln+ | \verb+Exp+ | \verb+Succ+ | \verb+Zero+ | \verb+Pred+ \\ \end{tabular} \end{center} ~ \textbf{Sucres syntaxiques.} En plus des structures du \lo, le \lo de \emph{Proba Caml} définit également les <> suivants : \begin{center} \verb+let +$var$\verb+ : +$ty$\verb+ := +$terme$\verb+ in +$terme'$ \\ \verb+let rec +$var$\verb+ : +$ty$\verb+ := +$terme$\verb+ in +$terme'$ \end{center} respectivement équivalents à : \begin{center} \verb+(fun +$var$\verb+ : +$ty$\verb+ => +$terme'$\verb+) +$terme$ \\ \verb+(fun +$var$\verb+ : +$ty$\verb+ => +$terme'$\verb+) (fix +$var$\verb+ : +$ty$\verb+ := +$terme$\verb+)+ \end{center} ainsi que les sucres syntaxiques de Coq pour les arguments des abstractions \verb+fun+ : \begin{displaymath} \begin{array}{rcl} \texttt{fun (}var\texttt{ : }ty\texttt{) (}var'\texttt{ : }ty'\texttt{) => }terme & \equiv & \texttt{fun }var\texttt{ : }ty\texttt{ => fun }var'\texttt{ : } ty'\texttt{ => }terme \\ \texttt{fun }var\texttt{ }var'\texttt{ : }ty\texttt{ => }terme & \equiv & \texttt{fun }var\texttt{ : }ty\texttt{ => fun }var'\texttt{ : }ty\texttt{ => }terme \\ \end{array} \end{displaymath} ~ \textbf{Opérations prédéfinies.} Outre les opérations infixes classiques, \emph{Proba Caml} reconnaît les fonctions de base sur les naturels \verb+Pred+, \verb+Succ+, ainsi que sur les réels \verb+Exp+, \verb+Ln+. Ces fonctions sont déclarées dans le module \texttt{lo.ml} lui-même (ce qui est une assez mauvaise stratégie). \addcontentsline{toc}{subsection}{Transformateur $\Pi$} \subsection*{Transformateur $\Pi$} J'ai également écrit le transformateur $\Pi$ en OCaml (tout comme \emph{Proba Caml}, dont, d'ailleurs, il dérive directement). On en trouvera les sources dans le sous-dossier \texttt{pi}. On peut les consulter directement en ligne, ou bien télécharger l'archive \texttt{pi.tar.gz} que l'on décompresse comme pour PCaml avec \texttt{gunzip} puis \texttt{tar xvf} (ou, sous Windows, télécharger et décompresser \texttt{pi.zip}). Les fichiers source jouent exactement les mêmes rôles que pour \emph{Proba Caml}, avec le transformateur proprement dit dans le fichier \texttt{lo.ml}. Tout comme pour \emph{Proba Caml}, j'ai volontairement omis de proposer une distribution directement exécutable de $\Pi$. Il faut donc là encore compiler à la main, exactement comme pour \emph{Proba Caml}, en changeant, si l'on veut, le nom de l'exécutable \verb+pcaml+ en \verb+pi+. ~ Le transformateur $\Pi$ est d'utilisation assez simple. De deux choses l'une : soit l'utilisateur lance l'invite interactif de $\Pi$ et tape directement son code \lo, soit il l'écrit dans un fichier qu'il demande alors au transformateur de lire, en le passant en paramètre. Dans les deux cas, $\Pi$ écrit la formule Coq obtenue directement à l'écran, ou, sur demande de l'utilisateur (option \texttt{-o}), sous la forme d'un module source Coq. En fait, la syntaxe de ligne de commande de \verb+pi+ est la même que celle de \verb+pcaml+. Précisons que le résultat est la formule Coq elle-même, sur la sortie standard par défaut, tout autre message étant envoyé par défaut vers la sortie erreur standard. ~ Contrairement à Proba Caml, le transformateur $\Pi$ ne reconnaît que les définitions de variables : \begin{itemize} \item \texttt{let }\lbrack\texttt{rec}\rbrack $\dots$ pour la définition d'algorithmes \item ou bien, pour déclarer une variable libre sans donner de code : \begin{displaymath} \texttt{Variable }var\texttt{ : }ty\texttt{ .} \end{displaymath} \end{itemize} ~ La syntaxe du \lo de $\Pi$ suit celle du \lo de Proba Caml (voir ci-avant), avec laquelle elle a été dernièrement <> ; cependant, à la différence de l'interpréteur, le transformateur n'accepte que la définition des points fixes conformément à la restriction suivant les deux classes que j'ai distinguées en \ref{s-pi-fix} : \begin{itemize} \item pour les points fixes déterministes : \begin{displaymath} \texttt{fix }var\texttt{ ( }var' \texttt{ : } ty' \texttt{ ) variant " }ordre\texttt{ " : } ty \texttt{ := } terme \end{displaymath} correspondant au terme de point fixe : \begin{displaymath} \mathsf{fix} ~ var : ~ ty' \rightarrow ty . ~ \lambda var' : ty' . ~ terme \end{displaymath} où $ordre$ est l'ordre sur le variant, supposé bien fondé, à spécifier \emph{en Coq} (on donnera par exemple \texttt{Lt} pour l'ordre classique sur les entiers naturels). \\ \item pour les points fixes probabilistes : \begin{displaymath} \texttt{fix } var\texttt{ prob " } ens \texttt{ " variant " }ordre\texttt{ " : } ty \texttt{ := } expr \end{displaymath} correspondant au terme de point fixe : \begin{displaymath} \mathsf{fix} ~ var : ~ \bigcirc ~ ty . ~ \mathsf{prob} ~ expr \end{displaymath} où $ens$ est un ensemble de flots tels qu'un échantillonnage sur ces flots termine, et $ordre$ est l'ordre sur le variant flot, supposé bien fondé, tous deux à spécifier \emph{en Coq}. \end{itemize} ~ Le \texttt{let rec} (aussi bien en local \texttt{let rec ... in} que l'instruction \texttt{let rec}) est alors restreint à ces deux structures (en remplaçant simplement \texttt{fix} par \texttt{let rec}). ~ \textbf{Remarque :} pour préserver la <> dans le sens <> (tout programme en \lo de $\Pi$ est accepté par \emph{Proba Caml}), \emph{Proba Caml} reconnaît ces syntaxes restreintes en ignorant les chaînes Coq. \clearpage \addcontentsline{toc}{section}{Références} \bibliographystyle{alpha} \bibliography{lo} \addcontentsline{toc}{section}{Table des figures} \listoffigures \end{document}