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

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

Изначально➤ метод использовался в математической логике, также нашёл применение➤ в теории графов, комбинаторике, общей алгебре, математической лингвистике, но наибольшее распространение как самостоятельно изучаемый метод получил в теоретической информатике[1], где применяется в вопросах семантики языков программирования, формальной верификации, вычислительной сложности, функционального программирования.

В отличие от нётеровой индукции — наиболее общей формы математической индукции, применяемой над произвольными фундированными множествами, — в понятии о структурной индукции подразумевается конструктивный характер, вычислительная реализация. При этом фундированность совокупности — свойство, необходимое для рекурсивной определяемости[2], таким образом, структурную рекурсию можно считать частным вариантом нётеровой индукции[1].

История

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

С другой стороны, не позднее начала 1950-х годов метод трансфинитной индукции уже распространялся на произвольные частично упорядоченные множества, удовлетворяющие условию обрыва возрастающих цепей (что эквивалентно фундированности[6]), в то же время Генкин отсылал к возможности индукции «в некоторых типах частично-упорядоченных систем»[7]. В 1960-е годы метод закрепился под наименованием нётеровой индукции (по аналогии с нётеровым кольцом, в котором выполнено условие обрыва возрастающих цепей идеалов)[8].

Явное определение структурной индукции, ссылающееся как на рекурсивную определимость, так и на нётерову индукцию, дано Бёрстоллом (англ. Rod Burstall) в конце 1960-х годов[9], и в литературе по информатике именно к нему относят введение метода[10][11].

В дальнейшем в информатике возникло несколько направлений, основывающихся на структурной индукции как базовом принципе, в частности, таковы структурная операционная семантика языков программирования Плоткина (англ. Gordon Plotkin)[12], серия индуктивных методов формальной верификации[13][14], структурно-рекурсивный язык запросов UnQL[15]. В 1990-е годы в теоретической информатике получил распространение метод коиндукции, применяемый над нефундированными (как правило, бесконечными) структурами и считающийся двойственным структурной индукции[16].

В связи с широким применением в теоретической информатике и немногочисленностью упоминаний в математической литературе, по состоянию на 2010-е годы считается, что выделение структурной индукции как особого метода в большей степени характерно для информатики, нежели для математики[17].

Определение

Наиболее общее определение[18][19] вводится для класса структур ${\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)}}}$.

Рекурсивность в этом определении реализуется совокупностью вложенных структур: как только есть способ определять выводить свойства структуры исходя из свойств всех предшествующих ей, можно говорить о рекурсивной определимости структуры.

В литературе по информатике распространена и другая форма определения структурной индукции, ориентированная на рекурсию по построению[20], в ней ${\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}})}$[21].

Примеры

Введение принципа в информатику мотивировалось рекурсивным характером таких структур данных, как списки и деревья[22]. Первый пример над списком, приводимый Бёрстоллом — утверждение о свойствах свёртки списков ${\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}$-дольным), в теоремах об амальгамировании графов^[англ.], свойств деревьев и лесов[23]. Другие структуры в математике, для которых применяется структурная индукция — перестановки, матрицы и их тензорные произведения, конструкции из геометрических фигур в комбинаторной геометрии.

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

Примечания

1. Штеффен, Рютинг, Хут, 2018, p. 179.
2. Рекурсия — статья из Математической энциклопедии. Н. В. Белякин
3. J. Loś^[пол.]. Quelques remarques, théorèmes et problèmes sur les classes définissables d'algèbres // Studies in Logic and the Foundations of Mathematics. — 1955. — Vol. 16. — P. 98—113. — doi:10.1016/S0049-237X(09)70306-4.
4. Гундерсон, 2011, p. 48.
5. Карри, 1969, при этом указывая: «Обычная математическая индукция с настоящей точки зрения является структурной индукцией по системе самов; она так часто встречается <…> что стоит считать её третьим видом — натуральной индукцией».
6. А. Г. Курош. Лекции по общей алгебре. — М.: Физматлит, 1962. — С. 21—22 (§5. Условие минимальности). — 399 с.
7. Л. Генкин. О математической индукции. — М.: Физматгиз, 1962. — С. 36 (заключение). — 36 с.
8. П. Кон. Универсальная алгебра. — М.: Мир, 1969. — С. 33—34. — 351 с.
9. Бёрстолл, 1969.
10. Tools and Notions for Program Construction. An Advanced Course / D. Néel (ed.). — Cambridge University Press, 1982. — С. 196. — 400 с. — ISBN 0-512-24801-9.
11. О. А. Ильичёва. Формальное описание семантики языков программирования. — Ростов-на-Дону: ЮФУ, 2007. — С. 99—100. — 223 с.
12. G. Plotkin. The origins of structural operational semantics // The Journal of Logic and Algebraic Programming. — 2004. — P. 3—15. — doi:10.1016/j.jlap.2004.03.009.
13. Z. Manna, S. Ness, J. Vuillemin. Inductive methods for proving properties of programs // Communications of the ACM. — 1973. — Vol. 16, № 8. — P. 491—502. — doi:10.1145/355609.362336.
14. C. Reynolds, R. Yeh. Induction as the basis for program verification // Proceedings of the 2nd international conference on Software engineering (ICSE ’76). — Los Alamitos: IEEE Computer Society Press, 1976. — С. 389.
15. P. Buneman, M. Fernandez, D. Suciu. UnQL: a query language and algebra for semistructured data based on structural recursion // The VLDB Journal. — 2000. — Vol. 9, № 1. — P. 76—110. — doi:10.1007/s007780050084.
16. R. Milner, M. Tofte. Co-induction in relational semantics // Theoretical Computer Science. — Vol. 87, № 1. — P. 209—220.
17. Гундерсон, 2011, p. 48: «In the rest of mathematics, the term “structural induction” is rarely used outside of computer science applications — as a friend once said, “it’s all just induction”».
18. Бёрстолл, 1969, p. 42.
19. Гундерсон, 2011, p. 42.
20. Штеффен, Рютинг, Хут, 2018, pp. 177—178.
21. Штеффен, Рютинг, Хут, 2018, pp. 178.
22. Бёрстолл, 1969, p. 43, 45.
23. Гундерсон, 2011, p. 49, 257, 384, 245.
24. Штеффен, Рютинг, Хут, 2018, p. 214.

Литература

• B. Steffen, O. Rüthing, M. Huth. Mathematical Foundations of Advanced Informatics. — Springer, 2018. — Vol. 1. Inductive Approaches. — ISBN 978-3-319-68396-6.
• R. M. Burstall. Proving properties of programs by structural induction // The Computer Journal^[англ.]. — 1969. — Vol. 12, № 1. — P. 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 с.