您如何在 Agda 中表示 CoC 的条款？

Question

例如，在 Agda 中的 STLC 可以这样表示：

data Type : Set where
*   : Type
_⇒_ : (S T : Type) → Type

data Context : Set where
ε   : Context
_,_ : (Γ : Context) (S : Type) → Context

data _∋_ : Context → Type → Set where
here  : ∀ {Γ S} → (Γ , S) ∋ S
there : ∀ {Γ S T} (i : Γ ∋ S) → (Γ , T) ∋ S

data Term : Context → Type → Set where
var : ∀ {Γ S} (v : Γ ∋ S) → Term Γ S
lam : ∀ {Γ S T} (t : Term (Γ , S) T) → Term Γ (S ⇒ T)
app : ∀ {Γ S T} (f : Term Γ (S ⇒ T)) (x : Term Γ S) → Term Γ T

（来自here。）但是，试图将其适应于构造微积分是有问题的，因为类型和术语是单一类型。这意味着不仅 Context/Term 必须相互递归，而且 Term 必须在自身上建立索引。这是一个初步的尝试：

data Γ : Set

data Term : Γ → Term → Set

data Γ where
  ε   : Γ
  _,_ : (ty : Term) (ctx : Γ) → Γ
infixr 5 _,_

data Term where
    -- ...

不过，Agda 抱怨 Term 不在其初始声明的范围内。是否有可能以这种方式表示，或者我们真的需要为 Term 和 Type 设置不同的类型？我非常希望在 Agda 中看到 CoC 的最小/参考实现。

Answer 1

众所周知，这是一个非常困难的问题。据我所知，在 Agda 中编码 CoC 没有“最小”的方式。你必须要么证明很多东西，要么使用浅编码，要么使用繁重的（但非常明智的）技术，比如商归纳，或者首先定义无类型的术语，然后将它们具体化为有类型的术语。以下是一些相关文献：

Functional Program Correctness Through Types, Nils Anders Danielsson -- 本文的最后一章是对依赖类型语言的形式化。这是大量引理式的形式化，还包含一些无类型的术语。

Type checking and normalisation, James Chapman -- 本文的第五章是依赖类型语言的形式化。它也是大量引理式的形式化，除了许多引理只是相应数据类型的构造函数。例如，您可以将显式替换作为构造函数而不是计算函数（之前的论文没有针对类型的替换，仅针对术语，而本论文甚至对类型也有显式替换）。

Outrageous but Meaningful Coincidences. Dependent type-safe syntax and evaluation，Conor McBride——本文提出了一种依赖类型理论的深度编码，它具体化了该理论的浅层编码。这意味着作者没有定义替换和证明它的属性，而是使用 Agda 的评估模型，但还提供了目标语言的完整语法。

Typed Syntactic Meta-programming、Dominique Devriese、Frank Piessens -- 将非类型化术语具体化为类型化术语。当我研究 IIRC 时，代码中有很多假设，因为这是一个元编程框架而不是形式化。

Type theory eating itself?, Chuangjie Xu & Martin Escardo -- 单一文件形式化。与往常一样，几种数据类型相互定义。使用“模仿”替换操作行为的显式传输进行显式替换。

EatEval.agda——我们通过结合前两个形式化的想法得到这个。在这个文件中，我们没有定义多个显式传输，而是只有一个传输，它允许将术语的类型更改为在表示上相等的类型。 IE。我们没有通过构造函数显式指定替换行为，而是有一个构造函数，它说“如果在 Agda 中评估两种类型给出相同的结果，那么您可以通过构造函数将一种类型的术语转换为另一种类型”。

Type Theory in Type Theory using Quotient Inductive Type，Thorsten Altenkirch，Ambrus Kaposi——这是我想说的最有希望的方法。它通过商类型设备在类型级别“合法化”计算。但是我们在 Agda 中还没有商类型，它们基本上是在论文中假设的。不过，人们在商类型上做了很多工作（有一个完整的论文：Quotient inductive-inductive definitions -- Dijkstra, Gabe），所以我们可能会在某个时候拥有它们。

Decidability of Conversion for Type Theory in Type Theory、Andreas Abel、Joakim Öhman、Andrea Vezzosi -- untyped terms 具体化为 typed ones。 Lots of properties。也有很多元理论证明和一个特别有趣的设备，允许使用相同的逻辑关系证明可靠性和完整性。形式化是巨大的，并且得到了很好的评论。

Agda (zip file with the development) 中的外延 Martin-Löf 类型理论的 setoid 模型，Erik Palmgren -- 摘要：

抽象。我们展示了 setoid 的 Agda 形式化的细节 具有 Pi、Sigma、外延恒等式的 Martin-Löf 类型理论模型 类型、自然数和无限的宇宙等级 拉塞尔。一个关键成分是使用 Aczel 的 V 型 迭代集作为 setoids 的外延宇宙，它允许 对类型相等的良好解释。

Coq in Coq、Bruno Barras 和 Benjamin Werner - Coq 中 CC 的形式化 (the code)。无类型术语具体化为类型 + 大量引理 + 元理论证明。

感谢 András Kovács 和 James Chapman 的建议。