Mantık ve Bildirimsel Programlama
Mantık ve bildirimsel programlama, problemleri ilişkiler, olgular ve kurallar olarak ifade etmekte, çözüm arayışını açık adım adım talimatlar yerine bir çıkarım motoruna bırakmaktadır.
Tanım
Mantık programlama, bir programın mantıksal cümleler (olgular ve kurallar) kümesi olduğu bildirimsel bir paradigmadır ve hesaplama, genellikle birleştirme (unification) ile çözünürlük (resolution) kullanılarak otomatik çıkarım yoluyla, bu bilgiye karşı sorguları yanıtlamak üzere ilerlemektedir.
Kapsam
Bu konu, Horn cümleleri ve çözünürlüğe (Prolog'da olduğu gibi) dayalı mantık programlamayı, kısıt mantık programlamayı ve bir şeyin nasıl hesaplanacağından ziyade neyin geçerli olması gerektiğini belirten daha geniş bildirimsel fikri kapsamaktadır. Birleştirme (unification), geri izlemeli arama (backtracking search), mantık programlarının model-teorik ve ispat-teorik semantiği ile mantıksal belirtimin kontrolden ayrılması da bu kapsamda incelenmektedir.
Temel sorular
- Mantıksal cümlelerden bir hedefi ispatlayarak hesaplama yapmak ne anlama gelmektedir?
- Birleştirme (unification) ve geri izleme (backtracking), ilişkisel bir program üzerinde aramayı nasıl gerçekleştirmektedir?
- Mantığın kontrolden ayrılması nasıl kesinleştirilmektedir?
- Kısıtlar, saf mantık programlamayı nasıl genişletmektedir?
Temel kuramlar
- Çözünürlük ilkesi
- Robinson'ın çözünürlüğü, birinci dereceden mantık için tek, makine odaklı bir çıkarım kuralı sunarak, mantık programlamayı hesaplama açısından uygulanabilir kılan çıkarımsal motoru sağlamaktadır.
- Mantık artı kontrol
- Kowalski'nin analizi, bir programın mantıksal içeriğini (neyin doğru olduğu) kontrol bileşeninden (ispatın nasıl arandığı) ayırarak, mantık programlamayı mantığı sabit tutarken kontrolü değiştirmenin bir yolu olarak çerçevelemektedir.
- Mantık programlarının bildirimsel ve prosedürel semantiği
- Lloyd, belirli mantık programlarının model-teorik, sabit nokta ve operasyonel semantiğini resmileştirmekte ve bunların yazışmalarını kanıtlayarak mantık programlarının anlamını temellendirmektedir.
Klinik önem
Bildirimsel ve mantık tabanlı teknikler, veritabanı sorgu dilleri, kısıt çözücüler, bilgi gösterimi ve kural motorlarının temelini oluşturmaktadır. Algoritmalar yerine problemleri belirtmeye verdikleri önem, onları kombinatoryal arama, yapılandırma ve akıl yürütme görevleri için oldukça uygun kılmaktadır.
Tarihçe
Robinson'ın 1965 tarihli çözünürlük ilkesi (resolution principle) çıkarımsal temeli atmıştır. 1970'lerin başında Colmerauer ve Roussel Prolog'u yaratmış, Kowalski ise Horn cümlelerinin prosedürel yorumunu dile getirmiştir. Paradigma 1980'ler boyunca gelişmiş, Japonya'nın Beşinci Nesil projesini etkilemiş ve daha sonra kısıt mantık programlama ile cevap kümesi programlamaya doğru genişlemiştir.
Tartışmalar
- Saflık ve pratik kontrol
- Mantık programlama dilleri, saf bildirimsel mantık idealini, verimliliği artıran ancak temiz mantık/kontrol ayrımını tehlikeye atan kesme (cut) ve sıralama gibi açık kontrol için pratik ihtiyaçlarla dengelemektedir.
Öne çıkan isimler
- Robert Kowalski
- Alain Colmerauer
- J. Alan Robinson
- John Lloyd
- Philippe Roussel
İlgili konular
Temel eserler
- kowalski1979
- robinson1965
- lloyd1987
- colmerauer1993
Sıkça sorulan sorular
- Mantık programlama, zorunlu (imperative) programlamadan nasıl farklılaşmaktadır?
- Bir işlem dizisi belirtmek yerine, bir mantık programı olguları ve kuralları bildirmekte ve bir çıkarım motoru sorguları yanıtlayan ispatları aramaktadır; böylece programcı, bir şeyi nasıl hesaplayacağından ziyade neyin doğru olduğuna odaklanmaktadır.
- Birleştirme (unification) nedir?
- Birleştirme (unification), iki mantıksal terimi özdeş kılan bir ikame (substitution) bulma sürecidir; mantık programlarının hedefleri cümle başlıklarıyla eşleştirdiği temel mekanizmadır.