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

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

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

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

Історія

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

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

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

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

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

Визначення

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

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

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

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

${\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)}}$.

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

Приклади

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

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

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

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

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

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

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

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

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

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

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

Література

• 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 (2 квітня). — С. 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 с. (рос.)