平心在线:逻辑式编程语言极简实现(使用C#) - 4. 代码实现(完结)

admin 1天前 科技 46 1

本文是本系列的完结篇。本系列前面的文章:

  • 逻辑式编程语言极简实现(使用C#) - 1. 逻辑式编程语言先容
  • 逻辑式编程语言极简实现(使用C#) - 2. 一道逻辑题:谁是凶手
  • 逻辑式编程语言极简实现(使用C#) - 3. 运行原理

下昼,吃饱饭的老明和小皮,各拿着一杯刚买的咖啡回到会议室,最先了逻辑式编程语言的最后一课。

老明喝了一口咖啡,说:“你看咖啡机,是不是咖啡的列表。”

“啥?”小皮有点懵圈,“你说工厂的话还好明白,列表不太像。”

“每次点一下按钮,就相当于挪用了一次next,出来一杯咖啡。而它自己并不包罗咖啡,每一次都是现场磨豆冲出来的。这正是一个典型的惰性列表。”

“有点原理,然则这跟逻辑式编程语言注释器有什么关系呢?”

“这就是下面要说的流盘算模式,它是实现分支遍历的焦点技巧。”

下面先讲流盘算模式,然后再讲替换求解的实现与分支遍历的实现。

流(Stream)盘算模式

老明在白板上写下“Stream”,说:“Stream最常见的用途是用来示意数目未知或者无限的列表。在代码中怎么界说流呢?我们先来看看自然数,自然数是无限的,那我们怎么界说自然数列呢?”

“这很显然,不就是0、1、2、3、4、5等等吧。”

老明鄙夷地看着小皮,说:“若是我是你的数学老师,那我一定要罚你站在墙角数完所有自然数……想想数学归纳法!”

“哦哦,哎!数学这些乌漆嘛黑的知识总是喜欢偷偷溜走。自然数的界说简朴来说(严谨的不会),由两部门组成:

  1. (起点部门)0是自然数;
  2. (递归部门)随便自然数加1也是自然数。

“这样我们凭据第1部门,获得起点0;再凭据第2部门,一直加1,依次获得1、2、3、4、5等自然数。”

“看来基础照样不错的。”老明微笑着点点头,然后最先进入正文……

从自然数的界说,我们可以获得启发,Stream的界说也是由两部门组成

  1. 起点:第一个元素(非空流);
  2. 递归:一个无参函数,挪用它会返回这个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 s1s2拼接成一个“长”Stream的Append方式。

若何组织这个“长”Stream呢?

首先,若是s1是空Stream,那么拼接后的Stream显然就是s2

否则,根据Stream界说,分两个部门举行组织:

  1. 第一个元素,显然就是s1的第一个元素;
  2. 剩余Stream,就是s1的剩余Stream,拼上s2,这里是个递归界说。

根据上面剖析的组织方式,我们就能轻松地写下代码:

public Stream Append(DelayedStream f)
{
    if (IsEmpty()) return f();
    return MakeStream(Curr, () => GetRest().Append(f));
}

在这个实现中,f是尚未盘算的s2。我们需要只管推迟s2第一个元素的盘算,由于推迟着推迟着可能就没了不用算了。在许多场景中,这个可以节约不需要的盘算,甚至制止死循环(“这都是血泪教训。”老明捂脸)。

下面是一个AnyAppend的例子:

Interleave方式

AnyiAny的区别只有顺序。Anyi使用交替的顺序。

以是响应的,我们需要一个方式,这个方式把两个Stream s1s2中的元素交替地拼接组成一个“长”Stream。

首先,若是s1是空Stream,那么“长”Stream显然就是s2

否则,分两部门组织:

  1. 第一个元素是s1的第一个元素;
  2. 这里和Append方式的区别是把s1s2的位置调换了,剩余Stream是s2交替拼上s1的剩余Stream,同样是个递归界说。

代码如下:

public Stream Interleave(DelayedStream f)
{
    if (IsEmpty()) return f();
    return MakeStream(Curr, () => f().Interleave(GetRest));
}

这里使用惰性的f是异常需要的,由于我们不希望取剩余Stream的时刻挪用GetRest

Bind方式

这个方式比较复杂,是对应到All运算中两两组合参数里的分支的历程。

平心在线:逻辑式编程语言极简实现(使用C#) - 4. 代码实现(完结) 第1张

不同于Append/Interleave作用在两个Stream上,Bind方式作用在一个Stream和一个Goal上。

为什么不是两个Stream呢?

前面已经剖析过了,k.All(g1, g2)这个运算,是把g2蕴含的条件,追加到g1所包罗的Stream中的每个替换里。

同时,g2是个函数。追加这个动作自己由g2表达。

举例来说,假设stg1所包罗的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》里的命名……

下面是一个AllBind的例子:

平心在线:逻辑式编程语言极简实现(使用C#) - 4. 代码实现(完结) 第2张

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()));
}

同理实现OriAnyi

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()));
}

同理实现AndiAlli

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的原理:

  1. NMiniKanren代码形貌的是一个Goal。Goal是一个替换到Stream的函数。
  2. 从NMiniKanren代码可以构建一张形貌了条件关系的图。每条路径对应一个替换,使用流盘算模式可以很巧妙地实现对所有路径的遍历。
  3. 使用代入消元法求解未知量。

另外NMiniKanren究竟只是一门教学级的语言,实用上一定一塌糊涂,说难听点也就是个玩具。我们学习的重点不在于NMiniKanren,而在于实现NMiniKanren的历程中所用到的手艺和头脑。掌握了这些方式后,可以凭据自己的需要举行优化或扩展,或者将这些方式应用到其他问题上。

“神奇!”小皮瞪着眼睛摸摸脑壳,以前以为宛若天书般的逻辑式编程语言就这么学完了,还包罗了注释器的实现。

“认真学习了一天半的效果照样不错了。嘿嘿。”老明欣慰地拍了拍小皮的肩膀,微微笑道,“世上无难事,只怕有心人。正好今天周五了,周末就来公司把这两天落下的事情补完吧。”

小皮:“???”

PS:最后,用《The Reasoned Schemer》里的两页实现镇楼。俗话说得好,C#只是恰饭,真正的快乐还得看Scheme/Lisp。

平心在线:逻辑式编程语言极简实现(使用C#) - 4. 代码实现(完结) 第3张

平心在线:逻辑式编程语言极简实现(使用C#) - 4. 代码实现(完结) 第4张

,

欧博开户网址

欢迎进入欧博开户网址(Allbet Gaming):www.aLLbetgame.us,欧博网址开放会员注册、代理开户、电脑客户端下载、苹果安卓下载等业务。

欧博开户声明:该文看法仅代表作者自己,与本平台无关。转载请注明:平心在线:逻辑式编程语言极简实现(使用C#) - 4. 代码实现(完结)

网友评论

  • (*)

最新评论

  • UG环球会员充值 2020-09-22 00:15:02 回复

    UG环球欢迎进入环球UG官网(UG环球):www.ugbet.us,环球UG官方网站:www.ugbet.net开放环球UG网址访问、环球UG会员注册、环球UG代理申请、环球UG电脑客户端、环球UG手机版下载等业务。给你我所有的赞美

    1

文章归档

站点信息

  • 文章总数:441
  • 页面总数:0
  • 分类总数:8
  • 标签总数:929
  • 评论总数:127
  • 浏览总数:4557