indexing - ACL2 中的排序映射

Question

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

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

有没有其他方法可以更有效地做到这一点？

Answer 1

从您的示例中，我不清楚您要做什么。

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

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

但这并不是特别有效。这两个操作都是 O(n)。此外，作为实际考虑，该put操作将需要 O(n) 个 conses，这特别昂贵，因为cons分配了内存。

通常最好只使用普通的关联列表，即使用aconsand assoc。主要优点是，因为它只是简单地将新的键/值对放在列表的前面，acons是 O(1)，所以构建映射通常要便宜得多。如果需要，您始终可以对 alist 的键进行排序，例如，使用set::mergesort或一些自定义排序功能。

访问 alists 仍然是 O(n)。但是， ACL2(h) 中提供了快速列表，并且本质上提供了一种以哈希表速度获取列表的方法。另请参阅std/alists的文档。