5.1- TP - Formules logiques

Avant toute chose

Attention, quelques consignes sur le code !

Les noms des variables doivent être explicites, en particulier lorsque leur rôle n'est pas évident. On tolère l et sa décomposition x::q pour une liste, f pour une formule, i pour un indice... Mais restez cohérents.
Votre code doit être commenté, et les types des arguments ainsi que le type de retour des fonctions doit être précisé. C'est d'autant plus vrai pour les fonctions auxiliaires.
Vous devez testez chacune des fonction que vous écrivez. Vous disposez d'une variable formule_test à cet effet.

Formules propositionnelles

1. Définitions

Une formule propositionelle est définie inductivement comme

soit une variable
soit, si est une formule, qui signifie "l'inverse de e"
soit, si et sont des formules,
- pour le "et"
- pour le "ou"

Par exemple, est une formule.

La valeur de vérité d'une formule, pour une valuation de ses variables (c'est à dire qu'on assigne à chaque variable "vrai" ou "faux"), est le résultat de l'opération logique usuelle sur la formule, dans laquelle on a remplacé chaque variable par sa valeur.

Question 1

Soit les variables . Écrivez des formules qui sont vraies seulement dans les cas suivants :

Si les trois variables sont vraies
Si exactement une des trois variable est vraie
Si les trois variables n'ont pas la même valeur

2. Formules sous forme d'arbres

Rappels de OCaml : types énumération

En OCaml, il est possible de déclarer des types "énumération", de la manière suivante :

type classe = MP | MPSI | PCSI | PC

Un élément de ce type a 4 valeurs possible, une pour chaque variant défini.

On peut aussi ajouter des données à un variant avec le mot-clé of. Par exemple :

type classe = MP | MPSI | PCSI | PC | Autre of string

Enfin, il est possible stocker une donnée du type lui-même dans un variant ! Par exemple, si on veut redéfinir le type list pour les entiers, on peut écrire

type liste_entier = Vide | Element of (int * liste_entier)

int * liste_entier est ici le type d'un tuple de deux éléments, un entier et une liste d'entiers.

Question 2

On a commencé à définir un type formule. Complétez la définition pour ajouter les variants manquants.

OCaml

Loading editor...

type formule = 
     Var of char
    |Neg of formule
    (*à compléter*)
    ;;

Question 3

Définissez une variable formule_test qui contient la formule

OCaml

Loading editor...

Question 4

Écrivez une fonction nombre_variable de type formule -> int qui renvoie le nombre de variables dans un arbre de formule (en comptant chaque apparition d'une variable). Testez-la sur formule_test.

OCaml

Loading editor...

Rappels de OCaml : instructions et impression

Pour afficher une valeur en OCaml, il faut utiliser la fonction qui correspond au type de l'objet. Les fonctions disponibles sont : print_int, print_char, print_string, print_float. Pour revenir à la ligne, on utilise print_newline () (attention à bien ajouter () à la fin !).
En OCaml, certaines fonctions renvoie un type particulier, le type unit. En particulier, c'est le cas de toutes les fonctions d'affichage. Il devient alors possible de "chainer" ces fonctions, c'est à dire d'en utiliser plusieurs à la suite. Pour cela, on utilise ; pour les séparer.
Lorsqu'on utilise des ;, ou bien plusieurs if ou match, il est bon de mettre des parenthèses pour délimiter les blocs.

Je vous fournis une fonction print_char_list comme exemple. Notez qu'elle renvoie le type unit, c'est à dire qu'elle ne renvoie rien.

OCaml

Loading editor...

(*affiche une liste de caractères*)
let print_char_list (l: char list): unit = 
    (*Cette fonction auxiliaire effectue l'affichage en récursif, excépté les crochets*)
    let rec aux (l: char list): unit =
        match l with 
            |[] -> ()
            |x::q -> (print_char x; print_string ", "; aux q)
    in
    print_char '['; aux l; print_char ']'; print_newline ()

OCaml

Loading editor...

print_char_list ['b'; 'o'; 'n'; 'j'; 'o'; 'u'; 'r']

Question 5

Écrivez une fonction de type formule -> unit qui permet d'afficher un arbre de formule, et testez-là sur formule_test.

Indice

Vous avez plusieurs options :

afficher l'arbre comme une formule dans la notation usuelle (donc avec les opérateurs entre leurs opérandes)
(plus compliqué) afficher l'arbre sous forme d'arbre. Je vous conseille alors de calculer au passage la profondeur de chaque noeud, et de l'afficher avec une identation correspondant à sa profondeur.

OCaml

Loading editor...

3. Evaluation d'une formule

On va procéder à l'évalutation de formules en forme arborescentes. Pour cela, on va utiliser une table de hashage (Hashtbl), qui est une structure associative qui implémente une interface de dictionnaire. L'utilisation d'une Hashtbl n'est pas exigible sans rappel, mais on peut vous la demander en rappelant son interface. C'est donc ce que vous allez faire ici.

Interface de Hashtbl en OCaml

Création d'une table : Hashtbl.create n créé une table avec une capacité initale n, renvoie unit
Ajout d'un élément : Hashtbl.add table clé valeur, renvoie unit
Récupération d'un élément : Hashtbl.find table clé, renvoie la valeur associée à la clé (ou une erreur si elle n'existe pas)
Autre option : Hashtbl.find_opt table clé, renvoie Some (valeur) si la valeur existe, et None sinon.
Test d'existence : Hashtbl.mem table clé, renvoie true si la clé est présente, false sinon.
Supression : Hashtbl.remove table clé, renvoie unit.
Parcours : Hashtbl.iter fonction table applique une fonction de type clé -> valeur -> unit à chaque élément de la table.

Question 6

Créer une table de hashage, puis ajoutez-y les correspondances suivantes : | clé | valeur | |---|---------| | 'a' | true | | 'b' | true | | 'c' | false | | 'd' | false |

Quel est le type de votre table, après ajout des valeurs ?

OCaml

Loading editor...

Question 7

Ecrivez une fonction récursive eval_arbre de type formule -> (char, bool) Hashtbl.t -> bool qui renvoie la valeur d'une formule si toutes les variables de la formule sont fixées dans la table, et renvoie une erreur sinon.

Donnez sa complexité en temps et en espace.

Rappels de OCaml : les erreurs

Il y a plusieurs façon de gérer les erreurs en OCaml, mais la manière la plus simple est d'utiliser l'instruction failwith "raison de l'erreur". Elle peut correspondre à tous les types, pour plus de facilité d'utilisation.

OCaml

Loading editor...

4. Satisfiabilité

On va maintenant essayer de trouver si une formule est satisfiable.

Question 8

Ecrivez une fonction qui renvoie une Hashtbl contenant toutes les variables d'une formule, associé à faux.

OCaml

Loading editor...

OCaml

Loading editor...

(*Cette fonction converti une Hashtbl en liste*)
let hastbl_to_list t = List.of_seq (Hashtbl.to_seq t);;

Question 9

Ecrivez une fonction qui determine si une formule est satifiable en essayant toutes les possibilités de valeurs de variables.

Vous pouvez commencez avec une table de Hashage qui associe "faux" à toutes les variables, et ensuite faire une fonction récursive sur la liste des variables, qui

essaye toutes les possibilités pour les variables qui la suivent (elle non inclue)
si cela n'a pas satisfait la formule, change sa valeur à "vrai", puis reessaye toutes les possibilités pour les variables qui suivent.

OCaml

Loading editor...

Entrez le code donné en cours pour accéder à la solution :

Code d'accès