逻辑式编程语言极简实现（使用C#） - 1. 逻辑式编程语言介绍

可可姥姥 發表於 2020-6-28 09:58:00

逻辑式编程语言极简实现（使用C#） - 1. 逻辑式编程语言介绍

相信很多朋友对于逻辑式编程语言，都有一种最熟悉的陌生人的感觉。一方面，平时在书籍、在资讯网站，偶尔能看到一些吹嘘逻辑式编程的话语。但另一方面，也没见过周围有人真正用到它（除了SQL）。
遥记当时看《The Reasoned Schemer》（一本讲逻辑式编程语言的小人书），被最后两页的解释器实现惊艳到了。看似如此复杂的计算逻辑，其实现竟然这么简洁。不过碍于当时水平有限，也就囫囵吞枣般看了过去。后来有一天，不知何故脑子灵光一闪，把图遍历和流计算模式联系在一起，瞬间明白了《The Reasoned Schemer》中的做法。动手写了写代码，果然如此，短短两百来行代码，就完成了解释器的实现，才发现原来如此简单。很多时候，并非问题本身有多难，只是没有想到正确的方法。
本系列将尽可能简洁地说明逻辑式编程语音的原理，并实现一门简单的逻辑式编程语言。考虑到C#的用户较多，因此选择用C#来实现。实现的这门语言就叫NMiniKanren。文章总体内容如下：
<ul>
<li>NMiniKanren语言介绍
<ul>
<li>语言基础</li>
<li>一道有趣的逻辑题：谁是凶手</li>
</ul>
</li>
<li>NMiniKanren运行原理
<ul>
<li>构造条件关系图，遍历分支</li>
<li>代入消元法解未知量</li>
</ul>
</li>
<li>实现NMiniKanren
<ul>
<li>流计算模式简介</li>
<li>代入消元法的实现</li>
<li>遍历分支的实现</li>
</ul>
</li>
</ul>
故事从两个正在吃午餐的程序员说起。
老明和小皮是就职于同一家传统企业的程序员。这天，两人吃着午餐。老明边吃边刷着抖音，鼻孔时不时喷出几条米粉。
小皮是一脸麻木地刷着求职网和资讯网，忽然几个大字映入眼底：《新型逻辑式编程语言重磅出世，即将颠覆IT界！》小皮一阵好奇，往下一翻，结果接着的是一些难懂的话，什么“一阶逻辑”，什么“合一算法”，以及鬼画符似的公式之类。
小皮看得索然无味，但被勾引起来的对逻辑式编程的兴趣仿佛<s>澳洲</s>森林大火一样难以平息。于是伸手拍下老明高举手机的左手，问道：“嘿！逻辑式编程有了解过么？是个啥玩意儿？”
“逻辑式编程啊……嘿嘿，前段时间刚好稍微了解了一下。”老明鼻孔朝天吸了两口气，“我说的稍微了解，是指实现了一门逻辑式编程语言。”
“不愧是资深老IT，了解也比别人深入一坨坨……”
“也就比你早来一年好不好……我是一边看一本奇书一边做的。Dan老师（Dan Friedman）写的《The Reasoned Schemer》。这本书挺值得一看的，书中使用一门教学用的逻辑式编程语言，讲解这门语言的特性、用法、以及原理。最后还给出了这门语言的实现。核心代码只用了两页纸。
<img src="https://img2020.cnblogs.com/blog/576869/202006/576869-20200627220458829-1626404081.jpg" alt="" loading="lazy">
“所谓逻辑式编程，从使用上看是把声明式编程发挥到极致的一种编程范式。普通的编程语言，大部分还是基于命令式编程，需要你告诉机器每一步执行什么指令。而逻辑式编程的理念是，我们只需要告诉机器我们需要的目标，机器会根据这个目标自动探索执行过程。
“逻辑式编程的特点是可以反向运行。你可以像做数学题一样，声明未知量，列出方程，然后程序会为你求解未知量。”
<img src="https://img2020.cnblogs.com/blog/576869/202006/576869-20200627220400214-349321078.png" alt="" loading="lazy">
“挺神奇的。听起来有点像AI编程。不过这么高级的东西怎么没有流行起来？感觉可以节省不少人力。”小皮忽然有种饭碗即将不保的感觉。
“嘿嘿……想得美。其实逻辑式编程，既不智能，也不好用。你回忆一下你中学的时候是怎么解方程组的？”
“嗯……先盯一会方程组，看看它长得像不像有快捷解法的样子。看不出来的话就用代入法慢慢算。这和逻辑式编程有什么关系？”
“逻辑式编程并不智能，它只是把某种类似代入法的通用算法内置到解释器里。逻辑式编程语言写的程序运行时，不过是根据通用算法进行求解而已。它不像人一样会去寻找更快捷的方法，同时也不能解决超纲问题。
<img src="https://img2020.cnblogs.com/blog/576869/202006/576869-20200628095521604-908166855.png" alt="" loading="lazy">
“而且逻辑式编程语言的学习成本也不低。如果你要用好这门语言，你得把它使用的通用算法搞清楚。虽然你写的声明式的代码，但内心要时刻清楚程序的执行过程。如果你拿它当个黑盒来用，那很可能你写出来的程序的执行效率会非常低，甚至跑出一些莫名其妙的结果。”
“哦哦，要学会用它，还得先懂得怎么实现它。这学习成本还挺高的。”小皮跟着吐槽，不过他知道老明表明上看似嫌弃逻辑式编程的实用性，私底下肯定玩得不亦乐乎，并且也喜欢跟别人分享。于是小皮接着道：“虽然应该是用不着，但感觉挺有意思的，再仔细讲讲呗。天天写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！”老明打了个响指，“我们先用简单的例子看看代码结构。”只见老明两指轻轻夹住一只筷子，勾出几条米粉，快速在桌上摆出如下代码：
<pre><code class="language-CSharp">// k提供NMiniKanren的方法，q是待求解的未知变量。
var res = KRunner.Run(null /* null表示输出所有可能的结果 */, (k, q) =>
{
// q == 5 或者 q == 6
return k.Any(
 k.Eq(q, 5),
 k.Eq(q, 6));
});
KRunner.PrintResult(res);// 输出结果：
</code></pre>
“代码中，<code>KRunner.Run</code>用于运行一段NMiniKanren代码，它的声明如下。”老明继续拨动米粉：
<pre><code class="language-CSharp">public class KRunner
{
public static IList<object> Run(int? n, Func<KRunner, FreshVariable, Goal> body)
{
 ...
}
}
</code></pre>
“其中，参数<code>n</code>是返回结果的数量限制，<code>n = null</code>表示无限制；参数<code>body</code>是一个函数：
<ul>
<li>函数的第一个参数是一个<code>KRunner</code>实例，用于引用NMiniKanren方法；</li>
<li>函数的第二个参数是我们将要求解的未知量；</li>
<li>函数的函数体是我们编写的NMiniKanren代码；</li>
<li>函数的返回值为需要满足的约束条件。</li>
</ul>
“接着我们看函数体的代码。<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>个结果。”小皮用筷子改了下代码：
<pre><code class="language-CSharp">// k提供NMiniKanren的方法，q是待求解的未知变量。
var res = KRunner.Run(1 /* 输出1个结果 */, (k, q) =>
{
// q == 5 或者 q == 6
return k.Any(
 k.Eq(q, 5),
 k.Eq(q, 6));
});
KRunner.PrintResult(res);// 输出结果：
</code></pre>
“这样程序只会输出5一个结果。在一些包含递归的代码中，可能会有无穷多个结果，这种情况下需要限制输出结果的数量来避免程序不会终止。”
“原来如此。不过这个例子太简单了，有没有其他更好玩的例子。”
老明喝下一口汤，说：“好。时间不早了，我们回公司找个会议室慢慢说。”
<h2 id="nminikanren支持的数据类型">NMiniKanren支持的数据类型</h2>
到公司后，老明的讲课开始了……
首先，要先明确NMiniKanren支持的数据类型。后续代码都要基于数据类型来编写，所以规定好数据类型是基础中的基础。
简单起见，NMiniKanren只支持四种数据类型：
<ul>
<li><code>string</code>：就是一个普普通通的值类型，仅有值相等判断。</li>
<li><code>int</code>：同<code>string</code>。使用<code>int</code>是因为有时候想少写两个双引号……</li>
<li><code>KPair</code>：二元组。可用来构造链表及其他复杂的数据结构。如果你学过Lisp会对这个数据结构很熟悉。下面详细说明。</li>
<li><code>null</code>：这个类型只有<code>null</code>一个值。表示空引用或者空数组。</li>
</ul>
<h3 id="kpair类型">KPair类型</h3>
<code>KPair</code>的定义为：
<pre><code class="language-CSharp">public class KPair
{
public object Lhs { get; set; }
public object Rhs { get; set; }

// methods
...
}
</code></pre>
<code>KPair</code>除了用作二元组（其实是最少用的）外，更多的是用来构造链表。构造链表时，约定一个<code>KPair</code>作为一个链表的节点，<code>Lhs</code>为元素值，<code>Rhs</code>为一下个节点。当<code>Rhs</code>为<code>null</code>时链表结束。空链表用<code>null</code>表示。
<pre><code class="language-CSharp">public static KPair List(IEnumerable<object> lst)
{
var fst = lst.FirstOrDefault();
if (fst == null)
{
 return null;
}
return new KPair(fst, List(lst.Skip(1)));
}
</code></pre>
<blockquote>
使用<code>null</code>表示空链表其实并不合适，这里纯粹是为了简单而偷了个懒。
</blockquote>
<img src="https://img2020.cnblogs.com/blog/576869/202006/576869-20200628095545819-189774916.png" alt="" loading="lazy">
我们知道，很多复杂的数据结构都是可以通过链表来构造的。所以虽然NMiniKanren只有三种数据类型，但可以表达很多数据结构了。
这时候小皮有疑问了：“C#本身已经自带了<code>List</code>等容器了，为什么还要用<code>KPair</code>来构造链表？”
“为了让底层尽可能简洁。”老明说道，“我们都知道，程序本质上分为数据结构和算法。算法是顺着数据结构来实现的。简洁的数据结构会让算法的实现显得更清晰。相比C#自带的<code>List</code>，使用<code>KPair</code>构造的链表更加清晰简洁。按照构造的方式，我们的链表定义为：
<ol>
<li>空链表<code>null</code>；</li>
<li>或者是非空链表。它的第一个元素为<code>Lhs</code>，并且<code>Rhs</code>是后续的链表。</li>
</ol>
“链表相关的算法都会顺着定义的这两个分支实现：一个处理空链表的分支，一个处理非空链表的递归代码。比如说判断一个变量是不是链表的方法：
<pre><code class="language-CSharp">public static bool IsList(object o)
{
// 空链表
if (o == null)
{
 return true;
}
// 非空链表
if (o is KPair p)
{
 // 递归
 return IsList(p.Rhs);
}
// 非链表
return false;
}
</code></pre>
“以及判断一个元素是不是在链表中的方法：
<pre><code class="language-CSharp">public static bool Memeber(object lst, object e)
{
// 空链表
if (lst == null)
{
 return false;
}
// 非空链表
if (lst is KPair p)
{
 if (p.Lhs == null && e == null || p.Lhs.Equals(e))
 {
 return true;
 }
 else
 {
 // 递归
 return Memeber(p.Rhs, e);
 }
}
// 非链表
return false;
}
</code></pre>
“数据类型明确后，接下来我们来看看NMiniKanren能做什么。”
<h2 id="目标goal">目标（Goal）</h2>
编写NMiniKanren代码是一个构造目标（<code>Goal</code>类型）的过程。NMiniKanren解释器运行时将求解使得目标成立的所有未知量的值。
显然，有两个平凡的目标：
<ul>
<li><code>k.Succeed</code>：永远成立，未知量可取任意值。</li>
<li><code>k.Fail</code>：永远不成立，无论未知量为何值都不成立。</li>
</ul>
其中<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>成立；否则不成立。
这里的相等，指的是值相等：
<ul>
<li>不同类型不相等。</li>
<li><code>string</code>类型相等当且仅当值相等。</li>
<li><code>KPair</code>类型相等当且仅当它们的<code>Lhs</code>相等且<code>Rhs</code>相等。</li>
</ul>
从<code>KPair</code>相等的定义，可以推出由<code>KPair</code>构造的数据结构（比如链表），相等条件为当且仅当它们结构一样且对应的值相等。
接下来我们看几个例子。
<h3 id="等于一个值">等于一个值</h3>
<pre><code class="language-CSharp">KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
return k.Eq(q, 5);
}));// 输出
</code></pre>
直接<code>q</code>等于<code>5</code>。
<h3 id="等于一个链表">等于一个链表</h3>
<pre><code class="language-CSharp">KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
return k.Eq(q, k.List(1, 2));
}));// 输出[(1 2)]
</code></pre>
<code>k.List(1, 2)</code>相当于<code>new KPair(1, new KPair(2, null))</code>，用来快速构造链表。
<h3 id="链表间的相等">链表间的相等</h3>
<pre><code class="language-CSharp">KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
return k.Eq(k.List(1, q), k.List(1, 2));
}));// 输出
</code></pre>
这个例子比较像一个方程了。<code>q</code>匹配<code>k.List(1, 2)</code>的第二项，也就是<code>2</code>。
<h3 id="无法相等的例子">无法相等的例子</h3>
<pre><code class="language-CSharp">KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
return k.Eq(k.List(2, q), k.List(1, 2));
}));// 输出[]
</code></pre>
由于<code>k.List(2, q)</code>的第一项和<code>k.List(1, 2)</code>的第一项不相等，所以这个目标无法成立，<code>q</code>没有值。
<h3 id="不成立的例子">不成立的例子</h3>
<pre><code class="language-CSharp">KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
return k.Fail;
}));// 输出[]
</code></pre>
目标无法成立，<code>q</code>没有值。
<h3 id="永远成立的例子">永远成立的例子</h3>
<pre><code class="language-CSharp">KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
return k.Succeed;
}));// 输出
</code></pre>
目标恒成立，<code>q</code>可取任意值。输出<code>_0</code>表示一个可取任意值的自由变量。
<h2 id="更多构造目标的方式">更多构造目标的方式</h2>
目标可以看作布尔表达式，因此可以通过“与或非”运算，用简单的目标构造成复杂的“组合”目标。我们把被用来构造“组合”目标的目标叫做该“组合”目标的子目标。
<h3 id="定义未知量">定义未知量</h3>
在前面的例子中，我们只有一个未知量<code>q</code>。<code>q</code>既是未知量，也是程序输出。
在处理更复杂的问题时，通常需要定义更多的未知量。定义未知量的方法是<code>k.Fresh</code>：
<pre><code class="language-CSharp">// 定义x, y两个未知量
var x = k.Fresh()
var y = k.Fresh()
</code></pre>
新定义的未知量和<code>q</code>一样，可以用来构造目标：
<pre><code class="language-CSharp">// x == 2
k.Eq(x, 2)
// x == y
k.Eq(x, y)
</code></pre>
<h3 id="与">与</h3>
使用“与”运算组合的目标，仅当所有子目标成立时，目标才成立。
使用方法<code>k.All</code>来构造“与”运算组合的目标。
<pre><code class="language-CSharp">var g = k.All(g1, g2, g3, ...)
</code></pre>
当且仅当<code>g1</code>, <code>g2</code>, <code>g3</code>, ......，都成立时，<code>g</code>才成立。
特别的，空子目标的情况，即<code>k.All()</code>，恒成立。
<h4 id="例">例</h4>
<pre><code class="language-CSharp">KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
return k.All(
 k.Eq(q, 1),
 k.Eq(q, 2));
}));// 输出[]

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
var x = k.Fresh();
var y = k.Fresh();
return k.All(
 k.Eq(x, 1),
 k.Eq(y, x),
 k.Eq(q, k.List(x, y)));
}));// 输出[(1 1)]
</code></pre>
<h3 id="或">或</h3>
使用“或”运算组合的目标，只要一个子目标成立时，目标就成立。
使用方法<code>k.Any</code>来构造“或”运算组合的目标。
<pre><code class="language-CSharp">var g = k.Any(g1, g2, g3, ...)
</code></pre>
当<code>g1</code>, <code>g2</code>, <code>g3</code>, ......中至少一个成立，<code>g</code>成立。
特别的，空子目标的情况，即<code>k.Any()</code>，恒不成立。
<h4 id="例-1">例</h4>
<pre><code class="language-CSharp">KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
return k.Any(
 k.Eq(q, 5),
 k.Eq(q, 6));
}));// 输出

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
var x = k.Fresh();
var y = k.Fresh();
return k.All(
 k.Any(k.Eq(x, 5), k.Eq(y, 6)),
 k.Eq(q, k.List(x, y)));
}));// 输出[(5 _0), (_0 6)]
</code></pre>
<h3 id="非">非？</h3>
MiniKanren（以及NMiniKanren）不支持“非”运算。支持“非”会让miniKanren的实现复杂很多。
这或许令人惊讶。“与或非”在逻辑代数中一直像是连体婴儿似的扎堆出现。并且“非”运算是单目运算符，看起来应该更简单。
然而，“与”和“或”运算是在已知的两（多）个集合中取交集或者并集，结果也是已知的。而“非”运算则是把一个已知的集合映射到可能未知的集合，遍历“非”运算的结果可能会很久或者就是不可能的。
对于基于图搜索和代入法求解的miniKanren来说，支持“非”运算需要对核心的数据结构和算法做较大改变。因此以教学为目的的miniKanren没有支持“非”运算。
不过，在一定程度上，也是有不完整替代方法的。
<h3 id="if这个比较奇葩可以先跳过">If（这个比较奇葩，可以先跳过）</h3>
If是一个特殊的构造目标的方式。对应《The Reasoned Schemer》中的<code>conda</code>。
<pre><code class="language-CSharp">var g = k.If(g1, g2, g3)
</code></pre>
如果<code>g1</code>且<code>g2</code>成立，那么<code>g</code>成立；否则当且仅当<code>g3</code>成立时，<code>g</code>成立。
这个和<code>k.Any(k.All(g1, g2), g3)</code>很像，但他们是有区别的：
<ul>
<li><code>k.Any(k.All(g1, g2), g3)</code>会解出所有让<code>k.All(g1, g2)</code>或者<code>g3</code>成立的解</li>
<li><code>k.If(g1, g2, g3)</code>如果<code>k.All(g1, g2)</code>有解，那么只给出使<code>k.All(g1, g2)</code>成立的解；否则再求使得<code>g3</code>成立的解。</li>
</ul>
也可以说，If是短路的。
这么诡异的特性有什么用呢？
它可以部分地实现“非”运算的功能：
<pre><code class="language-CSharp">k.If(g, k.Fail, k.Succeed)
</code></pre>
这个这里先不详细展开了，后面用到再说。
<h2 id="控制输出顺序">控制输出顺序</h2>
这是一个容易被忽略的问题。如果程序需要求出所有的解，那么输出顺序影响不大。但是一些情况下，求解速度很慢，或者解的数量太多甚至无穷，这时只求前几个解，那么输出的内容就和输出顺序有关了。
因为miniKanren以图遍历的方式来查找问题的解，所以解的顺序其实也是解释器运行时遍历的顺序。先看如下例子：
<pre><code class="language-CSharp">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, "a"), k.Eq(y, "b")),
 k.Eq(q, k.List(x, y)));
}));// 输出[(1 a), (1 b), (2 a), (2 b)]
</code></pre>
有两个未知变量<code>x</code>和<code>y</code>，<code>x</code>可能的取值为1或2，<code>y</code>可能的取值为a或b。可以看到，程序查找解的顺序为：
<ul>
<li><code>x</code>值为1
<ul>
<li><code>y</code>值为a，<code>q=(1 a)</code></li>
<li><code>y</code>值为b，<code>q=(1 b)</code></li>
</ul>
</li>
<li><code>x</code>值为2
<ul>
<li><code>y</code>值为a，<code>q=(2 a)</code></li>
<li><code>y</code>值为b，<code>q=(2 b)</code></li>
</ul>
</li>
</ul>
如果要改变这个顺序，我们有一个交替版的“与”运算<code>k.Alli</code>：
<pre><code class="language-CSharp">KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
var x = k.Fresh();
var y = k.Fresh();
return k.Alli(
 k.Any(k.Eq(x, 1), k.Eq(x, 2)),
 k.Any(k.Eq(y, "a"), k.Eq(y, "b")),
 k.Eq(q, k.List(x, y)));
}));// 输出[(1 a), (2 a), (1 b), (2 b)]
</code></pre>
不过这个交替版也不是交替得很漂亮。下面增加<code>x</code>可能的取值到3个：
<pre><code class="language-CSharp">KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
var x = k.Fresh();
var y = k.Fresh();
return k.Alli(
 k.Any(k.Eq(x, 1), k.Eq(x, 2), k.Eq(x, 3)),
 k.Any(k.Eq(y, "a"), k.Eq(y, "b")),
 k.Eq(q, k.List(x, y)));
}));// 输出[(1 a), (2 a), (1 b), (3 a), (2 b), (3 b)]
</code></pre>
同样，“或”运算也有交替版。
正常版：
<pre><code class="language-CSharp">KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
return k.Any(
 k.Any(k.Eq(q, 1), k.Eq(q, 2)),
 k.Any(k.Eq(q, 3), k.Eq(q, 4)));
}));// 输出
</code></pre>
交替版：
<pre><code class="language-CSharp">KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
return k.Anyi(
 k.Any(k.Eq(q, 1), k.Eq(q, 2)),
 k.Any(k.Eq(q, 3), k.Eq(q, 4)));
}));// 输出
</code></pre>
后面讲到miniKanren实现原理时会解释正常版、交替版为什么会是这种表现。
<h2 id="递归">递归</h2>
无递归，不编程！
递归给予了程序语言无限的可能。NMiniKanren也是支持递归的。下面我们实现一个方法，这个方法构造的目标要求指定的值或者未知量是一个所有元素都为1的链表。
<h3 id="错误的示范">错误的示范</h3>
一个值或者未知量的元素都为1，用递归的方式表达是：
<ol>
<li>它是一个空链表</li>
<li>或者它的第一个元素是1，且剩余部分的元素都为1</li>
</ol>
直译为代码就是：
<pre><code class="language-CSharp">public static Goal AllOne_Wrong(this KRunner k, object lst)
{
var d = k.Fresh();
return k.Any(
 // 空链表
 k.Eq(lst, null),
 // 非空
 k.All(
 k.Eq(lst, k.Pair(1, d)),// 第一个元素是1
 k.AllOne_Wrong(d)));// 剩余部分的元素都是1
}
</code></pre>
直接运行这段代码，死循环。
为什么呢？因为我们直接使用C#的方法来定义函数，C#在构造目标的时候，会运行最后一行的<code>k.AllOne_Wrong(d)</code>，于是就陷入死循环了。
<h3 id="正确的做法">正确的做法</h3>
为了避免死循环，在递归调用的地方，需要用<code>k.Recurse</code>方法特殊处理一下，让递归的部分变为惰性求值，防止直接调用：
<pre><code class="language-CSharp">public static Goal AllOne(this KRunner k, object lst)
{
var d = k.Fresh();
return k.Any(
 k.Eq(lst, null),
 k.All(
 k.Eq(lst, k.Pair(1, d)),
 k.Recurse(() => k.AllOne(d))));
}
</code></pre>
随便构造两个问题运行一下：
<pre><code class="language-CSharp">KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
var x = k.Fresh();
var y = k.Fresh();
return k.All(
 k.AllOne(k.List(1, x, y, 1)),
 k.Eq(q, k.List(x, y)));
}));// 输出[(1 1)]

KRunner.PrintResult(KRunner.Run(null, (k, q) =>
{
var x = k.Fresh();
var y = k.Fresh();
return k.All(
 k.AllOne(k.List(1, x, y, 0)),
 k.Eq(q, k.List(x, y)));
}));// 输出[]
</code></pre>
<code>k.Recurse</code>这种处理方法其实是比较丑陋而且不好用的。特别是多个函数相互调用引起递归的情况，很可能会漏写<code>k.Recurse</code>导致死循环。
听到这里，小皮疑惑道：“这个有点丑诶。刚刚网上瞄了下《The Reasoned Schemer》，发现人家的递归并不需要这种特殊处理。看起来直接调用就OK了，跟普通程序没啥两样，很美很和谐。”
“因为《The Reasoned Schemer》使用Lisp的宏实现的miniKanren，宏的机制会有类似惰性计算的效果。”老明用擦白板的抹布拍了下小皮的脑袋，“可惜你不会Lisp。如果你不努力提升自己，那丑一点也只能将就着看了。”
<h2 id="关于数值计算">关于数值计算</h2>
MiniKanren没有直接支持数值计算。也就是说，miniKanren不能直接帮你解像<code>2 + x = 5</code>的这种方程。如果要直接支持数值计算，需要实现很多数学相关的运算和变换，会让miniKanren的实现变得非常复杂。MiniKanren是教学性质的语言，只支持了最基本的逻辑判断功能。
“没有‘直接’支持。”小皮敏锐地发现了关键，“也就是可以间接支持咯？”
“没错！你想想，0和1是我们支持的符号，与和或也是我们支持的运算符！”老明兴奋起来了。
“二进制？”
“是的！任何一本计算机组成原理教程都会教你怎么做！这里就不多说了，你可以自己回去试一下。”
“嗯嗯。我以前这门课学得还不错，现在还记得大概是先实现半加器和全加器，然后构造加法器和乘法器等。”小皮干劲十足，从底层开始让他想起了小时候玩泥巴的乐趣。
“而且用miniKanren实现的不是一般的加法器和乘法器，是可以反向运行的加法器和乘法器。”
“有意思，晚上下班回去就去试试。”小皮真心地说。正如他下班回家躺床上后，就再也不想动弹一样真心实意。
（注：《The Reasoned Schemer》第7章、第8章会讲到相关内容。）
<h2 id="小结">小结</h2>
“好了，NMiniKanren语言的介绍就先说到这里了。”老明拍了拍手，看了看前面的例子，撇了撇嘴，“以C#的DSL方式实现出来果然丑很多，语法上都不一致了。不过核心功能都还在。”
“接下来就是最有意思的部分，NMiniKanren的原理了吧？”
“是的。不过在继续之前，还有个问题。”
“啥问题？”
“中午米线都用来打码了。现在肚子饿了，你要请我吃下午茶。”
<hr>
NMiniKanren的源码在：https://github.com/sKabYY/NMiniKanren
示例代码在：https://github.com/sKabYY/NMiniKanren/tree/master/NMiniKaren.Tests 
来源：https://www.cnblogs.com/skabyy/p/13199800.html

頁: [1]

琼殿技术论坛's Archiver

逻辑式编程语言极简实现（使用C#） - 1. 逻辑式编程语言介绍