diff options
| -rw-r--r-- | programme-inf110.tex | 90 |
1 files changed, 42 insertions, 48 deletions
diff --git a/programme-inf110.tex b/programme-inf110.tex index ed105ae..c6217c7 100644 --- a/programme-inf110.tex +++ b/programme-inf110.tex @@ -32,7 +32,7 @@ % % \begin{document} -\title{Logique et Fondements de l'Informatique\\Attendus du cours en 2023–2024} +\title{Logique et Fondements de l'Informatique\\Attendus du cours en 2024–2025} \author{David A. Madore} \maketitle @@ -71,27 +71,24 @@ Git: \input{vcline.tex} récursives, combinateur $\mathsf{Y}$. \item \textbf{Typage :} $\lambda$-calcul simplement typé, et sa version enrichie par les types produits, sommes, $1$ et $0$ ; - terminaison des programmes écrits dans ce dernier (sans détails) ; - correspondance de Curry-Howard entre $\lambda$-calcul simplement - typé enrichi et calcul propositionnel intuitionniste ; algorithme de - Hindley-Milner (basique). + terminaison des programmes écrits dans ce dernier (normalisation + forte ; sans preuve ni détails) ; correspondance de Curry-Howard + entre $\lambda$-calcul simplement typé enrichi et calcul + propositionnel intuitionniste. \item \textbf{Calcul propositionnel :} règles de logique en déduction naturelle, et au moins une présentation des preuves (arbre de séquents, ou drapeau) ; écriture et vérification des $\lambda$-termes de preuve (sans entrer dans le détail pointilleux des notations) ; différence entre logique intuitionniste et logique - classique ; notion de calcul des séquents et de preuve sans coupure - (sans détails) ; notions des axiomes de Hilbert / combinateurs - $\mathsf{S},\mathsf{K},\mathsf{I}$ (sans détails). -\item \textbf{Continuations et call/cc :} la notion générale de - continuation, l'idée générale de la fonction call/cc et son rapport - avec la loi de Peirce, l'idée générale du continuation-passing-style - (sans détails). + classique ; propriété de la disjonction et décidabilité du calcul + propositionnel intuitionniste (idée). \item \textbf{Sémantiques du calcul propositionnel intuitionniste :} - \emph{au moins une} des quatre sémantiques vues en cours (Kripke, - ouverts, réalisabilité propositionnelle, problèmes finis), sa - correction, et comment on s'en sert pour montrer qu'une formule - propositionnelle n'est pas démontrable. + sémantique des ouverts, sa correction et sa complétude ; définition + de la sémantique de la rélisabilité propositionnelle, et sa + correction ; savoir utiliser \emph{au moins une} des sémantiques + vues en cours (ouverts, réalisabilité propositionnelle, + éventuellement Kripke ou les problèmes finis) pour montrer qu'une + formule propositionnelle n'est pas démontrable. \item \textbf{Quantificateurs :} règles \emph{générales} d'introduction et d'élimination du $\forall$ et $\exists$, et $\lambda$-termes de preuve correspondants (sans entrer dans le @@ -99,12 +96,14 @@ Git: \input{vcline.tex} logique du premier ordre avec égalité. \item \textbf{Arithmétique du premier ordre :} les axiomes de Peano ; l'idée générale que Curry-Howard sur l'arithmétique de Heyting - permet d'extraire des algorithmes des preuves ; la possibilité de - formaliser $\varphi_e(i){\downarrow}$ en arithmétique de + permet d'extraire des algorithmes des preuves ; le fait qu'il est + possible formaliser $\varphi_e(i){\downarrow}$ en arithmétique de Heyting/Peano ; le fait que vérifier si une preuve est valable est décidable, mais que savoir si un énoncé est un théorème est - seulement semi-décidable ; l'énoncé du théorème de Gödel et au moins - une certaine idée de la preuve par machines de Turing. + seulement semi-décidable ; l'énoncé du théorème de Gödel et l'idée + de sa démonstration. +\item \textbf{Coq :} l'utilisation générale de Coq telle que pratiquée + en TP. \end{itemize} \bigskip @@ -120,37 +119,32 @@ Git: \input{vcline.tex} avec $\mathsf{Y}$. \item Les détails du typage de quelque langage de programmation que ce soit (autres que les variantes du $\lambda$-calcul simplement typé - vus en cours, Hindley Milner, et les parties de Coq vues en TP), - notamment rien de ce qui concerne Scheme, Haskell ou quelque autre - langage mentionné en passant dans le cours ; le sous-typage, le - polymorphisme ad hoc, les types dépendants, ou les autres - fonctionnalités de certains systèmes de typages mentionnés en - passant dans le cours. Les subtilités de l'algorithme de - Hindley-Milner (problème du polymorphisme du \texttt{let}, - restriction de valeur). -\item Les subtilités des règles structurales en calcul des séquents. - Le fonctionnement de l'élimination des coupures ou sa preuve. Le - $\overline{\lambda}$-calcul (juste mentionné en cours). Le détail - de l'équivalence entre déduction naturelle et calcul des séquents. - Le détail de l'élimination des $\lambda$ grâce aux combinateurs - $\mathsf{S},\mathsf{K},\mathsf{I}$. -\item Le fonctionnement détaillé de la fonction call/cc. Les détails - du continuation-passing-style (conversion systématique) ou de son - typage. Le $\lambda\mu$-calcul (juste mentionné en cours). -\item La complétude de telle ou telle sémantique du calcul - propositionnel intuitionniste. Les subtilités de la réalisabilité - propositionnelle (p.ex., la réalisabilité de la formule de Tseitin). - La sémantique des problèmes finis. + vus en cours, et les parties de Coq vues en TP), notamment rien de + ce qui concerne Scheme, Haskell ou quelque autre langage mentionné + en passant dans le cours ; le sous-typage, le polymorphisme ad hoc, + les types dépendants, ou les autres fonctionnalités de certains + systèmes de typages mentionnés en passant dans le cours. + L'algorithme de Hindley-Milner. +\item Le calcul des séquents, le fonctionnement de l'élimination des + coupures ou sa preuve. Le $\overline{\lambda}$-calcul. Les axiomes + de Hilbert, et les combinateurs $\mathsf{S},\mathsf{K},\mathsf{I}$. +\item La notion de continuation. La fonction call/cc. Le + continuation-passing-style ou de son typage. Le + $\lambda\mu$-calcul. +\item Les subtilités de la réalisabilité propositionnelle (p.ex., la + réalisabilité de la formule de Tseitin). La sémantique de Kripke et + celle des problèmes finis ne sont pas exigibles (mais pourront être + utilisées si on le souhaite). \item Le $\lambda$-cube de Barendregt, les subtilités de la différence entre $\exists$ et types sommes, la notion de prédicativité/imprédicativité. -\item Les détails de Curry-Howard pour quoi que ce soit d'autre que le - calcul propositionnel intuitionniste. -\item Les subtilités des différences et rapports entre Heyting et - Peano (sauf s'il s'agit, par exemple, de vérifier si une - démonstration donnée utilise un raisonnement par l'absurde). -\item Les détails de la démonstration du théorème de Gödel, les - systèmes précis auxquels il s'applique. +\item Les subtilités des différences et rapports entre l'arithmétique + de Heyting et celle de Peano (sauf s'il s'agit, par exemple, de + vérifier si une démonstration donnée utilise un raisonnement par + l'absurde). +\item Les détails de la démonstration du théorème de Gödel, la + formalisation des systèmes précis auxquels il s'applique. +\item Les détails de la syntaxe de Coq. \end{itemize} |