我发誓曾经有一件 T 恤出售，上面写着不朽的话：

什么部分

你不明白吗？

就我而言，答案就是...... 全部！

特别是，我经常在 Haskell 论文中看到这样的符号，但我不知道它的含义是什么。我不知道它应该是什么样的数学分支。

我当然认识到希腊字母的字母，以及诸如 “∉” 之类的符号（通常意味着某些东西不是一组的元素）。

另一方面，我以前从未见过 “⊢”（ 维基百科称它可能意味着 “分区” ）。我也不熟悉这里使用的 vinculum。 （通常它表示一小部分，但不会出现在这里是这种情况。）

如果有人至少可以告诉我从哪里开始想要理解这个符号海洋的含义，那将会有所帮助。

• 水平条表示 “[以上] 暗示 [下方]”。
• 如果在 [以上] 的多个表达式 ，并考虑它们一起相与 ; 所有 [上述] 必须为真以保证 [下方]。
• :表示有类型
• ∈意思是在 。 （同样∉表示 “不在”。）
• Γ通常用于指代环境或上下文; 在这种情况下，它可以被认为是一组类型注释，将标识符与其类型配对。因此x : σ ∈ Γ意味着环境Γ包括x具有类型σ的事实。
• ⊢可以作为证明或确定。 Γ ⊢ x : σ表示环境Γ确定x具有类型σ 。
• ,是包括具体的附加假设到环境中的一种方式Γ 。
  因此， Γ, x : τ ⊢ e : τ'意味着环境Γ ， 以及x具有类型τ的附加的超越假设 ，证明e具有类型τ' 。

根据要求：运营商优先级，从最高到最低：

• 特定于语言的中缀和 mixfix 运算符，例如λx λ x . e ， ∀ α . σ ，和τ → τ' ， let x = e0 in e1 ，以及用于功能应用的空白。
• :
• ∈和∉
• , （左联想）
• ⊢
• 分隔多个命题的空格（关联）
• 横杠

这种语法虽然看起来很复杂，但实际上相当简单。基本思想来自形式逻辑：整个表达是一种含义，上半部分是假设，下半部分是结果。也就是说，如果你知道顶部表达式是真的，你可以得出结论底部表达式也是真的。

符号

另外要记住的是，有些字母具有传统意义; 特别是，Γ代表你所处的 “背景” - 即你所看到的其他类型的东西。所以像Γ ⊢ ...意味着 “表达式...当你知道Γ中每个表达式的类型时。

⊢符号实质上意味着你可以证明某些东西。所以Γ ⊢ ...是一份声明说：“我可以证明...在上下文Γ 。这些声明也被称为类型的判断。

另外要记住的是：在数学中，就像 ML 和 Scala 一样， x : σ表示x类型为σ 。您可以像 Haskell 的x :: σ一样阅读它。

每条规则的含义

所以，知道这一点，第一个表达式变得很容易理解：如果我们知道x : σ ∈ Γ （即x已某种类型的σ在某些情况下Γ ），那么我们就知道Γ ⊢ x : σ （即，在Γ ， x具有类型σ ）。所以真的，这并没有告诉你任何超级有趣的东西; 它只是告诉你如何使用你的上下文。

其他规则也很简单。例如，拿[App] 。该规则有两个条件： e₀是从某种类型τ到某种类型τ'的函数， e₁是类型τ的值。现在你知道你将通过应用获得什么类型的e₀到e₁ ！希望这不是一个惊喜:)。

下一个规则有一些新的语法。特别地， Γ, x : τ仅表示由Γ和判断x : τ组成的上下文。因此，如果我们知道变量x的类型为τ且表达式e的类型为τ' ，我们也知道采用x并返回e的函数的类型。这只是告诉我们如果我们弄清楚函数采用什么类型以及它返回什么类型该怎么做，所以它也不应该令人惊讶。

下一个只是告诉你如何处理let语句。如果你知道有些表达e₁的类型为τ只要x有一个类型σ ，然后let表达式，局部结合x到类型的值σ将会使e₁有一个类型τ 。实际上，这只是告诉你一个 let 语句本质上允许你用一个新的绑定扩展上下文 - 这正是let做的！

[Inst]规则处理子类型。它说的是，如果你有类型的值σ' ，它是一个子类型的σ （ ⊑表示偏序关系），那么表达式也是类型σ 。

最终规则涉及泛化类型。快速搁置：自由变量是一个变量，它不是由某个表达式中的 let 语句或 lambda 引入的; 这个表达式现在依赖于来自其上下文的自由变量的值。规则是说如果在你的上下文中有任何变量α 不是 “自由” 的，那么可以肯定地说任何类型为你的表达式知道e : σ将具有任何 α值的类型。

如何使用规则

那么，既然您已了解符号，那么您对这些规则有何看法？好吧，您可以使用这些规则来确定各种值的类型。为此，请查看您的表达式（例如fxy ）并找到一个与您的语句匹配的结论（底部）的规则。让我们称之为你想要找到你的 “目标”。在这种情况下，你会看到以e₀ e₁结尾的规则。当你发现这一点时，你现在必须找到规则，证明这条规则的所有内容。这些东西通常对应于子表达式的类型，因此您实际上是对表达式的某些部分进行递归。您只需执行此操作，直到完成校对树，这样可以证明表达式的类型。

因此，所有这些规则都是精确地指定 - 并且在通常的数学上迂腐的细节：P - 如何找出表达式的类型。

现在，如果您曾经使用 Prolog，这应该听起来很熟悉 - 您实际上是像人类 Prolog 解释器一样计算证明树。 Prolog 被称为 “逻辑编程” 是有原因的！这也很重要，因为我介绍 HM 推理算法的第一种方法是在 Prolog 中实现它。这实际上非常简单，并且清楚地表明了这一点。你当然应该尝试一下。

注意：我可能在这个解释中犯了一些错误，并且如果有人指出它们会很喜欢它。我实际上会在几周内在课堂上报道，所以我会更自信：P。

如果有人能够至少告诉我从哪里开始想要理解这个符号海洋意味着什么

参见 “ 编程语言的实用基础 ”，第 2 章和第 3 章，通过判断和推导来讨论逻辑风格。整本书现已在亚马逊上市。

第 2 章

归纳定义

归纳定义是编程语言研究中不可或缺的工具。在本章中，我们将开发归纳定义的基本框架，并举例说明它们的使用。归纳定义包括一组用于推导各种形式的判断或断言的规则 。判断是关于指定排序的一个或多个句法对象的陈述。规则规定了判决有效性的必要和充分条件，从而充分确定其含义。

2.1 判决

我们从判断的概念开始，或者关于句法对象的断言 。我们将利用多种形式的判断，包括以下例子：

• n nat - n是一个自然数
• n = n1 + n2 -n是n1和n2之和
• τ 型 - τ是一种类型
• e ： τ - 表达式e具有类型τ
• ë⇓N - 表达式e具有值v

判断表明一个或多个句法对象具有彼此某种关系的属性或立场。财产或关系本身被称为判断形式 ，并且一个或多个对象在该关系中具有该属性或立场的判断被认为是该判断形式的实例 。判断形式也称为谓词 ，构成实例的对象是其主语 。我们为判断断言J持有a 而写了一个 J.当强调判断的主题并不重要时，（文字在这里切断）