Exerciții rezolvate: Logică propozițională

Exercițiul 1. Scrieți o funcție care ia ca parametru o formulă în formă normală conjunctivă (listă de listă de literale) și returnează mulțimea tuturor literalelor pure, i.e., care apar cu o singură polaritate (fie doar pozitiv, fie doar negat).

Scriem întâi o funcție care colectează literalele pure dintr-o singură clauză (listă de literale). O variantă de abordare ar fi colectarea literalelor pozitive și negative în două mulțimi, și apoi eliminarea elementelor comune. Alegem o altă soluție: acumulăm mulțimea de propoziții care au apărut cu ambele polarități, și deasemenea mulțimea literalelor pure (care au apărut până în prezent doar cu o polaritate).

Avem nevoie de un tip literal: 

type lit = P of string | N of string
Deasemenea, pentru a crea mulțimi de literale scriem un modul care conține tipul literal și funcția standard de comparare: 
module Lit = struct
  type t = lit
  let compare = compare
end
Pentru literalele care apar cu ambele polarități e suficient să ținem minte mulțimea numelor lor. Instanțiem deci module pentru mulțimi de nume (șiruri) și mulțimi de literale: 
module SS = Set.Make(String)
module LS = Set.Make(Lit)
Avem nevoie deasemenea de o funcție pentru negația unui literal: 
let neg = function
  | P s -> N s
  | N s -> P s
Putem acum defini funcția care prelucrează o clauză. Ea va acumula o pereche de mulțimi: cea a numelor de propoziții care au fost văzute cu ambele polarități, și cea a literalelor care au fosît văzute doar cu o polaritate. Parcurgem lista de literale (clauza) cu List.fold_left. Funcția de prelucrare va avea ca prim parametru (și rezultat) o pereche de mulțimi (bad, good) descrisă ca mai sus, iar ca al doilea parametru, un literal (elementul curent al listei). Distingem trei cazuri: 
let purelit1 = List.fold_left (fun (bad, pure) ->
    function P s | N s as lit -> if SS.mem s bad then (bad, pure)
      else let nl = neg lit in
           if LS.mem nl pure then (SS.add s bad, LS.remove nl pure)
           else (bad, LS.add lit pure)
)
Interpretorul inferează pentru funcția purelit1 următorul tip: 
val purelit1 : SS.t * LS.t -> lit list -> SS.t * LS.t = <fun>
Din cei trei parametri pentru List.fold_left, am specificat doar funcția de prelucrare. Deci, funcția purelit1 va lua ceilalți doi parametri rămași (o valoare inițială pentru perechea de mulțimi, și lista de literale), și va returna o nouă valoare pentru perechea de mulțimi. Astfel, purelit1 poate fi aplicată repetat pentru o listă de clauze, actualizând perechea de mulțimi după prelucrarea fiecărei liste. Pentru a obține funcția finală dorită, iterăm funcția purelit1 cu List.fold_left pe lista de clauze, pornind de la perechea de mulțimi vide. Din rezultat ne interesează doar mulțimea literalelor pure, adică al doilea element al perechii, care se obține cu funcția standard snd (second): 
let purelit clauses = snd (List.fold_left purelit1 (SS.empty, LS.empty) clauses)
Am avut de prelucrat o listă de liste, pentru care sunt necesare două iterări (cicluri) încuibate: o parcurgere a listei de liste, și în interior câte o parcurgere pentru fiecare listă-element. Ambele parcurgeri se fac cu List.fold_left, iar valoarea acumulată după parcurgerea unei liste-element (aici, o clauză) e punctul de plecare pentru parcurgerea următoarei liste-element. E util într-un astfel de caz să definim o funcție pentru parcurgerea unei singure liste (cu o valoare inițială dată deasemenea ca parametru), și aceasta poate fi folosită direct ca funcție pentru ciclul exterior (parcurgerea listei de liste).

Exercițiul 2. Considerăm formule propoziționale reprezentate prin tipul 

type bexp = V of string
            | Neg of bexp
            | And of bexp * bexp 
            | Or of bexp * bexp
care sunt în formulă normală conjunctivă, adică nu există subexpresii And într-o expresie Or, și negația se aplică doar literalelor.
Scrieți o funcție care ia ca parametru o astfel de formulă și returnează o reprezentare ca listă de liste de clauze .

Definim întâi tipurile pentru formula booleană, și pentru literale. O variabilă propozițională V "a" va fi convertită în literalul pozitiv P "a", iar negația ei Neg (V "a") în literalul negativ N "a". 

type bexp = V of string
            | Neg of bexp
            | And of bexp * bexp 
            | Or of bexp * bexp
type lit = P of string | N of string
Mai departe, scriem o funcție care transformă în clauză (listă de literale) o formulă care conține disjuncții. Fiind deja în formă normală conjunctivă, înseamnă că sub o disjuncție nu putem avea conjuncții, iar negația se aplică doar direct propozițiilor.
Pentru o disjuncție, am putea crea separat lista literalelor pentru fiecare subexpresie, și apoi să le concatenăm. Însă concatenarea pentru liste e ineficientă, pentru că trebuie parcursă până la capăt prima listă. Scriem atunci o funcție care primește ca parametru o listă cu literale deja extrase (rezultatul parțial) și adaugă la ea literalele din formulă: 
let rec oneclause lst = function
  | V s  -> P s :: lst
  | Neg (V s)  -> N s :: lst
  | Or (e1, e2) -> oneclause (oneclause lst e1) e2
  | _ -> failwith "formula not in CNF"
Pentru propoziții pozitive sau negate, literaul e adăugat în capul listei. Pentru disjuncție, sunt adăugate întâi literalele din primul operand, apoi din al doilea. Pentru orice alt caz (conjuncție, sau negație aplicată unei formule mai complexe) generăm o excepție -- aceste cazuri nu ar trebui să apară dacă formula e deja în CNF.

Mai departe, construim pe aceeași structură o funcție care ia o listă de clauze și adaugă clauzele pentru o formulă. Pentru o conjuncție, fiecare din operanzi va genera o clauză (sau mai multe, dacă conține la râdul lui conjuncții). Pentru orice altă formulă, folosim funcția anterioară, pornind de la lista vidă de literale: 

let mkclauses =
  let rec mkcls2 clist = function
  | And (e1, e2) -> mkcls2 (mkcls2 clist e1) e2
  | f -> oneclause [] f :: clist
  in mkcls2 []

Marius Minea
Last modified: Sun Nov 10 22:00:00 EET 2013