欣德利你不明白吗？“
我现在找不到它，但我发誓曾经是一件出售不朽字的T恤衫：
什么部分
难道你不明白？
就我而言，答案就是......全部！
特别是，我经常在Haskell论文中看到这样的符号，但我不知道它的含义。 我不知道它应该是什么数学分支。
当然，我认识到希腊字母的字母，以及诸如“∉”之类的符号（通常意味着某物不是集合中的一个元素）。
另一方面，我从未见过“⊢”（维基百科声称它可能意味着“分区”）。 我也不熟悉在这里使用vinculum。 （通常它表示一个分数，但在这里并不是这种情况。）
我想，SO不是解释整个Milner Hindley算法的好地方。 但是如果有人能够告诉我从哪里开始寻求理解这个符号之海意味着什么，那将是有益的。 （我相信我不会是唯一想知道的人......）
:意味着有类型 ∈装置是英寸 （同样∉表示“不在”）。 Γ通常用于指代环境或上下文; 在这种情况下，可以将其视为一组类型注释，将标识符与其类型配对。 因此x : σ ∈ Γ表示环境Γ包括x具有类型σ的事实。 ⊢可以被读作证明或确定。 Γ ⊢ x : σ意味着环境Γ确定x具有类型σ 。 ,是包括具体的附加假设到环境中的一种方式Γ 。 因此，
Γ, x : τ ⊢ e : τ'表示环境Γ ，并且附加的重写假设x具有类型τ ，证明e具有类型τ' 。 这个语法虽然看起来很复杂，但其实很简单。 基本思想来自逻辑：整个表达式的含义是上半部分是假设，下半部分是结果。 也就是说，如果你知道顶部表达式是真的，你可以得出结论底部表达式也是真实的。
符号
另外要记住的是，一些字母具有传统意义， 特别是，Γ代表你所处的“背景” - 也就是说，你所看到的其他事物的类型。 所以像Γ ⊢ ...这样的东西就意味着“表达...当你知道Γ中每个表达的类型。
该⊢符号实质上意味着，你可以证明一些东西。 所以Γ ⊢ ...是一个声明，说“我可以证明...在上下文中Γ 。这些陈述也称为类型判断。
还有一点需要注意：在数学中，就像ML和Scala一样， x : σ意味着x类型为σ 。 你可以像Haskell的x :: σ一样阅读它。
每条规则的含义
因此，知道这一点，第一个表达式变得容易理解：如果我们知道x : σ ∈ Γ （即， x在某些情况下Γ具有某种类型σ ），那么我们知道Γ ⊢ x : σ （也就是说，在Γ ， x类型为σ ）。 所以真的，这并不是告诉你任何超级有趣的事情; 它只是告诉你如何使用你的上下文。
其他规则也很简单。 例如，拿[App] 。 该规则有两个条件： e₀是从某种类型τ到某种类型τ'的函数， e₁是类型τ的值。 现在你知道通过将e₁ e₀应用于e₁将得到什么类型！ 希望这不是一个惊喜:)。
下一个规则有更多新的语法。 特别地， Γ, x : τ只意味着由Γ和判断x : τ组成的上下文。 因此，如果我们知道变量x的类型为τ ，并且表达式e的类型为τ' ，那么我们也知道函数的类型，它接受x并返回e 。 这只是告诉我们如果我们找出了函数需要什么类型以及它返回什么类型，该怎么做，所以它也不应该是令人惊讶的。
下一个只是告诉你如何处理let语句。 如果你知道只要x有一个类型σ ，那么表达式e₁有一个类型τ ，那么一个将x与σ类型值局部结合的let表达式将使得e₁具有类型τ 。 真的，这只是告诉你一个let语句基本上可以让你用一个新的绑定扩展上下文 - 这正是let做的！
[Inst]规则处理子分类。 它说的是，如果你有类型的值σ' ，它是一个子类型的σ （ ⊑表示偏序关系），那么表达式也是类型σ 。
最终的规则涉及泛化类型。 快速抛开：一个自由变量是一个变量，它不是由let语句或lambda表达式引入的; 这个表达式现在取决于上下文中自由变量的值。规则是说如果在你的上下文中有任何变量α不是“自由”的，那么可以肯定地说任何表达式的类型是你知道e : σ将具有该类型的任何α值。
如何使用规则
所以，现在你明白了这些符号，你对这些规则做了什么？ 那么，你可以使用这些规则来确定各种值的类型。 要做到这一点，看看你的表达式（比如说fxy ），并找到一条与你的陈述相符的结论（底部）。 让我们称之为你试图找到你的“目标”的东西。 在这种情况下，你会看看以e₀ e₁结尾的规则。 当你发现这一点时，你现在必须找到规则来证明这条规则之上的一切。 这些东西通常对应于子表达式的类型，所以你基本上是在表达式的某些部分递归。 你直到你完成你的证明树为止，这会给你一个表达式类型的证明。
因此，所有这些规则都是精确指定的 - 并且在通常的数学迂腐细节中：P-如何计算表达式的类型。
现在，如果你曾经使用过Prolog，这应该听起来很熟悉 - 你基本上像计算人类Prolog解释器那样计算证明树。 Prolog被称为“逻辑编程”是有原因的！ 这也是重要的，因为我首先介绍HM推理算法的第一种方法是在Prolog中实现它。 这实际上非常简单，并且使得事情变得清晰。 你当然应该尝试一下。
注意：我可能在这个解释中犯了一些错误，如果有人指出，我会很喜欢它。 我会在几周内在课堂上讲到这一点，所以我会更有信心：P。
如果有人能够至少告诉我从哪里开始寻求理解这个符号之海意味着什么
参见“ 编程语言的实践基础 ”，第2章和第3章，关于通过判断和派生逻辑的方式。 整本书现在在亚马逊上可用。
第2章
归纳定义
归纳定义是编程语言研究中不可或缺的工具。 在本章中，我们将开发归纳定义的基本框架，并举例说明它们的用法。 归纳定义由一系列用于推导各种形式的判断或断言的规则组成。 判断是关于指定排序的一个或多个语法对象的陈述。 这些规则为判断的有效性指定了必要和充分的条件，因此完全确定了其含义。
2.1判决
我们从判断的概念开始，或者从句法对象的断言开始。 我们将利用多种形式的判断，包括这样的例子：
判断表明，一个或多个语法对象具有一个属性或彼此之间存在某种关系。 财产或关系本身被称为判断形式，并且判断一个或多个物体拥有该财产或站在该关系中，这被认为是该判断形式的一个实例。 判断形式也称为谓词，构成实例的对象是其主语。 我们写的判断断言歼的持有为J。 当强调判断的主题并不重要时，（文中切断）
链接地址: http://www.djcxy.com/p/2285.html