µP T S 语言
您将编写一个 Prolog 程序，该程序将处理来自名为 µP TS 的小型 λ 演算的抽象语法树中的表达式（名称来自于它是一种纯类型(Pure Type System)系统，接近系统 U (System U)）。 µP T S 的特点是混合了正常的表达式和类型。
所以在这种语言中，类型是“正常”值（我们也说“一等值”），可以作为参数传递，作为函数的结果返回，或者存储在数据结构中。表示这一事实的一种方法是说“type:type”；就像 int 是整数的类型一样，type 是类型的类型，所以 42: int 和 int: type，因为 type 本身就是一个类型，所以我们有 type: type。
因此，语言的语法不区分子语言和类型：两者是共同的。更准确地说，该语言的核心具有以下语法，对类型和“正常”表达式都有效：
• c 代表任何预定义的常量，这包括整数、预定义的类型（int、list、type、…）和预定义的操作（cons、nil、+、-、…）；
• x 是对变量的引用；
• λx：e1.e2 是 e1 类型的参数 x 和主体 e2 的函数；
• e1 e2 是对带有当前参数e2 的函数e1 的调用；
• Πx：e1.e2 是一个函数的类型，该函数采用 e1 类型的参数并返回 e2 类型的值。 x的作用域当然是表达式e2，这种形式是对∀x.e2和e1→e2的推广：如果x没有出现在e2中，那么我们可以像语法糖一样用e1→e2写成Πx：e1 .e2 和 Πx：type.e2 等价于多态类型 ∀x.e2。
• let x: e1 = e2 in e3 是类型 e1 和值 e2 的变量 x 的局部声明，其范围是 e2 和 e3（此声明允许递归）。
例如，Haskell identity = λx → x 的恒等函数的类型通常表示为identity :: α → α，这实际上意味着 ∀α.α → α。 在我们的语言中，这被写成 Πα: type.Πx: α.α，这意味着恒等函数实际上接受两个参数，第一个 (α, 类型) 是第二个 (α 类型的 x) 的类型. 因此，调用可能看起来像 identity int 5，它对应于获取函数标识，然后将其专门用于整数情况，最后将参数 5 传递给它。 评估规则是 λ 演算的通常规则：
这些规则对应于单个执行步骤； 因此，只要有必要，它们就会被重复使用，并尽可能应用它们。 预定义的常量有以下类型：
整数并不奇怪，特别是如果我们对 + 和 – 的类型使用 → 表示法：int → int → int。
最有趣的部分是列表：预定义列表的类型为 list t n，其中 t 是每个元素的类型，n 是列表的大小。所以列表类型构造函数接受两个参数（第一个是类型，第二个是整数），结果是一个类型。所以 nil 接受一个参数 t，它是列表元素的类型，并返回一个空列表类型
合适的。在这种情况下，Π用于参数多态，类型可以读取∀t.list t 0。最后，cons有四个参数：列表中元素的类型，要添加的项，长度列表的尾部，列表的尾部，它返回一个相同类型的列表，只是长度增加了1。
在这四个 Π 中，第一个对应于参数多态性，第二个和最后一个对应于正常函数（可以用符号 τ1 → τ2 表示），第三个对应于所谓的依赖类型，其中一个参数是一个值而不是一个类型（在我们的例子中是 n），出现在类型中。
图 1 显示了键入规则。主要判断的形式为表示 e1 在上下文 Γ 中具有类型 e2，Γ 是给出每个已知变量类型的列表。相应的规则必须确保仅当表达式在语法上有效时判断才为真，它只引用现有变量，并且没有打字错误。
第一条规则简单地说，仅引用变量的表达式的类型是与上下文 Γ 中的该变量相关联的表达式，这当然意味着该变量必须存在于 Γ 中。 λ 的类型规则与课程中看到的经典规则相同，除了使用 Πx: e1.e3 而不是 e1 → e3，并且除了它还确保 e1 本身是一个有效的类型表达式。同样，Πx 的类型规则：e1.e2 只是验证 e1 和 e2 都是格式良好的类型。
函数调用的规则有点棘手。通常的规则：
只说：
所以有2个区别：
• 当然，使用Π。
• 替换e5 中的[e2 / x]：这是使用Πx: … 的x 的地方。 如果 x 没有出现在 e5 中（因此 Πx: e4.e5 可以写成 e4 → e5），那么替换没有区别，但是如果 xy 出现了，如 Πt: type.list t 0，那么类型结果当然必须反映已通过的参数
规则表明 e1 和 e2 在两个表达式归约为相同结果的意义上是等价的。 因此，检查这种关系的一种方法是尽可能多地在 e1 和 e2 上应用归约规则，直到我们得到相同的结果或没有更多可归约的结果。 请注意，这里的归约是在非空上下文中完成的，这与经典评估不同：可能存在未实例化的变量。 例如，我们必须能够发现即使 x 和 y 未知。 由于语言是纯粹的，因此评估的顺序无关紧要。 此外，是隐含的，因此例如 λx: t.x 和 λy: t.y 被视为两个相同的表达式。
在提供的代码中，表达式 µP T S 由以下 Prolog 项表示：
工作：：
对于这项工作，您将直接处理 Prolog 中的抽象语法，而无需词法和句法分析器读取外部表示，因为 Prolog 的语法足够灵活，可以接受。
µP T S 语言在实践中有点过于简约和冗长，因此我们希望能够使用它而不必编写所有这些类型。为此，您将实现一个类型推断系统，即类似于用于 Haskell 的系统。但是，由于 µP TS 是一种类型依赖语言，因此类型检查（同时进行推理）要困难得多，例如，它可能需要进行一些评估。
µP TS 的实现将分两部分完成：一部分使用上面介绍的 µP TS（我们称之为内部语言），另一部分使用这种语言的扩展（我们称之为表面语言），为程序员带来各种便利。
到目前为止，提供的代码已经实现了有用的内部语言操作元素：用术语替换变量的 subst 操作、规范化规则等，而不是根据图 1 的规则检查类型。
因此，您的代码将负责处理表面语言的添加内容，例如以下功能：
• 我们可以在局部定义中省略类型注释，并且当 E2 的类型可以轻松推断时只写 let (X, E2, E3)。
• 当 X 不用时，我们可以写 E1 -> E2 而不是 arw (X, E1, E2)
不曾用过。 注意：我们在这里使用 Prolog 的语法糖，它自动解释 E1 -> E2，就像我们写的 -> (E1, E2)。
• 可以添加类型的显式注释，形式为 E1: E2，这意味着 E1 必须具有类型 E2。 在这里，E1: E2 实际上被 Prolog 读取，就好像我们写了：(E1, E2)。
• 如果这个表达式的上下文已经告诉我们它的类型应该是什么，我们可以省略函数形式参数上的类型注释（因此写成 fun (X, E2)）。 例如我们可以使用
因为类型注释已经给了我们 x 的类型。
• 我们可以写X (E)，而不是写函数调用app (X, E)，甚至可以将这种表示法用于柯里化调用中的任意数量的参数。：例如，app(app (app (X , E1), E2), E3) 可以写成 X (E1, E2, E3)。
所以我们可以写 + (E1, E2)，而不是 app (app (+, E1), E2)，即
Prolog 允许我们编写 E1 + E2。
• 我们可以编写一系列局部声明，let (Decls, E)，其中 Decls 是形式为 X = E 的声明列表。此外，部分 X 可以具有形式 带有类型注释的函数调用：
1 隐式参数
除了上面的语法添加之外，表面语言的最大变化是参数可以是隐式的。 为此，我们添加类型 forall (X, E1, E2)（如果可以推断出 E1，我们可以缩写为 forall (X, E2)），它与 arw (X, E1, E2) 相同，只是它表示这个论点是隐含的。 例如，我们可以这样写：
其中 (t -> t) 周围的括号是必需的，否则 Prolog 会认为我们已经编写了 forall ((t, t) -> t)。 在内部语言中，这将对应于：
与 Haskell 自动发现这种多态性（所谓的 let-polymorphism，这是 Hindley-Milner 类型推断的关键元素）不同，在 µPT S 中，程序员可以在它们适用的地方编写 forall。
2 细化
表面语言和内部语言之间的联系是通过将第一种语言转换为第二种语言来建立的，这称为精化，这是一个将语法糖的消除与类型推断相结合的阶段。
这种转换主要是基于表面语言的打字规则。这些显然是基于内部语言的，除了它们是双向的以帮助信息传播。更具体地说，有两个相互递归的规则，每个都没有覆盖
在某些情况下：从 e1 和环境 Γ 中，验证 e1 的类型是否正确并计算其类型 (e2)，而这表明不仅有 e1 和环境 Γ还有它的类型 e2，然后必须验证 e1 的类型是否正确，并且它确实具有类型 e2。
图 2 显示了相关规则。您的工作将是按照这些规则实施详细说明。主要区别在于细化不仅检查类型，还返回表面代码的详细形式，即内部语言的等效版本，具有所有类型注释且没有语法糖。例如，如果表面代码检查必须使用“coercion int_to_bool”规则，则返回的代码应明确调用 int to bool 函数来进行此转换。同样，如果规则“coercion du ∀”允许您推断 nil 不仅具有 forall (t, type, list (t, 0)) 类型而且还有 list (int, 0) 类型，那么我们必须返回应app (nil , int) 显式实例化隐式参数 t 的代码。
为了方便工作，我为您提供的内部语言操作（例如 subst、normalize）实际上接受 forall (X, E1, E2) 形式的条款，并将它们视为等同于 arw (X, E1, E2)。通过这种方式，我们可以在精化期间（forall 和 arw 之间的区别很重要）和之后（区别不再存在）使用相同的类型
3 验证
细化是一个可能很复杂的阶段，它很容易给它添加越来越多的乐趣，所以为了保护自己免受这个阶段的错误，细化的结果被检查。验证，所以类型系统的安全性不依赖于在阐述上。 更准确地说，通过细化返回的内部语言的代码来验证哪个实现了内部语言的类型规则，以验证细化代码e是否正确键入。
这部分代码也提供给您，因此您可以确保您的代码正常工作。