From 856cd686149ab7571b3da9636076d3d2b33c03a7 Mon Sep 17 00:00:00 2001 From: "David A. Madore" 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