Coinduction - ясное, краткое описание

Question

Я изучаю коиндукцию (, а не индукция) как часть класса по статическому анализу. Порывшись в интернете, я просто не нахожу четкого, краткого описания:

• Что такое коиндукция
• Как коиндукция на самом деле что-то доказывает (кажется, что коиндукция похожа на взмах волшебной руки в обработках, которые я читала)
• Какие предложения требуют коиндуктивного доказательства
• Как использовать коиндуктивное доказательство

Answer 1

Мое понимание (которое может быть неправильным) звучит так:

Коиндукция - это способ доказать вещи о бесконечных структурах данных.

Точно так же, как индукция, поначалу это кажется обманом. Главное, что нужно понять, это то, что вместо:

1. доказательство того, что что-то работает для базовых случаев
2. доказательство того, что оно работает для каждого "одного шага", при условии, что оно работает для всех (конечных) случаев
3. затем утверждая, что оно работает для всех (конечных) случаев (это индукция)

вы вместо этого:

1. докажите, исходя из предположения, что он работает для всех не конечных случаев, что он работает для каждого "одного шага"
2. утверждают, что поэтому он работает для всех не конечных случаев (это коиндукция, и это оправдано, поскольку каждый не конечный случай представляет собой (конечную) последовательность одиночных шагов, за которыми следует бесконечная часть, которая работает по гипотезе) 1020 *

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

Эта статья полезна в некоторых отношениях и вводит в заблуждение других (по крайней мере, тех, кто не связан с теорией категорий, среди которых я себя считаю).

Answer 2

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

Answer 3

Coinduction немного легче понять в контексте логического программирования. Я рекомендую следующий учебный документ: «Программирование коиндуктивной логики и его приложения» Гупты и др., Который появился в Proc. Международной конференции по программированию логики 2007. Так же, как рекурсия соответствует индукции (наименьшая семантика с фиксированной точкой), ко-рекурсия соответствует коиндукции (наибольшая семантика с фиксированной точкой). Можно думать о совместной рекурсии как о "рекурсии без базового случая". В отсутствие базового случая критерии завершения должны основываться на распознавании циклов в вычислении (рациональное бесконечное доказательство). Более подробная информация в учебном документе.