Fonctions de transformations
Le coeur du projet s'effectue sur la transformation d'une formule selon une grammaire, en un autre type de formule, correspondant à une grammaire plus propice à des calculs. Ainsi, l'utilisateur pourra, grâce aux fonctions de transformations, pouvoir modifier ses formules dans la grammaire qui l'intéresse et ces fonctions sont primordiales pour la transformation finale et l'élimination des conjonctions.
Nous considèrons les 2 grammaires suivantes :
La grammaire Pos
où x est une variable propositionnelle, et a un programme.
La grammaire Nab
où x est une variable propositionnelle, et a un programme.
Nous considèrons également les formules suivantes :
exprimant le Nabla d'un ensemble de formule en fonction de la nécessité et la possibilité et vice-versa.
Nous considèrons que tout programme utilisant ces fonctions sera précédé de la commande :
open Types ;;
Fonctions de transformations de formules sous différentes grammaires :
val pos_To_Nab : formule_pos -> formule_nab
convertit une fonction selon la grammaire Pos vers la grammaire Nab.
Cette fonction est récursive.
val nab_To_Pos : formule_nab -> formule_pos
convertit une fonction selon la grammaire Nab vers la grammaire Pos.
Cette fonction est récursive.
val conj : formule_pos list -> formule_pos
à partir de la liste [a1; ... ; an], créer la formule Conj(...Conj(Conj(Vrai,a1),a2)...,an).
Cette fonction est tail-récursive.
val disj : formule_pos list -> formule_pos
à partir de la liste [a1; ... ; an], créer la formule Disj(...Disj(Disj(Faux,a1),a2)...,an).
Cette fonction est tail-récursive.
val trans_nab : formule_pos list -> formule_pos
cette fonction prend une liste [a1;...an] et renvoie une formule de type formule_pos correspondant à l'écriture du Nabla en fonction de la possibilité et la necessité.
Fonctions développées :
pos_To_Nab
let rec pos_To_Nab f = match f with
Nec(q) -> Disjn(Nabn([pos_To_Nab q]), Nabn([]))
| Poss(q) -> Nabn([pos_To_Nab q;VRAIn])
| Conj(p,q) -> Conjn( pos_To_Nab p, pos_To_Nab q)
| Disj(p,q) -> Disjn (pos_To_Nab p, pos_To_Nab q)
| Imp(p,q) -> Impn (pos_To_Nab p, pos_To_Nab q)
| Neg(q) -> Negn (pos_To_Nab q)
| Lit q -> Litn q
| VRAI -> VRAIn
| FAUX -> FAUXn
;;nab_To_pos
let rec nab_To_Pos f = match f with
VRAIn -> VRAI
| FAUXn -> FAUX
| Conjn(p,q) -> Conj(nab_To_Pos p, nab_To_Pos q)
| Disjn(p,q) -> Disj(nab_To_Pos p, nab_To_Pos q)
| Impn(p,q) -> Imp(nab_To_Pos p, nab_To_Pos q)
| Negn(q) -> Neg( nab_To_Pos q)
| Nabn liste -> let liste_deja_traduite = List.map nab_To_Pos liste in trans_nab liste_deja_traduite
| Litn q -> Lit q
;;conj
let rec conj liste = List.fold_left (fun x y -> Conj(x,y)) VRAI liste ;;
disj
let rec disj liste = List.fold_left (fun x y -> Disj(x,y)) FAUX liste ;;
trans_nab
let trans_nab liste = let c = conj (List.map (fun x -> Poss x) liste) and d = Nec (disj liste) in Conj(c,d) ;;
Explication des fonctions :
La fonction conj permet d'appliquer à une liste d'éléments de type formule_pos la conjonction de tous ses éléments, de la forme, pour une liste [a1;...;an] : a1 ^ a2 ^ ... ^ an. Ainsi, en utilisant le typage de formule_pos : Conj(Conj(Conj(...Conj(VRAI,a1),a2)...)). Cette fonction est tail-récursive et récursive. Cette fonction sera utile pour la transformation d'une formule de grammaire Nab vers une fonction de grammaire Pos. La compléxité de cette fonction est estimée à O(n2).
La fonction disj, de manière analogque à la fonction conj, permert, pour une liste [a1;...an]de créer la formule Disj(Disj(...Disj(FAUX,a1)...)) de type formule_pos. Elle sera primordiale dans l'utilisation de la fonction nab_To_Pos via le traitement de la fonction trans_nab. Elle est tail-recursive. La compléxité de cette fonction est estimée à O(n2).
La fonction trans_nab permet de retranscrire la transformation du nabla en fonction de la possibilité et de la nécessité selon la formule définie plus haut. Elle permet de transformer un noeud de type Nabn. Elle est tail-recursive. Sa complexité est estimée à O(n).
La fonction pos_To_Nab permet de transformer une formule utilisant la grammaire Pos vers une formule équivalente utilisant la grammaire Nab. Cette fonction permet une transformation totale des noeuds de la formule de type formule_pos sous forme d'arbres n-aires, en un arbre n-aires de type formule_nab. Chaque noeud est testé et transformé en son noeud correspondant dans l'autre grammaire, selon le typage de la formule. Deux exceptions sont faites pour le noeud Pos et Nec, qui seront transformés selon les formules vu plus haut. Cette fonction est récursive. Sa complexité est estimée à O(2n).
La fonction nab_To_Pos, de manière analogue à pos_To_Nab permet une transformation d'une formule utilisant la grammaire Nab vers une fonction équivalente utilisant la grammaire Pos. Le noeud Nabn est convertit en utilisant la fonction trans_nab, qui effectue la transformation du nabla vers la possibilité et la nécessité. Cette fonction est récursive. Sa complexité est estimée à O(2n).
Améliorations possibles :
Les transformations restent assez coûteuses, cependant nous pourrions peut-être automatiser l'intégralité des transformations à l'aide d'une fonction itérative, en recodant, par exemple, les formules sous forme de tableaux et non d'arbres n-aires. Alors, nous pourrions utiliser des fonctions tail-récursives et des procédés itératifs sur l'indice des tableaux.