Mai*_*tor 46 haskell type-theory agda dependent-type idris
依赖类型通常被宣传为一种方法,使您能够断言程序是否符合规范.因此,例如,要求您编写一个对列表进行排序的代码- 您可以通过将"sort"的概念编码为类型并编写诸如的函数来证明代码是正确的List a -> SortedList a.但是,您如何证明规范SortedList是正确的？难道不是这样,您的规范越复杂,您对该规范作为类型的编码就越不可能吗？
Jer*_*man 37
这是静态的类型系统版本,您如何判断您的测试是否正确？
我可以诚实地给出的唯一答案是,是的,您的规范越复杂和笨拙,您犯错的可能性就越大.您可以将类型理论形式主义中的某些东西搞得一团糟,就像将程序描述形式化为可执行函数一样.
希望你的规范很简单,小到足以通过检查来判断,而你的实现可能要大得多.一旦你有一些形式化的"种子"想法,你可以证明从这些想法中得出的想法是正确的.从这个角度来看,您可以更容易地从更简单的部分机械地和可证地推导出部分规范,并最终从您的规范中获得实现,您获得正确实现的可能性就越大.
但是不清楚如何形式化某些东西,这可能会导致你在将你的想法转化为形式主义时犯错误 - 你可能认为你证明了一件事,当你真正证明了另一件事 - 或者你可能发现自己在做类型理论研究以形式化一个想法.
Han*_*Lub 19
这是任何规范语言(甚至英语)的问题,而不仅仅是依赖类型.你自己的帖子就是一个很好的例子:它包含一个非正式的"排序函数"规范,只需要对结果进行排序,这不是你想要的(\xs -> []符合条件).例如参见这篇文章从M炼面包车Laarhoven的博客.
use*_*465 14
我认为这是另一种方式:良好类型的程序不能证明是无意义的(假设系统是持久的),而规范可能不一致或只是愚蠢.所以它不是"如何确保这段代码反映我的柏拉图式的想法？"而是"如何确保我的想法有意义地投射到一个有根据的纯粹语法规则的平面上？".如何确保你看到的鸟是一只模仿鸟[对于一些提供的模仿鸟的概念]？那么,研究鸟类并提高你成功的机会.但作为始终与人类,你不能 100%肯定.
类型理论是通过引入形式规则,机器检查证明(这是一篇非常相关的论文)和其他东西来缓解人类思维不完美的一种方法,它可以集中注意力,从而大大简化问题(如Brouwer所说:"数学仅仅是我们思想的确切部分,并没有更少,但你不能指望任何工具让你的思想"正确",因为没有统一的正确概念.IOW,没有办法正式连接非正式和正式:非正式就像在IOmonad 里面- 没有逃脱.
所以它不是"这种语法是否反映了我非常精确的语义？",而是"我可以将我的原始语义附加到这种强结构语法吗？".程序是适当的物质对象,而想法是繁琐的近似,只能按照惯例成为适当的物质对象.因此,我们使用约定形成一些基础,然后我们只相信它,因为相信所有众多想法的一小部分而不是所有想法更为明智.
正式方法可以做的一件事,我认为其他人没有涉及的是帮助将简单的事物与更复杂的事物联系起来.您可能不确定如何准确指定Set数据结构应该如何表现,但如果您可以根据排序列表编写简单版本,则可以证明基于平衡搜索树的花哨版本通过toList函数正确地与之相关.也就是说,您可以使用正式方法将您对排序列表的信心转移到平衡搜索树.
你如何证明数学是正确的？也就是说,你如何证明整数加法是计算苹果的正确方法,或者你如何证明真正的加法是增加权重的正确方法？在形式/数学和非正式/真实之间总是存在接口.它需要技巧和数学/物质品味来找到解决特定问题的适当形式.正式方法不会消除这种情况.
形式方法的价值是双重的:
你不会知道你的程序是否正确,除非你知道它实际满足的属性.在您知道您的排序例程是否"正确"之前,您首先必须知道它实际上做了什么.找出问题的任何程序都将是一种正式的方法(甚至单元测试!),因此拒绝"正式方法"的人实际上只是将自己局限于可用方法的一小部分.
即使你知道如何找出一个程序实际上做了什么,人们也会在他们的数学推理中犯错误(我们不是理性的生物,无论某些意识形态可能会声称); 所以让机器检查我们是有帮助的.这与我们使用单元测试的原因相同 - 运行桌面检查并确保程序完成我们想要的操作是很好的.但让计算机进行检查并告诉我们结果是否正确有助于防止错误.让计算机检查我们关于程序行为的证明是完全相同的原因.
| 归档时间： |
|
| 查看次数： |
1965 次 |
| 最近记录： |