FONDEMENTS THÉORIQUES : CALCULABILITÉ ET SÉMANTIQUE

36h C / 12h TD / 2 EE / 3 crédits ECTS / SI_FTH

Yolaine Bourda, Guy Vidal Naquet

l'objectif de ce module est de présenter une partie des concepts et des outils mathématiques qui sont sous jacents aux méthodes et objets utilisés en informatique. Une première partie, Modèles de calcul, où l'on définira de façon rigoureuse la notion intuitive de ce qui est « faisable ou non par un ordinateur », sera consacrée à l'étude des modèles formels de résolution de problèmes et aux conséquences pratiques. Une deuxième partie, Théorie des langages formels, présentera les concepts mathématiques régissant les langages de programmation, leur construction et leur analyse et proposera des méthodes de résolution des problèmes inhérents à certains types de langages. Enfin, une dernière partie, Logique, en s'appuyant sur les fondements de logique mathématique, abordera les concepts de modèle et de démonstration et présentera les applications classiques du domaine (Prolog, Intelligence Artificielle, ...).

Modèles de Calcul

Machines de Turing

Langages et fonctions récursifs. Problèmes indécidables.

Complexité

Hiérarchies Temps, Espace. Réductions et Problèmes Complets. Résultats indépendants des modèles.

-calcul

Termes, réduction, forme normale. - calcul typé. Application : Lisp et Haskell.

Modèles du Parallélisme

Algèbres de processus. Réseaux de Petri.

Introduction à l'informatique Quantique

Rappels mathématiques sur les espaces de Hilbert. Q-bits et transformations. Application à la complexité et à la sécurité.

Théorie des langages formels

Monoides libres et langages. La hiérarchie de Chomsky

Langages Réguliers et Automates Finis

Déterminisme et non déterminisme. Minimisation. Propriétés de fermeture et de décidabilité. Caractérisation par les Expressions Régulières.

Langages Indépendants du Contexte et Automates à Pile

Formes normales. Propriétés de fermeture. Equivalence avec les automates à pile. Langages déterministes. Propriétés de Décidabilité et d'indécidabilité.

Logique

Structures algébriques

Termes. Unification.

Systèmes de réécriture

Terminaison. Confluence. Théorème de Knuth-Bendix.

Calcul des propositions

Logique du 1er ordre

Théorie de la preuve. Théorie des modèles. Méthode des tableaux. Théorème de Herbrand. Résolution. Stratégies de résolution. Application : le langage Prolog.

Logiques modales

Logiques temporelles.

Logiques de description

Bibliographie

Fondements mathématiques de l'informatique, J. Stern, Mc Graw-Hill 1990.
An introduction to functional programming through lambda calculus, Greg Michaelson, International Computer Science Series 1988.
Outils logiques pour l'IA - Delahaye - Eyrolles- 1988.
Logique mathématique - Cori - Dunod - 2003.