L3 INFORMATIQUE de l'IM2AG MODULE : INF361 TITRE DU COURS : Modèles de Calculs (MCAL) Le contenu est divisée en deux parties : - MT (M.Périn) : 8 CM d'1h30, 8 TD de 1h30 - LC (JF.Monin) : 8 CM d'1h30, 8 TD de 1h30 + 1 mini-projet en k-nôme avec soutenance RESPONSABLES : - Partie MT : Michaël Périn, Jean-Claude Fernandez - Partie LC : Jean-François Monin, Catherine Parent PRÉREQUIS : Bases de la logique, Connaissance en programmation impérative et fonctionnelle, Automates à nombre d'états fini Les UEs ci-dessous sont une bonne préparation INF124 : Modélisation des structures informatiques INF121 : Introduction à la programmation impérative en caml INF232 : Automates et Langages COMPÉTENCES VISÉES - Maîtriser la notion universelle de calculabilité à travers l'étude fine de deux modèles élémentaires de calcul : Machine de Turing et Lambda-calcul, qui illustrent des mécanismes présents dans les langages de programmation (état, évaluation d'expression). - Comprendre que les modèles sont équivalents et que la notion de calculabilité est indépendante du langage de programmation. - Connaître les systèmes de types qui sont à la base des langages et des assistants de preuve modernes. - Comprendre les notions de décidabilité, de calculabilité et le principe de réduction d'un problème à un autre - Connaître les résultats classiques d'indécidabilité et de non-calculabilité et ainsi appréhender les limites de l'informatique À l'issue de ce cours l'étudiant est capable : - de comprendre une preuve de réduction d'un problème à un autre - d'identifier certains problèmes indécidables - de conduire une preuve simple d'indécidabilité - d'identifier les caractéristiques d'un modèle de calcul - de mesurer la puissance expressive et calculatoire de l'itération et de la récursion - d'utiliser les possibilités des systèmes de types avancés. - de relier logique, structures de données et de contrôle PROGRAMME RÉSUMÉ 1. Machine de Turing Le cours s'appuie sur les machines de Turing pour étudier les notions de calculabilité et de décidabilité. - Machines de Turing: Définition et variantes - Équivalence entre machines de Turing et automates à piles - Décidabilité et indédidabilité - Principe de réduction - Théorème d'indécidabilité de Rice 2. Lambda-calcul - Termes - Substitutions, alpha-conversion et beta-réduction - Typage simple, typage polymorphe - Représentation de structures de données - Normalisation faible et forte, confluence, convergence - Programmation par itérateurs et par points fixes - Correspondance de Curry-Howard BIBLIOGRAPHIE LIVRES - Introduction à la calculabilité, Pierre Wolper, Inter-Éditions BD - Logicomix, 2010, Vuibert, 352 pages. FILM - The Imitation Game, 2014, réalisé par Morten Tyldum : l'adaptation cinématographique de la biographie «Alan Turing ou l'énigme de l'intelligence» d'Andrew Hodges. - Automata, 2014, réalisé par Gabe Ibáñez : une reflexion sur les capacités des machines DOCUMENTS ÉLECTRONIQUES - Notes de cours, exercices de TD et annales d'examens sont disponibles sur le site du cours http://www-verimag.imag.fr/~perin/enseignement/L3/mcal/