邏輯式編程語言極簡實現(使用C#) - 3. 運行原理

来源:https://www.cnblogs.com/skabyy/archive/2020/07/02/13209724.html

圖文講解,一門教學級邏輯式編程語言,NMiniKanren,的運行原理。 ...


本系列前面的文章:

第二天,好為人師的老明繼續開講他的私人課堂。

“今天講NMiniKanren的運行原理。”老明敲了敲白板,開始塗畫代碼,“我們從一個喜聞樂見的例子開始。”

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
    var x = k.Fresh();
    var y = k.Fresh();
    return k.All(
        k.Any(k.Eq(x, 1), k.Eq(x, 2)),
        k.Any(k.Eq(y, x), k.Eq(y, "b")),
        k.Eq(q, k.List(x, y)));
}));

“這題我會了!”小皮在例子下邊寫下答案:

[(1 1), (1 b), (2 2), (2 b)]

看到小皮沒把昨天的知識忘光,老明略感欣慰:“不錯。你這個答案是怎麼算出來的呢?”

“呃……就是那個……”小皮忽然卡殼了。這種問題就好比幾何證明題,明明一眼就能看出來的兩條垂直線,真下手證明卻發現還挺不容易。小皮抓了幾把頭髮,總算理出一縷思緒:“大概就是找出所有條件可能的組合……然後算一下解……”小皮一邊說,一邊在白板上寫著:

  • x == 1
    • y == x => (x y) == (1 1)
    • y == "b" => (x y) == (1 "b")
  • x == 2
    • y == x => (x y) == (2 2)
    • y == "b" => (x y) == (2 "b")

“嗯,其實你已經知道怎麼算出答案來了。只是對於其中的細節還不甚明瞭。我們接下來要做的事要理清楚這個計算過程,得到一個每一步都可以由電腦明確執行的演算法。

“這個演算法其實就是你所說這樣,找出所有可能的條件組合。每組條件組合可以求出一個解,也可能自相矛盾從而無解。由於NMiniKanren中的條件都是相等條件,所以一組條件組合可以看作一個替換(Substitution)。一個替換能產生一個解,或者無解。

“因此,只需解決下麵兩個問題:

  1. 要在什麼數據結構上按照什麼順序遍歷替換
  2. 如何從替換中算出一個解,或者判斷其無解。”

遍歷分支

首先,我們要從代碼構造出一個數據結構(其實就是一張圖)。這個數據結構能夠按照一定的順序進行遍歷,並依次生成替換。

例子中的代碼使用到了EqAnyAll這三種構造目標的方法。下麵分別探討怎樣從這三種方法構造出我們需要的數據結構來。

Eq

k.Eq(a, b)構造的目標是什麼意思呢?”老明以一個看似平凡的問題開頭。

“簡單,意思就是a要等於b這個條件。”

“孤立地看,是這樣。但是考慮到上下文,更精確地說應該是,在上下文的基礎上追加a等於b這個條件。”

小皮有點不解:“emm……多了‘追加’有什麼不同呢?”

“從文字上看,多了‘追加’後,目標的解釋從一種名詞(一組條件)變成了動詞(追加條件)。這樣一來,目標不僅表達了一組條件,同時也表達了這些條件如何跟上下文結合。就Eq的情況來說,這個結合方式是‘追加’。而AnyAll會有其他結合方式。”

“雖然還不是很明白,我想這個要等AnyAll的情況一起對比才能清晰起來。我還另外有個問題,上下文指的是什麼?”

“狹義地說,上下文是解釋器運行到這一條代碼時,已執行的代碼生成的替換。

上下文 <-> 一個替換 <-> 一組條件

“廣義上看,上下文還應該包含回溯分支等控制信息,不過目前我們先忽略這些。

“綜合起來,按照對Eq目標的解釋,我們可以用下圖來表示這個目標。”

Any(或)

“接著看Any。按照上面的討論,我們要怎麼解釋Any目標呢?”老明繼續發問。

解釋目標要說清楚兩個方面:名詞(什麼條件)和動詞(如何與上下文結合)。以一開始的例子中的k.Any(k.Eq(x, 1), k.Eq(x, 2))為例。名詞方面自然就是x等於1和x等於2兩個條件了,不過這兩個條件是‘或’的關係。動詞方面,應該是從上下文分岔出兩個分支,一個分支追加x等於1這個條件,另一個分支追加x等於2這個條件。”

“很好。也就是說,和Eq不同,Any操作和上下文結合後,會生成多個替換。”老明贊許地點點頭,“它把參數的分支都放在一起,就像加法似的。用圖表示的話,就像下麵這樣。”

All(與)

“最後是All……”

“這個我也會了!”小皮打斷老明,“k.All(a, b)名詞上表示條件a且條件b;動詞上表示上下文先追加a,再追加b。”

“你說的太籠統了。ab可能都有多個分支,這種情況下怎麼做?”老明接著問道。

小皮想了想一開始做的例子,答道:“這種情況要取所有組合,也就是a的分支和b的分支兩兩組合!最後分支數量等於a分支數量乘以b分支數量。”

“很好。如果Any類比加法,那麼All類比的是乘法。下麵這圖描述了開頭例子中的All方法的結合過程。

這是個有向圖,每條邊表示一次追加條件的過程。每條從開始節點(上下文)到結尾的路徑,上面的節點組合起來就是一個替換。遍歷所有路徑,我們就遍歷了所有替換。而遍歷的順序,就是解釋器輸出結果的順序。

Anyi

接下來我們還可以來看看Anyi

普通的Any使用的普通的樹結構遍歷順序:

Anyi以交替的順序遍歷分支:

Alli類似採用交替的順序遍歷,這裡就不再畫了(主要是不好畫,懶)。

再看目標(Goal)

上一篇主要從構造目標的角度出發,介紹了不同方式構造出來的目標。為了實現NMiniKanren的解釋器,我們需要更加深入地瞭解在解釋器的實現中,Goal是什麼類型。

在前面的討論中,我們知道,目標的含義是對上下文/一個替換按照某種方式追加一些條件,返回零個、一個或多個替換——Eq返回一個;AnyAll可能返回多個;另外前面沒討論到的Fail會返回零個。

從這個描述不難看出,最方便表述目標類型的是一個單參數函數,其參數是一個替換,返回值是替換的枚舉,相當於C#中的Enumerable<替換>,也可以說是一個替換的流(Stream)。

Goal: (替換) -> Stream<替換>

Goal(替換)這個函數調用的含義是把Goal包含的條件,追加到替換上,返回一系列(因為可能有分支,就會變成多個)的替換。

“為什麼不直接用List呢?”小皮又發問了。

“因為很多情況下,分支數量會很多,甚至是無窮多,而我們只需要挨個取前面幾個結果就夠了。這種情況下使用List會極大降低解釋器效率,甚至造成死迴圈。”

遞歸的情況

“略。”

“啥?”小皮瞪了下眼。

“懶得畫,留著思考吧。”

替換求解

“生成替換後,剩下的就是求解了。

“替換求解的方法很簡單,就是應用一下小學時學過的代入消元法。來,看看這個怎麼解。”老明一邊說一邊寫下例題:

(1) y == x
(2) q == (x y)
(3) x == 1

畢竟是小學難度的題目,小皮看了一眼,馬上就有瞭解法:“x等於1是確定的了,把(3)代入(1)後,y也等於1。把(1)和(3)都代入(2),得到q等於(1 1)。”

“解是求出來了,不過你覺得你這個步驟有通用性嗎?”老明虛著眼說,“電腦能自覺地使用你這個蛇皮順序嗎?”

“呃……”小皮陷入沉思。判斷代入順序的規則似乎還挺麻煩的。或者簡單粗暴按照所有順序都代入一遍?

“其實沒想象中複雜,按順序代入一遍,再反過來代入一遍,就OK了。”

按順序代入

把(1)代入(2)(3):

(1) y == x
(2) q == (x x)
(3) x == 1

把(2)代入(3):

(1) y == x
(2) q == (x x)
(3) x == 1

在解釋器實現中,條件是一條一條追加上來的。可以每次追加條件的時候,將已有的條件代入新條件,這樣就把這一步化解到生成替換的過程中了。

加入條件(1) y == x:

(1) y == x

加入條件(2) q == (x y):

(1) y == x
(2) q == (x x)

加入條件(3) x == 1:

(1) y == x
(2) q == (x x)
(3) x == 1

按相反順序代入

把(3)代入(2)(1):

(1) y == 1
(2) q == (1 1)
(3) x == 1

把(2)代入(1):

(1) y == 1
(2) q == (1 1)
(3) x == 1

搞定!

這隻是個簡單的例子。實際情況還可能會出現無解、自由變數以及死迴圈等情況。這裡就不多贅述了。

再議“非”運算

“現在能看出NMiniKanren為什麼不支持‘非’運算了嗎?”

小皮認真想了一會,說:“豈止不支持‘非’,‘大於’和‘小於’這些也不行吧。按照代入消元法,NMiniKanren只支持相等條件。”。

“那如果要支持這些運算應該怎麼做呢?”

“要拓展條件的類型。除了相等條件,還要有不相等條件等。響應的求解演算法也要有所變化。”

“沒錯。改動雖然不大,但是代碼看起來會混亂得多。所以以教學為目的的話,就不支持這些了。”

小結

不知不覺時間已到了喜聞樂見的午餐時間,於是老明總結道:“雖然還沒有落地成代碼,但運行原理算是弄清楚了。關鍵點就兩個:

  1. 要在什麼數據結構上按照什麼順序遍歷替換。
  2. 如何從替換中算出一個解,或者判斷其無解。

“第一點,我們從代碼構造了一張圖。該圖的每條路徑對應一個替換,遍歷路徑的順序就是遍歷替換的順序。同時也明確了目標Goal的類型。

“第二點,我們使用代入消元法,來回兩遍代入解出了所有未知量。”

“接下來可以寫代碼實現NMiniKanren解釋器了吧。”理解了原理後,小皮的十條手指已經饑渴難耐,蚯蚓似的扭動著。

“不著急,下午還要先講一個編程小技巧,然後就可以開搞了。”


您的分享是我們最大的動力!

更多相關文章
  • 一.官方文檔 https://pypi.org/project/muggle-ocr/ 二模塊安裝 pip install muggle-ocr # 因模塊過新,阿裡/清華等第三方源可能尚未更新鏡像,因此手動指定使用境外源,為了提高依賴的安裝速度,可預先自行安裝依賴:tensorflow/numpy ...
  • 案例故事: 即時通訊(IM)軟體有很多,比如企業微信,釘釘,飛書,Skype, 微軟的Lync等, 這些軟體現在都很牛,還能監控誰誰在不在電腦旁工作,誰誰誰提前下班溜了。。。 一次偶然的機會,有個妹子請教我,她每天都想準時18點下班, 她問我如何做到: 假裝企業微信線上,併在2個小時後(20點)準時 ...
  • 引用的DLL MySql.Data.MySqlClient System.Data City實體 public class City { public int ID { get; set; } public string Name { get; set; } public string Countr ...
  • 在項目的實際開發過程中,我們經常會遇到Tab頁面的開發 EciTab控制項有多種使用方式: 下麵介紹Frame容器方式: 下麵介紹的Tab頁面採用的策略是 Tab頁面管理幾個子頁面,頁面組織上用Iframe管理的模式 採用Iframe的原因主要有兩個 1.開發簡單,每一個頁面都是簡單的畫面 2.性能考 ...
  • 官網 http://www.hzhcontrols.com/ 前提 入行已經7,8年了,一直想做一套漂亮點的自定義控制項,於是就有了本系列文章。 GitHub:https://github.com/kwwwvagaa/NetWinformControl 碼雲:https://gitee.com/kww ...
  • 在 Xunit 中使用依賴註入 Intro 之前寫過一篇 xunit 的依賴註入相關的文章,但是實際使用起來不是那麼方便 今天介紹一個基於xunit和微軟依賴註入框架的“真正”的依賴註入使用方式 ——— Xunit.DependencyInjection, 來自大師的作品,讓你在測試代碼里使用依賴註 ...
  • 在KeyPress事件中寫入 private void txtBoxKeyPress(object sender, KeyPressEventArgs e) { if ((e.KeyChar >= 'a' && e.KeyChar <= 'z') || (e.KeyChar >= 'A' && e. ...
  • 多Sheet導入教程 說明 本教程主要說明如何使用Magicodes.IE.Excel完成多個Sheet數據的Excel導入。 要點 多個相同格式的Sheet數據導入 多個不同格式的Sheet數據導入 主要步驟 1. 多個相同格式的Sheet數據導入 1.1 創建導入Sheet的Dto 主要代碼如下 ...
一周排行
  • 比如要拆分“呵呵呵90909086676喝喝999”,下麵當type=0返回的是中文字元串“呵呵呵,喝喝”,type=1返回的是數字字元串“90909086676,999”, private string GetStrings(string str,int type=0) { IList<strin ...
  • Swagger一個優秀的Api介面文檔生成工具。Swagger可以可以動態生成Api介面文檔,有效的降低前後端人員關於Api介面的溝通成本,促進項目高效開發。 1、使用NuGet安裝最新的包:Swashbuckle.AspNetCore。 2、編輯項目文件(NetCoreTemplate.Web.c ...
  • 2020 年 7 月 30 日, 由.NET基金會和微軟 將舉辦一個線上和為期一天的活動,包括 微軟 .NET 團隊的演講者以及社區的演講者。本次線上大會 專註.NET框架構建微服務,演講者分享構建和部署雲原生應用程式的最佳實踐、模式、提示和技巧。有關更多信息和隨時瞭解情況:https://focu... ...
  • #abp框架Excel導出——基於vue #1.技術棧 ##1.1 前端採用vue,官方提供 UI套件用的是iview ##1.2 後臺是abp——aspnetboilerplate 即abp v1,https://github.com/aspnetboilerplate/aspnetboilerp ...
  • 前言 本文的文字及圖片來源於網路,僅供學習、交流使用,不具有任何商業用途,版權歸原作者所有,如有問題請及時聯繫我們以作處理。 作者:碧茂大數據 PS:如有需要Python學習資料的小伙伴可以加下方的群去找免費管理員領取 input()輸入 Python提供了 input() 內置函數從標準輸入讀入一 ...
  • 從12年到20年,python以肉眼可見的趨勢超過了java,成為了當今It界人人皆知的編程語言。 python為什麼這麼火? 網路編程語言搜索指數 適合初學者 Python具有語法簡單、語句清晰的特點,這就讓初學者在學習階段可以把精力集中在編程對象和思維方法上。 大佬都在用 Google,YouT ...
  • 在社會上存在一種普遍的對培訓機構的學生一種歧視的現象,具體表現在,比如:當你去公司面試的時候,一旦你說了你是培訓機構出來的,那麼基本上你就涼了,那麼你瞞著不說,然後又通過了面試成功入職,但是以後一旦在公司被髮現有培訓經歷,可能會面臨被降薪,甚至被辭退,培訓機構出來的學生,在用人單位眼裡就是能力低下的 ...
  • from typing import List# 這道題看了大佬寫的代碼,經過自己的理解寫出來了。# 從最外圍的四周找有沒有為O的,如果有的話就進入深搜函數,然後深搜遍歷# 判斷上下左右的位置是否為Oclass Solution: def solve(self, board: List[List[s ...
  • import requests; import re; import os; # 1.請求網頁 header = { "user-agent":'Mozilla/5.0 (Macintosh; Intel Mac OS X 10_15_5) AppleWebKit/537.36 (KHTML, li ...
  • import requests; import re; import os; import parsel; 1.請求網頁 header = { "user-agent":'Mozilla/5.0 (Macintosh; Intel Mac OS X 10_15_5) AppleWebKit/537. ...