PROLOG І ЧИСТЕ ЛОГІЧНЕ ПРОГРАМУВАННЯ

Мова Prolog був створений як програмне середовище логічного програмування, в якій рішення знаходить машина виведення на основі відомих аксіом. Однак реалізація принципів логічного програмування пов'язана з такими ж проблемами, з якими зіткнулися автори автоматизації винахідницької діяльності на основі ТРВЗ (див. Параграф 1.1).

Однією з проблем є неповнота опису завдань в математичній логіці. Наприклад, у наведеному раніше математичному визначенні факторіала

мається на увазі, що IV- натуральне число. Крім того, тут неявним чином до читача доводиться інформація, що спочатку слід порівняти поточне значення змінної з нулем, а тільки при неуспішному порівнянні заглиблюватися в рекурсію. При успішному же порівнянні нікому не прийде в голову шукати альтернативні рішення для IV = 0. Тепер ще раз подивимося на обчислення факторіала на мові Prolog.

factorial (0,1).

factorial (N, F) N1 is Nl, factorial (N1, FI),

F is N * F1.

Оскільки машина виведення мови Prolog перебирає предикати в базі знань в тому порядку, в якому вони записані в програмі, це відповідає такому ж неявному принципом, що використовується в математичній нотації. Якщо ж ми поміняємо місцями предикати factorial, то програма гарантовано впаде в нескінченну рекурсію.

Розглянемо дуже просту програму, що використовує даний предикат:

go: - read (X),

factorial (X, F),

F> 100 / write ( 'Large factorial');

write ( 'Small factorial').

Ця програма зчитує число з вхідного потоку і обчислює його факторіал. Якщо отриманий факторіал більше 100, то на екран виводиться повідомлення, що факторіал великий, інакше - повідомлення, що факторіал маленький. Тепер, якщо ми вкажемо мета go і введемо число 1, то замість очікуваного тексту Small factorial отримаємо повідомлення

ERROR: Out of local stack.

У чому ж справа? Проблема полягає в тому, що при невиконанні умови F> 100 Prolog намагається знайти альтернативне рішення для факторіала, а саме після поглиблення в рекурсію до значення N = 0 буде намагатися застосувати другий примірник предиката factorial і, природно, потрапить в область негативних чисел.

Виправити ситуацію допоможе наступна модифікація предикатів обчислення факторіала:

factorial (0,1).

factorial (N, F) N> 0, N1 is Nl,

factorial (N1, FI), F is N * F1.

Тепер другий предикат виконується тільки для позитивних N. Крім того, порядок проходження предикатів в тексті програми вже не важливий.

Як ми бачимо, Prolog вирішує завдання методом перебору, що обмежує його можливості для нескінченних вихідних множин. Спробуємо тепер довести методами логічного програмування просту теорему, що оперує зі змінними, і будемо використовувати числа Пеано. Доведемо, що сума парних чисел є парним числом.

Для початку згадаємо наведене раніше визначення парного числа:

Правило evz визначає четноеть нуля, а правило evs - парність числа N + 2, на 2 більшого, якщо N - парне число. Правила для підсумовування чисел Пеано виглядають наступним чином:

Правило pz задає залежність 0 + N = N, а правило ps - М + + 1 + N = S + 1, якщо М + N = S. Тепер можна сформулювати теорему про суму парних чисел:

Для будь-яких т, п, якщо even (m) і even (n), то існує таке s, що plus (m, п, s) і even (s).

Доведення. Використовуємо правила визначення парного числа evz і evs.

Випадок !: :, де від = 0.

evenin ') - припущення

plus ( 0, п, п) - випливає з правила evz

Таким чином, існує таке s, що plus ( 0, п, s) і events).

Випадок 2: , де т = (р (р (т '))).

even (n) - припущення

plus (m ', п', s ') і even (s') для деяких s '- припущення plus (p (m'), п, p (s ')) - з правила ps

plus (p (p (m ')), п, p (p (s'))) - з правила ps

even (p (p (s '))) - з правила evs

Існує таке s, що plus (p (m '), п, p (s')) і even (s)

Теорема доведена.

Однак спроба реалізувати подібне доказ на мові Prolog призведе до того, що доведеться обмежувати число значень, які перебираються в ході докази. Так, якщо записати на мові Prolog наведене вище визначення парного числа

even (0),

even (N) N1 is N-2, even (N1),

то на відміну від індуктивного визначення тут є рекурсія, що не допускає абстракції. Поки Prolog не огорнули до нуля, він не зможе визначити парність числа. Доказ даної теореми на мові Prolog може виглядати приблизно так:

proof (X, Y) even (X), even (Y),

Z is X + Y, even (Z).

Корінна відмінність доказів методами логічного програмування полягає в тому, що тут досить розглянути лише два випадки: 0 + N = NviM + 2 + N = S, якщо М + N = S 1, де А /, N, S - парні числа. Методами імперативного програмування ми повинні перевіряти гіпотези для кожної пари чисел, а оскільки безлічі цілих чисел нескінченні, такий доказ неможливо.

 
Переглянути оригінал
< Попер   ЗМІСТ   ОРИГІНАЛ   Наст >