Компьютерные рассуждения о любопытном выводе Пролога Булоса

Question

Любопытный вывод Бооло был изначально сформулирован здесь с уравнениями. Это рекурсивное определение функции f и предиката d с помощью синтаксиса N+, натуральных чисел без нуля, сгенерированных из 1 и s(.).

Но это также может быть сформулировано с помощью клаузул рога. Логическое содержание не совсем то же самое, предикат f фиксирует только положительный аспект функции, но тип проблемы остается тем же. Возьмите следующую программу Prolog:

f(_, 1, s(1)).
f(1, s(X), s(s(Y))) :- f(1, X, Y).
f(s(X), s(Y), T) :- f(s(X), Y, Z), f(X, Z, T).

d(1).
d(s(X)) :- d(X).

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

?- f(X,X,Y).
X = 1,
Y = s(1) 
X = s(1),
Y = s(s(s(1))) 
X = s(s(1)),
Y = s(s(s(s(s(s(s(s(s(s(...)))))))))) 
ERROR: Out of global stack

?- f(s(s(s(s(1)))), s(s(s(s(1)))), X), d(X).

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

Answer 1

Одно из решений: абстрактная интерпретация

прелиминарии

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

Вместо этого он интерпретирует программу более абстрактно. Поэтому такие интерпретаторы называются абстрактными интерпретаторами.

Представление программы

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

Чтобы упростить рассуждения о программе, я теперь сделаю все объединения явными. Легко видеть, что это не меняет смысла программы и может быть легко автоматизировано. Я получаю:

f (_, X, Y): -
        Х = 1,
        Y = s (1).
f (Arg, X, Y): -
        Arg = 1,
        X = s(X0),
        Y = s(s (Y0)),
        f (Arg, X0, Y0).
f (X, Y, T):-
        X = s(X0),
        Y = s(Y0),
        f (X, Y0, Z),
        f (X0, Z, T).

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

Абстракция

Я использую следующую абстракцию: вместо того, чтобы рассуждать над конкретными терминами 1, s(1), s(s(1)) и т.д., я использую атом d для каждого члена T, для которого я могу доказать, что d( T ) держит.

Позвольте мне показать вам, что я имею в виду под следующей интерпретацией объединения:

интерпретировать (d = N):- d(N). 

Это говорит:

Если d(N) держит, то N должен считаться идентичным атому d который, как мы уже говорили, будет обозначать любой термин, для которого d/1 держит.

Обратите внимание, что это значительно отличается от того, что фактическое объединение между конкретными терминами d а также N средства! Например, мы получаем:

? - интерпретировать (X = s(s(1))).
Х = д.

Довольно странно, но я надеюсь, что вы можете привыкнуть к этому.

Расширение абстракции

Конечно, интерпретация одного объединения недостаточно для рассуждения об этой программе, поскольку она также содержит дополнительные языковые элементы.

Поэтому я расширяю абстрактную интерпретацию:

• конъюнкция
• вызовы f/3,

Интерпретировать союзы легко, но как насчет f/3?

Инкрементальные деривации

Если во время абстрактной интерпретации мы сталкиваемся с целью f(X, Y, Z) тогда мы знаем следующее: в принципе, аргументы, конечно, могут быть объединены с любыми условиями, для которых цель достигнута. Таким образом, мы отслеживаем те аргументы, для которых мы знаем, что запрос может быть успешным в принципе.

Таким образом, мы снабжаем предикат дополнительным аргументом: списком f/3 цели, которые являются логическими последствиями программы.

Кроме того, мы реализуем следующее очень важное положение: если мы сталкиваемся с объединением, которое не может быть безопасно истолковано в абстрактных терминах, то мы выдаем ошибку, а не молча терпим неудачу. Это может, например, произойти, если объединение не удастся, если рассматривать его как абстрактную интерпретацию, хотя оно будет успешным как конкретное объединение, или если мы не сможем полностью определить, относятся ли аргументы к предполагаемой области. Основная цель этого положения состоит в том, чтобы избежать непреднамеренного устранения фактических решений из-за упущений в абстрактном интерпретаторе. Это наиболее важный аспект в интерпретаторе, и любой теоретико-доказательный механизм будет сталкиваться с тесно связанными вопросами (как мы можем гарантировать, что никакие доказательства не будут пропущены?).

Вот:

интерпретировать (Var = N, _):-
        must_be(var, Var),
        must_be(земля, N),
        d(N)
        Var = d.
истолковать ((A,B), Ds):-
        интерпретировать (A, Ds),
        интерпретировать (B, Ds).
истолковать (F (A, B, C), Ds):-
        член (f (A, B, C), Ds).

Quis Custodiet Ipsos Custodes?

Как мы можем сказать, действительно ли это правильно? Это сложная часть! На самом деле, оказывается, что вышеприведенного недостаточно, чтобы быть уверенным, чтобы охватить все случаи, потому что он может просто потерпеть неудачу, если d(N) не держит. Очевидно, недопустимо, чтобы абстрактный интерпретатор молчал, если он не может обработать ошибки. Итак, нам нужен хотя бы еще один пункт:

интерпретировать (Var = N, _):-
        must_be(var, Var),
        must_be(земля, N),
        \+ d(N),
        ошибка_домена (d, N).

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

За этой областью интерпретация объединения становится:

интерпретировать (Var = N, _): -
        must_be (земля, N),
        (вар (вар) ->
            (   d(N) -> Var = d;   N = s(d) -> Var = d;   N = s(s(d)) -> Var = d;   domain_error(d, N));   Var == любая -> правда;   domain_error(any, Var)).

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

Как выяснится, этого определения достаточно, чтобы ответить на заданный вопрос. Тем не менее, это явно оставляет желать лучшего: это сложнее, чем хотелось бы, и становится все сложнее сказать, охватили ли мы все случаи. Заметьте, однако, что любой теоретико-доказательный подход сталкивается с тесно соответствующими проблемами: чем сложнее и мощнее он становится, тем сложнее сказать, все ли он верен.

Все деривации: Увидимся в точке фиксации!

Теперь осталось вывести все, что следует из исходной программы.

Вот оно, простое вычисление с фиксированной точкой:

производные (Ds):-
        функтор (руководитель, ф, 3),
        findall(Head-Body, пункт (Head, Body), пункты),
        Deriveable_fixpoint(пункты, [], Ds).

Deriveable_fixpoint(пункты, Ds0, Ds):-
        findall(D, clauses_derivable(Clauses, Ds0, D), Ds1, Ds0),
        term_variables(Ds1, Vs),
        maplist(=(любой), Vs),
        сортировка (Ds1, Ds2),
        (   same_length(Ds2, Ds0) -> Ds = Ds0; Deriveable_fixpoint(пункты, Ds2, Ds)).

clauses_derivable(Clauses, Ds0, Head):-
        член (руководитель, пункты),
        интерпретировать (Body, Ds0).

Так как мы выводим основные термины, sort/2 удаляет дубликаты.

Пример запроса:

? - производные (Ds).
ОШИБКА: Аргументы недостаточно проработаны

В некоторой степени антиклиматически, абстрактный интерпретатор не может обработать эту программу!

Коммутативность на помощь

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

В этом случае я сделаю последнее и оставлю первое в качестве упражнения. Вместо того, чтобы искать доказательства, мы ищем эквивалентные способы написания программы, чтобы наш интерпретатор мог получить нужные свойства. Например, сейчас я использую коммутативность соединения для получения:

f (_, X, Y): -
        Х = 1,
        Y = s(1).
f(Arg, X, Y):-
        Arg = 1,
        f(Arg, X0, Y0),
        X = s(X0),
        Y = s(s(Y0)).
f(X, Y, T):-
        f(X, Y0, Z),
        f(X0, Z, T),
        X = s(X0),
        Y = s(Y0).

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

iamque opus exegi, потому что:

? - производные (Ds).
Ds = [f (любой, d, d)].

Это показывает, что в каждом решении f/3 последние два аргумента всегда являются терминами, для которых d/1 держит! В частности, это касается и приведенных вами примеров аргументов, даже если нет надежды когда-либо реально вычислить конкретные термины!

Заключение

Абстрактной интерпретацией мы показали:

• для всех X где f(_, _, X) имеет место, d(X) также держит
• за этим, для всех Y где f(_, Y, _) имеет место, d(Y) тоже держит.

Вопрос задан только для особого случая первого свойства. Мы показали значительно больше!

В итоге:

Если f(_, Y, X) держит, то d(X) держит и d(Y) держит.

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

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

+1 за отличный вопрос и справку.