sml - 在Why3ML 中输入 lambda 的正确方法是什么？

Question

我想用 lambda 验证一个函数。例如：

  let map (t : array int) (f : array int -> array int) : array int =
    f t

但是，这会产生错误：

文件“map_reduce.mlw”，第 25 行，字符 4-7：此应用程序使用可变类型数组 int 实例化纯类型变量 'b

是否可以在Why3 中使用 lambda 函数？输入这些 lambda 函数的正确方法是什么？

Answer 1

Why3 中的 Lambda 函数是纯函数。特别是，它们的类型不能包含任何可变区域。这就是您的定义被拒绝的原因。替换array为没有区域的类型，例如 ，set可以正常工作：

use set.Set
let map (t : set int) (f : set int -> set int) : set int = f t