В чем разница между значением и обозначением?

В программировании семантики языка, он часто слышал , что люди говорят о означая и денотат . Кажется, они не одинаковы. В чем разница? Связано ли первое с операционной семантикой, а второе - с денотационной семантикой? Спасибо.

«Значение» используется в более широком смысле, чем обозначение.

Первоначальная дихотомия, унаследованная от логики и философии, находится между «смыслом» и «обозначением» (которое философы называют «ссылкой»).

Это различие можно проиллюстрировать на оригинальном примере Фреге. Он отметил, что фразы «утренняя звезда» и «вечерняя звезда» относятся к одному и тому же объекту - планете Венера - но что предложение «утренняя звезда и вечерняя звезда - это одна и та же планета» фактически передает некоторую информацию читателю. Он предположил, что значение именной фразы может выходить за рамки фактического объекта, который он обозначает, включая что-то о том, как он представляет объект, который он обозначает.

$8 \times 7$$56$

При построении денотационной семантики мы пытаемся построить модель языка, в котором неразличимые программы обозначают - ссылаются - на один и тот же математический объект. Цель состоит в том, чтобы упростить рассуждения о поведении программ, поскольку мы можем рассуждать об обозначениях, математических объектах, не беспокоясь о деталях представления программы. Это позволяет нам избежать необходимости иметь дело с аспектами значения программ, которые нам не интересны.

То, как смысл и обозначение относятся к операционной семантике, является более сложным и различным. Я могу расширить свой ответ позже, чтобы покрыть это, но я должен бежать сейчас. :)

РЕДАКТИРОВАТЬ: Хорошо, я расширяю этот ответ сейчас.

Связь между «обозначением» и «ссылкой» в значительной степени точна, и именно потому, что люди, которые изобрели денотационную семантику (например, Скотт и Стрейчи), вполне сознательно воспринимали идеи из философской логики как часть своего проекта.

Чтобы понять, как смысл и операционная семантика связаны, полезно вспомнить понятие философа Майкла Дамметта о «теории смысла» и о том, чем оно отличается от «семантической теории».

В терминологии Даммета семантическая теория - это композиционный способ связывания предложений для определения математических объектов. В логике смысл предложения является его истинностной ценностью, и он определяется из истинностных ценностей его составляющих. В денотационной семантике языков программирования используется гораздо более широкий спектр математических объектов, но она работает аналогично - мы даем значение термина программы в терминах значения его подтерм. Таким образом, в терминологии Даммета денотационная семантика предлагает семантические теории языков программирования.

Смысл-теория также композиционный способ соотнесения предложения к математическим объектам, но кроме того , она содержит изложение того , что оправдывает соотношение между предложением и математическим объектом. Он разработал эту идею, чтобы понять, как интуиционистские математики понимают понятие истины. В частности, они имели композиционный отчет о значении логических связок, но не давали им семантических значений так же, как это делают классические логики. Например, в трактовке интуиционистской логики Брауэра-Хейтинга-Колмогорова истина определяется следующим образом:

• $A \land B$$(p_1, p_2)$$p_1$$A$$p_2$$B$
• $A \vee B$$(i, p)$$i$$0$$1$$i$$0$$p$$A$$i$$1$$p$$B$
• $A \to B$$A$$B$
• $\forall x.\;A(x)$$n$$A(n)$
• $\exists x.\;A(x)$$(n, p)$$n$$p$$A(n)$

$A$$A$

Теперь отметим, что это определение связывает суждения и истинные ценности, но связь должна быть обоснована возможностью дать канонические доказательства.

Операционная семантика входит в картину через это понятие обоснования. Операционная семантика - это просто описание того, что делает абстрактная машина. После того, как мы даем денотационную семантику, мы обычно хотим показать, что денотационная семантика верна операционной семантике. Это свойство называется адекватностью (наряду с полной абстракцией его старшего брата ), и оно в точности равнозначно теории смысла, которая связывает состояния абстрактной машины с денотационными объектами, которая закрыта при сокращении абстрактной машины.

Это на самом деле не вся история, так как я изложил здесь, как соединить операционный и денотационный подходы с помощью модели реализуемости. Теории типов также могут иметь теоретико-доказательную семантику (действительно, именно эта перспектива была тем, что Даммет больше всего интересовало), но я не объяснил эту связь в этом посте.