Выразителен ли «почти чистый» Пролог?

Если брать чистый Scheme. Возможно, достаточно чистого Пролога. Чистая схема будет представлять собой лямбда-выражения с определенной строгой стратегией оценки вызова по значению. Таким образом, мы могли бы реализовать чистую схему следующим образом на Прологе, опираясь на индексы де Брейна:

eval(P*Q, H) :- !,
   eval(P, R),
   eval(Q, S),
   reduce(R, S, H).
eval(X, X).

reduce(b(R), S, J) :- !,
   subst(R, 0, S, H),
   eval(H, J).
reduce(R, S, R*S).

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

Вот пример запроса, SUCC и ZERO взяты из здесь:

?- ZERO = b(b(0)), SUCC = b(b(b(1*(2*1*0)))), 
   eval(SUCC*(SUCC*ZERO)*f*a, X).
ZERO = b(b(0)),
SUCC = b(b(b(1*(2*1*0)))),
X = f*(f*a)

Просто символы и списки (деревья).

Вам также нужны логические значения схемы #t и #f, если вы не хотите кодировать все в чистом лямбда-исчислении. Вы также исключаете значения функций, что, к счастью, упрощает этот ответ. Хотя вам придется разрешить частный случай форм верхнего уровня (define name (lambda ...)). (Все остальное, включая расширенные let выражения, может быть дефункционализировано.)

Итак, мое утверждение таково: нет, между этим расплывчатым подмножеством Схемы и чистым Прологом, как вы его определили, нет разрыва в выразительности. Мой аргумент (это не доказательство) конструктивен, он переводит код схемы для пересечения списка из этого ответа в Пролог.

В частности, это:

(define intersect
  (lambda (set1 set2)
    (cond
      ((null? set1)(quote ()))
      ((member? (car set1) set2)
       (cons (car set1)
             (intersect (cdr set1) set2)))
      (else (intersect (cdr set1) set2)))))

становится:

intersect(Set1, Set2, Result) :-
    cond([
        ['null?'(Set1), result([])],
        [cond_1(Set1, Set2), body_1(Set1, Set2)],
        [else, body_2(Set1, Set2)]], Result).

cond_1(Set1, Set2, Result) :-
    car(Set1, Car),
    'member?'(Car, Set2, Result).

body_1(Set1, Set2, Result) :-
    car(Set1, Car),
    cdr(Set1, Cdr),
    intersect(Cdr, Set2, PartialIntersection),
    cons(Car, PartialIntersection, Result).

body_2(Set1, Set2, Result) :-
    cdr(Set1, Cdr),
    intersect(Cdr, Set2, Result).

и это:

(define member?
  (lambda (a lat)
    (cond
      ((null? lat) #f)
      (else (or (equal? (car lat) a) 
                (member? a (cdr lat)))))))

становится:

'member?'(A, Lat, Result) :-
    cond([
        ['null?'(Lat), result('#f')],
        [else, or([or_case_1(Lat, A),
                   or_case_2(Lat, A)])]], Result).

or_case_1(Lat, A, Result) :-
    car(Lat, Car),
    'equal?'(Car, A, Result).

or_case_2(Lat, A, Result) :-
    cdr(Lat, Cdr),
    'member?'(A, Cdr, Result).

Обратите внимание, что вложенные выражения должны быть невложенными, и во всех случаях, кроме самых тривиальных, это проще всего сделать, определив вспомогательные предикаты Пролога. Это не увеличивает размер кода нелинейно.

В этих определениях используются следующие переводы стандартных конструкций Scheme:

'equal?'(X, Y, '#t') :-
    =(X, Y, true).
'equal?'(X, Y, '#f') :-
    =(X, Y, false).

'null?'(Value, Result) :-
    'equal?'(Value, [], Result).

car([Car | _Cdr], Car).

cdr([_Car | Cdr], Cdr).

cons(Car, Cdr, [Car | Cdr]).

or([], '#f').
or([Goal | Goals], Result) :-
    if (Goal,
       Result = '#t',
       or(Goals, Result)).

cond([], _Result) :-
    throw(error(cond_without_else, _)).
cond([[Condition, Body] | OtherCases], Result) :-
    if (Condition,
       call(Body, Result),
       cond(OtherCases, Result)).

Некоторые вспомогательные материалы для получения простого значения из тела случая cond и для случая else:

result(Result, Result).

else('#t').

И это вся внутренне нечистая, внешне чистая поддержка Пролога, которая вам нужна:

if (Goal, True, False) :-
    call(Goal, Truth),
    (   Truth == '#t' -> call(True)
    ;   Truth == '#f' -> call(False)
    ;   throw(error(type_or_instantiation_error(Truth), _)) ).

Я назвал это if/3 вместо if_/3, потому что это не совсем «стандарт» if_/3: он ожидает, что условие будет оцениваться как истинное значение схемы, а не true или false. Не стесняйтесь массировать его до «стандартной» формы. Обновлено: есть несколько «достаточно хороших» способов определить (=)/3, которые будут работать в контексте этого ответа, но чтобы избежать дальнейшего отказа от велосипедов, просто используйте определение из https://stackoverflow.com/a/27358600/4391743.

Тесты:

?- 'member?'(a, [x, y, a, c], Result).
Result = '#t' ;
false.

?- intersect([a, b, c, d], [c, d, e, f], Result).
Result = [c, d] ;
false.

Просто symbol/1 и dif/2 являются достаточными расширениями логически чистого Пролога.

Доказательство:

Этот ответ содержит оценщик выражений схемы, evil/2. Он понимает lambda и quote и может быть легко расширен для обработки встроенных процедур списка, таких как list, car, cdr и т. д. Помимо чистого (Горн) Пролога, он использует только symbol/1 и dif/2. Хотя это интерпретатор и будет работать медленно, его существование показывает, что те же самые операции со списками, которые выполняет Scheme, могут быть выполнены в таком почти чистом Прологе. (Я думаю, что symbol/1 тоже не понадобился бы, если бы символы Схемы были переведены в symb(prolog_atom), а не напрямую в prolog_symbol)

Редактировать

Это расширяет evil/2 для обработки if, #t и #f (представленных true и false):

evil(true, _, true).
evil(false, _, false).

evil([if, E1, E2, E3], Env, Val) :-
    evil(E1, Env, false),
    symbols(E2),
    evil(E3, Env, Val).

evil([if, E1, E2, E3], Env, Val) :-
    evil(E1, Env, V),
    dif (V, false),
    symbols(E3),
    evil(E2, Env, Val).

Это расширяет evil/2 до обработки equalp. Он даже мощнее, чем Scheme eq*, поскольку он также будет приравнивать некоторые замыкания:

evil([equalp, E1, E2], Env, true) :-
    evil(E1, Env, V),
    evil(E2, Env, V).

evil([equalp, E1, E2], Env, false) :-
    evil(E1, Env, V1),
    evil(E2, Env, V2),
    dif (V1, V2).