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

Question

我正在阅读Coq的线性逻辑机械化http://www.cs.cmu.edu/~iliano/projects/metaCLF2/inc/dl/papers/lsfa17.pdf和https://github.com/brunofx86/LL我无法term从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):

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

Answer 1

关于你提到的主要问题,语法var (t : T)在定义构造函数只是一些替代(短)语法var : forall t : T, term,它可以一样好被写入var : T -> term(因为没有变量的发生t在term).

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

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.

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

最后,可以注意到,Type它不是指固定类型,而是Type_i指i >=0由Coq内核自动确定和检查索引的给定位置.有关此主题的更多信息,请参阅CPDT的Universes章节的第一部分