PROGRAMARE LOGICA ECUATIONALA

editia a III-a

Virgil Emil Cazanescu

October 4, 2008

Chapter 1

IN PRIMUL RAND SEMANTICA

Aceasta varianta este independenta de lectiile privind rescrierea ramamand necesare cunostiintele privind algebrelemultisortate. Mentionam ca cei doi membri ai unei egalitati trebuie sa aiba acelas sort.

1.1 Introducere

Pentru orice signatura multisortata (S,) si orice multime de variabile X notam -algebra liber generata de X cuT(X).

Definitia 1.1.1 O ecuatie conditionata este

(X)l.=s r if H

unde X este o multime S-sortata de variabile, l si r sunt doua elemente de sort s din T(X) iar H o multime finitade egalitati formale din T(X) T(X). 2

O ecuatie conditionata n care H = devine neconditionata si este numita pe scurt ecuatie. In acest caz scriem doar(X)l

.=s r n loc de (X)l

.=s r if .

Definitia 1.1.2 Algebra D satisface ecuatia conditionata (X)l.=s r if H , fapt notat prin

D |= (X)l.=s r if H

daca pentru orice morfism h : T(X) D pentru care hs(u) = hs(v) pentru orice u.=s v H , avem hs(l) = hs(r).

2

In cele ce urmeaza indicele din |= va fi omis. El va fi mentionat atunci cand este pericol de confuzie.Observam ca D |= (X)l

.=s r daca si numai daca hs(l) = hs(r) pentru orice morfism h : T(X) D.

In continuare fixam o multime de ecuatii conditionate, numite axiome sau clauze.

Definitia 1.1.3 Spunem ca algebra D satisface sau ca D e o -algebra si scriem D |= daca D satisface toateecuatiile conditionate din . 2

1.2 Semantica si Corectitudine

Vom lucra ntr-o -algebra A.Fie relatia pe A definita prin

a c daca si numai daca (h : A M |= )hs(a) = hs(c).

Mai observam ca =

{Ker(h) | h : A M |= }.

Deoarece nucleul unui morfism este o relatie de congruenta si deoarece orice intersectie de relatii de congruente esteo relatie de congruenta, deducem ca este o relatie de congruenta.

1

2 CHAPTER 1. IN PRIMUL RAND SEMANTICA

Congruenta este numita congruenta semantica.

Dam doua reguli de deductie ale rescrierii Sub si Rew.

Sub Pentru orice (X) l.=s r if H si orice morfism h : T(X) A

(u.=s v H)hs(u)

.=s hs(v) implica hs(l)

.=s hs(r).

Rew Pentru orice (X) l.=s r if H si orice morfism h : T(X) A

(u.=s v H)(d As )hs(u)

.=s d si hs(v)

.=s d implica hs(l)

.=s hs(r).

Lema 1.2.1 Pentru orice morfism f : A M |= , Ker(f) este nchis la Rew.

Demonstratie: Fie (X)l.=s r if H n si h : T(X) A un morfism cu proprietatea ca pentru orice u

.= v H

exista cuv cu proprietatile h(u) Ker(f) cuv si h(v) Ker(f) cuv. Prin urmare (h; f)(u) = f(cuv) = (h; f)(v) pentruorice u

.= v H . Deoarece h; f : T(X) M |= rezulta ca (h; f)s(l) = (h; f)s(r), deci hs(l) Ker(f) hs(r).2

Deoarece orice relatie reflexiva si nchisa la Rew este nchisa si la Sub obtinem lema urmatoare.

Lema 1.2.2 Pentru orice morfism f : A M |= , Ker(f) este nchis la Sub.

Propozitie 1.2.3 Congruenta semantica este nchisa la substitutie.

Demonstratie: Congruenta semantica este o intersectie de congruente nchise la substitutie. Deoarece o intersectiede congruente nchise la substitutii este o congruenta nchisa la substitutii rezulta ca este o congruenta nchisala substitutie. 2

Propozitie 1.2.4 Daca este o congruenta nchisa la substitutii, atunci A/ |= .

Demonstratie: Notam cu : A A/ morfismul de factorizare canonic.Fie (X)l

.=s r if H n si h : T(X) A/ un morfism astfel ncat ht(u) = ht(v) pentru orice u

.=t v H .

Cum T(X) este algebra proiectiva exista un morfism f : T(X) A astfel ncat f ; = h. Pentru orice u.=t v H

deoarece t(ft(u)) = t(ft(v)) deducem ft(u) ft(v).Deoarece este o congruenta nchisa la substitutii obtinem fs(l) fs(r). Prin urmare s(fs(l)) = s(fs(r)), de

unde hs(l) = hs(r). 2

Fie A factorizarea lui A prin congruenta si fie : A A morfismul cat.

Teorema 1.2.5 A |=

Demonstratie: Se aplica propozitiile 1.2.3 si 1.2.4. 2

Teorema 1.2.6 Pentru orice -algebra B si pentru orice morfism h : A B exista si este unic un morfismh# : A B astfel ncat ;h# = h.

Demonstratie: Este suficient sa aratam ca a c implica h(a) = h(c) si apoi sa aplicam proprietatea de univer-salitate a algebrei cat. Intr-adevar a c implica h(a) = h(c) deoarece h : A B |= . 2

Corolar 1.2.7 Daca A este -algebra initiala, atunci A este -algebra initiala.

Demonstratie: Fie B o -algebra arbitrara.Cum A este -algebra initiala rezulta ca exista un unic -morfism h : A B.Conform teoremei 1.2.6 exista un unic -morfism h# : A B astfel ncat ;h

# = h. Aratam ca h# este uniculmorfism de -algebre de la A la B.Daca f : A B este un alt morfism atunci ; f este morfism de la A la B, rezultand ca ; f = h, deci f = h#.

Chapter 2

UNIFICAREA

Toate algebrele sunt presupuse libere. Prin substitutie vom ntelege un morfism ntre doua algebre libere.

Problema unificarii. Se dau un numar finit de perechi de termeni li.=si ri si se cere gasirea unui unificator,

adica a unei substitutii u cu proprietatea u(li) = u(ri) pentru orice i.

2.1 Algoritmul de unificare

Vom lucra cu doua liste: solutie si de rezolvat. Initial lista solutie este vida si lista de rezolvat contine multimeaecuatiilor de unificat.

Algoritmul de unificare consta n executia nedeterminista a urmatorilor trei pasi.

1. Scoate. Se scoate din lista de rezolvat orice ecuatie de forma t.= t.

2. Descompune. Orice ecuatie din lista de rezolvat de forma

f(a1, a2, . . . , an).= f(b1, b2, . . . , bn)

se nlocuieste cu ecuatiile a1.= b1, a2

.= b2, ..., an

.= bn,

3. Elimina. Orice ecuatie din lista de rezolvat, de forma x.= t sau t

.= x n care x este o variabila care nu apare

n t este mutata sub forma x.= t n lista solutie. In toate celelalte ecuatii x se substitue cu t.

Algoritmul este oprit cu concluzia inexistentei unui unificator n urmatoarele doua cazuri.1) Existenta n lista de rezolvat a unei ecuatii de forma f(a1, a2, . . . , an)

.= g(b1, b2, . . . , bm) cu f 6= g,

2) Existenta n lista de rezolvat a unei ecuatii de forma x.= t sau t

.= x n care x este o variabila care apare n t

si este diferita de t.

Oprirea normala a algoritmului se face prin epuizarea listei de rezolvat, caz n care, asa cum vom proba mai jos, listasolutie coincide cu cel mai general unificator.

2.2 Terminare

Terminarea algoritmului este probata folosind n ordine lexicografica doua criterii exprimate prin numere naturale:

1. numarul variabilelor care apar n lista de rezolvat, care in functie de pasul algoritmului utilizat are urmatoareacomportare

(a) Scoate: ramane egal sau se micsoreaza,

(b) Descompune: ramane egal,

(c) Elimina: se micsoreaza

2. numarul aparitiilor simbolurilor(semnelor) care apar n lista de rezolvat, care se micsoreaza n cele doua cazuricare ne mai intereseaza Scoate si Descompune.

3

4 CHAPTER 2. UNIFICAREA

2.3 Corectitudine

Corectitudinea algoritmului se bazeaza pe demonstrarea faptului ca multimea unificatorilor pentru ecuatiile dinreuniunea celor doua liste este un invariant, adica nu se modifica prin aplicarea celor trei pasi ai algoritmului.

Deoarece pentru pasul Scoate afirmatia este evidenta ne referim doar la ceilalti pasi.Descompune: Observam ca pentru orice substitutie s egalitatea

s(f(a1, a2, . . . , an)) = s(f(b1, b2, . . . , bn))

este echivalenta cuf(s(a1), s(a2), . . . , s(an)) = f(s(b1), s(b2), . . . , s(bn))

adica cu s(ai) = s(bi) pentru orice i [n].Elimina: Observam ca orice unificator u pentru ecuatiile din reuniunea celor doua liste atat nainte de aplicarea

pasului cat si dupa aceasta trebuie sa satisfaca egalitatea u(x) = u(t). Pentru o substitutie s cu proprietatea s(x) =s(t) observam ca

x t; s = s

deoarece (x t; s)(x) = s(t) = s(x) si (x t; s)(y) = s(y) pentru orice alta variabila y. Prin urmare pentru o astfelde substitutie

s(l) = s(r) daca si numai daca s((x t)(l)) = s((x t)(r))

ceea ce arata ca un unificator pentru ecuatiile din reuniunea celor doua liste dinainte de aplicarea pasului esteunificator si pentru ecuatiile din reuniunea celor doua liste de dupa aplicarea pasului si reciproc.

Algoritmul este oprit cu concluzia inexistentei unui unificator deoarece n cele doua situatii mentionate se constataca multimea unificatorilor este vida.

Sa observam ca variabilele care apar n membrul stang al ecuatiilor din lista solutie sunt diferite doua cate douasi nu mai apar n nici una dintre celelalte ecuatii din cele doua liste.

Faptul poate fi dovedit prin inductie.Mentionam ca aplicarea primilor doi pasi ai algoritmului nu modifica lista solutie si nu produc aparitii noi de

variabile n cele doua liste.Fie x

.= t ecuatia introdusa n lista solutie prin aplicarea pasului Elimina. Deoarece variabilele din membrul

stang ai listei solutie precedenta nu apar n celelalte ecuatii rezulta ca variabila x este diferita de celelalte variabilecare apar n membrul stang al ecuatiilor din lista solutie. In plus prin substituirea lui x cu t n celelalte ecuatiivariabila x dispare din ele deoarece x nu apare n t. Deoarece nici x si nici variabilele din membrul stang ai listeisolutie precedenta nu apar n t rezulta ca dupa efectuarea substitutiei lui x cu t variabilele din membrul stang ailistei solutie nu apar n restul ecuatiilor.

Sa presupunem ca algoritmul s-a terminat prin epuizarea listei de rezolvat. Sa notam cu k numarul ecuatiilor dinlista solutie si cu xi

.= ti pentru i [k] ecuatiile din ea.

Fie U substitutia definita prinU(xi) = ti pentru orice i [k].

Definitia este corecta deoarece variabilele xi sunt distincte. Deoarece variabilele xi nu apar n termenii ti deducemca U(ti) = ti, prin urmare U(ti) = U(xi), deci U este un unificator. Vom dovedi ca este cel mai general.

Observam ca pentru orice substitutie s compunerea U ; s este tot un unificator. Vom arata ca orice alt unificatoreste de aceasta forma. Fie u un alt unificator, adica u(xi) = u(ti) pentru orice i [k]. Observam ca U ;u = u, caciu(U(xi)) = u(ti) = u(xi) pentru orice i [k] si u(U(y)) = u(y) pentru orice alta variabila y.

Deci U este cel mai general unificator, deoarece orice alt unificator poate fi exprimat ca o compunere a lui U cuo substitutie. In plus observam ca el este idempotent deoarece U ;U = U .

In cele ce urmeaza vom scrie CGU ca o prescurtare pentru Cel mai General Unificator.

In semantica operationala a limbajelor declarative rescrierea joaca un rol primordial. Pentru a rescrie un elementa cu ajutorul unei reguli l

.=s r se pune problema identificarii unui subtermen al lui a cu imaginea lui l printr-o

substitutie. Aceasta problema de potrivire(matching n engleza) se poate rezolva tot cu ajutorul algoritmului deunificare. Mai precis se cauta a se unifica l cu un subtermen al lui a n care toate variabilele sunt considerateconstante.

Chapter 3

TEOREMELE LUI HERBRAND

3.1 Introducere

Reamintim urmatoarele definitii specifice logicii ecuationale multisortate.

Definitia 3.1.1 Fie -algebra T(X) si G = {l1.=s1 r1, . . . , ln

.=sn rn} o multime de egalitati formale ntre elemente

din T(X). Atunci = (X)l.=s r if G se numeste clauza. Notam cu o multime de clauze.

Notatii 3.1.2 Fie A o -algebra si o clauza ca mai sus. Notam A |= daca pentru orice morfism h : T(X) Aastfel ncat h(li) = h(ri) pentru orice i [n] avem h(l) = h(r). Similar A |= daca A |= pentru orice . Inacest caz spunem ca A este o -algebra.

Notatii 3.1.3 Notam cu T = T() -algebra initiala (adica obiectul initial n categoria -algebrelor) si cu T,-algebra initiala (adica obiectul initial n categoria -algebrelor, subcategorie a categoriei -algebrelor).

Introducem o noua definitie si o noua notatie pentru programarea logica ecuationala.

Definitia 3.1.4 Fie A o -algebra si G = {l1.=s1 r1, . . . , ln

.=sn rn} o multime de egalitati formale ntre elemente

din T(X). A |= (X)G daca exista morfismul h : T(X) A astfel ncat h(li) = h(ri) pentru orice i [n] .

Notatii 3.1.5 Fie o multime de clauze si G = {l1.=s1 r1, . . . , ln

.=sn rn} o multime de egalitati formale ntre

elemente din T(X). Notam |= (X)G daca A |= (X)G pentru orice -algebra A.

Programarea logica ecuationala isi pune urmatoarea problema (X)G.Teoremele lui Herbrand se refera la posibilitatea rezolvarii acestor ecuatii n toate -algebrele.Morfismele de algebre se extind natural pentru perechi de elemente si pentru multimi de perechi de elemente.

Daca h : A B atunci pentru orice a, b A prin definitie h((a, b)) = (h(a), h(b)) sau hs(a.=s b) = (hs(a)

.=s hs(b)).

De asemenea n locul notatiei hs(a) = hs(b) vom mai utiliza hs((a, b)) B.

3.2 Teoremele lui Herbrand

In literatura de specialitate se gasesc doua teoreme ale lui Herbrand. Teorema care urmeaza combina cele douateoreme ntr-una singura.

Teorema 3.2.1 Urmatoarele afirmatii sunt echivalente:

1. |= (X)G ;

2. T, |= (X)G ;

3. Exista : T(X) T astfel ncat |= ()(G), unde (G) = {(l1) =s1 (r1), ..., (ln) =sn (rn)} .

Demonstratie: (1) (2) este evidenta, deoarece T, este o -algebra.(2) (3) Conform ipotezei, exista h : T(X) T, astfel ncat h(li) = h(ri) pentru orice i [n]. Pentru ca

T(X) este algebra libera si deci proiectiva, exista : T(X) T astfel ncat ; = h.

5

6 CHAPTER 3. TEOREMELE LUI HERBRAND

T(X) T

T,

-

@@@@@R

h

Figure 3.1: Proiectivitatea -algebrei T(X)

Avem deci ca (li) = (ri) pentru orice i [n]. Deoarece T, se obtine prin factorizarea algebrei T lacongruenta semantica deducem ca (li) (ri) pentru orice i [n].

Rezulta ca pentru orice morfism f : T A |= ca f((li)) = f((ri)) pentru orice i [n].Prin urmare |= ()(G).(3) (1) Fie M o -algebra. Avem de aratat ca M |= (X)G.Aratam ca ;M : T(X) M este morfismul care verifica proprietatea din definitie. Deoarece M |= ,

din ipoteza rezulta ca M |= ()(G). Utilizand n definitie morfismul M : T M deducem ca M ((li)) =M ((ri)), pentru orice i [n]. Rezulta ca (;M )(li) = (;M )(ri), pentru orice i [n].

Deci M |= (X)G si demonstratia se ncheie. 2

Prima echivalenta a teoremei arata ca problema programarii logice se reduce la rezolvarea ei n -algebra initiala0,, pas deosebit de mare deoarece n loc de o clasa de algebre lucram numai cu o algebra.

A treia afirmatie din teorema ne arata ca rezolvarea problemei se poate face utilizand numai algebre libere. Eaface legatura cu programarea ecuationala si cu conceptul de solutie.

A treia afirmatie mai arata ca pentru existenta solutiei este necesar ca suporturile din -algebra initiala T,corespunzatoare sorturilor variabilelor cuantificate existential, sa fie nevide.

Exercitiu. Data signatura , sa se determine multimea sorturilor pentru care suportul corespunzator din T estenevid.

Din a treia afirmatie a teoremei lui Herbrand se mai vede ca solutia : T(X) T se cauta ntr-o subalgebraT a algebrei T(X) n care este pusa problema (X)G. Chiar daca n T nu mai apare nici o variabila, acest fapteste neglijat n practica. Sa presupunem ca avem de rezolvat ecuatia x = f(y) unde evident X = {x, y}. Solutiaeste data chiar de aceasta ecuatie, adica n T({y}) chiar daca suportul corespunzator lui y este vid n T. Prinurmare ecuatia x = f(y) va avea solutie numai n algebrele n care suportul corespunzator sortului lui y este nevid.In continuare ne vor interesa si astfel de solutii.

Chapter 4

CORECTITUDINEA REGULILOR

PROGRAMARII LOGICE

4.1 Preliminarii

Amintim ca pentru o -algebra A, Sen(A ) = {a=sb | s S, a, b As} (propozitiile lui A).

In continuare vom considera o multime de ecuatii conditionate, iar G Sen(A).

Spunem ca |= (A)G daca, pentru orice -morfism h : A M |= , avem hs(a) = hs(b), pentru oricea=sb G. Pentru usurinta, vom mai nota si cu h(G) M faptul ca hs(a) = hs(b), pentru orice a=sb G, undeh : A M.

Congruenta semantica A , relativ la o -algebra A, este definita prin:

a A b |= a=sb hs(a) = hs(b), pentru orice h : A M|= .

Observatie. |= (A)G daca si numai daca G A .

Propozitie 4.1.1 Daca h : A B este un -morfism, atunci h(A ) B .

Demonstratie Fie a A b. Vrem sa aratam ca h(a) B h(b).

Fie f : B M|= . Cum h; f : A M|= si a A b, rezulta ca (h; f)(a) = (h; f)(b), echivalent cuf(h(a)) = f(h(b)). Cum f a fost ales arbitrar, rezulta ca h(a) B h(b). 2

Corolar 4.1.1 Daca |= (A)G si h : A B un -morfism, atunci |= (B)h(G).

Demonstratie Din ipoteza, conform observatiei, deducem ca G A . Aplicand Propozitia 4.1.1, deducem h(G) B , deci, conform observatiei, |= (B)h(G). 2

Fie A o -algebra si z o noua variabila de sort s astfel ncat z / As. Consideram algebra liber generata deA {z}, T(A {z}), pe care o notam cu A[z]. Un element c din A[z] se numeste context daca numarul aparitiilorlui z n c este 1. Pentru d As, vom nota cu (z d) : A[z] A unicul -morfism cu proprietatea (z d)(z) = dsi (z d)(a) = a, pentru orice a A. Pentru orice t din A[z] si a As, vom prefera sa scriem t[a], n loc de(z a)(t).

Datorita faptului ca regulile programarii logice lucreaza pe multimi de egalitati formale, vom defini notiunea decontext extins. Fie A o -algebra, c A[z]s un context si v As. O egalitate formala de forma c=sv sau v=sc senumeste context extins. Un context extins c=sv (respectiv v=sc) va fi notat cu C. Sa observam ca(c=sv)[a] = (z a)(c=sv) = (c[a]=sc[v]) = (c[a]=sv).

Orice morfism h : A B se poate extinde, n mod unic, la un morfism hz : A[z] B[z] prin hz(z) = z sihz(a) = h(a), pentru orice a A. Pentru orice a A, avem (z a);h = hz; (z h(a)). Pentru un context c A[z]deducem ca h(c[a]) = hz(c)[h(a)], unde hz(c) este context.

7

8 CHAPTER 4. CORECTITUDINEA REGULILOR PROGRAMARII LOGICE

Pentru C un context extins, se observa ca hz(C) este un context extins si ca

h(C[a]) = hz(C)[h(a)].

4.2 Solutii si reguli de deductie

Problema programarii logice este (A)G.

Definitie 4.2.1 Un -morfism s : A B se numeste solutie pentru (A)G daca |= (B)s(G).

Propozitie 4.2.1 Compunerea unei solutii cu orice -morfism este solutie.

Demonstratie Fie s : A B o solutie pentru (A)G si h : B C un morfism. Vrem sa aratam ca s;h : A Ceste solutie pentru (A)G, adica |= (C)(s;h)(G).

Deoarece s : A B este solutie pentru (A)G, atunci |= (B)s(G). Corolarul 4.1.1 implica |= (C)h(s(G)).Deci |= (C)(s;h)(G) si astfel s;h este solutie pentru (A)G. 2

Din propozitia precedenta rezulta ca daca avem o solutie, atunci aceasta nu este unica. Acest fapt ne ndeamnasa cautam o solutie cat mai generala.

In general, solutiile sunt construite n mai multe etape, aparand n final ca o compunere de morfisme. Morfismelecare apar n procesul de calcul si care, speram, ca n final sa furnizeze o solutie sunt numite morfisme calculate.

In continuare vom prezenta regulile de deductie folosite n programarea logica. Aceste reguli ne permit sa trecemde la o multime G de egalitati formale la o alta multime G de egalitati formale, obtinand si un morfism calculat.Aplicarea acestor reguli va nceta n momentul n care ajungem la o multime vida de egalitati formale. In acestpunct, putem compune toate morfismele calculate gasite, n ordinea aparitiei lor, si astfel vom obtine o solutiepentru problema initiala. Aceasta afirmatie va fi probata mai tarziu n ipoteza ca toate regulile de deductie utilizatesunt corecte.

Mentionam n continuare mai multe reguli de deductie utile n programarea logica.

Regula morfismului: Daca G Sen(T(X)) si : T(X) T(Y ), atunci

Gm (G),

cu morfismul calculat .

Regula reflexiei extinse: Daca G Sen(T(X)) si : T(X) T(Y ) astfel ncat s(l) = s(r), atunci

G {l=sr} re (G),

cu morfismul calculat .

Regula reflexiei: Daca G Sen(T(X)) si : T(X) T(Y ) astfel ncat = CGU{l, r}, atunci

G {l=sr} r (G),

cu morfismul calculat .

Regula pararescrierii: Fie G Sen(T(X)), (Y )l=sr if H si morfismul : T(Y ) T(X). Daca C esteun context extins cu variabila distinsa z de sort s, atunci

G {C[s(l)]} pr G (H) {C[s(r)]}.

Mentionam ca pentru pararescriere, morfismul calculat este morfismul identitate.

Regula paramodulatiei extinse: Fie (Y )l=sr if H . Consideram X astfel ncat XY = , G Sen(T(X))si morfismul : T(X Y ) T(Z) astfel ncat s(l) = s(a), unde a T(X)s. Daca C este un context extins cuvariabila distinsa z de sort s, atunci

G {C[a]} pe (G H {C[r]}),

4.3. LEGATURI INTRE REGULILE DE DEDUCTIE 9

cu morfismul calculat /X , restrictia lui la T(X).

Regula paramodulatiei: Fie (Y )l=sr if H . Consideram X astfel ncat X Y = ,G Sen(T(X)) si morfismul : T(X Y ) T(Z) astfel ncat = CGU{l, a}, unde a T(X)s. Daca C esteun context extins cu variabila distinsa z de sort s, atunci

G {C[a]} p (G H {C[r]}),

cu morfismul calculat /X , restrictia lui la T(X).

Comentariu Dorinta exprimata mai sus de a obtine o solutie cat mai generala face ca regulile de deductie utilizate desemantica operationala a programarii logice sa fie mai restrictive. Mai precis reflexia este reflexia extinsa cu conditiasuplimentara ca sa fie cel mai general unificator pentru l si r, iar paramodulatia este paramodulatia extinsa ncare este cel mai general unificator pentru l si a. Conform uzantelor presupunem X Y = , fapt posibil datoritacuantificarii universale a clauzei care ne permite sa alegem variabile noi n locul celor din Y ori de cate ori estenecesar.

4.3 Legaturi ntre regulile de deductie

In continuare vom prezenta legaturile ntre regulile de deductie pentru programarea logica. Aceste legaturi suntimportante, ajutandu-ne, de exemplu, sa demonstram mai usor unele proprietati ale regulilor de deductie.

In primul rand, este evident ca regula reflexiei si regula paramodulatiei sunt cazuri particulare ale regulilor reflexieiextinse si, respectiv, paramodulatiei extinse (caz particular n care cerem ca morfismul implicat n regula sa fie uncel mai general unificator, nu doar un -morfism).

Observam caG {l=sr} m (G) {s(l)

.= s(r)},

cu morfismul calculat , ceea ce arata ca regula morfismului si eliminarea egalitatilor evidente permit eliminarearegulii reflexiei extinse dintre regulile de lucru.

Propozitie 4.3.1 Pararescrierea este un caz particular de paramodulatie extinsa.

Demonstratie Consideram pararescrierea G {C[hs(l)]} pr G h(H) {C[hs(r)]}, unde (Y )l=sr if H sih : T(Y ) T(X) este un -morfism (presupunem X Y = ).

Luam a = hs(l). Sa consideram -morfismul : T(X Y ) T(X) definit prin:

1. (y) = h(y), pentru orice y Y ,

2. (x) = x, pentru orice x X .

Observam ca (t) = t, pentru orice t T(X) si (u) = h(u), pentru orice u T(Y ).Deoarece G este o multime de egalitati formale din Sen(T(X)), rezulta ca s(u=sv) = (s(u)=ss(v)) = (u=sv),

pentru orice u=sv G. In concluzie, putem scrie (G) = G.Similar, H este o multime de egalitati formale din Sen(T(Y )) si astfel avem s(u=sv) = (s(u)=ss(v)) =

(hs(u)=shs(v)), pentru orice u=sv H . In concluzie, putem scrie (H) = h(H).De asemenea, contextul extins C este o egalitate formala din Sen(T(X {z})) si astfel avem z(C) = C.Observam ca s(r) = hs(r) si s(a) = s(hs(l)) = hs(l) = s(l), deoarece l, r T(Y ).Putem aplica regula paramodulatiei extinse pentru (Y )l=sr if H si : T(XY ) T(X) astfel obtinand:

G {C[hs(l)]} = G {C[a]} pe (G H {C[r]}) = (G) (H) (C[r]) =

= G h(H) z(C)[s(r)] = G h(H) C[hs(r)].

Morfismul calculat /X este identitatea lui T(X). 2

Propozitie 4.3.2 Daca pentru orice clauza (Y )l=sr if H din , orice variabila din Y apare n l, atunci pararescriereaeste un caz particular de paramodulatie n care substitutia calculata este o identitate.

10 CHAPTER 4. CORECTITUDINEA REGULILOR PROGRAMARII LOGICE

Demonstratie Pastram notatiile si demonstratia din propozitia precedenta. Vom proba, n plus, ca este cel maigeneral unificator pentru l si a.

Fie u : T(X Y ) B un unificator pentru l si a. Deoarece us(l) = us(a) = us(hs(l)) si orice variabila din Yapare n l, deducem ca u(y) = u(h(y)), pentru orice y Y .

Notam cu u|X restrictia lui u la X si observam ca u|X (x) = u(x), pentru orice x X .Observam ca ;u|X = u: pentru orice x X , u|X ((x)) = u|X (x) = u(x), si pentru orice y Y , u|X ((y)) =

u|X (h(y)) = u(h(y)) = u(y).

Deci este cel mai general unificator pentru l si a deoarece u = ;u|X . 2

Lema 4.3.1 Daca (Y )t=st , atunci Gp (x t)(G), unde x este o variabila care apare n G si nu apare n t.

Demonstratie Alegem o aparitie a lui x n G si scriem G = G C[x], unde C este un context extins. Aplicandregula paramodulatiei pentru (Y )t=st , a = x, = CGU{a, l} = CGU{x, t} = x t, obtinem:

G = G C[x]p (x t)(G C[t]) = (x t)(G).

Ultima egalitate este adevarata deoarece x nu apare n t. 2

Ipoteza x apare n G nu este esentiala deoarece, daca x nu apare n G, (x t)(G) = G si prin urmare (x t)(G)se obtine din G n 0 pasi.

Lema 4.3.2 (Lema substitutiei) Daca sunt ndeplinite urmatoarele conditii: G este o multime finita,(x)x=x pentru orice variabila x, (x1 x2 . . . xn)f(x1, x2, . . . , xn)=f(x1, x2, . . . , xn) pentru orice sim-bol de operatie f , atunci regula morfismului poate fi realizata prin regula paramodulatiei.

Demonstratie Primele doua afirmatii care urmeaza dovedesc ca axiomele lemei substitutiei, mai sarace decat celeale lemei 4.3.1, sunt suficiente pentru a demonstra concluzia lemei 4.3.1:

1. Substitutia unei variabile x cu o variabila y poate fi realizata prin regula paramodulatiei n prezentaaxiomei (y)y=y.

In cazul n care x apare n G si x 6= y se aplica Lema 4.3.1. In rest, evident.

2. Aratam ca substitutia unei variabile cu un termen poate fi realizata prin paramodulatie n prezentaaxiomelor (x)x=x si (x1 x2 . . . xn)f(x1, x2, . . . , xn)=f(x1, x2, . . . , xn).

Vom demonstra acest lucru prin inductie dupa structura termenului t.Primul pas al inductiei este chiar (1).Presupunem ca t = f(t1, t2, . . . , tn).Daca x nu apare n G, atunci nu avem nimic de demonstrat. Presupunem ca x apare n G si folosind

(x1 x2 . . . xn)f(x1, x2, . . . , xn)=f(x1, x2, . . . , xn) , unde variabilele x1, . . . , xn sunt noi, si Lema 4.3.1 deducem

Gp (x f(x1, x2, . . . , xn))(G).

In continuare se aplica ipoteza de inductie pentru orice 1 i n, substituind fiecare xi cu ti.Mai observam ca

x f(x1, x2, . . . , xn) ; x1 t1 ; x2 t2 ; . . . ; xn tn = x f(t1, t2, . . . , tn),

deoarece variabilele x1, x2, . . . , xn sunt noi.

3. Aratam ca regula morfismului poate fi realizata prin regula paramodulatiei.

Fie h : T(X) T(Y ). Cum var(G) = {x1, x2, . . . , xn} X , a realiza regula morfismului revine la a nlocuifiecare variabila xi cu h(xi). Putem realiza acest lucru conform punctelor (1) si (2):

- ntai nlocuim fiecare variabila xi cu o variabila noua zi, pentru orice 1 i n:

Gp (x1 z1)(G)p . . .p (xn zn)(. . . (x1 z1)(G) . . .) = G

- acum nlocuim pentru fiecare 1 i n, variabila zi cu h(xi):

Gp (z1 h(x1))(G)

p . . .

p (zn h(xn))(. . . (z1 h(x1))(G) . . .) = h(G). 2

4.4. CORECTITUDINEA REGULILOR DE DEDUCTIE 11

Paramodulatie

Paramodulatieextinsa

Pararescriere Morfism Reflexieextinsa

Reflexie

-eliminareaegalitatiilor

XXXXXXXXXXXXXXXXXz

Lema 3.1

?

var(l) = YProp.3.2

QQ

QQQk

Prop.3.1

/

9

9

ZZZ+

Prop.3.3

6

Figure 4.1: Legaturile dintre regulile de deductie

Observatie. In demonstratia anterioara, la pasul (3), este extrem de important sa schimbam toate variabilele xi cuvariabile noi. Altfel am putea obtine rezultate nedorite, ca n exemplul de mai jos:

Daca h : T({x, y}) T({x, y, z}), h(x) = z, h(y) = x si G = {x=y}, atunci:

h(G) = (h(x)=h(y)) = (z=x),

(x h(x))((y h(y))(G)) = (x h(x))(x=x) = (z=z).Deci h(G) 6= (x h(x))((y h(y))(G)).

Propozitie 4.3.3 Regula paramodulatiei extinse se poate obtine din regula morfismului si regula pararescrierii.

Demonstratie Fie (Y )l=sr if H , : T(X Y ) T(Z) astfel ncat s(l) = s(a), unde a T(X)s. Fie Cun context extins si z o variabila noua. Aplicand regula morfismului pentru morfismul , obtinem:

G {C[a]} m (G) {(C[a])}.

Mentionam urmatoarele egalitati:

(C[a]) = z(C)[(a)] = z(C)[(l)].

Acum putem aplica regula pararescrierii si obtinem:

(G) {z(C)[(l)]} pr (G) (H) {z(C)[(r)]} = (G H {C[r]}).

Deci G {C[a]} m (G) {z(C)[(l)]} pr (G H {C[r]}). 2

Putem sintetiza legaturile gasite ntre regulile de deductie pentru programarea logica prin Figura 1.

4.4 Corectitudinea regulilor de deductie

Definitie 4.4.1 Fie R o regula de deductie. Sa presupunem ca aplicand regula R obtinem G R G cu morfismulcalculat . Spunem ca regula R este o regula corecta daca este ndeplinita urmatoarea conditie: daca s este osolutie pentru G, atunci ; s este solutie pentru G.

Daca se aplica numai reguli corecte ajungandu-se, n final, la multimea vida de ecuatii (sau la o multime formatadoar din egalitati adevarate), atunci compunerea tuturor morfismelor calculate este o solutie a problemei initiale.Aceasta afirmatie rezulta din faptul ca morfismul identitate este solutie pentru orice multime de egalitati adevarate,inclusiv multimea vida.

In continuare vom arata ca regulile de deductie considerate n sectiunile anterioare sunt corecte.

Deoarece |= (X)l=sl, orice solutie pentru G este solutie si pentru G{l=sl}. Prin urmare eliminarea egalitatiloradevarate este o regula corecta.

Propozitie 4.4.1 Regula morfismului este corecta.

Demonstratie Presupunem ca G m (G), unde : T(X) T(Y ). Fie s : T(Y ) T(Z) o solutie pentru(G), adica |= (Z)s((G)). Trebuie sa aratam ca ; s este solutie pentru G, adica |= (Z)(; s)(G), ceea ce esteevident. 2

12 CHAPTER 4. CORECTITUDINEA REGULILOR PROGRAMARII LOGICE

Propozitie 4.4.2 Regula reflexiei extinse este corecta.

Demonstratie Stim ca regula reflexiei extinse se poate obtine din regula morfismului. Cum regula morfismului estecorecta, rezulta ca si regula reflexiei extinse este corecta. 2

Corolar 4.4.1 Regula reflexiei este corecta.

Propozitie 4.4.3 Regula pararescrierii este corecta.

Demonstratie Consideram pararescrierea G C[s(l)]pr G (H) {C[s(r)]}, unde(Y )l=sr if H si : T(Y ) T(X) un -morfism.

Fie S : T(X) B o solutie pentru (X)G (H) {C[s(r)]}, adica

|= (B)S(G (H) {C[s(r)]}). (1)

Avem de aratat ca S : T(X) B este solutie pentru (X)(G C[s(l)]), adica

|= (B)S(G {C[s(l)]}).

Fie h : B M|= . Din (1) deducem (S;h)(G) (;S;h)(H) (S;h)(C[s(r)]) M . Prin urmare deducem:

(S;h)(G) M , (2)

(;S;h)(H) M , (3)

(S;h)(C[s(r)]) M . (4)

Deoarece M |= (Y )l=sr if H , folosind morfismul ;S;h : T(Y ) M si relatia (3), deducem ca(;S;h)s(l) = (;S;h)s(r). (5)

Probam ca(z (l));S;h = (z s(r));S;h. (6)

Observam ca cei doi membri sunt -morfisme de la T(X {z}) la M.Pentru orice x X avem (z s(l))(x) = x = (z s(r))(x). Pe de alta parte (z s(l))(z) = s(l) si

(z s(r))(z) = s(r). Folosind (5) deducem ca

((z s(l));S;h)s(z) = (;S;h)s(l) = (;S;h)s(r) = ((z s(r);S;h)s(z).

Prin urmare egalitatea (6) este probata.

Observam ca h(S(C[s(l)])) = ((z s(l));S;h)(C)(6)= ((z s(r));S;h)(C) = (S;h)(C[s(r)]).

Din (4) deducem ca h(S(C[s(l)])) M . Folosind (2) deducem h(S(G {C[s(l)]})) M . 2

Propozitie 4.4.4 Regula paramodulatiei extinse este corecta.

Demonstratie Din Propozitia 4.3.3 stim ca orice paramodulatie extinsa se poate obtine din regula morfismului siregula pararescrierii. Din Propozitiile 4.4.1 si 4.4.3 stim ca regulile morfismului si pararescrierii sunt corecte, de underezulta ca si regula paramodulatiei extinse este corecta. 2

Corolar 4.4.2 Regula paramodulatiei este corecta.

Chapter 5

RESCRIERI

5.1 Reguli de Deductie pentru Rescriere

Reamintim alte reguli de deductie pentru Rescriere n algebra A denumite Reflexivitate, Tranzitivitate si Compa-tibilitate cu operatiile din :

R a.=s a

T a.=s d si d

.=s c implica a

.=s c

C ai.=si ci pentru i [n] implica A(a1, a2, . . . , an)

.=s A(c1, c2, . . . , cn) pentru orice s1s2...sn,s.

Aceste reguli mpreuna cu Sub permit o demonstratie mai usoara a rezultatelor teoretice.

Pornind de la regulile de substitutie respectiv rescriere vom introduce nca doua reguli de deductie n algebra A,substitutia si respectiv rescrierea n subtermeni.

SSub Pentru orice (X) l.=s r if H si orice morfism h : T(X) A

(u.=s v H)hs(u)

.=s hs(v) implica (c A[z]s context) c[hs(l)]

.=s c[hs(r)]

SRew Pentru orice (X) l.=s r if H si orice morfism h : T(X) A

(u.=s v H)(d As )hs(u)

.=s d si hs(v)

.=s d implica (c A[z]s context) c[hs(l)]

.=s c[hs(r)]

Remarcati ca SRew, rescrierea ntr-un subtermen, este o regula de deductie mai puternica decat Rew, rescrierea,care poate fi obtinuta din SRew pentru c = z. Analog SSub = Sub.

Se observa ca Rew si R implica Sub. Indicatie: se ia d = h(v).

5.2 Rescriere

Data o multime de ecuatii conditionate putem defini rescrierea, sau mai pe scurt rescrierea, ca fiind cea mai micarelatie nchisa la R, T, C, Rew. Din pacate unele demonstratii sunt greu de facut lucrand cu o astfel de definitie,fapt pentru care vom da n cele ce urmeaza o constructie efectiva pentru rescriere. Constructia este facuta n treietape, multimea intervenind numai n a treia etapa. In prima etapa este definita nchiderea la contexte ale uneirelatii. In a doua etapa este construita nchiderea unei relatii n multimea preordinilor compatibile cu operatiile

5.2.1 Inchiderea la contexte

Definitia 5.2.1 O relatie Q pe A se numete nchisa la contexte daca pentru orice context c si pentru orice perechede elemente a, d din A, aQd implica c[a]Qc[d].

Observatia 5.2.2 Fie Q o relatie pe A nchisa la contexte. Daca Q este nchisa la Sub, respectiv Rew, atunciQ este nchisa la SSub, respectiv SRew.

Definitia 5.2.3 O relatie AA se numeste compatibila pe componente cu operatiile algebrei A daca

a si d implica A(a1, . . . , ai1, a, ai+1, . . . , an) sA(a1, . . . , ai1, d, ai+1, . . . , an)

pentru orice s1...sn,s, orice i [n], unde aj Asj pentru orice j {1, . . . , i 1, i+ 1, . . . , n} si a, d Asi .

13

14 CHAPTER 5. RESCRIERI

Propozitie 5.2.4 O relatie este nchisa la contexte daca si numai daca este compatibila pe componente cu operatiilealgebrei.

Demonstratie: Presupunem Q nchisa la contexte. Pentru a demonstra compatibilitatea pe componente cu operatia aplicam ipoteza pentru un context de forma (a1, . . . , ai1, z, ai+1, . . . , an).

Reciproca se arata prin inductie structurala n A[z].Pasul 0: c = z. Pentru orice (a, d) Q, c[a] = a, c[d] = d, deci (c[a], c[d]) Q.Pentru c = (a1, . . . , ai1, c

, ai+1, . . . , an) unde c A[z] este un context

c[a] = (z a)(c) = A(a1, . . . , ai1, (z a)(c), ai+1, . . . , an) = A(a1, . . . , ai1, c

[a], ai+1, . . . , an).

La fel c[d] = A(a1, . . . , ai1, c[d], ai+1, . . . , an).

Din ipoteza de inductie c[a]Qc[d] si tinand cont de compatibilitatea pe componente obtinem c[a]Qc[d].

Definitia 5.2.5 Daca Q este o relatie pe A vom nota

Q = {(c[a], c[d]) : (a, d) Qs, c A[z] este context unde variabila z are sortul s}.

Propozitie 5.2.6 Q este cea mai mica relatie inchisa la contexte care include Q.

Demonstratie: Pentru a dovedi ca Q este inchisa la contexte, vom prefera sa aratam ca este compatibila pecomponente cu opreratiile. Fie (c[a], c[d]) n Q unde (a, d) Q, un simbol de operatie si ai niste elemente dinA. Folosind contextul c = (a1, . . . , ai1, c, ai+1, . . . , an) deducem ca (c[a], c[d]) este n Q. Dar calculand ca maisus

c[a] = A(a1, . . . , ai1, c[a], ai+1, . . . , an) si c[d] = A(a1, . . . , ai1, c[d], ai+1, . . . , an)

prin urmare (A(a1, . . . , ai1, c[a], ai+1, . . . , an), A(a1, . . . , ai1, c[d], ai+1, . . . , an)) este n Q.Incluziunea Q Q se demonstreaza folosind contextul z.Daca R este nchisa la contexte, atunci Q R implica Q R.

5.2.2 Inchiderea la preordini compatibile cu operatiile

Lema 5.2.7 (Compatibilitatea pe argumente) Fie AA o relatie tranzitiva si reflexiva n algebra A. Daca este compatibila pe componente cu operatiile algebrei A, atunci e compatibila cu operatiile, adica nchisa la C.

Demonstratie: Fie s1...sn,s si ai, bi Asi astfel ncat aisibi pentru orice i [n].Aratam ca A(a1, . . . , an) sA(b1, . . . , bn).Daca n = 0 avem A sA din reflexivitate.Daca n = 1 avem din ipoteza A(a1) sA(b1).Daca n 2 aplicand succesiv ipoteza obtinem

A(a1, a2, . . . , an) sA(b1, a2, . . . , an) sA(b1, b2, a3, . . . , an) s . . . sA(b1, b2, . . . , bn)

Din tranzitivitatea relatiei deducem A(a1, a2, . . . , an) sA(b1, b2, . . . , bn)

Propozitie 5.2.8Q este cea mai mica preordine compatibila cu operatiile care include Q.

Demonstratie: Deoarece relatiaQ este reflexiva si tranzitiva este suficient sa demonstram compatibilitatea cu

operatiile numai pentru cate o componenta, adica sa aratam pentru fiecare s1...sn,s ca aQ d implica

A(a1, . . . , ai1, a, ai+1, . . . , an)Q A(a1, . . . , ai1, d, ai+1, . . . , an).

Probam prin inductie dupa numarul pasilor din aQ d. Presupunem deci a Q u si u

Q d cu un numar

mai mic de pasi ceea ce prin ipoteza de inductie implica

A(a1, . . . , ai1, u, ai+1, . . . , an)Q A(a1, . . . , ai1, d, ai+1, . . . , an).

Deoarece Q este compatibila pe componente cu operatiile, din a Q u rezulta ca

A(a1, . . . , ai1, a, ai+1, . . . , an) Q A(a1, . . . , ai1, u, ai+1, . . . , an).

Prin tranzitivitate obtinem A(a1, . . . , ai1, a, ai+1, . . . , an)Q A(a1, . . . , ai1, d, ai+1, . . . , an).

Evident Q QQ .

Fie R o preordine compatibila cu operatiile care include Q. Compatibilitatea cu operatiile implica Q R, de

unde deducemQ R deoarece R este reflexiva si tranzitiva.

Notam u Q v daca exista a A astfel ncat uQ a si v

Q a.

5.3. CORECTITUDINEA RESCRIERII 15

5.2.3 rescriere

Fixam

Definim prin inductie sirul crescator de multimi de perechi de elemente din A.

Q0 =

Qn+1 = {(h(l), h(r)) : (Y )l =s r if H , h : T(Y ) A, si ((u, v) H)hs(u) Qn hs(v)}

Prin definitie Q este reuniunea sirului crescator definit mai sus.

In cazul n care Q este definita ca mai sus, n loc deQ vom prefera sa scriem

= .

Relatia

= este denumita rescriere sau mai scurt rescriere.

Propozitie 5.2.9

= este nchisa la SRew.

Demonstratie: Fie (Y )l =s r if H , h : T(Y ) A morfism cu proprietatea hs(u) Q hs(v) pentru orice

(u, v) H si un context c A[z]s . Trebuie aratat ca c[h(l)]

= c[h(r)].

Deoarece H este finita si numarul pasilor utilizat n hs(u) Q hs(v) unde (u, v) H este finit exista un n naturalastfel ncat hs(u) Qn hs(v) pentru orice (u, v) H. Prin urmare (h(l), h(r)) Qn+1. Deoarece (h(l), h(r)) Q

deducem c[h(l)]

= c[h(r)]. 2

Propozitie 5.2.10

= este cea mai mica relatie nchisa la R, T, C si Rew.

Demonstratie: Evident

= este nchisa la R, T si C si, fiind nchisa la SRew, este nchisa si la Rew.

Fie W o relatie nchisa la R, T, C si Rew. Demonstram prin inductie dupa n ca Qn W.Daca n = 0 avem Q0 = W.Pentru n 1 fie (h(l), h(r)) Qn, unde (Y )l =s r if H , h : T(Y ) A si ((u, v) H)hs(u) Qn1 hs(v).Din ipoteza de inductie Qn1 W . Cum W este nchisa la C rezulta ca W este nchisa la contexte, deci Qn1

W . Folosind faptul caW este nchisa la R si T rezulta caQn1W . Din ((u, v) H)hs(u) Qn1 hs(v) obtinem

((u, v) H)hs(u) W hs(v). Folosind nchiderea lui W la Rew rezulta ca (h(l), h(r)) W , deci Qn W.

Prin urmare Q W si folosind propozitia 5.2.8 deducem caQW.

5.3 Corectitudinea rescrierii

Toate regulile de deductie de mai sus sunt corecte pentru . Vom demontra acest fapt numai pentru cele maiimportante.

Lema 5.3.1 Regulile R, T si C sus sunt corecte pentru .

Demonstratie: Relatia este o congruenta, prin urmare este reflexiva, tranzitiva si compatibila cu operatiile( s1s2...sn,s, ai bi pentru orice i [n] implica A(a1, a2, . . . , an) A(b1, b2, . . . , bn)). De aici rezulta ca este nchisa la regulile de deductie R, T si C, adica ele sunt corecte pentru .

Intr-o lectie anterioara s-a demonstrat ca Sub si Rew sunt corecte pentru . Tinand cont de observatiile de maisus putem deduce:

Corolar 5.3.2 . (Corectitudinea rescrierii pentru )

In general rescrierea nu este completa pentru .

16 CHAPTER 5. RESCRIERI

5.4 Intalnirea prin rescriere. Corectitudine si completitudine

Fie relatia de ntalnire atasata lui. Prin definitie a b daca si numai daca exista c astfel ncat a

c si

b c. Observam ca . (Corectitudinea ntalnirii pentru )

Propozitie 5.4.1 este nchisa la Sub.

Demonstratie: Fie (X)l =s r if H n si h : T(X) A un morfism cu proprietatea ca ht(u) ht(v) pentru

orice u =t v H. Prin urmare pentru orice u =t v H exista cuv cu proprietatile h(u) cuv si h(v)

cuv.

Cu Rew deducem h(l) h(r) deci h(l) h(r). 2

Reamintim ca daca este o congruenta nchisa la substitutii, atunci A/ |= .

Definitia 5.4.2 O relatie pe o multime A se numeste confluenta daca

(a, b, c A){[a b si a c] (d A)[b d si c d]}. 2

Propozitie 5.4.3 Daca este o preordine confluenta pe multimea A, atunci relatia definita prin

a b (c A)a c si b c

este cea mai mica echivalenta pe A care include .

Demonstratie:

Reflexivitatea rezulta luand c := a.

Simetria este evidenta.

Probam tranzitivitatea. Fie a b si b c. Observam ca exista d, e A astfel ncat a d, b d, b e sic e. Din confluenta rezulta existenta lui f A astfel ncat d f si e f . Rezulta ca a f si c f , decia c.

Pentru a dovedi ca , presupunand ca a b si observand ca b b deducem a b

Fie o relatie de echivalenta pe A care include . Probam ca include . Presupunand ca a b rezultaexistenta lui c A astfel ncat a c si b c. Deducem a c si b c, deci a b. 2

Observatia 5.4.4 Daca este o preordine confluenta si compatibila pe o -algebra multisortata, atunci este ocongruenta.

Demonstratie: Fie s1s2...sn,s si ai bi pentru orice i [n]. Pentru orice i [n], exista ci astfel ncat ai cisi bi ci, prin urmare

A(a1, a2, . . . , an) A(c1, c2, . . . , cn) si A(b1, b2, . . . , bn) A(c1, c2, . . . , cn).

Deci A(a1, a2, . . . , an) A(b1, b2, . . . , bn). 2

Teorema 5.4.5 Daca este confluenta, atunci este completa.

Demonstratie: Confluenta lui este necesara pentru ca sa devina congruenta. Deoarece este nchisa la

Sub deducem ca A/ |= .Fie a b. Utilizand morfismul de factorizare f : A A/ |= deducem f(a) = f(b) deci a b. 2

Chapter 6

COMPLETITUDINEA

PARAMODULATIEI

6.1 Prolog

Reamintim ca nseamna o multime de egalitati adevarate.

Teorema 6.1.1 Daca a d, atunci {a=sd}pr .

Demonstratie Presupunem a d. Atunci exista v astfel ncat a v si d

v. Tinand cont de definitia lui

,

putem scrie aQ v si d

Q v. Deoarece Q este reuniunea sirului crescator {Qn}nN , rezulta ca exista un numar

natural n cu proprietatea aQn v si d

Qn v, deci a Qn d.

Aratam prin inductie dupa n ca {a=sd}pr . Cazul n = 0 este evident. Presupunem ca pentru orice x, y

daca x Qn y, atunci {x=sy}pr . Presupunem ca a Qn+1 d.

Facem o noua inductie dupa numarul pasilorQn+1 folositi. Daca numarul pasilor este 0, atunci a = d, concluziafiind evidenta.

In cazul contrar, presupunem, de exemplu, ca a Qn+1 w si w Qn+1 d cu un pas mai putin. Din ipoteza de

inductie putem scrie {w=sd}pr .

Deoarece a Qn+1 w exista (Y )l=sr if H , morfismul h : T(Y ) T(X) astfel ncat h(u) Qn h(v),pentru orice u=v H , si contextul c n T(X {z}) astfel ncat a = c[hs(l)] si w = c[hs(r)]. Observam ca{c[hs(l)]=sd} pr h(H) {c[hs(r)]=sd} = h(H) {w

.=s d}.

Prin urmare, deoarece {w=sd}pr , deducem ca {a=sd}

pr h(H). Deoarece h(u) Qn h(v), pentru orice

u=v H , din ipoteza de inductie deducem h(H)pr , deci {a=sd}

pr . 2

Corolar 6.1.1 Daca G este o multime finita astfel ncat G , atunci Gpr .

6.2 Completitudinea

Observam ca identitatea lui T(Y ) este solutie pentru (Y ) deoarece |= (Y ). Prin urmare, daca Gp

cu morfismul calculat , atunci este o solutie pentru (X)G. Prin urmare, putem opri rezolvarea n momentulajungerii la o multime de egalitati adevarate.

Presupunem ca multimea de ecuatii conditionate satisface urmatoarele conditii: (x) x=x , pentru oricevariabila x, (x1 x2 . . . xn)f(x1, x2, . . . , xn)=f(x1, x2, . . . , xn) , pentru orice simbol de operatie f , si, pentruorice axioma (Y )l=sr if H , orice variabila din Y apare n l.

Teorema 6.2.1 (Teorema de completitudine) In conditiile de mai sus, daca este completa, atunci oricesolutie poate fi obtinuta numai cu regula paramodulatiei.

Demonstratie Fie : T(X) T(Y ) o solutie pentru (X)G, adica |= (Y )(G). Prin urmare, (G) este osubmultime a congruentei semantice, adica (G) .

17

18 CHAPTER 6. COMPLETITUDINEA PARAMODULATIEI

Deoarece este completa, adica =, deducem ca (G) . Conform Prologului obtinem (G)pr .

Deoarece pentru orice axioma (Y )l=sr if H , orice variabila din Y apare n l, deducem, din Propozitia4.3.2, ca orice pararescriere este un caz particular de paramodulatie n care substitutia calculata este o identitate.In concluzie, putem scrie (G)

p cu substitutia calculata identitatea.

Din Lema substitutiei deducem ca Gp (G) cu substitutia calculata .

Deci Gp cu substitutia calculata . 2

Chapter 7

COMPLETITUDINEA

NARROWINGULUI

7.1 Forme normale

Reamintim ca este relatia de rescriere n A.

Definitia 7.1.1 Elementul n A se numeste o forma normala pentru daca

(b A)(n b implica n = b).

Fie N multimea elementelor din A care sunt forme normale. Presupunem axioma Formei Normale unice

FN! (a A)(! fn(a) N)a fn(a).

Observatia 7.1.2 Daca a d, atunci fn(a) = fn(d).

Demonstratie: Din ipoteza si d fn(d) deducem a

fn(d), deci din unicitatea formei normale a lui a

deducem fn(a) = fn(d).

Observatia 7.1.3 Axioma FN! implica este confluenta.

Demonstratie: Presupunem a d si a

c. Deducem fn(a) = fn(d) = fn(c), deci d

fn(d) si c

fn(d).

Observatia 7.1.4 Functia fn : A N este surjectiva si

a d fn(a) = fn(d).

Demonstratie: Deoarece pentru orice element n n forma normala n = fn(n) rezulta surjectivitatea functiei fn.

Presupunem fn(a) = fn(d). Deoarece a fn(a) si d

fn(a) deducem a d.

Presupunem a d. Fie c A astfel ncat a c si d

c. Deducem fn(a) = fn(c) si fn(d) = fn(c), deci

fn(a) = fn(d). 2Pentru cazul algebrelor libere mai mentionam ca orice subexpresie a unei forme normal este tot o forma normala.

7.2 Introducere

Se lucreaza n algebre libere. Vom nota cu T(X) algebra din care ncepem sa lucram.Fie (Y )l

.=s r if H o clauza. Multimea de variabile Y va fi disjuncta de X . Vom presupune ca T(X) si

T(Y ) sunt subalgebre n T(X Y ) si notam cu iX si iY morfismele incluziune.

In continuare vom lucra cu un caz particular de paramodulatie denumit narrowing sau ngustare.

19

20 CHAPTER 7. COMPLETITUDINEA NARROWINGULUI

Narrowing(Ingustare): Fie (Y )l.=s r if H si = CGU(a, l) : T(X Y ) B unde a T(X) nu este o

variabila. Daca G este o multime de egalitati formale si C este un context extins din T(X {z}), atunci

G {C[a]} n (G H {C[r]})

cu morfismul calculat iX ; .2

Mentionam ca ipoteza care apare mai jos si anume ca membrul stang al concluziei unei axiome nu este o variabilaeste o ipoteza naturala deoarece n caz contrar daca conditiile axiomei sunt verificate, atunci orice termen ar puteafi rescris.

Propozitie 7.2.1 Daca pentru orice clauza (Y )l.=s r if H din l nu este variabila si orice variabila din Y apare

n l, atunci pararescrierea este un caz particular de ngustare n care substitutia calculata este o identitate.

Demonstratie: Este suficient sa reluam demonstratiile propozitiilor 4.3.1 si 4.3.2 si din egalitatea a = hs(l) dinfaptul ca l nu este o variabila rezulta ca nici a nu este variabila.

7.3 Lema de ridicare

Definitia 7.3.1 O substitutie se numeste normala daca duce orice variabila ntr-un element n forma normala.

Propozitie 7.3.2 Presupunem ca multimile de variabile X si Y sunt disjuncte si ca T(X) si T(Y ) sunt subalgebren T(X Y ).

Fie l T(Y ) astfel ncat orice variabila din Y apare n l si a T(X). Fie : X Y TZ o substitutie acarei restrictie la X este normala si (a) = (l).

Daca = CGU(a, l) : X Y TV si este unica substitutie pentru care = ; , atunci este normala.

Demonstratie: Existenta lui CGU(a, l) rezulta din faptul ca este unificator pentru a si l. In plus, fara a restrangegeneralitatea, putea sa presupunem ca V X Y si ca (v) = v pentru orice v V.

Fie v V. Vom studia doua cazuri.1. Daca v X , atunci (v) = ((v)) = (v) este normala prin ipoteza.2. Presupunem v Y . Deoarece a T(X) si v 6 X rezulta ca variabila v nu apare n a. Deoarece Y este

multimea variabilelor care apar n l, v apare n l. Dar (v) = v implica aparitia lui v n (l) = (a). Deoarecevariabila v nu apare n a rezulta ca v a fost introdus n (a) prin substitutia , deci exista x X o variabila careapare n a, astfel ncat v apare n (x). Prin urmare (v) este subtermen n ((x)) = (x). Deoarece (x) este prinipoteza o forma normala, rezulta ca orice subtermen al sau este o forma normala. In particular (v) este o formanormala. 2

Daca : X Z si : Y Z sunt doua functii cu domeniile disjuncte notam cu < , >: X Y Z unicafunctie care pe X actioneaza ca si pe Y ca .

Propozitie 7.3.3 Pentru orice (Y )l = r if H din presupunem ca orice variabila din Y apare n l. Fie G omultime de egalitati din T(X).

Daca : T(X) T(Z) este normala si(G) pr Q,

atunci = cu normala, exista R cu (R) = Q si

G n R cu substitutia calculata .

Demonstratie: Fie (Y )l.= r if H regula si : T(Y ) T(Z) substitutia utilizate n pararescrieie. Vom

presupune ca variabilele din Y sunt noi, adica Y este disjunct de X .Datorita normalitatii lui pararescrierea nu se poate face ntr-un subtermen de forma (x) unde x este o variabila,

asa ca presupunem ca ea se face n (a) = (l) unde a este un subtermen n G care nu este variabila. Prin urmare:

G = G {C[a]} si Q = (G) (H) {z(C)[(r)]}

unde z este o variabila noua, C este un context extins din T(X {z}) si (a) = (l).

7.3. LEMA DE RIDICARE 21

Fie = CGU(a, l) : X Y V si : V Z unica substitutie cu proprietatea =< , > . Deoarecerestrictia a lui < , > la X este normala conform ipotezei, si < , >(a) =< , >(l), aplicand propozitia 7.3.2rezulta normalitatea lui .

Notand cu : T(X) T(V ) restrictia lui la T(X) deducem ca = .

Rezulta ca

G n (G H {C[r]}) cu morfismul calculat .

Notand R = (G H {C[r]}) mai observam ca:

(R) = (; )(G H {C[r]}) =< , > (G H {C[r]}) = (G) (H) {z(C)[(r)]} = Q. 2

G

R

G

n

n

?

?

V

V

X

?

?

-

-

-

Z

Z

Z

1Z

1Z

?

?

S

Q = (R)

(G)

pr

pr

?

?

Propozitie 7.3.4 Pentru orice (Y )l.= r if H din presupunem ca orice variabila din Y apare n l. Fie G o

multime finita de egalitati din T(X).

Daca : T(X) T(Z) este normala si

(G)pr S,

atunci

Gn G

cu morfismul calculat

pentru care exista o substitutie normala cu proprietatile (G) = S si = .

Demonstratie: Prin inductie dupa numarul pasilor. Vom pune n evidenta prima pararescriere

(G) pr Qpr S.

Conform propozitiei precedente = cu normala, exista R cu (R) = Q si

G n R cu morfismul calculat .

Folosind ipoteza de inductie din (R)pr S deducem

Rn G

cu morfismul calculat

pentru care exista o substitutie normala cu proprietatile (G) = S si = . Din cele de mai sus rezulta ca

Gn G

cu morfismul calculat

si () = = . 2

22 CHAPTER 7. COMPLETITUDINEA NARROWINGULUI

7.4 Epilog

Propozitie 7.4.1 Fie G T(X) T(X) finita si morfismul h : T(X) T(Y ) cu h(G) = . Atunci Gr

cu substitutia calculata s pentru care exista morfismul f cu proprietatea s; f = h.

Demonstratie: Reamintim definitia reflexiei:Daca : A B este cel mai general unificator pentru l si r, atunci G {l =t r} r (G) cu mofismul

calculat .Vom demonstra prin inductie dupa numarul elementelor multimii G.Fie G = G {l =s r}. Din ipoteza h(l) = h(r). Fie u : T(X) T(Z) cel mai general unificator pentru l si r.

Atunci exista un unic v : T(Z) T(Y ) astfel ncat u; v = h.Observam conform definitiei de mai sus ca G r u(G) cu morfismul calculat u.

Cum v(u(G)) = h(G)ip= , aplicand ipoteza de inductie pentru u(G) deducem ca u(G)

r cu substitutia

calculata w pentru care exista f astfel ncat w; f = v.Atunci G

r cu substitutia calculata u;w. In plus h = u; v = (u;w); f . 2

7.5 Completitudine

Ipoteze. Pentru orice (Y )l.= r if H din presupunem ca orice variabila din Y apare n l. Rescrierea are

proprietatea formei normale unice (FN!).Reamintim ca proprietatea FN! implica confluenta rescrierii si completitudinea relatiei de ntalnire prin rescriere.Fie s : X Z o solutie pentru (X)G. Cu ipoteza FN! pentru solutia s se poate normaliza obtinand solutia

normala s : X Z definita prin s(x) = fn(s(x)) pentru orice x X. Observam ca s(x) s(x) pentru orice

x X. Prin inductie structurala se arata usor ca s(r) s(r) pentru orice r T(X). Pentru orice u =t v G

observam cas(u)

s

(u) si s(v) s

(v).

Probam ca s este solutie pentru (X)G adica |= (Z)s(G). Fie u.=t v G. Deoarece s este solutie pentru (X)G

deducem |= (Z)s(u).=t s(v), deci s(u) s(v). Dar s(u) s(u) si s(v) s(v) deci s(u) s(v) adica

|= (Z)s(u) =t s(v) (am folosit si tranzitiva). Rezulta ca |= (Z)s(G), deci s este solutie.

Propozitie 7.5.1 Orice solutie normala se obtine prin particularizarea unei solutii obtinute cu narrowing si reflexie.

Demonstratie: Fie s : T(X) T(Z) o solutie normala. Utilizand completitudinea relatiei de ntalnire prin

rescriere din |= (Z)s(G) rezulta ca s(G) , prin urmare conform prologului s(G)pr . Din lema de

ridicare rezulta existenta substitutiei cu

Gn G

cu morfismul calculat

si a substitutiei normale cu proprietatile (G) = si s = .Deoarece G este o multime de egalitati unificabile prin , deducem conform epilogului

G r cu morfismul calculat

si exista o substitutie cu proprietatea = . Deoarece s = deducem ca orice solutie normala s poate fiobtinuta prin particularizarea unei solutii gasite cu narrowing si reflexie.

Chapter 8

REZOLUTIE A` LA PROLOG

Programarea logica relationala, ilustrata n viata de toate zilele de limbajul Prolog, este bazata pe rezolutie.

8.1 Rezolutia

Axiomele, clauze Horn, au forma (Y )(v) if H unde1) (v) este un atom, adica este un predicat si v este un vector de termeni n concordanta cu aritatea lui iar2) H este o multime de atomi.

Telul este o multime de atomi. Punand n evidenta atomul asupra caruia va actiona rezolutia pentru o axiomaca mai sus telul devine {(s)} T. Ca mai sus presupunem ca variabilele din Y sunt disjuncte de variabilele din tel.

Fie = CGU(v, s). Prin rezolutie, cu substitutia calculata ajungem la telul (H T ).

8.2 Rezolutie = Narrowing = Paramodulatie

Trecerea de la varianta relationala la varianta ecuationala se face prin1) adaugarea la signatura a sortului b, transformarea predicatelor n simboluri de operatii avand rezultatul de sort b2) nlocuirea fiecarui atom (v) cu egalitatea (v)

.=b t unde t este o constanta de sort b reprezentand adevarul.

Varianta ecuationala a unei multimi de atomi C va fi notata cu Ce = {(v).=b t : (v) C}.

Propozitie 8.2.1 In varianta ecuationala, rezolutia se poate realiza prin narrowing si eliminarea egalitatilor reale.

Demonstratie: Fie G o multime de atomi si (Y )(v) if H o clauza Horn. Consideram G = G {(s)} si = CGU(v, s). Prin rezolutie obtinem (G H).

In varianta ecuationala Ge = Ge {(s).=b t} si (Y )(v)

.=b t if H

e.Alegem a = (s), l = (v) si observam ca = CGU(s, v) = CGU((s), (v)).Cum a nu este variabila rezulta ca putem aplica narrowing-ul:

Ge {(s).=b t} n (Ge He {t

.=b t}) =

((G H)e {t.=b t}) =

[(G H)]e {t.=b t}

In urma eliminarii egalitatii adevarate t.=b t obtinem varianta ecuationala a rezultatului rezolutiei, (G

H).

Corolar 8.2.1 Fie G o multime de atomi. Orice solutie pentru (X)G obtinuta cu rezolutia poate fi obtinuta prinnarrowing si eliminarea egalitatilor adevarate ca solutie pentru (X)Ge

Propozitie 8.2.2 Fie o multime de clauze Horn si G o multime de atomi. Aplicarea narrowing-ului folosind e

n varianta ecuationala Ge se poate realiza prin rezolutie folosind n G.

Demonstratie: Fie G = G {P (s)} si (Y )(v).=b t if H

e o clauza astfel ncat sa se poata aplica narrowing-ullui P (s)

.=b t. Atunci l = (v) si exista = CGU(l, a), unde a trebuie ales.

23

24 CHAPTER 8. REZOLUTIE A LA PROLOG

Singura varianta posibila pentru a este a = P (s). Observam ca a nu este variabila.Cum exista = CGU(a, l) rezulta ca P = si = CGU(v, s). Prin urmare

Ge n (Ge {t

.=b t} H

e) = (G H)e {t.=b t}.

Aplicand rezolutia obtinemG {P (s)} (G H) cu morfismul calculat

In concluzie din Ge n G1 cu e si morfismul calculat , deducem ca G se duce prin rezolutie cu si morfismulcalculat n F cu G1 = F

e {t.=b t}. 2

Corolar 8.2.2 Fie G o multime de atomi. Orice solutie pentru (X)Ge obtinuta prin narrowing si eliminareaegalitatilor adevarate poate fi obtinuta cu rezolutia ca solutie pentru (X)G.

Mai observam ca n varianta ecuationala a unui program Prolog reflexia nu poate fi aplicata deoarece unificareanu poate fi facuta n egalitatea (v) = t.

Concluzia este ca rezolutia este completa, fapt ce rezulta din teoremele de completitudine demonstrate anterior.

8.3. EXERCITIUL 1 25

8.3 Exercitiul 1

Se pastreaza notatiile din capitolele precedente. Se da urmatorul fragment de program EQLOG:

sort nat < nlist < list

op 0 : -> nat

op s : nat -> nat

op nil : -> list

op _ _ : list list -> list [assoc]

op cap : nlist -> nat

op cdr : nlist -> list

var E : nat

var L : list

eq cap(E L) = E ***> 1

eq cdr(E L) = L ***> 2

op # : list -> nat

eq #(nil) = 0 ***> 3

eq #(E L) = s(#(L)) ***> 4

Se cere sa se gaseasca solutie pentru urmatoarea interogare:

L{#(L) = s(s(0)), cap(L) = 0}

Rezolvare. Avem 3 variante:

sa unificam membrul stang din ecuatia 1 cu cap(L);

sa unificam membrul stang din ecuatia 3 cu #(L);

sa unificam membrul stang din ecuatia 4 cu #(L).

Vom alege ultima alternativa. Deoarece ecuatia 4 are variabile care apar n scop, redenumim variabilele si obtinem:#(E L1) = s(#(L1)).

Identificam cadrul de aplicare a paramodulatiei:

contextul c este z = s(s(0));

cel mai general unificator pentru #(L) si #(E L1) este L := EL1;

ecuatia care se utilizeaza nu este conditionata deci H este vid.

Noul scop este {cap(E L1) = 0, s(#(L1)) = s(s(0))}.Subtermenul unde se aplica paramodulatia este #(L1), iar ecuatia folosita este 4. Din nou vom face o redenumire

a variabilelor, ecuatia 4 devine #(E1 L2) = s(#L2) .

Dupa noul pas de paramodulatie, scopul devine: {cap(E E1 L2) = 0, s(s(#(L2))) = s(s(0))}. Se observa ca esteposibil sa facem din nou paramodulatie cu ecuatia 4 si putem intra astfel n ciclu infinit.

Vom unifica cap(E E1 L2) cu membrul stang al ecuatiei 1, n care redenumim variabilele; cel mai general unificatorcalculat este E2 := E,L1 := E1 L2. Contextul este z = 0.

Scopul devine {E = 0, s(s(#(L2))) = s(s(0))}.Unificam #(L2) cu membrul stang al ecuatiei 3; contextul este z = 0, cel mai general unificator, L2 := nil.

Noul scop este {E = 0, s(s(0)) = s(s(0))} .Prin aplicarea reflexiei, scopul devine si se adauga la solutie E := 0.Solutia L = 0 E1 nil se obtine astfel :

L = E L1

= E E1 L2

= E E1 nil

= 0 E1 nil

26 CHAPTER 8. REZOLUTIE A LA PROLOG

8.4 Exercitiul 2

Se da urmatorul fragment de program:

0 1

s x