Логіка в інформатиці

Логіка в інформатиці — це напрям досліджень та галузей знань, де логіка застосовується в інформатиці та штучному інтелекті. Використання логіки дуже ефективне в цих областях.^[1]

Умовно висловлюючись, можна сказати, що комп'ютер складається з матеріальної частини та математичного (програмного) забезпечення, або, використовуючи професійну лексику, з «заліза» і «взуття». І до того, і до іншого має саме безпосереднє відношення математична логіка, ні перше, ні друге без математичної логіки обійтися не можуть.

Область застосування

Включаються такі основні застосування:

• дослідження в логіці, викликані розвитком комп'ютерних наук. Наприклад, аплікативні обчислювальні системи, теорія обчислень і моделі обчислень;

• формальні методи і логіка міркування про поняття. Наприклад, семантична мережа^[2], семантична павутина;

• булева логіка і алгебра для розробки апаратного забезпечення комп'ютерів;

• розв'язання задач і структурне програмування для розробки прикладних програм і створення складних систем програмного забезпечення

• доказове програмування — технологія розробки алгоритмів і програм із доказами правильності алгоритмів;

• фундаментальні поняття і уявлення для комп'ютерних наук, які є природною областю для формальної логіки. Наприклад, семантика мов програмування^[3];

• логіка знань і припущень. Наприклад, штучний інтелект;

• мова Пролог і логічне програмування для створення баз знань та експертних систем і досліджень у сфері штучного інтелекту;

• логіка для опису просторового положення і переміщення;

• логіка в інформаційних технологіях. Наприклад, реляційна модель даних, реляційні СКБД, реляційна алгебра, реляційне числення^[4];

• логіка обчислень з об'єктами. Наприклад, комбінаторна логіка, суперкомбінатори^[5];

• логіка для компілювання програмного коду та його оптимізації. Наприклад, категоріальна абстрактна машина;

• логіка для еквівалентного перетворення об'єктів. Наприклад, лямбда-числення;

• перевиклад логіки і математики в термінах, зрозумілих фахівцям в комп'ютерних науках^[6].

Цей список продовжує поповнюватися.

Ефективність у комп'ютерних науках

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

Тестування програм може виявити наявність помилок у програмах, але не може гарантувати їх відсутність. Гарантії відсутності помилок в алгоритмах і програмах можуть дати тільки докази їх правильності. Алгоритм не містить помилок, якщо він дає правильні розв'язки для всіх допустимих даних.

Серйозною проблемою для комп'ютерних наук та інформатики є наявність помилок в алгоритмах і програмах, що публікуються в підручниках і навчальних посібниках, а також невміння викладачів і вчителів інформатики виявляти і виправляти помилки в алгоритмах і програмах, складених учнями.

Єдиний шлях для подолання цих проблем-це вивчення систематичних методів складання алгоритмів і програм з одночасним аналізом їх правильності в рамках доказового програмування з самого початку навчання основам алгоритмізації і програмування.

Складність для викладачів і програмістів полягає в тому, що вони повинні вміти писати не тільки алгоритми і програми, а й докази правильності своїх алгоритмів і програм. На жаль, зараз це не вміють робити ні математики, ні програмісти.

В результаті програмісти пишуть програми з великим числом помилок, які вони не можуть ні виявити, ні виправити. Масоване тестування програм на ЕОМ приносить програмістам безперечну користь, проте не дає гарантій повного позбавлення від помилок.

Практика застосування та вивчення доказових методів програмування показала, що ця технологія цілком доступна студентам математичних факультетів, яким цілком під силу написання доказів правильності алгоритмів, після перевірки та тестування програм на ЕОМ.

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

Математична логіка та розвиток інформатики

Інформатика як наука почала формуватися разом з створенням і бурхливим розвитком обчислювальної техніки. Її формування і визначення її предмета тривають дотепер. Інформатика — наука про зберігання, обробки і передачі інформації за допомогою комп'ютерів. Вона включає в себе великі розділи, які вивчають алгоритмічні, програмні та технічні засоби зберігання, обробки і передачі інформації. Математична логіка виявилася єдиною математичною наукою, методи якої стали найпотужнішими інструментами пізнання у всіх розділах інформатики. Тому скільки- серйозне вивчення інформатики немислимо без освоєння основ математичної логіки.

Щоб комп'ютер працював, він повинен бути оснащений програмним забезпеченням, тобто комплексом програм, що орієнтують комп'ютер на вирішення завдань того чи іншого класу. Слово «програма» має грецьке походження і означає «оголошення», «розпорядження». Уже саме поняття комп'ютерної програми, що передбачає чіткий алгоритмічний припис комп'ютера про порядок і характер дій, передбачає проникнення в програму, а також у процес її складання (в програмування) теорії алгоритмів.

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

Фундаментальна основа програмування

Теорія алгоритмів та математична логіка — фундаментальна основа програмування. У 30-ті рр. XIX ст. англійський математик Чарлз Беббідж висловив вперше ідею обчислювальної машини. І тільки сто років по тому логіки розробили чотири математично еквівалентні моделі поняття алгоритму. Саме в теорії алгоритмів було передбачено основні концепції, які лягли в основу принципів побудови і функціонування обчислювальної машини з програмним керуванням і принципів створення мов програмування. Ідею такої обчислювальної машини вперше змогли реалізувати болгарський учений С. Атанасов в 1940 р. і німецький вчений К. Цузе в 1942 р. Чотири головні моделі алгоритму породили різні напрямки в програмуванні.

 Моделі поняття алгоритму

• Перша модель — це абстрактна обчислювальна машина (Алан Тюрінг, Р. Пост). Вона з'явилася абстрактним прообразом реальних обчислювальних машин. Дотепер всі обчислювальні машини в деякому сенсі базуються на ідеї Тюрінга: їх пам'ять фізично складається з бітів, кожен з яких містить або 0, або 1. Програмне управління успадкувало від цих абстрактних машин і програму, вміщену в «постійну пам'ять» (ідея помістити програму ЕОМ в основну пам'ять, щоб мати можливість змінювати її в ході обчислень, належить Джону фон Нейманом), а структура команди сучасної ЕОМ великою мірою нагадує структуру команди машини Тюрінга. У рамках теорії машин Тюрінга викристалізувалися найважливіші для комп'ютерних додатків логіки поняття: обчислювана функція, здійсненне завдання, нерозв'язна (алгоритмічно) задача. Зібрано велику кількість визначень абстрактних обчислювальних машин і показано, як кожне з них можна звести до іншого певним кодуванням входів і виходів.
• Друга модель — це рекурсивні функції, ідея яких сходить до гільбертівського аксіоматичного підходу. Від них успадкувало свої основні конструкції сучасне структурне програмування.
• Третій спосіб опису алгоритмів — нормальні алгоритми А. А. Маркова. Вони послужили основою мови Рефал і багатьох інших мов обробки символьної інформації.
• Четвертий напрямок в теорії алгоритмів — так зване λ-числення — базується на ідеях радянського логіка Р. Шейнфінкеля та американського логіка Гаскелла Каррі. Виявилося, що для визначення всіх обчислюваних функцій досить операцій так званої λ — абстракції і суперпозиції. Ідеї λ -числення активно розвиваються в мові Лісп, функціональному програмуванні і в багатьох інших перспективних напрямах сучасного програмування.

Математична логіка стала бурхливо розвиватися на початку XX ст. на ґрунті здавалося б виключно далекої від додатків проблеми обґрунтування математики. Але саме ці дослідження поклали початок строгому визначенню алгоритмічних мов, показали їх колосальні можливості і принципові обмеження, розвинули техніку формалізації. Тому, коли в програмуванні було усвідомлено, що всяка програма є формалізацією, тоді ті що виникли тут математичні проблеми впали на ґрунт, ретельно підготовлений математичною логікою.

Опис комп'ютерних програм за допомогою математичної логіки

Перші спроби застосувати в програмуванні розвинені логічні обчислення і методи формалізації зробив американський логік Г. Б. Каррі. У 1952 р. він зробив доповідь «Логіка програмних композицій», ідеї якої випередили свій час принаймні на чверть століття. Каррі розглянув задачу програмування, як завдання складання більших програм з готових шматків. Було введено дві базисні системи конструкцій: перша — послідовне виконання, розгалуження і цикл, друга — послідовне виконання і умовний перехід. Він охарактеризував логічні засоби, які можна використовувати для композиції програм з підпрограм в кожному з цих випадків.

Як відомо, комп'ютер є свого роду «ідеальним бюрократом»: він не сприйме програму, написану на не до кінця формалізованою мовою, і приступить до роботи лише після того, як все виражено в повній відповідності з детальними інструкціями. Тому в 1960-ті рр. на перший план вийшли завдання точного визначення формальних мов досить складної структури. Математична логіка, підтримувана ідеями програмування, успішно з ними впоралася, розробили опис синтаксису складних і багатих виражальними засобами формальних мов.

У середині 1960-х рр. практично одночасно з'явився ряд піонерських робіт у галузі опису умов, яким задовольняє програма. Радянський математик В. М. Глушков в 1965 р. ввів поняття алгоритмічної алгебри, що послужило прообразом алгоритмічних логік. Ф. Енгелер в 1967 р. запропонував використовувати мови з нескінченно довгими формулами, щоб висловити нескінченну безліч можливостей, що виникають при різних виконаннях програми. Але найбільшу популярність придбали мови алгоритмічних логік. Ці мови були винайдені практично одночасно американськими логіками Р. У. Флойдом (1967), С. А. Р. Гоаром (1969) і вченими польської логічної школи, наприклад А. Сальвіцкім (1970) та ін.

Алгоритмічна логіка (або динамічна логіка, або програмна логіка, або логіка Гоара) — розділ теоретичного програмування, в рамках якого досліджуються аксіоматичні системи, що представляють засоби для завдання синтаксису і семантики мов програмування, а також для синтезу комп'ютерних програм та їх верифікації (перевірки правильності роботи). Мови алгоритмічних логік ґрунтуються на логіці предикатів 1 -го порядку і включають в себе висловлювання виду { A } S { B }, читаються наступним чином: «Якщо до виконання оператора S було виконано A, то після нього буде виконано B». Тут A називається передумовою, B — післяумовою, або обіцянкою S. Цією мовою даються логічні описання операторів присвоєння та умовного переходу, розгалуження, циклу.

Поряд з динамічної логікою 1-го порядку розглядається пропозиціональна динамічна логіка та її узагальнення — так звана логіка процесів, в якій виражені деякі властивості програми, що залежать від процесу її виконання. Різні динамічні логіки виходять при варіюванні засобів мов програмування, що використовуються в програмах. Ці засоби містять масиви та інші структури даних, рекурсивні процедури, циклічні конструкції, а також засоби задання недетермінованих програм.

Динамічна логіка є одним з типів логічних систем, що використовуються для логічного синтезу комп'ютерних програм. Логічний синтез — один із способів переходу від специфікації програми до реалізуючого алгоритму, що має форму точного міркування в деякій логічній системі. У динамічній логіці специфікація завдання задається у вигляді двох формул обчислення предикатів — передумови і післяумови, а аксіомами логічної системи є схеми передумови та післяумови, що пов'язуються тими чи іншими конструкціями мови програмування. Синтезована програма виходить у формі виведеного в динамічної логікою твердження, яка говорить, якщо аргументи завдання задовольняють задану передумову, то результат виконання синтезованої програми задовольняє задану післяумову.

У теоретичних роботах по динамічним логікам досліджуються питання несуперечності та повноти аксіоматичних систем, алгоритмічні складні властивості множин істинних формул, порівняння виразної потужності мов динамічної логіки.

Принципово інший спосіб визначення семантики програм, придатний, скоріше для опису всієї алгоритмічної мови, а не конкретних програм, запропонував в 1970 р. американський логік Д. Скотт. Він побудував математичну модель λ-числення і показав, як переводити функціональний опис мови структурного програмування в λ-числення і як визначити математичну модель алгоритмічного мови через модель λ-числення. Ця так звана денотаційна семантика алгоритмічних мов, стала практичним інструментом побудови надійних трансляторів із складних алгоритмічних мов. Так іще одна абстрактна область математичної логіки знайшла прямі практичні застосування.

Опис програмування та аналіз його концепцій за допомогою математичної логіки

Програмування — це процес складання програми, плану дій. Було відмічено, що класична логіка погано підходить для опису цього процесу хоча б тому, що вона погано підходить взагалі для опису всякого процесу в математиці. Ще на початку XX ст. стало ясно, що в математиці давно розійшлися поняття «існувати» і «бути побудованим», які з античних часів трактувалися як синоніми. Були виявлені так звані математичні об'єкти — «привиди» (множини, Функції, числа), існування яких доведено, але побудувати які можна. Причиною їх появи з'явився ефект поєднання класичної логіки з теоремою Геделя про неповноту формальної арифметики. Один з фундаментальних законів класичної логіки — закон виключеного третього (P ˅ ˥P) в деякому вільному трактуванні фактично означає, що ми знаємо все. Цей постулат звичайно ж ніяк не можна назвати реалістичним: ми знаємо надзвичайно мало, і чим більше дізнаємося, тим краще це розуміємо. Голландський математик Л. Е. Я. Брауер визначив логічні коріння «привидів», ще до відкриття теореми Геделя, в 1908 р., і почав побудову так званої інтуїтивної математики, яка не приймає закон (P ˅ ˥P), як універсальний. У 1930—1932 рр. другий голландець А. Гейтинг строго сформулював логіку, якою користувалися в інтуїтивній математиці — інтуїтивну логіку. Її математична інтерпретація, викладена радянським математиком А. М. Колмогоровим зберегла своє значення досі.

А. М. Колмогоров розглянув логіку як числення завдань. Кожна формула алгебри висловлювань розглядається не просто як формула, а як вимога вирішити завдання, тобто побудувати об'єкт, що задовольняє деяким умовам. Це так звана конструктивна інтерпретація логіки висловлювань. Логічні зв'язки розуміються як засоби побудови формулювань більш складних завдань з простіших, аксіоми — як завдання, вирішення яких дано, правила виводу — як способи перетворення рішень одних завдань у вирішення інших. Відзначимо, що рішення задачі — це не тільки сам шуканий об'єкт, а й доказ того, що він задовольняє пропонованим вимогам. Наприклад, формула A ˄ B розуміється в колмогорівській інтерпретації як завдання, яке полягає в тому, щоб побудувати розв'язок завдання A та розв'язок завдання B, правило висновку A, B \ A ˄ B — як перетворення, яке будує з об'єкта а, розв'язок завдання A, та об'єкта b, розв'язок завдання B, пару (a, b), розв'язок завдання A ˄ B. Об'єкт a, розв'язує завдання, зіставлене формулою A, називається реалізацією A. Цей факт позначається aRA. Центральним моментом конструктивного розуміння логічних формул є інтерпретація імплікації. Конструктивна імплікація A → B розуміється, як вимога побудувати ефективне перетворення f, застосоване до всіх реалізацій формули A і переводить їх у реалізації формули B.

Нечітке колмогорівське формулювання логіки, як обчислення завдань, породила численні різні конкретизації, давши цілу систему точних математичних визначень. Це формулювання знайшло застосування не тільки в інтуїтивній логіці, для якої вона була створена, а й в інших логічних системах. Строгі математичні семантики, засновані на ідеї Колмогорова, зазвичай називають семантиками реалізованості (на відміну від інших видів логічних семантик, які базуються на системах істиннісних значень). Першу реалізованість побудував американський логік С. К. Кліні в 1940 р. для арифметики з інтуїтивною логікою. У 1960-1980-х рр. з'явилися десятки понять реалізованості, як для систем, що базуються на інтуїтивній логіці, так і для інших логік. Радянський логік А. А. Воронков в 1985 р. вивів умови, при яких класична логіка може розглядатися як конструктивна. З них, зокрема, випливає, що необхідною (але не достатньою) умовою конструктивності класичної теорії є її повнота, тобто виводимість в ній для кожної замкнутої формули F або самої F, або її заперечення ˥F. Тим самим ще раз підтвердилося прозріння Брауера щодо логічних коренів неконструктивності. Зауважимо, що прикладами класичних теорій, що мають конструктивне тлумачення, служать елементарна геометрія і алгебраїчна теорія дійсних чисел.

Опис програмування за допомогою логіки засноване на певній аналогії між висновком формули в деякому логічному обчисленні і програмою вирішення завдання, що відповідає цій формулі при конструктивній інтерпретації логіки. Логічна теорія, відповідна структурним схемам програм, з'явилася в середині 1980-х рр. Структурні схеми відповідали нарождающемуся новому типу логіки — логіки схем програм, якою користується програміст для створення складних, багатоваріантних, ітеративних планів дій.

Верифікація програм за допомогою математичної логіки

Широке використання комп'ютерів у найрізноманітніших сферах людської діяльності ставить питання надійності програмного забезпечення комп'ютерів. Як відомо, правильність створеної програми зазвичай перевіряється на ряді так званих тестових прикладів, на початкових даних, для яких результат відомий або його можна передбачити. Неважко зрозуміти, що така перевірка здатна лише виявити наявність помилок у програмі, але не довести їх відсутність.

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

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

Сформулюємо тепер точне визначення поняття правильності програми. Нехай α — програма, P — твердження, що стосується вхідних даних, яке має бути істинно перед виконанням програми α (воно називається передумовою програми α), Q — твердження, яке має бути істинно після виконання програми α(воно називається післяумовою програми α). Розрізняють два види правильності програм: часткову і тотальну (повну). Програма α називається частково правильною щодо передумови P і післяумови Q, якщо кожен раз, коли перед виконанням α передумова P істинна для вхідних значень змінних, і α завершує роботу, післяумова Q також буде істинною для вихідних значень змінних. У цьому випадку будемо використовувати запис P [ α ] Q. Програма α називається тотально правильною відносно P і Q, якщо вона частково правильна відносно P і Q, і α обов'язково завершує свою роботу для вхідних значень змінних, які відповідають умові P. У цьому випадку пишемо P [ α! ] Q.

Звернемо увагу на те, що поняття правильності програми α сформульовано щодо відповідних тверджень (умов) P і Q. Тому з істинності твердження P [ α ] Q (або P [ α ! ] Q відповідно) не обов'язково слідує істинність твердження про правильність програми при інших передумовах та післяумовах. Аналогічним чином, заміна в P [ α ] Q (або P [ α ! ] Q) програми α на програму β, взагалі кажучи, не зберігає істінностного значення твердження про правильність. Не слід також думати, що за даних умов P і Q існує тільки одна програма α, для якої висловлення P [ α ] Q (або P [ α ! ] Q) істинно.

Говорити про правильність програми самої по собі безглуздо. Програма пишеться з метою вирішення тієї чи іншої конкретної задачі. Кожна правильно поставлена задача містить у собі умову (те, що дано) і питання, на які потрібно дати відповідь. При складанні програми умова задачі перетворюється на передумову, а питання перетвориться в післяумову, що має вже форму не питання, а твердження, яке має бути істинно всякий раз, коли відповідь на питання задачі правильна.

З визначень випливає, що всяка тотально правильна програма є частково правильною при тих же передумовах і післяумовах. Зворотне звичайно ж невірно. Зрозуміло, що тотальна правильність «краща» за часткову, хоча довести тотальну правильність програми, мабуть, складніше, ніж часткову.

Для доказу часткової правильності операторних програм зазвичай використовуються різні модифікації методу Флойда, який полягає в наступному. На схемі програми вибираються контрольні точки так, щоб будь-який циклічний шлях проходив принаймні через одну точку. З кожною контрольною точкою асоціюється спеціальна умова (індуктивне твердження або інваріант циклу), яка істинна при кожному переході через цю точку. З входом і виходом схеми також асоціюються перед- і післяумови. Потім кожному шляху програми між двома сусідніми контрольними точками зіставляється так звана умова правильності. Виконуваність всіх умов правильності гарантує часткову правильність програми.

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

Одна з модифікацій методу Флойда полягає в побудові кінцевої аксіоматичної системи (так званої «логіки Гоара»), що складається з схем аксіом і правил виводу, в якій як теореми виводяться твердження про часткову правильність програм, зокрема мовою програмування Паскаль. Така система використовується і для завдання аксіоматичної семантики мови Паскаль. Аксіоматичні системи, родинні логіці Гоара, розроблені і для інших алгоритмічних мов програмування.

Для доказу правильності рекурсивних програм використовується метод математичної індукції, пов'язаний з визначенням найменшої нерухомої точки, а для програм зі складними структурами даних (наприклад, графами, деревами) — індукція за структурою даних. При цьому в теоретичних дослідженнях за логікою Гоара розглядаються звичайні властивості Аксіоматизації в логіці — їх несуперечність і повнота.

Див. також

• Програмування
• Парадигма програмування
• Структурне програмування
• Логічне програмування
• Інформатика
• Комбінаторна логіка
• Розв'язання задач
• Доказове програмування
• Математична логіка
• Логіка Гоара
• Верифікація програмного забезпечення
• Алгоритм

Посилання

• Математична логіка та мови програмування [Архівовано 11 квітня 2017 у Wayback Machine.]
• Математична логіка та інформатика [Архівовано 11 квітня 2017 у Wayback Machine.]
• Математична логіка і логічне програмування [Архівовано 11 квітня 2017 у Wayback Machine.]

Примітки

1. Halpern J.Y., Harper R., Immerman N., Kolaitis Ph.G., Vardi M.Y., and Vianu V. On the unususal effectiveness of logic in computer science. — January, 2001 [Архівовано 30 липня 2012 у Wayback Machine.].
2. Roussopoulos N.D. A semantic network model of data bases. — TR No 104, Department of Computer Science, University of Toronto, 1976.
3. Scott D.S. The lattice of flow diagrams.-- Lecture Notes in Mathematics, 188, Symposium on Semantics of Algorithmic Languages.-- Berlin, Heidelberg, New York: Springer-Verlag, 1971, pp.~311-372.
4. Codd E. F. Relational Completeness of Data Base Sublanguages. [Архівовано 18 травня 2008 у Wayback Machine.] In: R. Rustin (ed.): Database Systems: 65-98, Prentice Hall and IBM Research Report RJ 987, San Jose, California, 1972.
5. Peyton Jones S., Eber J.-M., Seward J. Composing contracts: an adventure in financial engineering. [Архівовано 2 грудня 2008 у Wayback Machine.] — ICFP 2000
6. Asperti A, and Longo G. Categories, Types and Structures. Category Theory for the working computer scientist. — M.I.T. Press, 1991 (pp. 1-300)

Література

• 'Логіко-інформаційна система // Філософський енциклопедичний словник / В. І. Шинкарук (гол. редкол.) та ін. — Київ : Інститут філософії імені Григорія Сковороди НАН України : Абрис, 2002. — 742 с. — 1000 екз. — ББК 87я2. — ISBN 966-531-128-X.
• Вольфенгаген В. Э. Логика. Конспект лекций: техника рассуждений. 2-е изд., дополн. и перераб. — М: АО «Центр ЮрИнфоР», 2004. — 229 с ISBN 5-89158-135-3.
• Математическая логика и теория алгоритмов, Игошин В. И., 2008
• Колмогоров А. Н., Драгалин А. Г. Математическая логика. Изд. 3-е, 2006.
• П.Грогоно, Программирование на языке Pascal, М.:Мир, 1982, с.295, (Тестирование и верификация).