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

参见“<强>编程语言的实用基础。”，第2章和第3章，关于通过判断和推导的逻辑风格。整本书是现在在亚马逊上可用。

第2

归纳定义

归纳定义是编程语言研究中不可或缺的工具。在本章中，我们将开发归纳定义的基本框架，并给出一些它们的使用示例。归纳定义由一组规则组成，用于导出各种形式的判决或断言。判断是关于一个或多个指定类型的句法对象的陈述。规则指定了判断有效性的充分必要条件，从而完全确定了它的含义。

2.1判决

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

• nnat-n是自然数
• n=n1+n2-n是n1和n2之和
• τ类型-τ是一个类型
• e：τ-表达式e具有类型τ
• ev-表达式e具有值v

判决表明一个或多个句法对象具有属性或相互之间的某种关系。属性或关系本身被称为判断形式，一个或多个对象具有该属性或在该关系中的地位的判断被称为该判断形式的实例。判断形式也称为谓词，构成实例的对象是它的科目。我们写一个J来表示断言J持有一个的判决。当强调判决的主题不重要时，（此处截断文本）

该符号来自自然演绎。

符号称为旋转栅门。

这六条规则非常简单。

Var规则是相当琐碎的规则-它说如果类型标识符已经存在于您的类型环境中，那么要推断类型，您只需按原样从环境中获取它。

App规则说，如果你有两个标识符e0和e1并且可以推断它们的类型，那么你可以推断应用程序e0 e1的类型。如果你知道e0 :: t0 -> t1和e1 :: t0（相同的t0！），那么应用程序是类型良好的，类型是t1。

Abs和Let是用于推断lambda抽象和let-in类型的规则。

Inst规则表示您可以用不太通用的类型替换类型。

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

符号

另一件需要记住的事情是，一些字母具有传统含义；特别是，γ代表你所处的“上下文”-也就是说，你看到的其他事物的类型是什么。所以像Γ ⊢ ...这样的东西意味着“当你知道Γ中每个表达式的类型时，表达式...。

⊢符号本质上意味着你可以证明某事。所以Γ ⊢ ...是一个语句，说“我可以在上下文Γ中证明...。这些语句也称为类型判断。

另一件事要记住：在数学中，就像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 : σ的表达式都将具有任何值为α的类型。

如何使用规则

那么，现在你已经理解了这些符号，你会怎么处理这些规则呢？嗯，你可以使用这些规则来找出各种值的类型。为此，查看你的表达式（比如f x y）并找到一个具有与你的语句匹配的结论（底部）的规则。让我们称之为你试图找到的“目标”。在这种情况下，你会查看以e₀ e₁结尾的规则。当你找到这一点时，你现在必须找到证明在此规则之上的所有内容的规则。这些东西通常对应于子表达式的类型，所以你本质上是在表达式的某些部分上递归。你只需要这样做，直到你完成你的证明树，它给你一个表达式类型的证明。

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

如果你曾经使用过Prolog，这听起来应该很熟悉——你实际上是在像人类Prolog解释器一样计算证明树。Prolog被称为“逻辑编程”是有原因的！这也很重要，因为我第一次接触H-M推理算法是在Prolog中实现的。这实际上非常简单，并且让事情变得清晰。你一定要试一试。

注意：我可能在这个解释中犯了一些错误，如果有人能指出它们，我会很高兴的。几周后我将在课堂上讨论这个，所以那时我会更有信心： P.

• 单杠表示“[上面]意味着[下面]”。
• 如果[上面]中有多个表达式，那么将它们anded放在一起考虑；为了保证[下面]，所有[上面]必须为真。
• :表示有类型
• ∈表示在。（同样，∉表示“不在”。）
• Γ通常用于引用环境或上下文；在这种情况下，它可以被认为是一组类型注释，将标识符与其类型配对。因此x : σ ∈ Γ意味着环境Γ包括x具有类型σ的事实。
• ⊢可以读作证明或确定。Γ ⊢ x : σ表示环境Γ确定x具有类型σ。
• ,是包括特定附加假设进入环境Γ的一种方式。
  因此，Γ, x : τ ⊢ e : τ'意味着环境Γ，附加的，压倒一切的假设#2具有类型#3证明e具有类型τ'。

按要求：运算符优先级，从最高到最低：

• 特定于语言的中缀和混合修复运算符，例如λ x . e、∀ α . σ和τ → τ'、let x = e0 in e1，以及函数应用程序的空格。
• :
• ∈和∉
• ,（左关联）
• ⊢
• 分隔多个命题的空格（关联）
• 的单杠

有两种方法来考虑e：σ。一种是“表达式e具有类型σ”，另一种是“表达式e和类型σ的有序对”。

视图γ作为关于表达式类型的知识，实现为表达式和类型对的集合，e：σ。

旋转门意味着从左边的知识中，我们可以推断出右边的东西。

因此，第一条规则[Var]可以读取：
如果我们的知识γ包含对e：σ，那么我们可以从γ推断e具有类型σ。

第二条规则[App]可以读取：
如果我们可以推导出e_0的类型 τ → τ', ，我们可以推导出e_1的类型，那么我们可以推导出e_0e_1的类型。

通常写成γ， e：σ，而不写成γ{e：σ}。

因此，第三条规则[Abs]可以读作：
如果我们从用x：τ扩展的γ可以推断出e的类型为τ'，那么我们从γ可以推断出λx. e的类型 τ → τ'.

第四条规则[Let]留作练习。：-）

第五条规则[Inst]可以读作：
如果我们可以推断e的类型为σ'，而σ'是σ的子类型，那么我们可以推断e的类型为σ。

第六条也是最后一条规则[Gen]可以读作：
如果我们可以推导出e具有类型σ，并且α不是任何类型中的自由类型变量，那么我们可以推导出e具有类型 ∀α σ.

如何理解Hindley-Milner规则？

Hindley-Milner是一组相继演算形式的规则（不是自然演绎），它表明我们可以从程序的构造中推断出（最一般的）程序类型，而无需显式的类型声明。

符号和符号

首先，让我们解释符号，并讨论运算符优先级

• 是一个标识符（非正式地，变量名）。

• :表示是一个类型（非正式地，一个实例，或“is-a”）。

• （sigma）是一个变量或函数的表达式。

• 因此：读作“ is-a”

• ≤表示“是一个元素”

• （Gamma）是一个环境。

• （断言符号）表示声称（或证明，但在上下文中“断言”读起来更好。）

• :因此读作"断言， is-a"

• 是类型的实际实例（元素）。

• （tau）是一个类型：基本、变量（）、函数→或产品×'（此处未使用产品）

• →是一个函数类型，其中和``可能是不同的类型。

• .表示（lambda）是一个匿名函数，它接受一个参数并返回一个表达式。

• 让=在在表达式中表示，，在出现的地方替换。

• 表示前一个元素是后一个元素的子类型（非正式的-子类）。

• 是一个类型变量。

• .是一个类型，（对于所有）参数变量，，返回表达式

• 免费（）表示不是外部上下文中定义的自由类型变量的元素。（绑定变量是可替换的。）

线以上的一切都是前提，线以下的一切都是结论（Per Martin-Löf）

优先，通过例子

我从规则中提取了一些更复杂的示例，并插入了显示优先级的冗余括号：

• ：可以写成(𝑥 : 𝜎)

• :可以写成 𝚪 ⊦ (:）

• 游戏让=在：游戏相当于𝚪 ⊦ ((让（=）在）：）

• .：→等价 𝚪 ⊦ ((.）：（→））

然后，分隔断言语句和其他前提条件的大空格表示一组这样的前提条件，最后将前提与结论分开的水平线带来优先顺序的结束。

的规则

接下来是对规则的英文解释，每个解释后面都有松散的重述和解释。

变量

给定是（sigma）的一种类型，（Gamma）的一个元素，

换句话说，在中，我们知道是型，因为是中型。

这基本上是一个重言式。标识符名称是一个变量或一个函数。

功能应用

给定断言是一个函数类型，断言是一个
结论断言应用函数到是一个类型'

为了重申规则，我们知道函数应用程序返回类型'，因为函数具有类型→'并获得类型的参数。

这意味着如果我们知道一个函数返回一个类型，并将其应用于一个参数，结果将是我们知道它返回的类型的实例。

功能抽象

给定和类型断言是一个类型，'
结论断言一个匿名函数，返回表达式的类型是 𝜏→𝜏'.

同样，当我们看到一个接受并返回表达式的函数时，我们知道它是→'类型，因为（a）断言是'。

如果我们知道是类型，因此表达式是类型'，那么返回表达式的函数是类型→'。

让变量声明

给定类型为，和和类型为的断言类型为
结论断言let 𝑥=𝑒₀ in类型

松散地说，在（a）中绑定到，因为是一个，是一个，断言是一个。

这意味着如果我们有一个表达式是一个（变量或函数），还有一个名称，也是一个，以及一个类型的表达式，那么我们可以在中出现的任何地方替换。

实例化

给定类型为'的断言，'是
的子类型结论断言是类型

表达式是父类型，因为表达式是子类型'，而是'的父类型。

如果一个实例的类型是另一个类型的子类型，那么它也是那个超类型的实例——更一般的类型。

泛化

给定断言是和不是的自由变量的元素，
结论断言，键入所有参数表达式返回一个表达式

所以一般来说，对于所有返回的参数变量（），都被键入，因为我们知道是一个而不是一个自由变量。

这意味着我们可以泛化程序以接受未在包含范围中绑定的参数的所有类型（不是非局部的变量）。这些绑定变量是可替换的。

把它们放在一起

给定某些假设（例如没有自由/未定义的变量，已知环境），我们知道以下类型：

• 我们程序的原子元素（变量），
• 函数返回的值（函数应用程序），
• 函数抽象（Function Abstraction）
• let绑定（Let变量声明），
• 实例的父类型（实例化），以及
• 所有表达式（泛化）。

结论

结合这些规则，我们可以证明断言程序的最一般类型，而不需要类型注释。