有根有据的电感式如何选择设计？

Question

在研究有根据性时，我想看看不同设计的行为方式。例如，对于一个类型：

data _<_ (x : Nat) : Nat -> Set where
   <-b : x < (suc x)
   <-s : (y : Nat) -> x < y -> x < (suc y)

有根据很容易证明。但是如果类似的类型定义不同：

data _<_ : Nat -> Nat -> Set where
   z-< : (m : Nat) -> zero < (suc m)
   s<s : (m n : Nat) -> m < n -> (suc m) < (suc n)

很明显，在这两种情况下，下降链都不是无限的，但在第二种情况下，充分性不容易证明：不容易证明 (y -> y < x -> Acc y) 对于给定的 x.

是否有一些原则可以帮助选择第一种设计而不是第二种设计？

证明第二个定义的成立性并非不可能，只是需要额外的定理。在这里，依靠 _==_ 对于 Nat 的可判定性，我们可以为案例 (suc y) != x 构造新的 _<_，并且可以重写目标类型以使用已知问题的解决方案减小尺寸作为 suc y.

的解决方案

-- trying to express well-foundedness is tricky, because of how x < y is defined:
-- since both x and y decrease in the inductive step case, need special effort to
-- prove when the induction stops - when no more constructors are available
<-Well-founded : Well-founded Nat _<_
<-Well-founded x = acc (aux x) where
   aux : (x y : Nat) -> y < x -> Acc _<_ y
   aux zero    y       ()
   aux x       zero    z-<           = acc \_ ()
   aux (suc x) (suc y) (s<s y<x) with is-eq? (suc y) x
   ...                   | no  sy!=x = aux x (suc y) (neq y<x sy!=x)
   ...                   | yes sy==x rewrite sy==x = <-Well-founded x

Answer 1

第一个定义在某种意义上是"canonical"，而第二个则不是。在 Agda 中，每个归纳类型都有一个子项关系，它是有根据的和可传递的，尽管不一定是完整的、可判定的或证明无关的。对于 W 型，它是：

open import Data.Product
open import Data.Sum
open import Relation.Binary.PropositionalEquality

data W (S : Set)(P : S → Set) : Set where
  lim : ∀ s → (P s → W S P) → W S P

_<_ : ∀ {S P} → W S P → W S P → Set
a < lim s f = ∃ λ p → a ≡ f p ⊎ a < f p

如果我们定义Nat为W型，那么泛型_<_与第一个定义相同。即使我们不知道 Nat 的构造函数，第一个定义也建立了子项关系。第二个定义只是一个子项关系，因为我们知道 zero 可以从每个 suc n 到达。如果我们添加一个额外的 zero' : Nat 构造函数，那么情况就不会再这样了。

有根有据的电感式如何选择设计？

How to choose the design for a well-founded inductive type?

agda

non-termination