Logică și structuri discrete - Exerciții

1. Substituții Scrieți o funcție care ia ca parametri o substituție (reprezentată ca dicționar) și un termen și returnează termenul obtinut prin substituție.
Dicționarul (substituția) asociază fiecărei variabile un termen, de exemplu: { x → g(y), y → z }. Aplicând substituția termenului f(x, g(x), z) obținem f(g(z), g(g(z)), z). După cum vedeți, substituția trebuie aplicată din nou și valorii din dicționar, până la capăt. Presupuneți că substituția e corect definită (nu se ajunge la termeni infiniți).

2. Substituții bine definite Scrieți o funcție care ia ca parametru o substituție, reprezentată ca dicționar asociind termeni la șiruri (nume de variabile) și determină (returnează true/false) dacă e bine definită, adică dacă nu va duce la un termen infinit.
De exemplu, substituția { x → z, z → f(y), y → g(x) } e ciclică și ar continua la infinit: x = z = f(y) = f(g(x)) = f(g(z)) = f(g(f(y))) = ...
Scrieți o funcție auxiliară care ia o mulțime de variabile deja întâlnite și un termen și verifică (returnează true/false) că nicicare din variabilele din mulțime nu apar în termen sau în substituția acestuia.
Pentru exemplul dat, pornim cu mulțimea { x } și termenul z asociat lui x. Variabila z nu apare în { x }, deci continuăm să verificăm termenul f(y) asociat lui z, cu mulțimea {x, z} a variabilelor deja văzute. Avem un singur subtermen y care e o variabilă, și nu e în {x, z}, deci continuăm cu substituția g(x) a lui y și mulțimea {x, y, z}. Aici regăsim variabila x (unicul subtermen al lui g(x)) în mulțime, deci substituția nu e bine definită.
Cum un termen conține (în general) o listă de termeni, verificarea va trebui făcută pentru toți termenii din listă. Pentru aceasta puteți folosi List.for_all, tot după cum în tema precedentă, cea mai simplă soluție folosea exists:

type term = V of string
          | F of string * term list

let rec apare v = function
  | V nv -> nv = v
  | F(_, tl) -> List.exists (apare v) tl