Logica predicatelor - Laborator 10

type term = V of string
            | F of string * term list
type predform = Pr of string * term list
                | Neg of predform
                | And of predform * predform
                | Or of predform * predform
                | Forall of string * predform

1. Tipărirea
a) Scrieti o funcție recursivă care tipărește un termen.
b) Folosind funcția de mai sus, scrieți o funcție care tipărește un predicat.
De exemplu, printterm (F ("f", [V "x"; F ("g", [F ("a", []); V "y"]) ])) va tipări f(x, g(a, y)).

2. Variabile libere Scrieți o funcție care ia ca parametru o formulă în logica predicatelor și returnează mulțimea numelor tuturor variabilelor libere din formulă (o mulțime de șiruri).
De exemplu, freevars (And (Forall ("y", Pr("P", [V "x"; V "y"])), Forall ("x", Or (Pr("Q", [V "z"]), Pr("R", [V "x"]))))) e mulțimea {x, z}. Deși x e variabilă legată îm al doilea conjunct, ea e variabilă liberă în primul.

Indicație Pentru orice formulă structurată, mulțimea variabilelor libere e reuniunea mulțimilor pentru formulele componente. Pentru o formulă cu cuantificator, se exclude variabila cuantificată.

Scriem o funcție ajutătoare vars_of_term, întrucât și pentru un predicat, P(t1, t2, ... tn) și pentru un termen-funcție f(t1, t2, ... tn) va trebui să folosim (recursiv) funcția pentru o listă de termeni [t1; t2; ... tn]. E util ca funcția vars_of_term să ia ca parametru suplimentar o mulțime inițială de variabile și să returneze, adăugată la aceasta, mulțimea variabilelor din termen.

Situația e similară obținerii mulțimii tuturor șirurilor dintr-o listă de liste de șiruri. Am indicat mai jos și tipurile raportate de interpretor pentru fiecare funcție scrisă.

module S = Set.Make(String)
                   
let set_add_list = List.fold_left (fun s e -> S.add e s) 
val set_add_list : S.t -> S.elt list -> S.t = <fun>

let set_add_llist = List.fold_left set_add_list 
val set_add_llist : S.t -> S.elt list list -> S.t = <fun>
                                                          
let set_of_llist = set_add_llist S.empty
val set_of_llist : S.elt list list -> S.t = <fun>

În problema noastră, nu prelucrăm liste de șiruri, ci liste de termeni. Putem scrie două funcții mutual recursive folosind sintaxa let rec funcție1 = definiție1 and funcție2 = definiție2 în care fiecare definiție poate folosi ambele nume definite. Parametrul m de mai jos e mulțimea la care se adaugă variabilele din termenul dat ca al doilea parametru:

let rec vars_of_term m = function
  | V s -> ...
  | F (f, tlist) -> vars_of_termlist ...
and vars_of_termlist ... = List.fold_left ...

3. Cuantificare existențială Scrieți o funcție care ia ca parametru o formulă și tipărește pentru fiecare cuantificator existențial lista tuturor variabilelor cuantificate universal ai căror cuantificatori se aplică subformulei respective (adică în interiorul cărora se află cuantificatorul existențial).
Adăugați la tipul pentru formulă cu predicate o variantă pentru cuantificatorul existențial.
Această funcție e utilă pentru skolemizare, unde fiecare variabilă cuantificată existențial e înlocuită cu o funcție nouă având ca argumente toate variabilele corespunzătoare cuantificatorilor universali în interiorul cărora se află.
De exemplu, pentru formula ∀ x ∃ y . R(x, y) ∨ ∀ z ∃ t . P(x, t) ∧ S(y, z) pentru ∃ y se va tipări lista [x] iar pentru ∃ t, lista [x; z]. Cum nu s-a cerut decât tipărirea, funcția nu returnează un rezultat propriu-zis, ci va avea tipul unit (prin consecință, dacă expresiile din corpul funcției sunt apeluri la funcțiile print... care returnează unit).

Indicație Funcția va lua ca parametru suplimentar o listă (inițial vidă). La fiecare parcurgere a unui cuantificator universal, apelul recursiv se face adăugând la listă variabila cuantificată.

4. Număr de parametri Scrieți o funcție care ia ca parametru o formulă și care verifică faptul că fiecare funcție și predicat din formulă e folosit(ă) consecvent cu același număr de parametri.
De exemplu, check_arity (And(Pr("P", [V "x"]), Pr("P", [V "y"; V "z"]))) va returna false, pentru că predicatul P apare odată cu un argument și odată cu două.
La fel și pentru Pr("P", [F ("f", [F ("f", [V "x"; V "y"])])]) care folosește f cu 1 și 2 argumente.

Indicație Rezolvăm întâi o problemă simplă similară: scriem o funcție care returnează mulțimea tuturor numelor de funcții dintr-un termen. Mai exact, funcția ia ca prim parametru o mulțime de nume, și returnează această mulțime la care adaugă toate numele de funcție din termen. Această reformulare ajută la aplicarea repetată pe o listă de termeni, ca în problema 2.
Numele de variabile nu ne interesează, deci în cazul de bază funcția returnează mulțimea dată ca parametru, fără nicio schimbare. Pentru o funcție, adăugăm numele funcției la mulțimea primită, și iterăm recursiv funcția peste toți termenii argument. Prelucrarea cu List.fold_left are ca efect transmiterea la fiecare pas mai departe a mulțimii actualizate.

let rec funnames m = function
  | V s -> m
  | F (f, tlist) -> List.fold_left funnames (S.add f m) tlist

5. Redenumiri Scrieți o funcție care ia ca parametru o formulă cu cuantificatori și redenumește fiecare variabilă legată, adăugând un sufix unic (de exemplu bazat pe un număr).
De exemplu, rename (And (Forall ("x", Exists ("y", Pr("P", [V "x"; V "y"]))), Forall ("x", Pr("Q", [V "x"; V "z"])))) va returna
And (Forall ("x_1", Exists ("y_2", Pr("P", [V "x_1"; V "y_2"]))), Forall ("x_3", Pr("Q", [V "x_3"; V "z"]))), numerotând cei trei cuantificatori și variabilele corespunzătoare. z nu e redenumită, fiind variabilă liberă.
Indicație Folosiți aceeași structură de cod ca la temele pentru formule propoziționale în care se numărau diverse elemente componente. În plus, similar cu problema anterioară, transmiteți la fiecare apel pentru o subformulă un parametru de tip dicționar (corespondență între nume vechi și nume nou), pentru a o putea redenumi consecvent. De exemplu, următoarea funcție redenumește variabilele conform dicționarului dat parametru și numără operatorii de negație.

let rencnt m =
  let rec rc1 n = function
    | V s -> (n, try V (M.find s m) with Not_found -> V s)
    | Neg e -> let (n1, r1) = rc1 (n+1) e in (n1, Neg r1)
    | And (e1, e2) -> let (n1, r1) = rc1 n e1 in
                      let (n2, r2) = rc1 n1 e2 in
                      (n2, And(r1, r2))
  in rc1 1