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

Эта статья находится на начальном уровне проработки, в одной из её версий выборочно используется текст из источника, распространяемого под свободной лицензией
Материал из энциклопедии Руниверсалис

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

Изначально[⇨] метод использовался в математической логике, также нашёл применение[⇨] в теории графов, комбинаторике, общей алгебре, математической лингвистике, но наибольшее распространение как самостоятельно изучаемый метод получил в теоретической информатике[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] вводится для класса структур [math]\displaystyle{ \mathfrak S }[/math] (без уточнения природы структур [math]\displaystyle{ S \in \mathfrak S }[/math]) с отношением частичного порядка между структурами [math]\displaystyle{ \sqsubseteq }[/math], с условием минимального элемента [math]\displaystyle{ S_0 }[/math] в [math]\displaystyle{ \mathfrak S }[/math] и условием наличия для каждой [math]\displaystyle{ S \in \mathfrak S }[/math] вполне упорядоченной совокупности из всех строго предшествующих ей структур: [math]\displaystyle{ \triangledown S = \{ T \in \mathfrak S \mid T \sqsubset S \} }[/math]. Принцип структурной индукции в этом случае формулируется следующим образом: если выполнение свойства [math]\displaystyle{ P }[/math] для [math]\displaystyle{ \mathfrak S }[/math] следует из выполнения свойства для всех строго предшествующих ей структур, то свойство выполнено и для всех структур класса; символически (в обозначениях систем натурального вывода):

[math]\displaystyle{ \frac {\forall T \in \triangledown S : P(T) \Rightarrow P(S)} {\forall S \in \mathfrak S : P(S)} }[/math].

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

В литературе по информатике распространена и другая форма определения структурной индукции, ориентированная на рекурсию по построению[20], в ней [math]\displaystyle{ \mathfrak S }[/math] рассматривается как класс объектов, определённых над некоторым множеством атомарных элементов [math]\displaystyle{ \mathcal {A} \in \mathfrak S }[/math] и набором операций [math]\displaystyle{ \left \{ \mathcal o_i : \mathfrak S^{k_i} \to \mathfrak S \right \} }[/math], при этом каждый объект [math]\displaystyle{ S \in \mathfrak S }[/math] — результат последовательного применения операций к атомарным элементам. В этой формулировке принцип утверждает, что свойство [math]\displaystyle{ P }[/math] выполняется для всех объектов [math]\displaystyle{ S \in \mathfrak S }[/math], как только имеет место для всех атомарных элементов и для каждой операции [math]\displaystyle{ \mathcal o_i }[/math] из выполнения свойства для элементов [math]\displaystyle{ S_1, \dots, S_{i_k} }[/math] следует выполнение свойства для [math]\displaystyle{ \mathcal o_i (S_1, \dots, S_{i_k}) }[/math]:

[math]\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)} }[/math].

Роль отношения частичного порядка [math]\displaystyle{ \sqsubseteq }[/math] из общего определения здесь играет отношение включения по построению: [math]\displaystyle{ \forall_{j = 1\dots i_k} S_j \sqsubseteq \mathcal o_i (S_1, \dots, S_{i_k}) }[/math][21].

Примеры

Введение принципа в информатику мотивировалось рекурсивным характером таких структур данных, как списки и деревья[22]. Первый пример над списком, приводимый Бёрстоллом — утверждение о свойствах свёртки списков [math]\displaystyle{ \circledast }[/math] с элементами типа [math]\displaystyle{ T }[/math] двухместной функцией [math]\displaystyle{ \ast : T^2 \to T }[/math] и начальным элементом свёртки [math]\displaystyle{ t \in T }[/math] в связи с конкатенацией списков [math]\displaystyle{ \shortparallel }[/math]:

[math]\displaystyle{ (S_1 \shortparallel S_2) \circledast t = S_1 \circledast (S_2 \circledast t) }[/math].

Структурная индукция в доказательстве этого утверждения ведётся от пустых списков — если [math]\displaystyle{ S_1 = \bot }[/math], то:

левая часть, по определению конкатенации: [math]\displaystyle{ (\bot \shortparallel S_2) \circledast t = S_2 \circledast t }[/math],
правая часть, по определению свёртки: [math]\displaystyle{ \bot \circledast (S_2 \circledast t) = S_2 \circledast t }[/math]

и в случае, если список непуст, и начинается элементом [math]\displaystyle{ x }[/math], то:

левая часть, по определениям конкатенации и свёртки: [math]\displaystyle{ ((x::S_1) \shortparallel S_2) \circledast t = x \ast ((S_1 \shortparallel S_2) \circledast t) }[/math],
правая часть, по определению свёртки и предположению индукции: [math]\displaystyle{ (x::S_1) \circledast (S_2 \circledast t) = x \ast ((S_1 \shortparallel S_2) \circledast t) }[/math].

Предположение индукции основывается на истинности утверждения для [math]\displaystyle{ S_1 }[/math] и включении [math]\displaystyle{ S_1 \sqsubseteq x::S_1 }[/math].

В теории графов структурная индукция часто применяется для доказательств утверждений о многодольных графах (с использованием перехода от [math]\displaystyle{ (k-1) }[/math]-дольных к [math]\displaystyle{ k }[/math]-дольным), в теоремах об амальгамировании графов[англ.], свойств деревьев и лесов[23]. Другие структуры в математике, для которых применяется структурная индукция — перестановки, матрицы и их тензорные произведения, конструкции из геометрических фигур в комбинаторной геометрии.

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

Примечания

  1. ↑ 1,0 1,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 с.
Источник — https://xn--h1ajim.xn--p1ai/index.php?title=Структурная_индукция&oldid=5821376