AG
там есть два основных подхода - small-step и big-step
Size: a a a
2020 April 23
AG
мелкошаговый совсем автоматный, а крупношаговый ближе к денотационной семантике, он более абстрактный, т.е. оставляет технические вещи за кадром отчасти
PS
И на деле оба этих подхода вполне могут использоваться в рамках одного описания, если хочется чтобы получилась компактная запись, без чрезмерного количества правил :)
BD
сейчас будет еще вопрос, ща только найду контекст
BD
type checking rules + type environments (как это описывал Айкен) = оно как с оп семантикой пересекается?
AG
тайпчекер это же предварительный шаг, после парсинга
AG
отсеять семантически невалидные термы
PS
На этот раз я более строго сформулирую. Проверка типов относится к статической семантике языка. Статической — потому что проверка осуществляется во время компиляции.
PS
И для статической, и для динамической семантики может использоваться один и тот же формализм на основе правил переписывания. К тому же в некоторых ЯП граница между статическим и динамическим бывает довольно зыбкой. Но обычно под операционной семантикой подразумевают семантику динамическую.
PS
@clayrat Вы согласны?
AG
BD
ага, а переписывание термов в динамической семантике заканчивается когда? что там является терминалами?
AG
на нормальной форме
AG
заканчивается тогда когда заканчиваются правила :)
AG
это в общем ключевой момент, то для чего ОС и вводится: про систему неплохо бы доказать что она строго нормализующая, т.е. перепись 1) терминирует 2) на нормальной форме
BD
поняль, теперь круто бы поглядеть где-нибудь на работающие примеры сего
AG
примеры доказательства или просто small-step интерпретатора?
BD
примеры интерпретатора
BD
про доказательства примерно понятно
