Nat_lambda: -Term λsx.x reprezentuje liczbę naturalną 0. -Term λsx.s(s(...(sx)...)) gdzie s występuje n razy reprezentuje liczbę naturalną n. Mówimy, że term E rachunku lambda reprezentuje funkcję na liczbach naturalnych e:N^k -> N wtw gdy En1 ....nk = e (n1,...,nk) , gdzie n oznacza reprezentację liczby n w rachunku lambda,SLD rezolucja: W prologu stosujemy: SLD-rezolucję,regułę selekcji „left first”, strategię przeszukiwania,drzewa „depth first”, niezmienny porządek klauzul w procedurach,prolog jako metoda dowodzenia twierdzeń nie jest pewny, tzn. nie spełnia twierdzenia o pełności.Left first – reguła selekcji, w której R() = 1, tzn. w danym celu wybierany jest zawsze podlec pierwszy z lewej.Depth first – strategia przeszukiwania drzewa – przeszukiwanie lewymi gałęziami; dla pewnych drzew strategia ta może nie doprowadzić do rozwiązania, ale jest łatwa w realizacji,reguły selekcji: Regułą selekcji nazywamy funkcję R, która każdej skończonej derywacji liniowej (Gn,Cn,σn), 1=<n=<p takiej, że Gp = □ przyporządkowuje liczbę naturalną 1=<n=<k, gdzie k jest długością celu Gk.Tw. o nieistotności reguł selekcji,Niezależnie od wyboru reguły selekcji otrzymamy te same odpowiedzi obliczone dla Pu{G} z dokładnością do wariantu, tzn. jeżeli R1 i R2 są regułami selekcji i σ1 jest odpowiedzią obliczoną dla Pu{G} zgodną z R1 i σ2 jest odpowiedzią obliczoną zgodną z R2, to Gσ1 i Gσ2 są swoimi wariantami,SLD drzewo: SLD-drzewo dla Pu{G} zgodne z R jest drzewem skończonym lub nieskończonym, którego wierzchołki etykietowane są celami i spełniającym następujące warunki:a) korzeń drzewa jest etykietowany celem G,b) dla dowolnego wierzchołka etykietowanego celem G’ następniki tego wierzchołka są etykietowane kolejnymi celami, które powstają z G’ przez uzgodnienie wybranego zgodnie z R atomu z kolejnymi klauzulami programu,a) gałęzie pełnego SLD-drzewa dla Pu{G} reprezentują wszystkie derywacje dla Pu{G} zgodne z R, przy czym: gałęzie nieskończone reprezentują nieskończoną derywację (procedura się pętli), gałęzie skończone to: gałęzie udane (sukcesu), gałęzie chybione (porażki),
Posser: Jeżeli term M poprzez pewne ciągi β-redukcji redukuje się do termów N1 i N2 , to istnieje term M’ taki, że zarówno N1 jak i N2 można zredukować do M’ (poprzez ciągi β-redukcji). Term T jest normalizowalny, jeżeli można go zredukować do postaci normalnej, a jest silnie normalizowalny, jeżeli każda droga redukcji prowadzi do postaci normalnej,Beta: β-redukcja –obliczenia wykonywane przez procedurę symulowane są w rachunku lambda poprzez proces zwany β-redukcją. Aplikujemy procedurę Lambdax.M do argumentu N: (Lambdax.M)N->M[x/ N] w taki sposób, że każda zmienna wolna termu N pozostaje wolna po podstawieniu. Jest to możliwe do osiągnięcia po ewentualnym wcześniejszym zastosowaniu α-konwersji. Używamy oznaczenia T1=β T2 , aby powiedzieć, że termy T1 i T2 są równe modulo β-konwersja tzn. że mogą być zredukowane do tego samego termu dzięki zastosowaniu skończonej liczby β-konwersji. Aplikację PQ nazywamy β-redeksem, jeżeli term P jest w postaci λ-abstrakcji. Term M jest w postaci normalnej, jeżeli nie zawiera β-redeksów tzn. żaden podterm termu M nie jest Β-redeksem, α: α-konwersja to zamiana nazw zmiennych związanych Lambdax.M->α Lambday.M[x/y] ,gdzie y nienalezy FV(M) , a M[x/y] oznacza wynik podstawienia zmiennej y za każde wolne wystąpienie zmiennej x w termie M. Będziemy używać oznaczenia T1=αT2 , aby powiedzieć, że termy T1 i T2 są równe modulo α-konwersja tzn. że mogą być zredukowane do tego samego termu dzięki zastosowaniu skończonej liczby α-konwersji, retutacja lin: Liniową refutacją dla Pu{G} nazywamy skończoną liniową derywację dla Pu{G}, której ostatni cel jest klauzulą pustą.Niech G(n)C(n)a(n),1=<n=<p , będzie liniową refutacją dla Pu{G}. Odpowiedzią obliczoną dla Pu{G} wyznaczoną przez tę refutację nazywamy podstawienie α1- αn ograniczone do zmiennych występujących w G. tzn. α1- αn |V(G)
rach_Lambd: Zbiór Λ termów rachunku lambda konstrujue się indukcyjnie jako zbiór słów nad alfabetem Var u{(,),Lambda} gdzie Var jest przeliczalnym zbiorem zmiennych. Do zbioru Λ należą tylko termy skonstruowane w następujący sposób: -Dowolna zmienna ze zbioru Var jest termem rachunku lambda, czyli jeżeli xEVar , to xEΛ. -Jeżeli weźmiemy dowolny term M ze zbioru Λ oraz dowolną zmienną x ze zbioru Var, to wyrażenie postaci (Lambdax.M) jest termem rachunku lambda, czyli jeżeli MEΛ i xEVar , to (Lambdax.M)EΛ Powyższy sposób tworzenia termów nazywamy abstrakcją. -Inna metoda to metoda aplikacji, czyli jeżeli MEΛ i NEΛ, to (MN)EΛ. Wolnym wystąpieniem zmiennej x nazywamy tylko takie wystąpienie tej zmiennej, które nie jest w zasięgu żadnego Lambdax . Zbiór zmiennych wolnych termu M-oznaczany przez FV(M) zdefiniowany jest w zależności od budowy termu M w następujący sposób: -Jeżeli M jest pojedynczą zmienną tzn. M=x, to zmienna ta jest wolna, a zatem FV(M)={x}. -Jeżeli M jest postaci Lambdax.M' , to Lambdax wiąże wszystkie wolne wystąpienia zmiennej x w termie M’, a zatem FV(M)=FV(M’)-{x}. -Jeżeli M jest postaci PQ, to zmiennymi wolnymi termu M są wszystkie zmienne wolne występujące w termach P i Q, czyli FV(M)=FV(P)u FV(Q). Zmienna jest zmienną wolną termu M, jeżeli należy do zbioru FV(M), a zmienną związaną w przeciwnym wypadku. Term M jest domknięty wtw gdy FV(M) jest zbiorem pustym, ,rezolucja lin: Def. Reguła rezolucji liniowej Reguła rezolucji liniowej ma postać ←A1,…,Am,…,An – cel G B←B1,…,Bk – wariant klauzuli C program P ← (A1, ..., Am-1, B1, ..., Bk, Am+1, ..., An)s - nowy cel. gdzie s jest MGU zbioru {Am,B}, tzn: Ams =Bs Def. Derywacja liniowa Niech P będzie programem definitywnym, a G celem. Derywacja liniowa dla P ᴜ {G} nazywamy skończony lub nieskończony ciąg którego wyrazami są:(Gn,Cn,sn), 1<=n<=p lub 1<=n spełniający warunki: a) Dla każdego n, Cn jest wariantem klauzuli programu P nie zawierającym zmiennych występujących w G0,G1,…,Gn-1 b) Dla każdego n, Gn jest rezolwentą liniową celu Gn-1 oraz klauzuli Cn otrzymamy za pomocą podstawienia s
n,Prolog: Fakt 2.2 2 następujące warunki są równoważne:- formuła A wynika logicznie ze zbioru formuł Gw LPR- zbiór G ᴜ(¬A) nie jest spełnialny. Strategia Prologu:Niech P będzie programem definitywnym, a G-celemBierzemy pod uwagę zbiór P ᴜ {G} Jeżeli wykażemy, że zbiór P ᴜ {G} nie jest spełnialny, to na podstawie FAKTU 2.2. otrzymamy, że formuła ¬G wynika logicznie ze zbioru formuł tworzących program P.Cel G ma postać
/\(~(B1^…^ Bn)) <=> ~\/(B1 ^…^Bn)zatem formuła\/x1 ... \/xk (B1 ^…^Bn)wynika logicznie z P, gdzie x1,…,xk są wszystkimi zmiennymi występującymi w G. Tym samym znajdziemy obiekty x1,…,xk spełniające cel G.Horn: Def. Klauzula definitywna Klauzulą definitywną nazywamy klauzulę zawierającą dokładnie jeden literał pozytywny, co zapisujemy:B1, ..., Bn→A, gdzie B1, ..., Bn = B1 ^B2 ^... ^Bnw szczególności: n = 0 → A – klauzula jednostkowa – Fakt (1→A)n > 0,B1, ..., Bn → A – klauzula nie jednostkowa: reguła; regułę w praktyce zapisujemy jako:A ← B1, ..., Bn, gdzie A to głowa, B1, ..., Bn, - body – ciało reguły. Def. Program definitywny Programem definitywnym nazywamy dowolny skończony zbiór klauzul definitywnych, czyli zbiór formuł postaci:"(B1 ʌ..ʌBn →A).Def. Klauzula celu. Celem nazywamy klauzulę nie zawierającą literałów pozytywnych (m=0) ←B1,…,Bn która jest równoważna formule "(<-(B1 ^.... ^ Bn)) na podstawie tautologii KRZ: (p→0)→¬p Def. Klauzula Horna,...
Wujek_Misiek