6

从 Coq 中提取的 Ocaml 代码包括（在某些情况下）一个类型__和一个函数__，定义如下：

type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f

文档说，在过去，这种类型被定义为unit（因此__可以被视为()），但存在（罕见）将 type__的值应用于 type 的值的情况__。

__使用来自 OCaml 的模块的未记录函数Obj，但似乎定义的本质上是一个完全多态的函数，它吃掉它的所有参数（无论它们的数量是多少）。

是否有一些关于__无法消除的情况以及这种类型的值应用于相同类型的值的文档，无论是从理论（构造 Coq 术语，其中不可能消除）和实际情况（显示发生这种情况的实际情况） 观点看法？

4

1 回答 1

3

自述文件中引用的参考资料很好地概述了擦除问题。具体而言，本报告和本文都详细解释了 CIC 术语的类型方案和逻辑部分是如何被删除的，以及为什么必须有__ x = __. 问题不完全是__可能适用于它自己，而是它可能适用于任何事物。

不幸的是，在任何非病理情况下，这种行为是否重要还不清楚。给出的动机是能够提取任何Coq 术语，并且文档没有提到从实际角度来看真正有趣的任何案例。3上给出的例子是这个：

Definition foo (X : Type) (f : nat -> X) (g : X -> nat) := g (f 0).
Definition bar := foo True (fun _ => I).

执行Recursive Extraction bar.给出以下结果：

type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f

type nat =
| O
| S of nat

(** val foo : (nat -> 'a1) -> ('a1 -> nat) -> nat **)

let foo f g =
  g (f O)

(** val bar : (__ -> nat) -> nat **)

let bar =
  foo (Obj.magic __)

由于foo在 上是多态的Type，因此无法在其主体上简化f O应用程序，因为它可能具有计算内容。但是，因为Prop是 的子类型Type，foo也可以应用于True，这就是 中发生的情况bar。因此，当我们尝试减少bar时，我们将__被应用于O。

这种特殊情况不是很有趣，因为可以完全内联foo：

let bar g =
  g __

由于True不能应用于任何东西，如果g对应于任何合法的 Coq 术语，它的__论点也不会应用于任何东西，因此它是安全的__ = ()（我相信）。但是，有时无法预先知道是否可以进一步应用已删除的术语，这使得一般定义是__必要的。例如，在文件末尾附近查看Fun示例here 。

于 2013-04-07T21:13:58.817 回答