为什么这两个代码不等价？我正在检查两者之间的逻辑等价性，它们失败了，可能是什么错误？是否将其视为宽度不匹配，或由多个驱动程序驱动？我正在使用 cadence LEC 进行形式验证

我有一个类似于“可选映射”的递归函数*，具有以下签名：

我定义了一个等价的（模列表反转）尾递归函数（omap_tr如下），我想证明两者是等价的，至少在这种情况下Some。

我目前没有这样做，要么是因为我的归纳不变量不够强，要么是因为我没有正确应用双重归纳。我想知道这种转换是否有标准技术。

*功能已简化；例如None在这里似乎没用，但在原始功能中是必需的。

代码

这是（简化的）非尾递归函数的代码，以及函数的示例f：

例如，omap f只需将Z整数转换为nat整数：

我执行了我认为是标准的基于累加器的转换，同时为and添加了一个acc参数：fomap

尽管返回了一个反向列表，但它似乎有效。这是一个使用非空累加器的示例：

我的第一次尝试包括一个nil累加器：

但我没有做归纳。我认为这一定是因为不变量不足以处理一般情况。

尽管如此，在我看来，以下任何引理都应该是可证明的，但恐怕它们也不够强大，无法证明：

标准的双重归纳应该允许直接证明这些引理，还是我需要更强的不变量？

我正在使用boost库编写用于图挖掘的代码，并且我想使用该vf2_sub_graph_iso函数，如果存在图子图同构，则通常vf2_subgraph_iso返回，否则返回，但在我的情况下，我想让它仅在图完全相同时返回（结构和标签），在官方文档中提到：和谓词用于测试边和顶点是否等价。truefalsetrueEdgeEquivalencePredicateVertexEquivalencePredicate

这是图形文件：3test.txt，这是我的代码的一部分：

如何在my_callback我的案例中使用属性映射来实现功能等效？

更新

这是一个简单的图形文件，仅包含 2 个图形：

这些图具有相同的结构但不同的标签，因此此代码必须返回 false 而不是 true：

更新2

我没有在问题中提到，即使没有 id（在不同的图中），顶点也可以相同的小先例示例。

我必须证明~p→(q→r)≡ q→(pvr)

这是我到目前为止所做的：

我应该如何解决这个问题？

我试图为班级完成一些代码：

由于我最终可能无法返回任何东西，它告诉我最后这样做：

这让我感到惊讶，因为该方法的返回类型是 type int。然而，它告诉我要返回一个char！我正在使用 eclipse，并且习惯了无穷无尽的警告和东西，这是一个重大的惊喜。

那么，char真的是一个int吗？为什么会这样？

我有一个很大的列表，其中列出了某些类型的对象Order。此外，我已经定义了一个IEqualityComparer<Order>并且我的目标是有效地创建一个列表（或分组）列表，其中每个子列表都包含彼此相等的对象。从数学上讲，我有一个等价关系（IEqualityComparer），并且想要一个所有等价类的列表。我考虑过使用HashSet<Order>，Dictionary<>或者Lookup<>但它们似乎不适合我的情况。那么有什么想法吗？

C ++中的等价和相等有什么区别？

这里有一个非常相似的问题。但是，这个问题被标记为math，而我对 C++ 上下文中的含义很感兴趣。

要在上下文中查看这些术语：Scott Meyers 在本视频的示例中使用它们。

WHERE我想知道MySQL 中的以下两个子句之间是否有区别：

对比

我在以下 SQLFiddle 中得到这两个查询的不同结果：http ://sqlfiddle.com/#!2/725396/3

我使用 xy 坐标（左下角、右上角）查找重叠矩形（区域）的算法工作正常。但是我将重叠的组合在一起的算法似乎不起作用。有人可以告诉我我做错了什么吗？

我的程序从这样的 .txt 文件中读取 xy 坐标...

0 5 3 6 (0,5 is bottom left corner and 3,6 is top right corner)

2 7 8 9 (2,7 is bottom left corner and 8,9 is top right corner)

然后找出所有组在重叠矩形上的内容并打印出这些组。

即矩形 0 与 2 重叠，2 与 1 重叠，1 与 5 重叠。这意味着矩形 0、2、1 和 5 都在 1 组中，因此我可以打印出该组 #1。

即矩形 4 和 3 重叠，这意味着矩形 4 和 3 在组 #2 中。

即矩形 10 与 11 重叠，矩形 11 与矩形 12 重叠。这意味着矩形 10、11 和 12 都在第 3 组中，这样我就可以整齐地打印出来。

有人可以向我解释为什么这些在 IEEE 754 浮点中不相等：

非常感谢！