在 Prolog 中定义包括函数类型的类型层次结构
Defining a type hierarchy including function types in Prolog
我在大学学习后正在重温 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).
然后我使用 nonvar.
将 subtype 规则限制在第一个术语已经绑定的情况下
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 是一个 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
我在大学学习后正在重温 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).
然后我使用 nonvar.
subtype 规则限制在第一个术语已经绑定的情况下
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 是一个 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