1

在大学学习后，我正在重新访问 Prolog，并想描述一个包含函数类型的类型层次结构。到目前为止，这就是我得到的（SWISH 链接）：

% subtype/2 is true if the first argument is a direct subtype of
% the second.
subtype(bit, byte).
subtype(byte, uint16).
subtype(uint16, uint32).
subtype(uint32, uint64).
subtype(uint64, int).

subtype(int8, int16).
subtype(int16, int32).
subtype(int32, int64).
subtype(int64, int).

% isa/2 checks if there's a sequence of types that takes
% from X to Y.
isa(X,Y) :- subtype(X,Y).
isa(X,Y) :-
    subtype(X,Z),
    isa(Z,Y).

该程序适用于以下查询：

?- subtype(bit, int).
true
?- findall(X,isa(X,int),IntTypes).
IntTypes = [uint64, int64, bit, byte, uint16, uint32, int8, int16, int32]

然后我为上面的函数子类型添加了以下定义isa，其中函数是一个复杂的术语func(ArgsTypeList, ResultType)：

% Functions are covariant on the return type, and
% contravariant on the arguments' type.
subtype(func(Args,R1), func(Args,R2)) :-
    subtype(R1, R2).
subtype(func([H1|T],R), func([H2|T],R)) :-
    subtype(H2, H1).
subtype(func([H|T1],R), func([H|T2],R)) :-
    subtype(func(T1,R), func(T2,R)).

现在，我仍然可以进行一些有限检查，但即使尝试枚举所有子类型的byte堆栈溢出失败。

?- isa(func([int,int], bit), func([bit,bit], int)).
true
?- isa(X, byte).
X = bit ;
Stack limit (0.2Gb) exceeded

我究竟做错了什么？

4

2 回答 2

2

正如您所注意到的，该问题仅在您添加第二组subtype/2定义时才会出现。当您调用目标isa(X, byte)并要求第二个解决方案时，您使用第二个子句 for isa/2，从而导致subtype/2两个参数都未绑定的调用。最终，您最终调用了第二组subtype/2定义。查询中未绑定的第一个参数与func(Args,R1)术语统一，其中两个参数都是变量。因此，递归调用最终将重复变量和func(Args,R1)项之间的统一，从而创建一个不断增加的项，随着递归调用的增加，最终耗尽堆栈。

为了更清楚，请注意，要求第二个解决方案会导致将第二个子句用于isa/2以下绑定：

isa(X,byte) :- subtype(X,Z), isa(Z, byte).

每次subtype(X,Z)目标的解决方案都会导致下一个目标的失败isa(Z, byte)。因此，您不断回溯到第二组子句的第一个subtype/2子句。

理解这个问题的通常解决方案是使用 Prolog 系统跟踪机制。出于某种原因，我无法将它与 SWI-Prolog 一起使用，鉴于您对 SWISH 的引用，您似乎正在使用它，但我对 GNU Prolog 的运气更好：

{trace}
| ?- isa(X, byte).
1    1  Call: isa(_279,byte) ? 
2    2  Call: subtype(_279,byte) ? 
2    2  Exit: subtype(bit,byte) ? 
1    1  Exit: isa(bit,byte) ? 

X = bit ? ;
...
17    7  Exit: subtype(func([byte|_723],int),func([bit|_723],int)) ? 
...
20    8  Exit: subtype(func([bit,byte|_839],int),func([bit,bit|_839],int)) ? 
...
21    9  Call: subtype(_806,bit) ? 
21    9  Fail: subtype(_806,bit) ? 
...

24    9  Exit: subtype(func([bit,bit,byte|_985],int),func([bit,bit,bit|_985],int)) ? 
...
25    9  Call: subtype(_806,bit) ? 
25    9  Fail: subtype(_806,bit) ?

为简洁起见，我省略了大部分跟踪行，但您可以看到func/2正在构建第一个参数中具有不断增长的列表的术语。

如何解决问题？也许区分简单类型和复合类型？例如：

simple_subtype(bit, byte).
simple_subtype(byte, uint16).
simple_subtype(uint16, uint32).
simple_subtype(uint32, uint64).
simple_subtype(uint64, int).

simple_subtype(int8, int16).
simple_subtype(int16, int32).
simple_subtype(int32, int64).
simple_subtype(int64, int).

% Functions are covariant on the return type, and
% contravariant on the arguments' type.
compound_subtype(func(Args,R1), func(Args,R2)) :-
    simple_subtype(R1, R2).
compound_subtype(func([H1|T],R), func([H2|T],R)) :-
    simple_subtype(H2, H1).
compound_subtype(func([H|T1],R), func([H|T2],R)) :-
    compound_subtype(func(T1,R), func(T2,R)).

% subtype/2 is true if the first argument is a direct subtype of
% the second.
subtype(X,Y) :- simple_subtype(X,Y).
subtype(X,Y) :- compound_subtype(X,Y).

% isa/2 checks if there's a sequence of types that takes
% from X to Y.
isa(X,Y) :-
    subtype(X,Y).
isa(X,Y) :-
    subtype(X,Z),
    isa(Z,Y).

尽管如此，第二个和第三个子句compound_subtype/2还是有问题的，因为它们对列表的长度没有限制......

于 2018-08-26T14:58:37.107 回答
0

通过包含超类型的逻辑并根据绑定的变量使用一个或另一个，我能够避免无界左递归的问题。

首先，我为简单类型定义了一个子句，列举了所有稍后显式使用的类型：

simple_type(bit).
simple_type(byte).
% ...
simple_type(int).

然后，我仅将规则限制在subtype第一个术语已经绑定的情况下，使用nonvar.

subtype(func(Args,R1), func(Args,R2)) :-
    nonvar(R1),
    subtype(R1, R2).
subtype(func([H1|T],R), func([H2|T],R)) :-
    nonvar(H1),
    supertype(H1, H2).
subtype(func([H|T1],R), func([H|T2],R)) :-
    nonvar(T1),
    subtype(func(T1,R), func(T2,R)).

然后我定义了一个supertype规则，这与subtype简单类型相反......

supertype(X, Y) :-
    simple_type(X),
    subtype(Y, X).

...但是对于函数类型是完全重复的。

supertype(func(Args,R1), func(Args,R2)) :-
    nonvar(R1),
    supertype(R1, R2).
supertype(func([H1|T],R), func([H2|T],R)) :-
    nonvar(H1),
    subtype(H1, H2).
supertype(func([H|T1],R), func([H|T2],R)) :-
    nonvar(T1),
    supertype(func(T1,R), func(T2,R)).

isa仍然是一样的，有两个补充：

  • 类型与自身相同（即，int is-a int）。
  • 如果第一项未绑定但第二项绑定，则使用逆规则typeof。

_

isa(X,Y) :- X = Y.
isa(X,Y) :- subtype(X,Y).
isa(X,Y) :-
    nonvar(X),
    subtype(X,Z),
    isa(Z,Y).
isa(X,Y) :-
    var(X), nonvar(Y), typeof(Y,X).

最后，typeof与 正好相反isa，使用supertype代替subtype：

typeof(X,Y) :- X = Y.
typeof(X,Y) :- supertype(X,Y).
typeof(X,Y) :-
    nonvar(X),
    supertype(X,Z),
    typeof(Z,Y).
typeof(X,Y) :-
    var(X), nonvar(Y), isa(Y,X).

我注意到这些规则有很多效率低下和重复的结果，但至少它是有效的:)

?- setof(X, isa(func([byte, byte], uint32), X), All), length(All, L).

All = [func([bit, bit], int), func([bit, bit], uint32), func([bit, bit], uint64), func([bit, byte], int), func([bit, byte], uint32), func([bit, byte], uint64), func([byte, bit], int), func([byte, bit], uint32), func([byte, bit], uint64), func([byte, byte], int), func([byte, byte], uint32), func([byte, byte], uint64)],
L = 12
于 2018-09-03T12:22:14.523 回答