The horizontal bar means that "[above] implies [below]". If there are multiple expressions in [above], then consider them anded together; all of the [above] must be true in order to guarantee the [below]. : means has type ∈ means is in. (Likewise ∉ means "is not in".) Γ is usually used to refer to an environment or context; in this case it can be thought of as a set of type annotations, pairing an identifier with its type. Therefore x : σ ∈ Γ means that the environment Γ includes the fact that x has type σ. ⊢ can be read as proves or determines. Γ ⊢ x : σ means that the environment Γ determines that x has type σ. , is a way of including specific additional assumptions into an environment Γ. Therefore, Γ, x : τ ⊢ e : τ' means that environment Γ, with the additional, overriding assumption that x has type τ, proves that e has type τ'.

按请求:操作符优先级，从最高到最低:

特定于语言的中缀和混合运算符，例如λ x。E，∀α。σ， τ→τ'，令e1中的x = e0，函数应用为空白。 ： ∈和结果 (left-associative) ⊢ 分隔多个命题的空格(关联) 单杠

The horizontal bar means that "[above] implies [below]". If there are multiple expressions in [above], then consider them anded together; all of the [above] must be true in order to guarantee the [below]. : means has type ∈ means is in. (Likewise ∉ means "is not in".) Γ is usually used to refer to an environment or context; in this case it can be thought of as a set of type annotations, pairing an identifier with its type. Therefore x : σ ∈ Γ means that the environment Γ includes the fact that x has type σ. ⊢ can be read as proves or determines. Γ ⊢ x : σ means that the environment Γ determines that x has type σ. , is a way of including specific additional assumptions into an environment Γ. Therefore, Γ, x : τ ⊢ e : τ' means that environment Γ, with the additional, overriding assumption that x has type τ, proves that e has type τ'.

按请求:操作符优先级，从最高到最低:

特定于语言的中缀和混合运算符，例如λ x。E，∀α。σ， τ→τ'，令e1中的x = e0，函数应用为空白。 ： ∈和结果 (left-associative) ⊢ 分隔多个命题的空格(关联) 单杠

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

符号

另一件要记住的事情是，有些字母有传统意义;特别是，Γ表示您所处的“上下文”，即您所看到的其他事物的类型。比如Γ⊢……意思是“表达……当您知道Γ中每个表达式的类型时。

⊢符号本质上意味着你可以证明一些东西。所以Γ⊢…这句话的意思是“我可以证明……”在Γ上下文中。这些陈述也被称为类型判断。

另一件需要记住的事情是:在数学中，就像ML和Scala一样，x: σ意味着x具有类型σ。你可以像Haskell的x:: σ一样读取它。

每条规则的含义

因此，知道了这一点，第一个表达式就容易理解了:如果我们知道x: σ∈Γ(即，x在某些上下文中Γ有某种类型σ)，那么我们就知道Γ⊢x: σ(即，在Γ中，x有类型σ)。实际上，这并没有告诉你什么特别有趣的事情;它只是告诉你如何使用上下文。

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

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

下一个告诉你如何处理let语句。如果您知道某个表达式e₁的类型是τ，只要x的类型是σ，那么let表达式将x局部绑定到σ类型值将使e₁的类型是τ。实际上，这只是告诉您，let语句本质上允许您使用新绑定扩展上下文—这正是let所做的!

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

最后一条规则处理泛化类型。顺便说一句:自由变量是指表达式中没有由let语句或lambda引入的变量;这个表达式现在依赖于上下文中自由变量的值。这个规则说的是，如果在你的上下文中有某个变量α不是“自由的”，那么可以肯定地说，任何表达式，其类型你知道e: σ，对于α的任何值都有该类型。

如何使用规则

So, now that you understand the symbols, what do you do with these rules? Well, you can use these rules to figure out the type of various values. To do this, look at your expression (say f x y) and find a rule that has a conclusion (the bottom part) that matches your statement. Let's call the thing you're trying to find your "goal". In this case, you would look at the rule that ends in e₀ e₁. When you've found this, you now have to find rules proving everything above the line of this rule. These things generally correspond to the types of sub-expressions, so you're essentially recursing on parts of the expression. You just do this until you finish your proof tree, which gives you a proof of the type of your expression.

因此，所有这些规则所做的就是精确地指定——并且以通常的数学迂腐的细节——如何计算表达式的类型。

现在，如果您曾经使用过Prolog，那么这听起来应该很熟悉——您实际上是像人类Prolog解释器一样计算证明树。Prolog被称为“逻辑编程”是有原因的!这一点也很重要，因为我接触H-M推理算法的第一种方式是在Prolog中实现它。这实际上非常简单，并且清楚地说明了发生了什么。你当然应该试试。

注意:我可能在这个解释中犯了一些错误，如果有人能指出来，我会很高兴的。我会在几周后的课上讲到这个，到时我会更有信心，P。

这个符号来自自然演绎法。

⊢的标志被称为旋转门。

这6条规则非常简单。

Var规则是一个非常简单的规则——它说，如果类型环境中已经存在标识符的类型，那么要推断出类型，只需从环境中原样获取它。

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

Abs和Let是用来推断lambda-abstraction和Let -in类型的规则。

Inst规则说你可以用一个不那么通用的类型来代替一个类型。

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

将Γ视为关于表达式类型的知识，实现为表达式和类型对的集合，e: σ。

旋转门⊢意味着从左边的知识，我们可以推断出右边的是什么。

第一个规则[Var]可以这样理解: 如果我们的知识Γ包含对e: σ，那么我们可以从Γ推导出e的类型是σ。

第二条规则[App]可读为: 如果我们从Γ可以推断出e_0的类型是τ→τ'，我们从Γ可以推断出e_1的类型是τ，那么我们从Γ可以推断出e_0 e_1的类型是τ'。

通常写成Γ e: σ而不是Γ∪{e: σ}。

因此，第三条规则[Abs]可以理解为: 如果我们从Γ扩展x: τ可以推断出e具有类型τ'，那么我们从Γ可以推断出λx。E的类型是τ→τ'。

第四条规则[Let]留作练习。: -)

第五条规则[Inst]可读为: 如果我们从Γ可以推导出e的类型是σ'， σ'是σ的子类型，那么我们从Γ可以推导出e的类型是σ。

第六条也是最后一条规则[Gen]可读为: 如果我们从Γ可以推导出e的类型为σ，而α在Γ中的任何类型中都不是自由类型变量，那么我们从Γ可以推导出e的类型为∀α σ。

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

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

第二章

归纳定义

Inductive definitions are an indispensable tool in the study of programming languages. In this chapter we will develop the basic framework of inductive definitions, and give some examples of their use. An inductive definition consists of a set of rules for deriving judgments, or assertions, of a variety of forms. Judgments are statements about one or more syntactic objects of a specified sort. The rules specify necessary and sufficient conditions for the validity of a judgment, and hence fully determine its meaning.

2.1判断

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

N NAT - N为自然数 N = n1 + n2 - N是n1和n2的和 τ类型- τ是一个类型 E: τ -表达式E的类型为τ E⇓v -表达式E的值为v

A judgment states that one or more syntactic objects have a property or stand in some relation to one another. The property or relation itself is called a judgment form, and the judgment that an object or objects have that property or stand in that relation is said to be an instance of that judgment form. A judgment form is also called a predicate, and the objects constituting an instance are its subjects. We write a J for the judgment asserting that J holds of a. When it is not important to stress the subject of the judgment, (text cuts off here)