Связывание (свободных) идентификаторов: абстракция функций - часть 3

f: Mi * ... * Мn

где М, - структуры данных типа si.

В БНФ-нотации получается следующий синтаксис для функций:

<функция>::=<id>| (<абстракция_функции>)

<абстракция_функции>::= (<тип><id> {,<тип><id>} * )<тип>: <выражение>

В классической математической нотации абстракция функции иногда используется в связи с применением функции:

((s1x1, ..., snxn) s: Е) (e1, .... Еn)

где Еi - выражения типа si.

Интерпретация выражения синтаксической единицы <функция> всегда дает отображение. Если f - идентификатор, то отображение, соответствующее идентификатору, определяется конкретизацией, т.е. справедливо

I

Абстракции функций представляют отображения, а не какие-либо простые математические элементы. Вообще не существует никакой СПТ, которая переводилa бы абстракцию функции в однозначную нормальную форму, т. е. чтобы семантически эквивалентные функциональные выражения имели ту же самую нормальную форму. Однако можно указать правила замены термов для вычисления абстракции функции в связи с вызовом функции. Так как при этом вычисляется не само функциональное выражение, а только вызов функции, указываются только правила вычисления для применения функции с вычисленными значениями параметров (вызов значением, "call-by-value").

Если все аргументы еi терминированы, то применение функции в связи с абстракцией функции может быть вычислено по следующим правилам замены термов:

((s1x1, ..., snxn) s: Е) (e1, ..., Еn)

По этому правилу полностью вычисленные выражения в позициях аргументов подставляются в выражение тела абстракции функции. Можно было бы при применении вызова по имени вместо этого подставлять выражения-аргументы в тело Е без их предварительного вычисления. Однако это приводило бы при многократном вхождении хi в Е к многократному вычислению Еi. Впрочем, вызов по имени соответствует следующему простому определению семантической интерпретации:

f(a1, ...,an) =I