Description

Cette UE discute des deux principales formalisations de la notion d’algorithme et de ce qui est calculable par une machine : le lambda-calcul et les machines de Turing. Le formalisme du lambda-calcul (syntaxe, interprétation usuelle en termes de fonctions anonymes, curryfication) y est présenté ainsi que les règles de calcul associées (notion de réduction, substitution, règles de réduction, problème de capture de variable, notion de variable libre et liée, forme normale, résultat de Church-Rosser, stratégies de réduction (NOR et AOR)). Le pouvoir d'expressivité du lambda-calcul (booléens, entiers de Church, n-uplets, récursivité (combinateur de point fixe)) y est discuté. Cette UE inclut une présentation de la machine de Turing (ruban, tête de lecture/écriture, états, fonction de transition, configuration, mode accepteur, mode calculateur, machine universelle) et discute de son équivalence (sans preuve) avec le lambda-calcul et les autres modèles de calcul. La thèse de Church-Turing y est énoncée. Les règles du lambda-calcul et le fonctionnement des machines de Turing sont décrits et mis en œuvre en Haskell.

Compétences visées

À l'issue de l'UE, un étudiant est capable de :
- comprendre la notion d'algorithme à travers des exemples classiques de modèles de calcul.
- comprendre les fondements des langages fonctionnels et de l’architecture des ordinateurs
- comprendre l'abstraction d'un modèle de calcul "concret" en structures mathématiques comme le lambda-calcul, les fonctions primitives récursives et les machines de Turing.
 

Bibliographie

- Jean-Louis Krivine; "Lambda-calcul, types et mode`les », Masson, 1990.
- Edmond Bianco, "Informatique fondamentale : De la machine de Turing aux ordinateurs modernes », Birkha¨user, 1979.
- https://www.enseignement.polytechnique.fr/informatique/INF423/uploads/Main/chap7-good.pdf
 

Contacts

Responsable(s) de l'enseignement

• Eric Violard