帮助理解类型系统的学术符号

Question

我正在尝试理解关于编程语言设计的学术论文(pdf).特别是,它描述了一个名为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".

其余部分很难在不涉及纸张的情况下进行.我衷心地将诺曼拉姆齐对皮尔斯的推荐作为对类型理论的一个很好的介绍.

¹请注意,"推理"和"蕴涵"之间的区别要么是微妙的要么是不存在的 - 哪一个用于惯例,品味和/或细微差别.