Предсказать время выполнения извлеченного кода Coq для Haskell - PullRequest
Новая
       10

Предсказать время выполнения извлеченного кода Coq для Haskell

0 голосов
/ 22 апреля 2019

У меня есть следующая версия isPrime, написанная (и доказанная) в Coq.

  • Требуется около 30 секунд для Compute (isPrime 330) чтобы закончить на моей машине.
  • Извлеченному коду Haskell требуется около 1 секунды, чтобы убедиться, что 9767 является простым.

Согласно комментарию в этом посте , разница во времени ничего не значит, но мне интересно почему и есть ли другой способ предсказать производительность при извлечении кода 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.

1 Ответ

2 голосов
/ 22 апреля 2019

Ваш код 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

Между тем, на стороне Хаскеля оценка 2 * 2 == 5 происходит путем умножения двух Integers и сравнения их с другим Integer. Это несколько быстрее. ;)

Что удивительно, так это то, что оценка Coq isPrime 330 занимает всего 30 секунд вместо, скажем, 30 лет.

Я не знаю, что сказать о прогнозировании скорости извлеченного кода, за исключением того, что сказать, что примитивные операции над числами Пеано будут значительно ускорены, а другой код, вероятно, будет скромно быстрее, просто потому, что много работы ушло чтобы GHC генерировал быстрый код, а производительность не была в центре внимания разработки Coq.

...