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

【问题标题】：What's the difference between Map and Mapping in Isabelle?Isabelle 中的 Map 和 Mapping 有什么区别？
【发布时间】：2021-05-18 01:17:57
【问题描述】：

于是我上网，发现了这些：

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

提前致谢！

【问题讨论】：

【解决方案1】：

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

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

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

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

【讨论】：