如何理解Coq类型构造函数var(t:T)

问题描述：

我正在阅读Coq中的线性逻辑机械化 https://github.com/brunofx86/LL ，我很难理解

I am reading about mechanization of linear logic in Coq http://www.cs.cmu.edu/~iliano/projects/metaCLF2/inc/dl/papers/lsfa17.pdf and https://github.com/brunofx86/LL and I have trouble to understand the type constructors of the inductive type term from https://github.com/brunofx86/LL/blob/master/FOLL/LL/SyntaxLL.v:

Inductive term  :=
    |var (t: T) (* variables *)
    |cte (e:A) (* constants from the domain DT.A *)
    |fc1 (n:nat) (t: term) (* family of functions of 1 argument *)
    |fc2 (n:nat) (t1 t2: term). (* family of functions of 2 argument *)

关于此示例，我有两个问题(我正在阅读 https://本文中的softwarefoundations.cis.upenn.edu/lf-current/Basics.html ):

I have two question regarding this sample (I am reading https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html along this paper):

term的(超级)类型是什么? Software Foundations始终指定新类型的(超级)类型，例如Inductive color : Type;
主要问题-如何理解类型构造函数var (t: T)?. Software Foundation在其第一章中仅提供了两种类型的类型构造函数:常量white : color和函数primary : rgb → color.但是var (t: T)是一个非常奇怪的符号-它不是有效的函数类型定义，因为它没有显式的返回类型，也没有箭头.

what is the (super)type of term? Software Foundations always specifies the (super)type of the new type, like Inductive color : Type;
the main question - how to understand type constructor var (t: T)?. Software Foundation in its first chapter provides only two types of type constructors: constant white : color and function primary : rgb → color. But var (t: T) is very strange notation - it is not valid function type definition as it have no explicit return type and also it has no arrow.

答

关于您的主要问题，定义构造函数时的语法var (t : T)只是var : forall t : T, term的另一种(较短的)语法，写入var : T -> term(因为在term中没有出现变量t).

Regarding your main question, the syntax var (t : T) when defining a constructor is just some alternative (shorter) syntax for var : forall t : T, term, which can just as well be written var : T -> term (since there is no occurrence of variable t in term).

实际上，您可以通过处理定义然后检查以下命令来进行检查:

Actually, you can check this by processing the definition, then the following command:

Print term.

(* and Coq displays the inductive type with the default syntax, that is:

  Inductive term : Type :=
    var : T -> term
  | cte : A -> term
  | fc1 : nat -> term -> term
  | fc2 : nat -> term -> term -> term
*)

下一步(如上面的Coq输出所示)，数据类型term的类型的确是Type.

Next (as shown by the Coq output above), the type of the datatype term is indeed Type.

我记得在Coq中，所有类型也都有一个类型，并且后者始终是Prop，Set或Type.通常将类型的类型"称为排序. (排序Prop处理逻辑命题，而排序Set和Type处理所谓的信息性"类型.)

I recall that in Coq, all types have also a type, and this latter will always be Prop, Set or Type. A "type of type" is usually called a sort. (The sort Prop deals with logical propositions while the sorts Set and Type deal with so-called "informative" types.)

最后，可以注意到，Type不是指固定类型，而是指给定的Type_i，其中索引i >=0是由Coq的内核自动确定和检查的.有关此主题的更多信息，请参见例如CPDT 宇宙"一章的第一部分

Finally, it can be noted that Type does not refer to a fixed type, but to a given Type_i where the index i >=0 is automatically determined and checked by Coq's kernel. For more information on this topic, see for example the first section of the Universes chapter of CPDT

如何理解Coq类型构造函数var(t:T)

相关推荐