Что такое денотационная семантика?
Я ищу точное и понятное определение. Те, что я нашел, отличаются друг от друга:
- Из книги по функциональному реактивному программированию
Денотационная семантика - это математическое выражение формального значения языка программирования.
- Тем не менее, Википедия относится к ней как к подходу, а не как математическое выражение.
Денотационная семантика - это подход формализации значений языков программирования путем создания математических объектов (называемых денотациями), которые описывают значения выражений из языков.
2 ответа
Термин "денотационная семантика" относится как к математическим значениям программ, так и к подходу придания таких значений программам. Это как, скажем, слово "история", что означает историю чего-либо, а также всю область исследования истории вещей.
Я никогда не находил определения термина "денотационная семантика" полезными для понимания концепции и ее значения. Скорее, я думаю, что к нему лучше всего подходить, рассматривая формы рассуждений, которые допускает денотационная семантика.
В частности, денотационная семантика делает возможным эквациональное рассуждение с помощью ссылочно-прозрачных программ. Википедия дает это вводное определение ссылочной прозрачности:
Выражение называется прозрачным по ссылкам, если его можно заменить значением, не изменяя поведение программы (другими словами, получая программу с такими же эффектами и выходными данными на одном входе).
Но более точное определение не будет говорить о замене выражения "значением", а скорее о замене его другим выражением. Тогда ссылочная прозрачность - это свойство, при котором, если вы заменяете детали заменами, которые имеют одинаковое обозначение, то итоговые целые также имеют такое же обозначение.
Итак, IMHO, как программист, это ключевой момент для понимания: денотационная семантика - это то, как дать математические "зубья" понятию ссылочной прозрачности, чтобы мы могли дать принципиальные ответы на утверждения о правильности подстановки. Например, в контексте функционального программирования одним из ключевых приложений является: когда мы можем сказать, что два функционально-значимых выражения фактически обозначают "одну и ту же" функцию и, таким образом, одно из них может безопасно заменить другое? Классическим денотационным ответом является экстенсиональное равенство: две функции равны тогда и только тогда, когда они отображают одни и те же входные данные на одни и те же выходные данные, поэтому нам просто нужно доказать, обозначают ли рассматриваемые выражения экстенсивно эквивалентные функции. Так, например, Quicksort и Bubblesort - это существенно разные аргументы, но, по сути, они представляют собой одну и ту же функцию.
В контексте реактивного программирования большой вопрос будет: когда мы можем сказать, что два разных выражения, тем не менее, обозначают один и тот же поток событий или значение, зависящее от времени?