Akıl Yürütme Motoru 114'ü Asal Kanıtladı: Bir Negasyon Hatası
Açık kaynaklı zelph motorunda bir negasyon hatası 114'ü asal sayı olarak kanıtladı; forward chaining'deki ırk koşulu ve stratifikasyonla çözümü anlatılıyor.
zelph, her şeyi tek bir grafta modelleyen açık kaynaklı bir C++ akıl yürütme motoru: olgular, kurallar, yüklemler ve hatta sayılar birer graf düğümü. Sayılar rakam listeleri olarak temsil edilir; toplama, çarpma, bölme gibi işlemler çekirdekte gömülü aritmetik kodu değil, grafı yeniden yazan sıradan çıkarım kurallarıdır. Geliştirici bu altyapıyı sergilemek için ders kitabındaki tanıma sadık bir asallık testi yazmak istemiş: 'N'nin böleni yoksa N asaldır' kuralını negation-as-failure ile ifade etmiş.
Kural mantıksal olarak doğru olsa da program iki farklı hatayla çalışmıştır. Birinci hata basit: önek olmadan yazılan sayı bir atom olarak ayrıştırılmış, hiçbir aritmetik kural bir atomu bölemediği için hiçbir bölen olgusu üretilememiş ve negasyon her zaman doğru çıkarak her sayı asal gibi görünmüş. İkinci ve daha ilginç hata, motorun sıralı olmayan bir küme üzerinden kuralları yinelemesinden kaynaklanan bir 'ırk koşulu'ydu: negasyon, ilgili pozitif olgu henüz türetilmeden değerlendiriliyordu. Forward chaining monoton olduğundan (olgular asla geri alınmıyor), yanlış sonuç bir kez kanıtlanınca kalıcı hale geliyordu; sonuç, kural tanımlama sırasına göre değişen, tekrarlanabilirliği belirsiz bir hataydı.
Çözüm, 1980'lerden bilinen katmanlı (stratified) Datalog semantiğinin motora fiilen uygulanmasıydı: önce tüm pozitif kurallar sabit noktaya kadar çalıştırılır, ancak sonra negasyon içeren kurallar doyurulmuş olgu tabanına karşı değerlendirilir; bu iki aşama gerektiği kadar tekrarlanır. Aynı monotonluk özelliği hem hatanın hem çözümün kaynağıydı: yeni olgular bir negasyonu başarısız kılabilir ama asla yeniden başarılı kılamaz, dolayısıyla pozitif aşama bittikten sonra başarılı olan negasyon kesindir.
Düzeltme sonrası motor, keyfi hassasiyetli aritmetiği grafik yeniden yazma kuralları üzerinden çalıştırarak ders kitabı kuralını olduğu gibi doğru şekilde yürütebiliyor. Kütüphanede ayrıca negasyonsuz, pozitif katlama tabanlı bir asallık kanıtlama stratejisi de bulunuyor; bu yaklaşım bileşik sayılarda daha hızlı çalışıyor çünkü en küçük bölende arama durabiliyor. Yazar, bu deneyimden çıkardığı dersleri paylaşıyor: negation-as-failure ileri zincirleme motorlarında bir zamanlama sorunudur, sıraya bağlı hatalar küçültülüp regresyon testine dönüştürülmelidir ve kodun uygulamadığı semantiği belgelemek kendine yazılmış bir hata raporudur.