Пролог - декларативна мова, здатна вирішувати будь-які ребуси і доводити теореми

Пролог - декларативна мова, здатна вирішувати будь-які ребуси і доводити теореми

Уявіть собі високорівневу мову, в якій не потрібно вказувати ЯК отримати результат, замість цього потрібно просто вказати ЩО ви хочете отримати. При цьому область застосування мови не обмежена і мова здатна вирішувати ті ж завдання, що і будь-яка інша високорівнева мова, на зразок 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 X2 = 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 line

fail.

Відповідь: + + * + +, + * * + -, * * * + + (Для задавання питання про числові параметри доведеться написати ще пару рядків, але про це трохи пізніше.)

Переглянути код програми повністю (Visual Prolog 7.5)

implement main

open core

class predicates

askMainQuestion:() 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

goal

mainExe::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 main

open core

class predicates

askMainQuestion:() 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 main

goal

mainExe::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 line

fail.

Запускам програму і в ту ж секунду отримуємо всі можливі розстановки ферзей на шаховій дошці.

Переглянути код програми повністю

implement main

open core

class predicates

askMainQuestion:() 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 line

fail.

askMainQuestion().

abs(X, Result) :- X>=0, Result=X.

abs(X, Result) :- X<0, Result=-X.

run() :-

console::init(),

askMainQuestion(),

_ = stdIO::readchar().

end implement main

goal

mainExe::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 лежить у підмножині. В даному випадку замість A і B взято один і той же елемент «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 main

open core

domains

any = string.

group = string.

class predicates

firstQuestion:() 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

goal

mainExe::run(main::run).

Вивід

Prolog - чудова декларативна мова, проте постійні повисання не роблять їй честі (якщо хто-небудь знає способи боротьби з цим, прохання поділитися в коментарях). Справді, завдання пошуку циклів у графах вирішене давним давно, і усунення проблеми на рівні мови - цілком вирішуване завдання! Якби ця проблема була вирішена, можна було б скласти базу знань усіх відомих математичних фактів, і ставити будь-які питання! Або наприклад, змінити одну з базових аксіом математики і в моментально дізнатися як зміняться інші закони (а-ля геометрія Лобачевського в мить ока)! Звичайно, я налаштований дещо оптимістично, і мові потрібно трохи більше доопрацювань, але все ж... Наприклад, одна з можливих доробок: Prolog повинен вміти не тільки виходити із зациклювання, але і вміти обробляти зациклювання за певними правилами, щоб оперувати з нескінченними послідовностями, що задовольняють умову теореми, як наприклад в теоремі Больцано-Вейерштрасса. Втім, в поточному стані Prolog брешуть взагалі для чого б то не було: для пошуку причин зациклювань у мене пішло навіть більше часу, ніж для доказу самої теореми! (Імхо, лише моя думка)

Image