9

The third chapter of CPDT briefly discusses why negative inductive types are forbidden in Coq. If we had

Inductive term : Set :=
| App : term -> term -> term
| Abs : (term -> term) -> term.

then we could easily define a function 

Definition uhoh (t : term) : term :=
  match t with
    | Abs f => f t
    | _ => t
  end.

so that the term uhoh (Abs uhoh) would be non-terminating, with which "we would be able to prove every theorem".

I understand the non-termination part, but I don't get how we can prove anything with it. How would one prove False using term as defined above?

4

1 回答 1

4

阅读你的问题让我意识到我也不太理解亚当的论点。但是这种情况下的不一致很容易由康托尔通常的对角论证（逻辑中的悖论和谜题的永无止境的来源）引起。考虑以下假设：

Section Diag.

Variable T : Type.

Variable test : T -> bool.

Variables x y : T.

Hypothesis xT : test x = true.
Hypothesis yF : test y = false.

Variable g : (T -> T) -> T.
Variable g_inv : T -> (T -> T).

Hypothesis gK : forall f, g_inv (g f) = f.

Definition kaboom (t : T) : T :=
  if test (g_inv t t) then y else x.

Lemma kaboom1 : forall t, kaboom t <> g_inv t t.
Proof.
  intros t H.
  unfold kaboom in H.
  destruct (test (g_inv t t)) eqn:E; congruence.
Qed.

Lemma kaboom2 : False.
Proof.
  assert (H := @kaboom1 (g kaboom)).
  rewrite -> gK in H.
  congruence.
Qed.

End Diag.

这是一个可以用termCPDT 中定义的类型实例化的通用开发：T将是term和x是我们可以测试区分y的两个元素（例如和）。关键点是最后一个假设：我们假设我们有一个可逆函数，在您的示例中，它将是。使用该函数，我们玩了通常的对角化技巧：我们定义一个函数，该函数的构造不同于每个函数，包括它自己。矛盾由此产生。termApp (Abs id) (Abs id)Abs idg : (T -> T) -> TAbskaboomT -> T

于 2015-07-05T12:31:01.167 回答