Programare Logica Interpretari Si Modele

=== l ===

CAPITOLUL 1

INTRODUCERE

Programarea logică s-a dezvoltat la începutul anilor 1970 pentru a extinde lucrările referitoare la demonstrarea automată a teoremelor și la inteligența artificială.

Meritul introducerii programării logice rămâne în deosebi lui Kowalski și Colmerauer, chiar dacă trebuie de asemenea menționați Greén și Hoyes în această privință. În 1972 Kowalski și Colmerauer au ajuns la ideea fundamentală că logica poate fi utilizată ca un limbaj de programare. Sigla PROLOG (Programare în logică) a fost inventată și primul interpretor PROLOG a fost implementat în limbajul ALGOL-W de Roussel la Marsilia în anul 1972.

Ideea că logica de ordinul I, sau cel puțin anumite subansamble ale sale, puteau fi utilizate ca un limbaj de programare, a fost revoluționară. Una din ideile principale ale programării logice, dată de Kowalski, este că un algoritm este constituit din două componente disjuncte: logica și controlul. Logica formulează problema de rezolvat iar controlul formulează modul de rezolvare. Cu toate că sunt separate, aceste două componente aduc un anumit număr de avantaje, posibilitatea programatorului de a nu specifica decât componenta logică și de a lăsa controlul în întregime sistemului de programare logică nefiind singurul.

Limbajele de programare logică actuale se împarte în două mari categorii atât de diferite: limbaje „sistem” și limbaje „aplicații” (acești termeni nu sunt utilizați pentru precizare ci pentru a sesiza semnificația celor două categorii de limbaje).

În esență pentru limbajele „sistem” accentul este pus pe paralelismul și fără a se ține cont de nedeterminism și de programele definite (adică fără negație). Aceste limbaje sunt în deosebi utilizate pentru aplicațiile sistemului operaționale și ale programării orientate obiect. Pentru aceste limbaje controlul este încă mult efectuat de programator.

Pentru limbajele „aplicație” accentul este pus pe paralelismul sau ignorând nedeterminismul și programele fără restricții. Limbajele din această categorie includ: Quintus – PROLOG, micro – PROLOG și NU – PROLOG. Pentru aceste limbaje automatismul componentei de control pentru anumite aplicații a fost în mare parte obținut. Limbajele „aplicației” se adaptează mai bine sistemelor de baze de date deductive și sistemelor expert.

Teoria de ordinul I

Logica de ordinul I are două aspecte: sintaxa și semantica. Aspectul sintactic privește formulele bine formate admise de gramatica unui limbaj formal precum și problemele cele mai profunde de teoriei de demonstrării. Aspectul semantic se referă la semnificația dată formulelor bine formate și simbolurilor pe care acestea le conțin.

O teorie de ordinul I constă într-un alfabet, un limbaj de ordinul I, o mulțime de axiome și o mulțime de reguli de inferență. Limbajul de ordinul I este constituit din formule bine formate ale teoriei. Axiomele reprezintă un subansamblu desemnat de formule bine formate. Axiomele și regulile de inferență sunt utilizate pentru a deduce teoremele teoriei.

Un alfabet este construit din următoarele categorii de simboluri: variabile, constante, simboluri de funcție, simboluri de predicate, conectori, cuantificatori și simboluri de punctuație. Pentru orice alfabet numai categoriile: constante și simboluri de funcție pot fi vide. Conectorii vor fi: „~”, „”, „”, „”, „”; cuantificatorii sunt: „” și „”, iar simbolurile de punctuație: „(”, „)”, „ , ”. Ordinea de prioritate a acestora este:

Un termen poate fi definit recursiv astfel:

orice variabilă este un termen;

o constantă este un termen;

dacă f este un simbol de funcție de aritate n și t1, …, tn sunt termeni, atunci f(t1, …, tn) este un termen.

O formulă poate fi definită recursiv astfel:

dacă p este un simbol de predicat de aritate n și t1, …, tn sunt termeni, atunci p(t1, …, tn) este o formulă numită formula atomică sau atom;

dacă F și G sunt formule, atunci ~F, FG, FG, FG, FG sunt formule;

dacă F este o formulă și x o variabilă, atunci xF și xF este o formulă.

Un limbaj de ordinul I dat de un alfabet este un ansamblu de formule construite plecând de la simbolurile alfabetului. Semnificația conectorilor este următoarea: ~ este negația, conjuncția, disjuncția, implicația, echivalența, cuantificatorul existențial, iar cuantificatorul universal.

Domeniul de aplicare al lui x (respectiv x) în formula xF (reaspectiv xF) este F. o ocurență legată de o variabilă într-o formulă este o ocurență urmând unui cuantificator (imediat) sau o ocurență în domeniul de aplicare al unui cuantificator, a variabilei ce urmează imediat cuantificatorului. Toate celelalte ocurențe ale unei variabile sunt libere.

De exemplu în formulele xr(x)q(x) prima ocurență a lui x este legată în timp ce a doua este liberă deoarece domeniul de aplicare al lui x este r(x). Nu același lucru putem spune despre x(r(x)q(x)).

În formula x(r(x)q(x)) toate ocurențele lui x sunt legate deoarece domeniul de aplicare al lui x este r(x) și q(x).

O formulă închisă este o formulă falsă ocurenței libere.

Un literal se definește ca fiind un atom sau negația unui atom. Un literal pozitiv este un atom. Un literal negativ este negația unui atom.

O clauză este o formulă de forma:

x1…xn(L1…Lm)

unde fiecare Li, i{1,2,..,m} este un literal și x1, …, xn sunt toate variabile care apar în L1, …, Lm.

O clauză mai poate fi notată și sub forma:

x1…xs(A1…An~B1…~Bm)

unde A1,…, An, B1, …, Bm sunt atomi iar x1, …, xs sunt toate variabilele ce apar în acești atomi.

Se face notația următoare pentru această clauză:

A1…AnB1, …, Bm

Deci, într-o clauză toate variabilele sunt presupuse a fi universal cuantificate.

O clauză definită de program este o clauză de forma:

AB1, …, Bn

unde A se numește capul clauzei, iar B1, …, Bnse numește corpul ei.

O clauză unitară sau fapt este o clauză de forma:

A

adică o clauză definită de program are corpul vid.

Un program definit este o mulțime finită de clauze definite de program. Într-un program definit mulțimea tuturor clauzelor de program având același simbol de predicat „p” în capul lor se numește definiția lui „p”.

Un corp se definește ca fiind o clauză de forma:

B1, …, Bn

adică o clauză care are o consecință (un cap) vidă.

Observăm că dacă y1, …, yr sunt variabilele scopului B1, …, Bn această notație este înțeleasă ca:

y1…yr(~B1…~Bn) adică

~y1…yr(B1…Bn).

Cauza vidă, notată , este clauza care are o consecință și un corp (sau antecedent) vide și este înțeleasă ca o contradicție.

O clauză Horn este o clauză care este fie o clauză definită de program fie un scop.

Interpretări și modele

Pentru a fi capabili să precizăm dacă o formulă este adevărată sau falsă este necesar să dăm o semnificație fiecărui simbol al formulei. Dacă cuantificatorii și conectorii au o semnificație fixată, semnificațiile constantelor, variabilelor, simbolurilor de funcție și de predicate pot să varieze. O interpretare specifică un anumit domeniu de studiu (domeniu în care se află variabilele) precum și semnificația fiecărui simbol al formulei. Ne interesăm în special de interpretările pentru care formulele traduc o expresie adevărată în această interpretare.

O pre-interpretare a unui limbaj de ordinul I, L se definește ca fiind constituită din următoarele elemente:

o mulțime nedivă D numită domeniu al interpretării;

asignarea unui element din D fiecărei constante din L;

pentru fiecare simbol de funcție de aritate n din L, asignarea unei aplicații: DnD

o interpretare I a unui limbaj de ordinul I, L constă dintr-o pre-interpretare J a lui L din domeniul D, precum și din următoarele elemente: pentru fiecare simbol de predicat de aritate n al lui L asiganarea unei aplicații definită pe Dn cu valori în mulțimea {true, false}.

Fie J o pre-interpretare a unui limbaj de ordinul I, L. o asignare de variabile (relativ la J) este atribuirea fiecărei variabile din L a unui element din domeniul lui J. Dacă V este o asignare de variabile, atunci asignarea unui termen (relativ la J și V) din L se poate defini astfel:

asignarea unei variabile este asignarea sa după V;

asignarea unei constante este asignarea sa după J;

dacă t1`, …, tn` sunt asignările termenilor t1, …, tn și f ` este asignarea simbolului de aritate nf, atunci elementul f `(t1`, …, tn`) din D este asignarea termenului f(t1, …, tn).

Fie J o pre-interpretare a unui limbaj de ordinul I L, V o asignare de variabile relativ la J și A un atom. Presupunând că A este de forma p(t1, …, tn) și t1`, …, tn` sunt asignările termenilor t1, …, tn relativ la J și V, numim AJ,V=p(t1`, …, tn`) J – instanța lui A relativ la V. Mulțimea AJ = {AJ,V | V = o asignare de variabile relativă la J} se numește o J – instanță a lui A.

Fie J o interpretare de domeniu D a unui limbaj de ordinul I L și fie V o asignare de variabile. Putem să dăm atunci unei formule din L o valoare de adevăr {adevărat, false} relativ la I și V astfel:

dacă formula este un atom p(t1, …, tn) atunci valoarea de adevăr a sa este obținută calculând valoarea lui p`(t1`, …, tn`) unde p` este aplicația asociată lui p de interpretarea I și t1`, …, tn` sunt asignările termenilor t1, …, tn relativ la I și V.

dacă formula este de forma F, FG, FG, FG sau FG atunci valoarea sa de adevăr este dată de tabelul:

dacă formula este de forma xF atunci valoarea sa de adevăr este True (adevărat) dacă există dD astfel încât F are valoarea de adevăr True (adevărat) relativ la I și V(x/d), unde V(x/d) este asignarea de variabile V de restricția: x ia valoarea d; astfel valoarea de adevăr a formulei xF este Flase.

Dacă formula este de forma xF atunci valoarea sa de adevăr este True dacă pentru toți dD F are valoarea de adevăr True relativ la I și V(x/d), astfel valoarea sa de adevăr este Flase.

Se observă că valoarea de adevăr a unei formule închise nu depinde de asignarea de variabile. În consecință putem vorbi fără ambiguitate de valoarea de adevăr a unei formule închise relativ la o anumită interpretare. Dacă valoarea de adevăr a sa relativ la o interpretare este True spunem că formula este adevărată relativ la interpretare.

Fie I o interpretare pentru un limbaj de ordinul I L și w o formulă în L. Spunem că w este satisfiabilă în I dacă (w) este adevărată relativ la I și că w este validă în I dacă (w) este adevărată relativ la I.

Fie I o interpretare a unui limbaj de ordinul I L și F o formulă. Spunem că I este un model al lui F dacă F este adevărată relativ la I.

Fir T o teorie de ordinul I și L limbaj al lui T. Un model al lui T este o interpretare pentru L, interpretare care constituie un model pentru fiecare axiomă a teoriei T. Dacă T are un model spunem că T este consistentă.

Conceptul de model al unei formule închise poate să se generalizeze ușor la cel de model al unei mulțimi de formule închise astfel: fie S o mulțime de formule închise ale unui limbaj de ordinul I și I o interpretare a lui L. Spunem că I este un model al lui S dacă I este un model pentru fiecare formulă din S.

De asemenea putem extinde conceptul de satisfiabilitate și validitate la o mulțime de formule S astfel: spunem că S este satisfiabilă dacă L (limbajul de ordinul I din care fac parte elementele lui S) are o interpretare care este model pentru S și că S este validă dacă toate interpretările lui L sunt modele pentru S.

Considerând S o mulțime de formule închise și F o formulă închisă a unui limbaj de ordinul I L, spunem că F este o consecință logică a lui S dacă pentru toate interpretările I ale lui L, I este un model pentru S implică faptul că I este un model al lui F.

Se poate demonstra ușor, folosind notațiile de mai sus, următoarea teoremă: F este consecință logică a lui S dacă și numai dacă S{~F} este insatisfiabilă. O variantă de demonstrație este următoarea :

Presupunem că F este o consecință logică a lui S. Fie I o interpretare a lui L. Presupunând că I este un model pentru S, din ipoteză F = consecință logică a lui S, deducem faptul că I este un model pentru F. Deci I nu este model pentru ~F (și nici pentru S{~F}). Deoarece I a fost ales arbitrar S{~F} este insatisfiabilă.

Presupunem că S{~F} este insatisfiabilă. Demonstrăm că F este o consecință logică a lui S. Fie I o interpretare oarecare a lui L cu proprietatea că I este model pentru S. Deoarece S{~F} este insatisfiabilă (nu poate avea nici un model) rezultă faptul că I nu poate fi model al lui ~F. Deci I este un model al lui F și în concluzie F este consecință logică a lui S.

cctd

În practică această afirmație ne spune că dacă b este un scop de forma B1, …, Bn cu variabilele y1, …, yr pentru un program F și se cere sistemului de a demonstra faptul că mulțimea de clauze P{b} este insatisfiabilă, această cerință este echivalentă cu demonstrarea că y1…yr(B1…Bn) este o consecință logică a lui P.

Definesc ca fiind un termen închis un termen fără variabile și analog un atom închis ca fiind un atom fără variabile.

Fie L un limbaj de ordinul I. Universul Herbrand (notat UL) al lui L este mulțimea tuturor termenilor închiși pe care îi putem forma cu constantele și simbolurile care apar în L.

Exemplu: Fie programul p(x) q(f(x),g(x))

UL={a, f(a), g(a), f(f(a)), g(f(a)), f(g(a)), g(g(a)),…}

Baza Herbrand (notată BL) a limbajului L se definește ca fiind mulțimea tuturor atomilor închiși care pot fi formați utilizând simbolurile de predicate din L cu termeni închiși ai universului Herbrand ca argumente. Pentru exemplul anterior: BL={p(a), q(a,a), p(f(a)), p(g(a)),…}.

Dacă L este un limbaj de ordinul I, o pre-interpretare Hrebrand a lui L este pre-interpretarea lui L dată de următoarele elemente:

domeniul pre-interpretării este UL

constantele limbajului sunt interpretate prin ele însele în UL

dacă f este un simbol de funcție de aritate n în L, atunci aplicația pe (UL)n în UL definită prin: (t1,…,tn)f(t1,…,tn) este asignarea lui f.

O interpretare Herbrand a lui L este o interpretare oarecare bazată pe o pre-interpretare Herbrand a lui L.

Pentru toată interpretarea Herbrand subansamblu corespunzător bazei Herbrand este mulțimea tuturor atomilor închiși care sunt adevărați în această interpretare. Reciproc, fiind dat un subansamblu arbitrar al bazei Herbrand, există o interpretare Herbrand corespunzătoare, definită prin specificarea faptului că aplicația asociată unui simbol de predicat asociază valoarea True argumentelor sale când atomul format din simbolurile de predicat și de aceleași argumente este dat în subansamblul respectiv.

Un model Herbrand al unei mulțimi de formule închise S este o interpretare Herbrand care este modelul pentru S.

Este deseori comod să facem referire – prin abuz de limbaj – la o interpretare a unei mulțimi S de formule mai degrabă decât la un limbaj de ordinul I, limbaj din care provin formulele. Este natural ca în acest caz limbajul de ordinul I să fie definit de constantele, simbolurile de funcție și predicate ce apar în S. Putem acum vorbi de universul Herbran US și de Baza Herbrand BS ale lui S. În particular, mulțimea formulelor va fi adesea un program , putând astfel face referire la universul Herbrand U și la Baza Herbrand B a lui .

Este ușor de observat că dacă S este o mulțime de clase și dacă S are un model atunci S are un model Herbrand; și de aici faptul că S este insatisfiabilă dacă și numai dacă S nu are modele Herbrand.

Există diverse „forme normale” ale formelor, una dintre acestea fiind forma normală conjuctivă prenex. Spun că o formulă este în forma normală conjuctivă prenex dacă ea este forma: Qx1…Qxk((L11…L1m1)… (Ln1…Lnmn)) unde fiecare Q este un cuantificator existențial sau universal și fiecare Lij este un literal.

Pentru fiecare formulă există o formulă logică echivalentă cu ea în forma normală conjuctivă prenex.

Unificarea

Unul din scopurile principale ale unui sistem de programare logică este de a calcula legăturile. Aceste legături sunt determinate prin intermediul unificării.

O substituție este o mulțime finită de forma {V1/t1,…, Vn/tn} unde fiecare Vi este o variabilă, fiecare ti este un termen distinct de Vi și variabilele V1,…, Vn sunt distincte. Dacă toți termenii ti, i{1,2,.., n} sunt închiși atunci poartă numele de substituție închisă. Dacă ti,i{1,2,.., n} sunt variabile atunci se numește substituție de variabilă pură.

Fie ={ V1/t1,…, Vn/tn } o substituție și E o expresie (un termen, un literal, o conjuncție sau o disjuncție de literale). Prin E (instanța lui E prin ) înțelegem expresia obținută plecând de la E și înlocuind simultan fiecare ocurent al variabilei Vi in E printr-un termen ti corespunzător substituției, i{1,2,.., n}.

Dacă ={u1/s1,…,um/sm} și ={ V1/t1,…, Vn/tn } sunt două substituții, spunem că este componenta substituțiilor n și se definește ca fiind substituția obținută plecând de la mulțimea {u1/s1,…,um/sm , V1/t1,…, Vn/tn} înlăturând toată legătura ui/si pentru care ui=si și toată legătura Vj/tj pentru care Vj={u1,…,um}.

Substituția dată de mulțimea vidă este numită substituția identică și se notează cu .

Exemplu : E=p(x.y,f(a)), ={x/b,y/x} atunci E=p(b,x,f(a)). Dacă ={x/f(y),y/z}, și ={x/a,y/b,z/y} ={x/f(b),z/y}.

Fie E și F două expresii. Spunem că E și F sunt variante (sau E este o variantă a lui F sau Feste o variabtă a lui E) dacă există două substitiții și astfel încât E=F și F=E.

De exemplu : p(f(x,z),g(z),a) este o variantă a lui p(f(y,x),g(u),a).

Fie E o expresie și V o mulțime de variabile ce apar în E. O substituție de tip redenumire pentru E este o substituție de variabile pură {x1/y1,…,xn/yn} pentru care sunt îndeplinite condițiile : {x1,…,xn}V, yi sunt distincte i{1,2,.., n} și (V-{x1,…,xn}){y1,…,yn}=.

Dacă E și F sunt variante, atunci există substituțiile de redenumire pentru F respectiv E, și astfel încât E=F și F=E.

Fie S o mulțime finită de expresii simple. O substituție se numește unificator al lui S dacă S este un singleton (mulțime care are un singur element).

Un unificator al lui S se numește un cel mai general unificator al lui S (și îl notâm Upg) dacă pentru fiecare unificator al lui S există o substituție astfel încât =.

Fie S o mulțime finită de expresii simple (mulțime de termeni și/sau de atomi). Mulțimea diferențelor lui S se definește astfel: găsim poziția simbolului aflat cel mai la stânga care nu apare în toate expresiile lui S și extragem din fiecare expresie a lui S subexpresia ce începe de la poziția acestui simbol. Mulțimea tuturor acestor subexpresii este mulțimea diferențelor.

Exemplu: S={p(f(x), h(y), a), p(f(x), z, a), p(f(x), h(y), b)}

Muțimea diferențelor este {h(y), z}.

Algorimtul de unificare

Are următorii pași:

P1 : r=0, 0=

P2 : Dacă Sk este un singleton atunci k este un upg al lui S. STOP

Dacă Sk nu este un singleton atunci găsim mulțimea diferențelor Dk a lui Sk.

P3 : Dacă există V și t în Dk astfel încât V să fie o variabilă ce nu apare în t atunci k+1=k{V/t} și incrementăm pe k cu o unitate, mergând apoi la pasul P2.

Dacă S nu este unificabilă. STOP

Observăm că algoritmul prezent este nedeterminist, în sensul că putem face mai multe alegeri pentru v și t la pasul P3. Cu toate acestea, aplicarea a doi „upd” produși de algoritm conduce la expresii care diferă doar prin numele variabilelor. Este evident că algoritmul este finit deoarece S conține un număr finit de variabile și fiecare aplicare a pasului P3 elimină o variabilă.

PUNCTE FIXE

Tuturor programelor definite li se asociază o aplicație monotonă care joacă un rol foarte important în teorie.

Dacă S este o mulțime, o relație R pe S este o submulțime a produsului cartezian SS. Se utilizează în general notația xRy pentru (x,y)R.

O relație R pe mulțimea S este o relație de ordine parțială dacă sunt îndeplinite condițiile:

xRy, xS

xRy și yRx implică x=y, , x, yS

xRy și yRz implica xRz, , x, y,zS

De exemplu pentru o mulțime S fie 2S mulțimea părților sale. Atunci incluziunea mulțimilor: „” este o relație de ordine parțială pe 2S.

Se adoptă notația standard „” pentru o relație de ordine parțială pe 2S.

Fie S o mulțime și o relație de ordine parțială pe ea: . Atunci aS este un majorant al unei submulțimi X a lui S dacă ya pentru yX. Analog bS este un minorant al lui X dacă by pentru yX.

Fie S o mulțime și o relație de ordine parțială pe ea. Atunci aS este marginea superioară a unei submulțimi X a lui S (notată sup(X)) dacă a este un majorant al lui X și pentru toți majoranții a` ai lui X, avem aa`. Analog, bS este marginea inferioară a unei submulțimi X a lui S (notată inf(X)) dacă b este un minorant al lui X și pentru toți majoranții b` ai lui X, avem b`b.

O mulțime parțial ordonată L este o latice completă dacă sup(X) și inf(X) există, pentru toate submulțimile X ale lui L.

Notăm cu T cel mai mare element sup(L) și cu cel mai mic element inf(L) al laticii complete L.

În exemplul precedent, 2S este o latice completă.

Marginea superioară a unei familii de submulțimi ale lui S este reuniunea lor iar marginea inferioară a lor este intersecția. Cel mai mare element este S iar cel mai mic element este .

Definiție: Fie L o latice completă și T : L L o aplicație. Spunem că T este monoton dacă T(x)T(y) pentru xy.

Definiție: Fie L o latice completă și X o submulțime a sa. Spunem că X este (dirige`) dacă toate submulțimile finite ale lui X au o margine superioară în X.

Definiție: Fie L o latice completă și T : L L o aplicație. Spunem că T este continuu dacă T(sup(X)) = sup(T(X)) pentru toate subansamblele (dirige`) X ale lui L.

Interesul acestor definiții vine din faptul că pentru un program definit P, familia interpretărilor Herbrand formează o latice completă și deasemenea din acela că există o aplicație continuă asociată lui P. Să studiem acum punctele fixe ale aplicațiilor definite pe latice.

Definiție: Fie L o latice completă și T : L L o aplicație. Spunem că aL este cel mai mic punct fix al lui T dacă a este un punct fix (adică T(a)=a) și pentru toate punctele fixe b ale lui T, avem ab. Analog putem defini cel mai mare punct fix al lui T.

Teoremă: Fie L o latice completă și T : L L o aplicație monotonă. Atunci T are un cel mai mic punct fix (lfp(T)) și un cel mai mare punct fix (hlp(T)). În plus lfp(T) = inf{x / T(x)=x} = inf{x / T(x)x} și lfp(T) = sup{x / T(x)=x} = sup{x / T(x)x}.

Demonstrație: Fie G={ x / T(x)x } și g=inf(G). vom arăta că gG. deoarece gx pentru orice xG, prin monotonia lui T avem că T(g)T(x) pentru toți xG. deci T(g)<x pentru orice xG și prin urmare T(g)g prin definiția marginii inferioare. Deci gG.

Arătăm acum că g este un punct fix al lui T. Aceasta revine la a arăta că gT(g).

T(g)g implică T(T(g))T(g), implică T(g)G. Deci gT(g), în același fel în care g este punct fix al lui T.

Fie g`=inf{ x / T(x)=x }. Cum g este punct fix, avem g`g. Pe de altă parte { x / T(x)=x } { x / T(x)x } și avem deci gg`. Deci g=g`. Ceea ce trebuia demonstrat pentru cel mai mic punct fix: lfp(T), a fost demonstrat. Analog se realizează demonstrația pentru hlp(T).

Propoziție: Fie L o latice completă și T : L L o aplicație monotonă. Presupunând că aL și aT(a), atunci există un punct fix a` al lui T pentru care aa`. Analog, dacă bL și T(b)b, atunci există un punct fix b` al lui T pentru care b`b.

Demonstrație: în teorema precedentă este suficient de a considera a`=hlp(T) și b`=lfp(T).

În rezultatele ce le vom stabili în continuare, avem nevoie de conceptul de putere ordinală al lui T. Să amintim pentru început proprietățile elementare ale numerelor ordinale, pe care le vom numi simplu, ordinale. Intuitiv, ordinalele sunt numerele cu care de obicei lucrăm. Primul ordinal 0 este definit ca . În continuare definim: 1={}={0}, 2={, {}}={0, 1}, 3={, {}, {, {}}}={0,1,2} și așa mai departe. Există ordinale finite: întregii pozitivi. Primul ordinal infinit este ={0, 1, 2, …}, mulțimea întregilor pozitivi. S-a convenit să se noteze ordinalele finite prin litere romane: n, m, … și ordinalele arbitrare prin litere grecești: , , …

Se poate defini o relație de ordine “” pe mulțimea tuturor terminalelor astfel: dacă . De exemplu, n pentru toate ordinalele finite n. se scrie de obicei n în loc de n.

Dacă este un ordinal, succesorul lui este ordinalul +1={}, care este cel mai mic ordinal mai mare ca . De exemplu, 1=0+1, 2=1+1, 3=2+1 și așa mai departe.

Dacă este un ordinal succesor, fie =+1, notăm =-1. Un ordinal este numit ordinal limită dacă nu este succesorul nici unui ordinal. Cel mai mic ordinal limită (altul decât 0) este . După vine +1={}, +2=(+1)+1, +3, și așa mai departe. Ordinalul limită următor este 2 care este formată din toate ordinalele n și toate ordinalele +n, unde n. După acesta urmează 2+1, 2+2, … , 3, …

Principiul inducției transfinite se descrie astfel: fie P() o proprietate a ordinalelor. Presupunând că pentru un ordinal , dacă P() este adevărată pentru toți , atunci P() este adevărată, putem atunci să deducem că P() este adevărată pentru toate ordinalele .

Definiție: Fie L o latice completă și T : L L o aplicație monotonă. Atunci se definesc puterile ordinale ale lui T astfel:

T0 = 1

T = T(T(-1)) dacă este un ordinal succesor

T = sup{ T / } dacă este un ordinal limită și T0=T

T = T(T(-1)) dacă este un ordinal succesor

T = inf { T / } dacă este un ordinal limită

Propoziție: Fie L o latice completă și T : L L o aplicație monotonă. Atunci pentru toate ordinalele , T lfp(T) și T hfp(T). În plus există două ordinale 1 și 2 astfel încât 11 implică T1=lfp(T) și 22 implică T2=hfp(T).

Demonstrație: Demonstrația pentru lfp(T) decurge din punctele (a) și (e) prezentate mai jos. Demonstrațiile de la punctele (a), (b) și (c) folosesc inducția transfinită.

Demonstrăm că T lfp(T) pentru toți :

Dacă este un ordinal limită, atunci T = sup{ T / } lfp(T) prin ipoteza inducției transfinite. Dacă este un ordinal succesor atunci T=T(T(-1)) T(lfp(T))=lfp(T), prin ipoteza inducției, monotonia lui T și proprietatea punctului fix.

Demonstrăm că pentru toți , T T(+1):

Dacă este un ordinal succesor atunci T = T(T(-1)) T(T) = T(+1) prin ipoteza inducției și monotonia lui T. Dacă este un ordinal limită, atunci T = sup{ T / } sup{ T(+1) / } T(sup{T / })= T(+1), utilizând ipoteza inducției și monotonia lui T.

(c) Demonstrăm că pentru toți , , implică T T:

Dacă este un ordinal limită, atunci T = sup{ T / } = T. Dacă este un ordinal succesor, atunci (-1) și deci T T(-1) T, utilizând ipoteza inducției și (b).

Demonstrăm că pentru toți , , dacă și T = T atunci T = lfp(T):

Acum T T(+1) T, din (c). Deci T = T(T(+1)) = T(T) și deci T este un punct fix. În plus T = lfp(T) utilizând (a).

Demonstrăm că există astfel încât implică T = lfp(T):

Fie cel mai mic ordinal al cărui cardinal este mai mare decât al lui L. Presupunem că T lfp(T), pentru toți . Se definește h : L, prin h() = T. Atunci din (b) rezultă că h este injectivă, ceea ce contrazice alegerea lui . Astfel, T = lfp(T) pentru un și rezultatul decurge din (a) și (c).

Demonstrația pentru hfp(T) este analoagă.

Ctd.

Cel mai mic pentru care T = lfp(T) este numit ordinalul închideri lui T. Rezultatul următor arată că dacă presupunem în plus că T este continuu, ordinalul închideri lui T este .

Propoziție: Fie L o latice completă și T : L L o aplicație continuă. Atunci lfp(T) = T.

Demonstrație: Folosind propoziția (anterioară) este suficient să arătăm că T este un punct fix.

Avem că T(T) = T(sup{ Tn / n}) = sup{Tn / n} = T, utilizând continuitatea lui.

Ctd.

Analogia acestei propoziții pentru cel mai mare punct fix (hfp(T)) nu este adevărată, adică hfp(T) poate să nu fie egal cu T.

CAPITOLUL 2

PROGRAME DEFINITE

2.1 SEMANTICA DECLARATIVĂ

Acest paragraf se referă la cel mai mic model Herbrand al unui program definit. Acest model particular joacă un rol important în teorie. Vom arăta că cel mai mic model Herbrand este exact mulțimea atomilor închiși care constituie consecințe logice ale programului definit. Se va obține și o caracterizare importantă a celui mai mic model Herbrand ca punct fix. În final se va defini și conceptul de cheie (cle`) a unui răspuns corect.

Propoziție 2.1.1 (proprietatea intersecțieie modelelor):

Fie P un program definit și (Mi)iI o mulțime nevidă de modele Herbrand ale lui P. Atunci iIMi este un model Herbrand al lui P.

Demonstrație: iIMi este evident o interpretare Herbrand pentru P. Vom arăta că iIMi este un model al lui P.

P este un program definit. Fie AB1,…,Bn o regulă oarecare a lui P. Presupunem prin absurd că () o soluție cu proprietatea că {B1,…,Bn}iIMi și AiIMi {B1,…,Bn}Mi, iI AMi este model Herbrand al lui P. Deci AiIMi, presupunerea fiind falsă. În concluzie iIMi este un model Herbrand al lui P.

Cctd.

Deoarece toate programele definite P, admit BP (baza Herbrand) ca modele Herbrand, mulțimea tuturor modelelor Herbrand ale lui P este nevidă. Astfel intersecția tuturor modelelor Herbrand ale lui P este încă un model al lui P, numit cel mai mic model Herbrand. Îl vom nota MP.

Teorema următoare arată că atomii din MP sunt consecințele logice ale programului. Acest rezultat a fost stabilit de Van Endem și Kowalski.

Teorema 2.1.1: Fie P un program definit. Atunci:

MP = {ABP / A este o consecință logică a lui P}.

Demonstratie: Fie A o consecință logică a lui P. Folosind proprietățile prezentate anterior în capitolul 1, avem că P{A} este insatisfiabilă. Deci P{A} nu are modele Herbrand, ceea ce înseamnă că A este falsă în toate modelele Herbrand ale lui P. În concluzie A este adevărată în toate modelele Herbrand ale lui P, echivalent cu AMP.

Cctd.

Se dorește o caracterizare a celui mai mic model Herbrand al unui program utilizându-se conceptul de punct fix. Pentru acesta trebuie să asociem fiecărui program o latice completă.

Fie P un program definit. Atunci 2BP, care este mulțimea tuturor interpretărilor Herbrand ale lui P, este o latice completă împreună cu relația de ordine parțială a incluziunii mulțimilor: c. Cel mai mare element al acestei latice este BP și cel mai mic element, . Marginea superioară a unei mulțimi de interpretări Herbrand este reuniunea tuturor interpretărilor Herbrand din această mulțime. Marginea inferioară a acesteia o reprezintă intersecția lor.

Definiția 2.1.1: Fie P un program definit. Aplicația T : 2BP 2BP se definește astfel: Fie I o interpretare Herbrand. Atunci:

TP(I) = {ABP / AA1, … , An este o instanță fără variabile a unei clauze a lui P și {A1, … , An} I}

Evident operatorul TP este monoton. TP furnizează legătura între semantica declarativă și semantica procedurală a lui P.

Exemplu: Fie programul P:

p(f(x)) p(x);

q(a) p(x)

și interpretările: I1=BP, I2=TP(I1), I3=.

Atunci: TP(I1)={q(a)} {p(f(t)) / tUP}

TP(I2)={q(a)} {p(f(f(t))) / tUP}

TP(I3)=.

Propoziția 2.1.2: Fie P un program definit. Atunci aplicația TP este continuă.

Demonstrație: Fie X o partiție (dirige`e) a lui 2BP. Observăm că {A1, … , An} sup (X) dacă și numai dacă există IX astfel încâ {A1, … , An} I. Pentru a arăta că TP este continuu trebuie să arătăm că TP(sup(X)) = sup(TP(X)) pentru toate submulțimile (dirige`e) X.

Fie ATP(sup(X)).

AA1, … , An este o instanță fără variabile a unei clauze a lui P și {A1, … , An} sup(X).

AA1, … , An este o instanță fără variabile a unei clauze a lui P și {A1, … , An} I pentru un I X.

ATP(I) pentru IX.

Asup(TP(X))

cctd.

Interpretările Herbrand care sunt modele pot fi caracterizate prin aplicația TP.

Propoziția 2.1.3: Fie P un program definit și I o interpretare Herbrand a lui P. Atunci I este un model al lui P decă și numai dacă TP(I) I.

Demonstrație: I este un model al lui P dacă și numai dacă pentru fiecare instanță fără variabile AA1, … , An a fiecărei clauze a lui P, {A1, … , An} I implică AI, adică dacă și numai dacă TP(I) I.

Cctd.

Se ajunge acum la rezulzazul principal al teoriei. Următoarea teoremă, dată de Van Emden și Kowalski, furnizează o caracterizare în termeni de punct fix a celui mai mic model herbrand al unui program definit.

Teorema 2.1.2: Fie P un program definit. Atunci MP=lfp(TP)=TP.

Demonstrație: MP = inf{I / I este un model Herbrand al lui P}

= inf {I / TP(I) I}

= lfp(TP)

= TP

cctd.

Se poate demonstra însă că hfp(TP) TP.

Exemplu: Fie programul P:

p(f(x)) p(x);

q(a) p(x)

Atunci TP = {q(a)}, dar hfp(TP) = . De fapt hfp(TP) = TP(+1).

Definiție 2.1.2: Fie P un program definit și G un scop definit. Un răspuns pentru P{G} este o substituție pentru variabilele lui G.

Este evident că răspunsul nu conține obligatoriu o legătură pentru fiecare variabilă din G. În particular, dacă G nu are variabile, singurul răspuns posibil este substituția identică.

Definiția 2.1.3: Fie P un program definit, G scopul definit A1,…,Ak și un răspuns pentru P{G} dacă ()((A1…Ak)) este o consecință logică a lui P.

Se observă că, folosind rezultatele stabilite anterior, este un răspuns corect dacă și numai dacă P{ ((A1…Ak)) } este insatisfiabilă. Definiția prezentată mai sus a unui răspuns corect, redă bine semnificația intuitivă a acestui concept. Ea furnizează o descriere declarativă a ceea ce vrea a se obține plecând de la un program definit și de la un scop. Se va arăta în continuare echivalența între acest concept declarartiv și conceptul procedural corespondent, care este definit prin procedura de refutație definită de sistem.

În același mod cum returnează substituții un sistem de programare logică poate returna și răspunsul “nu”. Spunem că răspunsul “nu” este “corect” dacă P{G} este satisfiabilă.

Teorema 2.1.1 și definiția unui răspuns corect sugerează ideea de a generaliza această teoremă, adică un răspuns este corect dacă și numai dacă ((A1…Ak)) este adevărată în cel mai mic model Herbrand al programului. Acest rezultat însă nu este în general corect, după cum arată exemplul următor.

Exemplu: Fie programul P: p(a). Fie G scopul p(x) și substituția identică. Atunci MP={p(a)} și xp(x) este adevărată în MP. Totuși nu este un răspuns corect deoarece xp(x) nu este o consecință logică a lui P. Știim că xp(x) nu este o clauză și deci nu se poate stabili insatisfiabilitatea lui {p(a)}{ xp(x)}. Totuși dacă se face o restricție asupra substituției se poate obține un rezultat care generalizează teorema 2.1.

Teorema 2.1.3: Fie P un program definit și G un scop definit A1,…,Ak.Fie un răspuns pentru P{G} astfel încât (A1…Ak) este închisă. Atunci următoarele afirmații sunt echivalente:

este un răspuns corect

(A1…Ak) este adevărată în toate modelele Herbrand ale lui P

(A1…Ak) este adevărată în cel mai mic model Herbrand al lui P

Demonstrație: Este evident că demonstrația se reduce la a demonstra că c) implică a).

Dar: (A1…Ak) este adevărată în cel mai mic model herbrand al lui P

(A1…Ak) este adevărată în toate modelele Herbrand ale lui P

(A1…Ak) este falsă în toate modelele Herbrand ale lui p

P{(A1…Ak)} nu are modele Herbrand

P{(A1…Ak)} nu are modele.

Cctd.

2.2 CORECTITUDINEA REZOLUȚIEI SLD

În cele ce urmează se va introduce conceptul de semantică procedurală a programelor definite. Se vor defini răspunsurile calculate și se va stabili corectitudinea rezoluției SLD. Se vor evidenția de asemenea consecințele omiterii verificării ocurențelor în algoritmul de unificare.

Definiția 2.2.1: Fie G scopul A1,…,Am, … ,Ak și C clauza AB1, … ,Bq. Atunci G` derivă din G și C, utilizând un cel mai general unificator , dacă următoarele condiții sunt verificate:

Am este un atom, numit atom „ales”, în G

este un cel mai general unificator al lui Am și A

G` este scopul (A1, …, Am-1, B1, … , Bq, Am+1, … , Ak).

În terminologia rezoluției, G` se numește o rezolvantă a lui G și C.

Definiția 2.2.2: Fie P un program definit și G un scop definit. O derivare SLD a lui P{G} constă într-un șir (finit sau inifinit) G0=G, G1, … de scopuri, un șir C1, C2, … de variante de clauze ale programului P și un șir 1, 2, … de cei mai generali unificatori astfel încât Gi+1 derivă din Gi și Ci+1 utilizând I+1.

Fiecare Ci este o variantă adaptată a unei clauze corespunzătoare a programului astfel încât Ci nu are nici o variabilă care să fi apărut deja în derivația din Gi-1. Aceasta se poate obține de exemplu, indiciind variabilele din G cu 0 și variabilele Ci cu i. Acest procedeu de redenumire a variabilelor este cunoscut sub numele de standardizarea variabilelor separate. Procedeul este necesar deoarece, de exemplu, nu s-ar putea unifica p(x) și p(f(x)) în p(x) și p(f(x)). Fiecare variantă a clauzei din program C1, C2, … este numită clauză de intrare a derivației.

Definiția 2.2.3: O refutație SLD a lui P{G} este o derivație SLD finită a lui P{G} care are clauza vidă (notată ) ca ultim scop al derivării. Dacă Gn=, spunem că refutația are lungimea n.

Vom numi în cele ce urmează, pentru simplificare, o derivație SLD, simplu – derivare și o refutație SLD simplu – refutație.

Putem reprezenta o derivație SLD astfel:

G0=G C1, 1

G1 C2, 2

G2

.

.

.

Definiția 2.2.4: O refutație SLD fără restricții este o refutație SLD în care substituțiile i nu sunt neapărat cei mai generali unificatori ci sunt doar unificatori.

Derivațiile SLD pot fi finite sau infinite, reușite sau nereușite. O derivație SLD reușită este o derivație care se termină cu clauza vidă. Altfel spus o derivație reușită este o refutație. O derivație SLD care „nu reușește” este o derivație ce se încheie cu un scop nevid astfel încât atomul ales în acest scop nu se unifică cu capul nici unei clauze a programului.

Definiția 2.2.5: Fie P un program definit. „Mulțimea succeselor” programului P este mulțimea tuturor atomilor ABP pentru care P{A} are o refutație SLD.

Mulțimea succeselor reprezintă analogul procedural al celui mai mic model Herbrand. Într-un mod asemănător se definește corespondentul procedural al unui răspuns corect.

Definiția 2.2.6: Fie P un program definit și G un scop definit. Un răspuns calculat pentru P{G} este substituția obținută restrângând compunerea 1…n variabilelor lui G, unde 1, … , n este șirul celor mai generali unificatori utilizați într-o refutație SLD a lui P{G}.

Teorema 2.2.1 (corectitudinea rezoluției SLD):

Fie P un program definit și G un scop definit. Atunci toate răspunsurile calculate pentru P{G} sunt răspunsuri corecte pentru P{G}.

Demonstrație: Fie G scopul A1,…,Ak și 1, … , n șirul celor mai generali unificatori folosiți într-o refutație a lui P{G}. Trebuie să arătăm că ((A1…Ak) 1…n) este o consecință logică a lui P. Acest rezultat îl vom demonstra prin inducție după lungimea refutației.

Presupunem că lungimea refutației este n=1. Deci G este un scop de forma A1, programul are o clauză unitară de forma A și A1 = A1. Deoarece A11 este o instanță a unei clauze unitare a lui P, este evident că (A11) este o consecință logică a lui P.

Presupunem acum rezultatul adevărat pentru răspunsuri calculate printr-o refutație de lungime n-1. presupunem că 1, … , n reprezintă șirul celor mai generali unificatori utilizați într-o refutație a lui P{G} de lungime n.

Fie AB1,…,Bq (q0) prima clauză de intrare și Am atomul als în G. Prin ipoteza de inducție, ( A1 … Am-1) B1 … Bq Am+1 … Ak)1… n) este o consecință logică a lui P. Astfel, dacă q>0, ((B1 … Bq)1… n) este o consecință logică a lui P (Am1… n) care este asemenea lui (A1… n) este o consecință logică a lui P. Deci, ((A1 … Ak) 1… n) este o consecință logică a lui P.

Cctd.

Corolar 1: Fie P un program definit și G un scop definit. Presupunem că există o refutație SLD a lui P{G}. Atunci P{G} este insatisfiabilă.

Demonstrație: Fie G scopul A1,…,Ak. Conform teoremei 2.4 răspunsul calculat provenind din refutație este corect. Astfel, ((A1…Ak) ) este o consecință logică a lui P. Deci P{G} este insatisfiabilă.

Cctd.

Corolar 2: Mulțimea succeselor unui program definit este inclusă în cel mai mic model Herbrand al programului.

Demonstrație: Fie P un program și ABP astfel încât P{A} are o refutație. Conform teoremei 2.4, A este o consecință logică a lui P (teorema 2.1).

Cctd.

Am putea reformula corolarul 2 astfel: se poate arăta că dacă ABP și P{A} posedă o refutație de lungime n, atunci ATPn. Acest rezultat a fost dat de Apt și van Emden.

Dacă A este un atom, vom nota [A]={A`BP / există o substituție astfel încât A`=A}. [A] este astfel mulțimea tuturor instanțelor închise ale lui A. Într-un mod asemănător [A] desemnează [A]I unde I este o preinterpretare Herbrand.

Teorema 2.2.2: Fie P un program definit și G un scop definit A1,…,Ak. Presupunem că P{G} are o refutație SLD de lungime n și că 1 , … ,n formează șirul celor mai generali unificatori din refutație. Atunci j=1..k[Aj1…n] este inclusă în TPn.

Demonstrație: Rezultatul se demonstrează prin inducție după lungimea refutației.

Presupunem că n=1. Atunci G este un scop de forma A1, programul are o clauză unitară de forma A și A11=A1. Avem evident că [A] TP1.

Prsupunem rezultatul adevărat pentru refutații de lungime n-1 și considerăm o refutație a lui P{G} de lungime n. Fie Aj un atom al lui G. Se deosebesc două cazuri:

Aj nu este atom ales al lui G. Atunci Aj1 este un atom al lui G1, al doilea scop al refutației. Din ipoteza refutației avem că [Aj12…n] TP(n-1) și TP(n-1) TPn datorită monotoniei lui TP.

Aj este atom ales al lui G. Fie BB1, … ,Bq (q0) prima clauză de intrare. Atunci Aj1 este o instanță a lui B. Dacă q=0, avem că [B] TP1. Astfel, [Aj12…n] [Aj1] [B] TP1 TPn.

Dacă q>0, prin ipoteza inducției, [Bi12…n] TP(n-1), pentru i=1,…,q. Datorită definiției lui TP, avem că:

[Aj12…n] TPn.

cctd.

Să ne întoarcem acum la problema verificării ocurențelor. După cum am precizatmai sus, verificarea ocurențelor în algoritmul de unificare este destul de grea și marea parte a sistemelor PROLOG nu o iau în considerare pentru motivul pragmatic de a avea foarte rar nevoie de acest lucru. Această omisiune poate crea serioase probleme.

Exemplu: Fie programul:

test p(x,x)

p(x,f(x)) .

Fie dat scopul test, un sistem PROLOG fără verificarea ocurențelor va răspunde “DA” (adică este un răspuns corect)! Acest răspuns este complet fals deoarece nu este o consecință logică a programului. Problema provine din faptul că, fără verificarea ocurențelor, algoritmul de unificare al sistemului PROLOG va face eroarea de a unifica p(x,x) și p(x,f(x)). Astfel se vede că lipsa verificării ocurenței a distrus unul din principiile pe care se bazează programarea logică – corectitudinea rezoluției SLD.

Exemplu: Fie programul:

test p(x,x)

p(x,f(x)) p(x,x).

În acest caz, un sistem PROLOG fără verificarea ocurențelor va face o buclă infinită în algoritmul de unificare, deoarece va încerca de a utiliza o legătură „circulară” făcută în a II-a etapă a calculului.

Cu toate că aceste exemple pot părea artificiale este important de știut că le putem întâlni ușor în programe. Situația întâlnită cel mai des este în cazul programelor ce includ diferențe de liste. O diferență de liste este un termen de forma X-Y unde „-„ este o funcție binară. X-Y reprezintă diferența între două liste: X și Y.

De exemplu 34.56.12.x-x reprezintă lista [34, 56, 12]. În același mod x-x reprezintă lista vidă.

Spunem că două diferențe de liste x-y și z-w sunt compatibile dacă y=z. Atunci diferențele de liste compatibile pot fi concatenate utilizând definiția următoare:

Concat(x-y, y-z, x-z)

De exemplu putem concatena 12.34.67.45x-x și 36.89.y-y într-o singură etapă pentru a obține 12.34.67.45.36.89.z-z. Aceasta este evident o tehnică foarte utilă. În acelați timp este periculoasă în absența verificării ocurențelor.

Exemplu: Fie programul:

test concat (u-u, v-v, a*w-w)

concat(x-y, y-z, x-z) .

Fiind dat scopul test, un sistem PROLOG fără verificarea ocurențelor va răspunde <<DA>>. Altfel spus un astfel de sistem PROLOG concatenează lista vidă cu lista vidă și obține lista [a]!

Este posibil de a reduce pericolul creat de problema verificării ocurențelor, utilizând o anumită metodologie de programare. O altă idee este aceea de a recurge la un preprocesor care este capabil să identifice clauzele care pot pune probleme și să adauge un cod de verificare pentru acesta.

2.3 COMPLETAREA REZOLUȚIEI SLD

Lema 2.3.1: Fie P un program definit și G un scop definit. Presupunem că P {G} are o refutație SLD fără restricții. Atunci P {G} are o refutație SLD de aceeași lungime astfel încât dacă 1, … , n sunt unificatorii refutației SLD fără restricții și 1, … , n cei mai generali unificatori ai refutației SLD, atunci există o substituție astfel încât 1…n=1`…n`.

Demonstrație: Demonstrația se face prin inducție după lungimea refutației fără restricții.

Presupunem că n=1. Atunci P {G} are o refutație fără restricții G0=G, G1= cu C1 clauză de intrare și 1 unificator. Presupunem că 1 este un cel mai general unificator al atomului din G și al capului clauzei unitare C1. Atunci 1=1`. În plus P {G} are o refutație G0=G, G1= cu C1 clauză de intrare și 1 un cel mai general unificator.

Presupunem acum rezultatul adevărat pentru n-1. Presupunem că P {G} are o refutație fără restricții G0=G, G1, … ,Gn=, de lungime n, cu C1, … , Cn clauze de intrare și 1, … ,n unificatori. Atunci există un cel mai general unificator 1 pentru atomul ales din G și capul clauzei C1 astfel încât 1=1`. Deci P {G} are o refutație fără restricții G0=G, G1`,C2, … ,Gn= cu C1, … , Cn clauze de intrare și 1`, 2, … ,n unificatori, unde G1=G1`.

Prin ipoteza de inducție P {G1} are o refutație G1`,G2`, … ,Gn`= cu șirul celor mai generali unificatori 2`, … ,n` astfel încât există pentru care 2…n=2`…n`. Deci Deci P {G} are o refutație G0=G, G1`, … ,Gn`= cu 1`, … ,n` șirul celor mai generali unificatori, șir pentru a cărui termeni avem: 1…n=1`2…n=1`…n`.

Cctd.

Lema 2.3.2: Fie P un program definit, G un scop definit și o substituție. Presupunem că există o refutație SLD a lui P {G}. Atunci există o refutație SLD a lui P {G} de aceeași lungime, astfel încât, dacă 1, … ,n sunt cei mai generali unificatori ai refutației SLD a lui P {G} și 1`, … ,n` respectiv ai refutației SLD a lui P {G}, atunci există o substituție astfel încât 1…n=1` …n`.

Lemele prezentate anterior conduc la un rezultat (stabilit de Apt și van Emden), rezultat ce constituie o reciprocă a corolarului 2 al teoremei 2.2.1.

Teorema 2.3.1: Mulțimea succeselor unui program definit este egală cu cel mai mic model Herbrand al programului.

Demonstrație: Fie P un program definit. Conform corolarului 2 al teoremei 2.2.1 este suficient să arătăm că cel mai mic model Herbrand al lui P este inclus în mulțimea succeselor lui P. Presupunem că A se află în cel mai mic model Herbrand al lui P, deci există n astfel încât ATPn. Vom arăta prin inducție după n că ATPn implică P {A} are o refutație și deci că A aparține mulțimii succeselor lui P.

Presupunem că n=1. ATP1 semnifică faptul că A este o instanță fără variabile a unei clauze unitare a lui P. P {A} are evident o refutație.

Presupunem rezultatul adevărat pentru n-1. Fie ATPn. Prin definiția lui TP, există o instanță fără variabile a unei clauze BB1,…,Bk astfel încât A=B și {B1,…, Bk} TP(n-1) pentru o substituție . Prin ipoteza de inducție, P { Bi} are o refutație pentru I=1,2,..,k. Deoarece fiecare Bi este închisă, aceste refutații se pot combina într-o refutație a lui P { (B1,…, Bk)}. Deci P { A} are o refutație fără restricții și se poate aplica lema 2.3.1 pentru a obține o refutație a lui P { A}.

Cctd.

Teorema 2.3.2: Fie P un program definit și G un scop definit. Presupunem că P {G} este insatisfiabilă. Atunci există o refutație SLD a lui P {G}.

Demonstrație: Fie G un scop A1,…,Ak. Deoarece P {G} este insatisfiabilă, G este fals în MP. Deci, există o instanță închisă G a lui G, falsă în MP. Astfel: {A1,…,Ak} MP conform teoremei 2.3.1, există o refutație pentru P {Ai}, pentru i=1,2,…,k. Deoarece fiecare A1 este închisă, putem combina aceste refutații într-o refutație pentru P {G}. În final se aplică lema 2.3.2.

Cctd.

Să considerăm acum răspunsurile corecte. Nu este posibil de a demonstra exact reciproca teoremei 2.2.1 deoarece răspunsurile calculate sunt întotdeauna “mai generale”. Totuți se poate arăta că orice răspuns corect este o instanță a unui răspuns calculat.

Lema 2.3.3: Fie P un program definit și A un atom. Presupunem că (A) este o consecință logică a lui P. Atnci există o refutație SLD a lui P {A} având substituția identică ca răspuns calculat.

Demonstrație: Fie x1, … ,xn variabilele lui A, a1, … ,an constante distincte care nu apar nici în A nici în P și substituția { x1/a1, … ,xn/an}. Este evident că A este o consecință logică a lui P. Deoarece A este închisă, teorema 2.3.1 arată că P {A} are o refutație. Cum ai nu apar nici în P nici în A, înlocuind ai prin xi (i=1,2, … ,n) în această refutație se obține o refutație a lui A {A} cu substituția identică ca răspuns calculat.

Putem acum să demonstrăm rezultatul cel mai important al completării, rezultat stabilit de Clark.

Teorema 2.3.3 (completarea rezoluției SLD):

Fie P un program definit și G un scop defint. Pentru orice răspuns corect al lui P {G} există un răspuns calculat pentru P {G} și o substituție astfel încât =.

Demostrație: Fie G scopul A1,…,Ak. Deoarece este corect, ((A1…Ak) ) este o consecință logică a lui P. Conform lemei 2.3.3, există o refutație a lui P {Ai} pentru i=1, … ,k astfel încât răspunsul calculat este substituția identică. Putem combina aceste refutații într-o refutație a lui P {G} astfel încât răspunsul calculat să fie identitatea.

Fie 1,…,n șirul celor mai generali unificatori ai refutației lui P {G}. Atunci G1…n=G. Conform lemei 2.3.2, există o refutație a lui P {G} cu 1`, … ,n` șirul celor mai generali unificatori astfel încât 1…n=1`…n„, pentru o substituție `. Fie substituția 1`…n` restrânsă variabilelor din G. Atunci =, unde este o restricție însușită (approprie) a lui `.

Cctd.

2.4 INDEPENDENȚA REGULII DE EVALUARE

Vom introduce în continuare conceptul de regulă de evaluare, concept ce este folosit pentru a alege atomii în derivația SLD. Vom arăta că pentru orice regulă de evaluare aleasă, dacă P {G} este insatisfiabilă, putem găsi întotdeauna o refutație utilizând această regulă. Acest fapt poartă numele de “independența” regulii de evaluare. Vom arăta de asemena că orice funcție calculabilă poate fi calculată printr-un program definit.

Definiția 2.4.1: O regulă de evaluare este o funcție definită pe o mulțime de scopuri definite cu valori într-o mulțime de atomi astfel încât valoarea funcție pentru un scop este un atom al acestui scop, numit atom ales.

Definiția 2.4.2: Fie P un program definit, G un scop definit și R o regulă de evaluare. O derivație SLD a lui P {G} prin R este o derivație SLD a lui P {G} în care regula de evaluare R este folosită pentru a alege atomi.

Este important de realizat faptul că, utilizarea unei reguli de evaluare pentru a alege atomii într-o derivație SLD reprezintă o restricție, în sensul că, dacă același scop apare în locuri (endroits) diferite, regula de evaluare va alege întotdeauna același atom al scopului.

Definiția 2.4.3: Fie P un program definit, G un scop definit și R o regulă de evaluare. O refutație SLD a lui P {G} prin R este o derivație SLD a lui P {G} în care regula de evaluare R este folosită pentru a alege atomii.

Definiția 2.4.4: Fie P un program definit, G un scop definit și R o regulă de evaluare. Un răspuns R – calculat pentru P {G} este un răspuns calculat pentru P {G} care provine dintr-o refutație SLD a lui P {G} prin R.

Putem acum evidenția rezultatele independenței. Conform teoremei 2.3.2, dacă P {G} este insatisfiabilă, atunci există o refutație a lui P {G}. Vom arăta că, pentru orice regulă de evaluare R, există întradevăr o refutație a lui P {G} prin R. Acest rezultat semnifică, în principiu, că un sistem de programare logică poate utiliza acea regulă de evaluare care i se pare utilă.

Cheia rezultatului de independență o reprezintă următoarea lemă (pentru care s-a făcut următoarea notație: dacă C este o clauză definită a programului, atunci C+ este capul clauzei și C- corpul ei).

Lema 2.4.1: Fie P un program definit și G un scop definit. Presupunem că P {G} are o refutație SLD, G0=G, G1, … , Gq-1, Gq, Gq+1, … ,Gn= , cu C1, … ,Cn clauze de intrare și 1,…,n șirul celor mai generali unificatori.

Presupunem că:

Gq-1 este A1,…, Ai-1, Ai, … , Aj-1, Aj, … ,Ak

Gq este (A1,…, Ai-1, C-q, … , Aj-1, Aj, … ,Ak)q

Gq+1 este (A1,…, Ai-1, C-q, … , Aj-1, C-q+1, … ,Ak)qq+1

Atunci există o refutație SLD a lui P {G} în care Aj este ales în Gq-1 în locul lui Ai și Ai este ales în Gq în locul lui Aj. În plus, dacă este răspunsul calculat pentru P {G} plecând de la refutația dată și ` – răspunsul calculat pentru P {G} plecând de la noua refutație, atunci G este o variantă a lui G`.

Demonstrație: Avem că Ajqq+1=C+q+1q+1= C+q+1q q+1. Putem unifica Aj și C+q+1.

Fie q` un cel mai general unificator al lui Aj și C+q+1. Avem atunci: qq+1=q`, pentru o substituție . Evident putem presupune că q` nu acționează asupra variabilelor din Cq.

În plus, C+q= C+qq`= C+qqq+1= Aiqq+1= Aiq`. Putem deci unifica C+q și Aiq`. Presupunem că q+1` este un cel mai general unificator. Avem atunci =q+1„, unde ` este o substituție. În consecință, q q+1=q`q+1„. Am arătat deci că Ai și Aj pot fi alese în ordinea inversă.

Știim că Aiq`q+1`= C+qq`q+1`, și q este un cel mai general unificator al lui Ai și C+q. Deci q`q+1`=q, pentru o substituție . Dar Ajq=Ajq`q+1`= C+q+1q`q+1`= C+q+1q= C+q+1. Deci unifică Ajq și C+q+1 și în consecință =q+1„, unde „ este o substituție. De aici rezultă că q`q+1`=qq+1„ și deci al q+1-lea scop în noua refutație este o variantă a lui Gq+1.

Restul noii refutații se derulează în aceeași manieră ca refutația dată și rezultatul decurge de aici.

Cctd.

Teorema 2.4.1 (independența regulii de evaluare):

Fie P un program definit și G un scop definit. Presupunem că există o refutație SLD pentru P {G} având ca răspuns calculat . Atunci pentru orice regulă de evaluare R, există o refutație SLD a lui P {G} prin R cu un răspuns R – calculat ` astfel încât G` să fie o variantă a lui G.

Demonstrație: Aplicând de mai multe ori lema 2.4.1 rezultatul este evident.

Cctd.

Putem utiliza teorema anterioară (2.4.1) pentru a “întării” teoremele 2.3.1, 2.3.2 și 2.3.3, demonstrațiile fiind immediate.

Teorema 2.4.2: Fie P un program definit și R o regulă de evaluare.Atunci mulțimea R – succeselor lui P este egală cu cel mai mic model Herbrand al lui P.

Teorema 2.4.3: Fie P un program definit, G un scop definit și R o regulă de evaluare. Presupunem că P {G} este insatisfiabilă. Atunci există o refutație SLD a lui P {G} prin R.

Teorema 2.4.4: Fie P un program definit, G un scop definit și R o regulă de evaluare. Atunci pentru orice răspuns corect al lui P {G}, există un răspuns R – calculat pentru P {G} și o substituție astfel încât =.

Stabilim în contiunare un rezultat foarte important: toate funcțiile calculabile pot fi calculate printr-un program definit. Există mai multe moduri de a stabili acest rezultat, după definiția aleasă pentru conceptul de “calculabil”. De exemplu, Tarnlund a arătat că toate funcțiile calculabile în sens Turing pot fi calculate printr-un program definit. Shepherdson a stabilit rezultatul utilizând pentru aceasta mașinile cu registru nelimitat. Vom urmării în continuare rezultatele stabilite de Sebelik și Stepanek, arătând că orice funcție recursivă parțială poate fi calculată printr-un program definit.

Teorema 2.4.5: Fie f o funcție n-ară recursivă parțială. Atunci există un program definit Pf și un simbol de predicat (n+1) – ar pf astfel încât toate răspunsurile calculate pentru Pf {pf(sk1(0), … , s kn(0),x)} având forma {x / sk(0)} și pentru toți întregii pozitivi k1, … ,kn și k, avem f(k1, … ,kn) = k dacă și numai dacă {x / sk(0)} este un răspuns calculat pentru P {pf(sk1(0), … , s kn(0),x)}.

Demonstrație: În programul Pf, un întreg pozitiv k este reprezentat prin termenul sk(0), în care s reprezintă funcția succesor. Conform teoremei 2.4.1 putem presupune că toate răspunsurile calculate sunt R – calculate, unde R desemnează regula de evaluare care alege întotdeauna cel mai din stânga atom. Rezultatul se demonstrează prin inducție după numărul q de aplicații de compunere, recursie primitivă și de minimalizare necesare pentru a defini funcția f.

Presupunem că q=0. Atunci f poate fi funcția nulă, fie funcția succesor, fie o funcție de proiecție.

funcția nulă.

Presupunem că f este funcția nulă: f(x)=0. Definim programul Pf astfel: pf(x,0).

funcția succesor.

Presupunem că f este funcția succesor: f(x)=x+1. Definim programul Pf astfel: pf(x,s(x)).

funcția de proiecție.

Presupunem că f este funcția de proiecție definită prin: f(x1,…,xn)=xj, unde 1jn. Definim programul Pf astfel: pf(x1,…,xn,xj).

Evident, pentru fiecare din aceste funcții de bază (a,b,c), programul Pf respectiv are proprietățile cerute.

Presupunem acum că funcția recursivă parțială este definită prin q (q>0) aplicații de compunere, recursie primitivă și minimalizare.

Compunere.

Presupunem că f este definită prin: f(x1,…,xn)= h(g1(x1,…,xn)…gm(x1,…,xn)) unde g1… gm și h sunt funcții recursive parțiale. Prin ipoteza de inducție fiecărui gi îi corespunde un program Pgi și un simbol de predicat pgi care satisfac proprietățile din teoremă. În aceeați manieră lui h îi corespunde un program Ph și un simbol de predicat ph satisfăcând proprietățile teoremei. Putem presupune că programele Pg1, … ,Pgm și Ph nu au nici un simbol de predicat comun. Fie Pf reuniunea acestor programe și a clauzei: pf(x1,…,xn,z) pg1(x1,…,xn,y1), … , pgm(x1,…,xn,ym), ph(y1,…,ym,z). Este evident că toate răspunsurile calculate pentru Pf { pf(sk1(0), … , s kn(0),z)} sunt de forma {z / sk(0)}, utilizând ipoteza de inducție.

Acum presupunem că f(k1,…,kn)=k. Atunci există ni astfel încât gi(k1,…,kn)=ni, pentru 1im. Prin ipoteza inducției, { yi / sni(0)} este un răspuns calculat pentru Pgi { pgi(sk1(0), … , s kn(0),yi)}. În același mod, {z / sk(0)} este un răspuns calculat pentru Ph { pf(sn1(0), … , snm(0),z)}. Deci {z / sk(0)} este un răspuns calculat pentru Pf { pf(sk1(0), … , s kn(0),z)}.

Reciproc, presupunem că {z / sk(0)} este un răspuns calculat pentru Pf { pf(sk1(0), … , s kn(0),z)}. Din refutația care dă răspunsul, putem extrage răspunsurile calculate { yi / sni(0)} pentru Pgi { pgi(sk1(0), … , s kn(0),yi)}, 1in și un răspuns calculat {z / sk(0)} pentru Ph { pf(sn1(0), … , snm(0),z)}. Rezultă atunci din ipoteza de inducție că gi(k1,…,kn)=ni, pentru 1im și că h(n1,…,nm)=k. Deci f(k1,…,kn)=k.

Recursia primitivă.

Presupunem că f este definită prin:

f(x1,…,xn,0)= h(x1,…,xn)

f(x1,…,xn,y+1)=g(x1,…,xn, x, f(x1,…,xn,y)), unde h și g sunt funcții recursive parțiale. Prin ipoteza de inducție, lui h (respectiv lui g) îi corespunde un program definit Ph (respectiv Pg) și un simbol de predicat ph (respectiv pg) care satisfac proprietățile din teoremă. Putem de asemenea presupune că Ph și Pg nu au nici un simbol de predicat comun. Fie Pf reuniunea lui Ph, Pg și a clauzelor:

pf(x1,…,xn,0,z) ph(x1,…,xn,z)

pf(x1,…,xn,s(x),z) pf(x1,…,xn,y,u), pg(x1,…,xn,y,u,z).

Analog demonstrației făcute în cazul compunerii, Pf are proprietățile cerute.

Minimalizarea.

Presupunem că f este definită prin: f(x1,…,xn)=y(g(x1,…,xn,y)=0), unde g este o funcție recursivă parțială;

y(g(x1,…,xn,y)=0) desemnează cel mai mic y astfel încât g(x1,…,xn,z) să fie definit pentru orice zy și g(x1,…,xn,y)=0, dacă un astfel de y există; în caz contrar y(g(x1,…,xn,y)=0) este nedeterminat. Prin ipoteza inducției lui g îi corespunde un program definit Pg și un simbol de predicat pg, satisfăcând proprietățile teoremei.

Fie Pf reuniunea dintre Pg și clauzele:

pf(x1,…,xn,y) pg(x1,…,xn,0,u), r(x1,…,xn,0,u,y)

r(x1,…,xn,y,0,y)

r(x1,…,xn,y,s(y),z) pg(x1,…,xn,s(y),u), r(x1,…,xn,s(y),u,z).

O justificare asemănătoare celei date în cazul compunerii arată că Pf are proprietățile cerute de teoremă.

Cctd.

2.5 PROCEDURILE REFUTAȚIEI SLD

Vom pune în evidență în continuare strategiile ce pot fi adoptate de un sistem de programare logică în căutarea sa în cursul unei refutații. Vom arăta că utilizarea unei strategii de căutare mai întâi în profunzime are implicații importante în ceea ce privește completitudinea.

Spațiul de căutare este un anumit tip de arbore, numit arbore – SLD. Rezultatele stabilite anterior arată că pentru a construi arborele SLD sistemul deține cont de diferitele reguli de evaluare. O regulă de evaluare poate fi stabilită de la început și se poate construi arborele SLD utilizând această regulă de evaluare. Acest lucru reduce considerabil mărimea spațiului de căutare.

Definiția 2.5.1: Fie P un program definit și G un scop definit. Un arbore SLD pentru P {G} este un arbore ce verifică următoarele condiții:

Fiecare nod al arborelui este un scop definit

Rădăcina arborelui este G

Fie A1, …, Am, … , Ak (k1) un nod al arborelui și Am atom ales. Atunci, pentru toate clauzele de intrare AB1, …, Bq astfel încât Am și A să fie unificabile cu nu cel mai general unificator , nodul are ca fiu: (A1, …, Am-1, B1, …, Bq ,Am+1, … , Ak)

Nodurile care sunt clauza vidă nu au fii.

Fiecare ramură a arborelui SLD este o derivație a lui P {G}. Ramurile corespunzătoare derivațiilor reușite sunt numite ramuri de succes, ramurile corespunzătoare derivațiilor infinite sunt numite ramuri infinite, iar ramurile corespunzătoare derivațiilor ce eșuează sunt numite ramuri de eșec.

Definiția 2.5.2: Fie P un program definit, G un scop definit și R o regulă de evaluare. Arborele SLD pentru P {G} prin R este arborele SLD pentru P {G} în care atomii aleși sunt acei atomi aleși prin regula R.

Exemplu: Fie programul: 1. p(x,z)q(x,y),p(y,z)

2. p(x,x)

3. q(a,b)

și scopul p(x,b). Arborele SLD pentru acest program și acest scop este:

p(x,b)

1 2

q(x,y), p(y,b) {x / b}

succes

3

p(b,b)

1 2

q(b,u), x(u,b) {x / a}

eșec succes

Arborele SLD prezentat anterior vine de la regula de evaluare standard PROLOG (alege atomul cel mai din stânga). Atomii aleși sunt subliniați. Observăm că acest arbore este finit și are două ramuri de succes corespunzătoare răspunsurilor {x / a} și {x / b}.

Arborele pentru programul și scopul prezentat anterior folosind regula de evaluare care alege întotdeauna cel mai din dreapta atom este:

p(x,b)

1 2

q(x,y), p(y,b) {x / b}

succes

1 2

q(x,y),q(y,u),p(u,b) q(x,b)

1 2 3

q(x,y),q(y,u),q(u,v),p(v,b) q(x,y),q(y,b) {x / a}

succes

1 2 3

. . q(x,a)

. . eșec

infinit

Observăm că acest arbore este infinit și are de asemenea două ramuri de succes, corespunzătoare răspunsurilor {x / a} și {x / b}.

Acest exemplu ne arată că alegerea regulii de evaluare influențează considerabil mărimea și structura arborelui SLD corespunzător. În acelați timp, oricare ar fi alegerea pentru regula de evaluare, dacă P {G} este insatisfiabilă, arborele SLD corespunzător are o ramură de succes.

Teorema 2.5.1: Fie P un program definit, G un scop definit și R o regulă de evaluare. Presupunem că P {G} este insatisfiabilă. Atunci arborele SLD pentru P {G} prin R are cel puțin o ramură de succes.

Teorema 2.5.2: Fie P un program definit, G un scop definit și R o regulă de evaluare. Atunci orice răspuns corect pentru P {G} este “afișat” (arătat) pe arborele SLD pentru P {G} prin R.

“Afișat” înseamnă că, fiind dată , există o ramură de succes astfel încât să fie o instanță a răspunsului calculat plecând de la refutația corespunzătoare acestei ramuri.

Deci, doi arbori SLD pot fi foarte diferiți prin mărimea și structura lor dar sunt “aceeași” în ceea ce privește ramurile de succes.

Teorema 2.5.3: Fie P un program definit, G un scop definit și R o regulă de evaluare. Atunci toți arborii SLD pentru P {G} fie au o infinitate de ramuri de succes fie au același număr finit de ramuri de succes.

Demonstrație: Utilizând lema 2.4.1 puntem considera o bijecție între ramurile de succes ale oricărei perechi de arbori SLD.

De exemplu, în cei doi arbori prezentați anterior, ramurile respective de succes care dau răspunsul {x / a} pot fi transformate una în cealaltă utilizând lema 2.4.1.

Să ne întoarcem acum asupra problemei de explorare a arborilor SLD pentru a găsi ramurile de succes.

Definiție 2.5.3: O regulă de căutare este o startegie de explorare a arborilor SLD având ca scop găsirea ramurilor de succes. O procedură de refutație SLD este caracterizată printr-o regulă de evaluare și printr-o regulă de căutare.

Sisteme PROLOG standard folosesc regula de evaluare care alege întotdeauna cel mai din stânga atom și o regulă de căutare la început în profunzime. Regula de căutare este implementată utilizând un șir (un (cap, stâlp, morman?) – pile de buts) de scopuri. O instanță a acestuia reprezintă ramura care este în curs de explorare.

Evaluarea devine un șir amestecat de înaintări și respingeri pe acesta (sur cette pile). O propulsare survine atunci când atomul ales în scop în vârful șirului (pile) este unificat cu succes cu scopul unei clauze a programului. Rezolventa este atunci propulsată pe înălțimea șirului (pile). O respingere survine atunci când nu mai este nici o clauză a programului a cărui cap să fie unificat cu atomul ales al scopului. Atunci acest scop este respins.

Pentru un sistem de căutare mai întâi în profunzime, regula de căutare se reduce la o regulă de ordine, adică, o regulă ce specifică ordinea în care clauzele programelor trebuie încercate. Sistemele standard PROLOG utilizează ordinea clauzelor într-un program ca ordine fixă în care ele trebuie încercate. Este foarte simplu și eficace de implementat această regulă de căutare, dar are dezavantajul că fiecare apel al unei definiții încearcă clauzele definiției în aceeași ordine.

Evident, se preferă ca regula de căutare să fie justă, adică toate ramurile de succes ale arborelui SLD să fie în final găsite. Pentru arborii SLD infiniți, regulile de căutare nu vor fi în general juste.

Conform teoremei 2.5.7, dacă P {G} este insatisfiabilă oricare ar fi regula de evaluare, arborele SLD corespunzător va conține întotdeauna o ramură de succes. Întrebarea este următoarea: un sistem de programare logică cu o regulă de căutare mai întâi în profunzime, utilizând o ordine fixă pentru a încerca clauzele programelor și o regulă de evaluare arbitrară va găsii întotdeauna ramura de succes? Din nefericire răspunsul este nu. Cu alte cuvinte nici unul din rezultatele precedente ale completitudinii nu este aplicabil. La marea majoritate a sistemelor PROLOG deoarece din motive de eficacitate a fost obligată implementarea unor reguli de căutare care nu sunt juste în sensul arătat mai sus.

Exemplu: Fie programul P:

p(a,b)

p(c,b)

p(x,z)p(x,y),p(y,z)

p(x,y)p(y,x)

și G scopul p(a,c). Este simplu de arătat că P {G} are o refutație și în plus dacă se elimină o clauză din P, P {G} nu mai are refutație.

Afirmăm că oricare ar fi ordinea clauzelor programului P și regula de evaluare, un sistem de programare logică utilizând o căutare mai întâi în profunzime cu ordine fixă pentru încercarea clasuzelor programului, nu va găsii niciodată o refutație. Această afirmație decurge imediat din faptul că atât clauza 3 cât și clauza 4 au capetele complet generale. Ele se vor unifica întotdeauna cu orcare subscop. Astfel, dacă clauza 3 este înaintea clauzei 4 în program, sistemul nu va considera niciodată clauza 4 și vice versa. Totuși sunt necesare toate clauzele într-o refutație.

Arborele SLD rezultat din utilizarea regulii de evaluare standard, care alege atomul cel mai la stânga, și a ordinii pentru încercarea clauzelor dată de ordinea clauzelor în program este:

p(a,c)

4

p(a,y),p(y,c) p(c,a)

p(b,c) . 3 . 4 . 3 4.

3 4

p(b,u),p(u,c) p(c,b)

3 4 2 3 4

. . succes . .

infinit

După cum se observă, ramura cea mai din stânga a acestui arbore SLD este infinită și astfel o căutare mai întâi în profunzime nu va găsi niciodată ramura de succes. De fapt, pentru orice regulă de evaluare și orice ordine fixă a încercării clauzelor programului, ramura cea mai din stânga a arborelui SLD corespunzător va fi infinită.

Să discutăm acum despre importanța utilizării unor reguli de evaluare corespunzătoare. Aceasta ar fi evident un pas înainte spre programarea pur declarativă dacă ar fi posibilă construirea unor sisteme care să găsească automatic o regulă de evaluare corespunzătoare (approprie) pentru fiecare program executat de sistem. Fie programul slowsort:

sort(x,y) sorted(y), perm(x,y)

sorted(nil)

sorted(x.nil)

sorted(x.y.z) xy, sorted (y,z)

perm(nil,nil)

perm(x.y,u.v) delete(u,x.y,z), perm(z,v)

delete(x,x.y,y)

delete(x,y.z,y.w) delete(x,z,w)

0x

f(x)f(y) xy

primul lucru de remarcat este faptul că acest program nu funcționează pe un sistem PROLOG standard! Fie scopul sort(17.22.6.5.nil,y). Un sistem PROLOG standard va face o buclă infinită deoarece sorted face pentru y supoziții incorecte din ce în ce mai lungi. Astfel un mod de a fixa problema este de a schimba definiția lui sort în: sort(x,y) perm(x,y), sorted(y). Astfel programul funcționează chiar dacă este ineficient. El triază lista dată efectuând permută la întâmplare și utilizând atunci predicatul sorted pentru a verifica dacă permutările sunt triate. Interesul programului slowsort este că dă o componentă logică foarte clară pentru un program de triere. Dezavantajul pentru sistemele PROLOG standard este că singurul mod de a le face eficiente este de a schimba substanțial logica. Pentru a conserva logica simplă prezentată mai jos este necesară o regulă de evaluare care să facă pe rând cu predicatele perm și sorted. În acest caz lista este dată lui perm, care efectuează o permutație parțială și apoi verifică cu sorted, dacă permutația parțială este corectă până aici. Dacă sorted găsește că permutația parțială este întradevăr triată, perm continuă permutația și apoi verifică încă o dată cu sorted. Dacă nu perm distruge permutația parțială, face o permutație puțin diferită și verifică încă o dată cu sorted. Un astfel de program este evident mult mai eficient decât acela care face o permutare întreagă înainte de a verifica dacă ea este triată.

Astfel se poate obține un program de triaj mai eficient adăugând un control inteligent logicii simple. Există numeroase sisteme PROLOG care autorizează programatorul să specifice un astfel de control. De exemplu, în NU-PROLOG programatorul poate adăuga declarațiile „când”:

? – sorted(nil) când de fiecare dată

? – sorted(x.y) când y

programului. Dar că, argumentul de apel al lui sorted este nil sau este de forma s.t, unde t nu este o variabilă, apel se efectuează. Astfel, apelurile soerted(nil) și sorted(3.2.x) se vor efectua. Dacă argumentul de apel al lui sorted nu se unifică nici cu nil nici cu x.y, atunci apelul se efectuează (și eșuează). Dacă argumentul de apel al lui sorted este de forma y sau s.y, atunci apelul lui sorted este întârziat. Când un apel sorted(y) sau sorted(s.y) este întârziat, variabila y este marcată. Când această variabilă este legată în continuare subscopul în așteptare este reluat. Acest mecanism simplu are comportamentul dorit.

În sistemele PROLOG standard, un subscop „generator” trebuie să vină înaintea unui subscop „test”. Astfel perm trebuie să fie utilizat înaintea lui sorted, dacă slowsort trebuie să fie executat pe un sistem PROLOG standard. Totuși, în NU-PROLOG, „test” trebuie utilizat înaintea „generatorului”. Această ordine asigură o bună funcționare între „test” și „generator”. Funcționarea începe prin a pune în așteptare „testul”. „Generatorul” este apoi efectuat până ce crează o legătură care obligă „testul” a fi reluat, și așa mai departe.

Declarațiile „când” nu ar fi interesante dacă (RAJOUT) lor ar necesita întotdeauna intervenția programatorului. Totuși NU-PROLOG posedă un procesor care este capabil să adauge automat declarațiile: „când” numeroaselor programe pentru a obține un comportament mai inteligent. De exemplu, programul slowsort fiind dat la intrare, preprocesorul sortează declarațiile „când” de mai sus pentru sorted (el dă de asemenea declarații „când” pentru perm, delete și <=, dar nu avem nevoie de acestea). El efectuează aceasta găsind clauze cu apeluri recursive care ar putea crea bucle infinite, și generând astfel de declarații când pentru a stopa buclele. Preprocesorul este de asemenea capabil să recunoască faptul că sorted este un test și poate apărea înaintea lui perm în prima clauză. El nu va reordona sorted și perm dacă este necesar. Ridicând programatorului o parte de responsabilitate de a furniza controlul în acest fel, NU-PROLOG este un pas spre idealul programării pur declarative.

CAPITOLUL 3

PROGRAME NORMALE

3.1 INFORMAȚIA NEGATIVĂ

Sistemele de inferență pe care le-am evidențiat până acum sunt foarte specializate. Rezoluția SLD nu se aplică decât mulțimilor de clauze Horn cerând doar o singură clauză scop. Utilizând rezoluția SLD, nu se poate niciodată deduce o informație negativă. Fie P un program definit și ABP. Nu se poate demonstra că A este o consecință logică a lui P: Motivul este că P {A} este satisfiabilă deoarece BP este un model.

Pentru a ilustra aceasta, fie programul:

elev(Joe)

elev(Bill )

elev(Jim)

profesor(Mary)

presupunem acum că vrem să demonstrăm că Mry nu este un elev, adică elev(Mary). După cum am arătat anterior elev(Mary) nu este o consecință logică a programului. Totuși, trebuie observat că nici elev(Mary) nu este o consecință logică a programului. Vom introduce acum o regulă de inferență specială: dacă un atom închis A nu este o consecință logică a unui program, atunci se deduce A. Această regulă de inferență este denumită ipoteza lumii închise (CWA – closed world assumption). Folosind regula introdusă, se poate deduce elev(Mary), deoarece elev(Mary) nu este o consecință logică a programului.

Regula CWA este adesea o regulă foarte naturală în utilizarea într-un context de baze de date. În bazele de date relaționale, această regulă este obișnuit aplicată: informația care nu este prezentă explicit în baza de date este considerată ca falsă. Evident în cazul programelor logice situația se complică datorită prezenței clauzelor non-unitare (non unité). Conținutul informațional al unui program nu este determinat doar prin examinarea sa. Acum el este înțeles ca fiind mulțimea a tot ceea ce se poate deduce din program. A ști dacă folosirea regulii CWA este sau nu justificată, trebuie să se determine fiecărei aplicații particulare. Cu toate că este adesea natural să utilizăm regula CWA, folosirea sa nu este întotdeauna justificată.

Să considerăm acum un program P căruia îi putem aplica regula CWA. Fie ABP și presupunem că vrem să obținem A. pentru a utiliza CWA trebuie să arătăm că A nu este o consecință logică a lui P. Din nefericire, nu există nici un algoritm care să accepte la intrare un A arbitrar și să răspundă într-un timp finit dacă A este sau nu o consecință logică a lui P. Dacă A nu este o consecință logică a lui P, poate apărea o buclă infinită. Astfel, în practică, se restrânge aplicarea regulii CWA atomilor ABP în care tentativele de demonstrare eșuează într-un timp finit.

Pentru un program definit P, mulțimea eșecurilor SLD finite ale lui P este mulțimea tuturor ABP pentru care există un arbore SLD de eșecuri finite pentru P {A}, adică un arbore finit care nu conține nici o ramură de succes. Știim că dacă A este inclusă într-o mulțime de eșecuri SLD finite ale lui P, A nu este o consecință logică a lui P și toți arborii SLD pentru P {A} nu conțin decât ramuri infinite sau ramuri de eșec.

Să revenim la CWA. Pentru a arăta că ABP nu este o consecință logică a lui P, putem încerca să dăm sistemului A ca scop. Presupunem că A nu este în mulțimea succeselor lui P. Există atunci două posibilități: fie A se află în mulțimea eșecurilor SLD finite, fie nu este inclusă în ea. Dacă A este în mulțimea succeselor SLD finite, sistemul poate atunci să construiască un arbore SLD de eșecuri finite și va returna răspunsul “nu”. Regula CWA permite atunci să deducem A. În caz contrar, fiecare arbore SLD are cel puțin o ramură infinită. Atunci, în afara cazului în care sistemul este un mecanism pentru detectarea ramurilor infinite, el nu va putea niciodată să arate că A nu este o consecință logică a lui P.

Aceste observații ne conduc spre o altă regulă de inferență denumită regula negației prin eșec. Această regulă, studiată mai întâi de Clark, este de asemenea utilizată pentru a obține informații negative. Ea stabilește faptul că dacă A este în mulțimea eșecurilor SLD finite ale lui P, atunci se poate deduce A. Cum mulțimea eșecurilor SLD finite este o submulțime a complementarei mulțimii succeselor, se observă că regula negației este mai puțin puternică decât CWA. Totuși, în practică, a implementa o regulă depășind negația prin eșec este dificilă.

Negația prin eșec este ușor implementabilă prin punerea în opoziție a noțiunilor de succes și eșec. Presupunem că ABP și că avem scopul m A. Sistemul încearcă scopul A. Dacă A reușește, atunci A eșuează în timp ce dacă A eșuează, atunci A reușește.

Se remarcă în continuare că programele definite în numeroase situații nu au destulă expresivitate. Problema o constituie faptul că avem deseori nevoie de o condiție negativă în corpul unei clauze. Fie exemplul:

diferit(x,y) element(z,x), element(z,y)

diferit(x,y) element(z,x), element(z,y)

care definește faptul că două mulțimi sunt diferite. Programele PROLOG în practică necesită deseori o astfel de expresivitate suplimentară. Astfel, este important de a introduce programele care includ și literali negativi în corpul clauzelor lor. Aceste programe sunt programele normale.

Totuși, chiar dacă programele normale permit literali negativi în corpul clauzelor programului nu se poate încă deduce informația negativă. Pentru a obține informația negativă dintr-un program normal, putem completa programul. Aceasta semnifică a adăuga programului partea „numai dacă” a definiției simbolurilor de predicate, asemenea unei teorii de egaliate. În exemplul precedent dacă adugăm partea „numai dacă” a definiției predicatului elev, obținem:

x(elev(x) (x = Joe) (x=Bill) (x=Jim))

adăgând axiomele pentru = putem acum obține elev(Mary). Acest procedeu de completare este un alt mod de a exprima ideea că o informație care nu a fost dată prin program este considerată ca fiind falsă. Conceptul de răspuns corect poate fi extins în acest context spunând că un răspuns este corect dacă scopul căruia I se aplică răspunsul este o consecință logică a completării programului.

Mecanismul obișnuit ales pentru a calcula răspunsurile este de a utiliza rezoluția SLDNF, care este rezoluția SLD căreia I se adaugă regula de negație prin eșec.

3.2 EȘECURI FINITE

Principalele rezultate stabilite în continuare privesc mai multe caracterizări ale mulțimii de eșecuri finite ale unui program definit. Vom stabili la început definiția unei mulțimi de eșecuri finite ale unui program definit, definiție dată de Lassez și Maher.

Definiția 3.2.1: Fie P un program definit. Atunci FdP, mulțimea atomilor din BP care sunt eșecuri finite de profunzime d, este definită astfel:

AFP` dacă ATP1

AFdP, pentru d>1, dacă pentru fiecare clauză BB1,…,Bn a lui P și fiecare substituție astfel încât A=B și B1,…,Bn să fie închise, există k{1,…,n} astfel încât BkFd-1P.

Definiția 3.2.2: Fie P un program definit. Mulțimea eșecurilor finite FP ale lui P este definită prin:

FP=d1FdP

Propoziție 3.2.1: Fie P un program definit. Atunci FP=BP – TP.

Definiția 3.2.3: Fie P un program definit și G un scop definit. Un arbore SLD de eșecuri finite pentru P {G} este un arbore care este finit și nu conține ramuri de succes.

Definiția 3.2.4: Fie P un program definit. Mulțimea eșecurilor SLD finite ale lui P este mulțimea tuturor ABP pentru care există un arbore SLD de eșecuri finite pentru P {A}.

Trebuie remarcat că în această definiție nu este necesar ca toți arborii SLD să fie arbori de eșecuri finite dar, că există cel puțin unul.

Principala problemă este de a stabili echivalența între FP și mulțimea de eșecuri SLD finite. Vom începe prin a evidenția 2 leme stabilite de Apt și van Emden a căror demonstrații sunt evidente.

Lema 3.2.1: Fie P un program definit, G un scop definit și o substituție. Presupunem că P {G} are un arbore SLD de eșecuri finite de profunzime k. Atunci P {G} are de asemenea un arbore SLD de eșecuri finite de profunzime k.

Lema 3.2.2: Fie P un program definit și AiBP pentru i=1,…,m. Presupunem că, P { A1,…,Am} are un arbore SLD de eșecuri finite de profunzime k. Atunci există i{1,…,m} astfel încât P {Ai} are un arbore SLD de eșecuri finite de profunzime k.

Propoziție 3.2.2: Fie P un program definit și ABP. Dacă P {A} are un arbore SLD de eșecuri finite de profunzime k, atunci ATPk.

Demonstrație: Presupunem mai întâi că P {A} are un arbore SLD de eșecuri finite de profunzime 1. Atunci ATP1.

Presupunem rezultatul adevărat pentru k-1. Presupunem că P {A} are un arbore SLD de eșecuri finite de profunzime k. Presupunem pentru a obține o contradicție că ATPk. Atunci există o clauză BB1,…,Bn în P astfel încât A=B și {B1,…,Bn} TP(k-1) pentru o anumită substituție . Atfel, există un cel mai general unificator astfel încât A=B și =, unde =substituție. Observăm că (B1,…,Bn) este rădăcina unui arbore SLD de eșecuri finite de profunzime k-1. Conform lemei 3.2.1 acest arbore este același cu al lui (B1,…,Bn). Prin lema 3.2.2 un anumit Bi este rădăcina unui arbore SLD de eșecuri finite de profunzime k-1. Prin ipoteza de inducție, BiTP(k-1) ceea ce furnizează contradicția.

Cctd.

Este interesant de remarcat că reciproca propoziției 3.2.2 nu este adevărată. Se observă apoi, că eșecul SLD finit garantează numai existența unui arbore SLD de eșecuri finite, celelalte putând fi infinite. Ar fi util de a se identifica modul exact de alegere a atomilor care garantează găsirea unui arbore SLD de eșecuri finite, dacă există. În acest scop Lassez și Maher au introdus conceptul de echitate.

Definiția 3.2.5: O derivație SLD este echiatbilă dacă fie eșuează fie pentru fiecare atom B al derivației, (o versiune instanțiată a lui) B este ales într-un număr finit de etape.

Notăm că există derivații SLD printr-o regulă de evaluare standard care nu sunt echitabili. Pentru a obține echitatea alegând mulțimii (eventual vidă) de atomi introduși în etapele precedente ale derivației, dacă există un astfel de atom; dacă nu alegând atomul cel mai la stânga.

Definiția 3.2.6: Un arbore SLD este echitabil dacă toate ramurile arborelui sunt derivații SLD echitabile.

Propoziția 3.2.3: Fie P un program definit și A1,…,Am un scop definit. Presupunem că există o derivație echitabilă care nu eșuează A1,…,Am=G0,G1,… , cu șirul celor mai generali unificatori 1,2,3,…. Atunci, fiind dat k, există n astfel încât [Ai1…n] TPk, pentru i{1,…,m}.

Demonstrație: Teorema 2.2.2 arată că putem presupune că derivația este infinită. Este evident că e necesar de a arăta faptul că fiind dat i{1,…,m} și k, există n astfel încât [Ai1…n] TPk. Să fixăm i{1,…,m}. Rezultatul este evident adevărat pentru k=0.

Presupunem că este adevărat pentru k-1. presupunem că Ai1…p-1 este ales în scopul Gp-1. (Prin echiate Ai trebuie în final ales). Fie Gp scopul B1,…,Bq, unde q1. Prin ipoteza inducției există s astfel încât 2j=1[Bjp+1…p+s] TP(k-1). Avem deci [Ai1…p+s] TP(TP(k-1))=TPk.

Cctd.

Combinând rezultatele stabilite de Apt și vanEmden și cele stabilite de Lassez și Maher putem acum obține o caracterizare a mulțimii de eșecuri finite.

Teorema 3.2.1: Fie P un program definit și ABP. Următoarele afirmații sunt echivalente:

AFP

ATP

A este în mulțimea eșecurilor SLD finite

Orice arbore SLD, echitabil pentru P {A} este un arbore de eșecuri finite.

Demonstrație:

este echivalent cu b) conform propoziției 3.2.1.

d) implică c) este evident.

c) implică b) conform propoziției 3.2.2

În final, predupunem că d) nu este verificat. Atunci există o derivație echitabilă care nu eșuează pentru A. Conform propoziției 3.2.3, ATP. b) nu este deci verificată.

Cctd.

Teorema 3.2.1, arată că rezoluția SLD echitabilă este o implementare justă și completă a eșecului finit.

PROGRAME NORMALE

În acest paragraf se vor introduce programele normale. Acestea sunt programele care pot conține literali negativi în corpul clauzelor lor. Vom defini de asemenea completarea (la completion) unui program normal. Completarea va juca un rol important în rezultatele corectitudinii și completitudinii pentru regula de negație prin eșec și rezoluția SLDNF.

Definiția 3.3.1: O clauză de program este o clauză de forma AL1,…,Ln, unde A este un atom și L1,…,Ln sunt literali.

Definiția 3.3.2: Un program normal este o mulțime finită de clauze de program.

Definiția 3.3.3: Un scop normal este o clauză de forma L1,…,Ln, unde L1,…,Ln sunt literali.

Definiția 3.3.4: Definiția unui simbol de predicat p al unui program normal P este mulțimea tuturor clauzelor programului P care acceptă p în capul lor.

Fiecare program definit este un program normal, reciproca fiind falsă.

Pentru a justifica folosirea regulii de negație prin eșec, Clark a introdus ideea completării unui program normal. Vom da acum definiția completării.

Definiția 3.3.5: Fie p(t1, … ,tn) L1, … ,Lm o clauză de program a unui program normal P. Vom avea nevoie de un simbol de predicat =, care nu apare în P. Prima idee este de a transforma clauza dată în:

p(x1, … ,xn) (x1=t1) … (xn=tn) L1 … Lm

unde x1, … ,xn sunt variabile ce nu apar în clauză. Atunci, dacă y1, … ,yd sunt variabilele clauzei originale, se va transforma clauza în:

p(x1, … ,xn) y1 …yd((x1=t1) … (xn=tn) L1…Lm)

Presupunem că am făcut această transformare pentru fiecare clauză din definiția lui p. Obținem astfel k1 formulele transformate de forma:

p(x1, … ,xn) E1

.

.

.

p(x1, … ,xn) Ek

unde Ei are forma generală y1 …yd((x1=t1) … (xn=tn) L1…Lm).

Definiția completă a lui p este atunci formula:

x1 … xn(p(x1, … ,xn)E1…Ek).

Exemplu: Presupunem că definiția unui simbol de predicat p este:

p(y) q(y), r(a,y)

p(f(z)) q(z)

p(b) .

Atunci definiția completă a lui p este:

xp(x) (y ((x=y)q(y)r(a,y)) z ((x=f(z)q(z))(x=b)))

Exemplu: Definiția completă a simbolului de predicat elev în exemplul din capitolul 3.1 este:

x(elev(x) (x=Joe) (x=Bill) (x=Jim))

Anumite simboluri de predicate din program pot să nu apară în capul unei clauze a programului. Pentru un astfel simbol de predicat q adăugăm explicit clauza:

x1 … xnq(x1, … ,xn)

Aceasta este definiția unui astfel de predicat q dată implicit de program. Vom numi de asemenea această clauză definiția completă a lui q.

Este esențial de a spune = unor anumite axiome. Teoria de egalitate care urmează este suficientă pentru aceasta. În aceste axiome vom utiliza notația standard pentru diferit.

c d pentru toate perechile c,d de constante distincte.

(f(x1, … ,xn) g(y1, … ,ym)) pentru toate perechile f, g de simboluri de funcții distincte.

(f(x1, … ,xn) c), pentru toate constantele c și toate simbolurile de funcție f.

(t[x] x), pentru fiecare termen t[x] ce conține x și este diferit de x.

((x1 y1) … (xn yn) f(x1, … ,xn) f(y1, … ,yn)) pentru toate simbolurile de funcție f

(x=x)

((x1 = y1) … (xn = yn) f(x1, … ,xn) = f(y1, … ,yn)) pentru toate simbolurile de funcție f

((x1 = y1)…(xn = yn)(p(x1, … ,xn) p(y1, … ,yn)) pentru toate simbolurile de funcție p

Definiția 3.3.6: Fie P un program normal. Completarea lui P notată comp(P) este colecția definițiilor completate ale simbolurilor de predicate p ale lui P și ale axiomelor teoriei de egalitate.

Axiomele 6,7 și 8 sunt axiome obișnuite ale teoriei de ordinul întâi cu egalitate. Remarcăm că axiomele 6 și 8 reunite implică, faptul că, = este o relație de echivalență. Teoria de egalitate restrânge foarte mult interpretările posibile ale lui =. Această restricție este esențială pentru a obține justificarea dorită a negației prin eșec. Aproximativ vorbind, se obligă = a fi interpretat ca o relație de identitate pe UP.

Convenim acum, să considerăm completarea unui program normal și nu programul normal în sine ca principal obiect de interes. Chiar dacă programatorul dă numai programul normal sistemului de programare logică este de înțeles că, conceptual, programul normal este completat de sistem. Acestei noțiuni corespunde conceptul de răspuns corect. Se pune atunci problema de a arăta că rezoluția SLD căreia i se adaugă regula de negație prin eșec, este o implementare justă și completă a conceptului declarativ de răspuns corect.

Definiția 3.3.7: Fie P un program normal și G un scop normal. Un răspuns pentru P {G} este o substituție pentru variabilele din G.

Definiția 3.3.8: Fie P un program normal, G un scop normal L1, … ,Lm, și un răspuns pentru P {G}. Spunem că este un răspuns corect pentru comp(P) {G} dacă ((L1…Ln) ) este o consecință logică a lui comp(P).

Este important să stabilim că această definiție generalizează defiția unui răspuns corect dată în paragraful 2.1. Primul rezultat pentru a stabili aceasta este propoziția următoare:

Propoziție 3.3.1: Fie P un program normal. Atunci P este o consecință logică a lui comp(P).

Demonstrație: Fie M un model al lui comp(P). Trebuie să arătăm că M este un model al lui P. Fie p(t1, … ,tn) L1, … ,Lm o clauză a programului P și presupunem că L1, … ,Lm nu sunt adevărate în M, pentru o asignare de variabile y1, … ,yn a clauzei.

Considerăm definiția completată a lui p:

x1 … xn(p(x1, … ,xn)E1…Ek)

și presupunem că Ei este: y1 …yd((x1=t1) … (xn=tn) L1…Lm). Acum luăm pentru xj asignarea lui tj (1jn), dată de asignarea de variabile y1, … ,yn de mai sus. Ei este atunci adevărată în M deoarece L1, … ,Lm sunt adevărate în M și de asemenea deoarece M trebuie să satisfacă axioma 6. Deci p(t1, … ,tn) este adevărat în M.

cctd.

Definiția 3.3.9: Fie J o interpretare a unui program normal P și I o interpretare bazată pe J. Atunci TJP(I) se definește astfel: TJP(I) = {AJ,V/ A L1…Ln P, V este o asignare de variabile relativ la J și L1…Ln este adevărată relativ la I și V}.

Dacă J este preinterpretarea Herbrand a lui P, vom scrie TP în locul lui TJP. Această convenție coincide cu folosirea precedentă a lui TP. Remarcăm faptul că TJP nu este în general monoton.

De exemplu, dacă P este programul: pp, atunci TP nu este monoton. Totuși, dacă P este un program definit, atunci TJP este monoton. Multe alte proprietăți subliniate anterior ale lui TP se extind ușor la TJP.

Propoziția 3.3.2: Fie P un program normal, J o preinterpretare a lui P și I o interpretare bazată pe J. Atunci I este un model al lui P dacă și numai dacă TJP(I) I.

Demonstrația acestei propoziții este analoagă celei făcute pentru propoziția 2.1.3.

Rezultatul următor arată că punctele fixe ale lui TJP dau modelele lui comp(P).

Propoziția 3.3.3: Fie P un program normal, J o preinterpretare a lui P și I o interpretare bazată pe J. Presupunem că I, căruia I se adaugă relația identitate asignată lui =, este un model alteoriei egalității. Atunci I, împreună cu relația identitate, este un model al lui comp(P) dacă și numai dacă TJP(I) = I.

Demonstrație: Presupunem pentru început că TJP(I) = I. Deoarece am presupus că I împreună cu relația = este un model al teoriei egalității, este suficient să arătăm că această interpretare este un model al fiecărei definiții completate din comp(P). considerăm o astfel de definiție de forma: x1 … xnq(x1, … ,xn). Deoarece I este un punct fix, este evident că interpretarea este un model al acestei formule.

Considerăm acum o definiție de forma: x1 … xn(p(x1, … ,xn)E1…Ek). Deoarece TJP(I) I, rezultă de aici că interpretarea este un model al formulei: x1 … xn(p(x1, … ,xn) E1…Ek). În același mod, deoarece TJP(I) I, rezultă interpretarea este un model al formulei: x1 … xn(p(x1, … ,xn) E1…Ek).

Reciproc, presupunem că I căruia i se adaugă relația identitate asignată lui „=”, este un model al lui comp(P). Uitlizând faptul că interpretarea este un model al formulelor de forma x1 … xn(p(x1, … ,xn) E1…Ek), rezultă că TJP(I) I. În același mod, utilizând faptul că interpretarea este un model al formulelor de forma x1 … xn(p(x1, … ,xn) E1…Ek) rezultă că TJP(I) I. Deci avem egaliate: TJP(I) = I.

Cctd.

Propoziția 3.3.4: Fie P un program definit și ABP. Atunci Ahfp(TP) dacă și numai dacă comp(P) {A} are un model Herbrand.

Demonstrație: Presupunem că Ahfp(TP). Atunci hfp(TP) {s=s/sUP} este un model Herbrand al lui comp(P) {A}, conform propoziției 3.3.3.

Reciproc, presupunem că comp(P) {A} are un model Herbrand M. Prin teoria egalității, relația identitate pe UP trebuie să fie asignată lui = în modelul M. M este deci de forma I {s=s/sUP} pentru o interpretare Herbrand I a lui P. Deci I= TP(I) conform propoziției 3.3.3 și în consecință hfp(TP).

Cctd.

Propoziție 3.3.5: Fie P un program definit și A1, … ,Am atomi. Dacă (A1…Am) este o consecință logică a lui comp(P), atunci este de asemenea o consecință logică a lui P.

Demonstrație: Fie x1, … ,xk variabilele din A1…Am. Trebuie să arătăm că x1 … xk(A1…Am) este o consecință logică a lui P, adică P {x1 … xk(A1…Am)} este insatisfiabilă sau, într-o manieră echivalentă, S = P {A1…Am} este insatisfiabilă, unde Ai desemnează formula Ai în care s-au înlocuit x1, … ,xk prin constantele lui Skolen (appropries).

Deoarece S este în formă clauzală, ne vom limita la interpretările Herbrand ale lui S. Putem considera de asemenea I ca o interpretare a lui P (remarcăm că I nu este neapărat o interpretare Herbrand a lui P). Presupunem că I este un model al lui P. Considerăm preinterpretarea J obținută plecând de la I, suprimând asignările simbolurilor de predicate ale lui I. Conform propoziției 3.3.2 avem că TJP(I) I. Deoarece TJP este monoton, propoziția 1.5.1 ne arată că există un punct fix I` I al lui TP. Cum I` căruia I se adaugă relația identitate asignată lui =, este evident un model al teoriei egalității, propoziția 3.3.3 arată că această interpretare este un model la lui comp(P). Deci A1`…Am` este falsă în această interpretare. Deoarece I` I, obținem că A1`…Am` este falsă în I. Deci S este insatisfiabilă.

Cctd.

Observăm că dacă am combina propozițiile 3.3.1 și 3.3.5 ar rezulta că informația pozitivă care poate fi dedusă din comp(P) este exact informația pozitivă ce poate fi dedusă din P.

Teorema 3.3.1: Fie P un program definit, G un scop definit și un răspuns pentru P {G}. Atunci este un răspuns corect pentru comp(P) {G} dacă și numai dacă este un răspuns corect pentru P {G}.

Această teoremă arată că definiția răspunsului corect dată în acest paragraf generalizează pe aceea ce a fost dată în paragraful 2.1.

Orice program normal este consistent, dar completarea unui program normal poate să nu fie consistentă. Se caută acum o condiție sintactică slabă suficientă pentru a afirma că, completarea unui program normal este consistentă.

Definiția 3.3.10: O aplicație de nivel a unui program normal este o aplicație definită pe mulțimea simbolurilor de predicate ale programului cu valori în mulțimea întregilor pozitivi. Imaginea unui simbol de predicat prin această aplicație este “nivelul” acestui simbol de predicat.

Definiția 3.3.11: Un program normal este ierarhic dacă el posedă o aplicație de nivel astfel încât, în orice clauză a programului de forma p(t1, … ,tn) L1, … ,Lm, nivelul oricărui simbol de predicat ce se găsește în corpul clauzei este strict inferior nivelului lui p.

Definiția 3.3.12: Un program normal este stratifiabil dacă posedă o aplicație de nivel astfel încât, în orice clauză a programului de forma p(t1, … ,tn) L1, … ,Lm, nivelul simbolurilor de predicate a oricărui literal pozitiv din corpul clauzei este inferior sau egal cu nivelul lui p și nivelul simbolurilor de predicate a oricărui literal negativ din corpul clauzei este strict inferior nivelului lui p.

Este evident că toate programele definite și toate programele normale sunt stratifiabile. Putem presupune fără a pierde din generaliate, că nivelele unui program stratifiabil sunt: 0,1, … ,k. Programele normale stratifiabile au fost introduse de Apt, Blair și Walker pentru a generaliza o clauză de baze de date tratate de Chandra și Harel, și mai târziu, independent de van Emden.

Chair dacă aplicația TJP nu este în general monotonă, ea posedă o proprietate importantă asemănătoare monotoniei pentru programele normale stratifiabile.

Propoziția 3.3.6: Fie P un program normal stratifiabil și J o preinterpretare a lui P.

Presupunem că P nu are decât predicate de grad 0. Atunci P este definit și TJP este monoton pe laticea interpretărilor bazate pe J.

Presupunem că nivelul maxim al predicatelor lui P est k+1. Fie Pk mulțimea clauzelor programlui P având în capul lor un simbol de predicat de nivel k. Presupunem că Mk este o interpretare bazată pe J a lui Pk și că Mk este un punct fix al lui TJPk. Atunci A={Mk S / S { p(d1, … ,dn) / p este un simbol de predicat de nivel k+1 și fiecare di se află în domeniul lui J}} este o latice completă, indusă de incluziunea mulțimilor. În plus este o sublatice a laticilor interpretărilor bazate pe J, și TJP restrâns la este bine definit și monoton.

Corolar: Fie P un program normal stratifiabil. Atunci comp(P) are un model Herbrand normal minimal.

Demonstrație: Un model normal este un model în care relația identitate este asignată lui =. Minimal semnifică faptul că nu există modele Herbrand normale strict inferioare.

Demonstrația se face prin inducție după nivelul maxim k, al simbolurilor de predicate ale lui P. Cazul k=0 utilizează propoziția 3.3.6 a) și propoziția 1.5.1 pentru a obține cel mai mic punct fix al lui TP. Propoziția 3.3.3 furnizează modelul. Tercerea de la k la k+1 în inducție utilizează propoziția 3.3.6 b) luând în locul lui Mk punctul fix furnizat de ipoteza de inducție.

Cctd.

CORECTITUDINEA REZOLUȚIEI SLDMF

În acest paragraf vom introduce conceptul fundamental de răspuns corect pentru comp(P) {G}. Cum îl vom implementa? Ideea esențială este de a utiliza rezoluția SLD căreia i se adaugă negația prin eșec (rezoluția SLDMF). Vom demonstra corectitudinea regulii de negație prin eșec și a rezoluției SLDMF. Vom da de asemenea condiții suficiente pentru a evita ca un clacul să se blocheze.

În definițiile care urmează, va fi necesar să alegem literali în scopurile normale. Selecția literalilor este supusă regulii următoare. Orice literal pozitiv se poate alege, dar numai un literal negativ închis poate fi ales. Această condiție este numită „condiția de securitate” a selecției literalilor și o vom utiliza pentru a asigura corectitudinea rezoluției SLDMF.

Definiția 3.4.1: Fie G scopul L1, … ,Lm, … ,Lp și C clauza AM1, … ,Mq. Atunci G` derivă din G și C utilizând un cel mai general unificator dacă următoarele condiții sunt îndeplinite:

L nu este un atom, numit atomul „ales” în G

este un cel mai general unificator al lui Lm și al lui A

G` este scopul normal (L1, … ,Lm-1,M1, … ,Mq, Lm+1, … ,Lp)

Definiția 3.4.2: Fie P un program normal și G un scop normal. O refutație SLDMF de rang 0 a lui P {G} este un șir G0=G, G1, … , Gn= de scopuri normale, un șir C1, … ,Cn de variante de clauze ale programului P și un șir 1, … ,n de cei mai generali unificatori astfel încât Gi+1 derivă în Gi și Ci+1 utilizând i+1.

Definiția 3.4.3: Fie P un program normal și G un scop normal. Un arbore SLDMF de eșecuri finite de rang 0 pentru P {G} este un arbore ce verifică următoarele condiții:

Arborele este finit și fiecare nod al său este un scop normal nevid;

Rădăcina arborelui este G;

Singurii aleși în nodurile arborelui sunt literalii pozitivi;

Fie L1, … ,Lm, … ,Lp un nod care nu este un nod terminal. Presupunem că Lm este un atom ales. Atunci pentru fiecare (variantă de) clauză de program din P AM1, … ,Mq astfel încât Lm și A sunt unificabile prin , acest nod are un fiu: (L1, … ,Lm-1,M1, … ,Mq, Lm+1, … ,Lp)

Fie L1, … ,Lm, … ,Lp un nod terminal al arborelui și Lm un atom ales. Atunci nu există nici (o variantă) clauză de program din P a cărui cap să se unifice cu Lm.

Definiția 3.4.4: Fie P un program normal și G un scop normal. O refutație SLDMF de rang k+1 a lui P {G} este un șir G0=G, G1, … , Gn= de scopuri normale, un șir C1, … ,Cn de variante de clauze de program ale lui P sau de literali negativi închiși și un șir 1, … ,n de substituții astfel încât, pentru fiecare i (1in) să avem fie:

Gi+1 derivă în Gi și Ci+1 utilizând i+1, fie

Gi este scopul L1, … ,Lm, … ,Lp, literalul Lm ales în Gi este un literal negativ închis Am și există un arbore SLDNF de eșecuri finite de rang k pentru P {G}. În acest caz, Gi+1 este scopul L1, … ,Lm-1,Lm+1 … ,Lp,I+1 substituția identică și Ci+1 – literal Am.

Definiția 3.4.5: Fie P un program normal și G un scop normal. Un arbore SLDNF de eșecuri finite de rang k+1 pentru P {G} este un arbore ce satisface condițiile următoare:

Arborele este finit și fiecare nod al arborelui este un scop normal nevid;

Rădăcina arborelui este G;

Dacă L1, … ,Lm, … ,Lp este un nod al arborelui care nu este nod terminal și Lm literalul ales, atunci fie:

i) Lm este un atom și pentru fiecare (variantă de) clauză de program AM1, … ,Mq astfel încât Lm și A să fie unificabili cu un cel mai general unificator , nodul are un fiu (L1, … , Lm-1, M1, … , Mq, Lm+1, … , Lp), fie

ii) Lm este un literal negativ închis Am și există un arbore SLDNF de eșecuri finite de rang k pentru P{Am}, caz în care unicul fiu al modelului este: L1, … ,Lm-1,Lm+1 … ,Lp

Dacă L1, … , Lm, … ,Lp este un nod terminal al arborelui și Lm este literalul ales. Atunci fie:

Lm este un atom și nu există nici o (variantă de) clauză de program a cărui cap să se unifice cu Lm, fie

Lm este un literal negativ închis Am și există o refutație SLDNF de rang k a lui P{Am}.

Observăm că o refutație SLDNF (respectiv un arbore SLDNF de eșecuri finite) de rang k este de asemenea o refuatție SLDNF (respectiv un arbore SLDNF de eșecuri finite) de rang n, pentru toți nk.

Definiția 3.4.6: Fie P un program normal și G un scop normal. O refutație SLDNF a lui P {G} este o refutație SLDNF de rang k a lui P {G} pentru un anume k.

Definiția 3.4.7: Fie P un program normal și G un scop normal. Un arbore SLDNF de eșecuri finite pentru P {G} este un arbore SLDNF de eșecuri finite de rang k pentru P {G}, pentru un anume k.

Definiția 3.4.8: Fie P un program normal și G un scop normal. Un răspuns calculat pentru P {G} este substituția obținută restrângând compunerea 1…n varibilelor din G, unde 1, … ,n este șirul substituțiilor utilizate într-o refutație SLDNF a lui P {G}.

Deoarece literalii negativi aleși sunt închiși, rezultă că dacă Li este un literal negativ al lui G, Li trebuie să fie închisă. Această definiție extinde pe aceea a unui răspuns calculat dată în paragraful 2.2.

Acum, fiind dată defiția unui răspuns calculat, să considerăm procedura pe care un sistem de programare logică ar pute-o utiliza pentru a aclcula răspunsurile, ideea esențială fiind de a folosi rezoluția SLD căreia i se adaugă regula negației prin eșec. Când un literal pozitiv este ales, se va utiliza în principal rezoluția SLD pentru a deriva noul scop. Când un literal negativ închis este ales, procesul de derivare a scopului este natrenat recursiv pentru a încerca să stabilească sunscopul negativ. Se poate considera acest subsop negativ, ca leme separate care trebuiesc să fie stabilite pentru a calcula rezultatul. Având ales un literal negativ închis A într-un scop, se încearcă a se construi un arbore SLDNF de eșecuri finite de rădăcină A înaintea continuării restului calculului. Dacă s-a reușit construirea unui astfel de arbore de eșecuri finite, subscopul A reușește. În caz contrar, dacă s-a găsit o refutație SLDNF pentru A, atunci subscopul A eșuează. Să remarcăm faptul că legăturile nu sunt construite decât prin apelurile reușite ale literalilor pozitivi. Apelurile negative nu vor putea niciodată să creeze legături; ele vor reuși sau vor eșua. Astfel, negația prin eșec este doar un test.

Definiția 3.4.9: Fie P un program normal și G un scop normal. O derivație SLDNF a lui P {G} constă într-un șir (finit sau infinit) G0=G, G1, … de scopuri normale, un șir C1, … ,Cn de variante de clauze de program (numite clauze de intrare) ale lui P sau de literali negativi închiși și un șir 1, … de substituții ce satisfac următoarele condiții:

Pentru fiecare I, fie:

Gi+1 derivă din Gi și dintr-o clauză de intrare Ci+1 utilizând i+1, fie

Gi este L1, … ,Lm, … ,Lp, literalul ales în Gi este un literal negativ închis Am și există un arbore SLDNF de eșecuri finite pentru P {Am}. În acest caz, Gi+1 este L1, … ,Lm-1,Lm+1 … ,Lp,I+1 substituția identică și Ci+1 – literal Am.

Dacă șirul G0, G1, … de scopuri este finit, atunci fie

ultimul scop este vid, fie

ultimul scop este L1, … ,Lm, … ,Lp; Lm un atom, Lm este ales și nu există nici o (variantă de) clauză de program în P a cărui cap să se unifice cu Lm, fie

ultimul scop este L1, … ,Lm, … ,Lp; Lm este un literal negativ închis Am, Lm este ales și există o refutație SLDNF a lui P {Am}.

Definiția 3.4.10: Fie P un program normal și G un scop normal. Un arbore SLDNF pentru P {G} este un arbore ce verifică următoarele condițiile:

Fiecare nod al arborelui este un scop normal (eventual vid)

Rădăcina arborelui este G

Fie L1, … ,Lm, … ,Lp (p1) este un nod al arborelui care nu este nod terminal și presupunem că Lm literalul ales. Atunci fie:

i) Lm este un atom și pentru fiecare (variantă de) clauză de program AM1, … ,Mq astfel încât Lm și A să fie unificabile cu un cel mai general unificator , nodul are un fiu (L1, … , Lm-1, M1, … , Mq, Lm+1, … , Lp), fie

ii) Lm este un literal negativ închis Am și există un arbore SLDNF de eșecuri finite de pentru P{Am}, caz în care singurul fiu este: L1, … ,Lm-1,Lm+1 … ,Lp

d) Fie L1, … , Lm, … ,Lp (p1) un nod terminal al arborelui și presupunem că Lm este ales. Atunci fie:

i) Lm este un atom și nu există nici o (variantă de) clauză de program în P a cărui cap să se unifice cu Lm, fie

Lm este un literal negativ închis Am și există o refutație SLDNF de rang k a lui P{Am}.

e) Nodurile care sunt clauze vide nu au nici un fiu.

Conceptele de derivație SLDNF, refutație SLDNF și arbore SLDNF generalizează conceptele de derivație SLD, refutației SLD și respectiv arbore SLD. O derivație SLDNF este finită dacă ea este constituită dintr-un șir finit de scopuri, în caz contrar ea este infinită. O derivație SLDNF este reușită dacă ea este finită și dacă ultimul scop este scopul vid. O derivație SLDNF eșuează dacă ea este finită și ultimul scop nu este scopul vid. În același mod, se definesc ramurile de succes, ramurile inifnite și ramurile de eșec ale unui arbore SLDNF. Este evident că o derivație SLDNF reușită este o refutație SLDNF și un arbore SLDNF a cărui fiecare ramură de eșecuri este un arbore SLDNF de eșecuri finite.

Dacă un scop nu conține decât literali negativi care nu sunt închiși, atunci, din cauza condiției de securitate, nici un literal nu poate fi ales. Să formulăm această noțiune.

Un calcul al lui P {G} este o tentativă de a construi o derivație SLDNF a lui P {G}.

Definiția 3.4.11: Fie P un program normal și G un scop normal. Spunem că un calcul al lui P {G} se blochează (se înămolește – s`enlise) dacă într-un loc al derivației se ajunge la un scop care nu conține decât literali negativi ce nu sunt închiși.

Exemplu: Dacă G este un scop p(x) și P este un program normal, calculul lui P {G} se blochează imediat.

Să dăm acum o condiție suficientă pentru a fi siguri că rezoluția SLDNF nu se blochează niciodată.

Definiția 3.4.12: Fie P un program normal și G un scop normal.

Spunem că o clauza de program A L1, … ,Ln a lui P este admisibilă dacă fiecare variabilă ce apare în clauză, apare fie în capul A, fie într-un literal pozitiv al corpului L1, … ,Ln.

Spunem că o clauză de program A L1, … ,Ln a lui P este autorizată dacă fiecare variabilă ce apare în clauză, apare într-un literal pozitiv al corpului ei L1, … ,Ln.

Spunem că un scop G este autorizat dacă G este de forma L1, … ,Ln și toate variabilele care apar în G apar într-un literal pozitiv al corpului L1, … ,Ln.

Spunem că P {G} este autorizat dacă următoarele condiții sunt îndeplinite:

orice clauză a lui P este admisibilă

orice clauză din definiția unui simbol de predicat ce apare într-un literal pozitiv al corpului lui G sau într-un literal pozitiv al corpului unei clauze este autorizată

G este autorizată.

Observăm că o clauză unitară autorizată trebuie să fie închisă și că orice clauză autorizată este admisibilă.

Propoziția 3.4.1: Fie P un program normal și G un scop normal. Presupunem că P {G} este autorizat. Propozițiile următoare sunt atunci verificate:

nici un calcul al lui P {G} nu se blochează

orice răspuns calculat pentru P {G} este o substituție închisă tuturor variabilelor din G.

Demonstrație: a) Deoarece P {G} este autorizat, se poate demonstra că scopul într-o derivație SLDNF a lui P {G} este autorizat. Rezultatul decurge din faptul că un scop ce nu conține decât literali negativi care nu sunt închiși nu este autorizast.

Fie G scopul L1, … ,Lm și fie G0=G, G1, … , Gn= o refutație SLDNF a lui P {G} utilizând substituțiile 1, … ,n . amintim faptul că orice clauză de intrare a cărui scop se unifică cu un literal pozitiv la cel mai mare nivel al refutației are proprietatea că fiecare variabilă ce apare în capul clauzei apare de asemenea în corpul clauzei. Se poate arăta prin inducție după lungimea n a refutației că (L1 … Lm)1…n este închisă. Rezultatul decurge imediat de aici.

Lema 3.4.1: Fie p(s1, … ,sn) și p(t1, … ,tn) doi atomi.

Dacă p(s1, … ,sn) și p(t1, … ,tn) nu sunt unificabili atunci ((s1=t1) … (sn=tn)) este o consecință logică a teoriei egalității

Dacă p(s1, … ,sn) și p(t1, … ,tn) sunt unificabili cu un cel mai general unificator ={x1/r1,…, xk/rk} dat de algoritmul de unificare, atunci ((s1=t1) … (sn=tn) (x1=r1) … (xk=rk)) este o consecință logică a teoriei egalității.

Demonstrație: Presupunem că p(s1, … ,sn) și p(t1, … ,tn) sunt unificabili cu un cel mai general unificator ={x1/r1,…, xk/rk}. Atunci din axiomele 6,7 și 8 teoriei egalității rezultă că ((s1=t1) … (sn=tn) (x1=r1) … (xk=rk)) este o consecință logică a teoriei egalității. Restul lemei se demonstrează prin inducție după numărul k de etape din algoritmul de unificare pentru a încerca să se unifice p(s1, … ,sn) și p(t1, … ,tn).

Presupunem mai întâi că k=1. Dacă algoritmul de unificare găsește o substituție, de exemplu {x1/r1}, care unifică p(s1, … ,sn) și p(t1, … ,tn), atunci axioma 5 a teoriei egalității permite să arătăm că ((s1=t1) … (sn=tn) (x1=r1)) este o consecință logică a teoriei egalității. În caz contrar se folosește axioma 5 și una din axiomele 1 – 4 pentru a arăta că ((s1=t1) … (sn=tn)) este o consecință logică a teoriei egalității.

Presupunem acum rezultatul adevărat pentru k-1. Fie p(s1, … ,sn) și p(t1, … ,tn) aceia care algoritmul de unificare decide în k etape dacă sunt unificabili sau nu. Presupunem că 1={x1/r1`} este prim asubstituție făcută prin algoritmul de unificare. Atunci p(s1, … ,sn) 1 și p(t1, … ,tn) 1 sunt astfel încât algoritmul de unificare poate să descopere în k-41 etape dacă sunt unificabili sau nu.

Presupunem că p(s1, … ,sn)1 și p(t1, … ,tn)1 nu sunt unificabili. Atunci, prin ipoteza inducției, ((s1=t1)1 … (sn=tn)1) este o consecință logică a teoriei egalității. Rezultă atunci de aici și din faptul că 1 este prima substituție făcută prin algoritmul de unificare că ((s1=t1) … (sn=tn)) este o consecință logică a teoriei egalității.

Presupunem că p(s1, … ,sn)1 și p(t1, … ,tn)1 sunt unificabili. Din ipoteza inducției, se obține că ((s1=t1)1 … (sn=tn)1 (x2=r2) … (xk=rk) ) este o consecință logică a teoriei egalității. Rezultă atunci de aici și din faptul că r1 este r1`, unde = {x2/r2,…, xk/rk} și din axiomele 5,6,7 și 8 de egalitate că ((s1=t1) … (sn=tn) (x1=r1) … (xk=rk)) este o consecință logică a teoriei egalității.

Cctd.

Lema 3.4.2: Fie P un program normal și G un scop normal. Presupunem că literalul ales în G este pozitiv:

Dacă nu există scopuri derivate, atunci G este o consecință logică a lui comp(P)

Dacă mulțimea {G1, … ,Gr} de scopuri derivate este nevidă, atunci G G1 … Gr este o consecință logică a lui comp(P).

Demonstrație: Presupunem că G este scopul normal M1, … ,Mq și că literalul pozitiv ales Mj este p(s1, … ,sn). Dacă definiția completă a lui p este ( p(s1, … ,sn)) atunci este evident că G este consecință logică a lui comp(P).

Acum, presupunem că definiția completă a lui p este:

(p(x1, … ,xn) E1…Ek) unde Ei este de forma: yi,1…yi,di((x1=ti,1) … (xn=ti,n) Li,1…Li,mi). Rezultă că:

G ki=1 (M1 … Mj-1(s1=ti,1) … (sn=ti,n) Li,1…Li,mi Mj+1 … Mq) este o consecință logică a lui comp(P). Dacă p(s1, … ,sn) nu se unifică cu capul nici unei clauze de program din definiția lui p, atunci rezultă din lema 3.4.1 a) că G este o consecință logică a lui comp(P).

Pe de altă parte, presupunem că ar fi un cel mai general unificator al lui p(s1, … ,sn) și al lui p(ti,1, … ,ti,n). Atunci: (M1 … Mj-1(s1=ti,1) … (sn=ti,n) Li,1 … Li,mi Mj+1 … Mq (M1 … Mj-1 Li,1…Li,mi Mj+1 … Mq) este o consecință logică a lui comp(P) utilizând lema 3.4.1 b) și axiomele de egaliate 6,7 și 8. Astfel, dacă {G1, … ,Gr} este mulțimea scopurilor derivate, atunci G G1 … Gr este o consecință logică a lui comp(P).

Cctd.

Teorema 3.4.1 (corectitudinea regulii de negație prin eșec):

Fie P un program normal și G un scop normal. Dacă P {G} are un arbore SLDNF de eșecuri finite, atunci G este o consecință logică a lui comp(P).

Demonstrație: Demonstrația se face prin inducție după rangul k al arborelui SLDNF de eșecuri finite pentru P {G}. Fie G scopul L1, … ,Ln.

Presupunem mai întâi k=0. Atunci rezultatul decurge printr-o inducție standard după profunzimea arborelui utilizând lema 3.4.2.

Presupunem că rezultatul este adevărat pentru arbori SLDNF de eșecuri finite de rang k. Considerăm un arbore de eșecuri finite de rabg k+1 pentru P {G}. Vom stabili rezultatul printr-o inducție auxiliară după profunzimea acestui arbore.

Presupunem mai întâi că profunzimea acestui arbore este 1 și de asemenea că literalul ales în G este pozitiv. Atunci rezultatul decurge din lema 3.4.2 a). Dacă literalul Li ales în G este un literal negativ închis Ai, deoarece profunzimea este 1, există o refutație SLDNF de rang k a lui P {Ai}. Remarcăm că pentru un scop al cărui literal ales este pozitiv, scopul derivat este o consecință logică a scopului dat și a clauzei de intrare. Atunci, utilizând propoziția 3.3.1 și aplicând ipoteza de inducție asupra arborelui SLDNF de eșecuri finite de rang k-1 în această refutație, se obține că Ai este o consecință logică a lui comp(P). Deci ( L1…Ln) este de asemena o consecință logică a lui comp(P).

Presupunem acum că arborele SLDNF de eșecuri finite pentru P {G} are profunzimea d+1 și că literalul ales în G este pozitiv. Atunci rezultatul decurge din lema 3.4.2 b) și din ipoteza de inducție auxiliară. Presupunem că literalul ales în G este literalul negativ închis Li. Din ipoteza de inducție auxiliară se obține că ( L1… Li-1 Li+1… Ln) este de asemena o consecință logică a lui comp(P). Deci ( L1…Ln) este de asemena o consecință logică a lui comp(P).

Corolar: Fie P un program definit. Dacă AFP, atunci A este o consecință logică a lui comp(P).

Teorema 3.4.2 (corectitudinea rezoluției SLDNF):

Fie P un program normal și G un scop normal. Atunci orice răspuns calculat pentru P {G} este un răspuns corect pentru comp(P) {G}.

Demonstrație: Fie G un scop normal L1, … ,Lk și 1, … ,n șirul substituțiilor folosite într-o refutație SLDNF a lui P {G}. trebuie să arătăm că ((L1, … ,Lk)1 … n) este o consecință logică a lui comp(P). Rezultatul se arartă prin inducție după lungimea refutației SLDNF.

Presupunem mai întâi că n=1. Aceasta înseamnă că G este de forma L1. Considerăm două cazuri:

L1 este pozitiv.

Atunci P este o clauză unitară de forma A și L11=A1. deoarece L11 este o instanță a unei clauze unitare a lui P, rezultă de aici că (L11) este o consecință logică a lui P și deci a lui comp(P).

L1 este negativ.

În acest caz, L1 este închis, 1 este substituția identică și teorema arată că L1 este o consecință logică a lui comp(P).

Presupunem acum rezultatul adevărat pentru răspunsurile calculate care provin dintr-o refutație SLDNF de lungime n-1. Fie 1, …, n șirul substituțiilor folosite în refutația SLDNF a lui P {G} de lungime n. Fie Lm literalul ales în G. Există două cazuri:

Lm este pozitiv

Fie A M1, … ,Mq (q0) prima clauză de intrare. Din ipoteza de inducție, ((L1 … Lm-1 M1 … Mq Lm+1 … Lk)1 … n) este o consecință logică a lui comp(P). Deci, dacă q>0, ((M1, … ,Mq)1 … n) este o consecință logică a lui comp(P). În consecință, (Lm1 … n) care este egal cu (A1 … n) este o consecință logică a lui comp(P). deci, ((L1 … Lk )1 … n) este o consecință logică a lui comp(P).

Lm este negativ.

În acest caz, Lm este închis, 1 este substituția identică și teorema anterioară arată că Lm este o consecință logică a lui comp(P). Utilizând ipoteza de inducție, se obține că ((L1 … Lk )1 … n) este o consecință logică a lui comp(P).

Cctd.

Vom examina în continuare dacă se poate „slăbi” condiția de securitate pusă asupra alegerii literalilor. Începem prin a arăta că fără această condiție, teorema 3.4.1 nu mai este adevărată.

Exemplu: Fie programul P:

p q(x)

q(a)

Dacă nu considerăm condiția de securitate, literalul q(x) poate fi ales și se obține un arbore SLDNF de eșecuri finite pentru P { p}. Subscopul q(x) eșuează deoarece există o refutație a lui q(x) în care x este legat la a. În același timp, este ușor de văzut că p nu este o consecință logică a lui comp(P).

Este posibil să slăbim puțin condiția de securitate și să obținem aceleași rezultate. Fie condiția de securitate următoare, mai slabă. Subscopurile negative care nu sunt închise sunt autorizate să funcționeze. Dacă subscopul negativ reușește, vom proceda ca în cazul anterior. Dacă acesta eșuează, se verifică dacă nici o legătură n-a fost făcută asupra variabileleor scopului de început al refutației corespunzătoare. Dacă nici o legătură nu a fost făcută, subscopul negativ este autorizat să eșueze și se procedează ca în cazul precedent. Dacă nu, se alege un literal diferit și subscopul negativ este pus în așteptare în speranța că mai multe din variabilele sale vor fi legate ulterior. Alternativ, o eroare de control ar putea fi generată și programul se oprște.

Punctul cheie în acest caz este faptul că refutația care face să eșueze subscopul negativ trebuie să demonstreze câteva lucruri de forma (A) mai degrabă de cât (A). Pentru această condiție de securitate mai slabă, teoremele 3.4.1 și 3.4.2 rămân adevărate. Singura schimbare a demonstrațiilor lor o găsim în demonstrația teoremei 3.4.1 în locul unde am folosit faptul că A este închisă.

Cel mai simplu mod de a implementa condiția de securitate într-un sistem de programare logică este de a diferenția (separa) scopurile negative până când toate variabilele ce apar în subsop să fie legate de termenii închiși. Din nefericire, marea majoritate a sistemelor PROLOG nu au un mecanism care să le permită să diferențieze subsopurile și nu pot deci să utilizeze această metodă. Și mai grav, marea majoritate a sistemelor PROLOG „nu își nu dau oboseala” să verifice dacă subscopurile apelate sunt închise. Aceasta poate să ducă la o situație mai degrabă ciudată.

Exemplu: Fie programul:

p(a)

q(b)

și scopul normal p(x), q(x). Dacă acest program și acest scop sunt executate pe un sistem PROLOG care utilizează regula de evaluare standard, și nu verifică dacă subscopurile apelate sunt închise, atunci va returna răspunsul „da”! Pe de altă parte, MU-PROLOG și NU-PROLOG diferă primul subscop, rezolvă cel de al doilea scop și apoi vor rezolva primul scop pentru a da răspunsul corect {x / b}. Bineînțeles, problema cu acest scop particular poate fi rezolvată de un sistem PROLOG standard, reordonând subsopurile scopului.

COMPLETITUDINEA REZOLUȚIEI SLDNF

În acest paragraf vom arăta rezultatele completitudinii pentru regula de negație prin eșec pentru programele definite și pentru rezoluțiile SLDNF ale programelor ierarhice. Vom face de asemena un rezumat al principalelor rezultate ale capitolului.

Teorema 3.5.1 (completitudinea regulii de negație prin eșec):

Fie P un program definit și G un scop definit. Dacă G este o consecință logică a lui comp(P), atunci orice arbore SLD echitabil pentru P {G} este un arbore de eșecuri finite.

Demonstrație: Fie G scopul A1, … ,Aq. Presupunem că P {G} are un arbore SLD echitabil care nu este un arbore de eșecuri finite. Arătăm că comp(P) {(A1 … Aq)} are un model.

Fie BR o ramură care nu este o ramură de eșecuri în arborele SLD. Presupunem că BR este: G0=G, G1, … cu șirul celor mai generali unificatori 1, 2, … și clauzele de intrare C1, C2, … . Prima etapă este de a utiliza BR pentru a defini o preinterpretare J pentru P.

Presupunem că L este limbajul de ordinul I (sous – jacent) lui P. Evident presupunem L suficient de bogat pentru a putea standardiza variabilele separate în BR. Dfefinim o relație * pe mulțimea tuturor termenilor din L astfel: fie s și t doi termeni din L. Atunci s*t dacă există nN astfel încât s1 … n=t1 … n, adică dacă 1 … n unifică s și t. Este evident că * este o relație de echivalență. Se definește atunci domeniul D al preinterpretărilor J ca mulțimea tuturor claselor de echivalență ale termenilor lui L prin relația *. Dacă s este un termen al lui L, notâm [S] clasa de echivalență pentru * conținând pe s.

Să dăm acum asignările constantelor și simbolurilor defuncții din L. Dacă c este o constantă a lui L, I se asignează [e]. Dacă f este un simbol de funcție n –ară din L, îi asignăm lui f aplicația definită pe Dn cu valori în D care lui ([s1], … ,[sn]) îi asociază [f(s1, … ,sn)]. Este evident că această aplicație este bine definită. Aceasta completează definiția lui J.

Rămâne a da asignările simbolurilor de predicate pentru a extinde J unei interpretări a lui comp(P) {(A1 … Aq)}. Începem prin a defini mulțimea I0 astfel:

I0={p([t1], … ,[tn]) / p(t1, … ,tn) apare în BR}.

Arătăm că I0 TJP(I0), unde TJP este aplicația asociată preinterpretării J. Presupunem că p([t1], … ,[tn]) I0, unde p(t1, … ,tn) apare în Gi, i. Deoarece BR este echitabil și nu este o ramură de eșec, există j astfel încât p(s1, … ,sn) = p(t1, … ,tn)I+1 … I+j apare în scopul Gi+j și p(s1, … ,sn) este atomul ales în Gi+j. Presupunem că Ci+j+1 este p(r1, … ,rn) B1,…,Bm. Prin definiția lui TJP rezultă că p([r1I+j+1], … ,[rnI-j-1]) TP(I0). Atunci utilizând faptul că pentru orice k se poate presupune 1 … k idempotent, avem că:

p([t1], … ,[tn]) = p([t1I+1 … I+j], … ,[tnI+1 … I+j],)

= p([s1], … ,[sn])

= p([s1I+j+1], … ,[snI-j-1])

= p([r1I+j+1], … ,[rnI-j-1])

astfel că p([t1], … ,[tn]) TJP(I0). Deci I0 TJP(I0).

Acum, conform propoziției 1.5.1, există I astfel încât I0 I și I = TJP(I). I dă asignările simbolurilor de predicate din L. Am asignat relația egalitate lui “=”.

Astfel se completează definiția interpretării I, căreia I se adaugă relația identitate asignată lui =, pentru comp(P) {(A1 … Aq)}. Remarcăm că această interpretare este un model al lui (A1 … Aq) căci I0 I. Remarcăm de asemenea că această interpretare este evident un model al teoriei egalității. Deci, conform propoziției 3.3.3, I căruia I se adaugă relația identitate este un model al lui comp(P) {(A1 … Aq)}.

Cctd.

Corolar: Fie P un program definit și A BP. Dacă A este o consecință logică a lui comp(P) atunci A FP.

Modelul construit în demonstrația teoremei 3.5.1 nu este un model Herbrand. Exemplul următor arată că teorema 3.3.1 nu poate fi demonstrată limitându-ne la modelele Herbrand.

Exemplu: Considerăm programul P:

p(f(y)) p(y)

q(a) p(y)

Evidențiem că q(a) FP. În plus hfp(TP) = și în consecință q(a) hfp(TP). Conform propoziției 3.3.4, comp(P) {q(a)} nu posedă nici un model Herbrand.

Teorema 3.5.1 se generalizează programelor normale stratifiabile. Totuși această generalizare nu este chiar un rezultat al completitudinii, deoarece, după cum arată exemplul următor, existența unui arbore SLDNF (echitabil) nu este garantată, ca în cazul dfefinit, unde arborii SLD echitabili există întotdeauna. Pentru a obține un rezultat al completitudinii pentru programele normale stratifiabile, va fi deci necesar să impunem restricții suplimentare pentru a asigura existența unui arbore SLDNF echitabil.

Exemplu: Fie programul normal stratifiabil P:

q r

r p

r r

p p

Este ușor de arătat că q este o consecință logică a lui comp(P) dar că P {q} nu are nici un arbore SLDNF.

În ceea ce urmează vom aborda problema completitudinii rezoluției SLDNF.

Exemplu: Fie programul:

p(x)

q(a)

r(b)

și scopul p(x), q(x). Este evident că x / b este un răspuns corect. Totuși nu se poate calcula acest răspuns, nici măcar o versiune mai generală a lui.

Acest exemplu simplu ilustrează una din problemele pe care le avem pentru a obține un rezultat de completitudine pentru rezoluția SLDNF. Rezoluția SLD întoarce răspunsurile foarte generale. În exemplul de mai sus, ea va întoarce substituția identitate pentru subscopul p(x). Ceea ce dorim este ca regula de negație prin eșec să instanțieze mai departe pe x prin legătura x / b și să calculăm astfel răspunsul corect. Totuși, negația prin eșec este numai un test și nu poate face nici o legătură. În afara cazului în care este aplicată unui scop care este deja rădăcina unui arbore SLD de eșecuri finite, ea nu are nici un mecanism pentru a instanția mai departe scopul astfel încât să se obțină un astfel de arbore. În exemplul de mai sus, q(x) nu este rădăcina unui arbore SLD de eșecuri finite și negația prin eșec nu are nici un mijloc de a găsi legătura x / b.

Exemplul următor ilustrează o altă problemă care se pune pentru a obține completitudinea rezoluției SLDNF.

Exemplu: Fie programul normal P:

r p

r p

p p

Atunci substituția identitate este un răspuns corect pentru comp(P) {r}, dar el nu poate fi calculat.

Acest exemplu arată că pentru a obține un rezultat al completitudinii, va fi necesar să se impună restricții foarte tari. Vom arăta că pentru programele ierarhice, există un rezultat al completitudinii. Din nefericire acest rezultat nu este foarte util deoarece condiția de ierarhie interzice orice recursie pentru a stabili acest rezultat, trebuie să se generalizeze conceptul de regulă de evaluare.

Definiția 3.5.1: O regulă de evaluare sigură este o funcție definită pe o mulțime de scopuri normale (a cărei elemente nu sunt constituite doar din literali negativi neînchiși) cu valori într-o mulțime de literali, astfel încât valoarea funcției pentru un astfel de scop este fie un literal pozitiv, fie un literal negativ închis, numai literal ales, în acest scop.

Definiția 3.5.2: Fie P un program normal, G un scop normal și R o regulă de evaluare sigură.

O derivație SLDNF a lui P {G} prin R este o derivație SLDNF a lui P {G} în care se utilizează regula de evaluare R pentru a alege literali.

Un arbore SLDNF pentru P {G} prin R este un arbore SLDNF pentru P {G} în care se utilizează regula de evaluare R pentru a alege literali.

O refutație SLDNF a lui P {G} prin R este o refutație SLDNF a lui P {G} în care se utilizează regula de evaluare R pentru a alege literali.

Un răspuns R calculat pentru P {G} este un răspuns calculat pentru P {G} care provine dintr-o refutație SLDNF a lui P {G} prin R.

Teorema 3.5.2 (completitudinea rezoluției SLDNF pentru programe ierarhice): Fie P un program ierarhic normal, G un scop normal și R o regulă de evaluare sigură. Presupunem că P {G} este autorizat. Atunci:

Arborele SLDNF pentru P {G} prin R există și este finit

Dacă este un răspuns corect pentru comp(P) {G} și este o substituție închisă pentru toate variabilele lui G, atunci este un răspuns R – calculat pentru P {G}.

Demonstrație: a) Conform propoziției 3.4.1 a), calculul lui P {G} prin R nu se blochează.

Pentru a arăta că nu există derivații infinite, se folosesc mulțimi (multi – ensembles? ). Dacă M și M` sunt multi – mulțimi finite de întregi pozitivi, avem că M`<M dacă M` poate fi obținut plecând de la M înlocuind unul sau mai multe elemente ale lui M printr-un număr finit de întregi fiecare fiind inferior unui element înlocuit. Mulțimea tuturor multi – mulțimilor finite de întregi pozitivi indusă de relația < este o mulțime bine fondată. Considerăm acum mulțimea nivelelor de simboluri de predicate ce se găsesc în literali din corpul unui scop G prin scop al unei derivații SLDNF prin R. Deoarece P este ierarhic, fiul scopului G are o multi – mulțime mai mică decât G`. Nu există deci derivații infinite.

În plus, un argument de indicație după nivelele simbolurilor de predicate ne arată că arborele SLDNF pentru P {G} prin R într-adevăr există.

Remarcăm că, prin corolarul teoremei 3.3.6, comp(P) este consistent deoarece P este ierarhic. Fie G scopul L1, … ,Ln. Arborele SLDNF pentru P {G} prin R nu este un arbore de eșecuri finite, căci, în caz contrar, conform teoremei 3.4.1, ( L1 … Ln) ar fi o consecință logică a lui comp(P) ce ar contrazice consecința lui comp(P) și ipoteza că este corect.

Deci există o refutație SLDNF pentru P {G} prin R. Vom modifica alegerea literalilor de cel mai mare nivel ai acestei refutații astfel încât prima parte a acestei refutații să conțină scopurile în care literalul ales este negativ. Putem atunci aplica argumentul lemei 2.3.2, faptul că este o substituție închisă pentru toate variabilele lui G și faptul că P {G} este autorizată pentru a obține o refutație SLDNF a lui P {G} în care răspunsul calculat este .

Se aplică apoi argumentul lemei 2.4.1 astfel încât alegerea literalilor în vârful refutației se face folosind R. Deoarece nici un arbore de eșecuri finite subsidiar nu este modificat prin aceste construcții, literalii lui sunt cei aleși utilizând R. Astfel este un răspuns R – calculat pentru P {G}.

Cctd.

Rezumăm în final rezulatele principale stabilite pentru programele definite în acest capitol. Trebuie mai întâi să dăm o definiție suplimentară. Regula lui Herbrand este definită astfel: dacă comp(P) {A} nu are modele Herbrand atunci se deduce A.

Există deci trei reguli posibile pentru a deduce informația negativă: CWA, regula lui Herbrand și regula de negație prin eșec. Dacă P este un program definit, avem următoarele rezulate ilustrate în figură:

BP

TP

Hfp(TP) A este

A este dedusă prin TP dedusă

regula de negație prin CWA

prin eșec

A este

dedusă prin

regula lui Herbrand.

Deci:

{A BP / A poate fi dedusă prin regula de negație prin eșec} = BP \ TP.

{A BP / A poate fi dedusă prin regula lui Herbrand} = BP \ hfp(TP)

{A BP / A poate fi dedusă prin CWA} = BP \ hfp(TP).

Deoarece Tp hfp(TP) TP, rezultă că CWA este cea mai puternică regulă, urmată de regula lui Herbrand și regula negației prin eșec. Din faptul că Tp, hfp(Tp) și Tp sunt general distincte, rezultă că cele trei reguli sunt distincte.

Se poate combina teorema 3.2.1 și corolarele teoremelor 3.4.1 și 3.5.1 obținându-se un nou rezultat.

Teorema 3.5.3: Fie P un program definit și ABP. atunci condițiile următoare sunt echivalente:

A FP

A TP

A se află în mulțimea eșecurilor SLD finite

Orice arbore SLD echitabil pentru P {A} este un arbore de eșecuri finite

A este o consecință logică a lui comp(P).

Putem de asemenea combina teoremele 3.4.1 și 3.5.1.

Teorema 3.5.4: Fie P un program definit și G un scop definit. Atunci G este o consecință a lui comp(P) dacă și numai dacă P {G} are un arbore SLD de eșecuri finite.

Subliniem în final proprietățile care arată diferența între modelele (arbitrare) și modelele Herbrand ale lui comp(P) și între TP și hfp(TP). Fie ABP. Sunt adevărate:

Ahfp(TP) dacă și numai dacă comp(P) {A} are un model Herbrand

ATP dacă și numai dacă comp(P) {A} are un model.

PUNCTE FIXE

Tuturor programelor definite li se asociază o aplicație monotonă care joacă un rol foarte important în teorie.

Dacă S este o mulțime, o relație R pe S este o submulțime a produsului cartezian SS. Se utilizează în general notația xRy pentru (x,y)R.

O relație R pe mulțimea S este o relație de ordine parțială dacă sunt îndeplinite condițiile:

xRy, xS

xRy și yRx implică x=y, , x, yS

xRy și yRz implica xRz, , x, y,zS

De exemplu pentru o mulțime S fie 2S mulțimea părților sale. Atunci incluziunea mulțimilor: „” este o relație de ordine parțială pe 2S.

Se adoptă notația standard „” pentru o relație de ordine parțială pe 2S.

Fie S o mulțime și o relație de ordine parțială pe ea: . Atunci aS este un majorant al unei submulțimi X a lui S dacă ya pentru yX. Analog bS este un minorant al lui X dacă by pentru yX.

Fie S o mulțime și o relație de ordine parțială pe ea. Atunci aS este marginea superioară a unei submulțimi X a lui S (notată sup(X)) dacă a este un majorant al lui X și pentru toți majoranții a` ai lui X, avem aa`. Analog, bS este marginea inferioară a unei submulțimi X a lui S (notată inf(X)) dacă b este un minorant al lui X și pentru toți majoranții b` ai lui X, avem b`b.

O mulțime parțial ordonată L este o latice completă dacă sup(X) și inf(X) există, pentru toate submulțimile X ale lui L.

Notăm cu T cel mai mare element sup(L) și cu cel mai mic element inf(L) al laticii complete L.

În exemplul precedent, 2S este o latice completă.

Marginea superioară a unei familii de submulțimi ale lui S este reuniunea lor iar marginea inferioară a lor este intersecția. Cel mai mare element este S iar cel mai mic element este .

Definiție: Fie L o latice completă și T : L L o aplicație. Spunem că T este monoton dacă T(x)T(y) pentru xy.

Definiție: Fie L o latice completă și X o submulțime a sa. Spunem că X este (dirige`) dacă toate submulțimile finite ale lui X au o margine superioară în X.

Definiție: Fie L o latice completă și T : L L o aplicație. Spunem că T este continuu dacă T(sup(X)) = sup(T(X)) pentru toate subansamblele (dirige`) X ale lui L.

Interesul acestor definiții vine din faptul că pentru un program definit P, familia interpretărilor Herbrand formează o latice completă și deasemenea din acela că există o aplicație continuă asociată lui P. Să studiem acum punctele fixe ale aplicațiilor definite pe latice.

Definiție: Fie L o latice completă și T : L L o aplicație. Spunem că aL este cel mai mic punct fix al lui T dacă a este un punct fix (adică T(a)=a) și pentru toate punctele fixe b ale lui T, avem ab. Analog putem defini cel mai mare punct fix al lui T.

Teoremă: Fie L o latice completă și T : L L o aplicație monotonă. Atunci T are un cel mai mic punct fix (lfp(T)) și un cel mai mare punct fix (hlp(T)). În plus lfp(T) = inf{x / T(x)=x} = inf{x / T(x)x} și lfp(T) = sup{x / T(x)=x} = sup{x / T(x)x}.

Demonstrație: Fie G={ x / T(x)x } și g=inf(G). vom arăta că gG. deoarece gx pentru orice xG, prin monotonia lui T avem că T(g)T(x) pentru toți xG. deci T(g)<x pentru orice xG și prin urmare T(g)g prin definiția marginii inferioare. Deci gG.

Arătăm acum că g este un punct fix al lui T. Aceasta revine la a arăta că gT(g).

T(g)g implică T(T(g))T(g), implică T(g)G. Deci gT(g), în același fel în care g este punct fix al lui T.

Fie g`=inf{ x / T(x)=x }. Cum g este punct fix, avem g`g. Pe de altă parte { x / T(x)=x } { x / T(x)x } și avem deci gg`. Deci g=g`. Ceea ce trebuia demonstrat pentru cel mai mic punct fix: lfp(T), a fost demonstrat. Analog se realizează demonstrația pentru hlp(T).

Propoziție: Fie L o latice completă și T : L L o aplicație monotonă. Presupunând că aL și aT(a), atunci există un punct fix a` al lui T pentru care aa`. Analog, dacă bL și T(b)b, atunci există un punct fix b` al lui T pentru care b`b.

Demonstrație: în teorema precedentă este suficient de a considera a`=hlp(T) și b`=lfp(T).

În rezultatele ce le vom stabili în continuare, avem nevoie de conceptul de putere ordinală al lui T. Să amintim pentru început proprietățile elementare ale numerelor ordinale, pe care le vom numi simplu, ordinale. Intuitiv, ordinalele sunt numerele cu care de obicei lucrăm. Primul ordinal 0 este definit ca . În continuare definim: 1={}={0}, 2={, {}}={0, 1}, 3={, {}, {, {}}}={0,1,2} și așa mai departe. Există ordinale finite: întregii pozitivi. Primul ordinal infinit este ={0, 1, 2, …}, mulțimea întregilor pozitivi. S-a convenit să se noteze ordinalele finite prin litere romane: n, m, … și ordinalele arbitrare prin litere grecești: , , …

Se poate defini o relație de ordine “” pe mulțimea tuturor terminalelor astfel: dacă . De exemplu, n pentru toate ordinalele finite n. se scrie de obicei n în loc de n.

Dacă este un ordinal, succesorul lui este ordinalul +1={}, care este cel mai mic ordinal mai mare ca . De exemplu, 1=0+1, 2=1+1, 3=2+1 și așa mai departe.

Dacă este un ordinal succesor, fie =+1, notăm =-1. Un ordinal este numit ordinal limită dacă nu este succesorul nici unui ordinal. Cel mai mic ordinal limită (altul decât 0) este . După vine +1={}, +2=(+1)+1, +3, și așa mai departe. Ordinalul limită următor este 2 care este formată din toate ordinalele n și toate ordinalele +n, unde n. După acesta urmează 2+1, 2+2, … , 3, …

Principiul inducției transfinite se descrie astfel: fie P() o proprietate a ordinalelor. Presupunând că pentru un ordinal , dacă P() este adevărată pentru toți , atunci P() este adevărată, putem atunci să deducem că P() este adevărată pentru toate ordinalele .

Definiție: Fie L o latice completă și T : L L o aplicație monotonă. Atunci se definesc puterile ordinale ale lui T astfel:

T0 = 1

T = T(T(-1)) dacă este un ordinal succesor

T = sup{ T / } dacă este un ordinal limită și T0=T

T = T(T(-1)) dacă este un ordinal succesor

T = inf { T / } dacă este un ordinal limită

Propoziție: Fie L o latice completă și T : L L o aplicație monotonă. Atunci pentru toate ordinalele , T lfp(T) și T hfp(T). În plus există două ordinale 1 și 2 astfel încât 11 implică T1=lfp(T) și 22 implică T2=hfp(T).

Demonstrație: Demonstrația pentru lfp(T) decurge din punctele (a) și (e) prezentate mai jos. Demonstrațiile de la punctele (a), (b) și (c) folosesc inducția transfinită.

Demonstrăm că T lfp(T) pentru toți :

Dacă este un ordinal limită, atunci T = sup{ T / } lfp(T) prin ipoteza inducției transfinite. Dacă este un ordinal succesor atunci T=T(T(-1)) T(lfp(T))=lfp(T), prin ipoteza inducției, monotonia lui T și proprietatea punctului fix.

Demonstrăm că pentru toți , T T(+1):

Dacă este un ordinal succesor atunci T = T(T(-1)) T(T) = T(+1) prin ipoteza inducției și monotonia lui T. Dacă este un ordinal limită, atunci T = sup{ T / } sup{ T(+1) / } T(sup{T / })= T(+1), utilizând ipoteza inducției și monotonia lui T.

(c) Demonstrăm că pentru toți , , implică T T:

Dacă este un ordinal limită, atunci T = sup{ T / } = T. Dacă este un ordinal succesor, atunci (-1) și deci T T(-1) T, utilizând ipoteza inducției și (b).

Demonstrăm că pentru toți , , dacă și T = T atunci T = lfp(T):

Acum T T(+1) T, din (c). Deci T = T(T(+1)) = T(T) și deci T este un punct fix. În plus T = lfp(T) utilizând (a).

Demonstrăm că există astfel încât implică T = lfp(T):

Fie cel mai mic ordinal al cărui cardinal este mai mare decât al lui L. Presupunem că T lfp(T), pentru toți . Se definește h : L, prin h() = T. Atunci din (b) rezultă că h este injectivă, ceea ce contrazice alegerea lui . Astfel, T = lfp(T) pentru un și rezultatul decurge din (a) și (c).

Demonstrația pentru hfp(T) este analoagă.

Ctd.

Cel mai mic pentru care T = lfp(T) este numit ordinalul închideri lui T. Rezultatul următor arată că dacă presupunem în plus că T este continuu, ordinalul închideri lui T este .

Propoziție: Fie L o latice completă și T : L L o aplicație continuă. Atunci lfp(T) = T.

Demonstrație: Folosind propoziția (anterioară) este suficient să arătăm că T este un punct fix.

Avem că T(T) = T(sup{ Tn / n}) = sup{Tn / n} = T, utilizând continuitatea lui.

Ctd.

Analogia acestei propoziții pentru cel mai mare punct fix (hfp(T)) nu este adevărată, adică hfp(T) poate să nu fie egal cu T.

CAPITOLUL 2

PROGRAME DEFINITE

2.1 SEMANTICA DECLARATIVĂ

Acest paragraf se referă la cel mai mic model Herbrand al unui program definit. Acest model particular joacă un rol important în teorie. Vom arăta că cel mai mic model Herbrand este exact mulțimea atomilor închiși care constituie consecințe logice ale programului definit. Se va obține și o caracterizare importantă a celui mai mic model Herbrand ca punct fix. În final se va defini și conceptul de cheie (cle`) a unui răspuns corect.

Propoziție 2.1.1 (proprietatea intersecțieie modelelor):

Fie P un program definit și (Mi)iI o mulțime nevidă de modele Herbrand ale lui P. Atunci iIMi este un model Herbrand al lui P.

Demonstrație: iIMi este evident o interpretare Herbrand pentru P. Vom arăta că iIMi este un model al lui P.

P este un program definit. Fie AB1,…,Bn o regulă oarecare a lui P. Presupunem prin absurd că () o soluție cu proprietatea că {B1,…,Bn}iIMi și AiIMi {B1,…,Bn}Mi, iI AMi este model Herbrand al lui P. Deci AiIMi, presupunerea fiind falsă. În concluzie iIMi este un model Herbrand al lui P.

Cctd.

Deoarece toate programele definite P, admit BP (baza Herbrand) ca modele Herbrand, mulțimea tuturor modelelor Herbrand ale lui P este nevidă. Astfel intersecția tuturor modelelor Herbrand ale lui P este încă un model al lui P, numit cel mai mic model Herbrand. Îl vom nota MP.

Teorema următoare arată că atomii din MP sunt consecințele logice ale programului. Acest rezultat a fost stabilit de Van Endem și Kowalski.

Teorema 2.1.1: Fie P un program definit. Atunci:

MP = {ABP / A este o consecință logică a lui P}.

Demonstratie: Fie A o consecință logică a lui P. Folosind proprietățile prezentate anterior în capitolul 1, avem că P{A} este insatisfiabilă. Deci P{A} nu are modele Herbrand, ceea ce înseamnă că A este falsă în toate modelele Herbrand ale lui P. În concluzie A este adevărată în toate modelele Herbrand ale lui P, echivalent cu AMP.

Cctd.

Se dorește o caracterizare a celui mai mic model Herbrand al unui program utilizându-se conceptul de punct fix. Pentru acesta trebuie să asociem fiecărui program o latice completă.

Fie P un program definit. Atunci 2BP, care este mulțimea tuturor interpretărilor Herbrand ale lui P, este o latice completă împreună cu relația de ordine parțială a incluziunii mulțimilor: c. Cel mai mare element al acestei latice este BP și cel mai mic element, . Marginea superioară a unei mulțimi de interpretări Herbrand este reuniunea tuturor interpretărilor Herbrand din această mulțime. Marginea inferioară a acesteia o reprezintă intersecția lor.

Definiția 2.1.1: Fie P un program definit. Aplicația T : 2BP 2BP se definește astfel: Fie I o interpretare Herbrand. Atunci:

TP(I) = {ABP / AA1, … , An este o instanță fără variabile a unei clauze a lui P și {A1, … , An} I}

Evident operatorul TP este monoton. TP furnizează legătura între semantica declarativă și semantica procedurală a lui P.

Exemplu: Fie programul P:

p(f(x)) p(x);

q(a) p(x)

și interpretările: I1=BP, I2=TP(I1), I3=.

Atunci: TP(I1)={q(a)} {p(f(t)) / tUP}

TP(I2)={q(a)} {p(f(f(t))) / tUP}

TP(I3)=.

Propoziția 2.1.2: Fie P un program definit. Atunci aplicația TP este continuă.

Demonstrație: Fie X o partiție (dirige`e) a lui 2BP. Observăm că {A1, … , An} sup (X) dacă și numai dacă există IX astfel încâ {A1, … , An} I. Pentru a arăta că TP este continuu trebuie să arătăm că TP(sup(X)) = sup(TP(X)) pentru toate submulțimile (dirige`e) X.

Fie ATP(sup(X)).

AA1, … , An este o instanță fără variabile a unei clauze a lui P și {A1, … , An} sup(X).

AA1, … , An este o instanță fără variabile a unei clauze a lui P și {A1, … , An} I pentru un I X.

ATP(I) pentru IX.

Asup(TP(X))

cctd.

Interpretările Herbrand care sunt modele pot fi caracterizate prin aplicația TP.

Propoziția 2.1.3: Fie P un program definit și I o interpretare Herbrand a lui P. Atunci I este un model al lui P decă și numai dacă TP(I) I.

Demonstrație: I este un model al lui P dacă și numai dacă pentru fiecare instanță fără variabile AA1, … , An a fiecărei clauze a lui P, {A1, … , An} I implică AI, adică dacă și numai dacă TP(I) I.

Cctd.

Se ajunge acum la rezulzazul principal al teoriei. Următoarea teoremă, dată de Van Emden și Kowalski, furnizează o caracterizare în termeni de punct fix a celui mai mic model herbrand al unui program definit.

Teorema 2.1.2: Fie P un program definit. Atunci MP=lfp(TP)=TP.

Demonstrație: MP = inf{I / I este un model Herbrand al lui P}

= inf {I / TP(I) I}

= lfp(TP)

= TP

cctd.

Se poate demonstra însă că hfp(TP) TP.

Exemplu: Fie programul P:

p(f(x)) p(x);

q(a) p(x)

Atunci TP = {q(a)}, dar hfp(TP) = . De fapt hfp(TP) = TP(+1).

Definiție 2.1.2: Fie P un program definit și G un scop definit. Un răspuns pentru P{G} este o substituție pentru variabilele lui G.

Este evident că răspunsul nu conține obligatoriu o legătură pentru fiecare variabilă din G. În particular, dacă G nu are variabile, singurul răspuns posibil este substituția identică.

Definiția 2.1.3: Fie P un program definit, G scopul definit A1,…,Ak și un răspuns pentru P{G} dacă ()((A1…Ak)) este o consecință logică a lui P.

Se observă că, folosind rezultatele stabilite anterior, este un răspuns corect dacă și numai dacă P{ ((A1…Ak)) } este insatisfiabilă. Definiția prezentată mai sus a unui răspuns corect, redă bine semnificația intuitivă a acestui concept. Ea furnizează o descriere declarativă a ceea ce vrea a se obține plecând de la un program definit și de la un scop. Se va arăta în continuare echivalența între acest concept declarartiv și conceptul procedural corespondent, care este definit prin procedura de refutație definită de sistem.

În același mod cum returnează substituții un sistem de programare logică poate returna și răspunsul “nu”. Spunem că răspunsul “nu” este “corect” dacă P{G} este satisfiabilă.

Teorema 2.1.1 și definiția unui răspuns corect sugerează ideea de a generaliza această teoremă, adică un răspuns este corect dacă și numai dacă ((A1…Ak)) este adevărată în cel mai mic model Herbrand al programului. Acest rezultat însă nu este în general corect, după cum arată exemplul următor.

Exemplu: Fie programul P: p(a). Fie G scopul p(x) și substituția identică. Atunci MP={p(a)} și xp(x) este adevărată în MP. Totuși nu este un răspuns corect deoarece xp(x) nu este o consecință logică a lui P. Știim că xp(x) nu este o clauză și deci nu se poate stabili insatisfiabilitatea lui {p(a)}{ xp(x)}. Totuși dacă se face o restricție asupra substituției se poate obține un rezulatat care generalizează teorema 2.1.

Teorema 2.1.3: Fie P un program definit și G un scop definit A1,…,Ak.Fie un răspuns pentru P{G} astfel încât (A1…Ak) este închisă. Atunci următoarele afirmații sunt echivalente:

este un răspuns corect

(A1…Ak) este adevărată în toate modelele Herbrand ale lui P

(A1…Ak) este adevărată în cel mai mic model Herbrand al lui P

Demonstrație: Este evident că demonstrația se reduce la a demonstra că c) implică a).

Dar: (A1…Ak) este adevărată în cel mai mic model herbrand al lui P

(A1…Ak) este adevărată în toate modelele Herbrand ale lui P

(A1…Ak) este falsă în toate modelele Herbrand ale lui p

P{(A1…Ak)} nu are modele Herbrand

P{(A1…Ak)} nu are modele.

Cctd.

2.2 CORECTITUDINEA REZOLUȚIEI SLD

În cele ce urmează se va introduce conceptul de semantică procedurală a programelor definite. Se vor defini răspunsurile calculate și se va stabili corectitudinea rezoluției SLD. Se vor evidenția de asemenea consecințele omiterii verificării ocurențelor în algoritmul de unificare.

Definiția 2.2.1: Fie G scopul A1,…,Am, … ,Ak și C clauza AB1, … ,Bq. Atunci G` derivă din G și C, utilizând un cel mai general unificator , dacă următoarele condiții sunt verificate:

Am este un atom, numit atom „ales”, în G

este un cel mai general unificator al lui Am și A

G` este scopul (A1, …, Am-1, B1, … , Bq, Am+1, … , Ak).

În terminologia rezoluției, G` se numește o rezolvantă a lui G și C.

Definiția 2.2.2: Fie P un program definit și G un scop definit. O derivare SLD a lui P{G} constă într-un șir (finit sau inifinit) G0=G, G1, … de scopuri, un șir C1, C2, … de variante de clauze ale programului P și un șir 1, 2, … de cei mai generali unificatori astfel încât Gi+1 derivă din Gi și Ci+1 utilizând I+1.

Fiecare Ci este o variantă adaptată a unei clauze corespunzătoare a programului astfel încât Ci nu are nici o variabilă care să fi apărut deja în derivația din Gi-1. Aceasta se poate obține de exemplu, indiciind variabilele din G cu 0 și variabilele Ci cu i. Acest procedeu de redenumire a variabilelor este cunoscut sub numele de standardizarea variabilelor separate. Procedeul este necesar deoarece, de exemplu, nu s-ar putea unifica p(x) și p(f(x)) în p(x) și p(f(x)). Fiecare variantă a clauzei din program C1, C2, … este numită clauză de intrare a derivației.

Definiția 2.2.3: O refutație SLD a lui P{G} este o derivație SLD finită a lui P{G} care are clauza vidă (notată ) ca ultim scop al derivării. Dacă Gn=, spunem că refutația are lungimea n.

Vom numi în cele ce urmează, pentru simplificare, o derivație SLD, simplu – derivare și o refutație SLD simplu – refutație.

Putem reprezenta o derivație SLD astfel:

G0=G C1, 1

G1 C2, 2

G2

.

.

.

Definiția 2.2.4: O refutație SLD fără restricții este o refutație SLD în care substituțiile i nu sunt neapărat cei mai generali unificatori ci sunt doar unificatori.

Derivațiile SLD pot fi finite sau infinite, reușite sau nereușite. O derivație SLD reușită este o derivație care se termină cu clauza vidă. Altfel spus o derivație reușită este o refutație. O derivație SLD care „nu reușește” este o derivație ce se încheie cu un scop nevid astfel încât atomul ales în acest scop nu se unifică cu capul nici unei clauze a programului.

Definiția 2.2.5: Fie P un program definit. „Mulțimea succeselor” programului P este mulțimea tuturor atomilor ABP pentru care P{A} are o refutație SLD.

Mulțimea succeselor reprezintă analogul procedural al celui mai mic model Herbrand. Într-un mod asemănător se definește corespondentul procedural al unui răspuns corect.

Definiția 2.2.6: Fie P un program definit și G un scop definit. Un răspuns calculat pentru P{G} este substituția obținută restrângând compunerea 1…n variabilelor lui G, unde 1, … , n este șirul celor mai generali unificatori utilizați într-o refutație SLD a lui P{G}.

Teorema 2.2.1 (corectitudinea rezoluției SLD):

Fie P un program definit și G un scop definit. Atunci toate răspunsurile calculate pentru P{G} sunt răspunsuri corecte pentru P{G}.

Demonstrație: Fie G scopul A1,…,Ak și 1, … , n șirul celor mai generali unificatori folosiți într-o refutație a lui P{G}. Trebuie să arătăm că ((A1…Ak) 1…n) este o consecință logică a lui P. Acest rezultat îl vom demonstra prin inducție după lungimea refutației.

Presupunem că lungimea refutației este n=1. Deci G este un scop de forma A1, programul are o clauză unitară de forma A și A1 = A1. Deoarece A11 este o instanță a unei clauze unitare a lui P, este evident că (A11) este o consecință logică a lui P.

Presupunem acum rezultatul adevărat pentru răspunsuri calculate printr-o refutație de lungime n-1. presupunem că 1, … , n reprezintă șirul celor mai generali unificatori utilizați într-o refutație a lui P{G} de lungime n.

Fie AB1,…,Bq (q0) prima clauză de intrare și Am atomul als în G. Prin ipoteza de inducție, ( A1 … Am-1) B1 … Bq Am+1 … Ak)1… n) este o consecință logică a lui P. Astfel, dacă q>0, ((B1 … Bq)1… n) este o consecință logică a lui P (Am1… n) care este asemenea lui (A1… n) este o consecință logică a lui P. Deci, ((A1 … Ak) 1… n) este o consecință logică a lui P.

Cctd.

Corolar 1:

Fie A M1, … ,Mq (q0) prima clauză de intrare. Din ipoteza de inducție, ((L1 … Lm-1 M1 … Mq Lm+1 … Lk)1 … n) este o consecință logică a lui comp(P). Deci, dacă q>0, ((M1, … ,Mq)1 … n) este o consecință logică a lui comp(P). În consecință, (Lm1 … n) care este egal cu (A1 … n) este o consecință logică a lui comp(P). deci, ((L1 … Lk )1 … n) este o consecință logică a lui comp(P).

Lm este negativ.

În acest caz, Lm este închis, 1 este substituția identică și teorema anterioară arată că Lm este o consecință logică a lui comp(P). Utilizând ipoteza de inducție, se obține că ((L1 … Lk )1 … n) este o consecință logică a lui comp(P).

Cctd.

Vom examina în continuare dacă se poate „slăbi” condiția de securitate pusă asupra alegerii literalilor. Începem prin a arăta că fără această condiție, teorema 3.4.1 nu mai este adevărată.

Exemplu: Fie programul P:

p q(x)

q(a)

Dacă nu considerăm condiția de securitate, literalul q(x) poate fi ales și se obține un arbore SLDNF de eșecuri finite pentru P { p}. Subscopul q(x) eșuează deoarece există o refutație a lui q(x) în care x este legat la a. În același timp, este ușor de văzut că p nu este o consecință logică a lui comp(P).

Este posibil să slăbim puțin condiția de securitate și să obținem aceleași rezultate. Fie condiția de securitate următoare, mai slabă. Subscopurile negative care nu sunt închise sunt autorizate să funcționeze. Dacă subscopul negativ reușește, vom proceda ca în cazul anterior. Dacă acesta eșuează, se verifică dacă nici o legătură n-a fost făcută asupra variabileleor scopului de început al refutației corespunzătoare. Dacă nici o legătură nu a fost făcută, subscopul negativ este autorizat să eșueze și se procedează ca în cazul precedent. Dacă nu, se alege un literal diferit și subscopul negativ este pus în așteptare în speranța că mai multe din variabilele sale vor fi legate ulterior. Alternativ, o eroare de control ar putea fi generată și programul se oprște.

Punctul cheie în acest caz este faptul că refutația care face să eșueze subscopul negativ trebuie să demonstreze câteva lucruri de forma (A) mai degrabă de cât (A). Pentru această condiție de securitate mai slabă, teoremele 3.4.1 și 3.4.2 rămân adevărate. Singura schimbare a demonstrațiilor lor o găsim în demonstrația teoremei 3.4.1 în locul unde am folosit faptul că A este închisă.

Cel mai simplu mod de a implementa condiția de securitate într-un sistem de programare logică este de a diferenția (separa) scopurile negative până când toate variabilele ce apar în subsop să fie legate de termenii închiși. Din nefericire, marea majoritate a sistemelor PROLOG nu au un mecanism care să le permită să diferențieze subsopurile și nu pot deci să utilizeze această metodă. Și mai grav, marea majoritate a sistemelor PROLOG „nu își nu dau oboseala” să verifice dacă subscopurile apelate sunt închise. Aceasta poate să ducă la o situație mai degrabă ciudată.

Exemplu: Fie programul:

p(a)

q(b)

și scopul normal p(x), q(x). Dacă acest program și acest scop sunt executate pe un sistem PROLOG care utilizează regula de evaluare standard, și nu verifică dacă subscopurile apelate sunt închise, atunci va returna răspunsul „da”! Pe de altă parte, MU-PROLOG și NU-PROLOG diferă primul subscop, rezolvă cel de al doilea scop și apoi vor rezolva primul scop pentru a da răspunsul corect {x / b}. Bineînțeles, problema cu acest scop particular poate fi rezolvată de un sistem PROLOG standard, reordonând subsopurile scopului.

COMPLETITUDINEA REZOLUȚIEI SLDNF

În acest paragraf vom arăta rezultatele completitudinii pentru regula de negație prin eșec pentru programele definite și pentru rezoluțiile SLDNF ale programelor ierarhice. Vom face de asemena un rezumat al principalelor rezultate ale capitolului.

Teorema 3.5.1 (completitudinea regulii de negație prin eșec):

Fie P un program definit și G un scop definit. Dacă G este o consecință logică a lui comp(P), atunci orice arbore SLD echitabil pentru P {G} este un arbore de eșecuri finite.

Demonstrație: Fie G scopul A1, … ,Aq. Presupunem că P {G} are un arbore SLD echitabil care nu este un arbore de eșecuri finite. Arătăm că comp(P) {(A1 … Aq)} are un model.

Fie BR o ramură care nu este o ramură de eșecuri în arborele SLD. Presupunem că BR este: G0=G, G1, … cu șirul celor mai generali unificatori 1, 2, … și clauzele de intrare C1, C2, … . Prima etapă este de a utiliza BR pentru a defini o preinterpretare J pentru P.

Presupunem că L este limbajul de ordinul I (sous – jacent) lui P. Evident presupunem L suficient de bogat pentru a putea standardiza variabilele separate în BR. Dfefinim o relație * pe mulțimea tuturor termenilor din L astfel: fie s și t doi termeni din L. Atunci s*t dacă există nN astfel încât s1 … n=t1 … n, adică dacă 1 … n unifică s și t. Este evident că * este o relație de echivalență. Se definește atunci domeniul D al preinterpretărilor J ca mulțimea tuturor claselor de echivalență ale termenilor lui L prin relația *. Dacă s este un termen al lui L, notâm [S] clasa de echivalență pentru * conținând pe s.

Să dăm acum asignările constantelor și simbolurilor defuncții din L. Dacă c este o constantă a lui L, I se asignează [e]. Dacă f este un simbol de funcție n –ară din L, îi asignăm lui f aplicația definită pe Dn cu valori în D care lui ([s1], … ,[sn]) îi asociază [f(s1, … ,sn)]. Este evident că această aplicație este bine definită. Aceasta completează definiția lui J.

Rămâne a da asignările simbolurilor de predicate pentru a extinde J unei interpretări a lui comp(P) {(A1 … Aq)}. Începem prin a defini mulțimea I0 astfel:

I0={p([t1], … ,[tn]) / p(t1, … ,tn) apare în BR}.

Arătăm că I0 TJP(I0), unde TJP este aplicația asociată preinterpretării J. Presupunem că p([t1], … ,[tn]) I0, unde p(t1, … ,tn) apare în Gi, i. Deoarece BR este echitabil și nu este o ramură de eșec, există j astfel încât p(s1, … ,sn) = p(t1, … ,tn)I+1 … I+j apare în scopul Gi+j și p(s1, … ,sn) este atomul ales în Gi+j. Presupunem că Ci+j+1 este p(r1, … ,rn) B1,…,Bm. Prin definiția lui TJP rezultă că p([r1I+j+1], … ,[rnI-j-1]) TP(I0). Atunci utilizând faptul că pentru orice k se poate presupune 1 … k idempotent, avem că:

p([t1], … ,[tn]) = p([t1I+1 … I+j], … ,[tnI+1 … I+j],)

= p([s1], … ,[sn])

= p([s1I+j+1], … ,[snI-j-1])

= p([r1I+j+1], … ,[rnI-j-1])

astfel că p([t1], … ,[tn]) TJP(I0). Deci I0 TJP(I0).

Acum, conform propoziției 1.5.1, există I astfel încât I0 I și I = TJP(I). I dă asignările simbolurilor de predicate din L. Am asignat relația egalitate lui “=”.

Astfel se completează definiția interpretării I, căreia I se adaugă relația identitate asignată lui =, pentru comp(P) {(A1 … Aq)}. Remarcăm că această interpretare este un model al lui (A1 … Aq) căci I0 I. Remarcăm de asemenea că această interpretare este evident un model al teoriei egalității. Deci, conform propoziției 3.3.3, I căruia I se adaugă relația identitate este un model al lui comp(P) {(A1 … Aq)}.

Cctd.

Corolar: Fie P un program definit și A BP. Dacă A este o consecință logică a lui comp(P) atunci A FP.

Modelul construit în demonstrația teoremei 3.5.1 nu este un model Herbrand. Exemplul următor arată că teorema 3.3.1 nu poate fi demonstrată limitându-ne la modelele Herbrand.

Exemplu: Considerăm programul P:

p(f(y)) p(y)

q(a) p(y)

Evidențiem că q(a) FP. În plus hfp(TP) = și în consecință q(a) hfp(TP). Conform propoziției 3.3.4, comp(P) {q(a)} nu posedă nici un model Herbrand.

Teorema 3.5.1 se generalizează programelor normale stratifiabile. Totuși această generalizare nu este chiar un rezultat al completitudinii, deoarece, după cum arată exemplul următor, existența unui arbore SLDNF (echitabil) nu este garantată, ca în cazul dfefinit, unde arborii SLD echitabili există întotdeauna. Pentru a obține un rezultat al completitudinii pentru programele normale stratifiabile, va fi deci necesar să impunem restricții suplimentare pentru a asigura existența unui arbore SLDNF echitabil.

Exemplu: Fie programul normal stratifiabil P:

q r

r p

r r

p p

Este ușor de arătat că q este o consecință logică a lui comp(P) dar că P {q} nu are nici un arbore SLDNF.

În ceea ce urmează vom aborda problema completitudinii rezoluției SLDNF.

Exemplu: Fie programul:

p(x)

q(a)

r(b)

și scopul p(x), q(x). Este evident că x / b este un răspuns corect. Totuși nu se poate calcula acest răspuns, nici măcar o versiune mai generală a lui.

Acest exemplu simplu ilustrează una din problemele pe care le avem pentru a obține un rezultat de completitudine pentru rezoluția SLDNF. Rezoluția SLD întoarce răspunsurile foarte generale. În exemplul de mai sus, ea va întoarce substituția identitate pentru subscopul p(x). Ceea ce dorim este ca regula de negație prin eșec să instanțieze mai departe pe x prin legătura x / b și să calculăm astfel răspunsul corect. Totuși, negația prin eșec este numai un test și nu poate face nici o legătură. În afara cazului în care este aplicată unui scop care este deja rădăcina unui arbore SLD de eșecuri finite, ea nu are nici un mecanism pentru a instanția mai departe scopul astfel încât să se obțină un astfel de arbore. În exemplul de mai sus, q(x) nu este rădăcina unui arbore SLD de eșecuri finite și negația prin eșec nu are nici un mijloc de a găsi legătura x / b.

Exemplul următor ilustrează o altă problemă care se pune pentru a obține completitudinea rezoluției SLDNF.

Exemplu: Fie programul normal P:

r p

r p

p p

Atunci substituția identitate este un răspuns corect pentru comp(P) {r}, dar el nu poate fi calculat.

Acest exemplu arată că pentru a obține un rezultat al completitudinii, va fi necesar să se impună restricții foarte tari. Vom arăta că pentru programele ierarhice, există un rezultat al completitudinii. Din nefericire acest rezultat nu este foarte util deoarece condiția de ierarhie interzice orice recursie pentru a stabili acest rezultat, trebuie să se generalizeze conceptul de regulă de evaluare.

Definiția 3.5.1: O regulă de evaluare sigură este o funcție definită pe o mulțime de scopuri normale (a cărei elemente nu sunt constituite doar din literali negativi neînchiși) cu valori într-o mulțime de literali, astfel încât valoarea funcției pentru un astfel de scop este fie un literal pozitiv, fie un literal negativ închis, numai literal ales, în acest scop.

Definiția 3.5.2: Fie P un program normal, G un scop normal și R o regulă de evaluare sigură.

O derivație SLDNF a lui P {G} prin R este o derivație SLDNF a lui P {G} în care se utilizează regula de evaluare R pentru a alege literali.

Un arbore SLDNF pentru P {G} prin R este un arbore SLDNF pentru P {G} în care se utilizează regula de evaluare R pentru a alege literali.

O refutație SLDNF a lui P {G} prin R este o refutație SLDNF a lui P {G} în care se utilizează regula de evaluare R pentru a alege literali.

Un răspuns R calculat pentru P {G} este un răspuns calculat pentru P {G} care provine dintr-o refutație SLDNF a lui P {G} prin R.

Teorema 3.5.2 (completitudinea rezoluției SLDNF pentru programe ierarhice): Fie P un program ierarhic normal, G un scop normal și R o regulă de evaluare sigură. Presupunem că P {G} este autorizat. Atunci:

Arborele SLDNF pentru P {G} prin R există și este finit

Dacă este un răspuns corect pentru comp(P) {G} și este o substituție închisă pentru toate variabilele lui G, atunci este un răspuns R – calculat pentru P {G}.

Demonstrație: a) Conform propoziției 3.4.1 a), calculul lui P {G} prin R nu se blochează.

Pentru a arăta că nu există derivații infinite, se folosesc mulțimi (multi – ensembles? ). Dacă M și M` sunt multi – mulțimi finite de întregi pozitivi, avem că M`<M dacă M` poate fi obținut plecând de la M înlocuind unul sau mai multe elemente ale lui M printr-un număr finit de întregi fiecare fiind inferior unui element înlocuit. Mulțimea tuturor multi – mulțimilor finite de întregi pozitivi indusă de relația < este o mulțime bine fondată. Considerăm acum mulțimea nivelelor de simboluri de predicate ce se găsesc în literali din corpul unui scop G prin scop al unei derivații SLDNF prin R. Deoarece P este ierarhic, fiul scopului G are o multi – mulțime mai mică decât G`. Nu există deci derivații infinite.

În plus, un argument de indicație după nivelele simbolurilor de predicate ne arată că arborele SLDNF pentru P {G} prin R într-adevăr există.

Remarcăm că, prin corolarul teoremei 3.3.6, comp(P) este consistent deoarece P este ierarhic. Fie G scopul L1, … ,Ln. Arborele SLDNF pentru P {G} prin R nu este un arbore de eșecuri finite, căci, în caz contrar, conform teoremei 3.4.1, ( L1 … Ln) ar fi o consecință logică a lui comp(P) ce ar contrazice consecința lui comp(P) și ipoteza că este corect.

Deci există o refutație SLDNF pentru P {G} prin R. Vom modifica alegerea literalilor de cel mai mare nivel ai acestei refutații astfel încât prima parte a acestei refutații să conțină scopurile în care literalul ales este negativ. Putem atunci aplica argumentul lemei 2.3.2, faptul că este o substituție închisă pentru toate variabilele lui G și faptul că P {G} este autorizată pentru a obține o refutație SLDNF a lui P {G} în care răspunsul calculat este .

Se aplică apoi argumentul lemei 2.4.1 astfel încât alegerea literalilor în vârful refutației se face folosind R. Deoarece nici un arbore de eșecuri finite subsidiar nu este modificat prin aceste construcții, literalii lui sunt cei aleși utilizând R. Astfel este un răspuns R – calculat pentru P {G}.

Cctd.

Rezumăm în final rezulatele principale stabilite pentru programele definite în acest capitol. Trebuie mai întâi să dăm o definiție suplimentară. Regula lui Herbrand este definită astfel: dacă comp(P) {A} nu are modele Herbrand atunci se deduce A.

Există deci trei reguli posibile pentru a deduce informația negativă: CWA, regula lui Herbrand și regula de negație prin eșec. Dacă P este un program definit, avem următoarele rezulate ilustrate în figură:

BP

TP

Hfp(TP) A este

A este dedusă prin TP dedusă

regula de negație prin CWA

prin eșec

A este

dedusă prin

regula lui Herbrand.

Deci:

{A BP / A poate fi dedusă prin regula de negație prin eșec} = BP \ TP.

{A BP / A poate fi dedusă prin regula lui Herbrand} = BP \ hfp(TP)

{A BP / A poate fi dedusă prin CWA} = BP \ hfp(TP).

Deoarece Tp hfp(TP) TP, rezultă că CWA este cea mai puternică regulă, urmată de regula lui Herbrand și regula negației prin eșec. Din faptul că Tp, hfp(Tp) și Tp sunt general distincte, rezultă că cele trei reguli sunt distincte.

Se poate combina teorema 3.2.1 și corolarele teoremelor 3.4.1 și 3.5.1 obținându-se un nou rezultat.

Teorema 3.5.3: Fie P un program definit și ABP. atunci condițiile următoare sunt echivalente:

A FP

A TP

A se află în mulțimea eșecurilor SLD finite

Orice arbore SLD echitabil pentru P {A} este un arbore de eșecuri finite

A este o consecință logică a lui comp(P).

Putem de asemenea combina teoremele 3.4.1 și 3.5.1.

Teorema 3.5.4: Fie P un program definit și G un scop definit. Atunci G este o consecință a lui comp(P) dacă și numai dacă P {G} are un arbore SLD de eșecuri finite.

Subliniem în final proprietățile care arată diferența între modelele (arbitrare) și modelele Herbrand ale lui comp(P) și între TP și hfp(TP). Fie ABP. Sunt adevărate:

Ahfp(TP) dacă și numai dacă comp(P) {A} are un model Herbrand

ATP dacă și numai dacă comp(P) {A} are un model.