Конспект установочных лекций по комплексному курсу Информатика, Теория информации

       

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


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

Пример (описание функций с помощью выражений с идентификаторами). Под выражением  х * (х + 1) в математике часто понимается такая функция, которая заданное натуральное число отображает в то натуральное число, которое соответствует значению выражения при замене х на заданное число. При этом нет никакой разницы между интерпретациями термов х * (х + 1) и у * (у + 1). Но если х и у являются различными свободными идентификаторами, то интерпретация обоих выражений при заданной подстановке будет, вообще говоря, различна и тем самым выражения не будут семантически эквивалентными. Если выражения должны использоваться для представления функции, которая натуральному числу n

 N ставит в соответствие число п * (п + I), то использование идентификаторов n, х или у не должно иметь каких-либо различий.

Чтобы устранить нежелательную разницу между выражениями из-за "случайного" выбора конкретных идентификаторов, используемых в качестве держателей мест, и чтобы достичь абстрактного вида, в математике часто предпринимается введение обозначения функций; так, функцию (1) f: N

 N можно определить через (2) f(x) = х * (х + 1) для всех х
 N, что,


конечно, полностью равнозначно (3) f(y) = у * (у + 1) для всех у
 N.

Это может быть выражено через явное задание квантора всеобщности:

, (4)
nat х: f(x) = х * (х + 1).

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

В ЯП используется более последовательная нотация вида fet f= (nat x) nat: х * (х + 1), которая объединяет в себе и задание области (1), и определяющее функцию равенство (4). Кроме того, благодаря этому делается ясным, что идентификатор х используется исключительно в качестве держателя мес­та для свободно выбираемого фактического аргумента. При таком способе записи можно полностью проигнорировать введение обозначения f для функции благодаря использованию (в ЯП) записи (nat х) nat: х * (х + 1) как нотационного представления соответствующего отображения. При этом х в функциональном выражении называют уже не свободным,

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

Пусть Е - выражение типа s. Запись

(s1x1,…, snxn) s: Е

называется абстракцией функции, причем x1,…, xn называются формальными параметрами.



Последовательность символов (s1x1,…, snxn)s называется заголовком абстракции функции; она, в частности, задает тип абстракции функции. Тем самым специфицируется, что указанная выше абстракция функции представляет собой функцию вида

М1 * ... *
Мn
М,

причем Мi обозначают носители типа si,. Выражение Е называется телом (англ. body) абстракции функции.

Для каждой заданной конкретизации
 вышеприведенная абстракция функции определяет функцию



f: Mi * ... * Мn
 М,

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

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

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

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

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

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

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

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

I
 [f] =
 (f).

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

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

((s1x1, ..., snxn) s: Е) (e1, ..., Еn)
E[E1/x1, .... Еn/xn]

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

f(a1, ...,an) =I
1[E],



где
1 пусть определено, как выше. Конечно, при этом
 может быть внесено в конкретизацию. Функции могут быть нестрогими.

Итак, вычисление здесь происходит путем простой подстановки еще не переведенных в нормальную форму фактических параметров. Благодаря этому можно в отдельных случаях получить результат, даже когда один из фактических параметров не обладает нормальной формой (например, когда соответствующий формальный параметр в теле Е не встречается). Таким образом, при вызове по имени процесс завершается чаще, чем при вызове значением. Правда, если формальный параметр встречается в теле многократно, то в этом случае он неоднократно будет переводиться в нормальную форму и соответственно должен неоднократно вычисляться. Поэтому вызов по имени менее эффективен.

Абстракция функции представляет собой предписание для вычислений (блок-схему): для каждого набора параметров с помощью абстракции функции предписывается определенная схема вычислений. Если типы параметров и результата функции не должны определяться очень жестко или они устанавливаются по-разному, то для абстракции функции часто пишут без задания типа
х: Е и тогда говорят о
-абстракции.

В связи с абстракциями функции появляются некоторые (вопросы, такие, как связывание и подстановки

идентификаторов. Как уже неоднократно отмечалось, конкретный выбор идентификатора х в абстракции вида
х: Е пли ((m x) n: Е несуществен. Можно х заменить на любой другой идентификатор у, в предположении, что у сам не входит свободно в Е ("нe имеется конфликтов в обозначениях"). Тогда (m y) n: Е[y/x] семантически эквивалентно с вышеприведенным выражением. Систематическое переименование формальных параметров в
-исчислении называют также
-редукцией.

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


В частности, х не должен быть заменяемым в (m x) n: Е. Такое вхождение идентификатора х называется (аналог ситуации с кванторами) связанным вхождением.

Для большей ясности определим более точно, когда идентификатор х в выражение Е входит свободно: идентификатор х наверняка является свободным it выражении Е, ecли имеет место следующее:

·

Е состоит точно из идентификатора х;

·         Е состоит из одною указателя функции f(e1, .... Eт) и х входит свободно по крайней мере в одно из выражений e1, .... Eт

или в функциональное выражение для F;

·         Е есть абстракция функции вида(s1x1, ..snxn) sn+1: Е' и х входит свободно в Е'

и отличается от идентификаторов х; для 1 <=

i <= n;

·         Е имеет вид

if С then E else E'fi

и х входит свободно в С, Е или Е'.

Если х отлично от у и х не является свободным в ЕО, то справедливо

((m х) n:

Е)[ЕО/у] = (m х) n: (Е[ЕО/у]).

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

В абстракции функции (s1x1, ..snxn) sn+1: Е создаются связывания для формальных параметров относительно их вхождения в тело Е. Связывание для идентификатора относится всегда к области связанности или, точнее, к каждому свободному вхождению соответствующего идентификатора в область связанности. Для приведенной выше абстракции функции областью связанности для идентификатора х; является выражение Е.

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

Пример (вложенное связывание). В выражении

(*) (nat х) nat: (((nat х) nat: х * х) (х + 1))

связывание х во внутренней абстракции функции вложено. Выражение (*) равносильно выражению (после переименования х во внутренней области связанности)

(nat х) nat: (((nat у) nat: у * у) (х + 1)).

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

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

(nat х, nat у) nat: if х < у then у else х fi

описывает функцию выбора наибольшего из двух натуральных чисел.

Вычисление полинома (по схеме Горнера) при заданных коэффициентах а0, ..., an

описывается через

(nat х) nat: (...(an * х + an-1) * х + ... + a1) * х + а0.

Формальные параметры являются держателями мест для исходных данных, которые необходимы для выполнения вычислений.


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