Определение иерархии типов, включая типы функций в Прологе

Question

Я снова посещаю Пролог после изучения его в колледже и хотел бы описать иерархию типов, которая включает в себя типы функций.Пока что это то, что я получил ( 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

Что я делаю не так?

Answer 1

Мне удалось избежать проблемы неограниченной левой рекурсии, включив логику для супертипов и используя ту или иную зависимость в зависимости от того, какие из переменных связаны.

Сначала я определил предложение для простоготипы, перечисляющие все, что используется позже явно:

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

Answer 2

Проблема возникает, как вы заметили, только когда вы добавили второй набор 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 проблематичны, так как не накладывают никаких ограничений на длину списка ...