Commit 042fecc2 authored by Samuel Ben Hamou's avatar Samuel Ben Hamou
Browse files

Rédaction conclusion rapport.

parent 76d59e14
...@@ -554,8 +554,32 @@ Pour ce faire, il a suffit d'exhiber le $\lambda$-terme témoin $\lambda x \cdot ...@@ -554,8 +554,32 @@ Pour ce faire, il a suffit d'exhiber le $\lambda$-terme témoin $\lambda x \cdot
\subsection{Apports mutuels du stage} \subsection{Apports mutuels du stage}
Ce stage m'a permis d'avoir un premier aperçu, quelque peu biaisé du fait des conditions sanitaires, de ce à quoi peut ressembler le quotidien d'un chercheur. J'ai notamment pu découvrir la suprême frustration que constitue le fait d'achopper pendant plusieurs jours sur un problème, qui se trouve ensuite balayé d'un revers de main par quelqu'un d'autre -- en l'occurrence Pierre Letouzey -- soit car cette personne est plus coutumière des outils utilisés, soit tout simplement parce qu'elle trouve la bonne idée qui nous échappait depuis le début. J'ai aussi eu la joie de découvrir la satisfaction que procure un travail qui avance à bon rythme et qui prend une tournure plus intéressante que prévu, satisfaction qui efface sans nul doute l'amertume de des échecs passés.
Par ailleurs, j'ai pu me rendre compte à quel point l'activité de recherche scientifique est, pour reprendre les mots de Pierre Letouzey, un \og artisanat \fg{}, et qu'il me reste encore un long chemin à parcourir avant de pouvoir devenir moi-même un chercheur autonome, travail pour lequel ma motivation s'est encore développée pendant ce stage.
Enfin, j'ai eu la chance de travailler sur un sujet qui m'intéresse énormément, la logique et les assistants de preuve, auprès de l'un des fondateurs du domaine, que je ne remercierai jamais assez pour l'infinie patience dont il a fait preuve avec moi. Bien qu'assez proche du cours de logique que j'ai suivi au second semestre, ce stage m'a permis d'approfondir ma compréhension des concepts élémentaires de la logique, ainsi que d'améliorer ma maîtrise de Coq, un outil que je prenais pour ésotérique et peu utilisable en pratique, mais qui s'est révélé un allié puissant et parfois salutaire.
\medskip
De mon côté, j'espère avoir contribué à rendre le projet \verb+NatDed+ plus utilisable dans le cadre d'un cours d'introduction à la logique, d'une part en le rendant plus ergonomique (et donc plus aisé à utiliser en temps réel), et d'autre part en lui ajoutant de nouvelles perspectives d'illustration, notamment en ce qui concerne $\ZF$ et le $\lambda$-calcul.
J'espère aussi que mon travail aura permis à Pierre Letouzey de mieux cerner les limites du projet, et que cela l'aidera s'il souhaite poursuivre son travail sur \verb+NatDed+.
\subsection{Prolongements envisageables} \subsection{Prolongements envisageables}
Le sujet du stage était volontairement long, et plusieurs points n'ont pas pu être abordés. De plus, au cours du stage, plusieurs perspectives non explorées ont été évoquées, voici donc une liste non-exhaustive de prolongements envisageables de ce stage.
\begin{itemize}[label=$\bigstar$]
\item Comme mentionné plusieurs fois dans le rapport, l'encodage \emph{locally-nameless} des formules logique présente un certain nombre de défauts, dont la lisibilité. Il serait dès lors intéressant, dans l'optique d'un cours magistral, d'utiliser un encodage nommé pour toutes les variables, qu'elles soient libres ou liées. Ce travail a déjà été amorcé puisque Pierre Letouzey a démontré un théorème d'équivalence entre les deux formulations, il ne resterait donc plus qu'à traduire tous les énoncés des résultats que l'on veut présenter.
\item Les tactiques définies au cours du travail sur l'arithmétique de \textsc{Peano} gagneraient peut-être à être totalement automatisées, grâce à l'algorithme d'unification.
\item Ce stage s'est principalement concentré sur des aspects syntaxiques. Il pourrait être intéressant de creuser d'avantage les aspects méta-théoriques et sémantiques de la logique, par exemple en implémentant la sémantique de \textsc{Kripke} pour la logique intuitionniste, ou bien en creusant les modèles de $\ZF$ grâce à \cite{zfmod}.
\item Nous avons montré un sens de la correspondance de \textsc{Curry-Howard} -- celui qui permet de passer d'une dérivation de typage à une preuve -- mais la réciproque mérite aussi d'être considérée, quoiqu'elle soit moins utile en pratique.
\item Enfin, si le théorème de complétude a déjà été établi par Pierre Letouzey, nous n'avons en revanche pas eu le temps de nous pencher sur les théorèmes d'incomplétude de \textsc{Gödel}, dont la démonstration en Coq serait sûrement inédite.
\end{itemize}
%%% %%%
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment