\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 <<transformation>> 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'<<ensemble suffisant>> 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 : <<si $P$ est vérifiée, alors le
calcul de $e$ termine et $Q$ est vérifiée>>. 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 <<ensemble>> 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'<<espace
mesurable>> 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é <<globale>>, on procède en deux
étapes :
\begin{enumerate}
  \item D'abord, on se ramène à un mesurable <<connu>>, 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
  <<sous>> 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é <<globale>> 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 <<probabilité qu'un algorithme termine>>), 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é <<globale>>, 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 <<balises>>
\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 <<balisée>>.

~

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 (<<syntaxe abstraite>>) \\
  \verb+lo_parse.mly+ & Le parseur (<<syntaxe concrète>>, 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 <<point d'entrée>> : 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 <<sous-ensemble Caml de
\emph{Gallina}\footnote{Le <<langage>> de Coq lui-même, dit
  \emph{vernaculaire}, à ne pas confondre avec \ltac, le langage des
  tactiques de Coq.}>> que du <<vrai>> 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 <<sucres syntaxiques>> 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 <<unifiée>> ;
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 <<compatibilité entre
\emph{Proba Caml} et $\Pi$>> dans le sens <<naturel>> (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}
