相信很多朋友對于邏輯式程式設計語言，都有一種最熟悉的陌生人的感覺。一方面，平時在書籍、在資訊網站，偶爾能看到一些吹噓邏輯式程式設計的話語。但另一方面，也沒見過周圍有人真正用到它（除了SQL）。
本系列将盡可能簡潔地說明邏輯式程式設計語音的原理，并實作一門簡單的邏輯式程式設計語言。考慮到C#的使用者較多，是以選擇用C#來實作。
遙記當時看《The Reasoned Schemer》（一本講邏輯式程式設計語言的小人書），被最後兩頁的解釋器實作驚豔到了。看似如此複雜的計算邏輯，其實作竟然這麼簡潔。不過礙于當時水準有限，也就囫囵吞棗般看了過去。後來有一天，不知何故腦子靈光一閃，把圖周遊和流計算模式聯系在一起，瞬間明白了《The Reasoned Schemer》中的做法。動手寫了寫代碼，果然如此，短短兩百來行代碼，就完成了解釋器的實作，才發現原來如此簡單。很多時候，并非問題本身有多難，隻是沒有想到正确的方法。
本系列将盡可能簡潔地說明邏輯式程式設計語音的原理，并實作一門簡單的邏輯式程式設計語言。考慮到C#的使用者較多，是以選擇用C#來實作。實作的這門語言就叫NMiniKanren。文章總體内容如下：
NMiniKanren語言介紹
語言基礎
一道有趣的邏輯題：誰是兇手
NMiniKanren運作原理
構造條件關系圖，周遊分支
代入消元法解未知量
實作NMiniKanren
流計算模式簡介
代入消元法的實作
周遊分支的實作
故事從兩個正在吃午餐的程式員說起。
老明和小皮是就職于同一家傳統企業的程式員。這天，兩人吃着午餐。老明邊吃邊刷着抖音，鼻孔時不時噴出幾條米粉。
小皮是一臉麻木地刷着求職網和資訊網，忽然幾個大字映入眼底：《新型邏輯式程式設計語言重磅出世，即将颠覆IT界！》小皮一陣好奇，往下一翻，結果接着的是一些難懂的話，什麼“一階邏輯”，什麼“合一算法”，以及鬼畫符似的公式之類。
小皮看得索然無味，但被勾引起來的對邏輯式程式設計的興趣仿佛澳洲森林大火一樣難以平息。于是伸手拍下老明高舉手機的左手，問道：“嘿！邏輯式程式設計有了解過麼？是個啥玩意兒？”
“邏輯式程式設計啊……嘿嘿，前段時間剛好稍微了解了一下。”老明鼻孔朝天吸了兩口氣，“我說的稍微了解，是指實作了一門邏輯式程式設計語言。”
“不愧是資深老IT，了解也比别人深入一坨坨……”
“也就比你早來一年好不好……我是一邊看一本奇書一邊做的。Dan老師（Dan Friedman）寫的《The Reasoned Schemer》。這本書挺值得一看的，書中使用一門教學用的邏輯式程式設計語言，講解這門語言的特性、用法、以及原理。最後還給出了這門語言的實作。核心代碼隻用了兩頁紙。
“所謂邏輯式程式設計，從使用上看是把聲明式程式設計發揮到極緻的一種程式設計範式。普通的程式設計語言，大部分還是基于指令式程式設計，需要你告訴機器每一步執行什麼指令。而邏輯式程式設計的理念是，我們隻需要告訴機器我們需要的目标，機器會根據這個目标自動探索執行過程。
“邏輯式程式設計的特點是可以反向運作。你可以像做數學題一樣，聲明未知量，列出方程，然後程式會為你求解未知量。”
“挺神奇的。聽起來有點像AI程式設計。不過這麼進階的東西怎麼沒有流行起來？感覺可以節省不少人力。”小皮忽然有種飯碗即将不保的感覺。
“嘿嘿……想得美。其實邏輯式程式設計，既不智能，也不好用。你回憶一下你中學的時候是怎麼解方程組的？”
“嗯……先盯一會方程組，看看它長得像不像有快捷解法的樣子。看不出來的話就用代入法慢慢算。這和邏輯式程式設計有什麼關系？”
“邏輯式程式設計并不智能，它隻是把某種類似代入法的通用算法内置到解釋器裡。邏輯式程式設計語言寫的程式運作時，不過是根據通用算法進行求解而已。它不像人一樣會去尋找更快捷的方法，同時也不能解決超綱問題。
“而且邏輯式程式設計語言的學習成本也不低。如果你要用好這門語言，你得把它使用的通用算法搞清楚。雖然你寫的聲明式的代碼，但内心要時刻清楚程式的執行過程。如果你拿它當個黑盒來用，那很可能你寫出來的程式的執行效率會非常低，甚至跑出一些莫名其妙的結果。”
“哦哦，要學會用它，還得先懂得怎麼實作它。這學習成本還挺高的。”小皮跟着吐槽，不過他知道老明表明上看似嫌棄邏輯式程式設計的實用性，私底下肯定玩得不亦樂乎，并且也喜歡跟别人分享。于是小皮接着道：“雖然應該是用不着，但感覺挺有意思的，再仔細講講呗。天天寫CRUD，腦子都淡出個鳥了。”
果然老明坐直起來：“《The Reasoned Schemer》用的這門邏輯式程式設計語言叫miniKanren，用Scheme/Lisp實作的。去年給你安利過Scheme了，現在掌握得怎麼樣？”
“一竅不通……”小皮大窘。去年到現在，小皮一直很忙，并沒有自學什麼東西。如果沒有外力驅動的話，他還将一直忙下去。
“果然如此。是以我順手也實作了個C#魔改版本的miniKanren。就叫NMiniKanren。我把NMiniKanren實作為C#的一個DSL。這樣的好處是友善熟悉C#或者Java的人快速上手；壞處是DSL會受限于C#語言的能力，代碼看起來沒有Scheme版那麼優雅。”老明用左手做了個打引号的動作，“先從簡單的例子開始吧。比如說，有個未知量<code>q</code>，我們的目标是讓<code>q</code>等于5或者等于6。那麼滿足條件的<code>q</code>值有哪些？”
“不就是5和6麼……這也太簡單了吧。”
“Bingo！”老明打了個響指，“我們先用簡單的例子看看代碼結構。”隻見老明兩指輕輕夾住一隻筷子，勾出幾條米粉，快速在桌上擺出如下代碼：
“代碼中，<code>KRunner.Run</code>用于運作一段NMiniKanren代碼，它的聲明如下。”老明繼續撥動米粉：
“其中，參數<code>n</code>是傳回結果的數量限制，<code>n = null</code>表示無限制；參數<code>body</code>是一個函數：
函數的第一個參數是一個<code>KRunner</code>執行個體，用于引用NMiniKanren方法；
函數的第二個參數是我們将要求解的未知量；
函數的函數體是我們編寫的NMiniKanren代碼；
函數的傳回值為需要滿足的限制條件。
“接着我們看函數體的代碼。<code>k.Eq(q, 5)</code>表示<code>q</code>需要等于<code>5</code>，<code>k.Eq(q, 6)</code>表示<code>q</code>需要等于<code>6</code>，<code>k.Any</code>表示滿足至少一個條件。整段代碼的意思為：求所有滿足<code>q</code>等于<code>5</code>或者<code>q</code>等于<code>6</code>的<code>q</code>值。顯然答案為<code>5</code>和<code>6</code>，程式的運作結果也是如此。很神奇吧？”
“你這米粉打碼的功夫更讓我驚奇……”小皮仔細看了一會，“原來如此。不過這DSL的文法确實看着比較累。”
“主要是我想做得簡單一些。其實使用C#的Lambda表達式也可以實作像……”老明勾出幾條米粉擺出<code>q == 5 || q == 6</code>表達式，“……這樣的文法，不過這樣會增加NMiniKanren實作的複雜度。況且這無非是字首表達式或中綴表達式這種文法層面的差别而已，語義上并沒有變化。學習應先抓住重點，花裡胡哨的東西可以放到最後再來琢磨。”
“嗯嗯。<code>KRunner.Run</code>裡這個<code>null</code>的參數是做什麼用的呢？”
“<code>KRunner.Run</code>的第一個參數用來限制輸出結果的數量。<code>null</code>表示輸出所有可能的結果。還是上面例子的條件，我們改成限制隻輸出<code>1</code>個結果。”小皮用筷子改了下代碼：
“這樣程式隻會輸出5一個結果。在一些包含遞歸的代碼中，可能會有無窮多個結果，這種情況下需要限制輸出結果的數量來避免程式不會終止。”
“原來如此。不過這個例子太簡單了，有沒有其他更好玩的例子。”
老明喝下一口湯，說：“好。時間不早了，我們回公司找個會議室慢慢說。”
到公司後，老明的講課開始了……
首先，要先明确NMiniKanren支援的資料類型。後續代碼都要基于資料類型來編寫，是以規定好資料類型是基礎中的基礎。
簡單起見，NMiniKanren隻支援四種資料類型：
<code>string</code>：就是一個普普通通的值類型，僅有值相等判斷。
<code>int</code>：同<code>string</code>。使用<code>int</code>是因為有時候想少寫兩個雙引号……
<code>KPair</code>：二進制組。可用來構造連結清單及其他複雜的資料結構。如果你學過Lisp會對這個資料結構很熟悉。下面詳細說明。
<code>null</code>：這個類型隻有<code>null</code>一個值。表示空引用或者空數組。
<code>KPair</code>的定義為：
<code>KPair</code>除了用作二進制組（其實是最少用的）外，更多的是用來構造連結清單。構造連結清單時，約定一個<code>KPair</code>作為一個連結清單的節點，<code>Lhs</code>為元素值，<code>Rhs</code>為一下個節點。當<code>Rhs</code>為<code>null</code>時連結清單結束。空連結清單用<code>null</code>表示。
使用<code>null</code>表示空連結清單其實并不合适，這裡純粹是為了簡單而偷了個懶。
我們知道，很多複雜的資料結構都是可以通過連結清單來構造的。是以雖然NMiniKanren隻有三種資料類型，但可以表達很多資料結構了。
這時候小皮有疑問了：“C#本身已經自帶了<code>List</code>等容器了，為什麼還要用<code>KPair</code>來構造連結清單？”
“為了讓底層盡可能簡潔。”老明說道，“我們都知道，程式本質上分為資料結構和算法。算法是順着資料結構來實作的。簡潔的資料結構會讓算法的實作顯得更清晰。相比C#自帶的<code>List</code>，使用<code>KPair</code>構造的連結清單更加清晰簡潔。按照構造的方式，我們的連結清單定義為：
空連結清單<code>null</code>；
或者是非空連結清單。它的第一個元素為<code>Lhs</code>，并且<code>Rhs</code>是後續的連結清單。
“連結清單相關的算法都會順着定義的這兩個分支實作：一個處理空連結清單的分支，一個處理非空連結清單的遞歸代碼。比如說判斷一個變量是不是連結清單的方法：
“以及判斷一個元素是不是在連結清單中的方法：
“資料類型明确後，接下來我們來看看NMiniKanren能做什麼。”
編寫NMiniKanren代碼是一個構造目标（<code>Goal</code>類型）的過程。NMiniKanren解釋器運作時将求解使得目标成立的所有未知量的值。
顯然，有兩個平凡的目标：
<code>k.Succeed</code>：永遠成立，未知量可取任意值。
<code>k.Fail</code>：永遠不成立，無論未知量為何值都不成立。
其中<code>k</code>是<code>KRunner</code>的一個執行個體。C#跟Java一樣不能定義獨立的函數和常量，是以我們DSL需要的函數和常量就都定義為<code>KRunner</code>的方法或屬性。後面不再對<code>k</code>進行複述。
一個基本的目标是<code>k.Eq(v1, v2)</code>。這也是NMiniKanren唯一一個使用值來構造的目标，它表示值<code>v1</code>和<code>v2</code>應該相等。也就是說，當<code>v1</code>與<code>v2</code>相等時，目标<code>k.Eq(v1, v2)</code>成立；否則不成立。
這裡的相等，指的是值相等：
不同類型不相等。
<code>string</code>類型相等當且僅當值相等。
<code>KPair</code>類型相等當且僅當它們的<code>Lhs</code>相等且<code>Rhs</code>相等。
從<code>KPair</code>相等的定義，可以推出由<code>KPair</code>構造的資料結構（比如連結清單），相等條件為當且僅當它們結構一樣且對應的值相等。
接下來我們看幾個例子。
直接<code>q</code>等于<code>5</code>。
<code>k.List(1, 2)</code>相當于<code>new KPair(1, new KPair(2, null))</code>，用來快速構造連結清單。
這個例子比較像一個方程了。<code>q</code>比對<code>k.List(1, 2)</code>的第二項，也就是<code>2</code>。
由于<code>k.List(2, q)</code>的第一項和<code>k.List(1, 2)</code>的第一項不相等，是以這個目标無法成立，<code>q</code>沒有值。
目标無法成立，<code>q</code>沒有值。
目标恒成立，<code>q</code>可取任意值。輸出<code>_0</code>表示一個可取任意值的自由變量。
目标可以看作布爾表達式，是以可以通過“與或非”運算，用簡單的目标構造成複雜的“組合”目标。我們把被用來構造“組合”目标的目标叫做該“組合”目标的子目标。
在前面的例子中，我們隻有一個未知量<code>q</code>。<code>q</code>既是未知量，也是程式輸出。
在處理更複雜的問題時，通常需要定義更多的未知量。定義未知量的方法是<code>k.Fresh</code>：
新定義的未知量和<code>q</code>一樣，可以用來構造目标：
使用“與”運算組合的目标，僅當所有子目标成立時，目标才成立。
使用方法<code>k.All</code>來構造“與”運算組合的目标。
當且僅當<code>g1</code>, <code>g2</code>, <code>g3</code>, ......，都成立時，<code>g</code>才成立。
特别的，空子目标的情況，即<code>k.All()</code>，恒成立。
使用“或”運算組合的目标，隻要一個子目标成立時，目标就成立。
使用方法<code>k.Any</code>來構造“或”運算組合的目标。
當<code>g1</code>, <code>g2</code>, <code>g3</code>, ......中至少一個成立，<code>g</code>成立。
特别的，空子目标的情況，即<code>k.Any()</code>，恒不成立。
MiniKanren（以及NMiniKanren）不支援“非”運算。支援“非”會讓miniKanren的實作複雜很多。
這或許令人驚訝。“與或非”在邏輯代數中一直像是連體嬰兒似的紮堆出現。并且“非”運算是單目運算符，看起來應該更簡單。
然而，“與”和“或”運算是在已知的兩（多）個集合中取交集或者并集，結果也是已知的。而“非”運算則是把一個已知的集合映射到可能未知的集合，周遊“非”運算的結果可能會很久或者就是不可能的。
對于基于圖搜尋和代入法求解的miniKanren來說，支援“非”運算需要對核心的資料結構和算法做較大改變。是以以教學為目的的miniKanren沒有支援“非”運算。
不過，在一定程度上，也是有不完整替代方法的。
If是一個特殊的構造目标的方式。對應《The Reasoned Schemer》中的<code>conda</code>。
如果<code>g1</code>且<code>g2</code>成立，那麼<code>g</code>成立；否則當且僅當<code>g3</code>成立時，<code>g</code>成立。
這個和<code>k.Any(k.All(g1, g2), g3)</code>很像，但他們是有差別的：
<code>k.Any(k.All(g1, g2), g3)</code>會解出所有讓<code>k.All(g1, g2)</code>或者<code>g3</code>成立的解
<code>k.If(g1, g2, g3)</code>如果<code>k.All(g1, g2)</code>有解，那麼隻給出使<code>k.All(g1, g2)</code>成立的解；否則再求使得<code>g3</code>成立的解。
也可以說，If是短路的。
這麼詭異的特性有什麼用呢？
它可以部分地實作“非”運算的功能：
這個這裡先不詳細展開了，後面用到再說。
這是一個容易被忽略的問題。如果程式需要求出所有的解，那麼輸出順序影響不大。但是一些情況下，求解速度很慢，或者解的數量太多甚至無窮，這時隻求前幾個解，那麼輸出的内容就和輸出順序有關了。
因為miniKanren以圖周遊的方式來查找問題的解，是以解的順序其實也是解釋器運作時周遊的順序。先看如下例子：
有兩個未知變量<code>x</code>和<code>y</code>，<code>x</code>可能的取值為1或2，<code>y</code>可能的取值為a或b。可以看到，程式查找解的順序為：
<code>x</code>值為1
<code>y</code>值為a，<code>q=(1 a)</code>
<code>y</code>值為b，<code>q=(1 b)</code>
<code>x</code>值為2
<code>y</code>值為a，<code>q=(2 a)</code>
<code>y</code>值為b，<code>q=(2 b)</code>
如果要改變這個順序，我們有一個交替版的“與”運算<code>k.Alli</code>：
不過這個交替版也不是交替得很漂亮。下面增加<code>x</code>可能的取值到3個：
同樣，“或”運算也有交替版。
正常版：
交替版：
後面講到miniKanren實作原理時會解釋正常版、交替版為什麼會是這種表現。
無遞歸，不程式設計！
遞歸給予了程式語言無限的可能。NMiniKanren也是支援遞歸的。下面我們實作一個方法，這個方法構造的目标要求指定的值或者未知量是一個所有元素都為1的連結清單。
一個值或者未知量的元素都為1，用遞歸的方式表達是：
它是一個空連結清單
或者它的第一個元素是1，且剩餘部分的元素都為1
直譯為代碼就是：
直接運作這段代碼，死循環。
為什麼呢？因為我們直接使用C#的方法來定義函數，C#在構造目标的時候，會運作最後一行的<code>k.AllOne_Wrong(d)</code>，于是就陷入死循環了。
為了避免死循環，在遞歸調用的地方，需要用<code>k.Recurse</code>方法特殊處理一下，讓遞歸的部分變為惰性求值，防止直接調用：
随便構造兩個問題運作一下：
<code>k.Recurse</code>這種處理方法其實是比較醜陋而且不好用的。特别是多個函數互相調用引起遞歸的情況，很可能會漏寫<code>k.Recurse</code>導緻死循環。
聽到這裡，小皮疑惑道：“這個有點醜诶。剛剛網上瞄了下《The Reasoned Schemer》，發現人家的遞歸并不需要這種特殊處理。看起來直接調用就OK了，跟普通程式沒啥兩樣，很美很和諧。”
“因為《The Reasoned Schemer》使用Lisp的宏實作的miniKanren，宏的機制會有類似惰性計算的效果。”老明用擦白闆的抹布拍了下小皮的腦袋，“可惜你不會Lisp。如果你不努力提升自己，那醜一點也隻能将就着看了。”
MiniKanren沒有直接支援數值計算。也就是說，miniKanren不能直接幫你解像<code>2 + x = 5</code>的這種方程。如果要直接支援數值計算，需要實作很多數學相關的運算和變換，會讓miniKanren的實作變得非常複雜。MiniKanren是教學性質的語言，隻支援了最基本的邏輯判斷功能。
“沒有‘直接’支援。”小皮敏銳地發現了關鍵，“也就是可以間接支援咯？”
“沒錯！你想想，0和1是我們支援的符号，與和或也是我們支援的運算符！”老明興奮起來了。
“二進制？”
“是的！任何一本計算機組成原理教程都會教你怎麼做！這裡就不多說了，你可以自己回去試一下。”
“嗯嗯。我以前這門課學得還不錯，現在還記得大概是先實作半加器和全加器，然後構造加法器和乘法器等。”小皮幹勁十足，從底層開始讓他想起了小時候玩泥巴的樂趣。
“而且用miniKanren實作的不是一般的加法器和乘法器，是可以反向運作的加法器和乘法器。”
“有意思，晚上下班回去就去試試。”小皮真心地說。正如他下班回家躺床上後，就再也不想動彈一樣真心實意。
（注：《The Reasoned Schemer》第7章、第8章會講到相關内容。）
“好了，NMiniKanren語言的介紹就先說到這裡了。”老明拍了拍手，看了看前面的例子，撇了撇嘴，“以C#的DSL方式實作出來果然醜很多，文法上都不一緻了。不過核心功能都還在。”
“接下來就是最有意思的部分，NMiniKanren的原理了吧？”
“是的。不過在繼續之前，還有個問題。”
“啥問題？”
“中午米線都用來打碼了。現在肚子餓了，你要請我吃下午茶。”
NMiniKanren的源碼在：https://github.com/sKabYY/NMiniKanren
示例代碼在：https://github.com/sKabYY/NMiniKanren/tree/master/NMiniKaren.Tests