1

我从 Isabelle/HOL 理论手册中阅读了代码生成。不过，我还是觉得有点失落。我在哪里需要类似的东西linorder？我如何使用例如红黑树来加快速度？locale在程序细化的上下文中如何使用？...

是否有一些教程可以开始细化？如果没有，是否有一些简短的、独立的、正确的示例？

我们可以开发一个例子吗？

让我们假设我们有A :: 'a set并且我们知道finite A。我们如何继续生成例如有效的代码a ∈ A？

我们如何表达我们对finite A. 我们如何才能将数学理论（a ∈ A）与代码生成和优化分开？

4

1 回答 1

1

好的，我会尽力回答这个问题。请随时评论和编辑以改进它。如果您想要因果报应，您也可以复制此答案并重新发布（如果您的答案更好，我将删除我的答案）。

这个用户指南帮助我开始。

好的，让我们假设我们的理论在locale MyLocale.

locale MyLocale =
  fixes A :: "'a set"
  begin
    definition isInA :: "'a => bool" where
      "isInA a ⟷ a ∈ A"
  end

假设我们通过 aisInA实现语言环境来实现该功能。然后，我们可以生成代码并显示其正确性set Alist

definition code_isInA_list :: "'a list => 'a => bool"
  where "code_isInA_list Al a ⟷ a ∈ set Al"

lemma code_isInA_list_correct: 
 "code_isInA_list Al a = MyLocale.isInA (set Al) a"
  by(simp add: MyLocale.isInA_def code_isInA_list_def)

export_code code_isInA_list in Scala file -

这基本上会产生以下 Scala 代码

def code_isInA_list[A : HOL.equal](al: List[A], a: A): Boolean =
  Lista.member[A](al, a)

这些Lista.member函数是线性时间算法。我们能做得更好吗？

假设我们linorder的 type 上有一个'a。例如，我们有linorder自然数、字符串、列表、元组……我们通过写作'a ::linorder而不是 来表达这个假设'a。可以利用该linorder属性的一种数据类型是红黑树。在我们的语言环境中，A是一个set. 在集合中，元素的顺序无关紧要。所以我们可以使用更高效的红黑树来代替列表。红黑树比列表更有效，因为元素可以任意排序，而列表规定了固定的顺序。为了使用红黑树，我们从形式证明档案中导入 Collections 框架。在 thy 文件的开头，我们添加到该imports部分

"./isabelle_afp/Collections/Collections"

现在我们可以实现一个红黑树（rs）版本并显示它的正确性。Collections 框架中的函数rs_α（alpha<tab>在 jEdit 中键入 alpha）将红黑树映射到其对应的集合。

definition code_isInA_rs :: "('a ::linorder) rs => 'a => bool"
  where "code_isInA_rs Al a ⟷ rs_memb a Al"

lemma code_isInA_rs_correct: 
 "code_isInA_rs Ars a = MyLocale.isInA (rs_α Ars) a"
  by(simp add: MyLocale.isInA_def code_isInA_rs_def rs_correct)

export_code code_isInA_rs in Scala file -

我们产生以下代码

def code_isInA_rs[A : Orderings.linorder](al: RBT.rbt[A, Unit], a: A): Boolean =
  RBTSetImpl.rs_memb[A].apply(a).apply(al)

该rs_memb函数具有对数运行时间。托多：真的吗？我在哪里可以查到？

让我们进一步改进我们的代码。假设我们要坚持使用该code_isInA_list版本，因为在我们的代码中列表对我们来说更容易。我们可以code_isInA_list根据code_isInA_rs. 因此，我们使用list_to_rs它将列表转换为红黑树。通过该[code]属性，我们告诉代码生成器使用新版本。

lemma [code]: "code_isInA_list Al a ⟷ code_isInA_rs (list_to_rs Al) a"
  by(simp add: code_isInA_list_def code_isInA_rs_def rs_correct)

export_code code_isInA_list in Scala file -

我们产生以下代码。

def code_isInA_list[A : Orderings.linorder](al: List[A], a: A): Boolean =
  code_isInA_rs[A](RBTSetImpl.list_to_rs[A].apply(al), a)

我想创建一个红黑然后在其中进行查找比简单的列表版本更昂贵，但这只是一个例子。如果我们需要更多的查找，红黑树版本肯定会更高效。

让我们用一些类型来测试 Isabelle jEdit 中的代码。我们从自然数开始。

value[code] "code_isInA_list [(1::nat), 3, 7, 4] 4"

这导致True

接下来，我们尝试字符串。

value[code] "code_isInA_list [''a'', ''b'', ''xyz''] ''b''"

这导致

Wellsortedness error:
  Type char list not of sort linorder
  No type arity list :: linorder

错误消息告诉我们没有linorder在string类型上定义。所以我们引入以下理论。

"~~/src/HOL/Library/List_lexord"
"~~/src/HOL/Library/Code_Char"
"~~/src/HOL/Library/Code_Char_chr"
"~~/src/HOL/Library/Code_Char_ord"

现在我们得到了想要的结果True。该代码甚至适用于元组。

value[code] "code_isInA_list [(''a'', ''a''), (''b'', ''c''), (''xyz'', '''')] (''b'', ''c'')"
于 2013-03-27T19:20:40.807 回答