Извлечение Prop из Coq в Haskell приводит к пустому типу - PullRequest
Новая
       17

Извлечение Prop из Coq в Haskell приводит к пустому типу

1 голос
/ 25 апреля 2019

Я пытаюсь убедиться, что бесполезный Prop отбрасывается при извлечении Coq в Haskell .Однако, когда я использую следующий пример, я вижу, что и divides, и prime извлекаются как пустые типы Haskell.Почему это так? 

(***********)
(* isPrime *)
(***********)
Fixpoint isPrime (p : nat) : bool :=
  match p with
  | 0 => false
  | 1 => false
  | S p' => (negb (helper p p'))
  end.

(***********)
(* divides *)
(***********)
Definition divides (n p : nat) : Prop :=
  exists (m : nat), ((mult m n) = p).

(*********)
(* prime *)
(*********)
Definition prime (p : nat) : Prop :=
  (p > 1) /\ (forall (n : nat), ((divides n p) -> ((n = 1) \/ (n = p)))).

(***************************)
(* Extract to Haskell file *)
(***************************)
Extraction "/home/oren/some_file.hs" isPrime divides prime.

А вот что происходит с divides и prime: 

type Divides = ()

type Prime = ()

Какая польза от их извлечения?

1 Ответ

5 голосов
/ 25 апреля 2019

Это ожидаемое поведение. Вещи из Prop являются суждениями, означающими, что они не имеют отношения к вычислениям, потому что существуют суждения для обеспечения правильности, например, представлять предварительные и последующие условия алгоритма, не участвовать в вычислениях.

Ситуация аналогична ситуации типов в статически типизированных языках - обычно требуется стереть типы из среды выполнения. Здесь мы хотели бы, чтобы термины, которые являются доказательствами, тоже были стерты.

Это поддерживается системой типов Coq, которая запрещает утечку логической информации из типов от Prop до Type, например, 

Definition foo : True \/ True -> nat :=
  fun t => match t with
        | or_introl _ => 0
        | or_intror _ => 42
        end.

Результаты в 

Error:
Incorrect elimination of "t" in the inductive type "or":
the return type has sort "Set" while it should be "Prop".
Elimination of an inductive object of sort Prop
is not allowed on a predicate in sort Set
because proofs can be eliminated only to build proofs.

Возникает естественный вопрос:

Так что в идеале divides и prime должны быть полностью удалены из извлеченного файла, верно? Как они там существуют?

Как объясняет Пьер Летузи в своем обзоре извлечения в Coq :

Подведем итоги текущего состояния извлечения Coq. Теоретическая функция извлечения, описанная в [7], все еще актуальна и используется в качестве ядра системы извлечения. Эта функция сворачивается (но не может полностью удалить ) как логических частей (живущих в сортировке Prop), так и типов. Полное удаление может привести к опасным изменениям в оценке терминов и даже может привести к ошибкам или не прекращению в некоторых ситуациях.

...