Семантика вычислений
Материал из Википедии — свободной энциклопедии
Семантика вычислений — это определение процесса вычисления в виде последовательности правил перезаписи, которое вместе с представлением о сходимости впервые были использованы в контексте λ-исчисления. Сходимость важна также в системах автоматического доказательства, основанных на эквациональной логике первого порядка.
Содержание |
[править] Операциональная семантика
Операциональная семантика используется для синтаксических понятий языка. В ней функции рассматриваются как текстуальные правильно построенные определения, обеспечивающие апплицирование, а не как функции в математическом понимании этого термина.
[править] Денотационная семантика
Денотационная семантика выражениям в программе ставит в соответствие настоящие математические объекты. Важнейшие, в том числе пионерские, результаты построения таких семантик получены в работах Д. Скотта (D. Scott), который первым построил модель λ-исчисления, основанную на представлении о полном частично упорядоченном множестве}, или, сокращенно, п.ч.у. Для этого им были использованы функции, непрерывные на п.ч.у.
[править] Развитие семантики
Предметом постоянного интереса и исследования является построение систем доказательства корректности, или правильности программ. Наиболее разработанными оказались системы доказательства для случая корректности функциональных программ, которые восходят к системе LCF Р. Милнера (R. Milner) и системе Р. Бойера и Дж. Мура (R. Boyer and J. Moore).
Проводимые в настоящее время исследования сосредоточены на построении систем, основанных на конструктивной логике и установлении аналогии между программами и доказательствами. Существенно, что как программы, так и доказательства рассматриваются погруженными в λ-исчисление с типами, которое является формальной системой высших порядков. Тем самым обеспечивается возможность строить только таким программы, которые завершаются. Одной из подобных систем является система Coq.
В существующих языках используются различные подходы к построению стратегии вычисления значения. В языках семейства ML, а также в Scheme применяется вычисление по значению в варианте, допускающем использование не обязательно функциональных конструкций. В других языках используются отложенные вычисления, которые часто также называют ленивыми вычислениями. Механизмы такого рода использованы в языках Miranda и Haskell.
[править] См. также
- Семантика в программировании
- Лямбда-исчисление
- Лямбда-исчисление с типами
- Аппликативный компьютинг
- Аппликативные вычислительные системы
- Подстановка
[править] Литература
- Вольфенгаген В. Э. Конструкции языков программирования. Приемы описания. — М: АО «Центр ЮрИнфоР», 2001. — 276 с ISBN 5-89158-079-9.
