类型系统的学术符号

Question

我正在试着理解一本关于编程语言设计的academic paper。特别是，它描述了一个名为Featherweight Java的轻量级Java版本。它有如下表示法的类型规则：

x_ : C_, this : C |- e0 : E0         E0 <: C0
class C extends D {...}
if mtype(m,D) = D_->D0, then C_ = D_ and C0 = D0
---------------------------------------------------------------------------
C0 m(C_ x_){ return e0; } OK IN C

无论如何，这是我在文本中重现它的最好的尝试。然而，这篇论文似乎假设这样的符号是熟悉的，几乎不能解释它。有人能给我指出一个更好的解释吗？

Answer 1

这是一个特别复杂的例子，里面有几个独立的东西。

水平条符号通常用于推理规则。线上是前提(通常由一行上的空格分隔)，线下是结论。例如，

P0   P1   ...   Pn
------------------
        C

意思是“如果P0到Pn都成立，那么我们可以得出结论，C也成立。”

旋转门符号(⊦)通常用于表示蕴涵关系。在类型系统中，这通常意味着“如果我们假设类型位于左侧，我们可以派生右侧的类型”。冒号通常用于将变量或表达式与类型相关联，因此

x_ : C_, this : C ⊦ e0 : E0

意味着“假设x_具有类型C_，而this具有类型C，我们可以推导出e0具有类型E0。”

符号<:通常用于子类型关系，但这应该在论文中明确定义。

"class C extends D“位似乎指的是源程序的语法。也就是说，预期的前提是“显式声明C以扩展D”。

在不涉足这篇论文的情况下，很难摸索到剩下的部分。我由衷地赞同Norman Ramsey推荐的Pierce，认为它是类型理论的一个很好的介绍。

²请注意，“推理”和“蕴涵”之间的区别要么微妙，要么根本不存在-在哪里使用哪一个是惯例、品味和/或细微区别的问题。

Answer 2

本杰明·皮尔斯的本科生教科书Types and Programming Languages将教你理解Featherweight Java论文中使用的符号所需了解的一切。(我认为皮尔斯可能也是这篇论文的合著者。)

Answer 3

看起来像formal semantics，在这种语法情况下可能是denotational semantics，但有些符号看起来非常神秘。