Le plan du cours change d'année en année. Vous pouvez accéder au cours tel que je l'avais fait (ou avais prévu de le faire) en 2000-2001, 2001-2002, 2002-2003, 2003-2004, 2004-2005.

Cours de sémantique (année 2007-2008)

L'objectif de ce cours est d'introduire les étudiants aux différentes techniques utilisées pour décrire exactement le comportement des programmes. Ce cours est organisé en 9 séances de 2 heures, accompagnées de 9 séances de Travaux dirigés ou de travaux dirigés sur machine.

Dans tous les cas, je vous conseille la littérature suivante:

  1. Une très bonne introduction au lambda-calcul est fournie dans cet article de H. Barendregt and E. Barendsen, Introduction to Lambda Calculus, 1994
  2. Une introduction à Coq par moi-même: Coq in a Hurry
    3. ,
  3. Il y a un très bon livre de Hanne Riis Nielson et Flemming Nielson Semantics with Applications, a formal introduction, Wiley, 1992.
  4. Glynn Winskel, The Formal semantics of Programming Languages, An Introduction, MIT Press, 1993

Première séance: le lambda-calcul pur

Dans ce cours nous présentons le lambda-calcul pur, en le voyant comme un langage de programmation minimal. Nous montrons les difficultés de l'alpha-conversion, le pouvoir expressif du langage, et les propriétés de confluence. Ceci permet en particulier de distinguer les langages paresseux. Les notes de ce cours sont disponibles ici (en pdf).

TD de la première séance

Dans ces travaux dirigés, nous étudierons les exercices donnés dans les notes de cours

Devoir à la maison pour la première séance

Voici l'exercice concernant le lambda-calcul pur du dernier examen.

  1. Un chercheur lunatique et obstiné décide de représenter les valeurs booléennes de la façon suivante:

    F = lambda x y. x

    T = lambda x y. y

    Comment doit-il alors choisir la valeur de IF pour qu'elle ait le comportement usuel d'une expression conditionnelle?

  2. Notre chercheur veut maintenant représenter les listes, il se donne la représentation suivante:

    Cons = lambda x y z. z x y

    Nil = lambda x. x

    Quelle sont les formes normales des deux listes contenant un seul élément qui est respectivement F et T?

    Il propose ensuite les valeurs suivantes pour la fonction ESTVIDE qui permet de distinguer une liste vide d'une liste non vide. Lesquelles de ces valeurs sont-elles adaptées?

    1. lambda z. z T F
    2. lambda l. l (lambda x y z. z)(lambda x. x)(lambda x. F) T
    3. lambda l. l (lambda x y z. z)(lambda x y. T) F F
    4. lambda l. l (lambda x y. F)

Deuxième séance: le lambda-calcul typé

Dans ce cours nous présentons le typage simple du lambda-calcul. Nous voyons sans les démontrer certaines des propriétés des types: conservation des types à l'exécution, terminaison forte. Nous abordons ensuite l'inférence de type et le typage polymorphe. Ce cours est aussi une occasion pour ré-introduire l'utilisation de règles d'inférence (comme en logique). Les notes de cours sont disponibles ici (en pdf).

TD de la deuxième séance

On fera les exercices donnés en suivant ce lien.

Devoir à la maison pour la deuxième séance

On considère que les types t1, t2, t3 et t4 sont des types de base. Fournir des termes ayant les types suivants:

  1. (t1->t2->t3->t4)->(t1->t2)->(t2->t3->t4)->(t2->t3)->t1->t4
  2. (t2->t1)->(t1->t0)->(t2->t1->t0)
  3. (t1->t3)->(t2->t1)->(t3->t1->t4)->t1->t4

Troisième séance: la sémantique naturelle

Dans ce cours on présente la description d'un petit langage impératif dans le style de la sémantique naturelle. Les notes de ce cours sont disponibles en suivant ce lien (et vous pouvez avoir les sources Tex en suivant ce lien).

TD de la troisième séance

Dans les TD nous ferons les exercices proposés dans les notes de cours.

Si vous voulez construire vos propres documents électroniques contenant des dérivations de sémantique naturelle, je suggère que vous regardiez comment c'est fait dans les sources des notes de cours (pas terrible), ou que vous modifiiez le fichier suivant avec OpenOffice Draw (le même fichier au format svg, ou format pdf).

Devoirs à la maison pour la troisième séance

Construire une dérivation de sémantique naturelle pour l'exécution des programmes suivants dans l'environnement initial (x,1).(y,2).[] (j'utilise [] pour représenter l'environnement vide).

Quatrième séance: la sémantique dénotationnelle

Dans ce cours nous présentons une autre description du petit langage impératif utilisé comme exemple pour le cours précédent. Les notes de cours sont disponibles en suivant ce lien. On trouve également un développement Coq associé, où le théorème de Tarski est démontré à partir des axiomes de base de la logique classique et où ce théorème est ensuite utilisé pour produire la fonction qui représente la sémantique dénotationnelle des instructions. Une preuve mécanisée de correction de la fonction est également jointe.

TD de la quatrième séance

Dans cette séance, on fera les exercices proposés dans les notes de cours.

Devoirs à la maison pour la quatrième séance

On considère la fonction partielle des entiers vers les entiers qui n'est définie nulle part, on l'appelle bottom. On considère ensuite la fonction partielle F à deux arguments, le premier étant une fonction partielle des entiers vers les entiers et le deuxième étant un entier, et qui retourne un entier (quand elle est définie):

F(f,x) = if x <= 0 then 0 else x*f(x-1)

Pour toute fonction partielle des entiers dans les entiers g, la fonction F appliquée à g est à nouveau une fonction partielle des entiers dans les entiers. Par exemple, on peut considérer les fonctions bottom, F(bottom), F(F(bottom)), F(F(F(bottom))). Construisez un tableau à 10 colonnes et à 5 lignes, telle que la case de la ligne i et la colonne j contienne la valeur de F(F(...(bottom)), j), où F est répété i fois. Si l'on prolongeait le tableau suffisamment, que devraient contenir les cases (24,26) et (26, 24)?

Cinquième séance: Types dépendants et le système Coq

La cinquième séance est assurée par Loïc Pottier, il s'agit de décrire les fonctions avec types dépendant et leur application en logique.

TD pour la cinquième séance: le système Coq

Le système Coq peut servir à décrire des démonstrations automatiques, en particulier les démonstrations relatives aux descriptions sémantiques. Voir par exemple cette archive qui regroupe une description en Coq de tous les concepts de ce cours.

Sixième séance: Les ordres partiels complets

Dans ce cours nous apportons des précisions sur les structures mathématiques utilisées en sémantique dénotationnelle. Les notes de cours sont disponibles en suivant ce lien.

TD de la sixième séance

Dans cette séance, on fera les exercices proposés dans le cours de sémantique dénotationnelle (en particulier les exercices 1, 2, 3, 7, 9, 10).

Devoirs à la maison pour la sixième séance

Ce devoir a été déposé le 13 Mars au matin. Il est à faire pour le 20 mars au soir.

Soit S l'ensemble {1,2,3,4}, nous noterons bottom un objet qui n'est pas dans S et nous considérerons la fonction F de type(S -> S union {bottom})->(S->S union {bottom}). 

F(g,i) = si i = 1 alors g(2)
         si i = 2 alors g(4)
         si i = 3 alors g(3)
         si i = 4 alors 1
  1. Donnez, in extenso, les valeurs prises par les fonctions F, F2, F3, F4.
  2. Donnez, in extenso, les valeurs prises par le plus petit point fixe de F.

Septième séance: Sémantique axiomatique

Dans ce cours nous étudions un jeu de règles de raisonnement qui permettent de raisonner sur les programmes. Les notes de ce cours sont disponibles en suivant ce lien ce lien.

TD de la septième séance

Premier exercice

Trouver une propriété P pour que le triplet 

{P}x:=x+y; y:= y+2x{y=3x}
soit prouvable avec les règles de la logique de Hoare. Construisez la dérivation.

Deuxième exercice

Faire les preuves Coq suggérées dans ce fichier .

Troisième exercice

En raisonnant sur l'invariant de boucle, trouvez une précondition P, pour que la post-condition y=n3 soit satisfaite après l'exécution du programme suivant: 

while(x < n) do
  x := x+1;
  y := y+z;
  z := z+t;
  t := t+u;
done

Devoirs à la maison pour la septième séance

Trouvez des constantes a, b, c pour que le triplet de Hoare suivant soit dérivable. Construisez la dérivation. 

{x = 0 /\ y = a /\ z = b /\ t = c}
while (x < n) do
  x := x+1;
  y := y+z;
  z := z+t;
done
{y=n2+3n}

Huitième séance: Calcul de préconditions

Dans ce cours nous étudions le prolongement de la sémantique axiomatique qui permet de calculer les formules logiques qui doivent être satisfaites pour qu'un programme soit cohérent avec les annotations logiques qu'il comporte. Les notes de cours sont les mêmes que pour le cours précédent.

TD de la huitième séance

Dans cette séance nous avons étudié les exercices relatifs au calcul de pré-condition la plus faible des examens des années précédentes:

Premier exercice

Construisez un programme de quelques lignes qui suppose en entrée que la variable x contient une valeur positive ou nulle, qui modifie éventuellement plusieurs variables différentes de x et qui termine dans un état où y est la racine cubique de x. Annotez ce programme de façon à exprimer ces conditions et les invariants de boucle utilisés. Indiquez quelles sont les conditions de vérification engendrées pour ce programme. On préférera, si c'est possible, une solution qui n'effectue que des additions.

D'autres exercices sont proposés dans ce lien (merci à Marieke Huisman).

Examens des années précédentes

Mars 2005, correction, Janvier 2002, correction

Yves Bertot
Last modified: Mon Sep 5 08:32:37 MEST 2005