我正在实现 unification JavaScript 中的算法,用于计算两个给定术语的最通用统一词。简而言之,统一就是取两个项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>
但是,我只有一个问题:我实现一等变量的方式不是很好。我的实现方式如下:
- 每个变量都有一个
term
属性是null
最初(以表明该变量尚未实例化)。 - 当变量与非变量统一时,其
term
属性设置为非变量,这很好。 - 但是,当一个变量与另一个变量统一时就会出现问题。我们无法设置
term
将一个变量的属性传递给另一个变量,因为这会导致循环引用。因此,我创建一个新变量并设置term
将两个变量的属性传递给新变量。 - 这会导致另一个问题。如果我们统一许多变量,那么
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/