Mantık programlama: Prolog, unification ve resolution

Mantık programlama, programı mantık önermeleriyle yazar: neyin doğru olduğunu söylersin, sistem sorulan soruyu bu önermelerden kanıtlamaya çalışır. Bu yüzden declarative (bildirimsel) bir yaklaşımdır: sonucun ne olduğunu tarif edersin, nasıl hesaplanacağını değil. Dersin dili Prolog (1972, Colmerauer ve Roussel). Sınavda çıkan: bir veritabanı ve kurallar verilir, bir sorgunun tüm cevaplarını sırasıyla yazman ve unification sonuçlarını bulman istenir.

Altın kurallar:

1. Clause’lar yukarıdan aşağı, alt hedefler soldan sağa denenir.
2. Başarısızlıkta en son seçim noktasına geri dönülür (backtracking).
3. Büyük harfle başlayan değişkendir, küçük harfle başlayan atom.
4. is hesaplar, = sadece unify eder.
5. Cut başka clause’ların denenmesini engeller.

Mantıktan Prolog’a

Proposition (önerme) doğru ya da yanlış olabilen mantıksal bir ifadedir. Predicate calculus önermeleri compound term’lerle yazar: parent(ayse, can), bir functor (parent) ve argümanlar. Değişkenli önermeler için niceleyiciler var: $\forall X$ (her X için), $\exists X$ (bir X vardır).

Otomatik kanıt için önermeler standart bir biçime çevrilir: clausal form. Prolog bunun da kısıtlı bir halini kullanır: Horn clause. Bir Horn clause’un sol tarafında (sonuç kısmında) en fazla bir terim vardır:

$\text{grandparent}(X, Z) \leftarrow \text{parent}(X, Y) \wedge \text{parent}(Y, Z)$

Okunuşu: “parent(X, Y) ve parent(Y, Z) doğruysa grandparent(X, Z) doğrudur.” Sol tarafı boş olmayan Horn clause’lar Prolog’un fact ve rule’larıdır.

Prolog’un üç ifadesi

% fact: koşulsuz doğru
parent(ayse, can).
parent(ayse, deniz).
parent(mehmet, can).
parent(can, elif).
parent(deniz, kerem).
parent(deniz, lale).
male(mehmet). male(can). male(kerem).

% rule: baş :- gövde.   virgül = VE
father(X, Y) :- parent(X, Y), male(X).
grandparent(X, Z) :- parent(X, Y), parent(Y, Z).

?- parent(X, can).           % query (goal)
X = ayse ;
X = mehmet.

Değişkenin “değer alması” atama değildir; instantiation (örneklenme) bir kanıt arayışı sırasında geçicidir ve backtracking’de geri alınır. Bir clause içindeki aynı isimli değişkenler aynı şeyi gösterir; farklı clause’lardakiler bağımsızdır.

Unification

İki terimi aynı yapan değişken bağlamalarını bulma işlemi. Kurallar:

• Atom ya da sayı yalnızca kendisiyle eşleşir.
• Bağlanmamış bir değişken herhangi bir terimle eşleşir ve ona bağlanır.
• İki structure, functor’ları ve argüman sayıları aynıysa ve argümanları sırayla eşleşiyorsa eşleşir.

?- f(X, b) = f(a, Y).          X = a, Y = b
?- f(X, X) = f(a, b).          false          (X hem a hem b olamaz)
?- g(X, h(Y)) = g(k, h(X)).    X = k, Y = k
?- [H|T] = [1, 2, 3].          H = 1, T = [2,3]
?- [A, B|C] = [x, y, z, w].    A = x, B = y, C = [z,w]

Resolution ve arama sırası

Resolution, bir hedefi kanıtlamak için o hedefle unify olan bir clause bulup, clause’un gövdesini yeni hedefler olarak almaktır. Hedef listesi boşalınca kanıt tamamdır. Prolog backward chaining yapar: hedeften başlayıp fact’lere doğru geriye gider (fact’lerden başlayıp yeni fact türetmek forward chaining’dir; hedef az, fact çoksa backward daha verimli).

Prolog’un kararları:

• Derinlik öncelikli (depth-first): bir alt hedefin kanıtını bitirmeden sonrakine geçmez. Bellek açısından ucuz.
• Clause sırası: veritabanında yazıldığı sırayla, yukarıdan aşağı.
• Alt hedef sırası: soldan sağa.
• Backtracking: bir alt hedef başarısız olunca, en son seçim yapılan alt hedefe dönülür ve onun bir sonraki alternatifi denenir.

İzleme: ?- grandparent(ayse, G).

grandparent(ayse, G) :- parent(ayse, Y), parent(Y, G).

parent(ayse, Y)   1. çözüm Y = can
  parent(can, G)  G = elif               → CEVAP 1: G = elif
  başka parent(can, _) yok → backtrack
parent(ayse, Y)   2. çözüm Y = deniz
  parent(deniz, G)  G = kerem            → CEVAP 2
                    G = lale             → CEVAP 3
parent(ayse, Y)   başka çözüm yok → bitti

?- grandparent(ayse, G).
G = elif ; G = kerem ; G = lale.
?- father(F, can).
F = mehmet.

father(F, can) için önce parent(F, can) → F = ayse; male(ayse) başarısız → backtrack; F = mehmet, male(mehmet) ✔.

Kardeş kuralı ve \=

sibling(X, Y) :- parent(P, X), parent(P, Y), X \= Y.

?- sibling(can, S).
S = deniz.
?- sibling(kerem, S).
S = lale.

\= olmasa her kişi kendi kardeşi de çıkardı.

Aritmetik

?- X is 2 + 3 * 4.          X = 14
?- X = 2 + 3.               X = 2+3        (yapısal terim, hesaplanmadı)
?- X = 2 + 3, Y is X * 2.   X = 2+3, Y = 10
?- X is Y + 1.              instantiation error
?- 6 =:= 2 * 3.             true           (=:= iki tarafı hesaplayıp karşılaştırır)

is sağ tarafı hesaplar ve sol tarafla unify eder. Sağdaki tüm değişkenler önceden bağlı olmalı. Bu yüzden aritmetik içeren kurallarda alt hedef sırası önemlidir:

len([], 0).
len([_|T], N) :- len(T, N1), N is N1 + 1.

fact(0, 1).
fact(N, F) :- N > 0, N1 is N - 1, fact(N1, F1), F is N * F1.

speed(ford, 100).  time(ford, 2).
distance(C, D) :- speed(C, S), time(C, T), D is S * T.

?- len([a, b, c], N).      N = 3
?- fact(4, F).             F = 24
?- distance(ford, D).      D = 200

Listeler

[a, b, c] ve [H|T] gösterimi. Klasik ilişkiler:

member(X, [X|_]).
member(X, [_|T]) :- member(X, T).

append([], L, L).
append([H|T], L, [H|R]) :- append(T, L, R).

?- member(X, [p, q]).          X = p ; X = q
?- append([1], [2, 3], L).     L = [1,2,3]
?- append(X, Y, [1, 2]).       X = [], Y = [1,2] ;
                               X = [1], Y = [2] ;
                               X = [1,2], Y = []

Predicate’ler fonksiyon değil ilişkidir: aynı append birleştirir, böler, bir önek ya da sonek arar. Hangi argümanın girdi hangisinin çıktı olduğunu sorgu belirler.

Cut ve negation

Cut (!) her zaman başarılı olan bir hedeftir; ama backtracking ile üzerinden geri geçilemez. Geçildiği anda, bu predicate için yapılmış seçimler (hem önceki alt hedefler hem kalan clause’lar) dondurulur.

max(X, Y, X) :- X >= Y, !.
max(_, Y, Y).

maxbad(X, Y, X) :- X >= Y.
maxbad(_, Y, Y).

?- max(7, 3, M).       M = 7.
?- maxbad(7, 3, M).    M = 7 ; M = 3.     (ikinci cevap yanlış)

Cut verimlilik kazandırır ama programın anlamını clause sırasına bağlar; saf mantıktan uzaklaşır.

Negation as failure: \+ G, G kanıtlanamazsa başarılı olur. Bu, Prolog’un closed-world assumption’ına dayanır: veritabanından kanıtlanamayan her şey yanlıştır.

?- \+ parent(elif, _).    true      (elif'in çocuğu kayıtlı değil)
?- \+ parent(can, _).     false

Mantıksal “değil” ile aynı değildir: \+ bir değişkeni bağlamaz ve “bilinmeyen” durumu yoktur.

Prolog’un eksiklikleri

bad_anc(X, Y) :- bad_anc(Z, Y), parent(X, Z).   % sol özyineleme, önce
bad_anc(X, Y) :- parent(X, Y).

ancestor(X, Y) :- parent(X, Y).                 % taban önce
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).

?- bad_anc(ayse, elif).    sonsuz özyineleme (yığın taşar)
?- ancestor(ayse, D).      D = can ; D = deniz ; D = elif ; D = kerem ; D = lale

Uygulama alanları: ilişkisel veritabanı sorguları, uzman sistemler (expert systems), doğal dil işleme, kanıt sistemleri.

Sık yapılan hatalar

parent(ayse, can).
parent(ayse, deniz).
parent(mehmet, can).
parent(can, elif).
parent(deniz, kerem).
parent(deniz, lale).

grandparent(X, Z) :- parent(X, Y), parent(Y, Z).

sibling(X, Y) :- parent(P, X), parent(P, Y), X \= Y.

append([], L, L).
append([H|T], L, [H|R]) :- append(T, L, R).

len([], 0).
len([_|T], N) :- len(T, N1), N is N1 + 1.

fact(0, 1).
fact(N, F) :- N > 0, N1 is N - 1, fact(N1, F1), F is N * F1.

max(X, Y, X) :- X >= Y, !.
max(_, Y, Y).
maxbad(X, Y, X) :- X >= Y.
maxbad(_, Y, Y).

bad_anc(X, Y) :- bad_anc(Z, Y), parent(X, Z).
bad_anc(X, Y) :- parent(X, Y).
ancestor(X, Y) :- parent(X, Y).
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).