B
Есть динамическая семантика языка L, которая выражается в metaL
Size: a a a
2021 April 27
B
Языки и метаязыки понимаются в терминологии Тарского
AT
Ну, т.е. не верно, что логическая/динамическая семантика (обязательно) выражается на метаязыке? По крайней мере в контексте PLT?
B
Притормози
B
Есть требование на metaL — он должен быть выразительнее L
B
В данном случае L — это META II
B
metaL — это некоторый язык, который описывает динамическую семантику META II, или, проще, модель её вычислений
B
Именно относительно того, что можно можно синтаксически вывести в L (в вашей терминологии — в статической семантике L), но нельзя вывести в metaL относительно уже его синтаксических правил (для L это семантические правила, в вашей терминологии — правила динамической семантики, или модели вычислений), говорят о том, что L является unsound
AT
Тогда в каком смысле он "мета"?
B
Проще говоря, если в L мы можем получить то, что тип такого-то выражения будет строкой, но при этом тип этого выражения на самом деле (т.е. так получится в metaL) будет числом, т.е. вычислится число, а не строка — то L unsound
B
В совершенно естественном и традиционном смысле, который ввёл Тарский
AT
Which is... ? 😊
B
Родитель теории моделей
AT
Я знаю who is mr. Tarskiy, я спрашиваю про его определение мета-языка. 😊
B
Эм. Это язык, который должен описывать модель предметного языка.
МБ
В М2 типов нет. Вы пытаетесь логическую терминологию применить к вычислительной практике. А в этой практике у всякого языка уже есть семантика, на которой можно строить другую семантику.
B
Не важно, есть типы или нет
B
Есть ЯП, построенные, например, на нетипизированном лямбда-исчислении
МБ
Ну, просто, sound или unsound тут не играет роли.
B
Ну вообще практическую роль это имеет, но я ввёл это вам для разъяснения, что такое metaL и что такое L