我在Coq中编写(并证明)了以下版本的isPrime
。
30
在我的机器上完成需要大约Compute (isPrime 330)
秒。1
为秒,以验证9767
是素数。根据this post的评论,时间差异毫无意义,但我想知道为什么会这样?还有其他方法可以在提取Coq代码时预测性能吗?毕竟,有时性能确实很重要,一旦你努力证明它是正确的,很难改变Coq源。这是我的Coq代码:
(***********)
(* IMPORTS *)
(***********)
Require Import Coq.Arith.PeanoNat.
(************)
(* helper'' *)
(************)
Fixpoint helper' (p m n : nat) : bool :=
match m with
| 0 => false
| 1 => false
| S m' => (orb ((mult m n) =? p) (helper' p m' n))
end.
(**********)
(* helper *)
(**********)
Fixpoint helper (p m : nat) : bool :=
match m with
| 0 => false
| S m' => (orb ((mult m m) =? p) (orb (helper' p m' m) (helper p m')))
end.
(***********)
(* isPrime *)
(***********)
Fixpoint isPrime (p : nat) : bool :=
match p with
| 0 => false
| 1 => false
| S p' => (negb (helper p p'))
end.
(***********************)
(* Compute isPrime 330 *)
(***********************)
Compute (isPrime 330).
(********************************)
(* Extraction Language: Haskell *)
(********************************)
Extraction Language Haskell.
(***************************)
(* Use Haskell basic types *)
(***************************)
Require Import ExtrHaskellBasic.
(****************************************)
(* Use Haskell support for Nat handling *)
(****************************************)
Require Import ExtrHaskellNatNum.
Extract Inductive Datatypes.nat => "Prelude.Integer" ["0" "succ"]
"(\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))".
(***************************)
(* Extract to Haskell file *)
(***************************)
Extraction "/home/oren/GIT/CoqIt/FOLDER_2_PRESENTATION/FOLDER_2_EXAMPLES/EXAMPLE_03_PrintPrimes_Performance_Haskell.hs" isPrime.
您的Coq代码使用自然的Peano编码。 mult 2 2
的评估字面意思是减少:
mult (S (S 0)) (S (S 0)))
= (S (S 0)) + mult (S 0) (S (S 0)))
= (S (S 0)) + ((S (S 0)) + mult 0 (S (S 0)))
= (S (S 0)) + ((S (S 0)) + 0)
= (S (S 0)) + ((S 0) + (S 0))
= (S (S 0)) + (0 + (S (S 0))
= (S (S 0)) + (S (S 0))
= (S 0) + (S (S (S 0)))
= 0 + (S (S (S (S 0)))
= (S (S (S (S 0))))
然后检查平等mult 2 2 =? 5
进一步减少:
(S (S (S (S 0)))) =? (S (S (S (S (S 0)))))
(S (S (S 0))) =? (S (S (S (S 0))))
(S (S 0)) =? (S (S (S 0)))
(S 0) =? (S (S 0))
0 =? (S 0)
false
同时,在Haskell方面,对2 * 2 == 5
的评估是通过将两个Integers
相乘并将它们与另一个Integer
进行比较来进行的。这有点快。 ;)
令人难以置信的是,Coq对isPrime 330
的评估只需要30秒而不是30年。
我不知道如何预测提取代码的速度,除了说Peano数字的原始操作将大规模加速,而其他代码可能会适度更快,仅仅是因为GHC已经做了很多工作生成快速代码,性能并未成为Coq开发的重点。