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

Ответ 1

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

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

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

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

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

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

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

Поскольку у нас не обязательно есть область mathy, которая включает в себя концепцию non-term.

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

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

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

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

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

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

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

Еще один важный момент - это понятие о том, что "вы не можете сопоставлять совпадение по дну"... что, если мы думаем о дне как о бесконечном цикле (хотя с этой новой абстрактной моделью это не должно означать этого... это может быть segfault, например), то эта поговорка - не что иное, как другой способ выражения проблемы с остановкой. Следствием этого является то, что все разумные функции должны быть "монотонными" в том случае, если x <= y then 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

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

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