Семантика вычислений

Семантика вычислений — это определение процесса вычисления в виде последовательности правил перезаписи, которое вместе с представлением о сходимости впервые были использованы в контексте $\lambda$-исчисления. Сходимость важна также в системах автоматического доказательства, основанных на эквациональной логике первого порядка.

Операционная семантика

Основная статья: :en:Operational semantics

Операционная семантика (англ. operational semantics) используется для синтаксических понятий языка. В ней функции рассматриваются как текстуальные правильно построенные определения, обеспечивающие применение к аргументу, а не как функции в математическом понимании этого термина.

Денотационная семантика

Основная статья: :en:Denotational semantics

Денотационная семантика (англ. denotational semantics) выражениям в программе ставит в соответствие настоящие математические объекты, то есть, выражения обозначают (англ. to denote — откуда «денотационная») их величины^[1]. Важнейшие, в том числе пионерские, результаты построения таких семантик получены в работах Д. Скотта (D. Scott), который первым построил модель $\lambda$-исчисления, основанную на представлении о полном частично упорядоченном множестве. Для этого им были использованы функции, непрерывные на таком множестве.

Развитие семантики

Предметом постоянного интереса и исследования является построение систем доказательства корректности, или правильности программ. Наиболее разработанными оказались системы доказательства для случая корректности функциональных программ, которые восходят к системе LCF Робина Милнера и системе Р. Бойера (R. Boyer) и Дж. Мура (J. Moore).

Проводимые в настоящее время исследования сосредоточены на построении систем, основанных на конструктивной логике и установлении аналогии между программами и доказательствами. Существенно, что как программы, так и доказательства рассматриваются погруженными в $\lambda$-исчисление с типами, которое является формальной системой высших порядков. Тем самым обеспечивается возможность строить только такие программы, которые завершаются. Одной из подобных систем является система Coq.

В существующих языках используются различные подходы к построению стратегии вычисления значения. В языках семейства ML, а также в Scheme применяется вычисление по значению в варианте, допускающем использование не обязательно функциональных конструкций. В других языках используются отложенные вычисления, которые часто также называют ленивыми вычислениями. Механизмы такого рода использованы в языках Miranda и Haskell.

См. также

• Семантика (программирование)
• Лямбда-исчисление
• Лямбда-исчисление с типами
• Аппликативный компьютинг
• Аппликативные вычислительные системы
• Подстановка

Примечания

1. ↑ Филд А., Харрисон П. Функциональное программирование = Functional Programming. — М.: Мир, 1993. — С. 593-594. — 637 с. — ISBN 5-03-001870-0

Литература

• Вольфенгаген В. Э. Конструкции языков программирования. Приемы описания. — М: АО «Центр ЮрИнфоР», 2001. — 276 с. ISBN 5-89158-079-9