java - 类型系统的学术符号

Question

我正在尝试理解 academic paper (pdf) 关于编程语言设计。特别是，它描述了 Java 的轻量级版本，称为 Featherweight 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作为类型理论的一个很好的介绍。

1 请注意，“推论”和“蕴含”之间的区别要么很微妙，要么根本不存在——在哪里使用哪一个取决于惯例、品味和/或细微差别。