javascript - JavaScript 中的一等变量

标签 javascript variables unification first-class

我正在实现 unification JavaScript 中的算法,用于计算两个给定术语的最通用统一词。简而言之,统一就是取两个项t1的过程。和t2并将它们组合成一个新术语 t这是两者的特化 t1t2 。考虑(注意变量是大写的):

t1 := foo(jane, A, B)
t2 := foo(X, Y, rocks)

特化运算符表示 a ⊏ b 中“a 是 b 的特化” 。例如:

foo(jane, doe, X)   ⊏ t1
foo(on, the, rocks) ⊏ t2

两个术语的统一词是专门化这两个术语的术语。例如:

foo(jane, street, rocks) ⊏ t1
foo(jane, street, rocks) ⊏ t2

两个术语的最通用统一词是这两个术语的统一词,它概括了这两个术语的所有其他统一词(即所有其他统一词专门化了最通用的统一词)。例如:

foo(jane, street, rocks) ⊏ foo(jane, M, rocks)

因此foo(jane, M, rocks)t1 最通用的统一词和t2 。以下算法可用于计算一阶谓词逻辑项的最通用统一词。

  1. 如果两者t1t2是常量,那么当且仅当它们是相同的常量时它们才统一(例如 janestreetrocks 是常量)。
  2. 如果t1是一个变量并且 t2是一个非变量(即常数或复数项)则 t1实例化为t2当且仅当t1不会出现在 t2 中.
  3. 如果t2是一个变量并且 t1是一个非变量(即常数或复数项)则 t2实例化为t1当且仅当t2不会出现在 t1 中.
  4. 如果t1t2都是变量,那么它们都会互相实例化,并且共享值。
  5. 如果两者t1t2是复杂术语,那么它们统一当且仅当它们是同一类复杂术语并且它们相应的参数统一。
  6. 当且仅当两个术语遵循上述五个规则时,它们才是统一的。

无论如何,这就是我想要解决这个问题的方式:

function variable(name) {
    return {
        type: "variable",
        name: name,
        term: null
    };
}

function constant(name) {
    return {
        type: "non_variable",
        name: name,
        args: []
    };
}

function complex(name, args) {
    return {
        type: "non_variable",
        name: name,
        args: args
    };
}

现在,我们可以定义t1t2如下:

var t1 = complex("foo", [constant("jane"), variable("A"), variable("B")]);
var t2 = complex("foo", [variable("X"), variable("Y"), constant("rocks")]);

然后我们实现统一算法:

function unify(a, b) {
    var x = resolve(a);
    var y = resolve(b);

    var operation = 0;

    if (x.type === "non_variable") operation += 2;
    if (y.type === "non_variable") operation += 1;

    switch (operation) {
    case 0:
        return x.term = y.term = variable(x.name);
    case 1:
        if (occurs(x, y)) throw new Error(x.name + " occurs in " + show(y));
        return x.term = y;
    case 2:
        if (occurs(y, x)) throw new Error(y.name + " occurs in " + show(x));
        return y.term = x;
    case 3:
        if (x.name !== y.name) throw new
            Error(x.name + " and " + y.name + " are different terms");

        var ax = x.args;
        var ay = y.args;

        if (ax.length !== ay.length) throw new
            Error(x.name + " and " + y.name + " have different arities");

        var args = ax.map(function (t, i) {
            return unify(t, ay[i]);
        });

        return complex(x.name, args);
    }
}

function resolve(t) {
    if (t.type === "non_variable") return t;

    var v = t;
    while (v.type === "variable" && v.term) v = v.term;
    return t.term = v;
}

function show(t) {
    return t.name + "(" + t.args.map(function (t) {
        return t.type === "non_variable" &&
           t.args.length > 0 ? show(t) : t.name;
    }).join(", ") + ")";
}

function occurs(v, t) {
    return t.args.some(function (t) {
        t = resolve(t);
        return t.type === "variable" ? t === v : occurs(v, t);
    });
}

它有效:

var t = unify(t1, t2);

alert(show(t));
<script>
function variable(name) {
    return {
        type: "variable",
        name: name,
        term: null
    };
}

function constant(name) {
    return {
        type: "non_variable",
        name: name,
        args: []
    };
}

function complex(name, args) {
    return {
        type: "non_variable",
        name: name,
        args: args
    };
}

var t1 = complex("foo", [constant("jane"), variable("A"), variable("B")]);
var t2 = complex("foo", [variable("X"), variable("Y"), constant("rocks")]);

function unify(a, b) {
    var x = resolve(a);
    var y = resolve(b);

    var operation = 0;

    if (x.type === "non_variable") operation += 2;
    if (y.type === "non_variable") operation += 1;

    switch (operation) {
    case 0:
        return x.term = y.term = variable(x.name);
    case 1:
        if (occurs(x, y)) throw new Error(x.name + " occurs in " + show(y));
        return x.term = y;
    case 2:
        if (occurs(y, x)) throw new Error(y.name + " occurs in " + show(x));
        return y.term = x;
    case 3:
        if (x.name !== y.name) throw new
            Error(x.name + " and " + y.name + " are different terms");

        var ax = x.args;
        var ay = y.args;

        if (ax.length !== ay.length) throw new
            Error(x.name + " and " + y.name + " have different arities");

        var args = ax.map(function (t, i) {
            return unify(t, ay[i]);
        });

        return complex(x.name, args);
    }
}

function resolve(t) {
    if (t.type === "non_variable") return t;

    var v = t;
    while (v.type === "variable" && v.term) v = v.term;
    return t.term = v;
}

function show(t) {
    return t.name + "(" + t.args.map(function (t) {
        return t.type === "non_variable" &&
           t.args.length > 0 ? show(t) : t.name;
    }).join(", ") + ")";
}

function occurs(v, t) {
    return t.args.some(function (t) {
        t = resolve(t);
        return t.type === "variable" ? t === v : occurs(v, t);
    });
}
</script>

但是,我只有一个问题:我实现一等变量的方式不是很好。我的实现方式如下:

  1. 每个变量都有一个 term属性是 null最初(以表明该变量尚未实例化)。
  2. 当变量与非变量统一时,其 term属性设置为非变量,这很好。
  3. 但是,当一个变量与另一个变量统一时就会出现问题。我们无法设置term将一个变量的属性传递给另一个变量,因为这会导致循环引用。因此,我创建一个新变量并设置 term将两个变量的属性传递给新变量。
  4. 这会导致另一个问题。如果我们统一许多变量,那么 term链条会变得更长,这就是为什么我需要 resolve我上面的代码中的函数。它遍历term链并返回链中的最后一项。

所以我的问题是是否有更好的方法在 JavaScript 中创建一等变量(即两个变量之间共享值不需要使用 term 链)。如果有更好的方法请描述一下算法。

最佳答案

听起来您可以使用一个不相交的集合森林,这些术语将成为其中的成员。这具有高效的联合/查找。

http://en.wikipedia.org/wiki/Disjoint-set_data_structure#Disjoint-set_forests

一些谷歌搜索再次确认这被用于 prolog 统一实现中。

http://docs.lib.purdue.edu/cgi/viewcontent.cgi?article=2318&context=cstech

关于javascript - JavaScript 中的一等变量,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/29541576/

相关文章:

c# - 为什么要使用成员变量?

haskell - 如何在 CPS 中构建更高等级的 Coyoneda 类型的值?

javascript - 使用 jquery 迭代值的问题

javascript - 使用立即需要该状态进行 API 调用的 useState Hook 时,如何等待 setState 调用完成?

javascript - 使用 Javascript 将文本和变量写入 HTML

javascript - 如何在javascript中选择名称以某个特定字符串开头的元素?

list - 在Prolog中不统一删除列表的所有成员

python - 在 Python 中实现 Prolog 统一算法?回溯

javascript - ajax 和 javascript 的区别

javascript - 从标签 python 的 onclick 属性获取 URL