26

我在 Coq 的 SSReflect 扩展中发现了两个约定，它们看起来特别有用，但我还没有看到它们在较新的依赖类型语言（Lean、Agda、Idris）中被广泛采用。

首先，可能的谓词表示为布尔返回函数，而不是归纳定义的数据类型。这在默认情况下带来了可判定性，为计算证明开辟了更多机会，并通过避免证明引擎需要携带大量证明条款来提高检查性能。我看到的主要缺点是在证明时需要使用反射引理来操纵这些布尔谓词。

其次，具有不变量的数据类型被定义为包含简单数据类型和不变量证明的相关记录。例如，固定长度的序列在 SSReflect 中定义如下：

Structure tuple_of : Type := Tuple {tval :> seq T; _ : size tval == n}.

Aseq和该序列长度为某个值的证明。这与 Idris 定义这种类型的方式相反：

data Vect : (len : Nat) -> (elem : Type) -> Type

一种依赖类型的数据结构，其中不变量是其类型的一部分。SSReflect 方法的一个优点是它允许重用，例如，许多为它们定义的函数seq和关于它们的证明仍然可以与tuple（通过在底层上操作seq）一起使用，而使用 Idris 的方法，像reverse,append和类似的函数需要被重写为Vect. Lean 实际上在其标准库中具有等效的 SSReflect 样式vector，但它也具有 Idris 样式array，该样式似乎在运行时具有优化的实现。

一本面向 SSReflect 的书甚至声称Vect n A样式方法是一种反模式：

在依赖类型语言和 Coq 中，一个常见的反模式是将这些代数属性编码到数据类型和函数本身的定义中（这种方法的典型示例是长度索引列表）。虽然这种方法看起来很吸引人，因为它展示了依赖类型捕获数据类型和函数的某些属性的能力，但它本质上是不可扩展的，因为总会有另一个感兴趣的属性，这是设计者没有预见到的数据类型/函数，因此无论如何它都必须被编码为外部事实。这就是为什么我们提倡这种方法，其中数据类型和函数的定义尽可能接近程序员定义它们的方式，并且它们的所有必要属性都被单独证明。

因此，我的问题是，为什么这些方法没有被更广泛地采用。有没有我遗漏的缺点，或者它们的优点在对依赖模式匹配的支持比 Coq 更好的语言中不太重要？

4

2 回答 2

6

我可以就第一点提供一些想法（将谓词定义为布尔返回函数）。我对这种方法的最大问题是：那么根据定义，该函数不可能有错误，即使结果证明它计算的不是你想要计算的。在许多情况下，如果您必须在其定义中包含谓词的决策过程的实现细节，它也会掩盖您所说的谓词的实际含义。

在数学应用中，如果您想定义一个谓词，它是一般不可判定的事物的特化，即使它恰好在您的特定情况下是可判定的，也会存在问题。我在这里讨论的一个例子是用给定的表示来定义组：在 Coq 中，定义它的一种常用方法是 setoid ，其底层集合是生成器中的正式表达式，而“word”给出的等式等价”。一般来说，这种关系是不可判定的，尽管在许多特定情况下它是可判定的。但是，如果您仅限于使用可确定单词问题的演示文稿来定义组，那么您将失去定义将所有不同示例联系在一起的统一概念的能力，并且一般地证明关于有限表示或关于有限表示组的事情。另一方面，将词等价关系定义为抽象Prop或等价物很简单（如果可能有点长）。

就个人而言，我更喜欢首先给出谓词的最透明的定义，然后在可能的情况下提供决策过程（返回类型值的函数{P} + {~P}是我的偏好，尽管返回布尔值的函数也可以很好地工作）。Coq 的类型类机制可以提供一种方便的方式来注册此类决策过程；例如：

Class Decision (P : Prop) : Set :=
decide : {P} + {~P}.
Arguments decide P [Decision].

Instance True_dec : Decision True := left _ I.
Instance and_dec (P Q : Prop) `{Decision P} `{Decision Q} :
  Decision (P /\ Q) := ...

(* Recap standard library definition of Forall *)
Inductive Forall {A : Type} (P : A->Prop) : list A -> Prop :=
| Forall_nil : Forall P nil
| Forall_cons : forall h t, P h -> Forall P t -> Forall P (cons h t).
(* Or, if you prefer:
Fixpoint Forall {A : Type} (P : A->Prop) (l : list A) : Prop :=
match l with
| nil => True
| cons h t => P h /\ Forall P t
end. *)

Program Fixpoint Forall_dec {A : Type} (P : A->Prop)
  `{forall x:A, Decision (P x)} (l : list A) :
  Decision (Forall P l) :=
  match l with
  | nil => left _ _
  | cons h t => if decide (P h) then
                  if Forall_dec P t then
                    left _ _
                  else
                    right _ _
                else
                  right _ _
  end.
(* resolve obligations here *)
Existing Instance Forall_dec.
于 2018-03-27T17:58:18.047 回答
5

这在默认情况下带来了可判定性，为计算证明开辟了更多机会，并通过避免证明引擎需要携带大量证明条款来提高检查性能。

您不必像Edwin Brady 的论文中以“强制优化”的名义所描述的那样使用大的术语。Agda 确实有影响类型检查的强制（特别是如何计算宇宙是相关的），但我不确定仅在类型检查时使用的东西是否真的在运行时之前被删除。无论如何，Agda 有两个不相关的概念：.(eq : p ≡ q)通常eq是不相关（含义在类型检查时是不相关的，因此它在定义上等于任何其他此类类型的术语）和..(x : A)脊柱不相关（不确定它是否是正确的术语。我认为Agda 消息来源称这种事情为“非严格无关”），字面意思是删除计算上不相关但并非完全不相关的术语。所以你可以定义

data Vec {α} (A : Set α) : ..(n : ℕ) -> Set α where
  [] : Vec A 0
  _∷_ : ∀ ..{n} -> A -> Vec A n -> Vec A (suc n)

并将n在运行时间之前被擦除。或者至少它看起来是这样设计的，很难确定，因为 Agda 有很多文档记录不完整的特性。

你可以在 Coq 中编写那些零成本证明，因为它也实现了与Prop. 但是无关性在 Coq 的理论中根深蒂固，而在 Agda 中它是一个单独的特征，因此完全可以理解，为什么人们在 Coq 中比在 Agda 中更容易使用无关性。

SSReflect 方法的一个优点是它允许重用，例如，许多为它们定义的函数seq和关于它们的证明仍然可以与tuple（通过在底层上操作seq）一起使用，而使用 Idris 的方法函数，如 reverse、append 和喜欢需要重写Vect。

如果您无论如何都必须证明属性，并且这些证明与在索引数据上定义的函数具有相同的复杂性，那么这不是真正的重用。执行统一机制的工作并传递明确的证明并应用引理来从中获取length xs ≡ n（suc (length xs) ≡ n以及sym,和在许多情况下统一机制可以使您摆脱的所有其他引理）也很不trans方便。subst此外，由于滥用命题相等，您会失去一些清晰度：拥有xs : List A; length xs ≡ n + m而xs : Vec A (n + m)不是提高上下文的可读性，尤其是当它们通常是巨大的时。还有另一个问题：有时使用 SSReflect 的方法定义一个函数更难：你reverse提到Vect，我挑战你从头开始定义这个函数（使用reverseforList作为引擎盖下的“重用”部分），然后将你的解决方案与Data.VecAgda 标准库中的定义进行比较。如果默认情况下您没有为命题启用无关性（Agda 就是这种情况），那么如果您想证明，那么您还需要证明有关证明的属性，例如，reverse (reverse xs) ≡ xs这是很多非平凡的样板文件.

所以SSReflect的做法并不完美。另一个也是。有什么可以改善两者的吗？是的，装饰品（参见装饰品代数、代数装饰品和装饰品的本质）。您可以通过应用相应的装饰代数轻松获得Vec，List但我不能说您会从中获得多少代码重用以及类型是否会让您发疯。我听说人们实际上在某个地方使用装饰品。

所以并不是说我们有一个理想的 SSReflect 的解决方案，而其他人拒绝采用它。只是希望有一种更合适的方式来获得实际的代码重用。

更新

Anton Trunov在他们的评论中让我意识到我的思想有点过于 Agda，而且 Coq 中的人有可以大大简化证明的策略，所以在 Coq 中证明通常比定义更容易（前提是你有crushCPDT书中的武器）对数据的功能。好吧，那么我猜想默认情况下证明无关紧要和重型策略机制是 SSReflect 的方法在 Coq 中有效的原因。

于 2018-03-27T20:39:52.810 回答