agda - 您如何在 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 中看到 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 中外延 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 和 Benjamin Werner - Coq 中 CC 的形式化 (the code)。无类型术语具体化为类型术语 + 大量引理 + 元理论证明。

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