From 67bff1da2f98f8e3afb0f5f7bf23ab03100df4e2 Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Mon, 19 Jan 2026 12:32:22 +0100 Subject: Syllabus for 2025–2026 (and commit past years' versions). MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- programme-inf110-2024.tex | 160 ++++++++++++++++++++++++++++++++++++++++++++++ programme-inf110-2025.tex | 158 +++++++++++++++++++++++++++++++++++++++++++++ programme-inf110.tex | 37 +++++------ 3 files changed, 337 insertions(+), 18 deletions(-) create mode 100644 programme-inf110-2024.tex create mode 100644 programme-inf110-2025.tex diff --git a/programme-inf110-2024.tex b/programme-inf110-2024.tex new file mode 100644 index 0000000..ed105ae --- /dev/null +++ b/programme-inf110-2024.tex @@ -0,0 +1,160 @@ +%% This is a LaTeX document. Hey, Emacs, -*- latex -*- , get it? +\documentclass[12pt,a4paper]{article} +\usepackage[a4paper,hmargin=2cm,vmargin=3cm]{geometry} +\usepackage[french]{babel} +\usepackage[utf8]{inputenc} +\usepackage[T1]{fontenc} +%\usepackage{ucs} +\usepackage{times} +% A tribute to the worthy AMS: +\usepackage{amsmath} +\usepackage{amsfonts} +\usepackage{amssymb} +\usepackage{amsthm} +% +\usepackage{mathrsfs} +\usepackage{wasysym} +\usepackage{url} +% +\usepackage{graphics} +\usepackage[usenames,dvipsnames]{xcolor} +%\usepackage{tikz} +%\usetikzlibrary{arrows} +% +\theoremstyle{definition} +\newtheorem{comcnt}{Tout} +\newcommand\thingy{% +\refstepcounter{comcnt}\smallbreak\noindent\textbf{\thecomcnt.} } +\renewcommand{\thefootnote}{\fnsymbol{footnote}} +% +\DeclareUnicodeCharacter{00A0}{~} +% +% +% +\begin{document} +\title{Logique et Fondements de l'Informatique\\Attendus du cours en 2023–2024} +\author{David A. Madore} +\maketitle + +\centerline{\textbf{INF110}} + +{\footnotesize +\immediate\write18{sh ./vc > vcline.tex} +\begin{center} +Git: \input{vcline.tex} +\end{center} +\immediate\write18{echo ' (stale)' >> vcline.tex} +\par} + + +% +% +% + +\textbf{Sont au programme du cours} les notions suivantes : + +\begin{itemize} +\item \textbf{Calculabilité :} fonctions primitives récursives, + fonctions générales récursives, numérotation (notamment la notation + $\varphi_e(i)$), théorème s-m-n, astuce de Quine, existence d'une + fonction universelle pour les fonctions générales récursives (et + inexistence pour les primitives récursives), théorème de la forme + normale et possibilité de lancer des calculs en parallèle, théorème + de récursion de Kleene ; indécidabilité du problème de l'arrêt, + théorème de Rice ; machines de Turing et équivalence avec les + fonctions générales récursives ; parties décidables et + semi-décidables, équivalence entre semi-décidable et « image d'une + fonction calculable » ; la notion de réduction many-to-one et de + Turing ; le $\lambda$-calcul non typé, $\beta$-réduction, théorème + de Church-Rosser, redex extérieur gauche, entiers de Church, + équivalence du $\lambda$-calcul avec les fonctions générales + 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). +\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). +\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. +\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 + détail pointilleux des notations) ; logique du premier ordre pure, + 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 + 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. +\end{itemize} + +\bigskip + +\textbf{Ne sont explicitement pas exigibles} les notions suivantes : + +\begin{itemize} +\item Les détails de la fonction d'Ackermann ; les détails de la + notion d'arbre de calcul (autre que l'énoncé du théorème de la forme + normale) ; la notion de degré many-to-one ou de Turing ; les notions + de $\beta$-réduction autres qu'extérieur gauche, les subtilités de + l'ordre d'évaluation, le combinateur $\mathsf{Z}$ ou sa différence + 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. +\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. +\end{itemize} + + +% +% +% +\end{document} diff --git a/programme-inf110-2025.tex b/programme-inf110-2025.tex new file mode 100644 index 0000000..855b070 --- /dev/null +++ b/programme-inf110-2025.tex @@ -0,0 +1,158 @@ +%% This is a LaTeX document. Hey, Emacs, -*- latex -*- , get it? +\documentclass[12pt,a4paper]{article} +\usepackage[a4paper,hmargin=2cm,vmargin=3cm]{geometry} +\usepackage[french]{babel} +\usepackage[utf8]{inputenc} +\usepackage[T1]{fontenc} +%\usepackage{ucs} +\usepackage{times} +% A tribute to the worthy AMS: +\usepackage{amsmath} +\usepackage{amsfonts} +\usepackage{amssymb} +\usepackage{amsthm} +% +\usepackage{mathrsfs} +\usepackage{wasysym} +\usepackage{url} +% +\usepackage{graphics} +\usepackage[usenames,dvipsnames]{xcolor} +%\usepackage{tikz} +%\usetikzlibrary{arrows} +% +\theoremstyle{definition} +\newtheorem{comcnt}{Tout} +\newcommand\thingy{% +\refstepcounter{comcnt}\smallbreak\noindent\textbf{\thecomcnt.} } +\renewcommand{\thefootnote}{\fnsymbol{footnote}} +% +\DeclareUnicodeCharacter{00A0}{~} +% +% +% +\begin{document} +\title{Logique et Fondements de l'Informatique\\Attendus du cours en 2024–2025} +\author{David A. Madore} +\maketitle + +\centerline{\textbf{INF110}} + +{\footnotesize +\immediate\write18{sh ./vc > vcline.tex} +\begin{center} +Git: \input{vcline.tex} +\end{center} +\immediate\write18{echo ' (stale)' >> vcline.tex} +\par} + + +% +% +% + +\textbf{Sont au programme du cours} les notions suivantes : + +\begin{itemize} +\item \textbf{Calculabilité :} fonctions primitives récursives, + fonctions générales récursives, numérotation (notamment la notation + $\varphi_e(i)$), théorème s-m-n, astuce de Quine, existence d'une + fonction universelle pour les fonctions générales récursives (et + inexistence pour les primitives récursives), théorème de la forme + normale et possibilité de lancer des calculs en parallèle, théorème + de récursion de Kleene ; indécidabilité du problème de l'arrêt, + théorème de Rice ; machines de Turing et équivalence avec les + fonctions générales récursives ; parties décidables et + semi-décidables, équivalence entre semi-décidable et « image d'une + fonction calculable » ; la notion de réduction many-to-one et de + Turing ; le $\lambda$-calcul non typé, $\beta$-réduction, théorème + de Church-Rosser, redex extérieur gauche, entiers de Church, + équivalence du $\lambda$-calcul avec les fonctions générales + 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 (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 + preuve, 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 ; propriété de la disjonction et décidabilité du calcul + propositionnel intuitionniste (idée). +\item \textbf{Sémantiques du calcul propositionnel intuitionniste :} + 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 + détail pointilleux des notations) ; logique du premier ordre pure, + 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 ; 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 l'idée + de sa démonstration. +\item \textbf{Coq :} l'utilisation générale de Coq telle que pratiquée + en TP, et notamment les principales tactiques de raisonnement (sur + les connecteurs logiques, types inductifs, égalités, etc.). Le nom + des tactiques est exigible donc on recommande de préparer un + récapitulatif pour l'examen (un tel document est disponible sur la + page eCampus du cours). +\end{itemize} + +\bigskip + +\textbf{Ne sont explicitement pas exigibles} les notions suivantes : + +\begin{itemize} +\item Les détails de la fonction d'Ackermann ; les détails de la + notion d'arbre de calcul (autre que l'énoncé du théorème de la forme + normale) ; la notion de degré many-to-one ou de Turing ; les notions + de $\beta$-réduction autres qu'extérieur gauche, les subtilités de + l'ordre d'évaluation, le combinateur $\mathsf{Z}$ ou sa différence + 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, 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 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} + + +% +% +% +\end{document} diff --git a/programme-inf110.tex b/programme-inf110.tex index 855b070..bc2b72d 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 2024–2025} +\title{Logique et Fondements de l'Informatique\\Attendus du cours en 2025–2026} \author{David A. Madore} \maketitle @@ -65,10 +65,12 @@ Git: \input{vcline.tex} fonctions générales récursives ; parties décidables et semi-décidables, équivalence entre semi-décidable et « image d'une fonction calculable » ; la notion de réduction many-to-one et de - Turing ; le $\lambda$-calcul non typé, $\beta$-réduction, théorème - de Church-Rosser, redex extérieur gauche, entiers de Church, + Turing, la définition des degrés many-to-one et de Turing ; le + $\lambda$-calcul non typé, $\beta$-réduction, théorème de + Church-Rosser, redex extérieur gauche, entiers de Church, équivalence du $\lambda$-calcul avec les fonctions générales - récursives, combinateur $\mathsf{Y}$. + récursives, combinateur $\mathsf{Y}$ et son utilisation pour les + appels récursifs. \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 (normalisation @@ -83,12 +85,11 @@ Git: \input{vcline.tex} classique ; propriété de la disjonction et décidabilité du calcul propositionnel intuitionniste (idée). \item \textbf{Sémantiques du calcul propositionnel intuitionniste :} - 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. + sémantique des ouverts, sa correction et sa complétude ; sémantique + de Kripke, sa correction et sa complétude ; définition de la + sémantique de la rélisabilité propositionnelle, et sa correction ; + utilisation de la correction des sémantiques vues en cours 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 @@ -117,10 +118,10 @@ Git: \input{vcline.tex} \begin{itemize} \item Les détails de la fonction d'Ackermann ; les détails de la notion d'arbre de calcul (autre que l'énoncé du théorème de la forme - normale) ; la notion de degré many-to-one ou de Turing ; les notions - de $\beta$-réduction autres qu'extérieur gauche, les subtilités de - l'ordre d'évaluation, le combinateur $\mathsf{Z}$ ou sa différence - avec $\mathsf{Y}$. + normale) ; rien d'autre sur les réductions degrés many-to-one et de + Turing que leur définition ; les notions de $\beta$-réduction autres + qu'extérieur gauche, les subtilités de l'ordre d'évaluation, le + combinateur $\mathsf{Z}$ ou sa différence 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, et les parties de Coq vues en TP), notamment rien de @@ -136,12 +137,12 @@ Git: \input{vcline.tex} 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). + réalisabilité de la formule de Tseitin). La sémantique des + problèmes finis n'est pas exigible (mais pourra être utilisée 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é. + prédicativité/imprédicativité, le système $F$. \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 -- cgit v1.2.3