1

如何检查 FStar 中的两个集合是否相等？以下表达式的类型Type0不是Tot Prims.bool所以我不确定如何使用它来确定集合是否相等（例如在条件中）。是否应该使用不同的功能来代替Set.equal？

Set.equal (Set.as_set [1; 2; 3]) Set.empty
4

1 回答 1

3

中定义的集合FStar.Set使用函数作为表示。因此，s例如一组整数，只不过是一个将整数映射到布尔值的函数。例如，该集合{1, 2}表示为以下函数：

// {1, 2}
fun x -> if x = 1 then true
         else (
            if x = 2 then true
            else false 
         )

您可以添加/删除值（即制作一个新的 lambda），或要求一个值作为成员（即应用函数）。

但是，在比较两组 typeT时，您就不走运了：fors1和s2两组，s1 = s2意味着对于任何值x : T, s1 x = s2 x。当 的T居民集是无限的时，这是不可计算的。

解决方法 函数表示不适合您。您应该有一个表示其比较是可计算的。FStar.OrdSet.fst将集合定义为列表：您应该改用那个集合。

请注意，此OrdSet模块需要对集合中保存的值进行总排序。（如果你想要一组无序的值，我不久前就实现了，但它有点 hacky ......）

于 2019-11-19T11:19:35.247 回答