Laboratoire 6: Théorèmes et révisions

Sommaire

Preuves de théorèmes

Théorèmes sur `append`

Définir la fonction append qui prend deux listes en argument et renvoie la concaténation de ces deux listes.

Démontrer que la liste vide est l’élément neutre à gauche pour append, c’est-à-dire append [] xs = xs pour tout xs
Démontrer que la liste vide est l’élément neutre à droite pour append, c’est-à-dire append xs [] = xs pour tout xs
Définir la fonction rev qui inverse une liste. Par exemple, rev [1; 2; 3] = [3; 2; 1]
Démontrer que rev (append xs ys) = append (rev ys) (rev xs)

Théorèmes sur `filter`

Définir la fonction filter qui prend un prédicat et une liste en argument. Elle renvoie la liste filtrée.
Démontrer que filter (fun _ -> true) l = l
Définissez la fonction combine qui renvoie la conjonction de deux prédicats, c’est-à-dire que combine f g renvoie un prédicat qui est vrai pour une valeur x si f x et g x sont vraies.
Démontrer que filter (combine f g) l = filter f (filter g l)
Démontrer que filter f (append xs ys) = append (filter f xs) (filter f ys)

Théorèmes sur `fold`

Définir les fonctions fold_left et fold_right.
Définir une fonction sum qui fait la somme des éléments d’une liste (sans utiliser fold_left ou fold_right)
Démontrer que fold_left (+) 0 xs = sum xs
Démontrer que fold_right (+) 0 xs = sum xs
Démontrer que fold_left f init (append xs ys) = fold_left f init xs ++ fold_left f init ys

Révisions pour l’intra

Shadowing

Soit le programme suivant. Quelle est la valeur de x à la ligne indiquée ?

let x = 1 in
let f x =
  let x =
    x + 2 (* quelle est la valeur de x à cette ligne ? *)
  in
  x in
f x

Renommer de façon consistante ce x et s’assurer que le programme préserve la même sémantique.

RLE

Le codage par plage (run length encoding) consiste à compresser des données en remplaçant chaque séquence d’éléments identiques par une seule instance de l’élément ainsi que son nombre de répétitions.

On souhaite avoir deux fonctions, compress et decompress qui permettent de faire du codage par plage. Il est attendu qu’elles fonctionnent de la façon suivante :

# compress [1;1;1;2;2;4;4;4;2;1;3;3]
[(3,1);(2,2);(3,4);(1,2);(1,1);(2,3)]
# decompress [(1, true); (2, false); (3, true)]
[frue; false; false; true; true; true]

Donner la signature de compress et decompress.
Définir compress et decompress sans utiliser de replis (fold).
Donner une trace de l’évaluation de compress [1,1,1,2].
Énoncer une propriété qui est vraie pour la paire de fonction compress et decompress, qui permet de s’assurer que notre codage par plage est correct.
Définir compress et decompress en utilisant des replis (fold).

`find`

Donner une signature appropriée ainsi qu’une définition de la fonction suivante : find est une fonction qui prend en paramètre un prédicat et une liste. Elle retourne le premier élément de la liste qui satisfait au prédicat. On ne veut pas qu’une erreur soit générée s’il n’y a pas d’élément dans la liste qui satisfait au prédicat.

`filter_map`

Définir la fonction suivante :

val filter_map : ('a -> 'b option) -> 'a list -> 'b list

Donner ensuite un exemple d’utilisation de cette fonction ainsi que le résultat de cet exemple.

Listes associatives

Une manière de représenter un dictionnaire de valeurs en OCaml est d’utiliser une liste associative, qui associe des clés de type 'a à des valeurs de type b :

type ('a, 'b) dict = ('a * 'b) list

Définir la fonction lookup qui cherche un élément dans un dictionnaire et retourne sa valeur.

val lookup : 'a -> ('a, 'b) dict -> 'b option

Définir la fonction extend qui ajoute un élément dans un dictionnaire.

val extend : 'a -> 'b -> ('a, 'b) dict -> ('a, 'b) dict

Donner le type et définir une fonction dict_max qui retourne la clé de l’élément dont la valeur est maximale dans un dictionnaire.
Donner le type et définir une fonction values qui retourne toutes les valeurs d’une liste associative
Donner le type et définir une fonction dict_sum qui calcule la somme des valeurs d’un dictionnaire.

`iterate`

Donner une signature appropriée ainsi qu’une définition de la fonction suivante : iterate est une fonction qui prend en paramètre une fonction f, et une valeur initiale. Elle retourne la liste infinie construite an appliquant f à la valeur initiale, ensuite à ce résultat, etc. Par exemple, iterate (+1) 0 retourne la liste des entiers positifs.

Conversion

Définir la fonction suivante :

convert : (a -> c) -> (b -> c) -> (('a, 'b) result) list -> 'c list

Pour rappel, le type result est défini comme suit :

type ('a, 'b) result = Ok of 'a | Error of 'b

Donner ensuite un exemple d’utilisation de cette fonction ainsi que le résultat.

Définition de type

Définir un type pour représenter une valeur JSON. Une valeur JSON peut être :

une chaîne de caractère ("foo")
un nombre (42)
une liste de valeurs JSON (["foo", 42, 1, 3])
un dictionnaire qui associe des clés (chaînes de caractères) à des valeurs JSON ({"clé1": "valeur1", "clé2": 10})

Intra Été 2024

Question 1

Qu’est-ce qui est vrai pour les langages contenant des fonctions qui peuvent être de première classe et d’ordre supérieur ?

On peut passer des fonctions en argument.
Les fonctions sont des méthodes de classe.
Les fonctions ne peuvent manipuler que des types primitifs (nombres, caractères, et chaînes de caractères).
On peut créer des fonctions dans des fonctions pour les retourner.

Question 2

Les nombres de Stirling de second ordre sont définis par la formulation mathématique suivante : \begin{align*} S(n, 0) &= 0 \text{ pour } n > 0\newline S(0, k) &= 0 \text{ pour } k > 0\newline S(0, 0) &= 1 \newline S(n, k) &= k \times S(n-1, k) + S(n - 1, k - 1) \text{ pour } n > 0, k > 0 \end{align*}

Donner une définition de cette fonction en OCaml.

Question 3

Soit la définition suivante :

let f x y = x + (2 * y)

On souhaite la réécrire en utilisant la forme suivante. Écrire sa définition complète en remplaçant les ???.

let f = function ??? -> ???

Pour rappel, le mot clé function ne permet de définir une fonction qu’à un seul argument.

Question 4

Quel est la valeur qui résulte de l’évaluation de l’expression suivante ?

let f = fun x -> (fun y -> (fun x -> (x, y))) in
f 1 2 3

Question 5

Quel est la valeur qui résulte de l’évaluation de l’expression suivante ?

List.filter (fun x -> x > 5) 
  (List.map (min 7)
    [1; 2; 3; 4; 5; 6; 7; 8; 9; 10])

Pour rappel, la fonction min peut être définie comme suit :

let min (x : int) (y : int) : int =
  if x < y then
    x
  else
    y

Question 6

Soit la fonction length définie comme suit :

let rec length (l : 'a list) : int =
  match l with
  | [] -> 0
  | _ :: t -> 1 + (length t)

On observe le comportement suivant :

# length (List.init 500000 (fun _ -> 0));;
Stack overflow during evaluation (looping recursion?).

Expliquer quel est le problème.
Donner une trace des appels récursifs pour l’appel length [1; 2; 3]
Définir une version alternative de length qui n’a pas ce problème, sans utiliser de fonction du module List.

Question 7

Donner le type et définir une fonction is_increasing qui vérifie si une liste est composé d’entiers strictement croissants. Vous pouvez utiliser des fonctions du module List, mais il est possible également de définir cette fonction sans en utiliser.

Question 8

On souhaite représenter un système de fichiers hiérarchique par un type algébrique en OCaml. Dans ce système de fichiers, on souhaite deux types d’entrées :

des fichiers réguliers, ayant un contenu représenté par une chaîne de caractère.
des dossiers, pouvant contenir d’autres fichiers (fichiers réguliers ou dossiers).

De plus, on souhaite attribuer des permissions à chaque fichier (régulier et dossier), parmi les permissions classiques : permission de lecture (read), d’écriture (write), et d’exécution (execute). Un fichier peut avoir plusieurs permissions à la fois (par exemple, être accessible en lecture et écriture en même temps).

Modéliser cela sous forme de types algébriques.

Question 9

Soit le type suivant :

type expr =
    | Plus of expr * expr        (* a + b *)
    | Minus of expr * expr       (* a - b *)
    | Times of expr * expr       (* a * b *)
    | Divide of expr * expr      (* a / b *)
    | Num of int

Définir une fonction simplify qui remplace, pour toute expression x et pour toute constante n (introduite avec le constructeur Num) :

1 * x et x * 1 par l’expression x,
0 + x et x + 0 par l’expression x,
x / 1 par l’expression x
0 - n par la constante -n
x - 0 par l’expression x

Question 10

Donner le type et définir une fonction qui calcule le nombre de fois qu’un certain élément apparaît dans une liste. Donner deux définitions :

une sans utiliser de repli
une en utilisant un repli

Question 11

Plutôt que de représenter une liste comme son premier élément et un reste, on peut représenter une liste comme son préfixe et le dernier élément. C’est ce qu’on appellera une Tsil.

Soit la liste suivante :

1 :: (2 :: (3 :: []))

Son homologue Tsil pourrait être noté :

((([] :: 1) :: 2) :: 3)

Ou, avec des constructeurs nommés Nil et Snoc :

Snoc (Snoc (Snoc Nil 1) 2) 3

Soit la signature de module qui suit.

module type TSIL = sig
  type 'a t = Nil | Snoc of 'a t * 'a
  
  val nil : 'a t
  val snoc : 'a t -> 'a -> 'a t
  val length : 'a t -> int
  val map : ('a -> 'b) -> 'a t -> 'b t

end

Définir une implémentation d’un module Tsil ayant cette signature.

Question 12

Soit la fonction suivante :

let rec exp (x : int) (n : int) : int =
  if n = 0 then 1 else x * exp x (n - 1)

On souhaite démontrer que, pour tout \(n \geq 0, m \geq 0\) :

exp x (m + n) = exp x m * exp x n

La preuve se fait par induction sur m

Quels sont les cas à prouver ?
Quelle est l’hypothèse d’induction ?
Effectuer la preuve.

Plus d’exercices

Pour se préparer à l’intra, il est recommandé de :

relire les diapos, refaire les exemples et exercices des diapos
faire les exercices de labos qui n’ont pas pu être fait pendant les labos
regarder la documentation de la bibliothèque standard et réimplémenter des fonctions. En particulier, voir les modules suivants :
- List
- Option
- Result
- Fun
faire les exercices présents dans le livre de référence OCaml Programming: Correct + Efficient + Beautiful