如何在 SML 中编写此函数答案

【问题标题】：How do I write this function in SML如何在 SML 中编写此函数
【发布时间】：2014-02-03 05:46:56
【问题描述】：

我正在尝试在 Isabelle 中为作业中的某些任务编写一个函数我想确保我的功能正常工作所以我想在 SML 中对其进行测试，但我似乎无法弄清楚如何编写它。我从未使用/编写/学习过函数式编程，所以我遇到了一些麻烦用它。有人可以帮助我吗，或者 Isabelle 是否有关于测试的内容一个函数是如何工作的，他能给我指出正确的方向吗？

函数如下，基本上是删除第一次出现的列表中的元素并从列表中删除所有匹配项

fun del1:: "'a ⇒ 'a list ⇒ 'a list" where
  "del1 a Nil = Nil" |
  "del1 a (x#xs) = (if x = a then xs else x#(del1 a xs))"


fun delall:: "'a ⇒ 'a list ⇒ 'a list" where
  "delall a Nil = Nil" |
  "delall a (x#xs) = (if x = a then (delall a xs) else x#(delall a xs))"

【问题讨论】：

标签： functional-programming sml isabelle

【解决方案1】：

我不太确定我是否明白你的问题。首先，Isabelle/HOL 和 SML 的语法并没有非常不同。如果您只想在 SML 中获取函数的变体，可能最快的方法是使用 Isabelle 的代码生成器

export_code del1 delall in SML

这会导致类似

fun del1 A_ a [] = []
  | del1 A_ a (x :: xs) = (if HOL.eq A_ x a then xs else x :: del1 A_ a xs);

fun delall A_ a [] = []
  | delall A_ a (x :: xs) =
    (if HOL.eq A_ x a then delall A_ a xs else x :: delall A_ a xs);

但是，由于其中包含一些 Isabelle 特定的内容（例如用于摆脱类型类的字典构造），您可能更喜欢手写代码：

fun del1 a [] = []
  | del1 a (x::xs) = if x = a then xs else x :: (del1 a xs)

fun delall a [] = []
  | delall a (x::xs) = if x = a then delall a xs else x :: delall a xs

另一方面，如果您只是想在某些输入上尝试您的函数，您可以在 Isabelle 内部使用 value 进行操作。例如，

value "del1 (2::nat) [1, 2 , 3]"
value "delall ''x'' [''x'', ''y'', ''z'', ''q'', ''x'']"

【讨论】：

实际上所有这些都是我正在寻找的，但尤其是第二个，所以我可以理解我做错了什么......

【解决方案2】：

克里斯的回答几乎没有什么可补充的，只有这个细节：在 Isabelle2013-2 中，Isabelle/jEdit 文档面板有一些快速入门示例。这包括src/HOL/ex/ML.thy，它显示了一点 Isabelle/HOL 作为逻辑语言和 SML 作为功能语言，以及它们之间的一些联系。

【讨论】：