3

在研究有根据的时候，我想看看不同的设计是如何表现的。例如，对于一个类型：

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。

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

证明第二个定义的有根据并不难，它只需要额外的定理。在这里，依靠_==_for的可判定性，我们可以为 caseNat构造新的，并且可以重写目标类型以使用已知尺寸减小问题的解决方案作为 for 的解决方案。_<_(suc y) != xsuc 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
4

1 回答 1

1

第一个定义在某种意义上是“规范的”，而第二个定义不是。在 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-type，那么泛型_<_与第一个定义相同。即使我们不知道 的构造函数，第一个定义也建立了子项关系Nat。第二个定义只是一个子项关系，因为我们知道它zero可以从每个suc n. 如果我们添加了一个额外的zero' : Nat构造函数，那么就不会再出现这种情况了。

于 2019-11-17T12:06:16.740 回答