Структурна індукція

Використання методу зустрічається принаймні від 1950-х років, зокрема, в доведенні теореми Лоша про ультрадобутки застосовується індукція побудови формули, при цьому сам метод особливим чином явно не називався[3]. У ті ж роки метод застосовувався в теорії моделей для доведень над ланцюгами моделей, вважається, що поява терміна «структурна індукція» пов'язана саме з цими доведеннями[4]. Карі поділив усі види застосування індукції в математиці на два типи — дедуктивну індукцію і структурну індукцію, класичну індукцію над натуральними числами вважаючи підтипом останньої[5].

З іншого боку, не пізніше початку 1950-х років метод трансфінітної індукції вже поширювався на довільні частково впорядковані множини, що задовольняють умову обриву ростучих ланцюгів (що еквівалентно фундованості[6]), в той же час Генкін відсилав до можливості індукції «в деяких типах частково впорядкованих систем»[7]. У 1960-х роках метод закріпився під назвою нетерівська індукція (за аналогією з нетерівським кільцем, у якому виконано умову обриву ростучих ланцюгів ідеалів)[8].

Явне визначення структурної індукції, яке посилається як на рекурсивну ви́значність, так і на нетерівську індукцію, дав Берстолл) наприкінці 1960-х років[9], і в літературі з інформатики саме до нього відносять уведення методу[10][11].

Надалі в інформатиці утворилося декілька напрямів, які ґрунтуються на структурній індукції як базовому принципі, зокрема, такими є структурна операційна семантика мов програмування Плоткіна)[12], серія індуктивних методів формальної верифікації[13][14], структурно-рекурсивна мова запитів UnQL[15]. У 1990-х роках у теоретичній інформатиці поширився метод коіндукції, застосовуваний над нефундованих (як правило, нескінченних) структурах, який вважають дуальним для структурної індукції[16].

Через широке застосування в теоретичній інформатиці і нечисленність згадок у математичній літературі, станом на 2010-ті роки вважається, що виділення структурної індукції як особливого методу більшою мірою характерне для інформатики, ніж для математики[4].

Найзагальніше визначення[17][18] вводиться для класу структур ${\displaystyle {\mathfrak {S}}}$ (без уточнення природи структур ${\displaystyle S\in {\mathfrak {S}}}$) з відношенням часткового порядку між структурами ${\displaystyle \sqsubseteq }$, з умовою мінімального елемента ${\displaystyle S_{0}}$ в ${\displaystyle {\mathfrak {S}}}$ і умовою наявності для кожної ${\displaystyle S\in {\mathfrak {S}}}$ цілком упорядкованої сукупності зі всіх структур, що суворо передують їй: ${\displaystyle \triangledown S=\{T\in {\mathfrak {S}}\mid T\sqsubset S\}}$. Принцип структурної індукції в цьому випадку формулюється так: якщо виконання властивості ${\displaystyle P}$ для ${\displaystyle {\mathfrak {S}}}$ випливає з виконання властивості для всіх структур, що суворо передують їй, то властивість виконано і для всіх структур класу; символічно (в позначеннях систем натурального виведення):

${\displaystyle {\frac {\forall T\in \triangledown S:P(T)\Rightarrow P(S)}{\forall S\in {\mathfrak {S}}:P(S)}}}$.

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

В літературі з інформатики поширена й інша форма визначення структурної індукції, орієнтована на рекурсію за побудовою[19], в ній ${\displaystyle {\mathfrak {S}}}$ розглядається як клас об'єктів, визначених над деякою множиною атомарних елементів ${\displaystyle {\mathcal {A}}\in {\mathfrak {S}}}$ і набором операцій ${\displaystyle \left\{{\mathcal {o}}_{i}:{\mathfrak {S}}^{k_{i}}\to {\mathfrak {S}}\right\}}$, при цьому кожен об'єкт ${\displaystyle S\in {\mathfrak {S}}}$ — результат послідовного застосування операцій до атомарних елементів. У цьому формулюванні принцип стверджує, що властивість ${\displaystyle P}$ виконується для всіх об'єктів ${\displaystyle S\in {\mathfrak {S}}}$, як тільки має місце для всіх атомарних елементів і для кожної операції ${\displaystyle {\mathcal {o}}_{i}}$ з виконання властивості для елементів ${\displaystyle S_{1},\dots ,S_{i_{k}}}$ слідує виконання властивості для ${\displaystyle {\mathcal {o}}_{i}(S_{1},\dots ,S_{i_{k}})}$:

${\displaystyle {\frac {\forall A\in {\mathcal {A}}:P(A),\,\forall i:(P(S_{1}),\dots P(S_{i_{k}}\Rightarrow P({\mathcal {o}}_{i}(S_{1},\dots ,S_{i_{k}}))}{\forall S\in {\mathfrak {S}}:P(S)}}}$.

Роль відношення часткового порядку ${\displaystyle \sqsubseteq }$ з загального визначення тут грає відношення включення за побудовою: ${\displaystyle \forall _{j=1\dots i_{k}}S_{j}\sqsubseteq {\mathcal {o}}_{i}(S_{1},\dots ,S_{i_{k}})}$[20].

Запровадження принципу в інформатику мотивувалося рекурсивним характером таких структур даних, як списки і дерева[21]. Перший приклад над списком, наведений Берстоллом — твердження про властивості згортки списків ${\displaystyle \circledast }$ з елементами типу ${\displaystyle T}$ двомісною функцією ${\displaystyle \ast :T^{2}\to T}$ і початковим елементом згортки ${\displaystyle t\in T}$ у зв'язку з конкатенацією списків ${\displaystyle \shortparallel }$:

${\displaystyle (S_{1}\shortparallel S_{2})\circledast t=S_{1}\circledast (S_{2}\circledast t)}$.

Структурна індукція в доведенні цього твердження ведеться від порожніх списків — якщо ${\displaystyle S_{1}=\bot }$, то:

ліва частина, за визначенням конкатенації: ${\displaystyle (\bot \shortparallel S_{2})\circledast t=S_{2}\circledast t}$,

права частина, за визначенням згортки: ${\displaystyle \bot \circledast (S_{2}\circledast t)=S_{2}\circledast t}$

і в разі, якщо список непорожній, і починається елементом ${\displaystyle x}$, то:

ліва частина, за визначенням конкатенації та згортки: ${\displaystyle ((x::S_{1})\shortparallel S_{2})\circledast t=x\ast ((S_{1}\shortparallel S_{2})\circledast t)}$,

права частина, за визначенням згортки і припущенням індукції: ${\displaystyle (x::S_{1})\circledast (S_{2}\circledast t)=x\ast ((S_{1}\shortparallel S_{2})\circledast t)}$.

Припущення індукції ґрунтується на істинності твердження ${\displaystyle S_{1}}$ і включення ${\displaystyle S_{1}\sqsubseteq x::S_{1}}$.

В теорії графів структурна індукція часто застосовується для доведення тверджень про багатодольні графи (з використанням переходу від ${\displaystyle (k-1)}$-дольних до ${\displaystyle k}$-дольних), у теоремах про амальгамування графів, властивостей дерев і лісів[22]. Інші структури в математиці, для яких застосовується структурна індукція — перестановки, матриці і їх тензорні добутки, конструкції з геометричних фігур у комбінаторній геометрії.

Типове застосування в математичній логіці та універсальній алгебрі — структурна індукція побудови формул з атомарних термів, наприклад, показується, що виконання необхідної властивості ${\displaystyle P}$ для термів ${\displaystyle A}$ і ${\displaystyle B}$ тягне ${\displaystyle P(A\vee B)}$, ${\displaystyle P(A\wedge B)}$, ${\displaystyle P(\lnot A)}$ і так далі. Також за побудовою формул виконуються багато структурно-індуктивних доведень у теорії автоматів, математичній лінгвістиці; для доведення синтаксичної коректності комп'ютерних програм широко використовується структурна індукція за БНФ-визначенням мови (іноді навіть виділяється в окремий підтип — БНФ-індукція[23]).

• B. Steffen, O. Rüthing, M. Huth. Mathematical Foundations of Advanced Informatics. — Springer, 2018. — Т. 1. Inductive Approaches. — ISBN 978-3-319-68396-6.
• R. M. Burstall. Proving properties of programs by structural induction // The Computer Journal. — 1969. — Т. 12, № 1 (3 листопада). — С. 41–48. — DOI:10.1093/comjnl/12.1.41.
• D. Gunderson. Handbook of Mathematical Induction. Theory and Applications. — Boca Raton : CRC, 2011. — 893 с. — ISBN 978-1-4200-9364-3.
• Х. Карри. Основания математической логики. — М. : Мир, 1969. — 567 с. (рос.)