ACL2中的排序映射

Question

我必须在ACL2中使用排序的映射/索引结构。目前，我有以下几点：

( (key1 . (val1 val2)) (key2 . (val3)) (key3 . (val4 val5 val6)) )

还有其他更有效的方法吗？

Answer 1

从你的例子来看，我不清楚你想做什么。

当然，您可以在关联列表上定义操作，使其保持按键排序的顺序。在这种情况下：

• 您的get函数看起来就像acons
• 您的put函数需要查找放置元素的“正确”位置。

但这并不是特别有效。这两项行动都是O(n)。另外，作为一个实际考虑，put操作将需要O(n)会话，这是特别昂贵的，因为cons分配内存。

通常情况下，最好只使用普通的关联列表，即使用acons和assoc。主要的优点是，由于它简单地将新的键/值对转换到列表的前面，所以acons是O(1)，所以构造映射通常要便宜得多。如果需要的话，您可以随时对列表中的键进行排序，例如，使用集合:合并或某些自定义排序函数。

访问参与者仍然是O(n)。然而，快速主义者在ACL2(h)中是可用的，本质上提供了一种获得哈希表速度的方法。还请参阅性病/医务人员的文档。