时间戳

首页 > 解决方案 > Isabelle 中的 Map 和 Mapping 有什么区别？

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

问题描述

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

https://isabelle.in.tum.de/library/HOL/HOL/Map.html（地图）

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

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

提前致谢！

标签： functional-programmingtheoryisabelle

解决方案

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

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

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

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

推荐阅读