coq - 等价但不全等

全部

我正在编写 sf/plf 章节 Equiv。有一个练习

我们已经证明 [cequiv] 关系在命令上既是等价的又是全等的。你能想出一个命令上的等价关系而不是全等关系吗?

我不太明白等价和全等之间的区别。这似乎是一个程序的行为等价。任何人都可以对此进行更多解释吗?

谢谢

回答1

除了“行为等价”之外,还有其他等价。等价是自反、对称和传递的任何关系。同余是一种结构保持等价。

作为同余的等价的一个常见示例是算术模n。相等说模10是保留加法和乘法的等价关系,因此它是整数环算术的同余。但这不是一致的,例如用于“舍入到 0 整数除法”。例如。 23/11=23/1=3,即 23 mod 10 = 3 mod 1011 mod 10 = 1 mod 10,但 23/11 mod 10 <> 3/1 mod 10

相似文章

r - 在 R 中计算统计摘要时获取“NA”

我正在尝试将列从因子转换为数字,以便我可以运行统计摘要(平均值、中值、最大值、最小值)。但是,在运行此列的任何统计信息时,我不断得到NA。在运行任何转换代码之前,如果我运行str(),类型是'hms'...

随机推荐

最新文章