1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
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}
|
