问题标签 [proof]

多线程算法特别难以设计/调试/证明。Dekker 算法是一个很好的例子，说明了设计一个正确的同步算法是多么困难。Tanenbaum 的现代操作系统在其 IPC 部分中充满了示例。有没有人对此有很好的参考（书籍，文章）？谢谢！

我看到了这个问题，并且很好奇引理是什么（维基百科没有太大帮助）。

我知道这基本上是一个理论证明，为了使一种语言进入某个类别，它必须是正确的，但除此之外，我真的不明白。

有人愿意尝试以非数学家/计算机科学博士可以理解的方式在相当细化的层面上解释它吗？

为什么不能像数学陈述一样证明计算机程序？数学证明建立在其他证明的基础上，这些证明建立在更多证明和公理之上——我们认为这些真理是不言而喻的。

计算机程序似乎没有这样的结构。如果你写一个计算机程序，你怎么能把以前证明过的作品拿来用它们来证明你的程序的真实性？你不能，因为不存在。此外，编程的公理是什么？该领域的原子真理？

我对上述问题没有很好的答案。但似乎软件无法被证明，因为它是艺术而不是科学。如何证明毕加索？

我正在尝试 Coq，但我不完全确定我在做什么。是：

相当于：

编辑：我认为他们是。

如何在 Coq 中证明 (forall x, P x /\ Q x) -> (forall x, P x)？已经尝试了几个小时，但无法弄清楚如何将先行词分解为 Coq 可以消化的东西。（我是新手，显然:)

有谁知道以下任何例子？

1. 证明助手（例如Coq ）中关于正则表达式（可能通过反向引用扩展）的证明开发。
2. 关于正则表达式的依赖类型语言（例如Agda ）的程序。

在编写数学证明时，一个目标是继续压缩证明。证明变得更加优雅，但不一定更具可读性。压缩转化为更好的理解，因为您清除了不必要的字符和冗长。

我经常听到开发人员说你应该让你的代码占用空间尽可能小。这会很快产生不可读的代码。在数学中，这不是一个问题，因为该练习纯粹是学术性的。然而，在时间就是金钱的生产代码中，让人们试图弄清楚一些非常简洁的代码在做什么似乎没有多大意义。对于更冗长的代码，您可以获得可读性和节省。

您在什么时候停止压缩软件代码？

是否存在两个（确定性）有限状态机的等价性且总是需要有限时间的一般证明？也就是说，给定两个 FSM，你能否证明给定相同的输入，它们总是会产生相同的输出，而实际上不需要执行 FSM（这可能是非终止的？）。如果确实存在这样的证明，那么时间复杂度是多少？

当我们开始进入算法设计和更多离散的计算机科学主题时，我们最终不得不一直证明事情。每次我看到有人问如何真正擅长证明时，常见的（可能是懒惰的）答案是“练习”。

如果您掌握了基础知识，练习一切都很好，但是您如何进入数学证明的思维定势？感应何时点击？哪些资源最适合教授这些主题？在沉迷于证明写作之前应该研究哪些基础主题？

在处理递归运行时时如何确定递归树的高度？它与确定普通树的高度有何不同？

替代文本 http://homepages.ius.edu/rwisman/C455/html/notes/Chapter4/ch4-9.gif

编辑：对不起，我的意思是添加如何从递归关系中获取递归树的高度。