JavaScript 中的第一个 class 个变量

Question

我正在 JavaScript 中实现 unification 算法来计算两个给定项的最一般统一符。简而言之，合一是将两个术语 t1 和 t2 组合成一个新术语 t 的过程，它是 t1 和 t2 的特化.考虑（注意变量是大写的）：

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 的最通用的统一符。以下算法可用于计算一阶谓词逻辑项的最一般统一器。

如果 t1 和 t2 都是常量，那么当且仅当它们是相同的常量（例如 jane、street 和 rocks 是常数）。
如果 t1 是变量而 t2 是非变量（即常量或复数项），则 t1 实例化为 t2 如果并且仅当 t1 未出现在 t2.
如果 t2 是变量而 t1 是非变量（即常量或复数项），则 t2 实例化为 t1 如果并且仅当 t2 未出现在 t1.
如果 t1 和 t2 都是变量，那么它们都被实例化为彼此，据说共享值。
如果 t1 和 t2 都是复数项，那么当且仅当它们是同一种类的复数项并且它们对应的参数统一时，它们才会合一。
两个术语统一当且仅当它们遵循以上五个规则统一时。

无论如何，这就是我想解决这个问题的方法：

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

现在，我们可以定义t1和t2如下：

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>

然而，我只有一个问题：我实现第一个class变量的方式不是很好。我的实现方式如下：

每个变量都有一个term 属性，最初是null（表明变量还没有被实例化）。
当变量与非变量统一时，其 term 属性设置为非变量，这很好。
但是，当一个变量与另一个变量统一时，就会出现问题。我们不能将一个变量的 term 属性设置为另一个变量，因为那样会导致循环引用。因此，我创建了一个新变量并将两个变量的 term 属性都设置为新变量。
这会导致另一个问题。如果我们统一很多变量，那么 term 链将变得更长，这就是为什么我需要在上面的代码中使用 resolve 函数。它遍历 term 链和 returns 链中的最后一项。

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

Answer 1

听起来您可以使用术语所属的不相交集森林。这有效率 union/find.

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 中的第一个 class 个变量

First-class variables in JavaScript

javascript

variables

unification

first-class