Я слышал о (структурной) индукции. Это позволяет вам строить конечные структуры из более мелких и дает вам доказательные принципы для рассуждений о таких структурах. Идея достаточно ясна.
Но как насчет коиндукции? Как это работает? Как можно сказать что-либо убедительное о бесконечной структуре?
Есть (по крайней мере) два угла для рассмотрения, а именно, коиндукция как способ определения вещей и как метод доказательства.
Что касается коиндукции как метода доказательства, какова связь между коиндукцией и бисимуляцией?
Ответы:
Во-первых, чтобы развеять возможный когнитивный диссонанс: рассуждения о бесконечных структурах не проблема, мы делаем это постоянно. Пока структура конечно описываема, это не проблема. Вот несколько распространенных типов бесконечных структур:
Коиндуктивность как самая большая точка фиксации
Там, где индуктивные определения строят структуру из элементарных строительных блоков, коиндуктивные определения формируют структуры из того, как их можно деконструировать. Например, тип списков, элементы которых находятся в наборе
A
, определяется в Coq следующим образом:Неформально∀ хY,n i l ≠ c o n sИксY
list
типа является самым маленьким типом , который содержит все значения , построенные изnil
иcons
конструкторов, с аксиомой , что . И наоборот, мы можем определить самый большой тип, который содержит все значения, построенные из этих конструкторов, сохраняя аксиому дискриминации:list
изоморфна подмножествуcolist
. Кроме того,colist
содержит бесконечные списки: списки сcocons
поcocons
.flipflop
является бесконечным (циклический список) ; это бесконечный список натуральных чисел 0 : : 1 : : 2 : : ... .from 0
Рекурсивное определение правильно сформировано, если результат построен из меньших блоков: рекурсивные вызовы должны работать на меньших входах. Определение Corecursive будет правильно сформировано, если в результате будут построены более крупные объекты. Индукция смотрит на конструкторов, коиндукция смотрит на деструкторов. Обратите внимание, что дуальность не только меняется с меньшего размера на больший, но и вводится в выходные данные. Например, причина, по которой вышеприведенные определения
flipflop
иfrom
определения являются правильными, заключается в том, что вызов corecursive защищен вызовомcocons
конструктора в обоих случаях.Там, где утверждения об индуктивных объектах имеют индуктивные доказательства, утверждения о коиндуктивных объектах имеют коиндуктивные доказательства. Например, давайте определим бесконечный предикат для колистов; Интуитивно, бесконечные колисты - это те, которые не заканчиваются
conil
.Чтобы доказать, что колисты формы
from n
бесконечны, мы можем рассуждать путем коиндукции.from n
равноcocons n (from (1 + n))
. Это показывает, чтоfrom n
больше, чемfrom (1 + n)
, что является бесконечным по гипотезе коиндукции, следовательноfrom n
, бесконечно.Схожесть, коиндуктивное свойство
Коиндукция как метод доказательства также применима к конечным объектам. Интуитивно говоря, индуктивные доказательства об объекте основаны на том, как объект построен. Коиндуктивные доказательства основаны на том, как объект может быть разложен.
При изучении детерминированных систем обычно определяют эквивалентность через индуктивные правила: две системы эквивалентны, если вы можете перейти от одной к другой с помощью серии преобразований. Такие определения, как правило, не в состоянии охватить множество различных способов, которыми недетерминированные системы могут в конечном итоге иметь одинаковое (наблюдаемое) поведение, несмотря на разную внутреннюю структуру. (Коиндукция также полезна для описания бесконечных систем, даже когда они детерминированные, но здесь я не остановлюсь на этом.)
Недетерминированные системы, такие как параллельные системы, часто моделируются помеченными переходными системами . LTS - это ориентированный граф, в котором ребра помечены. Каждое ребро представляет собой возможный переход системы. След LTS - это последовательность меток ребер на пути в графе.
Сходство является коиндуктивным свойством. Его можно определить как наибольшую точку фиксации оператора: это наибольшее отношение, которое при расширении для идентификации эквивалентных состояний остается неизменным.
Рекомендации
Coq и исчисление индуктивных конструкций
Помеченные переходные системы и бисимуляции
Давиде Сангиорги. Пи-исчисление: теория мобильных процессов . Издательство Кембриджского университета, 2003. [ Амазонка ]
Глава в Заверенной программировании с зависимыми типами А. Chlipala
источник
Рассмотрим следующее индуктивное определение:
Обозначения:
источник
We can not turn the anchor around, so it goes away
.