functional-programming - Isabelle 中的 Map 和 Mapping 有什么区别？

Question

所以我上网，发现了这些:

https://isabelle.in.tum.de/library/HOL/HOL/Map.html ( map )

https://isabelle.in.tum.de/library/HOL/HOL-Library/Mapping.html (映射)

以“ map ”一词开头的两种理论。我通读了好一阵子，但我无法真正辨别出它们之间的任何显着差异。是否有时我应该使用前者而不是后者，反之亦然？

提前致谢!

Answer 1

Map.thy 给了你一些偏函数的词汇，写成'a ⇀ 'b，是'a ⇒ '的缩写b 选项。

另一方面，映射 理论将其包装到一种新型的部分函数中，这对于代码生成很有用。如果您尝试导出涉及 'a ⇀ 'b 类型的部分函数的代码，您将在导出代码中得到字面上的 'a ⇒ 'b 选项，这意味着那例如诸如询问此类函数的域之类的事情将根本无法执行。

另一方面，使用映射，您可以导出更合理的(有限)映射实现，例如关联列表或红黑树。

所以，简短的回答:不要担心映射，除非(以及何时)您想要导出可执行代码。