Page 58 - 《软件学报》2025年第8期

王榕 等: 基于记忆策略的元解释学习 3481

所有目标后, 通过将保存的元替换投影到其对应的元规则上来构建假设.

代码 1. 通用元解释器的 Prolog 代码.
prove([], G, G).

prove(Atom|Atoms,G1,G2) : −
prove_aux(Atom,G1,G3),

prove(Atoms,G3,G2).
prove_aux(Atom,G,G) : −
call(Atom).
prove_aux(Atom,G1,G4) : −
metarule(Name,MetaSub,(Atom : −Body)),

OrderTest,
save_subset(metasub(Name,MetaSub),G1,G3),
prove(Body,G3,G2).
对于“青蛙与荷叶问题”, MIL 首先尝试用 1 条子句和 0 个发明谓词来证明原子 f ([1,1,0,−1,−1],[−1,−1,0,1,1]).
当证明失败时, MIL 尝试通过增加子句 N 和发明谓词 M 的数量来证明该原子 (0 ⩽ M ⩽ N −1). 具体来说, 根据元
f ([1,1,0,−1,−1],[−1,−1,0,1,1]) 可以分解为两个体原子. 然后这两个体原子将以类似的方
规则的格式, 初始目标
式作为新目标进行证明. 一旦路径被证明为失败分支, MIL 学习者将回溯以证明下一个目标, 直到找到成功分支
为止.
图 3 显示了目标 f ([1,1,0,−1,−1],[−1,−1,0,1,1]) 在 N = 2 M = 1 情况下 SLD-树示意图. SLD-树展示了所
,
有可能的包含 2 条子句和 1 个发明的 2 元谓词 ( f1/2) 的程序. 图 3 中的蓝色子树表示当第 1 条子句已知为
f ([1,1,0,−1,−1],[−1,−1,0,1,1]) : −r1([1,1,0,−1,−1],[1,1,−1,0,−1]), f1([1,1,−1,0,−1],[−1,−1,0,1,1]) 时程序第 2
条子句的解空间, 如果 MIL 在完成包含两条子句的程序空间搜索后未能找到解, 则它将逐步增加子句的数量和发
明谓词的数量. 如图 4 所示的 SLD-树示意图, MIL 将重新从初始目标 f ([1,1,0,−1,−1],[−1,−1,0,1,1]) 开始搜索,
使用 3 条子句和 2 个发明的谓词. 从这个例子可以看到, 图 4 中的灰色子树与图 3 中的蓝色子树完全相同. 这意味
着, 目标 f1([1,1,−1,0,−1],[−1,−1,0,1,1]) 将会被重复证明.

… :−r1([1,1,−1,0,−1],[1,1,−1,−1,0]).
:−r1([1,1,0,−1,−1],[1,1,−1,0,−1]).
:−r1([1,1,0,−1,−1],[1,1,−1,0,−1]),
?−f([1,1,−1,0,−1],
[−1,−1,0,1,1]). −f1([1,1,−1,0,−1],[−1,−1,0,1,1]).
:−r1([1,1,−1,0,−1],[1,1,−1,−1,0]),
r1([1,1,−1,−1,0],Var).
:−r1([1,1,−1,−1,0],Var).
:−f1([1,1,−1,0,−1],[−1,−1,0,1,1]).
:−l2([1,1,−1,0,−1],[1,0,−1,1,−1]),
l2([1,0,−1,1,−1],Var). :−l2([1,1,−1,0,−1],[1,0,−1,1,−1]).
…
… :−l2([1,0,−1,1,−1],Var).

图 3 当 N = 2, M = 1 时, 目标 f ([1,1,0,−1,−1],[−1,−1,0,1,1]) 的 SLD-树的示意图

需要指出的是, 还有另一种包含未知变量的目标类型 (例如, 图 4 中的目标 f2([1,1,0,−1,−1],Var), 其中变量
Var 在 Prolog 中被称为匿名变量). 这些目标也将在 MIL 的后续学习过程中被重复证明. 例如, 图 5 中的灰色子树
与图 4 中的红色子树完全相同.
因此, 可以合理地认为冗余证明是 MIL 中存在的问题. 基于此动机, 我们提出了一种剪枝策略, 以避免重复证
明相同的目标.