问题标签 [transitivity]

I want to proof this lemma in Coq:

I know that Coq.Relations.Relation_Definitions defines transitivity for relations:

Definition transitive : Prop := forall x y z:A, R x y -> R y z -> R x z.

Simply using the proof tactic apply transitivity obviously fails. How can I apply the transitivity lemma to the goal above?

我被困在这个问题上。这个问题的答案应该是什么：

关系方案 Student Performance (name, courseNo, rolINo,grade) 具有以下函数依赖关系：
name, courseNo, ->grade
rolINo, courseNo ->grade
name -> rolINo
rolINo -> name

这种关系方案的最高范式是

(a) 2 NF (b) 3 NF (c) BCNF (d) 4 NF

我在 python 中有一个如下列表（真正的列表很大，我不能仅通过查看它来做到这一点）：

我将其拆分为数据和名称以处理数据：

考虑到电子邮件和电话，我需要做一个将所有重复项放在一起的字典，但我需要应用传递性：因为如果我们考虑电子邮件，第 0 行 = 第 2 行，如果我们考虑电话，第 1 行，第 1 行 = 行3 如果我们再次考虑电子邮件，我需要得到在这种情况下所有候选人都是 0、1、2 和 3，而 4 是单独的。

我创建了以下代码：

所以现在我需要应用传递性规则，将 0 到 3 和单独的 4 组合在一起。

如果你打印

你得到：

电子邮件 defaultdict(, {'a@gmail.com': [0, 2],'b@gmail.com': [1, 3], 'c@gmail.com': [4]})

phone defaultdict(, {'1': [0, 1], '3': [3], '2': [2], '4': [4]})

不知道如何让那些考虑传递属性的人联合起来。我需要得到类似的东西：

first_group: [0, 1, 2, 3]
second_group: [4]

谢谢！

我有一组序列化到文件的项目。有些项目可以依赖其他项目，但不允许循环引用。因此，它们需要以某种方式进行序列化，如果A依赖于B，B则首先在文件中对其进行序列化。

我写了我的Comparator，它使用一个reliesOn()函数来确定两个项目是否链接：

这适用于某些情况，但不是全部。在调试中，很明显排序依赖于 的传递性质Comparator，并且可以理解的是不会比较每个可能的项目配对。

例如，通过 5 个项目A，E如果：

那么一种可能的顺序是：

至少，E来之前B，B来之前A。

但是，在比较阶段（以释义为例），发生的C是与 比较E，返回，0因为它们没有关系。然后C是比较B，也返回0。

结果，排序算法假设B = E，但事实并非如此。（即使我违反了Comparator合同compare()。）如何以确保传递性的方式编写我的方法？

编辑：有人指出我正在对有向无环图执行拓扑排序。我正在回忆我的数据结构课程。幸运的是，维基百科似乎有一个很好的线性时间算法来执行这种排序——我会试一试。

我有一个 15 个城市的列表。我从可能的 15*14/2=105 对城市中随机抽取 70 对。对于 70 对中的每一对，我要求我的参与者判断 A 城市是否大于 B 城市。重要的是，有时参与者会犯“错误”并给出与他们之前的答案不相容的答案。（即，它违反了传递性）。

我需要一种方法来根据每个参与者的反应对我的城市进行排序，以最大限度地减少违反传递性的试验次数。

我不需要城市的实际顺序，因为可能没有唯一的解决方案。我只需要计算每个参与者给出的不及物答案的（最小）数量。

除了使用详尽搜索之外，我怎么能做到这一点？

编辑：举个例子，以城市 A、B、C、D 和 E 为例。参与者 Jon Doe 认为城市的正确顺序（从最小到最大）是 ABCDE。我不在乎他是否真的正确，我只在乎他的回答（如下所列）与他的信念是否相符。

在三项独立试验中，乔恩回答如下：

试验 1：A < B

试验 2：B < C (+)

试验 3：C < D

试验 4：D < E (+)

试验 5：E > B (*)

因此，试验 5 (*) 中的答案与试验 2 和 4 中的答案不兼容。要么一项试验（nr. 5）不符合 Jon 的信念，要么 2 项试验（2 和 4）不符合。我不在乎弄清楚 Jon 的信念（ABCDE）是什么，我只需要知道 Jon Doe 的“不及物答案的最小数量”是 1。

我有一个转换模板，如果转换是安全的，它应该在指向类型的指针之间进行转换。这类似于 static_cast 但允许用户定义类型。

示例：复杂类型的 2 种表示形式，一种作为具有 2 个用于 real/imag 的成员的结构，一种作为具有 2 个元素的数组。将指向其中一个的指针转换为指向另一个的指针是安全的。

我的模板如下所示：

也就是说，我可以从 Complex* 转换为 T*，从 T* 转换为 fftw_complex*。从语义上讲，这意味着我也可以从 Complex* 转换为 fftw_complex*。

但是我怎么能告诉编译器，这没关系？我试过：

并将它与几个基本类型（double、float、int ...）一起使用，以至少允许 T->base->U 这应该足够了。

不幸的是，编译器似乎没有找到 SafePtrCast< Complex , fftw_complex >的特化

有没有更好的方法来处理这个问题？我的模板有什么问题？

是否可以将休眠配置为仅从我依赖的项目中获取传递依赖项（compile（“foobar”））并禁用其他所有项目的传递性？这就是我到目前为止所尝试的：

它不起作用。根本没有传递依赖关系。

按照建议更新 1

虽然不考虑来自 foobar 的依赖关系：

更新 2

以下解决方案现在对我有用：

我一直试图理解，当我在 C++ 中使用常量参数和该对象内部的指针变量编写函数时，const 标志并不能保护底层内存不被修改。例如，在operator=()名为 的类的函数中执行以下操作是完全合法的X：

(*)：这与以下相同：

但不一样：

这将产生以下错误：

我理解为什么other.x被强制转换为 aint* const但我不明白为什么它没有同时被强制转换为 a const* int（即 a const int* const）。当我编写带有const参数的函数时，我的逻辑建议该参数中的任何内容都应该继承 constness，因为这应该是 的目的const，以保护基础数据不被修改。

当从类的版本之外访问指针成员时，const我认为应该合理地期望对象的const关键字应该保护从类中脱离出来的任何东西（甚至是内存）不被修改。反对这一点的论点是外部内存不属于该对象，因此保护它也不应该是它的责任。我的观点是，在这种情况下（在任何其他情况下，当它被其他地方以任何类型的访问权限访问时）我们正在从const对象中取出一些东西。换句话说，它让人们看到了自身之外的东西。那么不引起关注的原因是什么const呢？那不会

我想知道下面的 CTL 公式是否等价，如果是，你能帮助我说服自己它们是等价的吗？A(p U ( A(q U r) )) = A(A(p U q) U r)

我想不出任何与之相矛盾的模型，我的直觉告诉我这些公式是等价的，但我找不到任何支持该陈述的等价物。我试图将等价性 A(p U q) == not(E ((not q) U not(p or q)) 或 EG (not q)) 改写成有用但多次失败的东西。

我浏览了我的课程资料以及谷歌，但我找不到任何东西。但是，我确实在这里找到了另一个具有相同等价问题但没有答案的问题，因此我正在尝试进行第二次尝试。

我最近阅读了内存屏障中cpu的传递性，作者强调只有一般屏障才能保证传递性。但是，我不能很好地理解它。例如：

假设X在CPU3的缓存中，状态被修改；Y在CPU2的缓存中，状态也被修改。

如果我们在读屏障之前添加写屏障，CPU1 与 CPU2 共享它的存储缓冲区。（它成为一个普遍的障碍）

1) CPU1 在存储缓冲区中设置 X(X=1) 的值。

2) CPU2 从存储缓冲区（共享存储缓冲区）中读取 X 的值。

3）CPU2在存储缓冲区（写屏障）中标记X，并读取无效队列以确保没有来自CPU3的无效消息（读屏障）。

4) CPU2 想要将 X 的缓存行从无效更改为已修改，因此向 CPU3 发送无效消息。

5) CPU3接收到X的无效消息，将其放入无效队列并响应CPU2。

6) CPU2收到response后，将X = 1写入内存或缓存，并加载Y == 0。

...

7) CPU3在执行通用屏障时会发现它的无效队列中有X的无效消息，之后X必须等于1。

没关系，我可以理解。但是，我从perbook的图14.3中阅读了另一个示例，如下所示：

有一些机会触发断言。作者说将所有障碍更改为 smp_mb 可以在 Quick Quiz 14.2 的回答中修复它。

所以，我的问题是为什么我们需要将 thread1 中的屏障更改为 smp_mb？如果 thread0 和 thread1 在 CPU0 和 CPU1 上运行，并且它们共享一个存储缓冲区。在线程 1 执行 Store C = 1 后，它们的存储缓冲区会爆炸。

[A(wb), B, C]

因为thread2（在CPU2上运行）也使用smp_mb而不是barrier，所以它保证如果看到C == 1，A一定是1。

我在 MESI 内存一致性协议中描述了以上所有内容。也许作者的意思是有另一个协议使 thread1 中的屏障必须代替 smp_mb 来保证 cpu 的传递性？

谁能给我一个例子吗？

也许在特定协议中考虑传递性是一个错误。我们必须记住的是，rmb() 或 wmb() 并不能保证 cpu 的传递性，因为有很多不同的协议和架构。