Interested Article - Структурная индукция

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

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

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

История

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

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

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

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

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

Определение

Наиболее общее определение вводится для класса структур (без уточнения природы структур ) с отношением частичного порядка между структурами , с условием минимального элемента в Невозможно разобрать выражение (SVG (MathML можно включить с помощью плагина для браузера): Недопустимый ответ («Math extension cannot connect to Restbase.») от сервера «http://localhost:6011/ru.wikipedia.org/v1/»:): {\displaystyle \mathfrak S} и условием наличия для каждой вполне упорядоченной совокупности из всех строго предшествующих ей структур: . Принцип структурной индукции в этом случае формулируется следующим образом: если выполнение свойства для следует из выполнения свойства для всех строго предшествующих ей структур, то свойство выполнено и для всех структур класса; символически (в обозначениях систем натурального вывода ):

.

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

В литературе по информатике распространена и другая форма определения структурной индукции, ориентированная на рекурсию по построению , в ней рассматривается как класс объектов, определённых над некоторым множеством атомарных элементов и набором операций , при этом каждый объект — результат последовательного применения операций к атомарным элементам. В этой формулировке принцип утверждает, что свойство выполняется для всех объектов , как только имеет место для всех атомарных элементов и для каждой операции из выполнения свойства для элементов следует выполнение свойства для :

.

Роль отношения частичного порядка из общего определения здесь играет отношение включения по построению: .

Примеры

Введение принципа в информатику мотивировалось рекурсивным характером таких структур данных, как списки и деревья . Первый пример над списком, приводимый Бёрстоллом — утверждение о свойствах свёртки списков с элементами типа двухместной функцией и начальным элементом свёртки в связи с конкатенацией списков :

.

Структурная индукция в доказательстве этого утверждения ведётся от пустых списков — если , то:

левая часть, по определению конкатенации: ,
правая часть, по определению свёртки:

и в случае, если список непуст, и начинается элементом , то:

левая часть, по определениям конкатенации и свёртки: ,
правая часть, по определению свёртки и предположению индукции: .

Предположение индукции основывается на истинности утверждения для и включении .

В теории графов структурная индукция часто применяется для доказательств утверждений о многодольных графах (с использованием перехода от -дольных к -дольным), в теоремах об , свойств деревьев и лесов . Другие структуры в математике, для которых применяется структурная индукция — перестановки , матрицы и их тензорные произведения , конструкции из геометрических фигур в комбинаторной геометрии .

Типичное применение в математической логике и универсальной алгебре — структурная индукция по построению формул из атомарных термов, например, показывается, что выполнение требуемого свойства для термов и влечёт , , и так далее. Также по построению формул работают многие структурно-индуктивные доказательства в теории автоматов , математической лингвистике; для доказательства синтаксической корректности компьютерных программ широко используется структурная индукция по БНФ-определению языка (иногда даже выделяется в отдельный подтип — БНФ-индукция ).

Примечания

  1. , p. 179.
  2. Рекурсия — статья из Математической энциклопедии . Н. В. Белякин
  3. . 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 : .
  4. , p. 48.
  5. , при этом указывая: «Обычная математическая индукция с настоящей точки зрения является структурной индукцией по системе самов; она так часто встречается <…> что стоит считать её третьим видом — натуральной индукцией».
  6. А. Г. Курош . Лекции по общей алгебре. — М. : Физматлит, 1962. — С. 21—22 (§5. Условие минимальности). — 399 с.
  7. Л. Генкин. О математической индукции. — М. : Физматгиз , 1962. — С. 36 (заключение). — 36 с.
  8. П. Кон . Универсальная алгебра. — М. : Мир , 1969. — С. 33—34. — 351 с.
  9. .
  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 : .
  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 : .
  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 : .
  16. R. Milner , M. Tofte. Co-induction in relational semantics // . — Vol. 87, № 1 . — P. 209—220.
  17. , 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. , p. 42.
  19. , p. 42.
  20. , pp. 177—178.
  21. , pp. 178.
  22. , p. 43, 45.
  23. , p. 49, 257, 384, 245.
  24. , 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 // . — 1969. — Vol. 12, № 1 . — P. 41–48. — doi : .
  • D. Gunderson. Handbook of Mathematical Induction. Theory and Applications. — Boca Raton: CRC, 2011. — 893 с. — ISBN 978-1-4200-9364-3 .
  • Х. Карри . Основания математической логики. — М. : Мир, 1969. — 567 с.
Источник —

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