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
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
|
%% This is a LaTeX document. Hey, Emacs, -*- latex -*- , get it?
\documentclass[12pt,a4paper]{article}
\usepackage[a4paper,hmargin=2cm,vmargin=3cm]{geometry}
\usepackage[shorthands=off,french]{babel}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{newtxtext}
% 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}
\usepackage{hyperref}
%
\theoremstyle{definition}
\newtheorem{comcnt}{Tout}
\newcommand\thingy{%
\refstepcounter{comcnt}\smallbreak\noindent\textbf{\thecomcnt.} }
\renewcommand{\thefootnote}{\fnsymbol{footnote}}
%
\DeclareUnicodeCharacter{00A0}{~}
\DeclareUnicodeCharacter{2026}{...}
%
%
%
\begin{document}
\title{Logique et Fondements de l'Informatique\\Bibliographie et conseils de lecture}
\author{David A. Madore}
\maketitle
\centerline{\textbf{CSC-3TC34-TP / INF110}}
{\footnotesize
\immediate\write18{sh ./vc > vcline.tex}
\begin{center}
Git: \input{vcline.tex}
\end{center}
\immediate\write18{echo ' (stale)' >> vcline.tex}
\par}
%
%
%
\setlength{\parskip}{6pt plus 6pt}
Ce document rassemble quelques conseils de lecture pour
\emph{prolonger} ou bien \emph{compléter} le cours de « Logique et
Fondements de l'Informatique », ou simplement en rapport avec des
thématiques évoquées dans ce cours.
\begin{itemize}
\item\setlength{\parskip}{6pt plus 6pt}Commençons par un livre de
vulgarisation, qui est aussi un grand classique (et une référence de
toute une génération de geeks): \textit{Gödel, Escher, Bach} de
Douglas Hofstadter (1979).
C'est un livre très difficile à classer, ou même à décrire, puisqu'il
intercale des chapitres sérieux avec des dialogues humoristiques, et
qu'il parle à la fois de sciences et d'art (ça va des maths à la
biologie en passant par la physique, la linguistique, la philosophie
zen, la linguistique… et bien sûr les dessins d'Escher et la musique
de Bach, ainsi que des réflexions sur l'intelligence artificielle qui
restent étonnamment pertinentes pas loin de 50 ans après). Le thème
général est celui de la récursion et de l'auto-référence (et en
particulier, de variations sur le théorème de Gödel et l'astuce de
Quine). On trouve aussi dedans une formalisation précise de
l'arithmétique du premier ordre (mais présentée à un niveau grand
public) ainsi qu'une description d'un langage de programmation
(« BlooP ») qui calcule précisément les fonctions primitives
récursives.
En tout cas, je recommande très vivement ce livre (à la
lecture duquel je dois beaucoup d'être moi-même devenu mathématicien)
à tous ceux qui trouvent intéressants les thèmes abordés par ce cours.
L'original est en anglais, mais il y a une excellente traduction
française, à laquelle l'auteur lui-même a contribué.
\item Sur la \textbf{calculabilité}, il existe de nombreux ouvrages,
parmi lesquels on peut par exemple recommander :
\begin{itemize}
\item\textit{Computability Theory} de Barry Cooper (2003) : assez
court et pas trop indigeste
\item\textit{Calculabilité} de Benoît Monin \& Ludovic Patey (2022) :
beaucoup plus complet, mais très bien présenté
\item\textit{Turing Computability: Theory and Applications} de Robert
I. Soare (2016) : concis et complet
\item\textit{Computability Theory: An Introduction to Recursion
Theory} de Herbert B. Enderton (2011) : beaucoup plus élémentaire et
moins complet que les précédents
\end{itemize}
\item\setlength{\parskip}{6pt plus 6pt}Sur le \textbf{typage}, le
livre \textit{Types and Programming Languages} de Benjamin Pierce
(2002) aborde les aspects à la fois théoriques et pratiques du
typage dans différents langages de programmation de manière bien
plus complète que ce que j'ai pu faire en cours.
Beaucoup plus costaud : {\textit{Proofs and Types}} de Jean-Yves
Girard (disponible à l'adresse
\url{http://www.paultaylor.eu/stable/prot.pdf} ; il s'agit de la
traduction anglaise d'un original français, mais je crois que
l'original est devenu introuvable). Contient des définitions précises
de divers systèmes logiques et de typage, la preuve de leur
normalisation, et les explications mathématiquement précises sur la
correspondance de Curry-Howard.
\item\setlength{\parskip}{6pt plus 6pt}Sur le \textbf{théorème de
Gödel} : \textit{Gödel's Theorem (An Incomplete Guide to its Use and
Abuse)} de Torkel Franzén (2005) est un ouvrage de
semi-vulgarisation très bien écrit, et il prend notamment le temps
d'expliquer plein de malentendus sur l'usage fait de ce théorème
(notamment par des non-mathématiciens).
Je peux aussi recommander \textit{An Introduction to Gödel's Theorems}
de Peter Smith (Cambridge University Press, 2013), qui est moins de la
vulgarisation et plus précis et complet, et qui est également très
bien écrit, mais il est difficile à trouver.
\item\setlength{\parskip}{6pt plus 6pt}Sur la \textbf{programmation
fonctionnelle} : si ce style de programmation vous intéresse, je
vous recommande fortement d'apprendre au moins un des langages de
programmation Scheme (non typé, proche du $\lambda$-calcul) et/ou
Haskell (fortement typé, mais diffère du OCaml en ce qu'il est
« paresseux » et « purement fonctionnel », c'est-à-dire sans effets
de bord, et c'est très instructif de comprendre ce que cela permet).
\item\setlength{\parskip}{6pt plus 6pt}Concernant la programmation
fonctionnelle \textbf{non typée}, le livre \textit{Structure and
Interpretation of Computer Programs} d'Abelson et Sussman (1996 ;
aussi appelé le « Wizard Book », aussi bien en référence à
l'illustration de couverture que la compétence qu'il vous fera
acquérir) est un grand classique, qui a servi pendant des années de
support de cours au MIT. Il est épuisé au format papier, mais il
est librement disponible en ligne à l'adresse
\url{https://web.mit.edu/6.001/6.037/sicp.pdf} sur le site du MIT.
Il est basé sur le Scheme (mais ne présuppose pas la connaissance du
Scheme), mais il ne s'agit pas non plus d'un cours de Scheme : il
s'agit d'un cours de programmation fonctionnelle non typée et des
concepts fondamentaux qui vont avec. (Il y a aussi une “édition
JavaScript” du livre, plus récente, si vous préférez ce langage ;
mais je ne sais pas ce qu'elle vaut.)
Notamment, ce livre explique comment écrire un interpréteur Scheme en
Scheme (et ensuite comment le modifier), autrement dit, un programme
universel, et ce que ça nous apprend sur la programmation et la
sémantique des languages de programmation. (L'exposé \textit{The Most
Beautiful Program Ever Written} de William Byrd, disponible sur
YouTube à l'adresse \url{https://www.youtube.com/watch?v=OyfBQmvr2Hc},
peut également être intéressant comme une sorte de version très
abrégée de ce point.)
Le livre de Christian Queinnec \textit{Lisp in Small Pieces} (2007 ;
traduction d'un original français \textit{Les langages Lisp} devenu
introuvable) est également très instructif.
\item\setlength{\parskip}{6pt plus 6pt}Concernant la programmation
fonctionnelle \textbf{typée}, outre le OCaml, le Haskell est un
langage très intéressant (y compris mathématiquement). À son sujet,
le livre de Christopher Allen et Julie Moronuki \textit{Haskell
Programming from first principles} me semble bien (il n'existe pas
au format papier, mais le PDF est achetable en ligne à l'adresse
\url{https://haskellbook.com/}).
\end{itemize}
\bigskip
J'aurai certainement des ajouts à faire à cette liste ultérieurement.
%
%
%
\end{document}
|
