Помогите понять академическую нотацию для системы типов

Question

Я пытаюсь понять академическую статью (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».

Остальную часть трудно ухватить, не врываясь в бумагу. Я от всего сердца рекомендую Пирса от Нормана Рэмси как хорошее введение в теорию типов.

¹ Обратите внимание, что различие между «умозаключением» и «влечением» является либо тонким, либо вообще отсутствует - какой из них использовать, если это вопрос обычного, вкусового и / или тонкого различия.

Answer 2

Учебник для студентов Бенджамина Пирса Типы и языки программирования научит вас всему, что вам нужно знать, чтобы понять нотации, используемые в полулегком Java-документе. (Я думаю, что Пирс может быть соавтором этой газеты.)

Answer 3

Выглядит как формальная семантика , и в этом случае синтаксиса возможно денотационная семантика , но некоторые символы выглядят довольно загадочно.