1

这个问题是指使用 Isabelle/HOL 定理证明器生成代码。

当我distinct在列表中导出函数的代码时

export_code distinct in Scala file -

我得到以下代码

def member[A : HOL.equal](x0: List[A], y: A): Boolean = (x0, y) match {
  case (Nil, y) => false
  case (x :: xs, y) => HOL.eq[A](x, y) || member[A](xs, y)
}

def distinct[A : HOL.equal](x0: List[A]): Boolean = x0 match {
  case Nil => true
  case x :: xs => ! (member[A](xs, x)) && distinct[A](xs)
}

此代码具有二次运行时。有更快的版本吗？我想"~~/src/HOL/Library/Code_Char"在我的理论开始时导入字符串，并为列表设置有效的代码生成。一个更好的实现distinct是在 O(n log n) 中对列表进行排序并遍历列表一次。但我想一个人可以做得更好吗？

无论如何，是否有更快的实现distinct，也许还有其他Main可用的功能？

4

1 回答 1

7

我不知道 Isabelle2013 的库中是否有任何更快的实现，但您可以自己轻松完成，如下所示：

  1. 实现一个distinct_sorted确定排序列表的独特性的函数。
  2. 证明distinct_sorted确实distinct在排序列表上实现
  3. 证明实现distinct通过distinct_list和排序的引理，并将其声明为distinct.

总之，这看起来如下：

context linorder begin
fun distinct_sorted :: "'a list => bool" where
  "distinct_sorted [] = True"
| "distinct_sorted [x] = True"
| "distinct_sorted (x#y#xs) = (x ~= y & distinct_sorted (y#xs))"

lemma distinct_sorted: "sorted xs ==> distinct_sorted xs = distinct xs"
  by(induct xs rule: distinct_sorted.induct)(auto simp add: sorted_Cons)
end

lemma distinct_sort [code]: "distinct xs = distinct_sorted (sort xs)"
 by(simp add: distinct_sorted)

接下来，您需要一个高效的排序算法。默认情况下，sort使用插入排序。如果从 HOL/Library 导入 Multiset，sort将通过快速排序实现。如果您从形式证明档案中导入高效合并排序，您将获得合并排序。

While this can improve efficiency, there's also a snag: After the above declarations, you can execute distinct only on lists whose elements are instances of the type class linorder. As this refinement happens only inside the code generator, your definitions and theorems in Isabelle are not affected.

For example, to apply distinct to a list of lists in any code equation, you first have to define a linear order on lists: List_lexord in HOL/Library does so by picking the lexicographic order, but this requires a linear order on the elements. If you want to use string, which abbreviates char list, Char_ord defines the usual order on char. If you map characters to the character type of the target language with Code_Char, you also need the adaptation theory Code_Char_ord for the combination with Char_ord.

于 2013-03-21T11:22:38.897 回答