Isabelle:将"sqrt"导出到Haskell

Question

免责声明:我是伊莎贝尔的初学者.

我正在尝试使用"sqrt"将"sqrt"函数或函数和定义导出到Haskell.我的第一次尝试只是:

theory Scratch
   imports Complex_Main
begin
   definition val :: "real" where "val = sqrt 4"

   export_code val in Haskell 
end 

这导致以下错误:

Wellsortedness error
(in code equation root ?n ?x ?
              if equal_nat_inst.equal_nat ?n zero_nat_inst.zero_nat then zero_real_inst.zero_real
              else the_inv_into top_set_inst.top_set
                    (?y. times_real_inst.times_real (sgn_real_inst.sgn_real y)
                           (abs_real_inst.abs_real y ^ ?n))
                    ?x,
with dependency "val" -> "sqrt" -> "root"):
Type real not of sort {enum,equal}
No type arity real :: enum

所以我试图用Haskell的"Prelude.sqrt"替换"sqrt":

code_printing
  constant sqrt ? (Haskell) "Prelude.sqrt _"

export_code val in Haskell 

这仍然导致了同样的错误.这对我来说似乎很奇怪,因为用一些任意函数"f"替换"plus"似乎没问题:

definition val' :: "nat" where "val' = plus 49 1"

code_printing
  constant plus ? (Haskell) "_ `f` _" 

export_code val' in Haskell 

我该如何解决这个问题？

Answer 1

我不确定这个code_printing问题,但你期望在这里发生什么？Wellsortedness error代码生成期间通常意味着您尝试导出的内容根本不可计算(或者至少Isabelle不知道如何).

你期望sqrt 2在Haskell中编译什么？怎么样sqrt pi？您不能希望为所有实数生成可执行代码.Isabelle的默认实现将自己局限于有理数.

使用代码打印将Isabelle替换sqrt为Haskell sqrt只会给你一个类型错误,因为Haskell的sqrt工作在浮点数上,而不是在Isabelle的导出real类型上.

有一个文件~~/src/HOL/Library/Code_Real_Approx_By_Float将Isabelle对实数的操作映射到标准ML和OCaml中的浮点近似值,但这仅用于实验,因为如果你做那种事情就会失去所有正确性保证.

最后,在Formal Proofs存档中有一个条目提供精确的可执行代数实数,因此您至少可以使用平方根等进行一些操作,但这是一项很大的工作,性能可能非常差在某些情况下.

在Isabelle中也有一个自然数的sqrt运算(即它向下舍入),并且可以很容易地输出到Haskell.~~/src/HOL/Library/Discrete