Что произойдет, если мы попытаемся извлечь свидетеля, но на самом деле его не существует из термина экзистенциального типа?

12

Учитывая термин t : ∀x.∃y.(¬(x = 0) ⇒ x = S(y))в теории типов Мартина-Лофа, какова ценность того w(t(0)), где wнаходится оператор, извлекающий свидетельство термина экзистенциального типа?

день
источник
Я думаю, что вы имеете в виду . ¬(x=0)
Марк Рейтблатт
Да, Марк, спасибо за указание, исправлено.
день

Ответы:

12

ty.(¬(0=0)0=S(y))y¬(0знак равно0)0знак равноS(Y)¬(0знак равно0)0знак равно00знак равноS(0)0знак равноS(1)...Y

Марк Рейтблатт
источник
10

Чтобы продемонстрировать ответ Марка, рассмотрим следующее доказательство tвашего утверждения, написанное в Coq. В доказательстве мы предполагаем, что задан параметр kтипа nat. Мы используем kв качестве значения yв случае x = 0:

Parameter k : nat.

Theorem t : forall x : nat, { y : nat | x <> 0 -> x = S y}.
Proof.
  induction x.
  exists k; tauto.
  induction x.
  exists 0; auto.
  destruct IHx as [z G].
  exists (S z).
  intro H.
  elim G; auto.
Defined.

Мы можем доказать, что t 0равно k:

Theorem A: projT1 (t 0) = k.
Proof.
  auto.
Qed.

Это protT1есть потому, что t 0это не просто натуральное число, но на самом деле натуральное число с доказательством того, что 0 <> 0 -> 0 = S yи projT1выбрасывает доказательство.

Извлеченный код Ocaml t, полученный с помощью команды Extraction k:

(** val t : nat -> nat **)

let rec t = function
  | O -> k
  | S n0 -> (match n0 with
              | O -> O
              | S n1 -> S (t n0))

Опять же, мы можем видеть, что t 0это равно k, что было условно принятым параметром.

Андрей Бауэр
источник
Спасибо за пример в Coq, Андрей, это уточняет больше.
день