Правила обработки ограничений в SWI Prolog: существует ли "хранилище ограничений" только на время обработки целей верхнего уровня?
Я внимательно изучаю правила обработки ограничений (CHR), чтобы понять, могу ли я их понять (в том смысле, что здесь вычисляется и как классическая логика и даже линейная логика вписываются в это) и, возможно, применить их.
В книге Тома Фрювирта от 2009 года обсуждаются принципы CHR, но реализации, конечно, могут отличаться.
В данном случае я использую реализацию CHR в SWI Prolog.
Если я хорошо понимаю:
- Реализация CHR предоставит по крайней мере одно "хранилище ограничений" для выражения "состояния вычислений". Хранилище ограничений содержит только основные атомы (т.е. положительные литералы).
- В типичном сеансе CHR сначала настраивают хранилище ограничений с начальным состоянием. Один пишет программу CHR, содержащую правила CHR. Затем запускается программа CHR с хранилищем ограничений в качестве параметра. Повторное применение правил CHR с прямой цепочкой до тех пор, пока правила больше не будут применяться, итеративно (и деструктивно) преобразует хранилище ограничений из исходного состояния в некоторое конечное состояние. Затем можно изучить хранилище ограничений, чтобы найти желаемый ответ.
- В этом сценарии учитывается только недетерминизм ("недетерминизм фиксированного выбора"): когда несколько правил применяются в любом промежуточном состоянии, принимается любое.
- Недетерминизм "не знаю" с возвратом к точке выбора в случае последующего сбоя не рассматривается - реализация остается на усмотрение реализации, чтобы обеспечить это тем или иным способом, если это необходимо.
В качестве упражнения простейшая программа для вычисления 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) откатываются. Сам Пролог тогда терпит неудачу.