Правила обработки ограничений в SWI Prolog: существует ли "хранилище ограничений" только на время обработки целей верхнего уровня?

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

В книге Тома Фрювирта от 2009 года обсуждаются принципы CHR, но реализации, конечно, могут отличаться.

В данном случае я использую реализацию CHR в SWI Prolog.

Если я хорошо понимаю:

  1. Реализация CHR предоставит по крайней мере одно "хранилище ограничений" для выражения "состояния вычислений". Хранилище ограничений содержит только основные атомы (т.е. положительные литералы).
  2. В типичном сеансе CHR сначала настраивают хранилище ограничений с начальным состоянием. Один пишет программу CHR, содержащую правила CHR. Затем запускается программа CHR с хранилищем ограничений в качестве параметра. Повторное применение правил CHR с прямой цепочкой до тех пор, пока правила больше не будут применяться, итеративно (и деструктивно) преобразует хранилище ограничений из исходного состояния в некоторое конечное состояние. Затем можно изучить хранилище ограничений, чтобы найти желаемый ответ.
  3. В этом сценарии учитывается только недетерминизм ("недетерминизм фиксированного выбора"): когда несколько правил применяются в любом промежуточном состоянии, принимается любое.
  4. Недетерминизм "не знаю" с возвратом к точке выбора в случае последующего сбоя не рассматривается - реализация остается на усмотрение реализации, чтобы обеспечить это тем или иным способом, если это необходимо.

В качестве упражнения простейшая программа для вычисления GCD с использованием алгоритма Евклида и сохранения журнала операций:

% Constraint `logg(Ti,Msg)` retains the log message `Msg` at step `Ti`
% (which increases monotonically)
% Constraint `gcdpool(X)` denotes a "GCD pool member". At each step, we want
% to compute the GCD of all the X for which there is a `gcdpool(X)` constraint
% in the constraint store. A CHR transformation of the store always reduces the
% sum of the X (variant) while keeping the GCD of the GCD pool members constant
% (invariant). We will thus find a solution eventually.

:- module(my_gcd, [  gcdpool/1, logg/2 ]).
:- use_module(library(chr)).

:- chr_constraint gcdpool/1, logg/2.

% pool contains duplicate: drop one! 

gcdpool(N) \ gcdpool(N),logg(Ti,Msg) <=> To is Ti+1, logg(To,[[drop,[N,N],[N]]|Msg]).

% pool contains 1 and anything not 1: keep only 1

gcdpool(1) \ gcdpool(N),logg(Ti,Msg) <=> 1<N | To is Ti+1, logg(To,[[drop,[1,N],[N]]|Msg]).

% otherwise

gcdpool(N) \ gcdpool(M),logg(Ti,Msg) <=> 0<N, N<M | To is Ti+1, 
                                                    V is M-N, 
                                                    gcdpool(V), 
                                                    logg(To,[[diff,[N,M],[N,V]]|Msg]).

Все очень просто. Тестовый запуск в SWI Prolog

?- use_module(library(chr)).
?- [gcd].
?- chr_trace.
% now we enter a goal:
?- gcdpool(6),gcdpool(3),logg(0,[]).
CHR:   (0) Insert: gcdpool(6) # <907>
CHR:   (1) Call: gcdpool(6) # <907> ? [creep]
CHR:   (1) Exit: gcdpool(6) # <907> ? [creep]
CHR:   (0) Insert: gcdpool(3) # <908>
CHR:   (1) Call: gcdpool(3) # <908> ? [creep]
CHR:   (1) Exit: gcdpool(3) # <908> ? [creep]
CHR:   (0) Insert: logg(0,[]) # <909>
CHR:   (1) Call: logg(0,[]) # <909> ? [creep]
CHR:   (1) Try: gcdpool(3) # <908> \ gcdpool(6) # <907>, logg(0,[]) # <909> <=> 0<3,3<6 | _71386 is 0+1,_71404 is 6-3,gcdpool(_71404),logg(_71386,[[diff,[3,6],[3,_71404]]]).
CHR:   (1) Apply: gcdpool(3) # <908> \ gcdpool(6) # <907>, logg(0,[]) # <909> <=> 0<3,3<6 | _71386 is 0+1,_71404 is 6-3,gcdpool(_71404),logg(_71386,[[diff,[3,6],[3,_71404]]]). ? [creep]
CHR:   (1) Remove: gcdpool(6) # <907>
CHR:   (1) Remove: logg(0,[]) # <909>
CHR:   (1) Insert: gcdpool(3) # <910>
CHR:   (2) Call: gcdpool(3) # <910> ? [creep]
CHR:   (2) Exit: gcdpool(3) # <910> ? [creep]
CHR:   (1) Insert: logg(1,[[diff,[3,6],[3,3]]]) # <911>
CHR:   (2) Call: logg(1,[[diff,[3,6],[3,3]]]) # <911> ? [creep]
CHR:   (2) Try: gcdpool(3) # <908> \ gcdpool(3) # <910>, logg(1,[[diff,[3,6],[3,3]]]) # <911> <=> _78066 is 1+1,logg(_78066,[[drop,[3,3],[3]],[diff,[3,6],[3,3]]]).
CHR:   (2) Apply: gcdpool(3) # <908> \ gcdpool(3) # <910>, logg(1,[[diff,[3,6],[3,3]]]) # <911> <=> _78066 is 1+1,logg(_78066,[[drop,[3,3],[3]],[diff,[3,6],[3,3]]]). ? [creep]
CHR:   (2) Remove: gcdpool(3) # <910>
CHR:   (2) Remove: logg(1,[[diff,[3,6],[3,3]]]) # <911>
CHR:   (2) Insert: logg(2,[[drop,[3,3],[3]],[diff,[3,6],[3,3]]]) # <912>
CHR:   (3) Call: logg(2,[[drop,[3,3],[3]],[diff,[3,6],[3,3]]]) # <912> ? [creep]
CHR:   (3) Exit: logg(2,[[drop,[3,3],[3]],[diff,[3,6],[3,3]]]) # <912> ? [creep]
CHR:   (2) Exit: logg(1,[[diff,[3,6],[3,3]]]) # <911> ? [creep]
CHR:   (1) Exit: logg(0,[]) # <909> ? [creep]

gcdpool(3),
logg(2, [[drop, [3, 3], [3]], [diff, [3, 6], [3, 3]]]) .

Ответ дают последние две строки: единственное ограничение, оставшееся в хранилище ограничений, - это gcdpool(3), так что 3 - это ответ.

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

Специального "хранилища ограничений" нет. Программа CHR (каким-то образом) компилируется в Prolog, и "ограничение CHR" становится "предикатом Prolog". "Хранилище ограничений" как таковое является стеком так называемой цели верхнего уровня Пролога (она не реифицируется).

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

gcdpool(6),gcdpool(3),logg(0,[]).

После чего сразу же начинает свою работу программа CHR.

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

Более того, не имеет смысла пытаться создать хранилище ограничений в самой "программе CHR". Таким образом положивlogg(0,[])в код GCD не влияет. Вы должны поставитьlogg(0,[]) в цель CHR.

Вопрос

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

2 ответа

Что касается вопроса "Как мне вернуть результаты вычисления CHR в Пролог?".

Вы можете сделать что-то вроде:

:- chr_constraint item/1, get_item/1.

item(In) \ get_item(Out) <=> In = Out.

Запрос:

?- item(foo),get_item(X).
X = foo.

Взгляните на этот учебник для получения дополнительной информации: http://www.pathwayslms.com/swipltuts/chr/index.html

Я слежу за замечательным учебником Анны Огборн по CHR. Некоторые примечания:

Где находится хранилище ограничений CHR?

В приведенном выше руководстве в разделе 5 Какое правило срабатывает? мы читаем:

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

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

И под 6.1 Threads

Хранилище CHR является локальным для одного потока.

Это особенно болезненно при реализации сервера, использующего CHR.

Одно из решений - выполнять всю работу CHR в специальном потоке.

CHR-Constraint-Server от Falco Nogatz - полезный инструмент.

Игра 3 Little Pigs - полезный стартер для сервера, который использует CHR для своей логики.

У Pengine будет свой поток. Это может быть полезно для CHR.

В документации по SWI Prolog говорится в разделе глобальных переменных

Глобальные переменные - это ассоциации между именами (атомами) и терминами. Они по-разному отличаются от хранения информации с использованием assert/1 или recorda/3.

Значение живет в стеке Пролога (глобальном). Это означает, что время поиска не зависит от размера термина. Это особенно интересно для больших структур данных, таких как проанализированные XML-документы или хранилище глобальных ограничений CHR.

Что делать с возвратом?

Правила CHR не возвращаются, поскольку эта концепция не имеет смысла в подходе CHR. Однако в разделе " Заставить CHR взаимодействовать с Prolog" мы читаем:

Если Prolog в теле любого правила терпит неудачу, все изменения в хранилище с момента первоначальной попытки добавить ограничение (путем его вызова из Prolog) откатываются. Сам Пролог тогда терпит неудачу.

Другие вопросы по тегам