Является ли единственная разница между Inductive и CoInductive проверками правильности их использования (в Coq)?

Question

Сформулируем вопрос по-другому: если мы удалим проверку завершения и условие защищенности при использовании индуктивных и коиндуктивных типов данных, соответственно, исчезнет ли фундаментальное различие между индуктивным/коиндуктивным и фиксированным/кофиксным?

Под «фундаментальным отличием» я подразумеваю различие в основном исчислении Coq, а не различия в таких вещах, как синтаксис и поиск доказательств.

Кажется, в конечном итоге это сводится к вопросу об исчислении конструкций.

Примечание. Я знаю средство доказательства теорем, которое может доказать отсутствие проверки завершения/защищенности рекурсии/корекурсии. False– так что, если это поможет, пожалуйста, воспринимайте это как вопрос о неполном программировании, а не о доказательстве.

Answer 1

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

• уменьшается только в том случае, если его убывающий аргумент является конструктором

• уменьшается только под деструктором ( matchили примитивная проекция)

      (* stuck *)
(fix f x {struct x} := body f x)

(* not stuck *)
(fix f x {struct x} := body f x) (S y)
=
body (fix f x := body f x) (S y)


(* stuck *)
(cofix g x := body g x)

(* not stuck *)
match (cofix g x := body g x) with _ => _ end
= match body (cofix g x := body g x) x with _ => _ end

Эти своеобразные правила предназначены для того, чтобы гарантировать завершение. Если тебя это не волнует, и ты позволяешь fixа также cofixразворачиваться в любом контексте, то они ведут себя одинаково как комбинатор с фиксированной точкой:

      (fix f x := body f x)
=
(fun x => body (fix f x := body f x) x)

(cofix g x := body g x)
=
(fun x => body (cofix g x := body g x) x)