Page d’accueil
Navigation principale
avatar
Justine BENOUWT
avatarmp2i
Dépôt
Une erreur s’est produite lors du chargement des signatures de validation
mp2i
docs
tp
ocaml
logique.md
logique.md
Avatar de jbenouwt
3ab80b7a
Il y a 2 jours
logique.md
20,83 Kio
TP : Logique propositionnelle (en OCaml)
La première partie du TP s’intéresse à la syntaxe des formules propositionnelles (arbre syntaxique et définitions inductives). La seconde partie s’intéresse à la sémantique des formules propositionnelles (évaluation d’une formule et algorithme de Quine).
I. Syntaxe des formules propositionnelles
1. Arbre syntaxique implémentant les formules
Soit
mathcal V = {x_0,x_1,x_2,…}V={x
0
,x
1
,x
2
,…}
l’ensemble des variables propositionnelles. On définit dans ce TP l’ensemble des formules propositionnelles
mathcal P_mathcal VP
V
par induction ainsi :
mathcal V subset mathcal P_mathcal V;;;; top in mathcal P_mathcal V;;;; bot in mathcal P_mathcal V;;;; varphiin mathcal P_mathcal V Rightarrow lnot varphi in mathcal P_mathcal V;;;; varphi,psiin mathcal P_mathcal V Rightarrow varphiland psi in mathcal P_mathcal V;;;; varphi,psiin mathcal P_mathcal V Rightarrow varphilorpsi in mathcal P_mathcal VV⊂P
V
;⊤∈P
V
;⊥∈P
V
;φ∈P
V
⇒¬φ∈P
V
;φ,ψ∈P
V
⇒φ∧ψ∈P
V
;φ,ψ∈P
V
⇒φ∨ψ∈P
V
.
Quelles sont les assertions dans cette définition ? les règles d’inférence ?
Une définition inductive est dite ambiguë si un élément de l’ensemble peut être obtenu de plusieurs façons. Donnez un exemple de formule pouvant être construite de deux façons, puis modifiez la définition inductive ci-dessus pour qu’elle ne soit plus ambiguë.
Chaque formule propositionnelle peut être représentée par son arbre syntaxique. En C et en OCaml, on utilise l’arbre syntaxique pour implémenter les formules.
En C, on utiliserait le type suivant :
struct formule_s {
// étiquette du nœud : “top”, “bottom”, “ou”, “et”, “non”, ou un nom de variable
char* nom;
// sous-formule gauche, ou NULL s’il n’y en pas
struct formule_s* sfg;
// sous-formule droite, ou NULL s’il n’y en pas
struct formule_s* sfd;
};
En OCaml, un type somme nous permet d’être un peu plus précis, on utilisera le type suivant :
type formule =
(* assertions de la définition = feuilles de l’arbre syntaxique *)
| Top
| Bottom
| Var of int
(* règles d’inférence de la définition = nœuds internes de l’arbre syntaxique *)
| Non of formule
| Ou of formule * formule
| Et of formule * formule
Nous travaillerons en OCaml dans ce TP, mais vous devez être capable de ré-écrire les mêmes fonctions en C.
Voici des exemples de formules (qui pourront vous servir pour tester vos fonctions) :
let ex1 = Non (Ou (Et (Var 0, Var 1), Et (Var 0, Var 2)))
let ex2 = Ou (Et (Var 1, Bottom), Non (Var 3))
let ex3 = Et (Top, Non (Ou (Bottom, Et (Top, Non (Bottom)))))
Donnez les formules propositionnelles correspondant aux trois variables ex1, ex2, ex3 ci-dessus, et dessinez leurs arbres syntaxiques.
Quel type de parcours d’arbre faut-il effectuer pour récupérer la formule écrite avec la syntaxe usuelle ? Et pour récupérer la formule écrite en OCaml ?
Écrivez une fonction string_of_formule : formule -> string renvoyant la représentation usuelle d’une formule propositionnelle sous forme d’une chaîne de caractères. Attention au parenthésage. Exemples :
# string_of_formule ex1 ;;
– : string = “¬((x_0 ∧ x_1) ∨ (x_0 ∧ x_2))”
# string_of_formule ex2 ;;
– : string = “((x_1 ∧ ⊥) ∨ ¬x_3)”
# string_of_formule ex3 ;;
– : string = “(⊤ ∧ ¬(⊥ ∨ (⊤ ∧ ¬⊥)))”
2. Fonctions inductives classiques
Nous allons définir par induction quelques fonctions classiques sur l’ensemble des formules propositionnelles.
Rappelez la définition inductive de la taille d’une formule propositionnelle. Donnez les tailles des formules ex1, ex2, ex3.
Déduisez-en une fonction récursive taille : formule -> int.
Rappelez la définition inductive de la hauteur d’une formule propositionnelle. Donnez les hauteurs des formules ex1, ex2, ex3.
Déduisez-en une fonction hauteur : formule -> int.
Calculez soigneusement les complexités temporelles des fonctions taille et hauteur.
Rappelez la définition inductive de
varphi[psi/x], text{ avec } varphi, psiin mathcal P_mathcal V, xin mathcal Vφ[ψ/x], avec φ,ψ∈P
V
,x∈V
(substitution). Déduisez-en une fonction substitue : formule -> int -> formule -> formule.
Rappelez la définition inductive de l’ensemble des sous-formules d’une formule propositionnelle. Déduisez-en une fonction ensemble_sous_formules : formule -> formule list. La liste renvoyée pourra éventuellement contenir des doublons (dans le cas où la formule en paramètre contient plusieurs fois la même sous-formule).
II. Sémantique des formules propositionnelles
On utilise dans cette partie le même type formule défini dans la partie précédente.
1. Évaluation d’une formule
On définit une valuation comme un tableau de booléens :
type valuation = bool array
Si v est de type valuation, alors v.(i) donne la valeur de vérité associée à la variable propositionnelle Var i.
Voici par exemple la liste des 8 valuations existantes pour la formule correspondant à la variable ex1 définie dans la partie précédente :
let vals_3 = [ [|false;false;false|]; [|true;false;false|]; [|false;true;false|]; [|true;true;false|]; [|false;false;true|]; [|true;false;true|]; [|false;true;true|]; [|true;true;true|] ]
Rappelez la définition inductive de
[![varphi]!]_text v,text{ avec } varphiin mathcal P_mathcal V[[φ]]
v
, avec φ∈P
V
et v une valuation (évaluation). Déduisez-en une fonction evaluation : formule -> valuation -> bool.
Déterminez à la main si la valuation [|true;false;true|] est un modèle de la formule correspondant à la variable ex1, puis vérifiez votre réponse avec la fonction evaluation.
Écrivez une fonction modeles : formule -> valuation list -> valuation list telle que modeles phi valuations renvoie
text{Mod}(varphi)Mod(φ)
, avec le paramètre valuations étant la liste de toutes les valuations existantes pour la formule.
Dressez à la main la table de vérité de la formule correspondant à la variable ex1 afin de déterminer ses modèles, puis vérifiez votre réponse avec la fonction modeles et les valuations vals_3.
Quelle est la complexité de la fonction evaluation ? Combien une formule possède-t-elle de valuations existantes ? Quelle est donc la complexité de la fonction modeles ?
À partir de la fonction modeles, comment pourrait-on déterminer si une formule est satisfiable ? tautologique ? antilogique ?
2. Conséquence et équivalence sémantique
On rappelle que :
psiinmathcal P_mathcal V text{ est une conséquence sémantique de }varphiinmathcal P_mathcal V, text{ noté } varphivDashpsi, text{ ssi }Mod(varphi)subset Mod(psi)ψ∈P
V
est une cons
e
ˊ
quence s
e
ˊ
mantique de φ∈P
V
, not
e
ˊ
φ⊨ψ, ssi Mod(φ)⊂Mod(ψ)
psiinmathcal P_mathcal V text{ est équivalente sémantiquement à }varphiinmathcal P_mathcal V, text{ noté } varphiequivpsi, text{ ssi }Mod(varphi)= Mod(psi)ψ∈P
V
est
e
ˊ
quivalente s
e
ˊ
mantiquement
a
ˋ
φ∈P
V
, not
e
ˊ
φ≡ψ, ssi Mod(φ)=Mod(ψ)
Écrivez une fonction consequence : formule -> formule -> valuation list -> bool telle que consequence phi psi valuations détermine si
varphivDash psiφ⊨ψ
avec valuations la liste de toutes les valuations existantes. Exemples :
# let vals_4 = [[|false;false;false;false|]; [|true;false;false;false|]; [|false;true;false;false|]; [|true;true;false;false|]; [|false;false;true;false|]; [|true;false;true;false|]; [|false;true;true;false|]; [|true;true;true;false|]; [|false;false;false;true|]; [|true;false;false;true|]; [|false;true;false;true|]; [|true;true;false;true|]; [|false;false;true;true|]; [|true;false;true;true|]; [|false;true;true;true|]; [|true;true;true;true|]] ;;
# consequence ex1 ex2 vals_4 ;;
– : bool = false
# consequence ex1 (Ou (Var 2, Ou (Non (Var 0), Et (Non (Var 1), Non (Var 2))))) vals_4 ;;
– : bool = true
Écrivez aussi une fonction equivalence : formule -> formule -> valuation list -> bool. Exemples :
(* vals_4 vient de l’exemple précédent *)
# equivalence ex1 ex2 vals_4 ;;
– : bool = false
# equivalence ex1 (Ou (Non (Var 0), Et (Non (Var 1), Non (Var 2)))) vals_4 ;;
– : bool = true
Pour étudier la satisfiabilité d’une formule, quelques équivalences sémantiques permettent de simplifier la formule pour en éliminer les constantes logiques :
Écrivez une fonction elimine_constantes : formule -> formule qui prend en entrée une formule
varphiφ
et utilise les règles ci-dessus afin de renvoyer une formule
varphi’φ
′
telle que
varphi’equiv varphiφ
′
≡φ
, et soit
varphi’φ
′
est réduite à une constante, soit elle ne contient aucune constante. Exemples :
# elimine_constantes ex2 ;;
– : formule = Non (Var 3)
# elimine_constantes ex3 ;;
– : formule = Bottom
Montrez par induction structurelle sur phi que si phi ne contient pas de variable alors elimine_constantes phi est réduite à une constante.
3. Algorithme de Quine
Le « problème SAT » consiste à déterminer si une formule propositionnelle est satisfiable.
De quel type de problème s’agit-il ?
La première manière de résoudre le problème SAT est une approche par force brute : tester toutes les valuations possibles. C’est ce que fait la fonction modeles écrite plus haut, et ce n’est pas très efficace. La seconde manière de résoudre le problème SAT est l’algorithme de Quine, qui utilise une approche par backtracking.
L’algorithme de Quine consiste, à partir d’une formule f, à :
Calculer f’ = elimine_constantes f.
S’il reste au moins une variable propositionnelle dans f’ :
sélectionner arbitrairement une variable
xx
restante dans f’ ;
tester récursivement si
texttt{f’}[top/x]f’[⊤/x]
est satisfiable ;
tester récursivement si
texttt{f’}[bot/x]f’[⊥/x]
est satisfiable.
Sinon, conclure.
Comme tout algorithme de backtracking, on peut dessiner l’arbre correspondant à l’algorithme de Quine.
Considérons par exemple la formule
varphi = (alor b)land (lnot b lor lnot c)land(lnot a lor c)land(alor c)
, qui est donc la racine de notre arbre.
On sélectionne la variable a arbitrairement, on va la substituer par
bot
puis poursuivre (sous-arbre gauche) et la substituer par
top
puis poursuivre également (sous-arbre droit).
Étudions par exemple la branche droite. Par substitution on obtient la formule
varphi’ = (toplor b)land (lnot b lor lnot c)land(lnot top lor c)land(toplor c)
, puis en appliquant les règles de simplification pour enlever les constantes on trouve donc
varphi’ equiv topland (lnot b lor lnot c)land(bot lor c)landtop equiv (lnot b lor lnot c)land c
.
On sélectionne à partir de là arbitrairement une variable restante, disons b. On substitue b par
bot
puis on poursuit (sous-arbre gauche) et on la substitue par
top
puis on poursuit également (sous-arbre droit).
Suivons cette fois la branche gauche. Par substitution puis simplification on obtient
varphi” = (lnot bot lor lnot c)land c equiv (top lor lnot c)land c equiv top land c equiv c
.
On sélectionne la dernière variable restante, c, qu’on substitue à nouveau par les deux constantes logiques.
Il ne reste plus aucune variable, les feuilles sont étiquetées par des constantes.
Voici l’arbre correspondant au cheminement qu’on vient de faire :
Complétez les branches de l’arbre non détaillées ci-dessus.
À quelle condition sur l’arbre obtenu la formule est-elle satisfiable ? une tautologie ? une antilogie ? La formule de l’exemple ci-dessus est-elle donc satisfiable ? une tautologie ? une antilogie ?
À chaque étape de l’algorithme de Quine, on sélectionne la prochaine variable à substituer arbitrairement. On choisira ici de prendre la plus grande variable restante.
Écrivez une fonction max_var : formule -> int option qui calcule le numéro maximal d’une variable propositionnelle utilisée dans une formule. Le type option sert au cas où la formule ne contient aucune variable. La complexité devra être linéaire en la taille de la formule. Exemples :
“`ocaml
# max_var ex1 ;;
– : int option = Some 2
# max_var ex2 ;;
– : int option = Some 3
# max_var ex3 ;;
– : int option = None
“`
On utilisera le type suivant pour représenter l’arbre de Quine :
type arbre_quine =
| Feuille_top
| Feuille_bottom
| Noeud_interne of int * arbre_quine * arbre_quine
Pour tester vos codes, voici la formule de l’exemple précédent :
(* ((a ∨ b) ∧ (¬b ∨ ¬c)) ∧ ((¬a ∨ c) ∧ (a ∨ c))
avec c = Var 0, b = Var 1, a = Var 2 *)
let (exemple : formule) = Et ( Et ( Ou (Var 2, Var 1),
Ou (Non (Var 1), Non (Var 0))
),
Et ( Ou (Non (Var 2), Var 0),
Ou (Var 2, Var 0)
)
)
Écrivez une fonction quine : formule -> arbre_quine qui prend en paramètre une formule et renvoie l’arbre associé par l’algorithme de Quine.
Écrivez une fonction satisfiable_quine : arbre_quine -> bool qui détermine si une formule est satisfiable depuis l’arbre de l’algorithme de Quine de cette formule.
Si la formule est satisfiable, comment retrouver un modèle depuis l’arbre de Quine ?
Le problème SAT est un problème absolument central en informatique, parce que d’innombrables problèmes de décision se réduisent naturellement à lui. Il faut savoir implémenter l’algorithme de Quine.
Avec l’algorithme de Quine, écrivez une fonction tautologie : formule -> bool qui détermine si une formule propositionnelle est une tautologie. Cette fonction ne doit pas passer par le type arbre_quine.
III. Exercices
Exercice 1 : Fonctions supplémentaires sur les formules propositionnelles
Syntaxe
Écrivez une fonction nb_var_distinctes : formule -> int qui renvoie le nombre de variables propositionnelles distinctes apparaissant dans une formule. On essaiera d’être efficace. Exemples :
# nb_var_distinctes ex1 ;;
– : int = 3
# nb_var_distinctes ex2 ;;
– : int = 2
# nb_var_distinctes ex3 ;;
– : int = 0
Écrivez une fonction sous_formule : formule -> formule -> bool qui détermine si une formule est une sous-formule d’une autre.
Équivalence sémantique
Soit
x in mathcal V, varphiinmathcal P_mathcal V
. On peut définir le quantificateur universel ainsi :
forall x. varphi equiv varphi[top/x]land varphi[bot/x]
Déduisez-en une fonction quantificateur_universel : int -> formule -> formule telle que quantificateur_universel x phi renvoie une formule sémantiquement équivalente à
forall x. varphi
.
En vous inspirant de l’équivalence précédente, donnez une définition possible du quantificateur existentiel, et déduisez-en une fonction quantificateur_existentiel : int -> formule -> formule.
On peut utiliser la fonction equivalence écrite plus haut pour vérifier la validité de certaines équivalences sémantiques fondamentales. Par exemple la double négation
varphiequivlnotlnotvarphi
peut être vérifiée ainsi :
equivalence (Var 0) (Non (Non (Var 0))) [[|false|]; [|true|]]
Montrez les lois de De Morgan à l’aide de la fonction equivalence.
Algorithme de Quine
Avec l’algorithme de Quine, écrivez une fonction valuation_quine : formule -> valuation option qui renvoie une valuation qui satisfait la formule propositionnelle. Le type option sert à gérer le cas où la formule n’est pas satisfiable.
Avec l’algorithme de Quine, écrivez une fonction antilogie : formule -> bool qui détermine si une formule propositionnelle est une antilogie.
Montrez que l’algorithme de Quine termine.
Exercice 2 : portée des variables
Les variables propositionnelles seront dans cet exercice de type ‘a.
Modifiez le type formule afin d’y ajouter les deux quantificateurs ainsi que les connecteurs d’implication et d’équivalence. On appelle ce type ‘a formule_complete.
Définissez dans une variable ex_complet : char formule_complete la formule propositionnelle correspondant à l’arbre suivant :
Une occurrence d’une variable
x
dans une formule est un nœud de l’arbre étiqueté par
x
.
Une occurrence de
x
est dite libre si le chemin reliant l’occurrence à la racine ne contient pas de nœud
forall x
(ou plus précisément, de nœud
forall
dont le fils gauche est
x
) ni de nœud
exists x
. Une occurrence de
x
est dite liée dans le cas contraire.
Une variable est dite libre dans une formule si elle a au moins une occurrence libre, liée si elle a au moins une occurrence liée.
Écrivez une fonction est_liee : ‘a formule_complete -> ‘a -> bool qui indique si une variable est liée dans une formule.
Écrivez une fonction est_libre : ‘a formule_complete -> ‘a -> bool qui indique si une variable est libre dans une formule.
La portée d’une variable liée
x
est la sous-formule
varphi
des formules
forall x. varphi text{ et }exists x. varphi
.
Écrivez une fonction portee : ‘a formule_complete -> bool * ‘a -> ‘a formule_complete option qui prend en paramètre une formule et un couple (b, i) où b vaut true pour désigner le quantificateur universel et false pour désigner le quantificateur existentiel, et i désigne une variable propositionnelle ; et renvoie sa portée. S’il y a plusieurs occurrences liées de cette variable, on renverra la sous-formule située la plus à gauche dans l’arbre de la formule. Si elle n’apparaît pas dans la formule, on renverra None.
Exercice 3 : résolution par force brute du problème SAT
On reprend dans cet exercice les types formule et valuation définis dans les premières parties du TP.
L’algorithme de Quine est une approche par backtracking de la résolution de problème SAT. Comme tout problème de décision, on peut aussi le résoudre avec une approche par force brute.
Cette approche suit en fait un principe similaire à celui des tables de vérité : on évalue la formule propositionnelle pour chaque valuation existante et on regarde si l’une d’elle donne la valeur de vérité V.
On propose de construire l’ensemble des valuations existantes ainsi :
On commence par la valuation associant la valeur de vérité F à toutes les variables.
Pour passer à la valuation suivante :
On cherche la plus grande variable propositionnelle qui a pour valeur de vérité F.
On passe sa valeur de vérité à V.
On passe la valeur de vérité de toutes les variables propositionnelles plus grandes à F.
En appliquant cette méthode pour passer d’une valuation à la suivante, quelle sera la seconde valuation testée ? la troisième ? quatrième ? dernière ?
On définit l’exception suivante :
exception Derniere_valuation
Écrivez une fonction valuation_suivante : valuation -> unit qui modifie la valuation passée en paramètre pour construire la valuation suivante selon la méthode décrite ci-dessus. Cette fonction lève l’exception Derniere_valuation si la valuation passée en paramètre était la dernière à tester.
Écrivez une fonction satisfiable_brute : formule -> bool qui détermine si une formule est satisfiable en essayant toutes les valuations possibles (jusqu’à les épuiser ou en trouver une convenable).
Écrivez de même deux fonctions tautologie_brute : formule -> bool et antilogie_brute : formule -> bool qui déterminent respectivement si une formule propositionnelle est une tautologie ou antilogie avec une approche par force brute.
Pour aller plus loin
Modifiez la fonction ensemble_sous_formules de la première partie pour que la liste renvoyée ne contienne aucun doublon.
Reprenez les fonctions du TP avec l’implémentation en C des formules propositionnelles.
Par Justine BENOUWT
Sous licence CC BY-NC-SA
CC BY-NC-SA
Source des images : production personnelle
- none/plain text
- 24h