Описание значений выражений

Как уже упоминалось, существенный интерес представляют два дополняющих описания значения ("семантики") ЯП:

(1) операционная, ориентированная на вычисление значения по форме описания, которая дает алгоритм для вычисления значения выражения;

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

(3)   Форма (1) соответствует операционной семантике, а форма (2) - функциональной. Соответственно этому для выражения в аппликативном языке обе семантики определяются следующим образом:

(1)    семантика подстановки термов, которая представляется через алгоритм подстановок термов, приводящий выражение (при известных дополнительных условиях) в нормальную (примитивную) форму;

(2)    функция интерпретации I, которая отображает выражение ЯП на математические элементы.

При этом предполагается, что заданы "примитивная" вычислительная структура А с сигнатурой ? = (S, F), так что каждый носитель sА типа s в А содержит элемент 1, и система подстановки термов R над ?. В дальнейшем предполагается заданным множество ID идентификаторов. Оно соответствует формальному языку, который связан с синтаксической единицей <id>. Определяются множества D, FCT и Н.

D =def {а

sA:sS}

FCT =def {(f:sA1

x...xsAn> sAn+1): n

 N ^ f строгая ^ (i, 1<= i <=n + 1: siS)}.

D представляет множество элементов данных, FCT - множество функций, а

Н =-def D ^ FCT

есть множество "семантических" элементов, состоящее из множества элементов данных и множества отображений между элементами данных. D есть область значений для семантической интерпретации выражений. Н есть область значений для применяемых позднее конкретизаций.

Для задания операционной семантики будет применяться семантика подстановки термов. К томy же предполагаются заданными правила подстановки термов для термов над сигнатурой примитивных вычислительных структур. Пусть для терма из wЕ определена система R, которая полностью корректна и каждый терм t (с подходящим образом определенной интерпретацией, т.е.
I[t]

 ) переводит в однозначную нормальную форму. Далее предполагается, что терм t с I[t] =  не обладает никаким терминальным вычислением.


Для СПТ устанавливалось, что правила подстановок термов в АПТ могут применяться на любом месте. В противоположность этому для описания операционной семантики ЯП мы применяем такую концепцию подстановки термов, при которой выбор места применения определяется индивидуально. В последующем в выражениях ЯП должно быть целенаправленно установлено, на каком месте выражения ЯП должно быть возможно применение правила. Общая концепция применения ППТ на любом месте была бы неэффективной, так как при известных обстоятельствах благодаря этому упрощались бы термы, значение которых для вычисления результата на самом деле не используется. Однако существенно, что свободное применение правил на любом месте для определенных элементов ЯП приводило бы к незавершающимся вычислениям, тогда как целенаправленное управление применением может гарантировать завершение вычислений. В ЯП обычно встречаются выражения, чье вычисление завершается успешно, т.е. которые имеют значение , хотя они содержат подвыражения, для которых существуют незавершающиеся вычисления, т.е. значение которых =. Общая концепция безусловного применения неизбежно ведет для таких выражений к существованию незавершающихся вычислений.
Поэтому мы нуждаемся в ограниченном понятии применения ППТ. Эти правила должны применяться не в любом месте терма, а только при определенных условиях на подтерм. Для этой цели мы будем применять условные ППТ. Благодаря этому достигается более тонкое управление вычислением значения, т.е. выбор места применения правил в аппликативном выражении ЯП. Говорят также об управляемом потоке.
Пример (управляемое вычисление для нестрогих функций). Мы рассматриваем нестрогую функцию соr (условную or), которая соответствует последовательной дизъюнкции с функциональностью
fеt соr = (bool, bool) bool и таблицей значений:
соr       L           О       
L          L           L         L


О         L           О       
                        
Применяем следующие правила раскрытия:
хz ==> cor(x, y) cor(z, у),
 соr (true, y)  true,
 соr (false, у)  у.
Заметим, что в этом случае раскрытие терма cor(tl, t2) завершается даже тогда, когда завершается только вычисление t1, и дает значение true.
В дальнейшем для каждого элемента языка определяются условные ППТ, которые во взаимодействии с имеющимися для данной вычислительной структуры правилами обеспечивают, что для каждого замкнутого программного выражения t1 (т.е. для каждого программного выражения, которое не зависит от значения конкретизации) с интерпретацией а, система подстановки термов отображает вход t1 в выход t2, причем t2 есть однозначная нормальная форма t1 в соответствии с R. Впрочем, для определенного терма t с интерпретацией  вычисление не будет терминированным. Уместное обращение с такими термами - также дальнейшее основание для введения условных (управляемых) СПТ.

Содержание раздела

---

---