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.

Cours de sémantique

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 6 séances de 2 heures, accompagnées de 6 séances de Travaux dirigés sur machine.

Première séance

La première séance a pour objectif de présenter la sémantique naturelle. Les notes de cours ont la forme d'un article d'une dizaine de pages, postscript compressé.

TD de la première séance

Dans ces TD, nous construisons des dérivations d'exécution pour plusieurs programmes. Nous tâcherons d'évaluer la taille de ces dérivations et nous verrons comment automatiser la construction. Nous nous reposerons sur l'utilisation d'un système de démonstration sur ordinateur appelé Jape. Ce système est disponible sur la majeure partie des machines Unix et Macintosh. Nous utiliserons pour notre cours un fichier de configuration appelé little.jt (aussi en postscript compressé).

Deuxième séance

La deuxième séance a pour objectif de présenter la sémantique dénotationelle. Les notes de ce cours sont disponibles en postscript compressé.

TD de la deuxième séance

Vous pouvez accéder au sujet du TD.

Troisième séance

Pour la troisième séance nous approfondissons les notions d'ordre partiels complets. Voici des notes de cours correspondant approximativement au contenu de cette séance.

TD de la troisième séance

Dans ces TD, nous construisons un programme en Scheme qui implémente les différentes fonctions mathématiques décrite dans la première partie du cours. L'objectif est donc de construire:

1. Des environnements, c'est à dire des fonctions partielles des noms de variable (des symboles de scheme) vers les valeurs entières.
   1. L'environnement vide sera représenté par une fonction à un argument qui retourne toujours une erreur.
   2. Un environnement peut être modifié grâce à la fonction update, qui reçoit, dans cet ordre, un environnement e, un nom de variable v, et une valeur entière n, et retourne un environnement qui se comporte comme l'environnement e partout sauf en la variable v, pour laquelle ce nouvel environnement retourne n.
2. La sémantique des expressions arithmétiques sera représentée par une fonction denote-a qui prend un argument e qui est une expression et retourne une fonction des environnements vers les valeurs entières. La fonction denote-a représente la fonction écrite dans le cours avec le A majuscule en lettre ronde.
3. La sémantique des expressions booléennes sera représentée par une fonction denote-b qui prend un argument e qui est une expression booléenne et retourne une fonction des environnements vers l'ensemble {true, false}. La fonction denote-b représente la fonction écrite dans le cours avec le B majuscule en lettre ronde.
4. La sémantique des instructions sera représentée par une fonction denote-i qui prend un argument i qui est une instruction et retourne une fonction des environnements vers les environnements. La fonction denote-i représente la fonction écrite dans le cours avec le I majuscule en lettre ronde.
5. Pour la sémantique des instructions de boucle on se reposera sur une fonction fix-point qui prend en argument une fonction F d'un ensemble de fonctions dans lui-même et qui retourne un élement invariant par cette fonction, c'est à dire que mathématiquement les valeurs fix-point(F) et F(fixpoint(F)) sont deux fonctions égales en tout point. On étudiera également les moyens de construire cette fonction fix-point en scheme.

Quatrième séance

La quatrième séance revient sur la sémantique naturelle, en étudiant cette fois-ci la sémantique d'un petit langage fonctionnel. Les notes de cours sont disponibles.

TD de la quatrième séance

Dans ce TD, nous allons construire un interprète pour le petit langage fonctionnel vu en cours.

On considère que les expressions du langage considéré sont de la forme suivante:

(if e e e) | (lambda x e) | fix | (app e e)
 | n | v | (plus e e) | (greater e e) | (minus e e)

Dans cette leçon, nous utiliserons des environnements qui sont des listes de paires (variable . valeur). Les valeurs pourront être des valeurs entières, ou bien des closures, c'est à dire des expressions de la forme suivante:

(closure (lambda (x) e) environnement)

Dans ce langage fonctionnel les valeurs associées aux variables ne sont jamais mises à jour. On n'aura donc pas besoin de fonction "update". En revanche on pourra encore utiliser une fonction lookup.

1. définir la fonction lookup
2. construire la fonction eval-miniml qui est capable de traiter
• les variables,
• les valeurs numériques,
• les symboles true ou false.

tester cette fonction sur les expressions suivantes:

(eval-miniml '() '(plus 2 3))
(eval-miniml '() '(greater 3 2))
(eval-miniml '((x . 1)) '(plus 2 x))
(eval-miniml '((x . 2)) '(minus 3 x))

3. ajouter le traitement des lambda-expressions et des applications tester cette fonction sur les expressions suivantes:

   (eval-miniml '() '(app (lambda x (plus 2 x)) 3))
   (eval-miniml '() '(app (lambda x (app (lambda f (app (lambda x (app f 3)) 4))
                                         (lambda y (plus 2 x))))
   

   La dernière commande devrait retourner 5 ou 7 -- laquelle de ces deux valeurs à votre avis?)

4. ajouter le point fixe, en utilisant la règle suivante: la valeur du symbole fix est la cloture suivante:

   '(closure (lambda f (app f (lambda x (app (app fix f) x)))) ())
   

   tester avec la commande suivante:

   (eval-miniml '()
     '(app (lambda f (app f 3))
           (app fix (lambda sum
                        (lambda x (if (greater 1 x)
   	                           0
                                      (plus x (app sum (minus x 1)))))))))
   

5. refaire l'expérience en modifiant la fonction eval-miniml pour que la valeur retournée par fix soit la suivante:

   '(closure (lambda f (app f (app fix f))) ())
   

   Que se passe-t-il? Pouvez-vous expliquer ce phénomène?

6. revenez à la version du langage utilisée au point 4. Donner une expression de ce langage qui représente la multiplication. Pour tester

      (eval-miniml (app (app "votre fonction" 3) 4))
   

   doit retourner 12. Donner également une expression de ce langage qui représente la factorielle.

La solution de ces TD est disponible: programme scheme pour l'interprète du langage fonctionnel. Pour les étudiants intéressés, j'ai aussi une : sémantique naturelle en format Jape (aussi en postscript compressé), mais pour une sémantique différente de celle présentée en cours.

Cinquième seance

Notes du cours

Exercices

Voici l'examen de l'année 2000-2001 et la correction

Voici quelques exercices qui auraient pu servir d'examen exercices2.ps.gz et leurs reponses2.ps.gz.