Умовно висловлюючись, можна сказати, що комп'ютер складається з матеріальної частини та математичного (програмного) забезпечення, або, використовуючи професійну лексику, з «заліза» і «взуття». І до того, і до іншого має саме безпосереднє відношення математична логіка, ні перше, ні друге без математичної логіки обійтися не можуть.
Математична логіка та розвиток інформатики У свою чергу, інформатика як наука почала формуватися разом з створенням і бурхливим розвитком обчислювальної техніки. Її формування і визначення її предмета тривають по теперішній час. Інформатика — наука про зберігання, обробки і передачі інформації за допомогою комп'ютерів. Вона включає в себе великі розділи, які вивчають алгоритмічні, програмні та технічні засоби зберігання, обробки і передачі інформації. Математична логіка виявилася єдиною математичною наукою, методи якої стали найпотужнішими інструментами пізнання у всіх розділах інформатики. Тому скільки- серйозне вивчення інформатики немислимо без освоєння основ математичної логіки.
Щоб комп'ютер працював, він повинен бути оснащений програмним забезпеченням, тобто комплексом програм, що орієнтують комп'ютер на вирішення завдань того чи іншого класу. Слово «програма» має грецьке походження і означає "оголошення ", « розпорядження» . Уже саме поняття комп'ютерної програми, що передбачає чіткий алгоритмічний припис комп'ютера про порядок і характер дій, передбачає проникнення в програму, а також у процес її складання (в програмування) теорії алгоритмів . Але при більш пильному розгляді процес проникнення логіки в програми і програмування виявляється значно більш глибоким і органічним. Не тільки один розділ теорії алгоритмів працює тут, але виключно дієвим виявляється саме істота математичної логіки — її мову, її аксіоматичні теорії, висновки і теореми в них, властивості цих теорій.
Фундаментальна основа програмування Теорія алгоритмів та математична логіка — фундаментальна основа програмування. У 30 -і рр. XIX ст. англійський математик Чарлз Беббедж висловив вперше ідею обчислювальної машини. І тільки сто років по тому логіки розробили чотири математично еквівалентні моделі поняття алгоритму. Саме в теорії алгоритмів були передбачені основні концепції, які лягли в основу принципів побудови і функціонування обчислювальної машини з програмним керуванням і принципів створення мов програмування. Ідею такої обчислювальної машини вперше змогли реалізувати болгарський учений С. Атанасов в 1940 р. і німецький вчений К. Цузе в 1942 р. Чотири головні моделі алгоритму породили різні напрямки в програмуванні.
Моделі поняття алгоритму Перша модель — це абстрактна обчислювальна машина (А. Тьюринг, Р. Пост). Вона з'явилася абстрактним прообразом реальних обчислювальних машин. До цих пір всі обчислювальні машини в деякому сенсі базуються на ідеї Тьюринга: їх пам'ять фізично складається з бітів, кожен з яких містить або 0, або 1 . Програмне управління успадкувало від цих абстрактних машин і програму, вміщену в «постійну пам'ять» (ідея помістити програму ЕОМ в основну пам'ять, щоб мати можливість змінювати її в ході обчислень, належить Джону фон Нейманом), а структура команди сучасної ЕОМ в значній мірі нагадує структуру команди машини Тьюринга. У рамках теорії машин Тьюринга откристаллизовался найважливіші для комп'ютерних додатків логіки поняття: обчислювана функція, здійсненне завдання, нерозв'язна (алгоритмічно) задача. Зібрано велику кількість визначень абстрактних обчислювальних машин і показано, як кожне з них можна звести до іншого підходящої кодуванням входів і виходів.
Друга модель — це рекурсивні функції, ідея яких сходить до гильбертовськой аксиоматическому підходу. Від них успадкувало свої основні конструкції сучасне структурне програмування.
Третій спосіб опису алгоритмів — нормальні алгоритми А. А. Маркова. Вони послужили основою мови Рефал і багатьох інших мов обробки символьної інформації.
Четвертий напрямок в теорії алгоритмів — так зване λ -числення — базується на ідеях радянського логіка Р.Шейнфінкеля та американського логіка X. Б. Каррі. Виявилося, що для визначення всіх вичіслімих функцій досить операцій так званої λ — абстракції і суперпозиції. Ідеї λ -числення активно розвиваються в мові Лісп, функціональному програмуванні і в багатьох інших перспективних напрямах сучасного програмування.
Математична логіка стала бурхливо розвиватися на початку XX ст. на грунті здавалося б виключно далекій від додатків проблеми обгрунтування математики. Але саме ці дослідження поклали початок строгому визначенню алгоритмічних мов, показали їх колосальні можливості і принципові обмеження, розвинули техніку формалізації. Тому, коли в програмуванні було усвідомлено, що всяка програма є формалізацією, то виникнувші тут математичні проблеми впали на грунт, ретельно підготовлений математичною логікою .
Опис комп'ютерних програм за допомогою математичної логіки Перші спроби застосувати в програмуванні розвинені логічні обчислення і методи формалізації зробив американський логік X. Б. Каррі. У 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 рр. другий голландець А. Гейтинг строго сформулював логіку, якою користувалися в інтуїтивній математиці — інтуїтивну логіку. Її математична інтерпретація, викладена радянським математиком А. М. Колмогоровим зберегла своє значення до цих пір.