Typeset course syllabus.

1 files changed, 160 insertions, 0 deletions

diff --git a/programme-inf110.tex b/programme-inf110.tex
new file mode 100644
index 0000000..020698e
--- /dev/null
+++ b/programme-inf110.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}
+\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}