为什么没有新的依赖类型语言采用SSReflect的方法？

作者: 5678
发布时间: 2024-08-13 11:46:41 (10小时前)
转自：

3 条回复

0#
回复此人
LOGO | 2019-08-31 10-32

<div class =“post-text”itemprop =“text”> <BLOCKQUOTE> 这默认带来可判定性，通过计算开辟了更多的证明机会，并通过避免校对引擎携带大量证明条件来提高检查性能。 </BLOCKQUOTE> 您不必携带大型术语，如中所述 <a href="https://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf" rel="nofollow noreferrer"> 埃德温布拉迪的论文 </A> 在“强制优化”的名义下。 Agda确实有强制影响类型检查（特别是计算Universe的方式是相关的），但我不确定在类型检查时使用的东西是否真的在运行时被删除。无论如何，Agda有两个不相关的概念： <code> .(eq : p �� q) </code> 通常是无关紧要的（意思是 <code> eq </code> 在类型检查时间是无关紧要的，所以它在定义上等于这种类型的任何其他术语 <code> ..(x : A) </code> 脊椎不相关（不确定它是否是一个正确的术语。我认为Agda来源称这种事情为“非严格的无关紧要”），这实际上是为了消除计算上无关紧要但不完全无关的术语。所以你可以定义 <pre> <code> data Vec {��} (A : Set ��) : ..(n : ?) -> Set �� where [] : Vec A 0 _��_ : ? ..{n} -> A -> Vec A n -> Vec A (suc n) </code> </pre> 和 <code> n </code> 将在运行时间之前删除。或者至少它似乎是这样设计的，很难确定，因为Agda有很多记录不完整的功能。 你可以在Coq中编写那些零成本证明，因为它也会对生活中的东西产生无关紧要的影响 <code> Prop </code> 。但是无关紧要是内容深入Coq的理论，而在Agda中它是一个独立的特征，所以它完全可以理解，为什么人们比在Agda中更容易在Coq中找到无关紧要的东西。 <BLOCKQUOTE> SSReflect方法的一个优点是它允许重用，因此例如为许多定义的函数 <code> seq </code> 关于它们的证据仍然可以使用 <code> tuple </code> （通过操作底层证券 <code> seq </code> ），而Idris的方法函数如reverse，append等需要重写 <code> Vect </code> 。 </BLOCKQUOTE> 如果你必须要证明属性并且那些证明与索引数据定义的函数具有相同的复杂性，那么它不是真正的重用。完成统一机制的工作并传递明确的证据并应用引理来获得也是不方便的 <code> length xs �� n </code> 从 <code> suc (length xs) �� n </code> （并且 <code> sym </code> ， <code> trans </code> ， <code> subst </code> 以及统一机器在许多情况下可以拯救你的所有其他引理）。而且，你通过滥用命题平等而失去一些清晰度：拥有 <code> xs : List A; length xs �� n + m </code> 代替 <code> xs : Vec A (n + m) </code> 不会提高你的上下文的可读性，特别是如果它们很大，通常就是这种情况。还有另外一个问题：有时使用SSReflect方法定义函数会更难：你提到过 <code> reverse </code> 对于 <code> Vect </code> ，我挑战你从头开始定义这个功能（用 <code> reverse </code> 对于 <code> List </code> 作为引擎盖下的“重用”部分，然后将您的解决方案与中的定义进行比较 <code> Data.Vec </code> 来自Agda标准库。如果您默认情况下没有为命题启用不相关性（Agda就是这种情况），那么如果您想证明，例如，您还需要证明有关证据的属性。 <code> reverse (reverse xs) �� xs </code> 这是很多非平凡的样板。 所以SSReflect的方法并不完美。另一个也是。两者都有改进吗？是的，饰品（见 <a href="http://plv.mpi-sws.org/plerg/papers/mcbride-ornaments-2up.pdf" rel="nofollow noreferrer"> 观赏代数，代数装饰品 </A> 和 <a href="https://pages.lip6.fr/Pierre-Evariste.Dagand/stuffs/journal-2013-catorn-jfp/paper.pdf" rel="nofollow noreferrer"> 饰品的精髓 </A> ）。你可以轻松搞定 <code> Vec </code> 从 <code> List </code> 通过应用相应的观赏代数，但我不能说你将从中获得多少代码重用，以及类型是否会让你疯狂。我听说人们实际上在某处使用饰物。 因此，并不是我们拥有理想的SSReflect解决方案而其他人拒绝采用它。希望有更合适的方法来获得实际的代码重用。 的 UPDATE </强> 的 安东特鲁诺夫 </强> 在他们的评论中让我意识到我有点过于敏捷，Coq中的人有战术可以简化证明很多，所以在Coq证明通常更容易（只要你有武器像 <code> crush </code> 来自 <a href="http://adam.chlipala.net/cpdt/" rel="nofollow noreferrer"> CPDT </A> 比定义数据的功能。那么，我认为证明默认无关紧要，重型战术机器是使SSReflect的方法在Coq中有效的原因。 </DIV>

编辑
1#
回复此人
Gassyc加西可 | 2019-08-31 10-32

<div class =“post-text”itemprop =“text”> 我可以提供关于第一点的一些想法（将谓词定义为布尔返回函数）。这种方法的最大问题是：根据定义，函数不可能有错误，即使事实证明它的计算结果不是你想要计算的。在许多情况下，如果必须在其定义中包含谓词的决策过程的实现细节，它也会模糊谓词的实际含义。 在数学应用程序中，如果你想定义一个谓词，这个谓词通常是不可判定的东西，即使它在你的特定情况下恰好是可判定的，也会有问题。我在这里谈论的一个例子就是用给定的表示来定义组：在Coq中，定义它的常用方法是将底层集合作为生成器中的正式表达式，以及“单词”给出的相等性。等价”。一般来说，这种关系不是可判定的，尽管在很多特定情况下都是如此。但是，如果您仅限于定义具有可解决单词问题的演示文稿的组，则您将失去定义将所有不同示例联系在一起的统一概念的能力，并且通常证明有限演示或有限呈现组的事物。另一方面，将单词等价关系定义为抽象 <code> Prop </code> 或等价物是直截了当的（如果可能有点长）。 就个人而言，我更愿意首先给出最透明的谓词定义，然后尽可能提供决策程序（函数返回类型的值） <code> {P} + {~P} </code> 这是我的偏好，虽然布尔返回函数也可以正常工作）。 Coq的类型类机制可以提供一种方便的方式来注册这样的决策程序;例如： <pre> <code> 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. </code> </pre> </DIV>

编辑

登录后才能参与评论