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

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

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

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

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

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

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

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