Пролог – декларативный язык, способный решать любые ребусы и доказывать теоремы
Представьте себе высокоуровневый язык, в котором не нужно указывать КАК получить результат, вместо этого нужно просто указать ЧТО вы хотите получить. При этом область применения языка не ограничена и язык способен решать те же задачи, что и любой другой высокоуровневый язык, наподобие JAVA. Кажется фантастикой, не правда ли? Однако такой язык есть и называется он PROLOG. Посмотрим как PROLOG справляется с этой задачей на примере загадывания прологу некоторых загадок и попросим PROLOG выдать доказательство теоремы.
Загадка 1. Простенькая, математическая.»?» — произвольная математическая операция (+,-,*,/), дано уравнение ((((1?2)?3)?4)?5)?6=35. Найти неизвестные операции.Начнём описывать, что мы хотим получить. Поскольку знак операции неизвестен, он будет параметром.
formula (X1, X2, X3, X4, X5, X6, Sign1, Sign2, Sign3, Sign4, Sign5, Result):-operation (X1, X2, Sign1, PartialResult1), operation (PartialResult1, X3, Sign2, PartialResult2), operation (PartialResult2, X4, Sign3, PartialResult3), operation (PartialResult3, X5, Sign4, PartialResult4), operation (PartialResult4, X6, Sign5, Result).
Эта строка описывает формулу 1?2?3?4?5?6=Result. Фактически, она означает: формула верна, если существуют частичный результат 1, частичный результат 2… частичный результат 4, такие что верны операции. Однако пролог не знает что такое операция, поэтому опишем в каких случаях они верны:
operation (X1, X2,»+», Result) :- Result = X1 + X2.operation (X1, X2,»*», Result) :- Result = X1 * X2.operation (X1, X2,»/», Result) :- Result = X1 / X2.operation (X1, X2,»-», Result) :- Result = X1 — X2.
Мы описали формулу, и теперь мы можем задавать любые вопросы относительно неё. Например, мы можем задать следующие вопросы: 1)если X1=1×2=2… X6=6 Result=35 то какие возможны операции? 2)указана часть числовых параметров и часть операций, а также результат, узнать, каковы недостающие параметры? 3)указаны все операции, числовые параметры, результат; узнать, верна ли формула. При этом не нужно заботиться о том, как именно пролог найдёт ответ — нужно просто задать вопрос.
Итак, вопрос: askMainQuestion ():-formula (1,2,3,4,5,6, Sign1, Sign2, Sign3, Sign4, Sign5,35), stdio: write (Sign1, Sign2, Sign3, Sign4, Sign5), stdio: nl, %new linefail.
Ответ: ++*++, +**±, ***++ (Для задавания вопроса о числовых параметрах придётся написать ещё пару строк, но об этом чуть позже.)
Посмотреть код программы полностью (Visual Prolog 7.5) implement mainopen coreclass predicatesaskMainQuestion:() procedure.operation: (real, real, string, real) multi (i, i, o, o).formula: (real, real, real, real, real, real, string, string, string, string, string, real) nondeterm (i, i, i, i, i, i, o, o, o, o, o, i).abs: (real, real) nondeterm (i, o).clauses
operation (X1, X2,»+», Result) :- Result = X1 + X2.operation (X1, X2,»-», Result) :- Result = X1 — X2.operation (X1, X2,»*», Result) :- Result = X1 * X2.operation (X1, X2,»/», Result) :- Result = X1 / X2.
formula (X1, X2, X3, X4, X5, X6, Sign1, Sign2, Sign3, Sign4, Sign5, Result):-operation (X1, X2, Sign1, PartialResult1), operation (PartialResult1, X3, Sign2, PartialResult2), operation (PartialResult2, X4, Sign3, PartialResult3), operation (PartialResult3, X5, Sign4, PartialResult4), operation (PartialResult4, X6, Sign5, FinalResult), abs (FinalResult-Result, Difference), Difference<0.0001. %учитывание ошибок округления при делении
abs (X, Result) :- X>=0, Result=X.abs (X, Result) :- X<0, Result=-X.
askMainQuestion ():-formula (1,2,3,4,5,6, Sign1, Sign2, Sign3, Sign4, Sign5,35), stdio: write (Sign1, Sign2, Sign3, Sign4, Sign5), stdio: nl, fail.
askMainQuestion ().
run () :-console: init (), askMainQuestion (),_ = stdIO: readchar ().
end implement main
goalmainExe: run (main: run).
Загадка 2. Простенькая, нематематическая. Даны имена людей и родстенные отношения между ними. Найти всех братьев. Укажем конкретные родственные связи: parent («Tom», «Jake»).parent («Jim», «Jake»).parent («Timmi», «Tom»).uncle («Tom», «Peter»).brother («Timmi», «Cartman»).
Теперь опишем что означает родственная связь:
brother (Man1, Man2) :- parent (Man1, Parent), parent (Man2, Parent), Man1<>Man2.
(Человек1 и Человек2 братья, если существует ЧеловекРодитель, который является родителем для Человека1 и Человека2, и при этом Человек1 — это не Человек2).
brother (Man1, Man2) :- parent (ChildMan1, Man1), uncle (ChildMan1, Man2).
(Человек1 и Человек2 братья, если у Человека1 есть ребёнок, и Человек2 дядя этого ребёнка).
Теперь зададим вопрос о том, кто является братьями:
askMainQuestion ():-brother (X, Y), stdIO: write (X,» », Y), stdio: nl, fail.
Посмотреть код программы полностью implement mainopen coreclass predicatesaskMainQuestion:() procedure.parent: (string, string) multi (o, o) nondeterm (o, i) nondeterm (i, o).brother: (string, string) nondeterm (o, o) nondeterm (i, o).uncle: (string, string) nondeterm anyflow.clauses
parent («Tom», «Jake»).parent («Jim», «Jake»).parent («Timmi», «Tom»).uncle («Tom», «Peter»).
/*uncle (Man1, Man2) :- parent (Man1, ParentMan1), brother (ParentMan1, Man2). расскомментирование этой строки уронит программу*/brother («Timmi», «Cartman»).brother (Man1, Man2) :- parent (ChildMan1, Man1), uncle (ChildMan1, Man2).brother (Man1, Man2) :- parent (Man1, Parent), parent (Man2, Parent), Man1<>Man2.
askMainQuestion ():-brother (X, Y), stdIO: write (X,» », Y), stdio: nl, fail.
askMainQuestion ().
run () :-console: init (), askMainQuestion (),_ = stdIO: readchar ().
end implement maingoalmainExe: run (main: run).
Вывод программы: Timmi Cartman, Jake Peter, Tom Jim, Jim Tom. Сравните с тем, какое количество кода пришлось бы написать на императивном языке программирования.Теперь давайте рассмотрим что-нибудь посложнее Hello World-ных программ и поговорим о подводных камнях пролога.
Загадка 3. На шахматной доске стоит 8 ферзей. Ни один ферзь не бьёт другого ферзя. Найти расположение ферзей. Сначала опишем как может ходить ферзь:
attack (X1, Y1, X2, Y2) :- X2 = X1. %ферзь может атаковать, если атакуемая клетка и исходная на одной вертикалиattack (X1, Y1, X2, Y2) :- Y2 = Y1. % ферзь может атаковать, если атакуемая клетка и исходная на одной вертикалиattack (X1, Y1, X2, Y2) :- abs (X2 — X1, Abs), abs (Y2 — Y1, Abs). %… на одной диагонали
Теперь укажем в каких случаях ферзь не может бить другого ферзя:
any (0).any (1).any (2).any (3).any (4).any (5).any (6).any (7).dontAttack (X1, Y1, X2, Y2) :-any (X1), any (Y1), any (X2), any (Y2), not (attack (X1, Y1, X2, Y2)).
Тут возникает вопрос, зачем нужно перечисление всех возможных координат ферзя (any). Дело в том, что пролог устроен так, что он не может перебирать все возможные числовые или строковые значения. Все возможные значения величины, относительно которой задаётся вопрос, должны быть или перечислены в коде (как например, знаки в примере про нахождение знаков), или напрямую вычисляться на основе входных данных в вопросе (как например, результат формулы в примере про нахождение знаков, если в формуле не учитывать ошибки округления). Конечно, такое ограничение делает пролог не самым удобным языком для решения уравнений; однако, это никогда и не было основным предназначением этого языка.
Итак, мы описали, что означает что «один ферзь не бьёт другого ферзя», теперь нужно указать что каждый из 8 ферзей не бьёт другие 7 ферзей, однако писать 8×7=56 правил утомительно, поэтому опишем это правило рекурсивно. Зададим пустой массив и будем итеративно по одному добавлять в него по одному ферзю.
dontAttack ([]).
(если нет ферзей, то никакой ферзь не бьёт никакого другого)
dontAttack (X, Y, []) :- any (X), any (Y).
(если есть один единственный ферзь, то он не бьёт других ферзей)
dontAttack (X1, Y1, [X2, Y2 | OtherElements]) :-dontAttack ([X2, Y2 | OtherElements]), dontAttack (X1, Y1, X2, Y2), dontAttack (X1, Y1, OtherElements).
(если есть ферзь с координатами X1 и Y1 и массив ферзей, то ни один ферзь не бьёт другого, если 1) внутри массива ферзей ни один ферзь не бьёт другого 2)ферзь (X1, Y1) не бьёт первого ферзя из массива ферзей 3)если убрать из массива ферзей первого ферзя, то в полученном множестве ферзей ни один ферзь также не бьёт другого)
dontAttack ([X1, Y1 | OtherElements]) :-dontAttack (X1, Y1, OtherElements).
(если есть ферзь с координатами X1 и Y1 и массив ферзей, и ни один ферзь не бьёт другого, то если добавить ферзя в массив ферзей, то ни один ферзь по-прежнему не будет бить другого)
Теперь осталась задать вопрос о координатах этих ферзей. Однако, чтобы не получить множества одинаковых ответов, отличающихся лишь нумерацией ферзей, давайте скажем, что первый ферзь стоит в первом столбце, второй — во втором, и т.д.:
askMainQuestion ():-X1=0, X2=1, X3=2, X4=3, X5=4, X6=5, X7=6, X8=7, dontAttack ([X1, Y1, X2, Y2, X3, Y3, X4, Y4, X5, Y5, X6, Y6, X7, Y7, X8, Y8]), stdio: write (X1,»:», Y1,» — », X2,»:», Y2,» — », X3,»:», Y3,» — », X4,»:», Y4,» — », X5,»:», Y5,» — », X6,»:», Y6,» — », X7,»:», Y7,» — », X8,»:», Y8), stdio: nl, %new linefail.
Запускам программу, и в ту же секунду получаем все возможные расстановки ферзей на шахматной доске.
Посмотреть код программы полностью implement mainopen coreclass predicatesaskMainQuestion:() procedure.dontAttack: (integer, integer, integer, integer) nondeterm anyflow.attack: (integer, integer, integer, integer) nondeterm (i, i, i, i). %nondeterm anyflow.any:(integer) multi (o) determ (i).dontAttack: (integer, integer, integer*) nondeterm anyflow.dontAttack: (integer*) nondeterm anyflow.abs: (integer, integer) nondeterm (i, o) nondeterm (i, i).clauses
any (0).any (1).any (2).any (3).any (4).any (5).any (6).any (7).
attack (X1, Y1, X2, Y2) :- X2 = X1.attack (X1, Y1, X2, Y2) :- Y2 = Y1.attack (X1, Y1, X2, Y2) :- abs (X2 — X1, Abs), abs (Y2 — Y1, Abs).
dontAttack (X1, Y1, X2, Y2) :-any (X1), any (Y1), any (X2), any (Y2), not (attack (X1, Y1, X2, Y2)).
dontAttack (X1, Y1, [X2, Y2 | OtherElements]) :-dontAttack ([X2, Y2 | OtherElements]), dontAttack (X1, Y1, X2, Y2), dontAttack (X1, Y1, OtherElements).
dontAttack (X, Y, []) :- any (X), any (Y). %Граничное условие
dontAttack ([X1, Y1 | OtherElements]) :-dontAttack (X1, Y1, OtherElements).
dontAttack ([]).
askMainQuestion ():-X1=0, X2=1, X3=2, X4=3, X5=4, X6=5, X7=6, X8=7, dontAttack ([X1, Y1, X2, Y2, X3, Y3, X4, Y4, X5, Y5, X6, Y6, X7, Y7, X8, Y8]), stdio: write (X1,»:», Y1,» — », X2,»:», Y2,» — », X3,»:», Y3,» — », X4,»:», Y4,» — », X5,»:», Y5,» — », X6,»:», Y6,» — », X7,»:», Y7,» — », X8,»:», Y8), stdio: nl, %new linefail.
askMainQuestion ().
abs (X, Result) :- X>=0, Result=X.abs (X, Result) :- X<0, Result=-X.
run () :-console: init (), askMainQuestion (),_ = stdIO: readchar ().
end implement main
goalmainExe: run (main: run).
Теперь давайте попросим пролог доказать простенькую теорему. Подмножество группы является подгруппой тогда и только тогда, когда для любых элементов A и B из этого подмножества результат произведения A на обратный к B лежит в этом подмножестве. Для того, чтобы доказать, что подмножество является подгруппой, нужно доказать три пункта: 1)нейтральный элемент лежит в подмножестве 2)для каждого элемента из подмножества его обратный элемент лежит в подмножестве 3)произведение любых двух элементов подмножества лежит в подмножестве.Обозначим нейтральный элемент как «E» и дадим определение нейтрального элемента:
operation (A, «E», A) :- any (A).operation («E», A, A) :- any (A).
Элемент нейтральный, если при умножении любого элемента на нейтральный получается исходный элемент. (например, в целых числах 1 — это нейтральный элемент).
Добавим парочку конкретных элементов.
any («E»).any («M»).any («A»).any («B»).any («notA»).any («notB»).
Тут были введены некоторые другие элементы, помимо «E», поясним что это за элементы, описав их свойства:
ofGroup («M», «Set»).ofGroup («A», «SubSet»).ofGroup («B», «SubSet»).
А и B — элементы из подмножества, M — элемент из множества.
obratni («B», «notB»).obratni («notB», «B»).obratni («A», «notA»).obratni («notA», «A»).obratni («E», «E»).
«notA» — обратный к «A», «notB» — обратный к «B»
Теперь дадим определение обратного элемента:
operation (A, B, «E») :- obratni (A, B).operation (B, A, «E») :- obratni (A, B).
А обратный к B, если при умножении A на B получается нейтральный элемент (например 2×0,5 = 1). Как видите, у A и B здесь нет кавычек, это значит что имеются ввиду не конкретные элементы «А» и «В», а любые элементы.
Определение подмножества:
ofGroup (X, «Set») :- ofGroup (X, «SubSet»).
(элемент принадлежит множеству, если он принадлежит подмножеству)
Теперь укажем, что для любых элементов A и B из подмножества результат произведения A на обратный к B лежит в этом подмножестве (по условию теоремы)
ofGroup (C, «SubSet») :- obratni (B, NotB), operation (A, NotB, C), ofGroup (A, «SubSet»), ofGroup (B, «SubSet»), stdio: write (C,» is from subset, because », A,»*», NotB,»=», C,».»), stdio: nl.
Как видите, здесь мы добавили вывод на экран (stdio: write), это сделано чтобы трассировать действия пролога, узнать как пролог использовал это правило, чтобы увидеть ход доказательства теоремы.
Теперь осталось доказать три пункта из теоремы.Зададим вопрос про нейтральный элемент «E»:
firstQuestion () :-ofGroup («E», «SubSet»), stdio: write («E is from subset»),!…firstQuestion () :- stdio: write («E is NOT from subset»).
Про обратный элемент:
secondQuestion ():-ofGroup («notA», «SubSet»), stdio: write («notA is from subset»),!…secondQuestion () :- stdio: write («NotA is NOT from subset»).
Тут у вас мог возникнуть вопрос: нужно доказать что для любого элемента из подмножества, его обратный элемент принадлежит подмножеству, однако в вопросе прологу мы указали один единственный конкретный элемент — «notA». На самом деле, поскольку мы не накладывали на элемент «notA» никаких ограничений (кроме того, что это обратный элемент к элементу, принадлежащего подмножеству), то если мы возьмём любой обратный элемент, то для него будут верны все те же рассуждения, которые мы применили к «notA». Математики часто пользуются этим приёмом при доказательстве теорем. Этот приём особенно важен для Prolog-а, ведь он не может перебирать все строковые и численные значения.
Ну и теперь зададим вопрос про принадлежность к подмножеству результата произведения двух элементов из подмножества:
operation («A», «B», «AB»).thirdQuestion ():-operation («A», «B», AB), ofGroup (AB, «SubSet»), stdio: write («A*B is from subset»),!…thirdQuestion () :- stdio: write («A*B is NOT from subset»).
Запускаем… И программа падает, повиснув, от переполнения стека! Давайте разберёмся, почему это произошло. По сути, пролог пытается найти решение перебором введённых в него фактов. При поиске ответа на главный вопрос, пролог перебирает все факты, хоть как-то связанные с вопросом. Если неизвестно, истинен ли факт, он в свою очередь перебирает все факты, связанные уже с этим фактом. И так, пока не дойдёт до безусловных фактов, например до obratni («A», «notA») — «notA» обратный к «A». Был задан вопрос: принадлежит ли нейтральный элемент к подмножеству. Пролог видит правило ofGroup (C, «SubSet») :- obratni (B, NotB), operation (A, NotB, C), ofGroup (A, «SubSet»), ofGroup (B, «SubSet») и понимает, что если в качестве С подставить нейтральный элемент и найти A и B, удовлетворяющие правилу, то согласно правилу нейтральный элемент будет принадлежать подмножеству. Первым элементом среди существующих указан как раз таки обратный (any («E»)), поэтому Prolog выбирает его в качестве B. Итак, obratni («E», NotB). После этого Prolog задаёт вопрос:, а какой элемент обратный к «E»? — и находит ответ (obratni («E», «E»)). Итак, NotB = «E». После этого Prolog идет дальше по правилу и видит operation (A, NotB, C), в данному случае operation (A, «E», «E») и задаёт вопрос: какой элемент при перемножении на «E» даёт «E» — и находит ответ «E» (из правила operation (A, «E», «E») :- obratni (A, «E») и факта obratni («E», «E»).). Итак, A = «E».Идём по исходному правилу дальше: ofGroup (A, «SubSet»), в данном случае ofGroup («E», «SubSet»). И тут Prolog пытается ответить на тот же самый вопрос, что мы задавали вначале –, а принадлежит ли «E» к «SubSet» (нейтральный к подгруппе)? Программа зацикливается и начинает снова перебирать те же самые факты и правила, ходя по замкнутому кругу. Ну что ж, перепишем немного исходное правило: ofGroup (C, «SubSet») :- obratni (B, NotB), NotB<>«E», NotB<>«M», operation (A, NotB, C), ofGroup (A, «SubSet»), ofGroup (B, «SubSet»), stdio: write (C,» is from subset, because », A,»*», NotB,»=», C,».»), stdio: nl.Теперь в качестве NotB нельзя использовать «E» и «M», и программа не повиснет (да-да, и на «M» она тоже повисает).После этого программа в ту же секунду выдаёт доказательство трёх пунктов теоремы:
E is from subset, because B*notB=E.E is from subset (A и B лежат в подмножестве, поэтому произведение A на обратный к B лежит в подмножестве. Вывод доказательства можно сделать более подробным, если добавить больше команд write в правила)
E is from subset, because B*notB=E.notA is from subset, because E*notA=notA.notA is from subset
E is from subset, because B*notB=E.notB is from subset, because E*notB=notB.AB is from subset, because A*B=AB.A*B is from subset
Посмотреть код программы полностью implement mainopen coredomainsany = string.group = string.class predicatesfirstQuestion:() procedure.secondQuestion:() procedure.thirdQuestion:() procedure.operation: (any, any, any) nondeterm (i, i, i) nondeterm (o, i, i) nondeterm (i, i, o) nondeterm (o, o, i) nondeterm (o, o, o) nondeterm (i, o, i) nondeterm (i, o, o) nondeterm (o, i, o).obratni: (any, any) nondeterm (i, i) nondeterm (o, i) nondeterm (o, o) nondeterm (i, o).ofGroup: (any, group) nondeterm (i, i) nondeterm (o, i) nondeterm (i, o).any: (string) nondeterm (i) nondeterm (o).clauses
operation (A, B, «E») :- obratni (A, B).operation (B, A, «E») :- obratni (A, B).operation (A, «E», A) :- any (A).operation («E», A, A) :- any (A). %коммутативность относительно нейтрального и обратного является следствием из ассоциативности, но не входит в миниммальное определение группыoperation («A», «B», «AB»). %умножение А на В возможно
obratni («M», «notM»).obratni («notM», «M»).obratni («B», «notB»).obratni («notB», «B»).obratni («A», «notA»).obratni («notA», «A»).obratni («E», «E»).
any («E»).any («M»).any («A»).any («B»).any («notA»).any («notB»).any («notM»).
ofGroup (X, «Set») :- ofGroup (X, «SubSet»). %Определение подмножестваofGroup («E», «Set»).ofGroup («M», «Set»).ofGroup («A», «SubSet»).ofGroup («B», «SubSet»).ofGroup («notB», «Set»).ofGroup («notA», «Set»).
ofGroup (C, «SubSet») :- obratni (B, NotB), NotB<>«E», NotB<>«M», operation (A, NotB, C), ofGroup (A, «SubSet»), ofGroup (B, «SubSet»), stdio: write (C,» is from subset, because », A,»*», NotB,»=», C,».»), stdio: nl. % a (-b) э Set
firstQuestion () :-ofGroup («E», «SubSet»), stdio: write («E is from subset»),!…
firstQuestion () :- stdio: write («E is NOT from subset»).
secondQuestion ():-ofGroup («notA», «SubSet»), stdio: write («notA is from subset»),!…
secondQuestion () :- stdio: write («NotA is NOT from subset»).
thirdQuestion ():-operation («A», «B», AB), ofGroup (AB, «SubSet»), stdio: write («A*B is from subset»),!…
thirdQuestion () :- stdio: write («A*B is NOT from subset»).
run () :-console: init (), firstQuestion (), stdio: nl, stdio: nl, stdio: nl, secondQuestion (), stdio: nl, stdio: nl, stdio: nl, thirdQuestion (),_ = stdIO: readchar ().
end implement main
goalmainExe: run (main: run).
Вывод Prolog — замечательный декларативный язык, однако постоянные повисания не делают ему чести (если кто-нибудь знает способы борьбы с этим, просьба поделиться в комментариях). В самом деле, задача поиска циклов в графах решена давным давно, и устранение проблемы на уровне языка — вполне решаемая задача! Если бы эта проблема была решена, можно было бы составить базу знаний всех известных математических фактов, и задавать любые вопросы! Или например, изменить одну из базовых аксиом математики и в моментально узнать как изменятся другие законы (а-ля геометрия Лобачевского в мгновение ока)! Конечно, я настроен несколько оптимистично, и языку требуется немного больше доработок, но всё же… Например, одна из возможных доработок: Prolog должен уметь не только выходить из зацикливания, но и уметь обрабатывать зацикливания по определённым правилам, чтобы оперировать с бесконечными последовательностями, удовлетворяющими условию теоремы, как например в теореме Больцано-Вейерштрасса. Впрочем, в текущем состоянии Prolog врят ли пригоден вообще для чего бы то ни было: для поиска причин зацикливаний у меня ушло даже больше времени, чем для доказательства самой теоремы! (Имхо, всего лишь моё мнение)
