186 lines
4.7 KiB
TeX
186 lines
4.7 KiB
TeX
\documentclass{article}
|
|
|
|
\usepackage[T1]{fontenc}
|
|
\usepackage{xcolor}
|
|
\usepackage[french]{babel}
|
|
\usepackage{syntax}
|
|
\usepackage{listings}
|
|
\usepackage{amsmath}
|
|
\lstset{
|
|
language=caml,
|
|
columns=[c]fixed,
|
|
basicstyle=\small\ttfamily,
|
|
keywordstyle=\bfseries,
|
|
upquote=true,
|
|
commentstyle=,
|
|
breaklines=true,
|
|
showstringspaces=false}
|
|
%% installer texlive-lang-french pour cela
|
|
|
|
% ci-dessous: commenté car non offert sur les machines libre-service.
|
|
% décommentez si vous le souhaitez.
|
|
%\usepackage[french]{babel}
|
|
|
|
% pour compiler:
|
|
|
|
% faire pdflatex ex-rapport
|
|
% (si les references aux numeros de parties apparaissent comme des
|
|
% "?", recompiler une fois)
|
|
|
|
% la compilation de la bibliographie est davantage une "incantation":
|
|
% faire bibtex ex-biblio
|
|
% puis pdflatex ex-rapport (un nombre premier de fois)
|
|
|
|
|
|
% vous pouvez ensuite ouvrir le fichier ex-rapport.pdf
|
|
|
|
|
|
|
|
|
|
% elements du titre
|
|
\title{Pieuvre: le mini assitant de preuve}
|
|
\author{Marwan et Augustin}
|
|
\date{}
|
|
|
|
% definition de quelques macros, pour les maths
|
|
\newcommand{\litt}{\alpha}
|
|
\newcommand{\non}[1]{\overline{#1}}
|
|
\newcommand{\TODO}[1]{\textbf{\color{red}#1}}
|
|
\begin{document}
|
|
|
|
\maketitle
|
|
|
|
\section{Présentation}
|
|
|
|
Nous avons programmé \textbf{Pieuvre}, un assistant de preuve
|
|
pour la logique intuitionniste en \textbf{OCaml}.
|
|
Il permet, à l'aide d'une boucle interactive, de prouver des
|
|
prédicats simples.
|
|
|
|
Nous indiquons dans la partie~\ref{s:opt} comment compiler,
|
|
lancer et utiliser notre programme.
|
|
Nous exposons ensuite à la partie~\ref{s:orga} comment notre
|
|
programme est structuré.
|
|
Nous présentons enfin dans~\ref{s:stlc} notre implémentation
|
|
du $\lambda$-calcul simplement typé puis \ref{s:proof}
|
|
notre implémentation des preuves.
|
|
|
|
\section{Compiler et exécuter}
|
|
\label{s:opt}
|
|
Pour compiler : \lstinline{make pieuvre}
|
|
|
|
Pour exécuter \textbf{Pieuvre} et entrer dans la boucle
|
|
interactive de l'assistant de preuve, il suffit d'entrer la
|
|
commande \lstinline{./pieuvre}.
|
|
Sinon, on peut spécifier un des modes suivants:
|
|
\begin{itemize}
|
|
\item \texttt{-alpha}
|
|
|
|
qui vérifie l'$\alpha$-équivalence
|
|
de deux $\lambda$-termes séparés par \lstinline{&}.
|
|
|
|
\item \texttt{-reduce}
|
|
|
|
qui affiche les $\beta$-réduction
|
|
successives du $\lambda$-terme.
|
|
\end{itemize}
|
|
\section{Organisation du code}
|
|
\label{s:orga}
|
|
|
|
Le code est structuré de la manière suivante~:
|
|
\begin{itemize}
|
|
\item \lstinline{parser.mly} et \lstinline{lexel.mll}
|
|
qui définissent l'analyse
|
|
syntaxique du $\lambda$-calcul simplément typé
|
|
ainsi que des tactiques.
|
|
|
|
\item \lstinline{lam.ml} qui contient notre implémentation
|
|
du $\lambda$-calcul simplement typé.
|
|
|
|
\item \lstinline{types.ml} qui contient la définition
|
|
des \lstinline{types} et \lstinline{typing.ml}
|
|
qui implémente l'algorithme de typage bidirectionnel
|
|
défini dans la partie~\ref{s:stlc}.
|
|
\item \lstinline{proof.ml} qui définit la structure d'une preuve
|
|
et implémente les tactiques.
|
|
|
|
\item \lstinline{main.ml} le point d'entrée de notre programme
|
|
qui fait l'interface avec l'utilisateur.
|
|
\end{itemize}
|
|
|
|
\section{$\lambda$-calcul simplement typé}
|
|
\label{s:stlc}
|
|
Avant de pouvoir réaliser des preuves, il faut pouvoir les encoder.
|
|
On utilise le $\lambda$-calcul simplement typé.
|
|
Dans notre programme, on utilise la syntaxe suivante
|
|
pour les types et pour les termes:
|
|
|
|
|
|
\begin{grammar}
|
|
<A, B> ::= \lstinline{X}
|
|
\alt \lstinline{A -> B}
|
|
\alt \lstinline{A /\ B}
|
|
\alt \lstinline{A \/ B}
|
|
\alt \lstinline{false}
|
|
\end{grammar}
|
|
|
|
\begin{grammar}
|
|
<M, N> ::= x
|
|
\alt \lstinline{fun (x : A) => M}
|
|
\alt \lstinline{M N}
|
|
\alt \lstinline{exf (M : A)}
|
|
\end{grammar}
|
|
Les termes ainsi définis se réduisent à l'aide des règles de
|
|
$\beta$-réduction rappelées dans les notes de
|
|
Selinger~\cite{SelingerNotes}.
|
|
Avant d'être $\beta$-réduit par \lstinline{betastep},
|
|
les termes sont d'abord
|
|
$\alpha$-convertis avec \lstinline{alpha_convert} afin d'éviter
|
|
les problèmes de substitution.
|
|
|
|
On remarque que l'on impose d'annoter le type de l'argument
|
|
d'une $\lambda$-abstraction. Tous les termes sont alors
|
|
typables avec les règles bidirectionnelles suivantes:
|
|
|
|
|
|
\TODO{règles de typage}
|
|
|
|
\[
|
|
\dfrac
|
|
{\lstinline{x : A} \in \Gamma}
|
|
{\Gamma \vdash \lstinline{x : A}}
|
|
\]
|
|
|
|
\[
|
|
\dfrac
|
|
{\Gamma \vdash \lstinline{M : B}}
|
|
{\Gamma \vdash \lstinline{fun (x : A) => M : A -> B}}
|
|
\]
|
|
|
|
\[
|
|
\dfrac{\Gamma \vdash M : \lstinline{A -> B}
|
|
\quad \Gamma \vdash N : \lstinline{A}}
|
|
{\Gamma \vdash \lstinline{M N} : \lstinline{B}}
|
|
\]
|
|
|
|
\[
|
|
\dfrac
|
|
{\Gamma \vdash \lstinline{M : false}}
|
|
{\Gamma \vdash \lstinline{exf (M : A) : A}}
|
|
\]
|
|
|
|
\section{Preuves}
|
|
\label{s:proof}
|
|
|
|
\TODO{Augustin}
|
|
|
|
\section{Vérification des preuves}
|
|
\TODO{parler de la vérification de preuve,
|
|
quelles difficultés ? quelles certitudes ?}
|
|
|
|
|
|
\bibliographystyle{plain}
|
|
\bibliography{ex-biblio}
|
|
|
|
\end{document}
|