1 Inférence de type

1. Définir un type typ des types en mini-ML.

2. Définir un type prog des programmes mini-ML avec annotations de type.

3. Définir une fonction infer de type

   (string * typ) list -> prog -> typ

   qui prend un environnement de typage et un programme et infère le type du programme. Dans le cas où le programme n’est pas typable, on lèvera une exception Not_typable préalablement déclarée. Il pourra être utile d’utiliser la fonction List.assoc pour trouver le type d’une variable dans un environnement.

4. Définir (en utilisant infer) une fonction check de type

   prog -> typ -> bool

   qui détermine si un programme admet un type donné. L’utiliser pour vérifier que

   • (3 + 2, true) a le type int * bool
   • (fun (x : int) → x + 1) 2 a le type int

5. Définir une fonction typable de type prog -> bool qui détermine si un terme est typable. L’utiliser pour vérifier que les fonctions suivantes ne sont pas typables :

   • (fun (x : int) → x) true
   • true 5
   • fst 3
   • (fun (x : int) → y)
   • (fun (f : int → int) → f false)

2 Évaluation

1. Définir une fonction fresh de type unit -> string qui renvoie un nouveau nom de variable à chaque appel : "x0", puis "x1", puis "x2", etc. On considérera que ces noms sont frais dans la suite, c’est-à-dire qu’il n’apparaissent pas dans les programmes considérés.

2. Définir une fonction sub de type

   prog -> string -> prog -> prog

   telle que sub t x u renvoie t dans lequel toutes les occurrences de x ont été remplacées par u (c’est-à-dire t[x↦u]). Vérifier que

   • le résultat de

     (x , y)[x ↦ 5]

     est

     (5 , y)

   • le résultat de

     (fun (x : int) → x)[x ↦ 5]

     est

     (fun (x : int) → x)

     (à α-conversion près)

   • le résultat de

     (fun (x : int) → x + y)[y ↦ x + 1]

     n’est pas

     (fun (x : int) → x + (x + 1))

3. Définir une fonction eval de type prog -> prog qui évalue un programme en une valeur. On lèvera une exception Cannot_evaluate lorsque l’on ne peut pas évaluer le programme. Vérifier que

   (fun (x : int) → x + x) 5

   s’évalue en 10.

3 La factorielle

On cherche à étendre le langage afin d’implémenter la fonction factorielle. À titre d’exercice, nous allons d’abord l’implémenter en OCaml.

1. Définir un opérateur de point fixe par

   let rec fix f x = f (fix f) x

2. Définir la fonction factorielle de façon récursive. Vérifier que 5! = 120.

3. Modifier votre implémentation de la factorielle de sorte à ne pas utiliser rec (mais vous pouvez utiliser fix). Vérifier que 5! = 120.

On cherche maintenant à étendre notre mini-ML de sorte à pouvoir y réaliser une définition similaire.

1. Ajouter au langage des opérations de

   • branchement conditionnel,
   • soustraction,
   • multiplication.

2. Ajouter un opérateur de point fixe.

3. Implémenter la fonction factorielle et vérifier que 5! = 120.

4. Implémenter la division euclidienne (qui calcule le quotient et le reste d’une division). Vérifier que pour a = 279 et b = 15 le quotient est 18 et le reste est 9.

5. Implémenter l’algorithme d’Euclide qui calcule le pgcd de deux entiers. vérifier que le pgcd de 1071 et 462 est 21.

4 Évaluation par machine abstraite

L’opération de substitution est assez coûteuse en pratique. Plutôt que d’effectuer les substitutions lors d’une application, il est plus efficace de propager un environnement d’évaluation qui est une liste de paires (x_i, v_i) constituées d’une variable et d’une valeur indiquant que au moment où on utilisera la variable x_i, il faudra la remplacer par sa valeur v_i.

1. Réimplémenter la fonction d’évaluation eval de type

   (string * prog) list -> prog -> prog

   sans utiliser la substitution, le premier argument étant l’environnement d’évaluation. Vérifier que

   (fun (x : int) → x + x) 5

   s’évalue en 10.