Макромодульний підхід у програмуванні включає питання, які стосуються семантичного аспекту програмування загалом [1] та програмуванню спеціально розробленою мовою зокрема. Розглянемо окремі з них.
Проаналізуємо оператор цієї мови, який задається синтаксичною формулою вигляду:
do <послідовність операторів>
while(<логічна формула>)
Означення. Логічна формула — це ланцюжок символів, які зображаються предикатом <логічна формула> в елементарній формальній системі з аксіомами:
1. <функціональний символ> +|-|*|/;
2. <предикатний символ> <|>|=;
3. <константа>x → <терм>x
4. <проблемна змінна>x → <терм>x
5. <функціональний символ>x → <терм>y → <рм>z<терм>yxz;
6. <предикатний символ>x → <терм>y → <терм>z<атом>yxz;
7. <атом>x; → <логічна формула>x;
8. <логічна формула>x → <логічна формула> y → <логічна формула>-x|x&y|x y.
Принципове питання полягає у тому, чи є довільна логічна формула загальнозначимою, чи ні. У першому випадку розглянута вище мовна конструкція призводить до „зациклювання” композиційної схеми, яка її містить. У по-іншому цикл завершується через скінченну кількість кроків.
Відомо [2], що не існує алгоритму який дозволяє розпізнати загальнозначимість довільної логічної формули. Це пов’язано з існуванням нескінченної кількості можливих інтерпретацій логічних формул. Але деякі окремі результати в цьому напрямку були одержані. Основна їх ідея полягає у тому, щоб спростити перевірку загальнозначимості формул. Це було зроблено шляхом побудови спеціальної області інтерпретації логічної формули — ербранівського базису. Він означується так:
1. Для будь-якої індивідної константи a, яка входить в логічну формулу G, покладемо a є H0. Якщо G не містить індивідних констант, то вважатимемо H0 = (c).
2. Для кожного n-місного функціонального символа f та індивідних констант a1,...,an є H0 вважатимемо f(a1,...,an) є Ha.
3. Для кожного n-місного функціонального символа f та термів g(a1,...,an),...,h(b1,...,bn) є H1 вважатимемо f (g(a1,...,an),...,h(b1,...,bn)) є Ha.
4. І так далі.
Тоді ербранівський базис H логічної формули G є об’єднанням H=H0ᴗH1ᴗ... . Зрозуміло, що при відсутності функціональних та індивідних констант ербранівський базис зводиться до множини H={c}.
Зрозуміло, що для перевірки незагальнозначимості (виконання) довільної логічної формули достатньо спростувати її на ербранівській області.
Означення. Основним прикладом диз’юнкта множини диз’юнктів S називатимемо терм, отриманий підстановкою в нього елементів ербранівського базису замість змінних.
Алгоритм доведення незагальнозначимості довільної логічної формули ґрунтується на наступній теоремі.
Теорема. Множина диз’юнктів S незагальнозначима тоді і тільки тоді, коли існує невиконувана множина S` основних прикладів диз’юнктів S.
Нехай існує скінченна невиконувана множина S` основних прикладів диз’юнктів S. Це значить, що в деякій інтерпретації I скінченна кількість диз’юнктів з S спростовується. Тому і S спростовується. Тобто S — незагальнозначима.
Процедура спростування полягає у наступному.
1. Перетворимо логічну формулу в КНФ.
2. Визначимо ербранівський базис множини диз’юнктів по рівням H0,H1,... .
3. i=0 .
4. Породжуємо множину основних прикладів диз’юнктів Si шляхом заміни змінних в S константами з Hi.
5. Якщо Si невиконувана, незагальнозначимість S встановлена.
6. i=i+1 . Перехід на 4.
Цей алгоритм завершує роботу через скінченну кількість кроків, якщо множина диз’юнктів S незагальнозначима, або працює нескінченно довго в протилежному випадку, при умові нескінченності ербранівського базису для S.
Розглянемо послідовність операторів мови як синтаксичну формулу:
do
<послідовність операторів>
assign(<проблемна змінна>,<значення проблемної змінної>)
<послідовність операторів>
while(<логічна формула>)
Присвоєння значення проблемній змінній може призвести до “зациклювання” композиційної схеми навіть при умові незагальнозначимості логічної формули.
Список використаних джерел:
1. Провотар А.И., Барткив А.Б. Верификация композиционных схем в CASE APS // Программно-алгоритмическое обеспечение решения задач прикладной математики. — Киев: Ин-т кибернетики им. В.М. Глушкова АН Украины. — 1993. — С. 43-47.
2. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем: Пер. с англ. — М.: Наука, 2013. — 360 с.
|
Голосування 
Ця робота ліцензується відповідно до Creative Commons Attribution 4.0 International License
Знайшли помилку? Виділіть помилковий текст мишкою і натисніть Ctrl + Enter