Что входит в написание денотационной функции отображения семантики?

Question

Я немного запутался в понятии денотационной семантики. Как я понимаю, денотационная семантика должна описывать, как функции и выражения работают в определенном языке программирования. Какая именно форма используется для описания этих функций и как они работают? Что такое "домен", и как можно построить функцию отображения?

Как пример, что было бы функцией отображения для "делай X в то время как Y"?

Я читал много материалов в Интернете, но это трудно понять. Будут ли эти описания похожи на контекстно-свободную грамматику?

Пожалуйста, дайте мне знать, спасибо!

Answer 1

Думайте об обозначении как о преобразовании синтаксиса в "значение". Вы, вероятно, увидите, что это написано в двойных скобках, чтобы вы могли читать [[3]] = 3 как "обозначение синтаксиса [число 3] является число 3".

Простой пример - арифметика. Обычно у вас есть такое обозначение, как

[[x + y]] = [[x]] + [[y]]

где + слева синтаксический плюс и + справа арифметический плюс. Чтобы сделать это более понятным, мы можем изменить синтаксис.

[[(+ x y)]] = [[x]] + [[y]]

Теперь чрезвычайно важный вопрос: каков диапазон (кодомен) этого картирования? До сих пор я предполагал, что достаточно рассматривать его как "некий математический домен, где живут числа и сложения", но этого, вероятно, недостаточно. Важно отметить, что ваш пример сломает его быстро.

[[do X while True]] = ???

Поскольку у нас не обязательно есть математический домен, который включает в себя понятие не прекращения.

В Haskell это решается путем вызова математической области "поднятой" областью или областью CPO, которая, по существу, напрямую добавляет отсутствие завершения. Например, если ваш домен unlifted является целыми числами I тогда поднятый домен ⊥ + I где ⊥ называется "дном", и это означает не прекращение.

Это означает, что мы могли бы написать (в синтаксисе Haskell)

[[let omega = 1 + omega in omega]] = ⊥

Boom. У нас есть смысл - смысл бесконечного цикла... вообще ничего!

Хитрость с поднятыми доменами в Haskell заключается в том, что, поскольку Haskell ленив (не строг), возможно иметь интересные взаимодействия типов данных и ⊥, Например, если у нас есть type IntList = Cons Int IntList | Nil затем поднял домен над IntList включает в себя ⊥ напрямую (полный бесконечный цикл), а также такие вещи, как Cons ⊥ ⊥ которые все еще не полностью решены, но предоставляют больше информации, чем старые ⊥,

И я пишу "больше информации" сознательно. CPOs формируют частичный порядок (это PO) "определенности". ⊥ максимально неопределен и поэтому <= к чему-либо еще в СРО. Тогда вы получите такие вещи, как Cons ⊥ ⊥ <= Cons 3 ⊥ которая образует цепочку в вашем частичном порядке. Вы часто тогда говорите, что если x <= y затем "y содержит больше информации, чем x" или же "y более определен, чем x".

Один из самых важных моментов этого для меня заключается в том, что, определяя эту структуру СРО в нашей математической области обозначения, мы можем действительно точно говорить о различиях между строгой и нестрогой оценкой. На строгом языке (или на самом деле, в строгих доменах, в которых ваш язык может иметь или не иметь некоторые из них), все ваши CPO являются "плоскими" в том смысле, что вы либо имеете полностью определенные результаты, либо ⊥ и ничего больше. Лень возникает именно тогда, когда ваш CPO не плоский.

Другим важным моментом является понятие, что "вы не можете сопоставить шаблон снизу"... что, если мы думаем о дне как о бесконечном цикле (хотя с этой новой абстрактной моделью это не обязательно означает, что… это это может быть, например, ошибка (segfault), тогда эта пословица - не что иное, как другой способ выражения проблемы остановки. Это является следствием того, что все разумные функции должны быть "монотонными" в том случае, если x <= y затем f x <= f y, Если вы потратите некоторое время с этим понятием, то увидите, что оно запрещает функции, которые ведут себя по-разному не снизу, независимо от того, являются ли их аргументы низами или нет. Например, остановившийся оракул не является монотонным

halting (⊥) = False     -- we can't pattern match on bottom!
halting _   = True

Но "сломанный оракул остановки"

hahahalting (⊥) = ⊥     -- we're still pattern matching, 
                            -- but at least the behavior is right
hahahalting _   = True

который мы пишем, используя seq

hahahalting x = x `seq` True    -- valid Haskell

Это также приводит к резкому облегчению опасности немонотонных функций, таких как Хаскеллаspoon, Мы можем написать их, воспользовавшись денотально необоснованным перехватом исключений... но это может вызвать очень странное поведение, если мы не будем осторожны.

Есть еще много вещей, которые вы можете извлечь из денотационной семантики, поэтому я предложу заметки Эдварда З. Янга о денотационной семантике.