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

Question

于是我上网查了一下，发现是这样的：

以“地图”一词开头的两种理论。我通读了很长一段时间，但我无法真正辨别出它们之间的任何显着差异。有没有什么时候我应该使用前者而不是后者，反之亦然？

提前致谢！

Answer 1

Map.thy给你一些词汇来讨论偏函数，写成'a ? 'b，它是的缩写'a ? 'b option。

Mapping另一方面，该理论将其包装成一种新型的偏函数，这对代码生成很有用。如果您尝试导出涉及类型为部分函数的代码'a ? 'b，您将'a ? 'b option在导出的代码中得到字面意思，这意味着例如请求此类函数的域之类的内容将根本无法执行。

随着Mapping，在另一方面，你可以导出到一个更明智的执行情况（有限）地图，如关联列表或红黑树。

所以，简短的回答：不要担心，Mapping除非（以及何时）要导出可执行代码。