你如何在 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。）但是，尝试将其适应构造微积分是有问题的，因为 Type 和 Term 是单一类型。这意味着不仅 Context/Term 必须相互递归，而且 Term 必须对其自身进行索引。这是初步尝试：

data Γ : Set

data Term : Γ → Term → Set

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

data Term where
    -- ...

然而，

Agda 抱怨说 Term 不在其初始声明的范围内。是否可以那样表示，或者我们真的需要为 Term 和 Type 设置不同的类型吗？我非常希望在 Agda 中看到 minimal/reference CoC 的实现。

Answer 1

众所周知，这是一个非常难的问题。据我所知，在 Agda 中没有 "minimal" 编码 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 -- 单文件形式化。一如既往，几种数据类型相互定义。 "mimic" 替换操作行为的显式传输的显式替换。

EatEval.agda——我们通过结合前两个形式化的想法得到这个。在这个文件中，我们没有定义多个显式传输，而是只有一个传输，它允许将术语的类型更改为指称相同的类型。 IE。我们没有通过构造函数显式指定替换行为，而是有一个构造函数表示 "if evaluating two types in Agda gives the same results, then you can convert a term of one type to the another one via a constructor".

Type Theory in Type Theory using Quotient Inductive Type, Thorsten Altenkirch, Ambrus Kaposi -- this is the most promising approach I'd say. It "legalizes" computation at the type level via the quotient types device. But we do not yet have quotient types in Agda, they are essentially postulated in the paper. People work a lot on quotient types (there is an entire thesis: Quotient inductive-inductive definitions -- Dijkstra, Gabe)，所以我们可能会在某个时候拥有它们。

Decidability of Conversion for Type Theory in Type Theory, Andreas Abel, Joakim Öhman, Andrea Vezzosi -- untyped terms reified as typed ones. Lots of properties。也有很多元理论证明和一个特别有趣的设备，允许使用相同的逻辑关系证明可靠性和完整性。形式化庞大且评论良好。

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

Abstract. We present details of an Agda formalization of a setoid model of Martin-Löf type theory with Pi, Sigma, extensional identity types, natural numbers and an infinite hiearchy of universe à la Russell. A crucial ingredient is the use of Aczel's type V of iterative sets as an extensional universe of setoids, which allows for a well-behaved interpretation of type equality.

Coq in Coq, Bruno Barras and Benjamin Werner -- a formalization of CC in Coq (the code)。无类型术语具体化为类型术语 + 大量引理 + 元理论证明。

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

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

How do you represent terms of the CoC in Agda?

agda