From 856cd686149ab7571b3da9636076d3d2b33c03a7 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Fri, 19 Jan 2024 23:11:36 +0100
Subject: Typeset course syllabus.
---
programme-inf110.tex | 160 +++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 160 insertions(+)
create mode 100644 programme-inf110.tex
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}
--
cgit v1.2.3