预测提取的Coq代码到Haskell的运行时间 [英] Predict running times of extracted Coq code to Haskell

问题描述

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

I have the following version of isPrime written (and proved) in Coq.

• 在计算机上完成计算（isPrime 330）
  大约需要 30 秒。


• 提取的Haskell代码花费大约 1 秒来验证 9767

• It takes around 30 seconds for Compute (isPrime 330) to finish on my machine.
• The extracted Haskell code takes around 1 second to verify that 9767 is prime.

根据此帖子，
时间差没有任何意义，但我想知道为什么吗？
，提取Coq代码时还有其他方法可以预测性能吗？毕竟，有时候性能很重要，一旦您努力证明Coq的正确性就很难改变Coq的来源。
这是我的Coq代码：

According to a comment in this post, the timing difference means nothing, but I wonder why is that? and is there any other way to predict performance when extracting Coq code? after all, sometimes performance does matter, and it's quite hard to change Coq source once you labored to prove it's correct. Here is my Coq code:

(***********)
(* 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 的评估实际上是通过减少进行的：

Your Coq code is using a Peano encoding of the naturals. The evaluation of mult 2 2 literally proceeds by the reduction:

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 进一步减少的收益：

and then checking the equality mult 2 2 =? 5 proceeds by the further reduction:

(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 的求值方法是将两个 Integer 相乘并将它们与另一个 Integer 。这有点快。;）

Meanwhile, on the Haskell side, the evaluation of 2 * 2 == 5 proceeds by multiplying two Integers and comparing them to another Integer. This is somewhat faster. ;)

在这里令人难以置信的是，Coq对 isPrime 330 的评估只需要30秒，而不是30年。

What's incredible here is that Coq's evaluation of isPrime 330 only takes 30 seconds instead of, say, 30 years.

我不知道如何预测提取的代码的速度，只是说对Peano数字的原始运算将大大加速，而其他代码可能会适度地更快，仅仅是因为要使GHC生成快速代码已经做了很多工作，而性能并不是Coq的开发重点。

I don't know what to say about predicting the speed of extracted code, except to say that primitive operations on Peano numbers will be massively accelerated, and other code will probably be modestly faster, simply because a lot of work has gone into making GHC generate fast code, and performance hasn't been an emphasis in Coq's development.

这篇关于预测提取的Coq代码到Haskell的运行时间的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！