Структу́рна інду́кція — конструктивний метод математичного доведення, який узагальнює математичну індукцію (застосовувану над натуральним рядом) на довільні рекурсивно означені частково впорядковані сукупності. Структурна рекурсія — реалізація структурної індукції у формі визначення, процедури доведення або програми, що забезпечує індукційний перехід над частково впорядкованою сукупністю.
Спочатку метод використовувався в математичній логіці, також знайшов застосування в теорії графів, комбінаториці, загальній алгебрі, математичній лінгвістиці, але найбільшого поширення як самостійно досліджуваний метод набув у теоретичній інформатиці, де застосовується в питаннях семантики мов програмування, формальної верифікації, обчислювальної складності, функційного програмування.
На відміну від нетерівської індукції — найзагальнішої форми математичної індукції, застосовуваної над довільними фундованими множинами, — в понятті про структурну індукцію мається на увазі конструктивний характер, обчислювальна реалізація. При цьому фундованість сукупності — властивість, необхідна для рекурсивної ви́значності, таким чином, структурну рекурсію можна вважати частковим варіантом нетерівської індукції.
Історія Використання методу зустрічається принаймні від 1950-х років, зокрема, в доведенні теореми Лоша про ультрадобутки застосовується індукція побудови формули, при цьому сам метод особливим чином явно не називався. У ті ж роки метод застосовувався в теорії моделей для доведень над ланцюгами моделей, вважається, що поява терміна «структурна індукція» пов'язана саме з цими доведеннями. Карі поділив усі види застосування індукції в математиці на два типи — дедуктивну індукцію і структурну індукцію, класичну індукцію над натуральними числами вважаючи підтипом останньої.
З іншого боку, не пізніше початку 1950-х років метод трансфінітної індукції вже поширювався на довільні частково впорядковані множини, що задовольняють умову обриву ростучих ланцюгів (що еквівалентно фундованості), в той же час відсилав до можливості індукції «в деяких типах частково впорядкованих систем». У 1960-х роках метод закріпився під назвою нетерівська індукція (за аналогією з нетерівським кільцем, у якому виконано умову обриву ростучих ланцюгів ідеалів) .
Явне визначення структурної індукції, яке посилається як на рекурсивну ви́значність, так і на нетерівську індукцію, дав ) наприкінці 1960-х років, і в літературі з інформатики саме до нього відносять уведення методу.
Надалі в інформатиці утворилося декілька напрямів, які ґрунтуються на структурній індукції як базовому принципі, зокрема, такими є структурна операційна семантика мов програмування ), серія індуктивних методів формальної верифікації, структурно-рекурсивна мова запитів UnQL. У 1990-х роках у теоретичній інформатиці поширився метод коіндукції, застосовуваний над нефундованих (як правило, нескінченних) структурах, який вважають дуальним для структурної індукції.
Через широке застосування в теоретичній інформатиці і нечисленність згадок у математичній літературі, станом на 2010-ті роки вважається, що виділення структурної індукції як особливого методу більшою мірою характерне для інформатики, ніж для математики.
Визначення Найзагальніше визначення вводиться для класу структур (без уточнення природи структур ) з відношенням часткового порядку між структурами , з умовою мінімального елемента в і умовою наявності для кожної цілком упорядкованої сукупності зі всіх структур, що суворо передують їй: . Принцип структурної індукції в цьому випадку формулюється так: якщо виконання властивості для випливає з виконання властивості для всіх структур, що суворо передують їй, то властивість виконано і для всіх структур класу; символічно (в позначеннях ):
.
Рекурсивність у цьому визначенні реалізується сукупністю вкладених структур: як тільки є спосіб виводити властивості структури виходячи зі властивостей усіх попередніх їй, можна говорити про рекурсивну визначність структури.
В літературі з інформатики поширена й інша форма визначення структурної індукції, орієнтована на рекурсію за побудовою, в ній розглядається як клас об'єктів, визначених над деякою множиною атомарних елементів і набором операцій , при цьому кожен об'єкт — результат послідовного застосування операцій до атомарних елементів. У цьому формулюванні принцип стверджує, що властивість виконується для всіх об'єктів , як тільки має місце для всіх атомарних елементів і для кожної операції з виконання властивості для елементів слідує виконання властивості для :
.
Роль відношення часткового порядку з загального визначення тут грає відношення включення за побудовою: .
Приклади Запровадження принципу в інформатику мотивувалося рекурсивним характером таких структур даних, як списки і дерева. Перший приклад над списком, наведений Берстоллом — твердження про властивості згортки списків з елементами типу двомісною функцією і початковим елементом згортки у зв'язку з конкатенацією списків :
.
Структурна індукція в доведенні цього твердження ведеться від порожніх списків — якщо , то:
ліва частина, за визначенням конкатенації: , права частина, за визначенням згортки:
і в разі, якщо список непорожній, і починається елементом , то:
ліва частина, за визначенням конкатенації та згортки: , права частина, за визначенням згортки і припущенням індукції: .
Припущення індукції ґрунтується на істинності твердження і включення .
В теорії графів структурна індукція часто застосовується для доведення тверджень про багатодольні графи (з використанням переходу від -дольних до -дольних), у теоремах про , властивостей дерев і лісів. Інші структури в математиці, для яких застосовується структурна індукція — перестановки, матриці і їх тензорні добутки, конструкції з геометричних фігур у комбінаторній геометрії.
Типове застосування в математичній логіці та універсальній алгебрі — структурна індукція побудови формул з атомарних термів, наприклад, показується, що виконання необхідної властивості для термів і тягне , , і так далі. Також за побудовою формул виконуються багато структурно-індуктивних доведень у теорії автоматів, математичній лінгвістиці; для доведення синтаксичної коректності комп'ютерних програм широко використовується структурна індукція за БНФ-визначенням мови (іноді навіть виділяється в окремий підтип — БНФ-індукція).
Примітки
Література