问题标签 [theorem]

我在 Isabelle/HOL 中实现了一些插入排序算法，用于生成代码（ML、Python 等）。我确信相应的函数可以正常工作，但我需要创建一些定理来证明它并确保它可以正常工作。我的功能是：

问题是我不知道如何正确创建定理。我需要证明有序列表与原始列表具有相同的长度，并且两个列表具有相同的元素名称。我的第一个定理是：

第一个定理试图证明列表是正确排序的，第二个定理试图证明两个列表具有相同的长度。

当我应用归纳和自动时，我希望得到 0 个子目标，这说明定理是正确的并且算法工作正常，但是在那之后我不知道如何删除子目标，我的意思是我不知道该怎么做简化规则（lemma [simp]: ""）来做，我会感谢你的帮助。

我正在使用 HOL-Z 中的数学工具包来释放一些 Isabelle 谓词。具体来说，我使用部分函数定义来定义我正在编写的 Z 规范中的一些关系，在其中我将模式转换为规范语句，以便我可以生成简单的 HOL 谓词。

来自 HOL-Z 工具包的定义

当我在谓词中编写以下内容时：

其中 balance 和 Bbalance 都是偏函数（在 Z 中），在 Isabelle 中的形式为 ('a <=> 'b)，我认为它表现良好。

我如何定义另一个函数，我说这两个部分函数对于所有 'x' 都是完全不相交的。我的意思是相同值在两个偏函数“balance”和“Bbalance”上的关系应用永远不会产生相同的值。就像是...

抱歉解释不佳。我们通过专家建议学习:)。

你好，谁能帮我解决这个问题

这就是我到目前为止所做的让

在这里应用主定理

现在卡住了。

您如何计算这些关系的紧密约束运行时间？

• T(n)=T(n-3)+n^2
• T(n) = 4T(n/4)+log^3(n)

对于第一个，我使用了给我 n^2 但不正确的替换方法，第二个我使用了 Masters Theorem 并得到了 nlog^4(n)，这也是不正确的。一个彻底的解释会很有帮助。谢谢！

问题：您有一个算法，将n 个大小的问题划分为六个子问题，大小为原始问题的四分之一。对于划分算法进行100 步和合并75n。算法的时间渐近复杂度是多少？

所以主定理的公式

对于这个问题a = 6和b = 4，但我不知道在哪里适合划分和合并信息。

可接受的结果是： O ( n ^1.2924 )、omega ( n ^1.2 ) 和O (1.001 ⁿ )

我已经使用SATbbox实现了碰撞检测，如果另一个高于或低于边界框，我会得到误报。

我将边界框的每个（现在）轴对齐面投影到它自己的角和其他bbox角上。

返回的碰撞数据是正确(depth, stepheight)的，但它为每个高于或低于边界框的对象返回碰撞的事实是ofc错误的。

aabb我根据一个有效的简单碰撞检查检查我的结果。

这是代码：

其中面法线定义为：

我添加了一个屏幕截图来显示问题：

所以问题是：

它对边界框下方或上方的所有对象返回误报。

这个问题是在考试中出现的，我不知道该怎么做，任何人都可以帮助我或给点提示。我觉得大师的方法在这里不适用？请帮忙。

T(n)=T(n/2)+ θ(logn)

这个问题是对以下问题isabelle proving commutativity for add的跟进，我的跟进时间太长，无法发表评论。如上所述的问题是显示定义如下的 add 函数的交换性：

试

由于缺少引理而被卡住（在归纳情况下）。我对这个问题感到好奇，并正在探索证明它的替代方法（尽管效率较低）。假设我们定义了引理

哪个Isabelle可以通过归纳自动证明那么归纳步骤就是证明

我们可以手动完成如下

但是，Isabelle 无法证明这一点，并且简化器似乎停留在第二行。但是，使用更明显的

而不是引理1，证明成功。它似乎能够在两个方向上使用 Lemma2，但不能使用我上面定义的 Lemma1。有谁知道为什么？我觉得我在某个地方忽略了一些明显的东西..

备注：我意识到简化器实际上只在一个方向上应用定义等，但使用启发式方法尝试将等式的两边简化为同一个术语

我对IEEE754双精度感到困惑，我考虑了两个问题：
1. 为什么区间 -2 ⁵⁴ , -2 ⁵⁴ +2, -2 ⁵⁴ +4...2 ⁵⁴中的每个数字都是可表示的？

2.为什么 2 ⁵⁴ +2 不可表示？

你能帮助我吗 ？我了解 IEEE754的工作方式- 但是，我看到它时遇到问题。

根据 Böhm-Jacopini 定理，可以仅使用三个语句来编写算法：

• 顺序
• 选择
• 迭代

很多老师都认为定理是一种信仰行为，他们教导不要使用（goto、jump、break、multiple return 等），因为这些指令是邪恶的。

但是当我要求解释时，没有人能够提供定理的证明。

我个人不认为这个定理是错误的，但我认为它在现实世界中的适用性并不总是更好的选择。

所以我做了一个小小的搜索，这些是我的疑问：

1. 该定理已在流程图结构上进行归纳证明，但它真的适用于计算机程序吗？
   根据维基百科，“Böhm 和 Jacopini 的作为程序转换算法并不真正实用，因此为在这个方向上的进一步研究打开了大门”。

2. 定理的一个结果证明每个“goto”都可以通过归纳转化为选择或迭代，但效率呢？我找不到任何证据表明可以重写每个算法以保持相同的性能。

3. 递归，递归算法真的可以只使用序列、选择和迭代来编写吗？我知道一些递归算法可以优化为循环（想想尾递归），但真的可以适用于所有人吗？

4. 干净的代码，我知道滥用跳转会产生可怕的代码，但我认为在某些情况下正确使用循环中的中断可以提高代码的可读性。

样本：

可以改写为：

就我个人而言，我认为这个定理并不是为了编写更好的代码而创建的，干净的代码必须遵循这个定理的想法已经因为一个奇怪的主观原因传播到了世界上。

5. 我发现了这篇有趣的文章：https : //www.cs.cornell.edu/~kozen/papers/bohmjacopini.pdf 我认为这证明了不能强迫真正的程序遵循 Jaopini 定理。
   你有同样的结论吗？

总结这个问题，我需要知道一个只使用（序列、选择和迭代）的程序是否真的比任何其他使用不同语句的程序更好，以及是否有证明或者是否都是主观的。