Синтаксис и семантика логического программирования

Логическое программирование — это парадигма программирования , включающая языки, основанные на формальной логике, включая Datalog и Prolog . В этой статье описываются синтаксис и семантика чисто декларативного подмножества этих языков. Как ни странно, название «логическое программирование» также относится к конкретному языку программирования, который примерно соответствует декларативному подмножеству Пролога. К сожалению, в этой статье этот термин следует использовать в обоих смыслах.

Программы декларативной логики полностью состоят из правил вида

H :- B1, ..., BN.

Каждое такое правило можно прочитать как импликацию :

B_{1}\land \ldots \land B_{n}\rightarrow H

что означает «Если каждый $B_{i}$ верно, тогда $H$ верно». Логические программы вычисляют набор фактов, подразумеваемых их правилами.

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

Ученый-компьютерщик

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

Синтаксис

Программа Datalog состоит из списка правил ( предложений Хорна ). ^[1] Если константа и переменная представляют собой два счетных набора констант и переменных соответственно, а отношение представляет собой счетный набор символов-предикатов , то следующая грамматика BNF выражает структуру программы регистрации данных:

<program> ::= <rule> <program> | ""
<rule> ::= <atom> ":-" <atom-list> "."
<atom> ::= <relation> "(" <term-list> ")"
<atom-list> ::= <atom> | <atom> "," <atom-list> | ""
<term> ::= <constant> | <variable>
<term-list> ::= <term> | <term> "," <term-list> | ""

Атомы также называют литералами . Атом слева от :- символ называется главой правила; атомы справа — это тело . Каждая программа Datalog должна удовлетворять условию, согласно которому каждая переменная, появляющаяся в заголовке правила, также появляется и в теле (это условие иногда называют ограничением диапазона ). ^[1]^[2]

Правила с пустым телом называются фактами . Например, фактом является следующее правило:

r(x) :- .

Синтаксический сахар

Многие реализации логического программирования расширяют приведенную выше грамматику, позволяя записывать факты без :-, вот так:

r(x).

Многие также позволяют писать 0-арные отношения без скобок, например:

p :- q.

Это просто аббревиатуры ( синтаксический сахар ); они не влияют на семантику программы.

Пример

Следующая программа вычисляет соотношение path, что является транзитивным замыканием отношения edge.

edge(x, y).
edge(y, z).
path(A, B) :- 
  edge(A, B).
path(A, C) :- 
  path(A, B), 
  edge(B, C).

Семантика

Существует три широко используемых подхода к семантике программ Datalog: теоретико-модельный , с фиксированной точкой и теоретико-доказательный . Можно доказать, что эти три подхода эквивалентны. ^[3]

Атом называется основным , если ни один из его подчленов не является переменным. Интуитивно каждая семантика определяет смысл программы как набор всех основных атомов, которые можно вывести из правил программы, исходя из фактов.

Теоретическая модель

Диаграмма Хассе интерпретаций Эрбрана программы Datalog
e(x, y). e(y, z). p(A, B) :- e(A, B). p(A, C) :- p(A, B), e(B, C).
Интерпретация $M$ — минимальная модель Эрбрана. Все интерпретации выше него также являются моделями, все интерпретации ниже него не являются моделями.

Правило называется заземленным, если все его атомы (головка и тело) заземлены. Основное правило R ₁ является основным примером другого правила R _{2 ,} если R ₁ является результатом замены констант для всех переменных в R ₂ .

Базой Эрбрана программы Datalog является набор всех основных атомов, которые можно создать с помощью констант, представленных в программе. Интерпретация ) — (также известная как экземпляр базы данных это подмножество базы Эрбрана. Основной атом истинен в интерпретации $I,$ он является элементом $I.$ если Правило истинно в интерпретации $I$ , если для каждого основного экземпляра этого правила все положения тела истинны в $I$ , то глава правила также истинна $I.$ в

Модель это программы регистрации данных P интерпретация $I$ P , которая содержит все основные факты P и делает все правила P истинными в $I.$ — Теоретико-модельная семантика утверждает, что смыслом программы Datalog является ее минимальная модель (т. е. пересечение всех ее моделей). ^[4]

Например, эта программа:

edge(x, y).
edge(y, z).
path(A, B) :- 
  edge(A, B).
path(A, C) :- 
  path(A, B), 
  edge(B, C).

есть эта вселенная Эрбрана: x, y, z

и эта база Эрбрана: edge(x, x), edge(x, y), ..., edge(z, z), path(x, x), ..., path(z, z)

и эта минимальная модель Эрбрана: edge(x, y), edge(y, z), path(x, y), path(y, z), path(x, z)

Фиксированная точка

Пусть $I$ — набор интерпретаций программы Datalog P , то есть $I = P (H)$ , где H — база Эрбрана P , а P — оператор набора степеней . Оператором непосредственного следствия для P является следующая карта $T$ от $I$ до $I$ : Для каждого основного экземпляра каждого правила в P , если каждое предложение в теле находится во входной интерпретации, добавьте заголовок основного экземпляра к выходной интерпретации. . Это отображение $T$ монотонно заданного относительно частичного порядка, включением подмножества в $T$ . По теореме Кнастера – Тарского это отображение имеет наименьшую неподвижную точку; по теореме Клини о неподвижной точке неподвижная точка является верхней границей цепи $T(\emptyset ),T(T(\emptyset )),\ldots ,T^{n}(\emptyset ),\ldots$ . Наименее неподвижная точка $M$ совпадает с минимальной моделью программы Эрбрана. ^[5]

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

теоретико-доказательный

Для данной программы $P$ дерево доказательства основного атома $A$ представляет собой дерево с корнем, помеченным $A$ , листьями, помеченными основными атомами из голов фактов в $P$ , и ветвями с дочерними элементами. $A_{1},\ldots ,A_{n}$ помечены основными атомами $G,$ так что существует основной экземпляр

G :- A₁, ..., A_n.

правила в $P$ . Теоретико-доказательная семантика определяет смысл программы Datalog как набора основных атомов, которые можно выделить из таких деревьев. Это множество совпадает с минимальной моделью Эрбрана. ^[6]

Кто-то может заинтересоваться, появляется ли конкретный основной атом в минимальной модели Эрбрана программы Datalog или нет, возможно, не особо заботясь об остальной части модели. Чтение сверху вниз деревьев доказательств, описанных выше, подсказывает алгоритм вычисления результатов таких запросов , такое чтение информирует алгоритм разрешения SLD , который формирует основу для оценки Пролога .

Другие подходы

Семантика Datalog также изучалась в контексте фиксированных точек над более общими полукольцами . ^[7]

Логическое программирование

Хотя название «логическое программирование» используется для обозначения всей парадигмы языков программирования, включая Datalog и Prolog, при обсуждении формальной семантики оно обычно относится к расширению Datalog с помощью функциональных символов . Логические программы также называются предложений Хорна программами . Логическое программирование, обсуждаемое в этой статье, тесно связано с «чистым» или декларативным подмножеством Пролога .

Синтаксис

Синтаксис логического программирования расширяет синтаксис журнала данных функциональными символами. Логическое программирование снимает ограничение диапазона, позволяя переменным появляться в заголовках правил, которые не появляются в их телах. ^[8]

Семантика

Благодаря наличию функциональных символов модели логических программ Эрбрана могут быть бесконечными. Однако семантика логической программы по-прежнему определяется как ее минимальная модель Эрбрана. Соответственно, неподвижная точка оператора непосредственного следствия может не сходиться за конечное число шагов (или к конечному множеству). Однако любой основной атом в минимальной модели Эрбрана будет иметь конечное дерево доказательств. Вот почему Пролог оценивается сверху вниз. ^[8] Как и в Datalog, можно доказать, что три семантики эквивалентны.

Отрицание

Логическое программирование обладает тем желательным свойством, что все три основных определения семантики логических программ совпадают. Напротив, существует множество противоречивых предложений по семантике логических программ с отрицанием. Источник разногласий заключается в том, что логические программы имеют уникальную минимальную модель Эрбрана, а в программах логического программирования (или даже регистрации данных) с отрицанием ее нет.

Синтаксис

Отрицание написано notи может располагаться перед любым атомом в тексте правила.

<atom-list> ::= <atom> | "not" <atom> | <atom> "," <atom-list> | ""

Семантика

Расслоенное отрицание

Логическая программа с отрицанием является стратифицированной когда можно отнести каждое отношение к некоторому слою , так что если отношение $R$ оказывается отрицаемым в теле отношения $S$ , то $R$ находится в более низком слое, чем $S.$ , ^[9] Теоретико-модельная семантика Datalog и семантика фиксированной точки могут быть расширены для обработки послойного отрицания, и такие расширения могут быть признаны эквивалентными.

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

Хотя стратифицированное отрицание является распространенным расширением Datalog, существуют разумные программы, которые не могут быть стратифицированы. Следующая программа описывает игру для двух игроков, в которой игрок побеждает, если у его противника нет ходов: ^[10]

move(a, b).
win(X) :- move(X, Y), not win(Y).

Эта программа не стратифицирована, но кажется разумным предположить, что a должен выиграть игру.

Семантика завершения

Идеальная семантика модели

Стабильная семантика модели

Семантика стабильной модели определяет условие для вызова определенных моделей Эрбрана программы стабильной . Интуитивно, стабильные модели — это «возможные наборы убеждений, которых мог бы придерживаться рациональный агент, учитывая [программу]» в качестве предпосылок. ^[11]

Программа с отрицанием может иметь много стабильных моделей или не иметь стабильных моделей. Например, программа

p :- not q.
q :- not p.

имеет две стабильные модели $\{p\}$ , $\{q\}$ . Программа с одним правилом

p :- not p.

не имеет стабильных моделей.

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

Хорошо обоснованная семантика

Дальнейшие расширения

Было предложено и изучено несколько других расширений Datalog, включая варианты с поддержкой целочисленных констант и функций (включая DatalogZ ), ^[12]^[13] ограничения неравенства в телах правил и агрегатные функции .

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

См. также

Ссылки

Примечания

^ Jump up to: ^а ^б Кери, Готтлоб и Танка 1989 , с. 146.
^ Эйснер, Джейсон; Филардо, Натаниэль В. (2011). де Моор, Оге; Готтлоб, Георг; Фурче, Тим; Селлерс, Эндрю (ред.). Dyna: расширение журнала данных для современного искусственного интеллекта . Datalog Reloaded, Первый международный семинар, Datalog 2010, Оксфорд, Великобритания, 16–19 марта 2010 г. Конспекты лекций по информатике. Том. 6702. Берлин, Гейдельберг: Springer. стр. 181–220. дои : 10.1007/978-3-642-24206-9_11 . ISBN 978-3-642-24206-9 .
^ ван Эмден, Миннесота; Ковальский, Р.А. (1 октября 1976 г.). «Семантика логики предикатов как языка программирования» . Журнал АКМ . 23 (4): 733–742. дои : 10.1145/321978.321991 . ISSN 0004-5411 . S2CID 11048276 .
^ Кери, Готтлоб и Танка 1989 , стр. 149.
^ Кери, Готтлоб и Танка 1989 , стр. 150.
^ Абитбул, Серж (1996). Основы баз данных . Аддисон-Уэсли. ISBN 0-201-53771-0 . OCLC 247979782 .
^ Хамис, Махмуд Або; Нго, Хунг К.; Пихлер, Рейнхард; Сучу, Дэн; Ван, Ису Реми (01 февраля 2023 г.). «Сходимость регистрации данных по (предварительным) полукольцам». arXiv : 2105.14435 [ cs.DB ].
^ Jump up to: ^а ^б Абитебул 1996 , с. 299.
^ Халеви, Алон Ю.; Мумик, Индерпал Сингх; Сагив, Иегошуа; Шмуэли, Одед (1 сентября 2001 г.). «Статический анализ в расширениях журналов данных» . Журнал АКМ . 48 (5): 971–1012. дои : 10.1145/502102.502104 . ISSN 0004-5411 . S2CID 18868009 .
^ Леоне, Н; Рулло, П. (1 января 1992 г.). «Безопасное вычисление обоснованной семантики запросов журнала данных» . Информационные системы . 17 (1): 17–31. дои : 10.1016/0306-4379(92)90003-6 . ISSN 0306-4379 .
^ Гельфонд, Майкл; Лифшиц, Владимир (1988). «Семантика стабильной модели для логического программирования». Ковальски, Роберт; Боуэн, Кеннет (ред.). Материалы Международной конференции и симпозиума по логическому программированию . МТИ Пресс. стр. 1070–1080.
^ Камински, Марк; Грау, Бернардо Куэнка; Костылев Егор Владимирович; Мотик, Борис; Хоррокс, Ян (12 ноября 2017 г.). «Основы декларативного анализа данных с использованием программ предельной регистрации данных». arXiv : 1705.06927 [ cs.AI ].
^ Грау, Бернардо Куэнка; Хоррокс, Ян; Камински, Марк; Костылев Егор Владимирович; Мотик, Борис (25 февраля 2020 г.). «Предельный журнал данных: декларативный язык запросов для анализа данных» . Запись ACM SIGMOD . 48 (4): 6–17. дои : 10.1145/3385658.3385660 . ISSN 0163-5808 . S2CID 211520719 .

Источники

Кери, С.; Готтлоб, Г.; Танка, Л. (март 1989 г.). «Что вы всегда хотели знать о Datalog (и никогда не осмеливались спросить)» (PDF) . Транзакции IEEE по знаниям и инженерии данных . 1 (1): 146–166. CiteSeerX 10.1.1.210.1118 . дои : 10.1109/69.43410 . ISSN 1041-4347 .

[FOOTNOTECeriGottlobTanca1989146-1] Jump up to: ^а ^б Кери, Готтлоб и Танка 1989 , с. 146.

[2] Эйснер, Джейсон; Филардо, Натаниэль В. (2011). де Моор, Оге; Готтлоб, Георг; Фурче, Тим; Селлерс, Эндрю (ред.). Dyna: расширение журнала данных для современного искусственного интеллекта . Datalog Reloaded, Первый международный семинар, Datalog 2010, Оксфорд, Великобритания, 16–19 марта 2010 г. Конспекты лекций по информатике. Том. 6702. Берлин, Гейдельберг: Springer. стр. 181–220. дои : 10.1007/978-3-642-24206-9_11 . ISBN 978-3-642-24206-9 .

[3] ван Эмден, Миннесота; Ковальский, Р.А. (1 октября 1976 г.). «Семантика логики предикатов как языка программирования» . Журнал АКМ . 23 (4): 733–742. дои : 10.1145/321978.321991 . ISSN 0004-5411 . S2CID 11048276 .

[FOOTNOTECeriGottlobTanca1989149-4] Кери, Готтлоб и Танка 1989 , стр. 149.

[FOOTNOTECeriGottlobTanca1989150-5] Кери, Готтлоб и Танка 1989 , стр. 150.

[6] Абитбул, Серж (1996). Основы баз данных . Аддисон-Уэсли. ISBN 0-201-53771-0 . OCLC 247979782 .

[7] Хамис, Махмуд Або; Нго, Хунг К.; Пихлер, Рейнхард; Сучу, Дэн; Ван, Ису Реми (01 февраля 2023 г.). «Сходимость регистрации данных по (предварительным) полукольцам». arXiv : 2105.14435 [ cs.DB ].

[FOOTNOTEAbiteboul1996299-8] Jump up to: ^а ^б Абитебул 1996 , с. 299.

[9] Халеви, Алон Ю.; Мумик, Индерпал Сингх; Сагив, Иегошуа; Шмуэли, Одед (1 сентября 2001 г.). «Статический анализ в расширениях журналов данных» . Журнал АКМ . 48 (5): 971–1012. дои : 10.1145/502102.502104 . ISSN 0004-5411 . S2CID 18868009 .

[10] Леоне, Н; Рулло, П. (1 января 1992 г.). «Безопасное вычисление обоснованной семантики запросов журнала данных» . Информационные системы . 17 (1): 17–31. дои : 10.1016/0306-4379(92)90003-6 . ISSN 0306-4379 .

[11] Гельфонд, Майкл; Лифшиц, Владимир (1988). «Семантика стабильной модели для логического программирования». Ковальски, Роберт; Боуэн, Кеннет (ред.). Материалы Международной конференции и симпозиума по логическому программированию . МТИ Пресс. стр. 1070–1080.

[12] Камински, Марк; Грау, Бернардо Куэнка; Костылев Егор Владимирович; Мотик, Борис; Хоррокс, Ян (12 ноября 2017 г.). «Основы декларативного анализа данных с использованием программ предельной регистрации данных». arXiv : 1705.06927 [ cs.AI ].

[13] Грау, Бернардо Куэнка; Хоррокс, Ян; Камински, Марк; Костылев Егор Владимирович; Мотик, Борис (25 февраля 2020 г.). «Предельный журнал данных: декларативный язык запросов для анализа данных» . Запись ACM SIGMOD . 48 (4): 6–17. дои : 10.1145/3385658.3385660 . ISSN 0163-5808 . S2CID 211520719 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]