本文是本系列的完结篇. 本系列前面的文章:
逻辑式编程语言极简实现(使用 C#) - 1. 逻辑式编程语言介绍
逻辑式编程语言极简实现(使用 C#) - 2. 一道逻辑题: 谁是凶手
逻辑式编程语言极简实现(使用 C#) - 3. 运行原理
下午, 吃饱饭的老明和小皮, 各拿着一杯刚买的咖啡回到会议室, 开始了逻辑式编程语言的最后一课.
老明喝了一口咖啡, 说:"你看咖啡机, 是不是咖啡的列表."
"啥?" 小皮有点懵圈,"你说工厂的话还好理解, 列表不太像."
"每次点一下按钮, 就相当于调用了一次 next, 出来一杯咖啡. 而它本身并不包含咖啡, 每一次都是现场磨豆冲出来的. 这正是一个典型的惰性列表."
- "有点道理, 但是这跟逻辑式编程语言解释器有什么关系呢?"
- "这就是下面要说的流计算模式, 它是实现分支遍历的核心技巧."
下面先讲流计算模式, 然后再讲替换求解的实现与分支遍历的实现.
流 (Stream) 计算模式
老明在白板上写下 "Stream", 说:"Stream 最常见的用途是用来表示数量未知或者无穷的列表. 在代码中怎么定义流呢? 我们先来看看自然数, 自然数是无穷的, 那我们怎么定义自然数列呢?"
"这很显然, 不就是 0,1,2,3,4,5 等等吧."
老明鄙夷地看着小皮, 说:"如果我是你的数学老师, 那我肯定要罚你站在墙角数完所有自然数...... 想想数学归纳法!"
" 哦哦, 哎! 数学这些乌漆嘛黑的知识总是喜欢偷偷溜走. 自然数的定义简单来说(严谨的不会), 由两部分组成:
(起点部分)0 是自然数;
(递归部分)任意自然数加 1 也是自然数.
"这样我们根据第 1 部分, 得到起点 0; 再根据第 2 部分, 一直加 1, 依次得到 1,2,3,4,5 等自然数."
"看来基础还是不错的." 老明微笑着点点头, 然后开始进入正文......
从自然数的定义, 我们可以得到启发, Stream 的定义也是由两部分组成:
起点: 第一个元素(非空流);
递归: 一个无参函数, 调用它会返回这个 Stream 去掉第一个元素后剩下部分组成的剩余 Stream.
第 2 部分之所以是个函数, 是为了获得惰性的效果, 仅当需要时才计算剩余的 Stream.
使用代码定义 Stream 如下:
- public delegate Stream DelayedStream();
- // Stream 的定义, 我们只会用到替换的 Stream, 所以这里就不做泛型了.
- public class Stream
- {
- // 第一个元素, 类型为 Substitution(替换)
- public Substitution Curr { get; set; }
- // 获取剩余 Stream 的方法
- public DelayedStream GetRest { get; set; }
- private static Stream MakeStream(Substitution curr, DelayedStream getRest)
- {
- return new Stream()
- {
- Curr = curr,
- GetRest = getRest
- };
- }
- ...
- }
其中 Substitution 是替换类, 后面会讲到这个类的实现.
还需要定义一个空 Stream, 除了表示空以外, 还用来作为有限 Stream 的结尾. 空 Stream 是一个特殊的单例.
正常来讲, 空 Stream 应该额外声明一个类型. 这里偷了个懒.
- private Stream() { }
- private static readonly Stream theEmptyStream = new Stream();
- public bool IsEmpty()
- {
- return this == theEmptyStream;
- }
- public static Stream Empty()
- {
- return theEmptyStream;
- }
特别的, 还需要一个构造单元素的 Stream 的方法:
- public static Stream Unit(Substitution sub)
- {
- return MakeStream(sub, () => Empty());
- }
只有这些平凡的构造方法还看不出 Stream 的用处, 接下来结合前面讲过的 NMiniKanren 运行原理, 探索如何使用 Stream 来实现替换的遍历.
Append 方法
回顾一下 Any 的运行原理, Any 的每个参数会各自返回一个 Stream. 这些 Stream 代表了各个参数包含的可能性. Any 操作把所有可能性放在一起, 也就是把这些 Stream 拼在一起组成一个长长的 Stream.
所以相应的, 我们需要把两个 Stream s1 和 s2 拼接成一个 "长"Stream 的 Append 方法.
如何构造这个 "长"Stream 呢?
首先, 如果 s1 是空 Stream, 那么拼接后的 Stream 显然就是 s2.
否则, 按照 Stream 定义, 分两个部分进行构造:
第一个元素, 显然就是 s1 的第一个元素;
剩余 Stream, 就是 s1 的剩余 Stream, 拼上 s2, 这里是个递归定义.
按照上面分析的构造方法, 我们就能轻松地写下代码:
- public Stream Append(DelayedStream f)
- {
- if (IsEmpty()) return f();
- return MakeStream(Curr, () => GetRest().Append(f));
- }
在这个实现中, f 是尚未计算的 s2. 我们需要尽量推迟 s2 第一个元素的计算, 因为推迟着推迟着可能就没了不用算了. 在很多场景中, 这个可以节省不必要的计算, 甚至避免死循环("这都是血泪教训." 老明捂脸).
下面是一个 Any 与 Append 的例子:
Interleave 方法
Anyi 和 Any 的区别只有顺序. Anyi 使用交替的顺序.
所以相应的, 我们需要一个方法, 这个方法把两个 Stream s1 和 s2 中的元素交替地拼接组成一个 "长"Stream.
首先, 如果 s1 是空 Stream, 那么 "长"Stream 显然就是 s2.
否则, 分两部分构造:
第一个元素是 s1 的第一个元素;
这里和 Append 方法的区别是把 s1 和 s2 的位置调换了, 剩余 Stream 是 s2 交替拼上 s1 的剩余 Stream, 同样是个递归定义.
代码如下:
- public Stream Interleave(DelayedStream f)
- {
- if (IsEmpty()) return f();
- return MakeStream(Curr, () => f().Interleave(GetRest));
- }
这里使用惰性的 f 是非常必要的, 因为我们不希望取剩余 Stream 的时候调用 GetRest.
Bind 方法
这个方法比较复杂, 是对应到 All 运算中两两组合参数里的分支的过程.
不同于 Append/Interleave 作用在两个 Stream 上, Bind 方法作用在一个 Stream 和一个 Goal 上.
为什么不是两个 Stream 呢?
前面已经分析过了, k.All(g1, g2)这个运算, 是把 g2 蕴含的条件, 追加到 g1 所包含的 Stream 中的每个替换里.
同时, g2 是个函数. 追加这个动作本身由 g2 表达.
举例来说, 假设 st 是 g1 所包含的 Stream 中的一个替换. 那么把 g2 蕴含的条件追加到 st 上, 其结果为 g2(st).
正是因为 Bind 方法中需要有追加条件这个动作, 所以 Bind 方法的第二个参数只能是既包含了条件内容, 也包含了追加方法的 Goal 类型.
用记号 s1 表示 g1 所包含的 Stream,Bind 方法的作用就是把 g2 蕴含的条件追加到 s1 中的每个替换里.
首先, 如果 s1 是个空 Stream, 那显然 Bind 的结果是空 Stream.
否则, 结果是 s1 的第一个元素追加 g2, 再拼上 s1 的剩余 Stream Bind g2 的结果. 这仍是递归定义, 不过是借助的 Append 方法进行 Stream 构造.
代码如下:
- public Stream Bind(Goal g)
- {
- if (IsEmpty()) return Empty();
- return g(Curr).Append(() => GetRest().Bind(g));
- }
这个方法为什么叫 Bind, 因为取名废只好抄《The Reasoned Schemer》里的命名......
下面是一个 All 与 Bind 的例子:
Bindi 方法
对应 Alli, 交替版的 Bind 方法. 代码实现不再多说, 直接把 Bind 实现中的 Append 换成 Interleave 即可:
- public Stream Bindi(Goal g)
- {
- if (IsEmpty()) return Empty();
- return g(Curr).Interleave(() => GetRest().Bindi(g));
- }
更多 Stream 的玩法, 参见《计算机程序的构造和解释》(简称《SICP》)第三章.
替换求解的实现
构造目标时会用到替换里的方法, 所以和上一篇顺序相反, 先讲替换求解.
替换
替换的定义为:
- public class Substitution
- {
- private readonly Substitution parent;
- public FreshVariable Var { get; }
- public object Val { get; }
- private Substitution(Substitution p, FreshVariable var, object val)
- {
- parent = p;
- Var = var;
- Val = val;
- }
- private static readonly Substitution theEmptySubstitution = new Substitution(null, null, null);
- public static Substitution Empty()
- {
- return theEmptySubstitution;
- }
- public bool IsEmpty()
- {
- return this == theEmptySubstitution;
- }
- public Substitution Extend(FreshVariable var, object val)
- {
- return new Substitution(this, var, val);
- }
- public bool Find(FreshVariable var, out object val)
- {
- if (IsEmpty())
- {
- val = null;
- return false;
- }
- if (Var == var)
- {
- val = Val;
- return true;
- }
- return parent.Find(var, out val);
- }
- ...
- }
这是个单链表的结构. 我们需要能在替换中追根溯源地查找未知量的值的方法(也就是将条件代入到未知量):
- public object Walk(object v)
- {
- if (v is KPair p)
- {
- return new KPair(Walk(p.Lhs), Walk(p.Rhs));
- }
- if (v is FreshVariable var && Find(var, out var val))
- {
- return Walk(val);
- }
- return v;
- }
例如在替换 (x=1, q=(x y), y=x) 中, Walk(q)返回(1 1).
注意替换结构里面, 条件都是未知量 = 值的形式. 但是在 NMiniKanren 代码中并非所有条件都是这种形式. 所以在追加条件时, 需要先将条件转化为未知量 = 值的形式.
追加条件时, 不是简单的使用 Extend 方法, 而是用 Unify 方法. Unify 方法结合了 Extend 和代入消元法. 它先将已有条件代入到新条件中, 然后再把代入后的新条件转化为未知量 = 值的形式:
- public Substitution Unify(object v1, object v2)
- {
- v1 = Walk(v1); // 使用已知条件代入到 v1
- v2 = Walk(v2); // 使用已知条件代入到 v2
- if (v1 is KPair p1 && v2 is KPair p2)
- {
- return Unify(p1.Lhs, p2.Lhs)?.Unify(p1.Rhs, p2.Rhs);
- }
- if (v1 is FreshVariable var1)
- {
- return Extend(var1, v2);
- }
- if (v2 is FreshVariable var2)
- {
- return Extend(var2, v1);
- }
- // 两边都是值. 值相等的话替换不变; 值不相等返回 null 表示矛盾.
- if (v1 == null)
- {
- if (v2 == null) return this;
- } else
- {
- if (v1.Equals(v2)) return this;
- }
- return null;
- }
Unify 方法实现了代入消元的第一遍代入(详情见上一篇).Unify 的全拼是 unification, 中文叫合一.
求解
由于 NMiniKanren 的输出只有未知量 q, 所以第二遍代入的过程只需要查找 q 的值即可:
Walk(q)
构造目标的实现
通过 Stream 的分析, 我们知道, 只要构造了目标, 自然就实现了分支的遍历.
Success 与 Fail
任何替换追加 Success, 相当于没追加, 所以 k.Success 直接返回一个只包含上下文的 Stream:
public Goal Succeed = sub => Stream.Unit(sub);
任何替换追加 Fail, 那它这辈子就完了, k.Fail 直接返回空 Stream
- public Goal Fail => sub => Stream.Empty();
- Eq
k.Eq(v1, v2)向上下文追加 v1 == v2 条件.
首先, 使用 Unify 方法将 v1 == v2 条件扩展到上下文代表的替换.
若扩展后的替换出现矛盾, 表示无解, 返回空 Stream.
否则返回只包含扩展后的替换的 Stream.
代码如下:
- public Goal Eq(object v1, object v2)
- {
- return sub =>
- {
- var u = sub.Unify(v1, v2);
- if (u == null)
- {
- return Stream.Empty();
- }
- return Stream.Unit(u);
- };
- }
- Any/Anyi
首先, 利用 Stream.Append 实现二目运算版本的 Or:
- public Goal Or(Goal g1, Goal g2)
- {
- return sub => g1(sub).Append(() => g2(sub));
- }
然后扩展到多参数:
- public Goal Any(params Goal[] gs)
- {
- if (gs.Length == 0) return Fail;
- if (gs.Length == 1) return gs[0];
- return Or(gs[0], Any(gs.Skip(1).ToArray()));
- }
同理实现 Ori 和 Anyi:
- public Goal Ori(Goal g1, Goal g2)
- {
- return sub => g1(sub).Interleave(() => g2(sub));
- }
- public Goal Anyi(params Goal[] gs)
- {
- if (gs.Length == 0) return Fail;
- if (gs.Length == 1) return gs[0];
- return Ori(gs[0], Anyi(gs.Skip(1).ToArray()));
- }
- All/Alli
利用 Stream.Bind 实现二目版本的 And:
- public Goal And(Goal g1, Goal g2)
- {
- return sub => g1(sub).Bind(g2);
- }
然后扩展到多参数:
- public Goal All(params Goal[] gs)
- {
- if (gs.Length == 0) return Succeed;
- if (gs.Length == 1) return gs[0];
- return And(gs[0], All(gs.Skip(1).ToArray()));
- }
同理实现 Andi 和 Alli:
- public Goal Andi(Goal g1, Goal g2)
- {
- return sub => g1(sub).Bindi(g2);
- }
- public Goal Alli(params Goal[] gs)
- {
- if (gs.Length == 0) return Succeed;
- if (gs.Length == 1) return gs[0];
- return Andi(gs[0], All(gs.Skip(1).ToArray()));
- }
串起来运行, 以及一些细枝末节
- public static IList<object> Run(int? n, Func<KRunner, FreshVariable, Goal> body)
- {
- var k = new KRunner();
- // 定义待求解的未知量 q
- var q = k.Fresh();
- // 执行 body, 得到最终目标 g
- var g = body(k, q);
- // 初始上下文是一个空替换, 应用到 g, 得到包含可行替换的 Stream s
- var s = g(Substitution.Empty());
- // 从 s 中取出前 n 个 (n==null 则取所有) 替换, 查找各个替换下 q 的解, 并给自由变量换个好看的符号.
- return s.MapAndTake(n, sub => Renumber(sub.Walk(q)));
- }
其中, MapAndTake 方法取 Stream 的前 n 个 (或所有) 值, 并 map 每一个值.
Renumber 将自由变量替换成_0,_1...... 这类符号.
NMiniKanren 的完整代码在这里: https://github.com/sKabYY/NMiniKanren
结尾
总结一下 NMiniKanren 的原理:
NMiniKanren 代码描述的是一个 Goal.Goal 是一个替换到 Stream 的函数.
从 NMiniKanren 代码可以构建一张描述了条件关系的图. 每条路径对应一个替换, 使用流计算模式可以很巧妙地实现对所有路径的遍历.
使用代入消元法求解未知量.
另外 NMiniKanren 毕竟只是一门教学级的语言, 实用上肯定一塌糊涂, 说难听点也就是个玩具. 我们学习的重点不在于 NMiniKanren, 而在于实现 NMiniKanren 的过程中所用到的技术和思想. 掌握了这些方法后, 可以根据自己的需要进行优化或扩展, 或者将这些方法应用到其他问题上.
"神奇!" 小皮瞪着眼睛摸摸脑袋, 以前觉得宛若天书般的逻辑式编程语言就这么学完了, 还包括了解释器的实现.
"认真学习了一天半的效果还是不错了. 嘿嘿." 老明欣慰地拍了拍小皮的肩膀, 微微笑道,"世上无难事, 只怕有心人. 恰好今天周五了, 周末就来公司把这两天落下的工作补完吧."
小皮:"???"
PS: 最后, 用《The Reasoned Schemer》里的两页实现镇楼. 俗话说得好, C# 只是恰饭, 真正的快乐还得看 Scheme/Lisp.
来源: https://www.cnblogs.com/skabyy/p/13232933.html