HowdoyourepresenttermsoftheCoCinAgda?

Representing, for example, the STLC in Agda can be done as:

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

(From here.) Trying to adapt this to the Calculus of Constructions, though, is problematic, because Type and Term are a single type. This means not only Context/Term must be mutually recursive, but also that Term must be indexed on itself. Here is an initial attempt:

data ? : Set

data Term : ? ? Term ? Set

data ? where
  ?   : ?
  _,_ : (ty : Term) (ctx : ?) ? ?
infixr 5 _,_

data Term where
    -- ...

Agda, though, complains that Term isn't in scope on its initial declaration. Is it possible to represent it that way, or do we really need to have different types for Term and Type? I'd highly like to see a minimal/reference implementation of CoC in Agda.

众所周知这是一个非常困难的问题。据我所知，在Agda中还没有“最小”的方式来编码CoC。您必须证明很多东西，或者使用浅层编码，或者使用诸如商数归纳之类的沉重（但完全明智）的技术，或者先定义未键入的术语，然后将它们分类为键入的术语。以下是一些相关文献：

Nils Anders Danielsson，《通过类型的功能程序正确性》，本论文的最后一章是对依赖类型语言的形式化。这是大量的引子形式的形式化，并且还包含一些未键入的术语。

类型检查和规范化，詹姆斯·查普曼（James Chapman）-本论文的第五章是依赖类型语言的形式化。这也是一种引理形式的形式化，除了许多引理只是对应数据类型的构造函数。例如，您可以将显式替换用作构造函数，而不是用作计算函数（先前的论文没有针对类型的替换，仅针对术语，而本论文甚至针对类型也具有明确的替换）。

令人发指，但有意义的巧合。从属类型安全的语法和评估，Conor McBride －本文提出了从属类型理论的深层编码，以简化该理论的浅层编码。这意味着作者仅使用Agda的评估模型，而不是定义替代和证明属性，而是提供了目标语言的完整语法。

类型化语法元编程，Dominique Devriese，Frank Piessens-未类型化的术语被化为类型化的术语。当我查看IIRC时，代码中有很多假设，因为这是元编程的框架而不是形式化的框架。

类型理论在吃东西吗？，徐创杰（Chuangjie Xu）和马丁·埃斯卡多（Martin Escardo）-单一文件格式。与往常一样，几种数据类型是相互定义的。使用显式传输的显式替换“模仿”替换操作的行为。

EatEval.agda-我们通过结合前两种形式化的思想来实现这一点。在此文件中，我们没有定义多个显式传输，而只有一个传输，它可以将术语的类型更改为符号上相等的术语。即，我们没有通过构造函数明确指定替换的行为，而是有一个单独的构造函数，它表示“如果在Agda中评估两种类型给出相同的结果，则可以通过构造函数将一种类型的术语转换为另一种类型的术语”。

使用商归纳类型的类型理论中的类型理论，Thorsten Altenkirch，Ambrus Kaposi-这是我要说的最有前途的方法。它通过商类型设备在类型级别“合法化”计算。但是我们在Agda中还没有商类型，它们在本文中已基本假定。人们在商类型上做了大量工作（有一个完整的论点：商归纳-归纳定义 -Dijkstra，Gabe），所以我们可能会在某个时候使用它们。

类型理论中类型理论转换的可判定性，Andreas Abel，JoakimÖhman，Andrea Vezzosi-未类型化的术语被归类为类型化的术语。很多属性。还具有大量的元理论证明和一个特别有趣的设备，该设备允许使用相同的逻辑关系来证明健全性和完整性。形式化是巨大的，并得到了很好的评论。

艾格达（开发中的zip文件）中的扩展Martin-Löf类型理论的setoid模型，Erik Palmgren-摘要：

抽象。我们介绍了马丁·洛夫类型理论的类固醇模型的阿格达形式化的详细信息，该模型具有Pi，Sigma，可扩展身份类型，自然数和无限大的拉塞尔的宇宙。一个关键因素是使用Aczel的V型迭代集作为setoid的可扩展范围，从而可以很好地解释类型相等。

Coq中的Coq，Bruno Barras和Benjamin Werner-Coq中CC的正式形式（代码）。未分类的术语被归类为类型+大量引理+元理论证明。

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