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

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

A 1 ,A 2 ,... ← A i ,A i+1 ,.... 这里, 正文字构成正体. 特别地, 一个具有空正体的子句称为纯
{A 1 ,A 2 ,...,¬A i ,¬A i+1 ,...} 或
负子句. 一个霍恩子句 (Horn 子句) 是一个最多包含一个正文字的子句. 一个确定子句形式为 head ← body (在 Prolog
head 是一个原子, 负文字的集合
中记作 Head : −Body), 其中包含恰好一个正文字. 对于给定的确定子句, 其正文字
body ≡ (a 1 ∧...∧a n ) 是一个目标 (原子的合取). 注意, 空目标表示为 true. 一个确定程序是一组有限的确定子句. 以
下, 我们聚焦于确定程序. 如果一个程序包含至少一个作为另一个谓词参数的谓词符号, 那么它被称为高阶程序.
其他未提及的术语可参见文献 [14,15].
MIL 基于 SLD-解析 (SLD-resolution) [16] 学习逻辑程序. 在 SLD-解析方法中, 通过找到一种 SLD-驳斥 [17] 来证
明一组 Horn 子句不可满足.
定义 1 (SLD-推导). 设 S 是由一组确定子句 D 和一组目标 {G 1 ,...,G q } 组成的 Horn 子句集. 一个 SLD-推导对
⟨ ⟩
于 S 是一系列的否定子句 N 0 ,N 1 ,...,N p , 满足以下所有性质:
(1) N 0 = G j , 其中 G j 是目标之一.
D 中存在一个确定子句
(2) 对于序列中的每一个 N i (0 ⩽ i < p), 如果 N i =← A 1 ,...,A k−1 ,A k ,A k+1 ,...,A n , 那么在
C i = A k ← B 1 ,...,B m , 使得当 m > 0 时, N i+1 =← A 1 ,...,A k−1 ,B 1 ,...,B m ,A k+1 ,...,A n ; 并且当 m = 0 时, N i+1 =← A 1 ,...,A k−1 ,
A k+1 ,...,A n .
定义 2 (SLD-驳斥). 当且仅当 N p = □ (空子句) 时, SLD 推导是一个 SLD-驳斥.
定义 3 (SLD-解式). 设 G 0 =← A 0 ,...,A m 为一个目标, C = B 0 ← B 1 ,...,B n 为一个 Horn 子句, 其中文字 A i 在替
θ
换 θ 下与 B 0 是可统一的. 目标 G 1 (称为 SLD-解式) G 1 =← A 0 ,...,A i−1 ,B 1 ,...,B n ,A i+1 ,...,A m 被认为是在替换 下, 通
过 C 从 G 0 推导出来的.
SLD-解析可以使用任何选择规则来选择目标中的文字. Prolog 总是选择目标中的最左边的文字 [18] . 相对于一
G 0 可能有多个 P 中的多个 Horn 子句进行解析. 我们将所有可能
个确定的程序 P, 目标 SLD-推导, 因为 G 0 可以与
的推导表示为一个 SLD-树.
定义 4 (SLD-树). 设 P 为一个确定性程序, G 0 为初始目标. P∪{G 0 } 的 SLD-树是一个 (可能是无限的) 树, 其中
每个节点是一个目标, 两个节点之间的边表示它们之间的 SLD-推导.
定义 5 (成功分支 [19] ). 设 P 是一个确定程序, G 0 是一个初始目标, T 是 P∪{G 0 } 的 SLD-树. 成功分支是根 ( G 0 )
与包含空子句的叶子之间的路径.
定义 6 (失败分支). 设 P 为一个确定程序, G 0 为一个初始目标, T 为 P∪{G 0 } 的一个 SLD-树. 失败分支是指从
根 ( G 0 ) 到一个包含非空目标的叶节点的一条路径.
1.2 元解释学习

通过利用经过改编的 Prolog 元解释器, MIL 方法通过证明一组目标来学习逻辑程序. 一个标准的 Prolog 元解
释器通过反复获取其头部与目标匹配的一阶子句来证明目标. 在此基础上, MIL 学习者通过额外获取其头部与目
标匹配的高阶元规则来证明目标. 一个 MIL 问题由 Input =< B,E, MS > 和 Output = H 组成. B 表示用户提供的背
+
+
景知识. E =< E ,E > 表示一对实例集, 其中 E 和 E 分别表示正例集和负例集. MS 表示元规则集. 这里, 元规则
−
−
被表示为如表 1 所示的高阶 Horn 子句.

表 1 元规则示例

名称 元规则 阶约束
Curry3 P(x,y) ← Q(x,y,R) P ≻ Q P ≻ R
,
Curry4 P(x,y) ← Q(x,y,R,S ) P ≻ Q P ≻ R P ≻ S
,
,
Precon P(x,y) ← Q(x),R(x,y) P ≻ Q P ≻ R
,
Postcon P(x,y) ← Q(x,y),R(y) P ≻ Q P ≻ R
,
Chain P(x,y) ← Q(x,z),R(z,y) P ≻ Q P ≻ R
,
Tailrec P(x,y) ← Q(x,z),P(z,y) P ≻ Q x ≻ z ≻ y
,