Семантика (информатика)

Математическое исследование смысла языков программирования

В теории языков программирования семантика — это строгое математическое исследование значения языков программирования . ^[1] Семантика присваивает вычислительное значение допустимым строкам в синтаксисе языка программирования . Оно тесно связано с семантикой математических доказательств и часто пересекается с ней .

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

История

В 1967 году Роберт Флойд опубликовал статью «Присвоение значения программам» ; его главной целью был «строгий стандарт доказательств компьютерных программ, включая доказательства правильности , эквивалентности и прекращения». ^{[2] [3]} Далее Флойд писал: ^[2]

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

В 1969 году Тони Хоар опубликовал статью о логике Хоара , основанную на идеях Флойда, которую теперь иногда все вместе называют аксиоматической семантикой . ^{[4] [5]}

В 1970-х годах появились термины операционная семантика и денотационная семантика . ^[5]

Обзор

Область формальной семантики охватывает все следующее:

• Определение семантических моделей
• Отношения между различными семантическими моделями
• Отношения между различными подходами к смыслу
• Связь между вычислениями и лежащими в их основе математическими структурами из таких областей, как логика , теория множеств , теория моделей , теория категорий и т. д.

Он имеет тесные связи с другими областями информатики, такими как проектирование языков программирования , теория типов , компиляторы и интерпретаторы , верификация программ и проверка моделей .

Подходы

Существует множество подходов к формальной семантике; они относятся к трем основным классам:

• Денотационная семантика , ^[6] при которой каждая фраза в языке интерпретируется как денотат , то есть концептуальное значение, которое можно мыслить абстрактно. Такие обозначения часто представляют собой математические объекты, населяющие математическое пространство, но это не является обязательным требованием. Ввиду практической необходимости денотации описываются с использованием той или иной формы математической нотации, которая, в свою очередь, может быть формализована как денотационный метаязык. Например, денотатационная семантика функциональных языков часто переводит язык в теорию предметной области . Денотационные семантические описания могут также служить композиционными переводами с языка программирования на денотационный метаязык и использоваться в качестве основы для проектирования компиляторов .
• Операционная семантика , ^[7] при которой выполнение языка описывается напрямую (а не посредством перевода). Операционная семантика во многом соответствует интерпретации , хотя опять же «язык реализации» интерпретатора обычно представляет собой математический формализм. Операционная семантика может определять абстрактную машину (такую ​​как машина SECD ) и придавать смысл фразам, описывая переходы, которые они вызывают в состояниях машины. В качестве альтернативы, как и в случае с чистым лямбда-исчислением , операционная семантика может быть определена посредством синтаксических преобразований фраз самого языка;
• Аксиоматическая семантика , ^[8] посредством которой человек придает значение фразам, описываяприменимые к ним аксиомы . Аксиоматическая семантика не делает различия между значением фразы и логическими формулами, которые ее описывают; его значение — это именно то, что можно доказать относительно него с помощью некоторой логики. Каноническим примером аксиоматической семантики является логика Хоара .

Помимо выбора между денотативным, операционным или аксиоматическим подходами, большинство вариаций формальных семантических систем возникает из-за выбора поддерживающего математического формализма. ^{[ нужна цитата ]}

Вариации

Некоторые варианты формальной семантики включают следующее:

• Семантика действий ^[9] — это подход, который пытается модулировать денотационную семантику, разделяя процесс формализации на два уровня (макро- и микросемантика) и предварительно определяя три семантических объекта (действия, данные и элементы получения) для упрощения спецификации;
• Алгебраическая семантика ^[8] — это форма аксиоматической семантики, основанная на алгебраических законах для формальногоописания и рассуждений о семантике программы . Он также поддерживает денотационную и операционную семантику ;
• Грамматики атрибутов ^[10] определяют системы, которые систематически вычисляют « метаданные » (называемые атрибутами ) для различных случаев синтаксиса языка . Грамматики атрибутов можно понимать как денотационную семантику, где целевой язык — это просто исходный язык, обогащенный аннотациями атрибутов. Помимо формальной семантики, грамматики атрибутов также использовались для генерации кода в компиляторах и для дополнения обычных или контекстно-свободных грамматик контекстно -зависимыми условиями;
• Категориальная (или «функториальная») семантика ^[11] использует теорию категорий в качестве основного математического формализма. Обычно доказывается, что категориальная семантика соответствует некоторой аксиоматической семантике, которая дает синтаксическое представление категориальных структур. Кроме того, денотационная семантика часто является примером общей категориальной семантики; ^[12]
• Семантика параллелизма ^[13] — это всеобъемлющий термин для любой формальной семантики, описывающей параллельные вычисления. Исторически важные параллельные формализмы включали модель актора и исчисление процессов ;
• Семантика игр ^[14] использует метафору, вдохновленную теорией игр ;
• Семантика преобразователя предикатов , ^[15] , разработанная Эдсгером В. Дейкстрой , описывает значение фрагмента программы как функцию, преобразующую постусловие в предусловие , необходимое для его установления.

Описание отношений

По ряду причин может возникнуть желание описать отношения между различными формальными семантиками. Например:

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

Также возможно связать множественную семантику через абстракции с помощью теории абстрактной интерпретации . ^{[ нужна цитата ]}

Смотрите также

• Вычислительная семантика
• Формальная семантика (логика)
• Формальная семантика (лингвистика)
• Онтология
• Онтология (информатика)
• Семантическая эквивалентность
• Семантическая технология

Рекомендации

1. Гоген, Джозеф А. (1975). «Семантика вычислений». Теория категорий в применении к вычислениям и управлению . Конспекты лекций по информатике. Том. 25. Спрингер . стр. 151–163. дои : 10.1007/3-540-07142-3_75. ISBN 978-3-540-07142-6.
2. Флойд, Роберт В. (1967). «Придание значения программам» (PDF) . В Шварце, Дж. Т. (ред.). Математические аспекты информатики. Материалы симпозиума по прикладной математике. Том. 19. Американское математическое общество. стр. 19–32. ISBN 0821867288.
3. Кнут, Дональд Э. «Мемориальная резолюция: Роберт В. Флойд (1936–2001)» (PDF) . Мемориалы факультетов Стэнфордского университета . Стэнфордское историческое общество.
4. Хоар, ЦАР (октябрь 1969 г.). «Аксиоматическая основа компьютерного программирования». Коммуникации АКМ . 12 (10): 576–580. дои : 10.1145/363235.363259 . S2CID  207726175.
5. Винскель, Глинн (1993). Формальная семантика языков программирования: введение. Кембридж, Массачусетс: MIT Press. п. хв. ISBN 978-0-262-23169-5.
6. Шмидт, Дэвид А. (1986). Денотационная семантика: методология развития языка . Издательство Уильяма К. Брауна. ISBN 9780205104505.
7. Плоткин, Гордон Д. (1981). Структурный подход к операционной семантике (Отчет). Технический отчет DAIMI FN-19. Кафедра компьютерных наук Орхусского университета .
8. Гоген, Джозеф А .; Тэтчер, Джеймс В.; Вагнер, Эрик Г.; Райт, Джесси Б. (1977). «Начальная семантика алгебры и непрерывные алгебры». Журнал АКМ . 24 (1): 68–95. дои : 10.1145/321992.321997 . S2CID  11060837.
9. Моссес, Питер Д. (1996). Теория и практика семантики действия (Доклад). Отчет БРИКС RS9653. Орхусский университет .
10. Дерансар, Пьер; Журдан, Мартен; Лорхо, Бернар (1988). «Грамматики атрибутов: определения, системы и библиография . Конспекты лекций по информатике 323. Springer-Verlag . ISBN» . 9780387500560.
11. Ловер, Ф. Уильям (1963). «Функториальная семантика алгебраических теорий». Труды Национальной академии наук Соединенных Штатов Америки . 50 (5): 869–872. Бибкод : 1963PNAS...50..869L. дои : 10.1073/pnas.50.5.869 . ПМК 221940 . ПМИД  16591125. 
12. Анджей Тарлецкий; Род М. Берстолл ; Джозеф А. Гоген (1991). «Некоторые фундаментальные алгебраические инструменты для семантики вычислений: Часть 3. Индексированные категории». Теоретическая информатика . 91 (2): 239–264. дои : 10.1016/0304-3975(91)90085-G .
13. Бэтти, Марк; Мемариан, Кайван; Ниенхейс, Киндилан; Пишон-Фарабод, Жан; Сьюэлл, Питер (2015). «Проблема семантики параллелизма языка программирования» (PDF) . Труды Европейского симпозиума по языкам и системам программирования . Спрингер . стр. 283–307. дои : 10.1007/978-3-662-46669-8_12 .
14. Абрамский, Самсон (2009). «Семантика взаимодействия: введение в семантику игры». У Эндрю М. Питтса; П. Дюбьер (ред.). Семантика и логика вычислений. Издательство Кембриджского университета. стр. 1–32. дои : 10.1017/CBO9780511526619.002. ISBN 9780521580571.
15. Дейкстра, Эдсгер В. (1975). «Защищенные команды, неопределенность и формальный вывод программ». Коммуникации АКМ . 18 (8): 453–457. дои : 10.1145/360933.360975 . S2CID  1679242.

дальнейшее чтение

Учебники

• Флойд, Роберт В. (1967). «Придание значения программам» (PDF) . В Шварце, Дж. Т. (ред.). Математические аспекты информатики. Материалы симпозиума по прикладной математике. Том. 19. Американское математическое общество. стр. 19–32. ISBN 0821867288.
• Хеннесси, М. (1990). Семантика языков программирования: элементарное введение с использованием структурной операционной семантики . Уайли. ISBN 978-0-471-92772-3.
• Теннент, Роберт Д. (1991). Семантика языков программирования. Прентис Холл. ISBN 978-0-13-805599-8.
• Гюнтер, Карл (1992). Семантика языков программирования . МТИ Пресс. ISBN 0-262-07143-6.
• Нильсон, HR; Нильсон, Флемминг (1992). Семантика в приложениях: формальное введение (PDF) . Уайли. ISBN 978-0-471-92980-2. Архивировано из оригинала (PDF) 17 апреля 2012 г. Проверено 27 мая 2011 г.
• Винскель, Глинн (1993). Формальная семантика языков программирования: введение . МТИ Пресс. ISBN 0-262-73103-7.
• Митчелл, Джон К. (1995). Основы языков программирования (Постскриптум) .
• Слоннегер, Кеннет; Курц, Барри Л. (1995). Формальный синтаксис и семантика языков программирования. Аддисон-Уэсли. ISBN 0-201-65697-3.
• Рейнольдс, Джон К. (1998). Теории языков программирования . Издательство Кембриджского университета. ISBN 0-521-59414-6.
• Харпер, Роберт (2006). Практические основы языков программирования (PDF) . Архивировано из оригинала (PDF) 27 июня 2007 г.(Рабочий проект)
• Нильсон, HR; Нильсон, Флемминг (2007). Семантика приложений: закуска. Спрингер. ISBN 978-1-84628-692-6.
• Стамп, Аарон (2014). Основы языка программирования . Уайли. ISBN 978-1-118-00747-1.
• Кришнамурти, Шрирам (2012). «Языки программирования: применение и интерпретация» (2-е изд.).

Конспект лекций

• Винскель, Глинн. «Денотационная семантика» (PDF) . Кембриджский университет.

Внешние ссылки

• Ааби, Энтони (2004). Введение в языки программирования. Архивировано из оригинала 19 июня 2015 г.Семантика.