预测提取的 Coq 代码到 Haskell 的运行时间

Question

我有以下版本的isPrime 用 Coq 编写（并证明）。

• Compute (isPrime 330) 大约需要 30 秒 在我的机器上完成。
• 提取的 Haskell 代码大约需要 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.

Answer 1

您的 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 开发的重点。