Не прекращающиеся индуктивные предикаты

Question

В отличном программировании и испытаниях в Изабель /HOL говорится

[...] в отличие от рекурсивных функций, для индуктивных определений нет требования завершения. (pdf стр. 40)

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

Answer 1

1. Нет. Для этого вам нужны коиндуктивные предикаты.
2. Не существует
3. Если вы посмотрите на принцип индукции, вы обнаружите, что у них есть дополнительная предпосылка. Например, "четное п". Это означает, что перед тем, как вы сможете применить принцип индукции, вам нужно знать, что у вас есть конечное деривация под рукой.

Answer 2

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

Хорошим примером является stream введите от ~~/src/HOL/Library/Stream:

codatatype 'a stream = SCons 'a "'a stream" (infixr "##" 65)

Это бесконечный список (обратите внимание, что в отличие, например, от списков на Haskell, этот тип потока должен быть бесконечно длинным, как если бы вы написали datatype Stream a = SCons a (Stream a) в Haskell, хотя "потенциально бесконечные" списки в стиле Haskell также возможны, ср. ленивые списки в AFP)

Затем вы можете, например, определить набор всех потоков, значения которых взяты из данного набора. Вы можете определить это как streams A = {s. sset s ⊆ A}, но в Изабель, это определяется коиндуктивно, как это:

coinductive_set streams :: "'a set ⇒ 'a stream set" for A :: "'a set"
  where "⟦a ∈ A; s ∈ streams A⟧ ⟹ a ## s ∈ streams A"

Другим, возможно, более простым примером, будет коиндуктивный предикат "для всех элементов" в потоках:

coinductive sall :: "('a ⇒ bool) ⇒ 'a stream ⇒ bool" for P :: "'a ⇒ bool" where
  "P x ⟹ sall P xs ⟹ sall P (x ## xs)"

Что касается вопроса о том, как построить такое бесконечное деривационное дерево, то есть показать, что коиндуктивный предикат имеет некоторое значение, вы должны сделать это с помощью коиндукции. Например, мы можем показать, что если P x держит, то sall P (sconst x) держит, где sconst x это просто ценность x повторяется бесконечно:

lemma sconst_reduce: "sconst x = x ## sconst x"
  by (subst siterate.code) simp_all

lemma sall_sconst: "P x ⟹ sall P (sconst x)"
proof (coinduction rule: sall.coinduct)
  assume "P x"
  thus "∃y ys. sconst x = y ## ys ∧ P y ∧ (ys = sconst x ∧ P x ∨ sall P ys)"
    by (subst sconst_reduce) auto
qed