在Prolog中定义包含函数类型的类型层次结构

Posted 2021-04-18

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

% 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

我究竟做错了什么？

答案

正如您所注意到的，当您添加第二组subtype/2定义时，问题才会发生。当你调用目标isa(X, byte)并要求第二个解决方案时，你使用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的第二和第三个条款仍然存在问题，因为它们对列表的长度没有限制......

另一答案

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

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

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是-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