Exerciții rezolvate: Logică propozițională

Exercițiul 1. Scrieți o funcție care ia ca parametru o formulă propozițională și returnează o formulă echivalentă, în care negația e aplicată doar direct propozițiilor. (Folosiți regulile lui de Morgan.)

Considerăm următorul tip recursiv pentru formule care pot conține variabile propoziționale (identificate prin numele lor, un șir), și operatorii de negație, conjuncție și disjuncție:

type bexp = V of string
            | Neg of bexp
            | And of bexp * bexp 
            | Or of bexp * bexp

Funcția pe care o scriem va prelucra formula recursiv, prin descompunere structurală, pe fiecare din cele 4 cazuri. Cazul de bază, o variabilă propozițională, rămâne neschimbat. Pentru conjuncție și disjuncție, transformarea trebuie doar aplicată fiecăruia din cei doi operanzi. Lucrul propriu-zis trebuie efectuat pentru (sub)formulele de tip negație, pentru care distingem încă o dată 4 cazuri, după formula aflată "sub" semnul de negație:

let rec push_neg = function
  | V s -> V s
  | And (e1, e2) -> And (push_neg e1, push_neg e2)
  | Or (e1, e2) -> Or (push_neg e1, push_neg e2)
  | Neg e -> (match e with
    | V s -> Neg (V s)
    | Neg e1 -> push_neg e1
    | And (e1, e2) -> Or (push_neg (Neg e1), push_neg (Neg e2))
    | Or (e1, e2) -> And (push_neg (Neg e1), push_neg (Neg e2))
  )

Dacă negația e aplicată doar unei propoziții, rezultatul e literalul negat -- de remarcat că rezultatul din a doua potrivire ("match") de tipare e rezultatul întregii funcții, nu doar transformarea expresiei e din Neg e . Pentru cazul Neg (Neg e1), cele două negații se anulează, deci trebuie prelucrată recursiv doar expresia e1 (acest lucru nu trebuie uitat !). Ultimele două cazuri reprezintă regulile lui de Morgan; și aici, transformarea trebuie aplicată mai departe expresiilor Neg e1 și Neg e2, pentru că și acestea pot fi expresii compuse.
Sintactic, a doua potrivire de tipare (cea interioară) nu trebuia pusă neapărat în paranteze, deoarece apare pe ultima poziție, și orice tipar e asociat cu ultimul "match" (sau "function"); structurarea este însă mai clară așa, si e necesară dacă nu e pe ultima ramură din primul tipar.
Ca exemplu, aplicând funcția scrisă

push_neg (Neg (And (V "a", Or (Neg (V "b"), V "c"))))

obținem rezultatul

Or (Neg (V "a"), And (V "b", Neg (V "c")))

Exercițiul 2. Scrieți o funcție care ia ca parametru o expresie booleană care poate conține constante (false sau true) și simplifică expresia după regulile cunoscute din algebra booleană.

Completăm tipul pentru expresii cu o variantă pentru constantele boolene false și true.

type bexp = B of bool
            | V of string
            | Neg of bexp
            | And of bexp * bexp 
            | Or of bexp * bexp

Observația cheie e că formula trebuie parcursă prin descompunere structurală în subformule, dar simplificarea se face la revenire, identificând tipare de siplificare după ce subformulele respective au fost deja simplificate.
Deasemenea, nu orice formulă poate fi simplificată (de exemplu, ar putea să nu conțină deloc constante boolene), deci rezultatul funcției e tot o formulă (expresie), și nu o valoare booleană. Ca atare, orice rezultat boolean trebuie scris ca și expresie B false sau B true, de tipul bexp, și nu doar ca false sau true (valori de tip bool, care ar produce erori de tip).
Ținând cont de aceste observații, funcția se scrie:

let rec simplify = function
  | Neg e -> (match simplify e with
    | B b -> B (not b)
    | r -> Neg r )
  | And (e1, e2) -> (match (simplify e1, simplify e2) with
    | (B false, _) | (_, B false) -> B false
    | (B true, e) | (e, B true) -> e
    | (r1, r2) -> And (r1, r2) )
  | Or (e1, e2) -> (match (simplify e1, simplify e2) with
    | (B false, e) | (e, B false) -> e
    | (B true, _) | (_, B true) -> B true
    | (r1, r2) -> Or (r1, r2) )
  | e -> e

Pentru fiecare din variante (negație, conjuncție, disjuncție), se face o potrivire de tipare în funcție de rezultatul simplificării subexpresiei. Pentru operatorii binari, potrivirea se poate face direct pe perechea celor două rezultate, (simplify e1, simplify e2) . Deasemenea, ținând cont de comutativitate, putem grupa tiparele simetrice, care au același rezultat.
Ultimul tipar se aplică oricărei expresii care nu s-a potrivit cu niciun tipar anterior. Pentru Neg, And, Or, aceasta înseamnă câ nu se mai fac simplificări după revenirea din simplificarea subexpresiilor. Pentru tiparul exterior, acest caz acoperă constantele și propozițiile, care nu mai pot fi simplificate. În orice potrivire de tipare, e absolut necesar să tratăm toate cazurile (ceea ce dealtfel e sesizat de compilator/interpretor printr-un avertisment).

Marius Minea

Last modified: Sun Nov 10 11:45:00 EET 2013