Michael Spivey：an Introduction To Logic Programming Through Prolog@1996

這份介紹 Prolog 的文件主要闡述了邏輯編程的核心概念、語義基礎、執行機制以及實際應用和實現方面的考慮。其主要論點可以歸納如下：

  1. 邏輯編程是一種聲明式編程範式，其程式即邏輯理論。

    • 與指令式編程（如 Pascal）透過指令序列改變記憶體狀態來描述計算過程不同，邏輯編程屬於聲明式範疇。程式由描述問題領域事實和關係的邏輯語句（通常是 Horn 子句）組成。
    • 一個程式可以被理解為一組關於某些事物及其關係的邏輯斷言。程式描述了「是什麼」，而不是「如何做」。
    • 這種聲明式特性使得程式具有獨立於執行機制的邏輯語義，程式的正確性可以透過其邏輯陳述是否真實來判斷，而非依賴於特定的執行步驟。

  2. 邏輯程式的語義基於模型理論，特別是最小模型。

    • 程式的意義由其所有可能的解釋（interpretation）構成的模型集合來定義。一個程式在某個解釋下為真，若程式中的每個子句在该解釋下為真。
    • 對於 Horn 子句程式，存在一個唯一的「最小模型」（least model），它包含了程式邏輯上所蘊含的所有地面的（ground，不含變數的）原子事實。文件強調，在最小模型中為真的地面事實正是程式試圖描述的關係。基於失敗的否定語義也通常參考這個最小模型。
    • 邏輯蘊含（logical entailment）是判斷結論是否正確的標準：一個子句由程式邏輯蘊含，若該子句在程式的所有模型中為真。

  3. 邏輯程式的執行是透過邏輯推理（證明尋找）來實現的。

    • 邏輯程式的執行不是指令的順序執行，而是從程式中的子句出發，運用推理規則推導新的結論，直到推導出與目標（goal）相關的結論。
    • 歸結（Resolution） 是主要的自動推理規則。它結合了替換（substitution）和地面歸結（ground resolution）的思想，允許在處理包含變數的子句時，透過合一（Unification） 過程來確定變數的綁定。
    • 合一 是歸結的核心機制，它尋找使兩個項相等的「最一般合一子」（most general unifier, m.g.u.）。合一使得程式的關係可以是雙向的（bi-directional）：同一個程式可以用於計算已知關係中的未知部分，而無需預先指定輸入和輸出參數。

  4. Prolog 實現採用了受限的歸結形式（SLD 歸結）和深度優先搜索策略以提高效率。

    • 一般的歸結過程搜索空間巨大。Prolog 採用 SLD 歸結（Selected-literal Linear Resolution for Definite clauses），這是一種受限的歸結形式，其中一個輸入子句始終是當前目標子句，且目標子句中的待解決字面量（literal）按固定順序（Prolog 為從左到右）選擇。
    • SLD 歸結保留了歸結的完備性（refutation completeness）：如果一個目標是程式的邏輯蘊含，則存在一個 SLD 歸結可以推導出空目標（表示成功）。
    • Prolog 實現透過探索 SLD 搜索樹來尋找歸結證明。它採用深度優先搜索策略來遍歷這棵樹。雖然深度優先搜索易於實現（通常使用堆棧），但如果搜索樹包含無限分支，它可能不是完備的（即可能找不到存在的解）。
    • 證明成功時，可以從歸結過程中計算得到的合一子（unifier）中提取出答案替換（answer substitution），給出滿足目標變數的特定綁定值。

  5. 基於失敗的否定（Negation as Failure, NAF）是處理邏輯否定的常用方法，但有其語義和實現上的限制。

    • Prolog 透過嘗試證明字面量 P，若證明失敗則推斷 not P 為真來實現否定。
    • NAF 的正確性依賴於封閉世界假設（closed world assumption）和程式的最小模型：任何無法從程式證明的事實被視為在最小模型中為假，進而在真實世界中也為假。
    • 在實現中，為確保健全性，被否定的字面量在執行 NAF 之前通常必須是地面的（ground），即不包含未綁定的變數。這對程式的書寫順序提出了要求。
    • 允許程式子句體中出現否定需要更複雜的語義模型，如分層程式（stratified programs），其關係可以分層定義，低層關係不依賴於高層關係，否定只涉及較低層的關係。

  6. 邏輯編程適用於多種問題領域，且高效實現依賴於特定的優化技術。

    • 邏輯編程自然適合處理關係型問題（如資料庫查詢）、搜索問題（圖形遍歷）、符號處理（語法分析、代數簡化）、以及某些模擬問題。
    • 為了實現高效的邏輯程式執行，需要先進的實現技術，包括：
      • 優化的資料結構：使用高效的方式表示項（terms）和替換（substitutions），以便快速執行合一操作（如結構共享、綁定函數、Trail 堆棧）。
      • 索引（Indexing）：根據目標字面量的結構快速定位可能匹配的程式子句，減少不必要的合一嘗試。
      • 尾遞歸優化（Tail Recursion Optimization, TRO）：將特定的遞歸模式轉換為迭代，減少堆棧空間的使用，使程式可以處理更深的遞歸而不會棧溢出。
      • 垃圾回收（Garbage Collection, GC）：回收不再可訪問的記憶體空間。
    • 文件也提到，為了追求速度，實際的 Prolog 實現有時會犧牲理論上的健全性（如省略合一的發生檢查），這可能導致推導出邏輯上不正確的結論。

總之，文件勾勒出一個完整的邏輯編程畫卷：從其嚴謹的邏輯基礎和模型語義，到基於歸結和合一的證明尋找執行機制，再到程式結構（遞歸、否定）與應用，最後深入到實現層面的具體優化技術，闡釋了如何將抽象的邏輯理論轉化為可用的程式語言實現。