%% 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}