У этой страницы есть серьезная проблема: она полезна только тем, кто уже очень хорошо понимает концепцию. Если вы не понимаете концепции, она не поможет на пути к пониманию. Функция энциклопедии состоит в том, чтобы выступать в качестве вводного материала для непосвященных, а не в качестве краткого справочника для тех, кто уже знаком с темой. Страница должна быть обогащена более четкими определениями, предназначенными для тех, кто еще не понимает тему, и примерами, чтобы люди могли конкретизировать свое понимание. -- Пметцгер ( разговор ) 15:59, 18 октября 2011 г. (UTC)
Я согласен с Пметцгером . Вот с чем я сталкиваюсь, это может помочь. Проблема для меня начинается во втором предложении, в котором говорится следующее:
Что такое «математический двойник»? "двойственность" приводит меня к совершенно новому, к теории категорий. А затем «структурная индукция» приводит меня к совершенно новой вещи.
«Коиндуктивные методы получают широкое распространение в компьютерных науках. В помощниках по доказательству, таких как Agda, Coq и Matita, кодататипы и коиндукция являются неотъемлемой частью логического исчисления. [...] Кодатипы и корекурсия уже давно отсутствуют функции в помощниках по доказательству, основанных на логика более высокого порядка. Новый (со) пакет определения типов данных Изабель, наконец, устраняет этот недостаток, в то же время обобщая и модульно поддерживая типы данных».
Действительно модульные (Co) типы данных для Isabelle/HOL
http://www21.in.tum.de/~traytel/papers/itp14-codata_impl/codata_impl.pdf
Коиндукция является математическим принципом доказательства. Это категорическая обратная индукция. Статью следует начать с этого, потому что в основном это так же просто, как индукция. Затем приведите простое доказательство по коиндукции. Затем перейдите к последствиям и вариантам использования. — Предыдущий неподписанный комментарий добавлен 141.45.12.231 ( обсуждение ) 23:04, 5 октября 2018 г. (UTC)