关于“依赖类型 lambda 演算的教程实现”的问题

Question

我有一点技术上的困难 这 很棒的教程。在第 5 页，教程讨论了简单类型 Lambda 的类型规则，并提出了可通过图 3 中的规则导出的以下判断。

我无法证明两者 id 也不 const 出于同样的原因。以 id 例子。

• 假设我正在查看类型检查规则 CHK. 。它说，为了 check types 我应该首先进行推理，然后将结果与我的预期进行比较。
• 为了对应用程序进行推理，我必须使用 APP 规则立即迫使我推断应用程序左侧的类型，即 (id :: α -> α)
• 为此，我正在使用 ANN 迫使我检查的规则 α -> α 是一种类型（我可以证明它没有问题）。然后我就赤身裸体了 id 符号并且必须证明它的类型是 α -> α.
• 最后，这里有一个问题。为了做到这一点，我将不得不使用 var 规则，这需要类型 id 明确地在上下文 Gamma 中设置，但它没有完成，因此证明失败了。

Answer 1

$\mathsf{id}$ 和 $\mathsf{常量}$ 不是微积分的变量，而是语法糖 $\lambda x ightarrow x$ 和 $\lambda x ightarrow \lambda y ightarrow x$ 分别。这在第 2.2 节末尾进行了说明，并通过使用无衬线字体而不是斜体巧妙地传达了这一点（这是此特定文档的印刷约定，而不是通用约定）。

例如类型判断$$ alpha ::\ast, y::\alpha \vdash (\mathsf{id}::\alpha ightarrow \alpha) \:y::rightarrow alpha $$也是类型判断$$ alpha ::\ast, y::\alpha \vdash (\lambda x ightarrow x ::\alpha ightarrow \alpha) \:y::rightarrow alpha。$$这是同一数学对象的不同表示法。