пролог - генерировать целые числа "раскручивать"

Question

Я пытаюсь определить термины лямбда-исчисления с помощью индексов Де Брюина.Я использую swi пролог на OS X.

Если я использую zero|successor представление натурального числа, я могу интерактивно завершить частично указанный термин.

nat(zero).
nat(s(X)) :- nat(X).

debruijn2(N)         :- nat(N).
debruijn2(ap(M, N))  :- debruijn2(M), debruijn2(N).
debruijn2(lambda(M)) :- debruijn2(M).

, например,Z и X объединяются с zero в ap(Z, X).

?- debruijn2(ap(X, Z)).
X = Z, Z = zero .

Но использование length для проверки чисел , таких как , приводит к ошибке типа, если только аргумент не указанdebruijn - это просто целое число.

debruijn(N)          :- length(_, N).
debruijn(ap(M, N))   :- debruijn(M), debruijn(N).
debruijn(lambda(M))  :- debruijn(M).

Запрос debruijn(X). успешно выполняется и X объединяется с 0.

?- debruijn(X).
X = 0 .

Однако запрос debruijn(ap(Z, X)).терпит неудачу, как будто length(_, ·) безвозвратно ограничивает свой второй аргумент целым числом.

?- debruijn(ap(Z, X)).
ERROR: Type error: `integer' expected, found `ap(_2944,_2946)' (a compound)
ERROR: In:
ERROR:   [10] throw(error(type_error(integer,...),context(...,_3008)))
ERROR:    [8] debruijn(ap(_3036,_3038)) at <...>:2
ERROR:    [7] <user>
ERROR:
ERROR: Note: some frames are missing due to last-call optimization.
ERROR: Re-run your program in debug mode (:- debug.) to get more detail.
   Exception: (8) debruijn(ap(_2362, _2364)) ? creep

Почему length/2 вызывает ошибку типа, а не просто не применяется к аргументу?

Answer 1

Альтернативный вариант выполнения на SWI-Prolog без дорогостоящих вызовов length/2 и catch/3:

debruijn(N)         :- simple(N), nat(N).
debruijn(ap(M, N))  :- debruijn(M), debruijn(N).
debruijn(lambda(M)) :- debruijn(M).

nat(0).
nat(I) :-
    nat(1, I).

nat(I, I).
nat(I, J) :-
    I2 is I + 1,
    nat(I2, J).

Предикат simple/1 успешно выполняется, если его аргумент не создан для составного термина.Это устаревший предикат, который никогда не был стандартизирован, но все еще встречается в некоторых системах Prolog (например, это предикат библиотеки в SWI-Prolog и встроенный предикат в SICStus Prolog).

Разница с length/2Решением, которое может или не может иметь отношение к вашему варианту использования, является поведение, когда debruijn/1 вызывается с отрицательным числомВ этом случае это решение будет зациклено и в конечном итоге приведет к ошибке, но length/2 сгенерирует исключение, которое оболочка catch/3 преобразует в сбой.

Answer 2

Я подозреваю, что это потому, что Пролог пытается оценить предикат length/2 во время поиска.Согласно manual , возникает ошибка, если второй аргумент связан с нецелым числом.Это отличается от простого сбоя проверки.

Вы можете использовать catch/3, чтобы превратить сбой в ложный предикат:

debruijn(N)          :- catch(length(_, N), _, false).
debruijn(ap(M, N))   :- debruijn(M), debruijn(N).
debruijn(lambda(M))  :- debruijn(M).

В ручном режиме указано, что восстановление выполняется из исключениядовольно медленно, хотя.Я ни в коем случае не эксперт по Прологу, так что, возможно, есть лучшее решение.