如何为有根据的归纳类型选择设计？

2024-06-03 • 问答

在研究有充分根据的同时，我想看看不同的设计如何表现。例如，对于以下类型：

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)

很明显，在两种情况下，下降链都不是无限的，但在第二种情况下，很难证明有充分的根据：要证明给定的{{1} }。

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

证明第二个定义的充分依据并不是很难，它只需要额外的定理即可。在这里，依靠(y -> y < x -> acc y)对于x的可判定性，我们可以为情况_==_构造新的Nat，并可以重写目标类型以使用解决已知问题的方法减小尺寸作为_<_的解决方案。

(suc y) != x

bai0131 回答：如何为有根据的归纳类型选择设计？

从某种意义上说，第一个定义是“规范的”，而第二个定义则不是。在阿格达（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构造函数，那么情况将不再如此。

agda non-termination

本文链接：https://www.f2er.com/3086997.html

如何为有根据的归纳类型选择设计？

bai0131 回答：如何为有根据的归纳类型选择设计？

大家都在问